summaryrefslogtreecommitdiff
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r--pretyping/evarconv.ml461
1 files changed, 290 insertions, 171 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9fd55a48..d37090a6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1,37 +1,41 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open CErrors
open Util
open Names
-open Term
+open Constr
+open Termops
+open Environ
+open EConstr
open Vars
open CClosure
open Reduction
open Reductionops
-open Termops
-open Environ
open Recordops
open Evarutil
open Evardefine
open Evarsolve
-open Globnames
open Evd
open Pretype_errors
-open Sigma.Notations
-open Context.Rel.Declaration
+open Context.Named.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
type unify_fun = transparent_state ->
- env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
+ env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
let debug_unification = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname =
"Print states sent to Evarconv unification";
Goptions.optkey = ["Debug";"Unification"];
@@ -39,6 +43,31 @@ let _ = Goptions.declare_bool_option {
Goptions.optwrite = (fun a -> debug_unification:=a);
}
+(*******************************************)
+(* Functions to deal with impossible cases *)
+(*******************************************)
+(* XXX: we would like to search for this with late binding
+ "data.id.type" etc... *)
+let impossible_default_case () =
+ let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
+ let (_, u) = Constr.destConst c in
+ Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx)
+
+let coq_unit_judge =
+ let open Environ in
+ let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
+ let na1 = Name (Id.of_string "A") in
+ let na2 = Name (Id.of_string "H") in
+ fun () ->
+ match impossible_default_case () with
+ | Some (id, type_of_id, ctx) ->
+ make_judge id type_of_id, ctx
+ | None ->
+ (* In case the constants id/ID are not defined *)
+ Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
+ (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))),
+ Univ.ContextSet.empty
+
let unfold_projection env evd ts p c =
let cst = Projection.constant p in
if is_transparent_constant ts cst then
@@ -46,21 +75,20 @@ let unfold_projection env evd ts p c =
else None
let eval_flexible_term ts env evd c =
- match kind_of_term c with
- | Const (c,u as cu) ->
+ match EConstr.kind evd c with
+ | Const (c, u) ->
if is_transparent_constant ts c
- then constant_opt_value_in env cu
+ then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u))
else None
| Rel n ->
(try match lookup_rel n env with
- | LocalAssum _ -> None
- | LocalDef (_,v,_) -> Some (lift n v)
+ | RelDecl.LocalAssum _ -> None
+ | RelDecl.LocalDef (_,v,_) -> Some (lift n v)
with Not_found -> None)
| Var id ->
(try
if is_transparent_variable ts id then
- let open Context.Named.Declaration in
- lookup_named id env |> get_value
+ env |> lookup_named id |> NamedDecl.get_value
else None
with Not_found -> None)
| LetIn (_,b,_,c) -> Some (subst1 b c)
@@ -72,11 +100,11 @@ let eval_flexible_term ts env evd c =
type flex_kind_of_term =
| Rigid
- | MaybeFlexible of Constr.t (* reducible but not necessarily reduced *)
- | Flexible of existential
+ | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *)
+ | Flexible of EConstr.existential
let flex_kind_of_term ts env evd c sk =
- match kind_of_term c with
+ match EConstr.kind evd c with
| LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c)
| Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c
@@ -86,10 +114,13 @@ let flex_kind_of_term ts env evd c sk =
| Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
| Cast _ | App _ | Case _ -> assert false
+let add_conv_pb (pb, env, x, y) sigma =
+ Evd.add_conv_pb (pb, env, EConstr.Unsafe.to_constr x, EConstr.Unsafe.to_constr y) sigma
+
let apprec_nohdbeta ts env evd c =
let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
if Stack.not_purely_applicative sk
- then Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state
+ then Stack.zip evd (fst (whd_betaiota_deltazeta_for_iota_state
ts env evd Cst_stack.empty appr))
else c
@@ -99,7 +130,7 @@ let position_problem l2r = function
let occur_rigidly (evk,_ as ev) evd t =
let rec aux t =
- match kind_of_term (whd_evar evd t) with
+ match EConstr.kind evd t with
| App (f, c) -> if aux f then Array.exists aux c else false
| Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true
| Proj (p, c) -> not (aux c)
@@ -109,7 +140,7 @@ let occur_rigidly (evk,_ as ev) evd t =
| Const _ -> false
| Prod (_, b, t) -> ignore(aux b || aux t); true
| Rel _ | Var _ -> false
- | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false
+ | Case (_,_,c,_) -> if eq_constr evd (mkEvar ev) c then raise Occur else false
in try ignore(aux t); false with Occur -> true
(* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose
@@ -133,20 +164,28 @@ let occur_rigidly (evk,_ as ev) evd t =
projection would have been reduced) *)
let check_conv_record env sigma (t1,sk1) (t2,sk2) =
- let (proji, u), arg = Universes.global_app_of_constr t1 in
+ let (proji, u), arg = Termops.global_app_of_constr sigma t1 in
let canon_s,sk2_effective =
try
- match kind_of_term t2 with
+ match EConstr.kind sigma t2 with
Prod (_,a,b) -> (* assert (l2=[]); *)
- let _, a, b = destProd (Evarutil.nf_evar sigma t2) in
- if dependent (mkRel 1) b then raise Not_found
- else lookup_canonical_conversion (proji, Prod_cs),
+ let _, a, b = destProd sigma t2 in
+ if noccurn sigma 1 b then
+ lookup_canonical_conversion (proji, Prod_cs),
(Stack.append_app [|a;pop b|] Stack.empty)
+ else raise Not_found
| Sort s ->
+ let s = ESorts.kind sigma s in
lookup_canonical_conversion
- (proji, Sort_cs (family_of_sort s)),[]
+ (proji, Sort_cs (Sorts.family s)),[]
+ | Proj (p, c) ->
+ let c2 = Globnames.ConstRef (Projection.constant p) in
+ let c = Retyping.expand_projection env sigma p c [] in
+ let _, args = destApp sigma c in
+ let sk2 = Stack.append_app args sk2 in
+ lookup_canonical_conversion (proji, Const_cs c2), sk2
| _ ->
- let c2 = global_of_constr t2 in
+ let (c2, _) = Termops.global_of_constr sigma t2 in
lookup_canonical_conversion (proji, Const_cs c2),sk2
with Not_found ->
let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in
@@ -154,12 +193,14 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
in
let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
+ let us = List.map EConstr.of_constr us in
+ let params = List.map EConstr.of_constr params in
let params1, c1, extra_args1 =
match arg with
| Some c -> (* A primitive projection applied to c *)
let ty = Retyping.get_type_of ~lax:true env sigma c in
let (i,u), ind_args =
- try Inductiveops.find_mrectype env sigma ty
+ try Inductiveops.find_mrectype env sigma ty
with _ -> raise Not_found
in Stack.append_app_list ind_args Stack.empty, c, sk1
| None ->
@@ -172,14 +213,19 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
else match (Stack.strip_n_app (l_us-1) sk2_effective) with
| None -> raise Not_found
| Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
- let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+ let u, ctx' = Universes.fresh_instance_from ctx None in
+ let subst = Univ.make_inverse_instance_subst u in
+ let c = EConstr.of_constr c in
let c' = subst_univs_level_constr subst c in
+ let t' = EConstr.of_constr t' in
let t' = subst_univs_level_constr subst t' in
- let bs' = List.map (subst_univs_level_constr subst) bs in
- let h, _ = decompose_app_vect t' in
+ let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in
+ let params = List.map (fun c -> subst_univs_level_constr subst c) params in
+ let us = List.map (fun c -> subst_univs_level_constr subst c) us in
+ let h, _ = decompose_app_vect sigma t' in
ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
(Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
- (n,Stack.zip(t2,sk2))
+ (n, Stack.zip sigma (t2,sk2))
(* Precondition: one of the terms of the pb is an uninstantiated evar,
* possibly applied to arguments. *)
@@ -250,7 +296,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
| UnifFailure _ as x -> fail x)
| UnifFailure _ as x -> fail x)
| Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
- if eq_constant (Projection.constant p1) (Projection.constant p2)
+ if Constant.equal (Projection.constant p1) (Projection.constant p2)
then ise_stack2 true i q1 q2
else fail (UnifFailure (i, NotSameHead))
| Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
@@ -263,8 +309,6 @@ let ise_stack2 no_app env evd f sk1 sk2 =
| Success i' -> ise_stack2 true i' q1 q2
| UnifFailure _ as x -> fail x
else fail (UnifFailure (i,NotSameHead))
- | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
- | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false
| Stack.App _ :: _, Stack.App _ :: _ ->
if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else
begin match ise_app_stack2 env f i sk1 sk2 with
@@ -294,11 +338,9 @@ let exact_ise_stack2 env evd f sk1 sk2 =
(fun i -> ise_stack2 i a1 a2)]
else UnifFailure (i,NotSameHead)
| Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
- if eq_constant (Projection.constant p1) (Projection.constant p2)
+ if Constant.equal (Projection.constant p1) (Projection.constant p2)
then ise_stack2 i q1 q2
else (UnifFailure (i, NotSameHead))
- | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
- | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false
| Stack.App _ :: _, Stack.App _ :: _ ->
begin match ise_app_stack2 env f i sk1 sk2 with
|_,(UnifFailure _ as x) -> x
@@ -310,6 +352,14 @@ let exact_ise_stack2 env evd f sk1 sk2 =
ise_stack2 evd (List.rev sk1) (List.rev sk2)
else UnifFailure (evd, (* Dummy *) NotSameHead)
+(* Add equality constraints for covariant/invariant positions. For
+ irrelevant positions, unify universes when flexible. *)
+let compare_cumulative_instances evd variances u u' =
+ match Evarutil.compare_cumulative_instances CONV variances u u' evd with
+ | Inl evd ->
+ Success evd
+ | Inr p -> UnifFailure (evd, UnifUnivInconsistency p)
+
let rec evar_conv_x ts env evd pbty term1 term2 =
let term1 = whd_head_evar evd term1 in
let term2 = whd_head_evar evd term2 in
@@ -321,7 +371,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
let e =
try
let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
- env evd term1 term2
+ env evd term1 term2
in
if b then Success evd
else UnifFailure (evd, ConversionFailed (env,term1,term2))
@@ -335,7 +385,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
match ground_test with
| Some result -> result
| None ->
- (* Until pattern-unification is used consistently, use nohdbeta to not
+ (* Until pattern-unification is used consistently, use nohdbeta to not
destroy beta-redexes that can be used for 1st-order unification *)
let term1 = apprec_nohdbeta (fst ts) env evd term1 in
let term2 = apprec_nohdbeta (fst ts) env evd term2 in
@@ -344,16 +394,16 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
(whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
(whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
in
- begin match kind_of_term term1, kind_of_term term2 with
+ begin match EConstr.kind evd term1, EConstr.kind evd term2 with
| Evar ev, _ when Evd.is_undefined evd (fst ev) ->
(match solve_simple_eqn (evar_conv_x ts) env evd
- (position_problem true pbty,ev,term2) with
+ (position_problem true pbty,ev, term2) with
| UnifFailure (_,OccurCheck _) ->
(* Eta-expansion might apply *) default ()
| x -> x)
| _, Evar ev when Evd.is_undefined evd (fst ev) ->
(match solve_simple_eqn (evar_conv_x ts) env evd
- (position_problem false pbty,ev,term1) with
+ (position_problem false pbty,ev, term1) with
| UnifFailure (_, OccurCheck _) ->
(* Eta-expansion might apply *) default ()
| x -> x)
@@ -369,8 +419,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
match is_unification_pattern_evar env evd ev lF tM with
| None -> fallback ()
| Some l1' -> (* Miller-Pfenning's patterns unification *)
- let t2 = nf_evar evd tM in
- let t2 = solve_pattern_eqn env l1' t2 in
+ let t2 = tM in
+ let t2 = solve_pattern_eqn env evd l1' t2 in
solve_simple_eqn (evar_conv_x ts) env evd
(position_problem on_left pbty,ev,t2)
in
@@ -379,34 +429,82 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let not_only_app = Stack.not_purely_applicative skO in
match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with
|Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
- switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
+ switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
|Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
- switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
+ switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
|None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO
|_, (UnifFailure _ as x) -> x
|Some _, _ -> UnifFailure (evd,NotSameArgSize) in
let eta env evd onleft sk term sk' term' =
assert (match sk with [] -> true | _ -> false);
- let (na,c1,c'1) = destLambda term in
+ let (na,c1,c'1) = destLambda evd term in
let c = nf_evar evd c1 in
- let env' = push_rel (LocalAssum (na,c)) env in
+ let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
let out1 = whd_betaiota_deltazeta_for_iota_state
(fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
let out2 = whd_nored_state evd
- (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty),
+ (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty),
Cst_stack.empty in
if onleft then evar_eqappr_x ts env' evd CONV out1 out2
else evar_eqappr_x ts env' evd CONV out2 out1
in
let rigids env evd sk term sk' term' =
- let b,univs = Universes.eq_constr_universes term term' in
- if b then
- ise_and evd [(fun i ->
- let cstrs = Universes.to_constraints (Evd.universes i) univs in
- try Success (Evd.add_constraints i cstrs)
- with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
- (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
- else UnifFailure (evd,NotSameHead)
+ let check_strict evd u u' =
+ let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in
+ try Success (Evd.add_constraints evd cstrs)
+ with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
+ in
+ let compare_heads evd =
+ match EConstr.kind evd term, EConstr.kind evd term' with
+ | Const (c, u), Const (c', u') when Constant.equal c c' ->
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ check_strict evd u u'
+ | Const _, Const _ -> UnifFailure (evd, NotSameHead)
+ | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.eq_ind ind ind' ->
+ if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+ else
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ let mind = Environ.lookup_mind mi env in
+ let open Declarations in
+ begin match mind.mind_universes with
+ | Monomorphic_ind _ -> assert false
+ | Polymorphic_ind _ -> check_strict evd u u'
+ | Cumulative_ind cumi ->
+ let nparamsaplied = Stack.args_size sk in
+ let nparamsaplied' = Stack.args_size sk' in
+ let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
+ if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
+ then check_strict evd u u'
+ else
+ compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u'
+ end
+ | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
+ | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
+ when Names.eq_constructor cons cons' ->
+ if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+ else
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ let mind = Environ.lookup_mind mi env in
+ let open Declarations in
+ begin match mind.mind_universes with
+ | Monomorphic_ind _ -> assert false
+ | Polymorphic_ind _ -> check_strict evd u u'
+ | Cumulative_ind cumi ->
+ let nparamsaplied = Stack.args_size sk in
+ let nparamsaplied' = Stack.args_size sk' in
+ let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
+ if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
+ then check_strict evd u u'
+ else
+ Success (compare_constructor_instances evd u u')
+ end
+ | Construct _, Construct _ -> UnifFailure (evd, NotSameHead)
+ | _, _ -> anomaly (Pp.str "")
+ in
+ ise_and evd [(fun i ->
+ try compare_heads i
+ with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
in
let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
let switch f a b = if on_left then f a b else f b a in
@@ -415,10 +513,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
match Stack.list_of_app_stack skF with
| None -> quick_fail evd
| Some lF ->
- let tM = Stack.zip apprM in
+ let tM = Stack.zip evd apprM in
miller_pfenning on_left
(fun () -> if not_only_app then (* Postpone the use of an heuristic *)
- switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM
+ switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
else quick_fail i)
ev lF tM i
and consume (termF,skF as apprF) (termM,skM as apprM) i =
@@ -432,7 +530,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in
let default i = ise_try i [f1; consume apprF apprM; delta]
in
- match kind_of_term termM with
+ match EConstr.kind evd termM with
| Proj (p, c) when not (Stack.is_empty skF) ->
(* Might be ?X args = p.c args', and we have to eta-expand the
primitive projection if |args| >= |args'|+1. *)
@@ -462,7 +560,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) =
let switch f a b = if on_left then f a b else f b a in
let eta evd =
- match kind_of_term termR with
+ match EConstr.kind evd termR with
| Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR ->
eta env evd false skR termR skF termF
| Construct u -> eta_constructor ts env evd skR u skF termF
@@ -472,7 +570,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| None ->
ise_try evd [consume_stack on_left apprF apprR; eta]
| Some lF ->
- let tR = Stack.zip apprR in
+ let tR = Stack.zip evd apprR in
miller_pfenning on_left
(fun () ->
ise_try evd
@@ -480,12 +578,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(fun i ->
if not (occur_rigidly ev i tR) then
let i,tF =
- if isRel tR || isVar tR then
+ if isRel i tR || isVar i tR then
(* Optimization so as to generate candidates *)
let i,ev = evar_absorb_arguments env i ev lF in
i,mkEvar ev
else
- i,Stack.zip apprF in
+ i,Stack.zip evd apprF in
switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
tF tR
else
@@ -496,8 +594,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* Evar must be undefined since we have flushed evars *)
let () = if !debug_unification then
let open Pp in
- Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())
- ++ fnl ()) in
+ Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in
match (flex_kind_of_term (fst ts) env evd term1 sk1,
flex_kind_of_term (fst ts) env evd term2 sk2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
@@ -509,9 +606,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *)
(* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *)
let ev1' = whd_evar i' (mkEvar ev1) in
- if isEvar ev1' then
+ if isEvar i' ev1' then
solve_simple_eqn (evar_conv_x ts) env i'
- (position_problem true pbty,destEvar ev1',term2)
+ (position_problem true pbty,destEvar i' ev1', term2)
else
evar_eqappr_x ts env evd pbty
((ev1', sk1), csts1) ((term2, sk2), csts2)
@@ -519,9 +616,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
(* we now unify r[?ev1] and ?ev2 *)
let ev2' = whd_evar i' (mkEvar ev2) in
- if isEvar ev2' then
+ if isEvar i' ev2' then
solve_simple_eqn (evar_conv_x ts) env i'
- (position_problem false pbty,destEvar ev2',Stack.zip(term1,r))
+ (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r))
else
evar_eqappr_x ts env evd pbty
((ev2', sk1), csts1) ((term2, sk2), csts2)
@@ -530,9 +627,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
(* we now unify ?ev1 and r[?ev2] *)
let ev1' = whd_evar i' (mkEvar ev1) in
- if isEvar ev1' then
+ if isEvar i' ev1' then
solve_simple_eqn (evar_conv_x ts) env i'
- (position_problem true pbty,destEvar ev1',Stack.zip(term2,r))
+ (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r))
else evar_eqappr_x ts env evd pbty
((ev1', sk1), csts1) ((term2, sk2), csts2)
| None, (UnifFailure _ as x) ->
@@ -585,7 +682,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1
| MaybeFlexible v1, MaybeFlexible v2 -> begin
- match kind_of_term term1, kind_of_term term2 with
+ match EConstr.kind evd term1, EConstr.kind evd term2 with
| LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
let f1 i = (* FO *)
ise_and i
@@ -596,8 +693,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(fun i ->
let b = nf_evar i b1 in
let t = nf_evar i t1 in
- let na = Nameops.name_max na1 na2 in
- evar_conv_x ts (push_rel (LocalDef (na,b,t)) env) i pbty c'1 c'2);
+ let na = Nameops.Name.pick na1 na2 in
+ evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
(fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
and f2 i =
let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
@@ -620,9 +717,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
ise_try evd [f1; f2]
(* Catch the p.c ~= p c' cases *)
- | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' ->
+ | Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' ->
let res =
- try Some (destApp (Retyping.expand_projection env evd p c []))
+ try Some (destApp evd (Retyping.expand_projection env evd p c []))
with Retyping.RetypeError _ -> None
in
(match res with
@@ -631,9 +728,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(appr2,csts2)
| None -> UnifFailure (evd,NotSameHead))
- | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') ->
+ | Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') ->
let res =
- try Some (destApp (Retyping.expand_projection env evd p' c' []))
+ try Some (destApp evd (Retyping.expand_projection env evd p' c' []))
with Retyping.RetypeError _ -> None
in
(match res with
@@ -648,14 +745,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
allow this identification (first-order unification of universes). Otherwise
fallback to unfolding.
*)
- let b,univs = Universes.eq_constr_universes term1 term2 in
- if b then
+ let univs = EConstr.eq_constr_universes env evd term1 term2 in
+ match univs with
+ | Some univs ->
ise_and i [(fun i ->
try Success (Evd.add_universe_constraints i univs)
with UniversesDiffer -> UnifFailure (i,NotSameHead)
| Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
(fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
- else UnifFailure (i,NotSameHead)
+ | None ->
+ UnifFailure (i,NotSameHead)
and f2 i =
(try
if not (snd ts) then raise Not_found
@@ -668,7 +767,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
if the first argument is a beta-redex (expand a constant
only if necessary) or the second argument is potentially
usable as a canonical projection or canonical value *)
- let rec is_unnamed (hd, args) = match kind_of_term hd with
+ let rec is_unnamed (hd, args) = match EConstr.kind i hd with
| (Var _|Construct _|Ind _|Const _|Prod _|Sort _) ->
Stack.not_purely_applicative args
| (CoFix _|Meta _|Rel _)-> true
@@ -689,7 +788,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let rhs_is_already_stuck =
rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
- if (isLambda term1 || rhs_is_already_stuck)
+ if (EConstr.isLambda i term1 || rhs_is_already_stuck)
&& (not (Stack.not_purely_applicative sk1)) then
evar_eqappr_x ~rhs_is_already_stuck ts env i pbty
(whd_betaiota_deltazeta_for_iota_state
@@ -703,16 +802,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
ise_try evd [f1; f2; f3]
end
- | Rigid, Rigid when isLambda term1 && isLambda term2 ->
- let (na1,c1,c'1) = destLambda term1 in
- let (na2,c2,c'2) = destLambda term2 in
+ | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 ->
+ let (na1,c1,c'1) = EConstr.destLambda evd term1 in
+ let (na2,c2,c'2) = EConstr.destLambda evd term2 in
assert app_empty;
ise_and evd
[(fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i ->
let c = nf_evar i c1 in
- let na = Nameops.name_max na1 na2 in
- evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i CONV c'1 c'2)]
+ let na = Nameops.Name.pick na1 na2 in
+ evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]
| Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
| Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1
@@ -745,17 +844,19 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
ise_try evd [f3; f4]
(* Eta-expansion *)
- | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
+ | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
eta env evd true sk1 term1 sk2 term2
- | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 ->
+ | _, Rigid when isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 ->
eta env evd false sk2 term2 sk1 term1
| Rigid, Rigid -> begin
- match kind_of_term term1, kind_of_term term2 with
+ match EConstr.kind evd term1, EConstr.kind evd term2 with
| Sort s1, Sort s2 when app_empty ->
(try
+ let s1 = ESorts.kind evd s1 in
+ let s2 = ESorts.kind evd s2 in
let evd' =
if pbty == CONV
then Evd.set_eq_sort env evd s1 s2
@@ -770,8 +871,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
[(fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i ->
let c = nf_evar i c1 in
- let na = Nameops.name_max n1 n2 in
- evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i pbty c'1 c'2)]
+ let na = Nameops.Name.pick n1 n2 in
+ evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
| Rel x1, Rel x2 ->
if Int.equal x1 x2 then
@@ -818,7 +919,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with
|_, (UnifFailure _ as x) -> x
|None, Success i' -> evar_conv_x ts env i' CONV term1 term2
- |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip (term1,sk1')) (Stack.zip (term2,sk2'))
+ |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2'))
end
| (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ ->
@@ -866,10 +967,8 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in
(i,t2::ks, m-1, test)
else
- let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
- let i = Sigma.Unsafe.of_evar_map i in
- let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
- let i' = Sigma.to_evar_map i' in
+ let dloc = Loc.tag Evar_kinds.InternalHole in
+ let (i', ev) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
(i', ev :: ks, m - 1,test))
(evd,[],List.length bs,fun i -> Success i) bs
in
@@ -887,19 +986,19 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
(fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2);
test;
(fun i -> evar_conv_x trs env i CONV h2
- (fst (decompose_app_vect (substl ks h))))]
+ (fst (decompose_app_vect i (substl ks h))))]
else UnifFailure(evd,(*dummy*)NotSameHead)
and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
- | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
+ | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite ->
let pars = mib.Declarations.mind_nparams in
(try
let l1' = Stack.tail pars sk1 in
let l2' =
- let term = Stack.zip (term2,sk2) in
- List.map (fun p -> mkProj (Projection.make p false, term)) (Array.to_list projs)
+ let term = Stack.zip evd (term2,sk2) in
+ List.map (fun p -> EConstr.mkProj (Projection.make p false, term)) (Array.to_list projs)
in
exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1'
(Stack.append_app_list l2' Stack.empty)
@@ -914,8 +1013,8 @@ let evar_conv_x ts = evar_conv_x (ts, true)
(* Profiling *)
let evar_conv_x =
if Flags.profile then
- let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in
- Profile.profile6 evar_conv_xkey evar_conv_x
+ let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in
+ CProfile.profile6 evar_conv_xkey evar_conv_x
else evar_conv_x
let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x ()
@@ -943,50 +1042,57 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) =
let choose_less_dependent_instance evk evd term args =
let evi = Evd.find_undefined evd evk in
let subst = make_pure_subst evi args in
- let subst' = List.filter (fun (id,c) -> Term.eq_constr c term) subst in
+ let subst' = List.filter (fun (id,c) -> EConstr.eq_constr evd c term) subst in
match subst' with
| [] -> None
- | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
+ | (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd)
-open Context.Named.Declaration
let apply_on_subterm env evdref f c t =
let rec applyrec (env,(k,c) as acc) t =
(* By using eq_constr, we make an approximation, for instance, we *)
(* could also be interested in finding a term u convertible to t *)
(* such that c occurs in u *)
- if e_eq_constr_univs evdref c t then f k
+ let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with
+ | None -> false
+ | Some cstr ->
+ try ignore (Evd.add_universe_constraints !evdref cstr); true
+ with UniversesDiffer -> false
+ in
+ if eq_constr c t then f k
else
- match kind_of_term t with
- | Evar (evk,args) when Evd.is_undefined !evdref evk ->
+ match EConstr.kind !evdref t with
+ | Evar (evk,args) ->
let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
let g decl a = if is_local_assum decl then applyrec acc a else a in
mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
| _ ->
- map_constr_with_binders_left_to_right
+ map_constr_with_binders_left_to_right !evdref
(fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
applyrec acc t
in
applyrec (env,(0,c)) t
-let filter_possible_projections c ty ctxt args =
+let filter_possible_projections evd c ty ctxt args =
(* Since args in the types will be replaced by holes, we count the
fv of args to have a well-typed filter; don't know how necessary
- it is however to have a well-typed filter here *)
- let fv1 = free_rels (mkApp (c,args)) (* Hack: locally untyped *) in
- let fv2 = collect_vars (mkApp (c,args)) in
+ it is however to have a well-typed filter here *)
+ let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in
+ let fv2 = collect_vars evd (mkApp (c,args)) in
let len = Array.length args in
- let tyvars = collect_vars ty in
+ let tyvars = collect_vars evd ty in
List.map_i (fun i decl ->
let () = assert (i < len) in
let a = Array.unsafe_get args i in
- (match decl with LocalAssum _ -> false | LocalDef (_,c,_) -> not (isRel c || isVar c)) ||
+ (match decl with
+ | NamedDecl.LocalAssum _ -> false
+ | NamedDecl.LocalDef (_,c,_) -> not (isRel evd (EConstr.of_constr c) || isVar evd (EConstr.of_constr c))) ||
a == c ||
(* Here we make an approximation, for instance, we could also be *)
(* interested in finding a term u convertible to c such that a occurs *)
(* in u *)
- isRel a && Int.Set.mem (destRel a) fv1 ||
- isVar a && Id.Set.mem (destVar a) fv2 ||
- Id.Set.mem (get_id decl) tyvars)
+ isRel evd a && Int.Set.mem (destRel evd a) fv1 ||
+ isVar evd a && Id.Set.mem (destVar evd a) fv2 ||
+ Id.Set.mem (NamedDecl.get_id decl) tyvars)
0 ctxt
let solve_evars = ref (fun _ -> failwith "solve_evars not installed")
@@ -1017,39 +1123,39 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
let env_evar = evar_filtered_env evi in
let sign = named_context_val env_evar in
let ctxt = evar_filtered_context evi in
- let instance = List.map mkVar (List.map get_id ctxt) in
+ let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in
let rec make_subst = function
- | decl'::ctxt', c::l, occs::occsl when isVarId (get_id decl') c ->
+ | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c ->
begin match occs with
| Some _ ->
- error "Cannot force abstraction on identity instance."
+ user_err Pp.(str "Cannot force abstraction on identity instance.")
| None ->
make_subst (ctxt',l,occsl)
end
| decl'::ctxt', c::l, occs::occsl ->
- let (id,_,t) = to_tuple decl' in
+ let id = NamedDecl.get_id decl' in
+ let t = EConstr.of_constr (NamedDecl.get_type decl') in
let evs = ref [] in
let ty = Retyping.get_type_of env_rhs evd c in
- let filter' = filter_possible_projections c ty ctxt args in
+ let filter' = filter_possible_projections evd c ty ctxt args in
(id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl)
| _, _, [] -> []
- | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in
+ | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in
let rec set_holes evdref rhs = function
| (id,_,c,cty,evsref,filter,occs)::subst ->
let set_var k =
match occs with
| Some Locus.AllOccurrences -> mkVar id
- | Some _ -> error "Selection of specific occurrences not supported"
+ | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported")
| None ->
let evty = set_holes evdref cty subst in
let instance = Filter.filter_list filter instance in
- let evd = Sigma.Unsafe.of_evar_map !evdref in
- let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in
- let evd = Sigma.to_evar_map evd in
+ let evd = !evdref in
+ let (evd, ev) = new_evar_instance sign evd evty ~filter instance in
evdref := evd;
- evsref := (fst (destEvar ev),evty)::!evsref;
+ evsref := (fst (destEvar !evdref ev),evty)::!evsref;
ev in
set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst
| [] -> rhs in
@@ -1077,12 +1183,12 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
(* We force abstraction over this unconstrained occurrence *)
(* and we use typing to propagate this instantiation *)
(* This is an arbitrary choice *)
- let evd = Evd.define evk (mkVar id) evd in
+ let evd = Evd.define evk (Constr.mkVar id) evd in
match evar_conv_x ts env_evar evd CUMUL idty evty with
- | UnifFailure _ -> error "Cannot find an instance"
+ | UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
| Success evd ->
match reconsider_unif_constraints (evar_conv_x ts) evd with
- | UnifFailure _ -> error "Cannot find an instance"
+ | UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
| Success evd ->
evd
else
@@ -1095,15 +1201,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
force_instantiation evd !evsref
| [] ->
let evd =
- try Evarsolve.check_evar_instance evd evk rhs
+ try Evarsolve.check_evar_instance evd evk rhs
(evar_conv_x full_transparent_state)
with IllTypedInstance _ -> raise (TypingFailed evd)
in
- Evd.define evk rhs evd
+ Evd.define evk (EConstr.Unsafe.to_constr rhs) evd
in
abstract_free_holes evd subst, true
with TypingFailed evd -> evd, false
+let to_pb (pb, env, t1, t2) =
+ (pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2)
+
let second_order_matching_with_args ts env evd pbty ev l t =
(*
let evd,ev = evar_absorb_arguments env evd ev l in
@@ -1113,18 +1222,22 @@ let second_order_matching_with_args ts env evd pbty ev l t =
else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
if b then Success evd else
*)
- let pb = (pbty,env,mkApp(mkEvar ev,l),t) in
+ let pb = to_pb (pbty,env,mkApp(mkEvar ev,l),t) in
UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))
let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in
- let (term1,l1 as appr1) = try destApp t1 with DestKO -> (t1, [||]) in
- let (term2,l2 as appr2) = try destApp t2 with DestKO -> (t2, [||]) in
+ let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in
+ let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
+ let () = if !debug_unification then
+ let open Pp in
+ Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1
+ ++ cut () ++ print_constr t2 ++ cut ())) in
let app_empty = Array.is_empty l1 && Array.is_empty l2 in
- match kind_of_term term1, kind_of_term term2 with
+ match EConstr.kind evd term1, EConstr.kind evd term2 with
| Evar (evk1,args1), (Rel _|Var _) when app_empty
- && List.for_all (fun a -> Term.eq_constr a term2 || isEvar a)
+ && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a)
(remove_instance_local_defs evd evk1 args1) ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
@@ -1132,9 +1245,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
| Some evd -> Success evd
| None ->
let reason = ProblemBeyondCapabilities in
- UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
+ UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason)))
| (Rel _|Var _), Evar (evk2,args2) when app_empty
- && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a)
+ && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
(remove_instance_local_defs evd evk2 args2) ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
@@ -1142,7 +1255,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
| Some evd -> Success evd
| None ->
let reason = ProblemBeyondCapabilities in
- UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
+ UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason)))
| Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
Success (solve_refl ~can_drop:true f env evd
@@ -1176,29 +1289,31 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
evar_conv_x ts env evd pbty t1 t2
let error_cannot_unify env evd pb ?reason t1 t2 =
- Pretype_errors.error_cannot_unify_loc
- (loc_of_conv_pb evd pb) env
+ Pretype_errors.error_cannot_unify
+ ?loc:(loc_of_conv_pb evd pb) env
evd ?reason (t1, t2)
let check_problems_are_solved env evd =
match snd (extract_all_conv_pbs evd) with
- | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2
+ | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb (EConstr.of_constr t1) (EConstr.of_constr t2)
| _ -> ()
+exception MaxUndefined of (Evar.t * evar_info * Constr.t list)
+
let max_undefined_with_candidates evd =
- (* If evar were ordered with highest index first, fold_undefined
- would be going decreasingly and we could use fold_undefined to
- find the undefined evar of maximum index (alternatively,
- max_bindings from ocaml 3.12 could be used); instead we traverse
- the whole map *)
- let l = Evd.fold_undefined
- (fun evk ev_info evars ->
- match ev_info.evar_candidates with
- | None -> evars
- | Some l -> (evk,ev_info,l)::evars) evd [] in
- match l with
- | [] -> None
- | a::l -> Some (List.last (a::l))
+ let fold evk evi () = match evi.evar_candidates with
+ | None -> ()
+ | Some l -> raise (MaxUndefined (evk, evi, l))
+ in
+ (** [fold_right] traverses the undefined map in decreasing order of indices.
+ The evar with candidates of maximum index is thus the first evar with
+ candidates found by a [fold_right] traversal. This has a significant impact on
+ performance. *)
+ try
+ let () = Evar.Map.fold_right fold (Evd.undefined_map evd) () in
+ None
+ with MaxUndefined ans ->
+ Some ans
let rec solve_unconstrained_evars_with_candidates ts evd =
(* max_undefined is supposed to return the most recent, hence
@@ -1207,11 +1322,11 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
| None -> evd
| Some (evk,ev_info,l) ->
let rec aux = function
- | [] -> error "Unsolvable existential variables."
+ | [] -> user_err Pp.(str "Unsolvable existential variables.")
| a::l ->
try
let conv_algo = evar_conv_x ts in
- let evd = check_evar_instance evd evk a conv_algo in
+ let evd = check_evar_instance evd evk (EConstr.of_constr a) conv_algo in
let evd = Evd.define evk a evd in
match reconsider_unif_constraints conv_algo evd with
| Success evd -> solve_unconstrained_evars_with_candidates ts evd
@@ -1229,11 +1344,11 @@ let solve_unconstrained_impossible_cases env evd =
match ev_info.evar_source with
| loc,Evar_kinds.ImpossibleCase ->
let j, ctx = coq_unit_judge () in
- let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in
+ let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
let ty = j_type j in
let conv_algo = evar_conv_x full_transparent_state in
let evd' = check_evar_instance evd' evk ty conv_algo in
- Evd.define evk ty evd'
+ Evd.define evk (EConstr.Unsafe.to_constr ty) evd'
| _ -> evd') evd evd
let solve_unif_constraints_with_heuristics env
@@ -1242,6 +1357,8 @@ let solve_unif_constraints_with_heuristics env
let rec aux evd pbs progress stuck =
match pbs with
| (pbty,env,t1,t2 as pb) :: pbs ->
+ let t1 = EConstr.of_constr t1 in
+ let t2 = EConstr.of_constr t2 in
(match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with
| Success evd' ->
let (evd', rest) = extract_all_conv_pbs evd' in
@@ -1258,6 +1375,8 @@ let solve_unif_constraints_with_heuristics env
match stuck with
| [] -> (* We're finished *) evd
| (pbty,env,t1,t2 as pb) :: _ ->
+ let t1 = EConstr.of_constr t1 in
+ let t2 = EConstr.of_constr t2 in
(* There remains stuck problems *)
error_cannot_unify env evd pb t1 t2
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 20:47:55 +0000