aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercion.ml13
-rw-r--r--pretyping/evarconv.ml123
-rw-r--r--pretyping/evarconv.mli8
-rw-r--r--pretyping/evarutil.ml53
-rw-r--r--pretyping/evarutil.mli13
-rw-r--r--pretyping/pretype_errors.ml46
-rw-r--r--pretyping/pretype_errors.mli28
-rw-r--r--pretyping/pretyping.ml3
-rw-r--r--pretyping/unification.ml8
9 files changed, 110 insertions, 185 deletions
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]
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-07 21:15:34 +0000