diff options
| -rw-r--r-- | parsing/printer.ml | 1 | ||||
| -rw-r--r-- | parsing/printer.mli | 1 | ||||
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_coercion.ml | 19 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 13 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 123 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 8 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 53 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 13 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 46 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 28 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/unification.ml | 8 | ||||
| -rw-r--r-- | proofs/clenv.ml | 3 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 20 | ||||
| -rw-r--r-- | proofs/logic.ml | 5 | ||||
| -rw-r--r-- | proofs/proofview.ml | 3 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 53 |
18 files changed, 144 insertions, 258 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 27dcffceae..f1f5d4c9f3 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -120,7 +120,6 @@ let pr_global_env = pr_global_env let pr_global = pr_global_env Idset.empty let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) -let pr_existential_key evk = str (string_of_existential evk) let pr_existential env ev = pr_lconstr_env env (mkEvar ev) let pr_inductive env ind = pr_lconstr_env env (mkInd ind) let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr) diff --git a/parsing/printer.mli b/parsing/printer.mli index 6a256bd599..ca91cfd4f6 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -76,7 +76,6 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds val pr_global : global_reference -> std_ppcmds val pr_constant : env -> constant -> std_ppcmds -val pr_existential_key : existential_key -> std_ppcmds val pr_existential : env -> existential -> std_ppcmds val pr_constructor : env -> constructor -> std_ppcmds val pr_inductive : env -> inductive -> std_ppcmds diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 5e574ce538..4f8344745e 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -1576,7 +1576,7 @@ let constr_of_pat env isevars arsign pat avoid = in let neq = eq_id avoid id in (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid - with NotUnifiable _ -> sign, 1, avoid + with Reduction.NotConvertible -> sign, 1, avoid in (* Mark the equality as a hole *) pat', sign, lift i app, lift i apptype, realargs, n + i, avoid diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 2610ed4ed7..5a2d840570 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -112,7 +112,7 @@ module Coercion = struct try isevars := the_conv_x_leq env x y !isevars; None - with NotUnifiable _ -> coerce' env x y + with Reduction.NotConvertible -> coerce' env x y and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in let dest_prod c = @@ -129,12 +129,12 @@ module Coercion = struct let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co - with NotUnifiable _ -> + with Reduction.NotConvertible -> let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in let _ = try isevars := the_conv_x_leq env eqT eqT' !isevars - with NotUnifiable _ -> raise NoSubtacCoercion + with Reduction.NotConvertible -> raise NoSubtacCoercion in (* Disallow equalities on arities *) if Reduction.is_arity env eqT then raise NoSubtacCoercion; @@ -323,7 +323,6 @@ module Coercion = struct (* appliquer le chemin de coercions de patterns p *) exception NoCoercion - exception NoCoercionNoUnifier of evar_map * unification_error let apply_pattern_coercion loc pat p = List.fold_left @@ -419,12 +418,12 @@ module Coercion = struct with Not_found -> raise NoCoercion in try (the_conv_x_leq env t' c1 evd, v') - with NotUnifiable _ -> raise NoCoercion + with Reduction.NotConvertible -> raise NoCoercion let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = try (the_conv_x_leq env t c1 evd, v) - with NotUnifiable (best_failed_evd,e) -> + with Reduction.NotConvertible -> try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match @@ -448,7 +447,7 @@ module Coercion = struct let t2 = Termops.subst_term v1 t2 in let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') - | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) + | _ -> raise NoCoercion (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) = @@ -459,12 +458,12 @@ module Coercion = struct inh_conv_coerce_to_fail loc env evd rigidonly (Some (nf_evar evd cj.uj_val)) (nf_evar evd cj.uj_type) (nf_evar evd t) - with NoCoercionNoUnifier (best_failed_evd,e) -> + with NoCoercion -> let sigma = evd in try coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t with NoSubtacCoercion -> - error_actual_type_loc loc env sigma cj t e + error_actual_type_loc loc env sigma cj t in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) @@ -491,7 +490,7 @@ module Coercion = struct in try fst (try inh_conv_coerce_to_fail loc env' isevars false None t t' - with NoCoercionNoUnifier _ -> + with NoCoercion -> coerce_itf loc env' isevars None t t') with NoSubtacCoercion -> error_cannot_coerce env' isevars (t, t')) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index bedd3eb749..5503a147a6 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -79,7 +79,6 @@ end module Default = struct (* Typing operations dealing with coercions *) exception NoCoercion - exception NoCoercionNoUnifier of evar_map * unification_error (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = @@ -187,11 +186,11 @@ module Default = struct with Not_found -> raise NoCoercion in try (the_conv_x_leq env t' c1 evd, v') - with NotUnifiable _ -> raise NoCoercion + with Reduction.NotConvertible -> raise NoCoercion let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = try (the_conv_x_leq env t c1 evd, v) - with NotUnifiable (best_failed_evd,e) -> + with Reduction.NotConvertible -> try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match @@ -219,7 +218,7 @@ module Default = struct | Some v2 -> Retyping.get_type_of env1 evd' v2 in let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') - | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) + | _ -> raise NoCoercion (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) = @@ -228,12 +227,12 @@ module Default = struct let (evd', val') = try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercionNoUnifier (best_failed_evd,e) -> + with NoCoercion -> let evd = saturate_evd env evd in try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercionNoUnifier _ -> - error_actual_type_loc loc env best_failed_evd cj t e + with NoCoercion -> + error_actual_type_loc loc env evd cj t in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 183cb1c953..3906f87288 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -19,7 +19,6 @@ open Recordops open Evarutil open Libnames open Evd -open Pretype_errors type flex_kind_of_term = | Rigid of constr @@ -129,42 +128,39 @@ let rec ise_try evd = function [] -> assert false | [f] -> f evd | f1::l -> - match f1 evd with - | Success _ as x -> x - | UnifFailure _ -> ise_try evd l + let (evd',b) = f1 evd in + if b then (evd',b) else ise_try evd l let ise_and evd l = let rec ise_and i = function [] -> assert false | [f] -> f i | f1::l -> - match f1 i with - | Success i' -> ise_and i' l - | UnifFailure _ as x -> x in + let (i',b) = f1 i in + if b then ise_and i' l else (evd,false) in ise_and evd l let ise_list2 evd f l1 l2 = let rec ise_list2 i l1 l2 = match l1,l2 with - [], [] -> Success i + [], [] -> (i, true) | [x], [y] -> f i x y | x::l1, y::l2 -> - (match f i x y with - | Success i' -> ise_list2 i' l1 l2 - | UnifFailure _ as x -> x) - | _ -> UnifFailure (evd, NotSameArgSize) in + let (i',b) = f i x y in + if b then ise_list2 i' l1 l2 else (evd,false) + | _ -> (evd, false) in ise_list2 evd l1 l2 let ise_array2 evd f v1 v2 = let rec allrec i = function - | -1 -> Success i + | -1 -> (i,true) | n -> - match f i v1.(n) v2.(n) with - | Success i' -> allrec i' (n-1) - | UnifFailure _ as x -> x in + let (i',b) = f i v1.(n) v2.(n) in + if b then allrec i' (n-1) else (evd,false) + in let lv1 = Array.length v1 in if lv1 = Array.length v2 then allrec evd (pred lv1) - else UnifFailure (evd,NotSameArgSize) + else (evd,false) let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in @@ -180,8 +176,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = else None else None in match ground_test with - | Some true -> Success evd - | Some false -> UnifFailure (evd,ConversionFailed (env,term1,term2)) + Some b -> (evd,b) | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) @@ -222,12 +217,9 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = ise_and i [(fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2); - (fun i -> - Success (solve_refl - (fun env i pbty a1 a2 -> - is_success (evar_conv_x ts env i pbty a1 a2)) - env i sp1 al1 al2))] - else UnifFailure (i,NotSameHead) + (fun i -> solve_refl (evar_conv_x ts) env i sp1 al1 al2, + true)] + else (i,false) in ise_try evd [f1; f2] @@ -255,12 +247,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = [(fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 rest2); (fun i -> evar_conv_x ts env i pbty term1 (applist(term2,deb2)))] - else UnifFailure (i,NotSameArgSize) + else (i,false) and f2 i = match eval_flexible_term env flex2 with | Some v2 -> evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2) - | None -> UnifFailure (i,NotSameHead) + | None -> (i,false) in ise_try evd [f1; f2] @@ -287,12 +279,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = [(fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) rest1 l2); (fun i -> evar_conv_x ts env i pbty (applist(term1,deb1)) term2)] - else UnifFailure (i,NotSameArgSize) + else (i,false) and f2 i = match eval_flexible_term env flex1 with | Some v1 -> evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2 - | None -> UnifFailure (i,NotSameHead) + | None -> (i,false) in ise_try evd [f1; f2] @@ -319,12 +311,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = if flex1 = flex2 then ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2 else - UnifFailure (i,NotSameHead) + (i,false) and f2 i = (try conv_record ts env i (try check_conv_record appr1 appr2 with Not_found -> check_conv_record appr2 appr1) - with Not_found -> UnifFailure (i,NoCanonicalStructure)) + with Not_found -> (i,false)) and f3 i = (* heuristic: unfold second argument first, exception made if the first argument is a beta-redex (expand a constant @@ -339,7 +331,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = match eval_flexible_term env flex2 with | Some v2 -> evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2) - | None -> UnifFailure (i,NotSameHead) + | None -> (i,false) else match eval_flexible_term env flex2 with | Some v2 -> @@ -348,7 +340,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = match eval_flexible_term env flex1 with | Some v1 -> evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2 - | None -> UnifFailure (i,NotSameHead) + | None -> (i,false) in ise_try evd [f1; f2; f3] end @@ -395,7 +387,8 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (position_problem true pbty,ev1,t2) else (* Postpone the use of an heuristic *) - Success (add_conv_pb (pbty,env,applist appr1,applist appr2) evd) + add_conv_pb (pbty,env,applist appr1,applist appr2) evd, + true | (Rigid _ | PseudoRigid _), Flexible ev2 -> if @@ -410,29 +403,30 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (position_problem false pbty,ev2,t1) else (* Postpone the use of an heuristic *) - Success (add_conv_pb (pbty,env,applist appr1,applist appr2) evd) + add_conv_pb (pbty,env,applist appr1,applist appr2) evd, + true | MaybeFlexible flex1, (Rigid _ | PseudoRigid _) -> let f3 i = (try conv_record ts env i (check_conv_record appr1 appr2) - with Not_found -> UnifFailure (i,NoCanonicalStructure)) + with Not_found -> (i,false)) and f4 i = match eval_flexible_term env flex1 with | Some v1 -> evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2 - | None -> UnifFailure (i,NotSameHead) + | None -> (i,false) in ise_try evd [f3; f4] | (Rigid _ | PseudoRigid _), MaybeFlexible flex2 -> let f3 i = (try conv_record ts env i (check_conv_record appr2 appr1) - with Not_found -> UnifFailure (i,NoCanonicalStructure)) + with Not_found -> (i,false)) and f4 i = match eval_flexible_term env flex2 with | Some v2 -> evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2) - | None -> UnifFailure (i,NotSameHead) + | None -> (i,false) in ise_try evd [f3; f4] @@ -440,8 +434,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = match kind_of_term c1, kind_of_term c2 with | Sort s1, Sort s2 when l1=[] & l2=[] -> - if base_sort_cmp pbty s1 s2 then Success evd - else UnifFailure (evd,NotSameHead) + (evd, base_sort_cmp pbty s1 s2) | Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] -> ise_and evd @@ -453,12 +446,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Ind sp1, Ind sp2 -> if eq_ind sp1 sp2 then ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2 - else UnifFailure (evd,NotSameHead) + else (evd, false) | Construct sp1, Construct sp2 -> if eq_constructor sp1 sp2 then ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2 - else UnifFailure (evd,NotSameHead) + else (evd, false) | CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) -> if i1=i2 then @@ -470,12 +463,10 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = bds1 bds2); (fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2)] - else UnifFailure (evd,NotSameHead) + else (evd,false) - | (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _), _ -> - UnifFailure (evd,NotSameHead) - | _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _) -> - UnifFailure (evd,NotSameHead) + | (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _), _ -> (evd,false) + | _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _) -> (evd,false) | (App _ | Meta _ | Cast _ | Case _ | Fix _), _ -> assert false | (LetIn _ | Rel _ | Var _ | Const _ | Evar _), _ -> assert false @@ -504,10 +495,10 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = bds1 bds2); (fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2)] - else UnifFailure (evd,NotSameHead) + else (evd,false) | (Meta _ | Case _ | Fix _ | CoFix _), - (Meta _ | Case _ | Fix _ | CoFix _) -> UnifFailure (evd,NotSameHead) + (Meta _ | Case _ | Fix _ | CoFix _) -> (evd,false) | (App _ | Ind _ | Construct _ | Sort _ | Prod _), _ -> assert false | _, (App _ | Ind _ | Construct _ | Sort _ | Prod _) -> assert false @@ -520,9 +511,9 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = end - | PseudoRigid _, Rigid _ -> UnifFailure (evd,NotSameHead) + | PseudoRigid _, Rigid _ -> (evd,false) - | Rigid _, PseudoRigid _ -> UnifFailure (evd,NotSameHead) + | Rigid _, PseudoRigid _ -> (evd,false) and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = let (evd',ks,_) = @@ -578,12 +569,12 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = & array_for_all (fun a -> a = term2 or isEvar a) args1 -> (* The typical kind of constraint coming from pattern-matching return type inference *) - Success (choose_less_dependent_instance evk1 evd term2 args1) + choose_less_dependent_instance evk1 evd term2 args1, true | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] & array_for_all (fun a -> a = term1 or isEvar a) args2 -> (* The typical kind of constraint coming from pattern-matching return type inference *) - Success (choose_less_dependent_instance evk2 evd term1 args2) + choose_less_dependent_instance evk2 evd term1 args2, true | Evar ev1,_ when List.length l1 <= List.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) first_order_unification ts env evd (ev1,l1) appr2 @@ -598,10 +589,8 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd = let (evd,pbs) = extract_all_conv_pbs evd in let heuristic_solved_evd = List.fold_left (fun evd (pbty,env,t1,t2) -> - match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with - | Success evd' -> evd' - | UnifFailure (evd,reason) -> - Pretype_errors.error_cannot_unify env evd ~reason (t1, t2)) + let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in + if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2)) evd pbs in Evd.fold_undefined (fun ev ev_info evd' -> match ev_info.evar_source with |_,ImpossibleCase -> @@ -610,24 +599,22 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd = (* Main entry points *) -exception NotUnifiable of evar_map * unification_error - let the_conv_x ?(ts=full_transparent_state) env t1 t2 evd = match evar_conv_x ts env evd CONV t1 t2 with - | Success evd' -> evd' - | UnifFailure (evd',e) -> raise (NotUnifiable (evd',e)) + (evd',true) -> evd' + | _ -> raise Reduction.NotConvertible let the_conv_x_leq ?(ts=full_transparent_state) env t1 t2 evd = match evar_conv_x ts env evd CUMUL t1 t2 with - | Success evd' -> evd' - | UnifFailure (evd',e) -> raise (NotUnifiable (evd',e)) + (evd', true) -> evd' + | _ -> raise Reduction.NotConvertible let e_conv ?(ts=full_transparent_state) env evd t1 t2 = match evar_conv_x ts env !evd CONV t1 t2 with - | Success evd' -> evd := evd'; true - | _ -> false + (evd',true) -> evd := evd'; true + | _ -> false let e_cumul ?(ts=full_transparent_state) env evd t1 t2 = match evar_conv_x ts env !evd CUMUL t1 t2 with - | Success evd' -> evd := evd'; true - | _ -> false + (evd',true) -> evd := evd'; true + | _ -> false diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index d2d74ff962..e1f507b0ac 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -13,9 +13,7 @@ open Environ open Reductionops open Evd -exception NotUnifiable of evar_map * Pretype_errors.unification_error - -(** returns exception NotUnifiable with best known evar_map if not unifiable *) +(** returns exception Reduction.NotConvertible if not unifiable *) val the_conv_x : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map val the_conv_x_leq : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map @@ -27,11 +25,11 @@ val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr - (**/**) (* For debugging *) val evar_conv_x : transparent_state -> - env -> evar_map -> conv_pb -> constr -> constr -> Evarutil.unification_result + env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool val evar_eqappr_x : transparent_state -> env -> evar_map -> conv_pb -> constr * constr list -> constr * constr list -> - Evarutil.unification_result + evar_map * bool (**/**) val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 13d193658f..774180c67b 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -584,9 +584,6 @@ let clear_hyps_in_evi evdref hyps concl ids = in (nhyps,nconcl) -(***************) -(* Unification *) - (* Inverting constructors in instances (common when inferring type of match) *) let find_projectable_constructor env evd cstr k args cstr_subst = @@ -948,7 +945,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 = (* Filter and restrict if needed *) let evd,evk,args = restrict_upon_filter evd evi evk - (fun (a1,a2) -> conv_algo env evd Reduction.CONV a1 a2) + (fun (a1,a2) -> snd (conv_algo env evd Reduction.CONV a1 a2)) (List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in (* Leave a unification problem *) let args1,args2 = List.split args in @@ -979,17 +976,9 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 = * Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn) *) -type unification_result = - | Success of evar_map - | UnifFailure of evar_map * unification_error - -let is_success = function Success _ -> true | UnifFailure _ -> false - exception NotInvertibleUsingOurAlgorithm of constr exception NotEnoughInformationToProgress exception OccurCheckIn of evar_map * constr -exception MetaOccurInBodyInternal -exception InstanceNotSameTypeInternal let rec invert_definition choose env evd (evk,argsv as ev) rhs = let aliases = make_alias_map env in @@ -1104,7 +1093,7 @@ and occur_existential evm c = and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd = try let (evd',body) = invert_definition choose env evd ev rhs in - if occur_meta body then raise MetaOccurInBodyInternal; + if occur_meta body then error "Meta cannot occur in evar body."; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) if occur_evar evk body then raise (OccurCheckIn (evd',body)); @@ -1130,17 +1119,18 @@ and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd = with | NotEnoughInformationToProgress -> postpone_evar_term env evd ev rhs - | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e -> - raise e + | NotInvertibleUsingOurAlgorithm t -> + error_not_clean env evd evk t (evar_source evk evd) | OccurCheckIn (evd,rhs) -> (* last chance: rhs actually reduces to ev *) let c = whd_betadeltaiota env evd rhs in match kind_of_term c with | Evar (evk',argsv2) when evk = evk' -> - solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c') + solve_refl + (fun env sigma pb c c' -> (evd,is_fconv pb env sigma c c')) env evd evk argsv argsv2 | _ -> - raise (OccurCheckIn (evd,rhs)) + error_occur_check env evd evk rhs (*-------------------*) (* Auxiliary functions for the conversion algorithms modulo evars @@ -1317,10 +1307,10 @@ let check_instance_type conv_algo env evd ev1 t2 = if isEvar typ2 then (* Don't want to commit too early too *) evd else let typ1 = existential_type evd ev1 in - match conv_algo env evd Reduction.CUMUL typ2 typ1 with - | Success evd -> evd - | UnifFailure _ -> - raise InstanceNotSameTypeInternal + let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in + if b then evd else + user_err_loc (fst (evar_source (fst ev1) evd),"", + str "Unable to find a well-typed instantiation") (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar @@ -1334,9 +1324,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) let evd = match kind_of_term t2 with | Evar (evk2,args2 as ev2) -> if evk1 = evk2 then - solve_refl - (fun env evd pbty a b -> is_success (conv_algo env evd pbty a b)) - env evd evk1 args1 args2 + solve_refl conv_algo env evd evk1 args1 args2 else if pbty = None then solve_evar_evar evar_define env evd ev1 ev2 @@ -1365,20 +1353,11 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) in let (evd,pbs) = extract_changed_conv_pbs evd status_changed in List.fold_left - (fun p (pbty,env,t1,t2) -> - match p with - | Success evd -> conv_algo env evd pbty t1 t2 - | UnifFailure _ as x -> x) (Success evd) + (fun (evd,b as p) (pbty,env,t1,t2) -> + if b then conv_algo env evd pbty t1 t2 else p) (evd,true) pbs - with - | NotInvertibleUsingOurAlgorithm t -> - UnifFailure (evd,NotClean (evk1,t)) - | OccurCheckIn (evd,rhs) -> - UnifFailure (evd,OccurCheck (evk1,rhs)) - | MetaOccurInBodyInternal -> - UnifFailure (evd,MetaOccurInBody evk1) - | InstanceNotSameTypeInternal -> - UnifFailure (evd,InstanceNotSameType evk1) + with e when precatchable_exception e -> + (evd,false) (** The following functions return the set of evars immediately contained in the object, including defined evars *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 705ab356fb..a4c07a0196 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -74,20 +74,13 @@ val whd_head_evar : evar_map -> constr -> constr val is_ground_term : evar_map -> constr -> bool val is_ground_env : evar_map -> env -> bool val solve_refl : - (env -> evar_map -> conv_pb -> constr -> constr -> bool) + (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) -> env -> evar_map -> existential_key -> constr array -> constr array -> evar_map - -type unification_result = - | Success of evar_map - | UnifFailure of evar_map * Pretype_errors.unification_error - -val is_success : unification_result -> bool - val solve_simple_eqn : - (env -> evar_map -> conv_pb -> constr -> constr -> unification_result) + (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> - unification_result + evar_map * bool (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index f663496dfb..6d1c54e63d 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -18,26 +18,15 @@ open Type_errors open Glob_term open Inductiveops -type unification_error = - | OccurCheck of existential_key * constr - | NotClean of existential_key * constr - | NotSameArgSize - | NotSameHead - | NoCanonicalStructure - | ConversionFailed of env * constr * constr - | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key - type pretype_error = (* Old Case *) | CantFindCaseType of constr - (* Type inference unification *) - | ActualTypeNotCoercible of unsafe_judgment * types * unification_error - (* Tactic unification *) - | UnifOccurCheck of existential_key * constr + (* Unification *) + | OccurCheck of existential_key * constr + | NotClean of existential_key * constr * Evd.hole_kind | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind * Evd.unsolvability_explanation option - | CannotUnify of constr * constr * unification_error option + | CannotUnify of constr * constr | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr @@ -106,15 +95,6 @@ let contract2 env a b = match contract env [a;b] with let contract3 env a b c = match contract env [a;b;c] with | env, [a;b;c] -> env,a,b,c | _ -> assert false -let contract4 env a b c d = match contract env [a;b;c;d] with - | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false - -let contract3' env a b c = function - | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d) - | NotClean (evk,d) -> let x,d = contract4 env a b c d in x,NotClean(evk,d) - | NotSameArgSize | NotSameHead | NoCanonicalStructure | ConversionFailed _ - | MetaOccurInBody _ | InstanceNotSameType _ as x -> contract3 env a b c, x - let raise_pretype_error (loc,env,sigma,te) = Loc.raise loc (PretypeError(env,sigma,te)) @@ -122,11 +102,10 @@ let raise_located_type_error (loc,env,sigma,te) = Loc.raise loc (PretypeError(env,sigma,TypingError te)) -let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty reason = - let (env, c, actty, expty), reason = contract3' env c actty expty reason in +let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty = + let env, c, actty, expty = contract3 env c actty expty in let j = {uj_val=c;uj_type=actty} in - raise_pretype_error - (loc, env, sigma, ActualTypeNotCoercible (j, expty, reason)) + raise_located_type_error (loc, env, sigma, ActualType (j, expty)) let error_cant_apply_not_functional_loc loc env sigma rator randl = raise_located_type_error @@ -158,20 +137,23 @@ let error_not_a_type_loc loc env sigma j = a precise location. *) let error_occur_check env sigma ev c = - raise (PretypeError (env, sigma, UnifOccurCheck (ev,c))) + raise (PretypeError (env, sigma, OccurCheck (ev,c))) + +let error_not_clean env sigma ev c (loc,k) = + Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k))) let error_unsolvable_implicit loc env sigma evi e explain = Loc.raise loc (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain))) -let error_cannot_unify env sigma ?reason (m,n) = - raise (PretypeError (env, sigma,CannotUnify (m,n,reason))) +let error_cannot_unify env sigma (m,n) = + raise (PretypeError (env, sigma,CannotUnify (m,n))) let error_cannot_unify_local env sigma (m,n,sn) = raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn))) let error_cannot_coerce env sigma (m,n) = - raise (PretypeError (env, sigma,CannotUnify (m,n,None))) + raise (PretypeError (env, sigma,CannotUnify (m,n))) let error_cannot_find_well_typed_abstraction env sigma p l = raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l))) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index f95514ade4..30ee6aaf67 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -17,26 +17,15 @@ open Inductiveops (** {6 The type of errors raised by the pretyper } *) -type unification_error = - | OccurCheck of existential_key * constr - | NotClean of existential_key * constr - | NotSameArgSize - | NotSameHead - | NoCanonicalStructure - | ConversionFailed of env * constr * constr - | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key - type pretype_error = (** Old Case *) | CantFindCaseType of constr - (** Type inference unification *) - | ActualTypeNotCoercible of unsafe_judgment * types * unification_error - (** Tactic Unification *) - | UnifOccurCheck of existential_key * constr + (** Unification *) + | OccurCheck of existential_key * constr + | NotClean of existential_key * constr * Evd.hole_kind | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind * Evd.unsolvability_explanation option - | CannotUnify of constr * constr * unification_error option + | CannotUnify of constr * constr | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr @@ -70,8 +59,7 @@ val jv_nf_betaiotaevar : (** Raising errors *) val error_actual_type_loc : - loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> - unification_error -> 'b + loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b val error_cant_apply_not_functional_loc : loc -> env -> Evd.evar_map -> @@ -105,12 +93,14 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b +val error_not_clean : + env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b + val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> Evd.evar_info -> Evd.hole_kind -> Evd.unsolvability_explanation option -> 'b -val error_cannot_unify : env -> Evd.evar_map -> ?reason:unification_error -> - constr * constr -> 'b +val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 003f507dcf..1ea2dbd002 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -640,8 +640,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj with Reduction.NotConvertible -> - error_actual_type_loc loc env !evdref cj tval - (ConversionFailed (env,cty,tval)) + error_actual_type_loc loc env !evdref cj tval end | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval) in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6e39d9831c..6121ba7d87 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -638,11 +638,9 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) let solve_simple_evar_eqn ts env evd ev rhs = - match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with - | UnifFailure (evd,reason) -> - error_cannot_unify env evd ~reason (mkEvar ev,rhs); - | Success evd -> - Evarconv.consider_remaining_unif_problems env evd + let evd,b = solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) in + if not b then error_cannot_unify env evd (mkEvar ev,rhs); + Evarconv.consider_remaining_unif_problems env evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] diff --git a/proofs/clenv.ml b/proofs/clenv.ml index b5770c8a78..8c4faa11cf 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -431,8 +431,7 @@ let clenv_unify_binding_type clenv c t u = let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with - | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e -> - raise e + | PretypeError (_,_,NotClean _) as e -> raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 3d37074428..36268de1ee 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -25,17 +25,15 @@ let depends_on_evar evk _ (pbty,_,t1,t2) = with NoHeadEvar -> false let define_and_solve_constraints evk c evd = - let evd = define evk c evd in - let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in - match - List.fold_left - (fun p (pbty,env,t1,t2) -> match p with - | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 - | UnifFailure _ as x -> x) (Success evd) - pbs - with - | Success evd -> evd - | UnifFailure _ -> error "Instance does not satisfy the constraints." + try + let evd = define evk c evd in + let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in + fst (List.fold_left + (fun (evd,b as p) (pbty,env,t1,t2) -> + if b then Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 else p) (evd,true) + pbs) + with e when Pretype_errors.precatchable_exception e -> + error "Instance does not satisfy constraints." let w_refine (evk,evi) (ltac_var,rawc) sigma = if Evd.is_defined sigma evk then diff --git a/proofs/logic.ml b/proofs/logic.ml index 7472918690..2835eb5429 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -55,9 +55,8 @@ let rec catchable_exception = function | Tacred.ReductionTacticError _ (* unification errors *) | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ - |NoOccurrenceFound _|CannotUnifyBindingType _ - |ActualTypeNotCoercible _|UnifOccurCheck _ - |CannotFindWellTypedAbstraction _ + |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ + |CannotFindWellTypedAbstraction _|OccurCheck _ |UnsolvableImplicit _)) -> true | Typeclasses_errors.TypeClassError (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 87a1e02a86..2802acfc1a 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -401,8 +401,7 @@ let rec catchable_exception = function | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _) (* unification errors *) | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ - |NoOccurrenceFound _|CannotUnifyBindingType _ - |ActualTypeNotCoercible _ + |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ |CannotFindWellTypedAbstraction _ |UnsolvableImplicit _)) -> true | Typeclasses_errors.TypeClassError diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index f86d6d271d..6af1f9d56c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -153,46 +153,16 @@ let explain_generalization env (name,var) j = str "it has type" ++ spc () ++ pt ++ spc () ++ str "which should be Set, Prop or Type." -let explain_unification_error env p1 p2 = function - | None -> mt() - | Some e -> - match e with - | OccurCheck (evk,rhs) -> - spc () ++ str "(cannot define " ++ quote (pr_existential_key evk) ++ - strbrk " with term " ++ pr_lconstr_env env rhs ++ - strbrk "that would depend on itself)" - | NotClean (evk,c) -> - spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key evk) - ++ strbrk " because " ++ pr_lconstr_env env c ++ - strbrk " is out of scope)" - | NotSameArgSize | NotSameHead | NoCanonicalStructure -> - (* Error speaks from itself *) mt () - | ConversionFailed (env,t1,t2) -> - if t1 <> p1 || t2 <> p2 then - spc () ++ str "(cannot unify " ++ pr_lconstr_env env t1 ++ - strbrk " and " ++ pr_lconstr_env env t2 ++ str ")" - else mt () - | MetaOccurInBody evk -> - spc () ++ str "(instance for " ++ quote (pr_existential_key evk) ++ - strbrk " refers to a metavariable - please report your example)" - | InstanceNotSameType evk -> - spc () ++ str "(unable to find a well-typed instantiation for " ++ - quote (pr_existential_key evk) ++ str ")" - - -let explain_actual_type env sigma j t reason = +let explain_actual_type env sigma j pt = let j = j_nf_betaiotaevar sigma j in - let t = Reductionops.nf_betaiota sigma t in + let pt = Reductionops.nf_betaiota sigma pt in let pe = pr_ne_context_of (str "In environment") env in let (pc,pct) = pr_ljudge_env env j in - let pt = pr_lconstr_env env t in - let ppreason = explain_unification_error env j.uj_type t reason in + let pt = pr_lconstr_env env pt in pe ++ - hov 0 ( str "The term" ++ brk(1,1) ++ pc ++ spc () ++ - str "has type" ++ brk(1,1) ++ pct ++ spc () ++ - str "while it is expected to have type" ++ brk(1,1) ++ pt ++ - ppreason ++ str ".") + str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ + str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "." let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = let randl = jv_nf_betaiotaevar sigma randl in @@ -450,14 +420,13 @@ let explain_wrong_case_info env ind ci = str "was given to a pattern-matching expression on the inductive type" ++ spc () ++ pc ++ str "." -let explain_cannot_unify env sigma m n e = +let explain_cannot_unify env sigma m n = let m = nf_evar sigma m in let n = nf_evar sigma n in let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in - let ppreason = explain_unification_error env m n e in str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ - str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "." + str "with" ++ brk(1,1) ++ pn ++ str "." let explain_cannot_unify_local env sigma m n subn = let pm = pr_lconstr_env env m in @@ -525,7 +494,7 @@ let explain_type_error env sigma err = | Generalization (nvar, c) -> explain_generalization env nvar c | ActualType (j, pt) -> - explain_actual_type env sigma j pt None + explain_actual_type env sigma j pt | CantApplyBadType (t, rator, randl) -> explain_cant_apply_bad_type env sigma t rator randl | CantApplyNonFunctional (rator, randl) -> @@ -542,13 +511,13 @@ let explain_pretype_error env sigma err = let env = make_all_name_different env in match err with | CantFindCaseType c -> explain_cant_find_case_type env sigma c - | ActualTypeNotCoercible (j,t,e) -> explain_actual_type env sigma j t (Some e) - | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs + | OccurCheck (n,c) -> explain_occur_check env sigma n c + | NotClean (n,c,k) -> explain_not_clean env sigma n c k | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp | VarNotFound id -> explain_var_not_found env id | UnexpectedType (actual,expect) -> explain_unexpected_type env sigma actual expect | NotProduct c -> explain_not_product env sigma c - | CannotUnify (m,n,e) -> explain_cannot_unify env sigma m n e + | CannotUnify (m,n) -> explain_cannot_unify env sigma m n | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id |