diff options
| -rw-r--r-- | engine/evarutil.mli | 2 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 6 | ||||
| -rw-r--r-- | pretyping/cases.ml | 12 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 85 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 475 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 11 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 8 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 8 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 10 | ||||
| -rw-r--r-- | pretyping/typing.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 21 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 22 |
13 files changed, 364 insertions, 306 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 7fdc7aac7..a2e2a07dd 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -76,7 +76,7 @@ val new_evar_instance : ?principal:bool -> constr list -> (constr, 'r) Sigma.sigma -val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list +val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list val safe_evar_value : evar_map -> existential -> constr option diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 425bb2d6f..36a96fdb5 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -259,7 +259,7 @@ let refresh_universes ty k = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in - let evm, ty = refresh_type env evm ty in + let evm, ty = refresh_type env evm (EConstr.of_constr ty) in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty) end } @@ -376,7 +376,7 @@ let discriminate_tac (cstr,u as cstru) p = let identity = Universes.constr_of_global (Lazy.force _I) in let trivial = Universes.constr_of_global (Lazy.force _True) in let evm = Tacmach.New.project gl in - let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in + let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in let outtype = mkSort outtype in let pred = mkLambda(Name xid,outtype,mkRel 1) in @@ -481,7 +481,7 @@ let mk_eq f c1 c2 k = Proofview.Goal.enter { enter = begin fun gl -> let open Tacmach.New in let evm, ty = pf_apply type_of gl c1 in - let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in + let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm (EConstr.of_constr ty) in let term = mkApp (fc, [| ty; c1; c2 |]) in let evm, _ = type_of (pf_env gl) evm term in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 915cd261d..a68daf4e5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -78,6 +78,9 @@ let list_try_compile f l = let force_name = let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na +let to_conv_fun f = (); fun env sigma pb c1 c2 -> + f env sigma pb (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) + (************************************************************************) (* Pattern-matching compilation (Cases) *) (************************************************************************) @@ -1583,7 +1586,7 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t = | LocalAssum _ -> p in let p = traverse_local_defs p in let u = lift (n' - n) u in - try Some (p, u, expand_vars_in_term extenv sigma u) + try Some (p, u, EConstr.Unsafe.to_constr (expand_vars_in_term extenv sigma (EConstr.of_constr u))) (* pedrot: does this really happen to raise [Failure _]? *) with Failure _ -> None in let subst0 = List.map_filter map subst in @@ -1628,14 +1631,15 @@ let abstract_tycon loc env evdref subst tycon extenv t = | Rel n when is_local_def (lookup_rel n env) -> t | Evar ev -> let ty = get_type_of env !evdref (EConstr.of_constr t) in - let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in + let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref (EConstr.of_constr ty) in let inst = List.map_i (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in let ev' = e_new_evar env evdref ~src ty in - begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,EConstr.of_constr (substl inst ev')) with + let ev = (fst ev, Array.map EConstr.of_constr (snd ev)) in + begin match solve_simple_eqn (to_conv_fun (evar_conv_x full_transparent_state)) env !evdref (None,ev,EConstr.of_constr (substl inst ev')) with | Success evd -> evdref := evd | UnifFailure _ -> assert false end; @@ -1650,7 +1654,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = let vl = List.map pi1 good in let ty = let ty = get_type_of env !evdref (EConstr.of_constr t) in - Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty + Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref (EConstr.of_constr ty) in let ty = lift (-k) (aux x ty) in let depvl = free_rels !evdref (EConstr.of_constr ty) in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 4540af28b..8f3f671ab 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -42,6 +42,9 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } +let to_conv_fun f = (); fun env sigma pb c1 c2 -> + f env sigma pb (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) + let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then @@ -341,7 +344,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = env evd term1 term2 in if b then Success evd - else UnifFailure (evd, ConversionFailed (env,term1,term2)) + else UnifFailure (evd, ConversionFailed (env,EConstr.of_constr term1,EConstr.of_constr term2)) with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with @@ -361,15 +364,15 @@ let rec evar_conv_x ts env evd pbty term1 term2 = (whd_nored_state evd (EConstr.of_constr term1,Stack.empty), Cst_stack.empty) (whd_nored_state evd (EConstr.of_constr term2,Stack.empty), Cst_stack.empty) in - begin match kind_of_term term1, kind_of_term term2 with + begin match EConstr.kind evd (EConstr.of_constr term1), EConstr.kind evd (EConstr.of_constr term2) with | Evar ev, _ when Evd.is_undefined evd (fst ev) -> - (match solve_simple_eqn (evar_conv_x ts) env evd + (match solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd (position_problem true pbty,ev, EConstr.of_constr 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 + (match solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd (position_problem false pbty,ev, EConstr.of_constr term1) with | UnifFailure (_, OccurCheck _) -> (* Eta-expansion might apply *) default () @@ -383,13 +386,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (i, NotSameHead) in let miller_pfenning on_left fallback ev lF tM evd = - let lF = List.map EConstr.Unsafe.to_constr lF in 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 = EConstr.of_constr (nf_evar evd (EConstr.Unsafe.to_constr tM)) (** FIXME *) in let t2 = solve_pattern_eqn env evd l1' t2 in - solve_simple_eqn (evar_conv_x ts) env evd + solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd (position_problem on_left pbty,ev, EConstr.of_constr t2) in let consume_stack on_left (termF,skF) (termO,skO) evd = @@ -441,7 +443,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (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)) (zip evd apprF) tM else quick_fail i) - ev lF tM i + ev lF (EConstr.of_constr tM) i and consume (termF,skF as apprF) (termM,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then consume_stack on_left apprF apprM i @@ -510,8 +512,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) tF tR else - UnifFailure (evd,OccurCheck (fst ev,tR)))]) - ev lF tR evd + UnifFailure (evd,OccurCheck (fst ev,EConstr.of_constr tR)))]) + (fst ev, Array.map EConstr.of_constr (snd ev)) lF (EConstr.of_constr tR) evd in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) @@ -529,33 +531,33 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | None, Success i' -> (* 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 - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar ev1', term2) + let ev1' = EConstr.of_constr (whd_evar i' (mkEvar ev1)) in + if EConstr.isEvar i' ev1' then + solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i' + (position_problem true pbty,EConstr.destEvar i' ev1', term2) else evar_eqappr_x ts env evd pbty - ((EConstr.of_constr ev1', sk1), csts1) ((term2, sk2), csts2) + ((ev1', sk1), csts1) ((term2, sk2), csts2) | Some (r,[]), Success i' -> (* 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 - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem false pbty,destEvar ev2',Stack.zip evd (term1,r)) + let ev2' = EConstr.of_constr (whd_evar i' (mkEvar ev2)) in + if EConstr.isEvar i' ev2' then + solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i' + (position_problem false pbty,EConstr.destEvar i' ev2',Stack.zip evd (term1,r)) else evar_eqappr_x ts env evd pbty - ((EConstr.of_constr ev2', sk1), csts1) ((term2, sk2), csts2) + ((ev2', sk1), csts1) ((term2, sk2), csts2) | Some ([],r), Success i' -> (* Symmetrically *) (* 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 - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar ev1',Stack.zip evd (term2,r)) + let ev1' = EConstr.of_constr (whd_evar i' (mkEvar ev1)) in + if EConstr.isEvar i' ev1' then + solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i' + (position_problem true pbty,EConstr.destEvar i' ev1',Stack.zip evd (term2,r)) else evar_eqappr_x ts env evd pbty - ((EConstr.of_constr ev1', sk1), csts1) ((term2, sk2), csts2) + ((ev1', sk1), csts1) ((term2, sk2), csts2) | None, (UnifFailure _ as x) -> (* sk1 and sk2 have no common outer part *) if Stack.not_purely_applicative sk2 then @@ -590,9 +592,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if Evar.equal sp1 sp2 then match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with |None, Success i' -> - Success (solve_refl (fun env i pbty a1 a2 -> - is_success (evar_conv_x ts env i pbty a1 a2)) - env i' (position_problem true pbty) sp1 al1 al2) + Success (solve_refl (to_conv_fun (fun env i pbty a1 a2 -> + is_success (evar_conv_x ts env i pbty a1 a2))) + env i' (position_problem true pbty) sp1 (Array.map EConstr.of_constr al1) (Array.map EConstr.of_constr al2)) |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (i,NotSameArgSize) else UnifFailure (i,NotSameHead) @@ -600,10 +602,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; f2] | Flexible ev1, MaybeFlexible v2 -> - flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) (EConstr.of_constr v2) + flex_maybeflex true (fst ev1, Array.map EConstr.of_constr (snd ev1)) (appr1,csts1) (appr2,csts2) (EConstr.of_constr v2) | MaybeFlexible v1, Flexible ev2 -> - flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) (EConstr.of_constr v1) + flex_maybeflex false (fst ev2, Array.map EConstr.of_constr (snd ev2)) (appr2,csts2) (appr1,csts1) (EConstr.of_constr v1) | MaybeFlexible v1, MaybeFlexible v2 -> begin match kind_of_term (EConstr.Unsafe.to_constr term1), kind_of_term (EConstr.Unsafe.to_constr term2) with @@ -964,7 +966,8 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) = if is_defined i (fst ev1) then evar_conv_x ts env i CONV t2 (mkEvar ev1) else - solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1, EConstr.of_constr t2))] + let ev1 = (fst ev1, Array.map EConstr.of_constr (snd ev1)) in + solve_simple_eqn ~choose:true (to_conv_fun (evar_conv_x ts)) env i (None,ev1, EConstr.of_constr t2))] let choose_less_dependent_instance evk evd term args = let evi = Evd.find_undefined evd evk in @@ -1109,7 +1112,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = match evar_conv_x ts env_evar evd CUMUL idty evty with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> - match reconsider_conv_pbs (evar_conv_x ts) evd with + match reconsider_conv_pbs (to_conv_fun (evar_conv_x ts)) evd with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> evd @@ -1123,8 +1126,8 @@ 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 - (evar_conv_x full_transparent_state) + try Evarsolve.check_evar_instance evd evk (EConstr.of_constr rhs) + (to_conv_fun (evar_conv_x full_transparent_state)) with IllTypedInstance _ -> raise (TypingFailed evd) in Evd.define evk rhs evd @@ -1173,11 +1176,13 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = UnifFailure (evd, CannotSolveConstraint ((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 (EConstr.of_constr x) (EConstr.of_constr y) in - Success (solve_refl ~can_drop:true f env evd - (position_problem true pbty) evk1 args1 args2) + Success (solve_refl ~can_drop:true (to_conv_fun f) env evd + (position_problem true pbty) evk1 (Array.map EConstr.of_constr args1) (Array.map EConstr.of_constr args2)) | Evar ev1, Evar ev2 when app_empty -> + let ev1 = (fst ev1, Array.map EConstr.of_constr (snd ev1)) in + let ev2 = (fst ev2, Array.map EConstr.of_constr (snd ev2)) in Success (solve_evar_evar ~force:true - (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd + (evar_define (to_conv_fun (evar_conv_x ts)) ~choose:true) (to_conv_fun (evar_conv_x ts)) env evd (position_problem true pbty) ev1 ev2) | Evar ev1,_ when Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) @@ -1239,9 +1244,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | 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) (to_conv_fun conv_algo) in let evd = Evd.define evk a evd in - match reconsider_conv_pbs conv_algo evd with + match reconsider_conv_pbs (to_conv_fun conv_algo) evd with | Success evd -> solve_unconstrained_evars_with_candidates ts evd | UnifFailure _ -> aux l with @@ -1260,7 +1265,7 @@ let solve_unconstrained_impossible_cases env evd = 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 + let evd' = check_evar_instance evd' evk (EConstr.of_constr ty) (to_conv_fun conv_algo) in Evd.define evk ty evd' | _ -> evd') evd evd diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 86ef8f56f..8a22aed2f 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -22,13 +22,14 @@ open Pretype_errors open Sigma.Notations let normalize_evar evd ev = - match kind_of_term (whd_evar evd (mkEvar ev)) with + let open EConstr in + match EConstr.kind evd (mkEvar ev) with | Evar (evk,args) -> (evk,args) | _ -> assert false -let get_polymorphic_positions f = +let get_polymorphic_positions sigma f = let open Declarations in - match kind_of_term f with + match EConstr.kind sigma f with | Ind (ind, u) | Construct ((ind, _), u) -> let mib,oib = Global.lookup_inductive ind in (match oib.mind_arity with @@ -49,10 +50,11 @@ let refresh_level evd s = let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) pbty env evd t = + let open EConstr in let evdref = ref evd in let modified = ref false in let rec refresh status dir t = - match kind_of_term t with + match EConstr.kind !evdref t with | Sort (Type u as s) when (match Univ.universe_level u with | None -> true @@ -72,20 +74,20 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) | _ -> t (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars top t = - match kind_of_term (whd_evar !evdref t) with - | App (f, args) when is_template_polymorphic env !evdref (EConstr.of_constr f) -> - let pos = get_polymorphic_positions f in + match EConstr.kind !evdref t with + | App (f, args) when is_template_polymorphic env !evdref f -> + let pos = get_polymorphic_positions !evdref f in refresh_polymorphic_positions args pos - | App (f, args) when top && isEvar f -> + | App (f, args) when top && isEvar !evdref f -> refresh_term_evars true false f; Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh univ_flexible true evi.evar_concl in + let ty' = refresh univ_flexible true (EConstr.of_constr evi.evar_concl) in if !modified then - evdref := Evd.add !evdref ev {evi with evar_concl = ty'} + evdref := Evd.add !evdref ev {evi with evar_concl = EConstr.Unsafe.to_constr ty'} else () - | _ -> Constr.iter (refresh_term_evars onevars false) t + | _ -> EConstr.iter !evdref (refresh_term_evars onevars false) t and refresh_polymorphic_positions args pos = let rec aux i = function | Some l :: ls -> @@ -100,17 +102,17 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) in aux 0 pos in let t' = - if isArity t then + if isArity !evdref t then (match pbty with | None -> t | Some dir -> refresh status dir t) else (refresh_term_evars false true t; t) in - if !modified then !evdref, t' else !evdref, t + if !modified then !evdref, EConstr.Unsafe.to_constr t' else !evdref, EConstr.Unsafe.to_constr t let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c = let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in - refresh_universes (Some false) env sigma ty + refresh_universes (Some false) env sigma (EConstr.of_constr ty) (************************) @@ -127,6 +129,8 @@ let test_success conv_algo env evd c c' rhs = is_success (conv_algo env evd c c' rhs) let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = + let t1 = EConstr.Unsafe.to_constr t1 in + let t2 = EConstr.Unsafe.to_constr t2 in match pbty with | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd @@ -134,29 +138,30 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = (* We retype applications to ensure the universe constraints are collected *) -exception IllTypedInstance of env * types * types +exception IllTypedInstance of env * EConstr.types * EConstr.types let recheck_applications conv_algo env evdref t = + let open EConstr in let rec aux env t = - match kind_of_term t with + match EConstr.kind !evdref t with | App (f, args) -> let () = aux env f in - let fty = Retyping.get_type_of env !evdref (EConstr.of_constr f) in - let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref (EConstr.of_constr x)) args in + let fty = Retyping.get_type_of env !evdref f in + let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in let rec aux i ty = if i < Array.length argsty then - match kind_of_term (whd_all env !evdref (EConstr.of_constr ty)) with + match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref ty)) with | Prod (na, dom, codom) -> - (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with + (match conv_algo env !evdref Reduction.CUMUL (EConstr.of_constr argsty.(i)) dom with | Success evd -> evdref := evd; - aux (succ i) (subst1 args.(i) codom) + aux (succ i) (Vars.subst1 args.(i) codom) | UnifFailure (evd, reason) -> - Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom)) - | _ -> raise (IllTypedInstance (env, ty, argsty.(i))) + Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), EConstr.Unsafe.to_constr dom)) + | _ -> raise (IllTypedInstance (env, ty, EConstr.of_constr argsty.(i))) else () - in aux 0 fty + in aux 0 (EConstr.of_constr fty) | _ -> - iter_constr_with_full_binders (fun d env -> push_rel d env) aux env t + iter_with_full_binders !evdref (fun d env -> push_rel d env) aux env t in aux env t @@ -169,7 +174,7 @@ type 'a update = | NoUpdate open Context.Named.Declaration -let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign +let inst_of_vars sign = Array.map_of_list (get_id %> EConstr.mkVar) sign let restrict_evar_key evd evk filter candidates = match filter, candidates with @@ -186,7 +191,7 @@ let restrict_evar_key evd evk filter candidates = | Some filter -> filter in let candidates = match candidates with | NoUpdate -> evi.evar_candidates - | UpdateWith c -> Some c in + | UpdateWith c -> Some (List.map EConstr.Unsafe.to_constr c) in let sigma = Sigma.Unsafe.of_evar_map evd in let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in (Sigma.to_evar_map sigma, evk) @@ -216,27 +221,25 @@ let restrict_instance evd evk filter argsv = open Context.Rel.Declaration let noccur_evar env evd evk c = + let open EConstr in let cache = ref Int.Set.empty (* cache for let-ins *) in let rec occur_rec check_types (k, env as acc) c = - match kind_of_term c with + match EConstr.kind evd c with | Evar (evk',args' as ev') -> - (match safe_evar_value evd ev' with - | Some c -> occur_rec check_types acc c - | None -> - if Evar.equal evk evk' then raise Occur - else (if check_types then - occur_rec false acc (existential_type evd ev'); - Array.iter (occur_rec check_types acc) args')) + if Evar.equal evk evk' then raise Occur + else (if check_types then + occur_rec false acc (existential_type evd ev'); + Array.iter (occur_rec check_types acc) args') | Rel i when i > k -> if not (Int.Set.mem (i-k) !cache) then let decl = Environ.lookup_rel i env in if check_types then - (cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (get_type decl))); + (cache := Int.Set.add (i-k) !cache; occur_rec false acc (Vars.lift i (EConstr.of_constr (get_type decl)))); (match decl with | LocalAssum _ -> () - | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i b)) + | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (Vars.lift i (EConstr.of_constr b))) | Proj (p,c) -> occur_rec true acc c - | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) + | _ -> iter_with_full_binders evd (fun rd (k,env) -> (succ k, push_rel rd env)) (occur_rec check_types) acc c in try occur_rec false (0,env) c; true with Occur -> false @@ -249,13 +252,14 @@ let noccur_evar env evd evk c = dependencies in variables are canonically associated to the most ancient variable in its family of aliased variables *) -let compute_var_aliases sign = +let compute_var_aliases sign sigma = let open Context.Named.Declaration in List.fold_right (fun decl aliases -> let id = get_id decl in match decl with | LocalDef (_,t,_) -> - (match kind_of_term t with + let t = EConstr.of_constr t in + (match EConstr.kind sigma t with | Var id' -> let aliases_of_id = try Id.Map.find id' aliases with Not_found -> [] in @@ -265,13 +269,16 @@ let compute_var_aliases sign = | LocalAssum _ -> aliases) sign Id.Map.empty -let compute_rel_aliases var_aliases rels = +let compute_rel_aliases var_aliases rels sigma = + let open EConstr in snd (List.fold_right (fun decl (n,aliases) -> (n-1, match decl with | LocalDef (_,t,u) -> - (match kind_of_term t with + let t = EConstr.of_constr t in + let u = EConstr.of_constr u in + (match EConstr.kind sigma t with | Var id' -> let aliases_of_n = try Id.Map.find id' var_aliases with Not_found -> [] in @@ -281,52 +288,57 @@ let compute_rel_aliases var_aliases rels = try Int.Map.find (p+n) aliases with Not_found -> [] in Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases | _ -> - Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases) + Int.Map.add n [Vars.lift n (mkCast(t,DEFAULTcast,u))] aliases) | LocalAssum _ -> aliases) ) rels (List.length rels,Int.Map.empty)) -let make_alias_map env = +let make_alias_map env sigma = (* We compute the chain of aliases for each var and rel *) - let var_aliases = compute_var_aliases (named_context env) in - let rel_aliases = compute_rel_aliases var_aliases (rel_context env) in + let var_aliases = compute_var_aliases (named_context env) sigma in + let rel_aliases = compute_rel_aliases var_aliases (rel_context env) sigma in (var_aliases,rel_aliases) let lift_aliases n (var_aliases,rel_aliases as aliases) = + let open EConstr in if Int.equal n 0 then aliases else (var_aliases, - Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (lift n) l)) + Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (Vars.lift n) l)) rel_aliases Int.Map.empty) -let get_alias_chain_of aliases x = match kind_of_term x with +let get_alias_chain_of sigma aliases x = match EConstr.kind sigma x with | Rel n -> (try Int.Map.find n (snd aliases) with Not_found -> []) | Var id -> (try Id.Map.find id (fst aliases) with Not_found -> []) | _ -> [] -let normalize_alias_opt aliases x = - match get_alias_chain_of aliases x with +let normalize_alias_opt sigma aliases x = + let open EConstr in + match get_alias_chain_of sigma aliases x with | [] -> None - | a::_ when isRel a || isVar a -> Some a + | a::_ when isRel sigma a || isVar sigma a -> Some a | [_] -> None | _::a::_ -> Some a -let normalize_alias aliases x = - match normalize_alias_opt aliases x with +let normalize_alias sigma aliases x = + match normalize_alias_opt sigma aliases x with | Some a -> a | None -> x -let normalize_alias_var var_aliases id = - destVar (normalize_alias (var_aliases,Int.Map.empty) (mkVar id)) +let normalize_alias_var sigma var_aliases id = + let open EConstr in + destVar sigma (normalize_alias sigma (var_aliases,Int.Map.empty) (mkVar id)) -let extend_alias decl (var_aliases,rel_aliases) = +let extend_alias sigma decl (var_aliases,rel_aliases) = + let open EConstr in let rel_aliases = - Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l)) + Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (Vars.lift 1) l)) rel_aliases Int.Map.empty in let rel_aliases = match decl with | LocalDef(_,t,_) -> - (match kind_of_term t with + let t = EConstr.of_constr t in + (match EConstr.kind sigma t with | Var id' -> let aliases_of_binder = try Id.Map.find id' var_aliases with Not_found -> [] in @@ -336,37 +348,38 @@ let extend_alias decl (var_aliases,rel_aliases) = try Int.Map.find (p+1) rel_aliases with Not_found -> [] in Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases | _ -> - Int.Map.add 1 [lift 1 t] rel_aliases) + Int.Map.add 1 [Vars.lift 1 t] rel_aliases) | LocalAssum _ -> rel_aliases in (var_aliases, rel_aliases) -let expand_alias_once aliases x = - match get_alias_chain_of aliases x with +let expand_alias_once sigma aliases x = + match get_alias_chain_of sigma aliases x with | [] -> None | l -> Some (List.last l) -let expansions_of_var aliases x = - match get_alias_chain_of aliases x with +let expansions_of_var sigma aliases x = + let open EConstr in + match get_alias_chain_of sigma aliases x with | [] -> [x] - | a::_ as l when isRel a || isVar a -> x :: List.rev l + | a::_ as l when isRel sigma a || isVar sigma a -> x :: List.rev l | _::l -> x :: List.rev l -let expansion_of_var aliases x = - match get_alias_chain_of aliases x with +let expansion_of_var sigma aliases x = + match get_alias_chain_of sigma aliases x with | [] -> x | a::_ -> a -let rec expand_vars_in_term_using sigma aliases t = match kind_of_term t with +let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t with | Rel _ | Var _ -> - normalize_alias aliases t + normalize_alias sigma aliases t | _ -> - let self aliases c = EConstr.of_constr (expand_vars_in_term_using sigma aliases (EConstr.Unsafe.to_constr c)) in - EConstr.Unsafe.to_constr (map_constr_with_full_binders sigma - extend_alias self aliases (EConstr.of_constr t)) + let self aliases c = expand_vars_in_term_using sigma aliases c in + map_constr_with_full_binders sigma (extend_alias sigma) self aliases t -let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env) +let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env sigma) -let free_vars_and_rels_up_alias_expansion aliases c = +let free_vars_and_rels_up_alias_expansion sigma aliases c = + let open EConstr in let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in @@ -379,25 +392,25 @@ let free_vars_and_rels_up_alias_expansion aliases c = | Var s -> cache_var := Id.Set.add s !cache_var | _ -> () in let rec frec (aliases,depth) c = - match kind_of_term c with + match EConstr.kind sigma c with | Rel _ | Var _ as ck -> if is_in_cache depth ck then () else begin put_in_cache depth ck; - let c' = expansion_of_var aliases c in - (if c != c' then (* expansion, hence a let-in *) - match kind_of_term c with + let c' = expansion_of_var sigma aliases c in + (if c != c' then (* expansion, hence a let-in *) (** FIXME *) + match EConstr.kind sigma c with | Var id -> acc4 := Id.Set.add id !acc4 | Rel n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3 | _ -> ()); - match kind_of_term c' with + match EConstr.kind sigma c' with | Var id -> acc2 := Id.Set.add id !acc2 | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1 | _ -> frec (aliases,depth) c end | Const _ | Ind _ | Construct _ -> - acc2 := Id.Set.union (vars_of_global (Global.env()) c) !acc2 + acc2 := Id.Set.union (vars_of_global (Global.env()) (EConstr.to_constr sigma c)) !acc2 | _ -> - iter_constr_with_full_binders - (fun d (aliases,depth) -> (extend_alias d aliases,depth+1)) + iter_with_full_binders sigma + (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1)) frec (aliases,depth) c in frec (aliases,0) c; @@ -407,11 +420,11 @@ let free_vars_and_rels_up_alias_expansion aliases c = (* Managing pattern-unification *) (********************************) -let rec expand_and_check_vars aliases = function +let rec expand_and_check_vars sigma aliases = function | [] -> [] - | a::l when isRel a || isVar a -> - let a = expansion_of_var aliases a in - if isRel a || isVar a then a :: expand_and_check_vars aliases l + | a::l when EConstr.isRel sigma a || EConstr.isVar sigma a -> + let a = expansion_of_var sigma aliases a in + if EConstr.isRel sigma a || EConstr.isVar sigma a then a :: expand_and_check_vars sigma aliases l else raise Exit | _ -> raise Exit @@ -422,24 +435,25 @@ module Constrhash = Hashtbl.Make let hash = hash_constr end) -let constr_list_distinct l = +let constr_list_distinct sigma l = let visited = Constrhash.create 23 in let rec loop = function | h::t -> + let h = EConstr.to_constr sigma h in if Constrhash.mem visited h then false else (Constrhash.add visited h h; loop t) | [] -> true in loop l let get_actual_deps evd aliases l t = - if occur_meta_or_existential evd (EConstr.of_constr t) then + if occur_meta_or_existential evd t then (* Probably no restrictions on allowed vars in presence of evars *) l else (* Probably strong restrictions coming from t being evar-closed *) - let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion aliases t in + let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion evd aliases t in List.filter (fun c -> - match kind_of_term c with + match EConstr.kind evd c with | Var id -> Id.Set.mem id fv_ids | Rel n -> Int.Set.mem n fv_rels | _ -> assert false) l @@ -462,10 +476,11 @@ let remove_instance_local_defs evd evk args = (* Check if an applied evar "?X[args] l" is a Miller's pattern *) let find_unification_pattern_args env evd l t = - if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then - let aliases = make_alias_map env in - match (try Some (expand_and_check_vars aliases l) with Exit -> None) with - | Some l as x when constr_list_distinct (get_actual_deps evd aliases l t) -> x + let open EConstr in + if List.for_all (fun x -> isRel evd x || isVar evd x) l (* common failure case *) then + let aliases = make_alias_map env evd in + match (try Some (expand_and_check_vars evd aliases l) with Exit -> None) with + | Some l as x when constr_list_distinct evd (get_actual_deps evd aliases l t) -> x | _ -> None else None @@ -473,15 +488,17 @@ let find_unification_pattern_args env evd l t = let is_unification_pattern_meta env evd nb m l t = (* Variables from context and rels > nb are implicitly all there *) (* so we need to be a rel <= nb *) - if List.for_all (fun x -> isRel x && destRel x <= nb) l then + let open EConstr in + if List.for_all (fun x -> isRel evd x && destRel evd x <= nb) l then match find_unification_pattern_args env evd l t with - | Some _ as x when not (dependent evd (EConstr.mkMeta m) (EConstr.of_constr t)) -> x + | Some _ as x when not (dependent evd (EConstr.mkMeta m) t) -> x | _ -> None else None let is_unification_pattern_evar env evd (evk,args) l t = - if List.for_all (fun x -> isRel x || isVar x) l + let open EConstr in + if List.for_all (fun x -> isRel evd x || isVar evd x) l && noccur_evar env evd evk t then let args = remove_instance_local_defs evd evk args in @@ -498,7 +515,7 @@ let is_unification_pattern_pure_evar env evd (evk,args) t = | Some _ -> true let is_unification_pattern (env,nb) evd f l t = - match kind_of_term f with + match EConstr.kind evd f with | Meta m -> is_unification_pattern_meta env evd nb m l t | Evar ev -> is_unification_pattern_evar env evd ev l t | _ -> None @@ -511,21 +528,23 @@ let is_unification_pattern (env,nb) evd f l t = dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *) let solve_pattern_eqn env sigma l c = + let open EConstr in let c' = List.fold_right (fun a c -> - let c' = subst_term sigma (EConstr.of_constr (lift 1 a)) (EConstr.of_constr (lift 1 c)) in - match kind_of_term a with + let c' = subst_term sigma (Vars.lift 1 a) (Vars.lift 1 c) in + match EConstr.kind sigma a with (* Rem: if [a] links to a let-in, do as if it were an assumption *) | Rel n -> let open Context.Rel.Declaration in let d = map_constr (lift n) (lookup_rel n env) in + let c' = EConstr.of_constr c' in mkLambda_or_LetIn d c' | Var id -> - let d = lookup_named id env in mkNamedLambda_or_LetIn d c' + let d = lookup_named id env in EConstr.of_constr (mkNamedLambda_or_LetIn d c') | _ -> assert false) l c in (* Warning: we may miss some opportunity to eta-reduce more since c' is not in normal form *) - shrink_eta (EConstr.of_constr c') + shrink_eta c' (*****************************************) (* Refining/solving unification problems *) @@ -543,35 +562,33 @@ let solve_pattern_eqn env sigma l c = let make_projectable_subst aliases sigma evi args = let sign = evar_filtered_context evi in - let evar_aliases = compute_var_aliases sign in + let evar_aliases = compute_var_aliases sign sigma in let (_,full_subst,cstr_subst) = List.fold_right (fun decl (args,all,cstrs) -> match decl,args with | LocalAssum (id,c), a::rest -> - let a = whd_evar sigma a in let cstrs = - let a',args = decompose_app_vect sigma (EConstr.of_constr a) in - match kind_of_term a' with + let a',args = decompose_app_vect sigma a in + match EConstr.kind sigma (EConstr.of_constr a') with | Construct cstr -> let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in Constrmap.add (fst cstr) ((args,id)::l) cstrs | _ -> cstrs in - (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs) + (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs) | LocalDef (id,c,_), a::rest -> - let a = whd_evar sigma a in - (match kind_of_term c with + (match EConstr.kind sigma (EConstr.of_constr c) with | Var id' -> - let idc = normalize_alias_var evar_aliases id' in + let idc = normalize_alias_var sigma evar_aliases id' in let sub = try Id.Map.find idc all with Not_found -> [] in - if List.exists (fun (c,_,_) -> Term.eq_constr a c) sub then + if List.exists (fun (c,_,_) -> EConstr.eq_constr sigma a c) sub then (rest,all,cstrs) else (rest, - Id.Map.add idc ((a,normalize_alias_opt aliases a,id)::sub) all, + Id.Map.add idc ((a,normalize_alias_opt sigma aliases a,id)::sub) all, cstrs) | _ -> - (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs)) + (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs)) | _ -> anomaly (Pp.str "Instance does not match its signature")) sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in (full_subst,cstr_subst) @@ -587,15 +604,18 @@ let make_projectable_subst aliases sigma evi args = *) let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env = + let open EConstr in let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in + let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src (List.map EConstr.Unsafe.to_constr inst_in_env) in let evd = Sigma.to_evar_map evd in - let t_in_env = whd_evar evd t_in_env in - let evd = define_fun env evd None (destEvar evar_in_env) t_in_env in + let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in + let evar_in_env = EConstr.of_constr evar_in_env in + let (evk, _) = destEvar evd evar_in_env in + let evd = define_fun env evd None (EConstr.destEvar evd evar_in_env) t_in_env in let ctxt = named_context_of_val sign in let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in - let evar_in_sign = mkEvar (fst (destEvar evar_in_env), inst_in_sign) in - (evd,whd_evar evd evar_in_sign) + let evar_in_sign = mkEvar (evk, inst_in_sign) in + (evd,whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign)) (* We have x1..xq |- ?e1 : τ and had to solve something like * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some @@ -617,10 +637,11 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si exception MorePreciseOccurCheckNeeeded let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = + let open EConstr in if Evd.is_defined evd evk1 then (* Some circularity somewhere (see e.g. #3209) *) raise MorePreciseOccurCheckNeeeded; - let (evk1,args1) = destEvar (whd_evar evd (mkEvar (evk1,args1))) in + let (evk1,args1) = EConstr.destEvar evd (EConstr.mkEvar (evk1,args1)) in let evi1 = Evd.find_undefined evd evk1 in let env1,rel_sign = env_rel_context_chop k env in let sign1 = evar_hyps evi1 in @@ -634,36 +655,38 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in let id = next_name_away na avoid in let evd,t_in_sign = - let s = Retyping.get_sort_of env evd (EConstr.of_constr t_in_env) in + let t_in_env = EConstr.of_constr t_in_env in + let s = Retyping.get_sort_of env evd t_in_env in let evd,ty_t_in_sign = refresh_universes - ~status:univ_flexible (Some false) env evd (mkSort s) in + ~status:univ_flexible (Some false) env evd (EConstr.mkSort s) in define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env in let evd,d' = match d with | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign) | LocalDef (_,b,_) -> + let b = EConstr.of_constr b in let evd,b = define_evar_from_virtual_equation define_fun env evd src b t_in_sign sign filter inst_in_env in evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in (push_named_context_val d' sign, Filter.extend 1 filter, - (mkRel 1)::(List.map (lift 1) inst_in_env), - (mkRel 1)::(List.map (lift 1) inst_in_sign), + (mkRel 1)::(List.map (Vars.lift 1) inst_in_env), + (mkRel 1)::(List.map (Vars.lift 1) inst_in_sign), push_rel d env,evd,id::avoid)) rel_sign (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1) in let evd,ev2ty_in_sign = - let s = Retyping.get_sort_of env evd (EConstr.of_constr ty_in_env) in + let s = Retyping.get_sort_of env evd ty_in_env in let evd,ty_t_in_sign = refresh_universes - ~status:univ_flexible (Some false) env evd (mkSort s) in + ~status:univ_flexible (Some false) env evd (EConstr.mkSort s) in define_evar_from_virtual_equation define_fun env evd src ty_in_env ty_t_in_sign sign2 filter2 inst2_in_env in let evd = Sigma.Unsafe.of_evar_map evd in let Sigma (ev2_in_sign, evd, _) = - new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in + new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src (List.map EConstr.Unsafe.to_constr inst2_in_sign) in let evd = Sigma.to_evar_map evd in - let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in - (evd, ev2_in_sign, ev2_in_env) + let ev2_in_env = (fst (destEvar evd (EConstr.of_constr ev2_in_sign)), Array.of_list inst2_in_env) in + (evd, EConstr.of_constr ev2_in_sign, ev2_in_env) let restrict_upon_filter evd evk p args = let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in @@ -722,7 +745,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst = type evar_projection = | ProjectVar -| ProjectEvar of existential * evar_info * Id.t * evar_projection +| ProjectEvar of EConstr.existential * evar_info * Id.t * evar_projection exception NotUnique exception NotUniqueInType of (Id.t * evar_projection) list @@ -730,19 +753,19 @@ exception NotUniqueInType of (Id.t * evar_projection) list let rec assoc_up_to_alias sigma aliases y yc = function | [] -> raise Not_found | (c,cc,id)::l -> - let c' = whd_evar sigma c in - if Term.eq_constr y c' then id + if EConstr.eq_constr sigma y c then id else match l with | _ :: _ -> assoc_up_to_alias sigma aliases y yc l | [] -> (* Last chance, we reason up to alias conversion *) - match (if c == c' then cc else normalize_alias_opt aliases c') with - | Some cc when Term.eq_constr yc cc -> id - | _ -> if Term.eq_constr yc c then id else raise Not_found + match (normalize_alias_opt sigma aliases c) with + | Some cc when EConstr.eq_constr sigma yc cc -> id + | _ -> if EConstr.eq_constr sigma yc c then id else raise Not_found let rec find_projectable_vars with_evars aliases sigma y subst = - let yc = normalize_alias aliases y in + let open EConstr in + let yc = normalize_alias sigma aliases y in let is_projectable idc idcl subst' = (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *) try @@ -752,12 +775,12 @@ let rec find_projectable_vars with_evars aliases sigma y subst = (* Then test if [idc] is (indirectly) bound in [subst] to some evar *) (* projectable on [y] *) if with_evars then - let f (c,_,id) = isEvar c && is_undefined sigma (fst (destEvar c)) in + let f (c,_,id) = isEvar sigma c in let idcl' = List.filter f idcl in match idcl' with | [c,_,id] -> begin - let (evk,argsv as t) = destEvar c in + let (evk,argsv as t) = destEvar sigma c in let evi = Evd.find sigma evk in let subst,_ = make_projectable_subst aliases sigma evi argsv in let l = find_projectable_vars with_evars aliases sigma y subst in @@ -805,19 +828,19 @@ let rec find_solution_type evarenv = function let rec do_projection_effects define_fun env ty evd = function | ProjectVar -> evd | ProjectEvar ((evk,argsv),evi,id,p) -> - let evd = Evd.define evk (mkVar id) evd in + let open EConstr in + let evd = Evd.define evk (Constr.mkVar id) evd in (* TODO: simplify constraints involving evk *) let evd = do_projection_effects define_fun env ty evd p in - let ty = whd_all env evd (EConstr.of_constr (Lazy.force ty)) in - if not (isSort ty) then + let ty = EConstr.of_constr (whd_all env evd (Lazy.force ty)) in + if not (isSort evd ty) then (* Don't try to instantiate if a sort because if evar_concl is an evar it may commit to a univ level which is not the right one (however, regarding coercions, because t is obtained by unif, we know that no coercion can be inserted) *) let subst = make_pure_subst evi argsv in - let ty' = replace_vars subst evi.evar_concl in - let ty' = whd_evar evd ty' in - if isEvar ty' then define_fun env evd (Some false) (destEvar ty') ty else evd + let ty' = Vars.replace_vars subst (EConstr.of_constr evi.evar_concl) in + if isEvar evd ty' then define_fun env evd (Some false) (destEvar evd ty') ty else evd else evd @@ -843,7 +866,7 @@ let rec do_projection_effects define_fun env ty evd = function type projectibility_kind = | NoUniqueProjection - | UniqueProjection of constr * evar_projection list + | UniqueProjection of EConstr.constr * evar_projection list type projectibility_status = | CannotInvert @@ -851,16 +874,16 @@ type projectibility_status = let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders = let effects = ref [] in + let open EConstr in let rec aux k t = - let t = whd_evar evd t in - match kind_of_term t with + match EConstr.kind evd t with | Rel i when i>k0+k -> aux' k (mkRel (i-k)) | Var id -> aux' k t - | _ -> map_constr_with_binders succ aux k t + | _ -> map_with_binders evd succ aux k t and aux' k t = - try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders + try EConstr.of_constr (project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders) with Not_found -> - match expand_alias_once aliases t with + match expand_alias_once evd aliases t with | None -> raise Not_found | Some c -> aux k c in try @@ -895,7 +918,7 @@ let extract_unique_projection = function let extract_candidates sols = try UpdateWith - (List.map (function (id,ProjectVar) -> mkVar id | _ -> raise Exit) sols) + (List.map (function (id,ProjectVar) -> EConstr.mkVar id | _ -> raise Exit) sols) with Exit -> NoUpdate @@ -929,12 +952,12 @@ let filter_effective_candidates evd evi filter candidates = | None -> candidates | Some filter -> let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in - List.filter (fun a -> Id.Set.subset (collect_vars evd (EConstr.of_constr a)) ids) candidates + List.filter (fun a -> Id.Set.subset (collect_vars evd a) ids) candidates let filter_candidates evd evk filter candidates_update = let evi = Evd.find_undefined evd evk in let candidates = match candidates_update with - | NoUpdate -> evi.evar_candidates + | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates | UpdateWith c -> Some c in match candidates with @@ -982,17 +1005,18 @@ let restrict_hyps evd evk filter candidates = let typablefilter = closure_of_filter evd evk (Some filter) in (typablefilter,candidates) -exception EvarSolvedWhileRestricting of evar_map * constr +exception EvarSolvedWhileRestricting of evar_map * EConstr.constr let do_restrict_hyps evd (evk,args as ev) filter candidates = + let open EConstr in let filter,candidates = match filter with | None -> None,candidates | Some filter -> restrict_hyps evd evk filter candidates in match candidates,filter with | UpdateWith [], _ -> error "Not solvable." | UpdateWith [nc],_ -> - let evd = Evd.define evk nc evd in - raise (EvarSolvedWhileRestricting (evd,whd_evar evd (mkEvar ev))) + let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in + raise (EvarSolvedWhileRestricting (evd,mkEvar ev)) | NoUpdate, None -> evd,ev | _ -> restrict_applied_evar evd ev filter candidates @@ -1000,6 +1024,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = (* ?e is assumed to have no candidates *) let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = + let open EConstr in let rhs = expand_vars_in_term env evd rhs in let filter = restrict_upon_filter evd evk @@ -1010,8 +1035,8 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = (* that says that the body is hidden. Note that expand_vars_in_term *) (* expands only rels and vars aliases, not rels or vars bound to an *) (* arbitrary complex term *) - (fun a -> not (isRel a || isVar a) - || dependent evd (EConstr.of_constr a) (EConstr.of_constr rhs) || List.exists (fun (id,_) -> isVarId id a) sols) + (fun a -> not (isRel evd a || isVar evd a) + || dependent evd a rhs || List.exists (fun (id,_) -> isVarId evd id a) sols) argsv in let filter = closure_of_filter evd evk filter in let candidates = extract_candidates sols in @@ -1042,6 +1067,9 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = * Note: argument f is the function used to instantiate evars. *) +let instantiate_evar_array evi c args = + EConstr.of_constr (instantiate_evar_array evi (EConstr.Unsafe.to_constr c) (Array.map EConstr.Unsafe.to_constr args)) + let filter_compatible_candidates conv_algo env evd evi args rhs c = let c' = instantiate_evar_array evi c args in match conv_algo env evd Reduction.CONV rhs c' with @@ -1061,6 +1089,8 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) = | _, None -> filter_candidates evd evk1 filter1 NoUpdate | None, Some _ -> raise DoesNotPreserveCandidateRestriction | Some l1, Some l2 -> + let l1 = List.map EConstr.of_constr l1 in + let l2 = List.map EConstr.of_constr l2 in let l1 = filter_effective_candidates evd evi1 filter1 l1 in let l1' = List.filter (fun c1 -> let c1' = instantiate_evar_array evi1 c1 argsv1 in @@ -1075,7 +1105,7 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) = if Int.equal (List.length l1) (List.length l1') then NoUpdate else UpdateWith l1' -exception CannotProject of evar_map * existential +exception CannotProject of evar_map * EConstr.existential (* Assume that FV(?n[x1:=t1..xn:=tn]) belongs to some set U. Can ?n be instantiated by a term u depending essentially on xi such that the @@ -1092,15 +1122,15 @@ exception CannotProject of evar_map * existential *) let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t = - let f,args = decompose_app_vect evd (EConstr.of_constr t) in - match kind_of_term f with + let f,args = decompose_app_vect evd t in + match EConstr.kind evd (EConstr.of_constr f) with | Construct ((ind,_),u) -> let n = Inductiveops.inductive_nparams ind in if n > Array.length args then true (* We don't try to be more clever *) else let params = fst (Array.chop n args) in - Array.for_all (is_constrainable_in false evd k g) params - | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args + Array.for_all (EConstr.of_constr %> is_constrainable_in false evd k g) params + | Ind _ -> Array.for_all (EConstr.of_constr %> is_constrainable_in false evd k g) args | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2 | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) | Var id -> Id.Set.mem id fv_ids @@ -1109,30 +1139,31 @@ let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t = | _ -> (* We don't try to be more clever *) true let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t = - let t' = expansion_of_var aliases t in + let t' = expansion_of_var evd aliases t in if t' != t then (* t is a local definition, we keep it only if appears in the list *) (* of let-in variables effectively occurring on the right-hand side, *) (* which is the only reason to keep it when inverting arguments *) - match kind_of_term t with + match EConstr.kind evd t with | Var id -> Id.Set.mem id let_ids | Rel n -> Int.Set.mem n let_rels | _ -> assert false else (* t is an instance for a proper variable; we filter it along *) (* the free variables allowed to occur *) - match kind_of_term t with + match EConstr.kind evd t with | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels | _ -> (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t -exception EvarSolvedOnTheFly of evar_map * constr +exception EvarSolvedOnTheFly of evar_map * EConstr.constr (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on the common domain of definition *) let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = + let open EConstr in (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *) - let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in + let fvs2 = free_vars_and_rels_up_alias_expansion evd aliases (mkEvar ev2) in let filter1 = restrict_upon_filter evd evk1 (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2) argsv1 in @@ -1161,12 +1192,12 @@ let check_evar_instance evd evk1 body conv_algo = (* FIXME: The body might be ill-typed when this is called from w_merge *) (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = - try Retyping.get_type_of ~lax:true evenv evd (EConstr.of_constr body) + try EConstr.of_constr (Retyping.get_type_of ~lax:true evenv evd body) with Retyping.RetypeError _ -> error "Ill-typed evar instance" in - match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with + match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with | Success evd -> evd - | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl)) + | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,EConstr.of_constr evi.evar_concl)) let update_evar_source ev1 ev2 evd = let loc, evs2 = evar_source ev2 evd in @@ -1178,9 +1209,10 @@ let update_evar_source ev1 ev2 evd = let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = try + let open EConstr in let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in - let evd' = Evd.define evk2 body evd in - let evd' = update_evar_source (fst (destEvar body)) evk2 evd' in + let evd' = Evd.define evk2 (EConstr.Unsafe.to_constr body) evd in + let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> f env evd pbty ev2 c @@ -1197,7 +1229,8 @@ let preferred_orientation evd evk1 evk2 = | _ -> true let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = - let aliases = make_alias_map env in + let open EConstr in + let aliases = make_alias_map env evd in if preferred_orientation evd evk1 evk2 then try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 with CannotProject (evd,ev2) -> @@ -1244,10 +1277,10 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar solve_evar_evar_aux force f g env evd pbty ev1 ev2 type conv_fun = - env -> evar_map -> conv_pb -> constr -> constr -> unification_result + env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> unification_result type conv_fun_bool = - env -> evar_map -> conv_pb -> constr -> constr -> bool + env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> bool (* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint * definitions. We try to unify the ti with the ui pairwise. The pairs @@ -1255,8 +1288,9 @@ type conv_fun_bool = * depend on these args). *) let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 = + let open EConstr in let evdref = ref evd in - if Array.equal (e_eq_constr_univs evdref) argsv1 argsv2 then !evdref else + if Array.equal (fun c1 c2 -> e_eq_constr_univs evdref (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) ) argsv1 argsv2 then !evdref else (* Filter and restrict if needed *) let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in let untypedfilter = @@ -1288,14 +1322,14 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = | Some l -> let l' = List.map_filter - (filter_compatible_candidates conv_algo env evd evi argsv rhs) l in + (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs (EConstr.of_constr c)) l in match l' with | [] -> raise IncompatibleCandidates | [c,evd] -> (* solve_candidates might have been called recursively in the mean *) (* time and the evar been solved by the filtering process *) if Evd.is_undefined evd evk then - let evd' = Evd.define evk c evd in + let evd' = Evd.define evk (EConstr.Unsafe.to_constr c) evd in check_evar_instance evd' evk c conv_algo else evd | l when List.length l < List.length l' -> @@ -1304,7 +1338,9 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = | l -> evd let occur_evar_upto_types sigma n c = + let c = EConstr.Unsafe.to_constr c in let seen = ref Evar.Set.empty in + (** FIXME: Is that supposed to be evar-insensitive? *) let rec occur_rec c = match kind_of_term c with | Evar (sp,_) when Evar.equal sp n -> raise Occur | Evar (sp,args as e) -> @@ -1341,14 +1377,15 @@ let occur_evar_upto_types sigma n c = * Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn) *) -exception NotInvertibleUsingOurAlgorithm of constr +exception NotInvertibleUsingOurAlgorithm of EConstr.constr exception NotEnoughInformationToProgress of (Id.t * evar_projection) list -exception NotEnoughInformationEvarEvar of constr -exception OccurCheckIn of evar_map * constr +exception NotEnoughInformationEvarEvar of EConstr.constr +exception OccurCheckIn of evar_map * EConstr.constr exception MetaOccurInBodyInternal let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = - let aliases = make_alias_map env in + let open EConstr in + let aliases = make_alias_map env evd in let evdref = ref evd in let progress = ref false in let evi = Evd.find evd evk in @@ -1365,7 +1402,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | (id,p)::_::_ -> if choose then (mkVar id, p) else raise (NotUniqueInType sols) in - let ty = lazy (Retyping.get_type_of env !evdref (EConstr.of_constr t)) in + let ty = lazy (EConstr.of_constr (Retyping.get_type_of env !evdref t)) in let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in evdref := evd; c @@ -1377,18 +1414,18 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = (* No unique projection but still restrict to where it is possible *) (* materializing is necessary, but is restricting useful? *) let ty = find_solution_type (evar_filtered_env evi) sols in - let ty' = instantiate_evar_array evi ty argsv in + let ty' = instantiate_evar_array evi (EConstr.of_constr ty) argsv in let (evd,evar,(evk',argsv' as ev')) = materialize_evar (evar_define conv_algo ~choose) env !evdref 0 ev ty' in - let ts = expansions_of_var aliases t in - let test c = isEvar c || List.mem_f Constr.equal c ts in + let ts = expansions_of_var evd aliases t in + let test c = isEvar evd c || List.mem_f (EConstr.eq_constr evd) c ts in let filter = restrict_upon_filter evd evk test argsv' in let filter = closure_of_filter evd evk' filter in let candidates = extract_candidates sols in let evd = match candidates with | NoUpdate -> let evd, ev'' = restrict_applied_evar evd ev' filter NoUpdate in - Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev'',t) evd + add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',t) evd | UpdateWith _ -> restrict_evar evd evk' filter candidates in @@ -1396,29 +1433,28 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = evar in let rec imitate (env',k as envk) t = - let t = whd_evar !evdref t in - match kind_of_term t with + match EConstr.kind !evdref t with | Rel i when i>k -> let open Context.Rel.Declaration in (match Environ.lookup_rel (i-k) env' with | LocalAssum _ -> project_variable (mkRel (i-k)) | LocalDef (_,b,_) -> try project_variable (mkRel (i-k)) - with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i b)) + with NotInvertibleUsingOurAlgorithm _ -> imitate envk (Vars.lift i (EConstr.of_constr b))) | Var id -> (match Environ.lookup_named id env' with | LocalAssum _ -> project_variable t | LocalDef (_,b,_) -> try project_variable t - with NotInvertibleUsingOurAlgorithm _ -> imitate envk b) + with NotInvertibleUsingOurAlgorithm _ -> imitate envk (EConstr.of_constr b)) | LetIn (na,b,u,c) -> - imitate envk (subst1 b c) + imitate envk (Vars.subst1 b c) | Evar (evk',args' as ev') -> if Evar.equal evk evk' then raise (OccurCheckIn (evd,rhs)); (* Evar/Evar problem (but left evar is virtual) *) let aliases = lift_aliases k aliases in (try - let ev = (evk,Array.map (lift k) argsv) in + let ev = (evk,Array.map (Vars.lift k) argsv) in let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in evdref := evd; body @@ -1428,7 +1464,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = if not !progress then raise (NotEnoughInformationEvarEvar t); (* Make the virtual left evar real *) - let ty = get_type_of env' evd (EConstr.of_constr t) in + let ty = EConstr.of_constr (get_type_of env' evd t) in let (evd,evar'',ev'') = materialize_evar (evar_define conv_algo ~choose) env' evd k ev ty in (* materialize_evar may instantiate ev' by another evar; adjust it *) @@ -1437,7 +1473,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = (* Try to project (a restriction of) the left evar ... *) try let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in - let evd = Evd.define evk' body evd in + let evd = Evd.define evk' (EConstr.Unsafe.to_constr body) evd in check_evar_instance evd evk' body conv_algo with | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *) @@ -1449,9 +1485,9 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | _ -> progress := true; match - let c,args = decompose_app_vect !evdref (EConstr.of_constr t) in - match kind_of_term c with - | Construct (cstr,u) when noccur_between 1 k t -> + let c,args = decompose_app_vect !evdref t in + match EConstr.kind !evdref (EConstr.of_constr c) with + | Construct (cstr,u) when Vars.noccur_between !evdref 1 k t -> (* This is common case when inferring the return clause of match *) (* (currently rudimentary: we do not treat the case of multiple *) (* possible inversions; we do not treat overlap with a possible *) @@ -1462,14 +1498,13 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | _ -> None with | Some l -> - let ty = get_type_of env' !evdref (EConstr.of_constr t) in + let ty = EConstr.of_constr (get_type_of env' !evdref t) in let candidates = try - let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in let t = map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) - self envk (EConstr.of_constr t) in - EConstr.Unsafe.to_constr t::l + imitate envk t in + t::l with e when CErrors.noncritical e -> l in (match candidates with | [x] -> x @@ -1480,11 +1515,10 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = evar'') | None -> (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *) - let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in - EConstr.Unsafe.to_constr (map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) - self envk (EConstr.of_constr t)) + map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) + imitate envk t in - let rhs = whd_beta evd (EConstr.of_constr rhs) (* heuristic *) in + let rhs = EConstr.of_constr (whd_beta evd rhs) (* heuristic *) in let fast rhs = let filter_ctxt = evar_filtered_context evi in let names = ref Idset.empty in @@ -1493,16 +1527,16 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | (decl :: ctxt'), (c :: s') -> let id = get_id decl in names := Idset.add id !names; - isVarId id c && is_id_subst ctxt' s' + isVarId evd id c && is_id_subst ctxt' s' | [], [] -> true | _ -> false in is_id_subst filter_ctxt (Array.to_list argsv) && - closed0 rhs && - Idset.subset (collect_vars evd (EConstr.of_constr rhs)) !names + Vars.closed0 evd rhs && + Idset.subset (collect_vars evd rhs) !names in let body = - if fast rhs then nf_evar evd rhs + if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *) else let t' = imitate (env,0) rhs in if !progress then @@ -1518,7 +1552,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = *) and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = - match kind_of_term rhs with + match EConstr.kind evd rhs with | Evar (evk2,argsv2 as ev2) -> if Evar.equal evk evk2 then solve_refl ~can_drop:choose @@ -1531,7 +1565,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = with NoCandidates -> try let (evd',body) = invert_definition conv_algo choose env evd pbty ev rhs in - if occur_meta evd' (EConstr.of_constr body) then raise MetaOccurInBodyInternal; + if occur_meta evd' body then raise MetaOccurInBodyInternal; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body)); @@ -1553,23 +1587,23 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = str "----> " ++ int ev ++ str " := " ++ print_constr body); raise e in*) - let evd' = check_evar_instance evd' evk body conv_algo in + let evd' = check_evar_instance evd' evk (EConstr.of_constr body) conv_algo in Evd.define evk body evd' with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd pbty ev sols rhs | NotEnoughInformationEvarEvar t -> - add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd + add_conv_oriented_pb (pbty,env,EConstr.mkEvar ev,t) evd | MorePreciseOccurCheckNeeeded -> - add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd + add_conv_oriented_pb (pbty,env,EConstr.mkEvar ev,rhs) evd | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e -> raise e | OccurCheckIn (evd,rhs) -> (* last chance: rhs actually reduces to ev *) - let c = whd_all env evd (EConstr.of_constr rhs) in - match kind_of_term c with + let c = EConstr.of_constr (whd_all env evd rhs) in + match EConstr.kind evd c with | Evar (evk',argsv2) when Evar.equal evk evk' -> - solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma (EConstr.of_constr c) (EConstr.of_constr c')) + solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c') env evd pbty evk argsv argsv2 | _ -> raise (OccurCheckIn (evd,rhs)) @@ -1610,7 +1644,7 @@ let reconsider_conv_pbs conv_algo evd = (fun p (pbty,env,t1,t2 as x) -> match p with | Success evd -> - (match conv_algo env evd pbty t1 t2 with + (match conv_algo env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) with | Success _ as x -> x | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e))) | UnifFailure _ as x -> x) @@ -1624,8 +1658,9 @@ let reconsider_conv_pbs conv_algo evd = (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) = + let open EConstr in try - let t2 = whd_betaiota evd t2 in (* includes whd_evar *) + let t2 = EConstr.of_constr (whd_betaiota evd t2) in (* includes whd_evar *) let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in reconsider_conv_pbs conv_algo evd with @@ -1638,5 +1673,5 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) | IllTypedInstance (env,t,u) -> UnifFailure (evd,InstanceNotSameType (evk1,env,t,u)) | IncompatibleCandidates -> - UnifFailure (evd,ConversionFailed (env,mkEvar ev1, EConstr.Unsafe.to_constr t2)) + UnifFailure (evd,ConversionFailed (env,mkEvar ev1,t2)) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index ac082d1bf..23cb245e0 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -7,6 +7,7 @@ (************************************************************************) open Term +open EConstr open Evd open Environ @@ -41,7 +42,7 @@ val refresh_universes : (* Also refresh Prop and Set universes, so that the returned type can be any supertype of the original type *) bool option (* direction: true for levels lower than the existing levels *) -> - env -> evar_map -> types -> evar_map * types + env -> evar_map -> types -> evar_map * Constr.types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> bool option -> existential_key -> constr array -> constr array -> evar_map @@ -52,7 +53,7 @@ val solve_evar_evar : ?force:bool -> env -> evar_map -> bool option -> existential -> existential -> evar_map val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> - bool option * existential * EConstr.t -> unification_result + bool option * existential * constr -> unification_result val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result @@ -62,7 +63,7 @@ val is_unification_pattern_evar : env -> evar_map -> existential -> constr list val is_unification_pattern : env * int -> evar_map -> constr -> constr list -> constr -> constr list option -val solve_pattern_eqn : env -> evar_map -> constr list -> constr -> constr +val solve_pattern_eqn : env -> evar_map -> constr list -> constr -> Constr.t val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool @@ -73,7 +74,7 @@ val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun -> evar_map val remove_instance_local_defs : - evar_map -> existential_key -> constr array -> constr list + evar_map -> existential_key -> 'a array -> 'a list val get_type_of_refresh : - ?polyprop:bool -> ?lax:bool -> env -> evar_map -> EConstr.constr -> evar_map * types + ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * Constr.types diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index f28fb84ba..c14d81505 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -13,14 +13,14 @@ open Environ open Type_errors type unification_error = - | OccurCheck of existential_key * constr - | NotClean of existential * env * constr (* Constr is a variable not in scope *) + | OccurCheck of existential_key * EConstr.constr + | NotClean of EConstr.existential * env * EConstr.constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * constr * constr (* Non convertible closed terms *) + | ConversionFailed of env * EConstr.constr * EConstr.constr (* Non convertible closed terms *) | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * types * types + | InstanceNotSameType of existential_key * env * EConstr.types * EConstr.types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 8a6d8b6b3..217deda4d 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -14,14 +14,14 @@ open Type_errors (** {6 The type of errors raised by the pretyper } *) type unification_error = - | OccurCheck of existential_key * constr - | NotClean of existential * env * constr + | OccurCheck of existential_key * EConstr.constr + | NotClean of EConstr.existential * env * EConstr.constr | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * constr * constr + | ConversionFailed of env * EConstr.constr * EConstr.constr | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * types * types + | InstanceNotSameType of existential_key * env * EConstr.types * EConstr.types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b689bb7c7..fbba682fc 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -756,7 +756,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre refreshed right away. *) let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in - let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in + let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref (EConstr.of_constr c) in let t = Retyping.get_type_of env.ExtraEnv.env !evdref (EConstr.of_constr c) in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj @@ -820,7 +820,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let t = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) - evdref j.uj_type in + evdref (EConstr.of_constr j.uj_type) in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) @@ -1003,7 +1003,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let tj = pretype_type empty_valcon env evdref lvar t in let tval = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) - evdref tj.utj_val in + evdref (EConstr.of_constr tj.utj_val) in let tval = nf_evar !evdref tval in let cj, tval = match k with | VMcast -> @@ -1014,7 +1014,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre if b then (evdref := evd; cj, tval) else error_actual_type ~loc env.ExtraEnv.env !evdref cj tval - (ConversionFailed (env.ExtraEnv.env,cty,tval)) + (ConversionFailed (env.ExtraEnv.env,EConstr.of_constr cty,EConstr.of_constr tval)) else user_err ~loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> @@ -1025,7 +1025,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre if b then (evdref := evd; cj, tval) else error_actual_type ~loc env.ExtraEnv.env !evdref cj tval - (ConversionFailed (env.ExtraEnv.env,cty,tval)) + (ConversionFailed (env.ExtraEnv.env,EConstr.of_constr cty,EConstr.of_constr tval)) end | _ -> pretype (mk_tycon (EConstr.of_constr tval)) env evdref lvar c, tval diff --git a/pretyping/typing.ml b/pretyping/typing.ml index db31541cd..1dcb5f945 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -309,7 +309,7 @@ let type_of ?(refresh=false) env evd c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type + Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type) else !evdref, j.uj_type let e_type_of ?(refresh=false) env evdref c = @@ -317,7 +317,7 @@ let e_type_of ?(refresh=false) env evdref c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in + let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type) in let () = evdref := evd in c else j.uj_type diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f282ec4f1..b8c9a93db 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -183,7 +183,7 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) = extra assumptions added by unification to the context *) let env' = pop_rel_context nb env in let sigma,c = pose_all_metas_as_evars env' sigma c in - let c = solve_pattern_eqn env sigma l c in + let c = solve_pattern_eqn env sigma (List.map EConstr.of_constr l) (EConstr.of_constr c) in let pb = (Conv,TypeNotProcessed) in if noccur_between 1 nb c then sigma,(k,lift (-nb) c,pb)::metasubst,evarsubst @@ -191,7 +191,7 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) = | Evar ev -> let env' = pop_rel_context nb env in let sigma,c = pose_all_metas_as_evars env' sigma c in - sigma,metasubst,(env,ev,solve_pattern_eqn env sigma l c)::evarsubst + sigma,metasubst,(env,ev,solve_pattern_eqn env sigma (List.map EConstr.of_constr l) (EConstr.of_constr c))::evarsubst | _ -> assert false let push d (env,n) = (push_rel_assum d env,n+1) @@ -841,7 +841,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb and unify_app_pattern dir curenvnb pb opt substn cM f1 l1 cN f2 l2 = let f, l, t = if dir then f1, l1, cN else f2, l2, cM in - match is_unification_pattern curenvnb sigma f (Array.to_list l) t with + match is_unification_pattern curenvnb sigma (EConstr.of_constr f) (Array.map_to_list EConstr.of_constr l) (EConstr.of_constr t) with | None -> (match kind_of_term t with | App (f',l') -> @@ -850,7 +850,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | Proj _ -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 | _ -> unify_not_same_head curenvnb pb opt substn cM cN) | Some l -> - solve_pattern_eqn_array curenvnb f l t substn + solve_pattern_eqn_array curenvnb f (List.map EConstr.Unsafe.to_constr l) t substn and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 = try @@ -1246,7 +1246,7 @@ let w_coerce env evd mv c = w_coerce_to_type env evd c cty mvty let unify_to_type env sigma flags c status u = - let sigma, c = refresh_universes (Some false) env sigma c in + let sigma, c = refresh_universes (Some false) env sigma (EConstr.of_constr c) in let t = get_type_of env sigma (EConstr.of_constr (nf_meta sigma c)) in let t = nf_betaiota sigma (EConstr.of_constr (nf_meta sigma t)) in unify_0 env sigma CUMUL flags t u @@ -1271,10 +1271,13 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) +let to_conv_fun f = (); fun env sigma pb c1 c2 -> + f env sigma pb (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) + let solve_simple_evar_eqn ts env evd ev rhs = - match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,EConstr.of_constr rhs) with + match solve_simple_eqn (to_conv_fun (Evarconv.evar_conv_x ts)) env evd (None,ev,EConstr.of_constr rhs) with | UnifFailure (evd,reason) -> - error_cannot_unify env evd ~reason (mkEvar ev,rhs); + error_cannot_unify env evd ~reason (EConstr.Unsafe.to_constr (EConstr.mkEvar ev),rhs); | Success evd -> Evarconv.consider_remaining_unif_problems env evd @@ -1308,14 +1311,14 @@ let w_merge env with_types flags (evd,metas,evars) = else let evd' = let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in - try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'' + try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' (fst ev, Array.map EConstr.of_constr (snd ev)) rhs'' with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev,rhs'') in w_merge_rec evd' metas evars' eqns | _ -> let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in let evd' = - try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'' + try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' (fst ev, Array.map EConstr.of_constr (snd ev)) rhs'' with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev, rhs'') in w_merge_rec evd' metas evars' eqns diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 22d01e401..1c10cdfea 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -788,7 +788,7 @@ let check_types env sigma mayneedglobalcheck deep newc origc = if deep then begin let t2 = Retyping.get_type_of env sigma (EConstr.of_constr origc) in let sigma, t2 = Evarsolve.refresh_universes - ~onlyalg:true (Some false) env sigma t2 in + ~onlyalg:true (Some false) env sigma (EConstr.of_constr t2) in let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in if not b then if @@ -2604,7 +2604,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let Sigma (t, sigma, p) = match ty with | Some t -> Sigma.here t sigma | None -> - let t = typ_of env sigma (EConstr.of_constr c) in + let t = EConstr.of_constr (typ_of env sigma (EConstr.of_constr c)) in let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in Sigma.Unsafe.of_pair (c, sigma) in @@ -3621,7 +3621,7 @@ let abstract_args gl generalize_vars dep id defined f args = RelDecl.get_name decl, RelDecl.get_type decl, c in let argty = Tacmach.pf_unsafe_type_of gl arg in - let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in + let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma (EConstr.of_constr ty) in let () = sigma := sigma' in let lenctx = List.length ctx in let liftargty = lift lenctx argty in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index c09bf59ce..b480fcd86 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -60,13 +60,19 @@ let contract1_vect env a v = | _ -> assert false let rec contract3' env a b c = function - | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d) + | OccurCheck (evk,d) -> + let d = EConstr.Unsafe.to_constr d in + let x,d = contract4 env a b c d in x,OccurCheck(evk, EConstr.of_constr d) | NotClean ((evk,args),env',d) -> + let d = EConstr.Unsafe.to_constr d in + let args = Array.map EConstr.Unsafe.to_constr args in let env',d,args = contract1_vect env' d args in - contract3 env a b c,NotClean((evk,args),env',d) + contract3 env a b c,NotClean((evk,Array.map EConstr.of_constr args),env',EConstr.of_constr d) | ConversionFailed (env',t1,t2) -> + let t1 = EConstr.Unsafe.to_constr t1 in + let t2 = EConstr.Unsafe.to_constr t2 in let (env',t1,t2) = contract2 env' t1 t2 in - contract3 env a b c, ConversionFailed (env',t1,t2) + contract3 env a b c, ConversionFailed (env',EConstr.of_constr t1,EConstr.of_constr t2) | NotSameArgSize | NotSameHead | NoCanonicalStructure | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities | UnifUnivInconsistency _ as x -> contract3 env a b c, x @@ -277,13 +283,13 @@ let explain_unification_error env sigma p1 p2 = function | Some e -> let rec aux p1 p2 = function | OccurCheck (evk,rhs) -> - let rhs = Evarutil.nf_evar sigma rhs in + let rhs = EConstr.to_constr sigma rhs in [str "cannot define " ++ quote (pr_existential_key sigma evk) ++ strbrk " with term " ++ pr_lconstr_env env sigma rhs ++ strbrk " that would depend on itself"] | NotClean ((evk,args),env,c) -> - let c = Evarutil.nf_evar sigma c in - let args = Array.map (Evarutil.nf_evar sigma) args in + let c = EConstr.to_constr sigma c in + let args = Array.map (EConstr.to_constr sigma) args in [str "cannot instantiate " ++ quote (pr_existential_key sigma evk) ++ strbrk " because " ++ pr_lconstr_env env sigma c ++ strbrk " is not in its scope" ++ @@ -293,6 +299,8 @@ let explain_unification_error env sigma p1 p2 = function | NotSameArgSize | NotSameHead | NoCanonicalStructure -> (* Error speaks from itself *) [] | ConversionFailed (env,t1,t2) -> + let t1 = EConstr.to_constr sigma t1 in + let t2 = EConstr.to_constr sigma t2 in if Term.eq_constr t1 p1 && Term.eq_constr t2 p2 then [] else let env = make_all_name_different env in let t1 = Evarutil.nf_evar sigma t1 in @@ -306,6 +314,8 @@ let explain_unification_error env sigma p1 p2 = function strbrk " refers to a metavariable - please report your example" ++ strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."] | InstanceNotSameType (evk,env,t,u) -> + let t = EConstr.to_constr sigma t in + let u = EConstr.to_constr sigma u in let t, u = pr_explicit env sigma t u in [str "unable to find a well-typed instantiation for " ++ quote (pr_existential_key sigma evk) ++ |