diff options
| -rw-r--r-- | engine/termops.ml | 27 | ||||
| -rw-r--r-- | engine/termops.mli | 6 | ||||
| -rw-r--r-- | ltac/rewrite.ml | 11 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 2 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 3 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 10 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 2 | ||||
| -rw-r--r-- | pretyping/find_subterm.ml | 2 | ||||
| -rw-r--r-- | pretyping/find_subterm.mli | 2 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 16 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 30 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 504 | ||||
| -rw-r--r-- | pretyping/unification.mli | 32 | ||||
| -rw-r--r-- | proofs/clenv.ml | 8 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 2 | ||||
| -rw-r--r-- | proofs/refine.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/inv.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 29 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 23 |
28 files changed, 427 insertions, 312 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 16e2c04c8..c1198e05a 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -164,9 +164,19 @@ let rel_list n m = in reln [] 1 +let local_assum (na, t) = + let open RelDecl in + let inj = EConstr.Unsafe.to_constr in + LocalAssum (na, inj t) + +let local_def (na, b, t) = + let open RelDecl in + let inj = EConstr.Unsafe.to_constr in + LocalDef (na, inj b, inj t) + let push_rel_assum (x,t) env = let open RelDecl in - push_rel (LocalAssum (x,t)) env + push_rel (local_assum (x,t)) env let push_rels_assum assums = let open RelDecl in @@ -278,14 +288,15 @@ let adjust_app_list_size f1 l1 f2 l2 = (applist (f1,extras), restl1, f2, l2) let adjust_app_array_size f1 l1 f2 l2 = + let open EConstr in let len1 = Array.length l1 and len2 = Array.length l2 in if Int.equal len1 len2 then (f1,l1,f2,l2) else if len1 < len2 then let extras,restl2 = Array.chop (len2-len1) l2 in - (f1, l1, appvect (f2,extras), restl2) + (f1, l1, mkApp (f2,extras), restl2) else let extras,restl1 = Array.chop (len1-len2) l1 in - (appvect (f1,extras), restl1, f2, l2) + (mkApp (f1,extras), restl1, f2, l2) (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate subterms of [c]; it carries an extra data [l] (typically a name @@ -321,16 +332,6 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with time being almost those of the ML representation (except for (co-)fixpoint) *) -let local_assum (na, t) = - let open RelDecl in - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let open RelDecl in - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - let fold_rec_types g (lna,typarray,_) e = let open EConstr in let ctxt = Array.map2_i (fun i na t -> local_assum (na, Vars.lift i t)) lna typarray in diff --git a/engine/termops.mli b/engine/termops.mli index 2b66c88a7..df3fdd124 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -29,7 +29,7 @@ val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds (** about contexts *) -val push_rel_assum : Name.t * types -> env -> env +val push_rel_assum : Name.t * EConstr.types -> env -> env val push_rels_assum : (Name.t * types) list -> env -> env val push_named_rec_types : Name.t array * types array * 'a -> env -> env @@ -208,8 +208,8 @@ val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array val adjust_app_list_size : constr -> constr list -> constr -> constr list -> (constr * constr list * constr * constr list) -val adjust_app_array_size : constr -> constr array -> constr -> constr array -> - (constr * constr array * constr * constr array) +val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array -> + (EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr array) (** name contexts *) type names_context = Name.t list diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index ccd45756a..4d65b4c69 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -711,7 +711,7 @@ let symmetry env sort rew = let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) by t = try let left = if l2r then c1 else c2 in - let sigma = Unification.w_unify ~flags env sigma CONV left t in + let sigma = Unification.w_unify ~flags env sigma CONV (EConstr.of_constr left) (EConstr.of_constr t) in let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs) ~fail:true env sigma in let evd = solve_remaining_by env sigma holes by in @@ -738,7 +738,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t = basically an eq_constr, except when preexisting evars occur in either the lemma or the goal, in which case the eq_constr also solved this evars *) - let sigma = Unification.w_unify ~flags:rewrite_unif_flags env sigma CONV left t in + let sigma = Unification.w_unify ~flags:rewrite_unif_flags env sigma CONV (EConstr.of_constr left) (EConstr.of_constr t) in let rew_evars = sigma, cstrs in let rew_prf = RewPrf (rel, prf) in let rew = { rew_car = car; rew_from = c1; rew_to = c2; rew_prf; rew_evars; } in @@ -1423,7 +1423,7 @@ module Strategies = error "fold: the term is not unfoldable !" in try - let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in + let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) (EConstr.of_constr unfolded) (EConstr.of_constr t) in let c' = Evarutil.nf_evar sigma c in state, Success { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; @@ -2045,15 +2045,16 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = in the context *) Unification.w_unify_to_subterm ~flags:rewrite_unif_flags - env sigma ((if l2r then c1 else c2),but) + env sigma (EConstr.of_constr (if l2r then c1 else c2),EConstr.of_constr but) with | ex when Pretype_errors.precatchable_exception ex -> (* ~flags:(true,true) to make Ring work (since it really exploits conversion) *) Unification.w_unify_to_subterm ~flags:rewrite_conv_unif_flags - env sigma ((if l2r then c1 else c2),but) + env sigma (EConstr.of_constr (if l2r then c1 else c2),EConstr.of_constr but) in + let c' = EConstr.Unsafe.to_constr c' in let nf c = Evarutil.nf_evar sigma c in let c1 = if l2r then nf c' else nf c1 and c2 = if l2r then nf c2 else nf c' diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 85d4ac06e..d8c933912 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1780,7 +1780,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacLetTac(na,c,clp,b,eqpat)) (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) (let_pat_tac b (interp_name ist env sigma na) - ((sigma,sigma'),c) clp eqpat) sigma') + ((sigma,sigma'),EConstr.of_constr c) clp eqpat) sigma') end } (* Derived basic tactics *) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 5e16d2da0..44cd22c8b 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -408,7 +408,7 @@ let find_subsubgoal c ctyp skip submetas gls = try let unifier = Unification.w_unify env se.se_evd Reduction.CUMUL - ~flags:(Unification.elim_flags ()) ctyp se.se_type in + ~flags:(Unification.elim_flags ()) (EConstr.of_constr ctyp) (EConstr.of_constr se.se_type) in if n <= 0 then {se with se_evd=meta_assign se.se_meta diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 42a8cac69..0c4fa7055 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -99,6 +99,9 @@ let is_info_scheme env t = match flag_of_type env t with | (Info, TypeScheme) -> true | _ -> false +let push_rel_assum (n, t) env = + Environ.push_rel (LocalAssum (n, t)) env + (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 18aeca6fa..308fb414e 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -332,7 +332,7 @@ let flags_FO = (Unification.default_no_delta_unify_flags ()).Unification.resolve_evars } let unif_FO env ise p c = - Unification.w_unify env ise Reduction.CONV ~flags:flags_FO p c + Unification.w_unify env ise Reduction.CONV ~flags:flags_FO (EConstr.of_constr p) (EConstr.of_constr c) (* Perform evar substitution in main term and prune substitution. *) let nf_open_term sigma0 ise c = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 683b33b89..3b420347b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -390,7 +390,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty 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 - (position_problem on_left pbty,ev,EConstr.of_constr t2) + (position_problem on_left pbty,ev,t2) in let consume_stack on_left (termF,skF) (termO,skO) evd = let switch f a b = if on_left then f a b else f b a in @@ -1216,7 +1216,7 @@ let error_cannot_unify env evd pb ?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) | _ -> () let max_undefined_with_candidates evd = @@ -1276,7 +1276,9 @@ let consider_remaining_unif_problems env let rec aux evd pbs progress stuck = match pbs with | (pbty,env,t1,t2 as pb) :: pbs -> - (match apply_conversion_problem_heuristic ts env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) with + 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 begin match rest with @@ -1292,6 +1294,8 @@ let consider_remaining_unif_problems 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 diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 3bcea4cee..b1fc7cbe9 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -147,17 +147,17 @@ let recheck_applications conv_algo env evdref t = | App (f, args) -> let () = aux env f 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 argsty = Array.map (fun x -> aux env x; EConstr.of_constr (Retyping.get_type_of env !evdref x)) args in let rec aux i ty = if i < Array.length argsty then match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref ty)) with | Prod (na, dom, codom) -> - (match conv_algo env !evdref Reduction.CUMUL (EConstr.of_constr argsty.(i)) dom with + (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with | Success evd -> evdref := evd; aux (succ i) (Vars.subst1 args.(i) codom) | UnifFailure (evd, reason) -> - Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), EConstr.Unsafe.to_constr dom)) - | _ -> raise (IllTypedInstance (env, ty, EConstr.of_constr argsty.(i))) + Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom)) + | _ -> raise (IllTypedInstance (env, ty, argsty.(i))) else () in aux 0 (EConstr.of_constr fty) | _ -> diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 23cb245e0..b83147514 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -63,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.t +val solve_pattern_eqn : env -> evar_map -> constr list -> constr -> constr val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 2b243d5b9..15409f2b8 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -85,7 +85,7 @@ let map_named_declaration_with_hyploc f hyploc acc decl = exception SubtermUnificationError of subterm_unification_error -exception NotUnifiable of (Constr.t * Constr.t * unification_error) option +exception NotUnifiable of (EConstr.t * EConstr.t * unification_error) option type 'a testing_function = { match_fun : 'a -> EConstr.constr -> 'a; diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index e7f0da93f..c7db84e3c 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -15,7 +15,7 @@ open Environ (** Finding subterms, possibly up to some unification function, possibly at some given occurrences *) -exception NotUnifiable of (constr * constr * unification_error) option +exception NotUnifiable of (EConstr.constr * EConstr.constr * unification_error) option exception SubtermUnificationError of subterm_unification_error diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index a93f2846b..e30ba21fd 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -504,7 +504,7 @@ let is_predicate_explicitly_dep env sigma pred arsign = let pv' = EConstr.of_constr (whd_all env sigma pval) in match EConstr.kind sigma pv', arsign with | Lambda (na,t,b), (LocalAssum _)::arsign -> - srec (push_rel_assum (na, EConstr.Unsafe.to_constr t) env) b arsign + srec (push_rel_assum (na, t) env) b arsign | Lambda (na,_,t), _ -> (* The following code has an impact on the introduction names diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index c14d81505..14b25ab36 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -29,7 +29,7 @@ type position = (Id.t * Locus.hyp_location_flag) option type position_reporting = (position * int) * EConstr.t -type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option +type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option type pretype_error = (* Old Case *) @@ -37,17 +37,17 @@ type pretype_error = (* Type inference unification *) | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (* Tactic unification *) - | UnifOccurCheck of existential_key * constr + | UnifOccurCheck of existential_key * EConstr.constr | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option - | CannotUnify of constr * constr * unification_error option - | CannotUnifyLocal of constr * constr * constr + | CannotUnify of EConstr.constr * EConstr.constr * unification_error option + | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr - | NoOccurrenceFound of constr * Id.t option - | CannotFindWellTypedAbstraction of constr * EConstr.constr list * (env * type_error) option - | WrongAbstractionType of Name.t * constr * types * types + | NoOccurrenceFound of EConstr.constr * Id.t option + | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (env * type_error) option + | WrongAbstractionType of Name.t * EConstr.constr * EConstr.types * EConstr.types | AbstractionOverMeta of Name.t * Name.t - | NonLinearUnification of Name.t * constr + | NonLinearUnification of Name.t * EConstr.constr (* Pretyping *) | VarNotFound of Id.t | UnexpectedType of constr * constr diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 217deda4d..2e707a0ff 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -30,7 +30,7 @@ type position = (Id.t * Locus.hyp_location_flag) option type position_reporting = (position * int) * EConstr.t -type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option +type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option type pretype_error = (** Old Case *) @@ -38,17 +38,17 @@ type pretype_error = (** Type inference unification *) | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (** Tactic Unification *) - | UnifOccurCheck of existential_key * constr + | UnifOccurCheck of existential_key * EConstr.constr | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option - | CannotUnify of constr * constr * unification_error option - | CannotUnifyLocal of constr * constr * constr + | CannotUnify of EConstr.constr * EConstr.constr * unification_error option + | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr - | NoOccurrenceFound of constr * Id.t option - | CannotFindWellTypedAbstraction of constr * EConstr.constr list * (env * type_error) option - | WrongAbstractionType of Name.t * constr * types * types + | NoOccurrenceFound of EConstr.constr * Id.t option + | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (env * type_error) option + | WrongAbstractionType of Name.t * EConstr.constr * EConstr.types * EConstr.types | AbstractionOverMeta of Name.t * Name.t - | NonLinearUnification of Name.t * constr + | NonLinearUnification of Name.t * EConstr.constr (** Pretyping *) | VarNotFound of Id.t | UnexpectedType of constr * constr @@ -94,32 +94,32 @@ val error_ill_typed_rec_body : val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b -val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b +val error_cannot_coerce : env -> Evd.evar_map -> EConstr.constr * EConstr.constr -> 'b (** {6 Implicit arguments synthesis errors } *) -val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b +val error_occur_check : env -> Evd.evar_map -> existential_key -> EConstr.constr -> 'b val error_unsolvable_implicit : ?loc:Loc.t -> env -> Evd.evar_map -> existential_key -> Evd.unsolvability_explanation option -> 'b val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> - ?reason:unification_error -> constr * constr -> 'b + ?reason:unification_error -> EConstr.constr * EConstr.constr -> 'b -val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b +val error_cannot_unify_local : env -> Evd.evar_map -> EConstr.constr * EConstr.constr * EConstr.constr -> 'b val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> - constr -> EConstr.constr list -> (env * type_error) option -> 'b + EConstr.constr -> EConstr.constr list -> (env * type_error) option -> 'b val error_wrong_abstraction_type : env -> Evd.evar_map -> - Name.t -> constr -> types -> types -> 'b + Name.t -> EConstr.constr -> EConstr.types -> EConstr.types -> 'b val error_abstraction_over_meta : env -> Evd.evar_map -> metavariable -> metavariable -> 'b val error_non_linear_unification : env -> Evd.evar_map -> - metavariable -> constr -> 'b + metavariable -> EConstr.constr -> 'b (** {6 Ml Case errors } *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 0b97cd253..510417879 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1203,7 +1203,7 @@ let whd_allnolet env = (* 4. Ad-hoc eta reduction, does not subsitute evars *) -let shrink_eta c = EConstr.Unsafe.to_constr (Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty))) +let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty)) (* 5. Zeta Reduction Functions *) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 5e6a40786..c3b82729d 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -198,7 +198,7 @@ val whd_zeta_stack : local_stack_reduction_function val whd_zeta_state : local_state_reduction_function val whd_zeta : local_reduction_function -val shrink_eta : EConstr.t -> constr +val shrink_eta : EConstr.constr -> EConstr.constr (** Various reduction functions *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 70aa0be6b..c5c19b49b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,13 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +module CVars = Vars + open CErrors open Pp open Util open Names open Term -open Vars open Termops +open EConstr +open Vars open Namegen open Environ open Evd @@ -30,6 +33,13 @@ open Locusops open Find_subterm open Sigma.Notations +type metabinding = (metavariable * EConstr.constr * (instance_constraint * instance_typing_status)) + +type subst0 = + (evar_map * + metabinding list * + (Environ.env * EConstr.existential * EConstr.t) list) + module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -55,41 +65,44 @@ let _ = Goptions.declare_bool_option { } let occur_meta_or_undefined_evar evd c = - let rec occrec c = match kind_of_term c with + let rec occrec c = match EConstr.kind evd c with | Meta _ -> raise Occur - | Evar (ev,args) -> - (match evar_body (Evd.find evd ev) with - | Evar_defined c -> - occrec c; Array.iter occrec args - | Evar_empty -> raise Occur) - | _ -> Constr.iter occrec c + | Evar _ -> raise Occur + | _ -> EConstr.iter evd occrec c in try occrec c; false with Occur | Not_found -> true let occur_meta_evd sigma mv c = let rec occrec c = (* Note: evars are not instantiated by terms with metas *) - let c = whd_evar sigma (whd_meta sigma (EConstr.of_constr c)) in - match kind_of_term c with + let c = whd_meta sigma c in + let c = EConstr.of_constr c in + match EConstr.kind sigma c with | Meta mv' when Int.equal mv mv' -> raise Occur - | _ -> Constr.iter occrec c + | _ -> EConstr.iter sigma occrec c in try occrec c; false with Occur -> true (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *) let abstract_scheme env evd c l lname_typ = + let open EConstr in + let mkLambda_name env (n,a,b) = + mkLambda (named_hd env (EConstr.Unsafe.to_constr a) n, a, b) + in List.fold_left2 (fun (t,evd) (locc,a) decl -> let na = RelDecl.get_name decl in let ta = RelDecl.get_type decl in - let na = match kind_of_term a with Var id -> Name id | _ -> na in + let ta = EConstr.of_constr ta in + let na = match EConstr.kind evd a with Var id -> Name id | _ -> na in (* [occur_meta ta] test removed for support of eelim/ecase but consequences are unclear... if occur_meta ta then error "cannot find a type for the generalisation" else *) - if occur_meta evd (EConstr.of_constr a) then mkLambda_name env (na,ta,t), evd + if occur_meta evd a then mkLambda_name env (na,ta,t), evd else - let t', evd' = Find_subterm.subst_closed_term_occ env evd locc (EConstr.of_constr a) (EConstr.of_constr t) in + let t', evd' = Find_subterm.subst_closed_term_occ env evd locc a t in + let t' = EConstr.of_constr t' in mkLambda_name env (na,ta,t'), evd') (c,evd) (List.rev l) @@ -98,16 +111,17 @@ let abstract_scheme env evd c l lname_typ = (* Precondition: resulting abstraction is expected to be of type [typ] *) let abstract_list_all env evd typ c l = - let ctxt,_ = splay_prod_n env evd (List.length l) (EConstr.of_constr typ) in + let ctxt,_ = splay_prod_n env evd (List.length l) typ in let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in let evd,typp = - try Typing.type_of env evd (EConstr.of_constr p) + try Typing.type_of env evd p with | UserError _ -> - error_cannot_find_well_typed_abstraction env evd p (List.map EConstr.of_constr l) None + error_cannot_find_well_typed_abstraction env evd p l None | Type_errors.TypeError (env',x) -> - error_cannot_find_well_typed_abstraction env evd p (List.map EConstr.of_constr l) (Some (env',x)) in + error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in + let typp = EConstr.of_constr typp in evd,(p,typp) let set_occurrences_of_last_arg args = @@ -123,12 +137,12 @@ let abstract_list_all_with_dependencies env evd typ c l = let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in let evd,b = Evarconv.second_order_matching empty_transparent_state - env evd ev' argoccs (EConstr.of_constr c) in + env evd ev' argoccs c in if b then let p = nf_evar evd ev in evd, p else error_cannot_find_well_typed_abstraction env evd - (nf_evar evd c) l None + c l None (**) @@ -148,51 +162,53 @@ let extract_instance_status = function | CUMUL -> add_type_status (IsSubType, IsSuperType) | CONV -> add_type_status (Conv, Conv) -let rec subst_meta_instances bl c = - match kind_of_term c with +let rec subst_meta_instances sigma bl c = + match EConstr.kind sigma c with | Meta i -> let select (j,_,_) = Int.equal i j in (try pi2 (List.find select bl) with Not_found -> c) - | _ -> Constr.map (subst_meta_instances bl) c + | _ -> EConstr.map sigma (subst_meta_instances sigma bl) c (** [env] should be the context in which the metas live *) let pose_all_metas_as_evars env evd t = let evdref = ref evd in - let rec aux t = match kind_of_term t with + let rec aux t = match EConstr.kind !evdref t with | Meta mv -> (match Evd.meta_opt_fvalue !evdref mv with - | Some ({rebus=c},_) -> c + | Some ({rebus=c},_) -> EConstr.of_constr c | None -> let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in + let ty = EConstr.of_constr ty in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in let src = Evd.evar_source_of_meta mv !evdref in - let ty = EConstr.of_constr ty in let ev = Evarutil.e_new_evar env evdref ~src ty in evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; - ev) + EConstr.of_constr ev) | _ -> - Constr.map aux t in + EConstr.map !evdref aux t in let c = aux t in (* side-effect *) (!evdref, c) -let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) = - match kind_of_term f with +let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst : subst0) = + let open EConstr in + let open Vars in + match EConstr.kind sigma f with | Meta k -> (* We enforce that the Meta does not depend on the [nb] 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 (List.map EConstr.of_constr l) (EConstr.of_constr c) in + let c = solve_pattern_eqn env sigma l c in let pb = (Conv,TypeNotProcessed) in - if noccur_between 1 nb c then + if noccur_between sigma 1 nb c then sigma,(k,lift (-nb) c,pb)::metasubst,evarsubst else error_cannot_unify_local env sigma (applist (f, l),c,c) | 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 (List.map EConstr.of_constr l) (EConstr.of_constr c))::evarsubst + sigma,metasubst,(env,ev,solve_pattern_eqn env sigma l c)::evarsubst | _ -> assert false let push d (env,n) = (push_rel_assum d env,n+1) @@ -456,15 +472,16 @@ let use_evars_pattern_unification flags = !global_pattern_unification_flag && flags.use_pattern_unification && Flags.version_strictly_greater Flags.V8_2 -let use_metas_pattern_unification flags nb l = +let use_metas_pattern_unification sigma flags nb l = + let open EConstr in !global_pattern_unification_flag && flags.use_pattern_unification || (Flags.version_less_or_equal Flags.V8_3 || flags.use_meta_bound_pattern_unification) && - Array.for_all (fun c -> isRel c && destRel c <= nb) l + Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l type key = | IsKey of CClosure.table_key - | IsProj of projection * constr + | IsProj of projection * EConstr.constr let expand_table_key env = function | ConstKey cst -> constant_opt_value_in env cst @@ -480,11 +497,11 @@ let unfold_projection env p stk = | None -> assert false) let expand_key ts env sigma = function - | Some (IsKey k) -> expand_table_key env k + | Some (IsKey k) -> Option.map EConstr.of_constr (expand_table_key env k) | Some (IsProj (p, c)) -> - let red = EConstr.Unsafe.to_constr (Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma - Cst_stack.empty (EConstr.of_constr c, unfold_projection env p [])))) - in if Term.eq_constr (mkProj (p, c)) red then None else Some red + let red = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma + Cst_stack.empty (c, unfold_projection env p []))) + in if EConstr.eq_constr sigma (EConstr.mkProj (p, c)) red then None else Some red | None -> None @@ -497,9 +514,9 @@ type unirec_flags = { let subterm_restriction opt flags = not opt.at_top && flags.restrict_conv_on_strict_subterms -let key_of env b flags f = +let key_of env sigma b flags f = if subterm_restriction b flags then None else - match kind_of_term f with + match EConstr.kind sigma f with | Const (cst, u) when is_transparent env (ConstKey cst) && (Cpred.mem cst (snd flags.modulo_delta) || Environ.is_projection cst env) -> @@ -544,8 +561,8 @@ let oracle_order env cf1 cf2 = Some (Conv_oracle.oracle_order (fun x -> x) (Environ.oracle env) false (translate_key k1) (translate_key k2)) -let is_rigid_head flags t = - match kind_of_term t with +let is_rigid_head sigma flags t = + match EConstr.kind sigma t with | Const (cst,u) -> not (Cpred.mem cst (snd flags.modulo_delta)) | Ind (i,u) -> true | Construct _ -> true @@ -561,15 +578,15 @@ let force_eqs c = let constr_cmp pb sigma flags t u = let cstrs = - if pb == Reduction.CONV then Universes.eq_constr_universes t u - else Universes.leq_constr_universes t u + if pb == Reduction.CONV then EConstr.eq_constr_universes sigma t u + else EConstr.leq_constr_universes sigma t u in match cstrs with | Some cstrs -> begin try Evd.add_universe_constraints sigma cstrs, true with Univ.UniverseInconsistency _ -> sigma, false | Evd.UniversesDiffer -> - if is_rigid_head flags t then + if is_rigid_head sigma flags t then try Evd.add_universe_constraints sigma (force_eqs cstrs), true with Univ.UniverseInconsistency _ -> sigma, false else sigma, false @@ -578,46 +595,47 @@ let constr_cmp pb sigma flags t u = sigma, false let do_reduce ts (env, nb) sigma c = - EConstr.Unsafe.to_constr (Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state - ts env sigma Cst_stack.empty (EConstr.of_constr c, Stack.empty)))) + Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state + ts env sigma Cst_stack.empty (c, Stack.empty))) let use_full_betaiota flags = flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3 -let isAllowedEvar flags c = match kind_of_term c with +let isAllowedEvar sigma flags c = match EConstr.kind sigma c with | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) | _ -> false -let subst_defined_metas_evars (bl,el) c = - let rec substrec c = match kind_of_term c with +let subst_defined_metas_evars sigma (bl,el) c = + let rec substrec c = match EConstr.kind sigma c with | Meta i -> let select (j,_,_) = Int.equal i j in substrec (pi2 (List.find select bl)) | Evar (evk,args) -> - let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in + let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal (EConstr.eq_constr sigma) args args' in (try substrec (pi3 (List.find select el)) - with Not_found -> Constr.map substrec c) - | _ -> Constr.map substrec c + with Not_found -> EConstr.map sigma substrec c) + | _ -> EConstr.map sigma substrec c in try Some (substrec c) with Not_found -> None -let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN = - match subst_defined_metas_evars (metasubst,[]) tyM with +let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM tyN = + match subst_defined_metas_evars sigma (metasubst,[]) (EConstr.of_constr tyM) with | None -> sigma | Some m -> - match subst_defined_metas_evars (metasubst,[]) tyN with + match subst_defined_metas_evars sigma (metasubst,[]) (EConstr.of_constr tyN) with | None -> sigma | Some n -> - if is_ground_term sigma (EConstr.of_constr m) && is_ground_term sigma (EConstr.of_constr n) then - let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma (EConstr.of_constr m) (EConstr.of_constr n) in + if is_ground_term sigma m && is_ground_term sigma n then + let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in if b then sigma else error_cannot_unify env sigma (m,n) else sigma -let rec is_neutral env ts t = - let (f, l) = decompose_appvect t in - match kind_of_term f with +let rec is_neutral env sigma ts t = + let open EConstr in + let (f, l) = decompose_app_vect sigma t in + match EConstr.kind sigma (EConstr.of_constr f) with | Const (c, u) -> not (Environ.evaluable_constant c env) || not (is_transparent env (ConstKey c)) || @@ -628,24 +646,25 @@ let rec is_neutral env ts t = not (Id.Pred.mem id (fst ts)) | Rel n -> true | Evar _ | Meta _ -> true - | Case (_, p, c, cl) -> is_neutral env ts c - | Proj (p, c) -> is_neutral env ts c + | Case (_, p, c, cl) -> is_neutral env sigma ts c + | Proj (p, c) -> is_neutral env sigma ts c | _ -> false -let is_eta_constructor_app env ts f l1 term = - match kind_of_term f with +let is_eta_constructor_app env sigma ts f l1 term = + match EConstr.kind sigma f with | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite && Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) - is_neutral env ts term + is_neutral env sigma ts term | _ -> false) | _ -> false -let eta_constructor_app env f l1 term = - match kind_of_term f with +let eta_constructor_app env sigma f l1 term = + let open EConstr in + match EConstr.kind sigma f with | Construct (((_, i as ind), j), u) -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with @@ -658,15 +677,20 @@ let eta_constructor_app env f l1 term = | _ -> assert false) | _ -> assert false -let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n = - let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn) curm curn = - let cM = EConstr.Unsafe.to_constr (Evarutil.whd_head_evar sigma (EConstr.of_constr curm)) - and cN = EConstr.Unsafe.to_constr (Evarutil.whd_head_evar sigma (EConstr.of_constr curn)) in +let print_constr_env env c = + print_constr_env env (EConstr.Unsafe.to_constr c) + +let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top env cv_pb flags m n = + let open EConstr in + let open Vars in + let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn : subst0) curm curn = + let cM = Evarutil.whd_head_evar sigma curm + and cN = Evarutil.whd_head_evar sigma curn in let () = if !debug_unification then - Feedback.msg_debug (Termops.print_constr_env curenv cM ++ str" ~= " ++ Termops.print_constr_env curenv cN) + Feedback.msg_debug (print_constr_env curenv cM ++ str" ~= " ++ print_constr_env curenv cN) in - match (kind_of_term cM,kind_of_term cN) with + match (EConstr.kind sigma cM, EConstr.kind sigma cN) with | Meta k1, Meta k2 -> if Int.equal k1 k2 then substn else let stM,stN = extract_instance_status pb in @@ -681,12 +705,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst else sigma,(k2,cM,stM)::metasubst,evarsubst | Meta k, _ - when not (dependent sigma (EConstr.of_constr cM) (EConstr.of_constr cN)) (* helps early trying alternatives *) -> + when not (dependent sigma cM cN) (* helps early trying alternatives *) -> let sigma = if opt.with_types && flags.check_applied_meta_types then (try let tyM = Typing.meta_type sigma k in - let tyN = get_type_of curenv ~lax:true sigma (EConstr.of_constr cN) in + let tyN = get_type_of curenv ~lax:true sigma cN in check_compatibility curenv CUMUL flags substn tyN tyM with RetypeError _ -> (* Renounce, maybe metas/evars prevents typing *) sigma) @@ -695,17 +719,17 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (* Here we check that [cN] does not contain any local variables *) if Int.equal nb 0 then sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst - else if noccur_between 1 nb cN then + else if noccur_between sigma 1 nb cN then (sigma, (k,lift (-nb) cN,snd (extract_instance_status pb))::metasubst, evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Meta k - when not (dependent sigma (EConstr.of_constr cN) (EConstr.of_constr cM)) (* helps early trying alternatives *) -> + when not (dependent sigma cN cM) (* helps early trying alternatives *) -> let sigma = if opt.with_types && flags.check_applied_meta_types then (try - let tyM = get_type_of curenv ~lax:true sigma (EConstr.of_constr cM) in + let tyM = get_type_of curenv ~lax:true sigma cM in let tyN = Typing.meta_type sigma k in check_compatibility curenv CUMUL flags substn tyM tyN with RetypeError _ -> @@ -715,7 +739,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (* Here we check that [cM] does not contain any local variables *) if Int.equal nb 0 then (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst) - else if noccur_between 1 nb cM + else if noccur_between sigma 1 nb cM then (sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst, evarsubst) @@ -730,15 +754,15 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb sigma,metasubst,((curenv,ev,cN)::evarsubst) | Evar (evk,_ as ev), _ when not (Evar.Set.mem evk flags.frozen_evars) - && not (occur_evar sigma evk (EConstr.of_constr cN)) -> - let cmvars = free_rels sigma (EConstr.of_constr cM) and cnvars = free_rels sigma (EConstr.of_constr cN) in + && not (occur_evar sigma evk cN) -> + let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in if Int.Set.subset cnvars cmvars then sigma,metasubst,((curenv,ev,cN)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Evar (evk,_ as ev) when not (Evar.Set.mem evk flags.frozen_evars) - && not (occur_evar sigma evk (EConstr.of_constr cM)) -> - let cmvars = free_rels sigma (EConstr.of_constr cM) and cnvars = free_rels sigma (EConstr.of_constr cN) in + && not (occur_evar sigma evk cM) -> + let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in if Int.Set.subset cmvars cnvars then sigma,metasubst,((curenv,ev,cM)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) @@ -781,30 +805,30 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | App (f1, l1), _ when flags.modulo_eta && (* This ensures cN is an evar, meta or irreducible constant/variable and not a constructor. *) - is_eta_constructor_app curenv flags.modulo_delta f1 l1 cN -> + is_eta_constructor_app curenv sigma flags.modulo_delta f1 l1 cN -> (try - let l1', l2' = eta_constructor_app curenv f1 l1 cN in + let l1', l2' = eta_constructor_app curenv sigma f1 l1 cN in let opt' = {opt with at_top = true; with_cs = false} in Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2' with ex when precatchable_exception ex -> - match kind_of_term cN with + match EConstr.kind sigma cN with | App(f2,l2) when - (isMeta f2 && use_metas_pattern_unification flags nb l2 - || use_evars_pattern_unification flags && isAllowedEvar flags f2) -> + (isMeta sigma f2 && use_metas_pattern_unification sigma flags nb l2 + || use_evars_pattern_unification flags && isAllowedEvar sigma flags f2) -> unify_app_pattern false curenvnb pb opt substn cM f1 l1 cN f2 l2 | _ -> raise ex) | _, App (f2, l2) when flags.modulo_eta && - is_eta_constructor_app curenv flags.modulo_delta f2 l2 cM -> + is_eta_constructor_app curenv sigma flags.modulo_delta f2 l2 cM -> (try - let l2', l1' = eta_constructor_app curenv f2 l2 cM in + let l2', l1' = eta_constructor_app curenv sigma f2 l2 cM in let opt' = {opt with at_top = true; with_cs = false} in Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2' with ex when precatchable_exception ex -> - match kind_of_term cM with + match EConstr.kind sigma cM with | App(f1,l1) when - (isMeta f1 && use_metas_pattern_unification flags nb l1 - || use_evars_pattern_unification flags && isAllowedEvar flags f1) -> + (isMeta sigma f1 && use_metas_pattern_unification sigma flags nb l1 + || use_evars_pattern_unification flags && isAllowedEvar sigma flags f1) -> unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2 | _ -> raise ex) @@ -819,13 +843,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb reduce curenvnb pb opt substn cM cN) | App (f1,l1), _ when - (isMeta f1 && use_metas_pattern_unification flags nb l1 - || use_evars_pattern_unification flags && isAllowedEvar flags f1) -> + (isMeta sigma f1 && use_metas_pattern_unification sigma flags nb l1 + || use_evars_pattern_unification flags && isAllowedEvar sigma flags f1) -> unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN cN [||] | _, App (f2,l2) when - (isMeta f2 && use_metas_pattern_unification flags nb l2 - || use_evars_pattern_unification flags && isAllowedEvar flags f2) -> + (isMeta sigma f2 && use_metas_pattern_unification sigma flags nb l2 + || use_evars_pattern_unification flags && isAllowedEvar sigma flags f2) -> unify_app_pattern false curenvnb pb opt substn cM cM [||] cN f2 l2 | App (f1,l1), App (f2,l2) -> @@ -840,32 +864,32 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | _ -> unify_not_same_head curenvnb pb opt substn cM cN - and unify_app_pattern dir curenvnb pb opt substn cM f1 l1 cN f2 l2 = + and unify_app_pattern dir curenvnb pb opt (sigma, _, _ as 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 (EConstr.of_constr f) (Array.map_to_list EConstr.of_constr l) (EConstr.of_constr t) with + match is_unification_pattern curenvnb sigma f (Array.to_list l) t with | None -> - (match kind_of_term t with + (match EConstr.kind sigma t with | App (f',l') -> if dir then unify_app curenvnb pb opt substn cM f1 l1 t f' l' else unify_app curenvnb pb opt substn t f' l' cN f2 l2 | 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 (List.map EConstr.Unsafe.to_constr l) t substn + solve_pattern_eqn_array curenvnb f l t substn - and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 = + and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn : subst0) cM f1 l1 cN f2 l2 = try let needs_expansion p c' = - match kind_of_term c' with + match EConstr.kind sigma c' with | Meta _ -> true | Evar _ -> true | Const (c, u) -> Constant.equal c (Projection.constant p) | _ -> false in let expand_proj c c' l = - match kind_of_term c with + match EConstr.kind sigma c with | Proj (p, t) when not (Projection.unfolded p) && needs_expansion p c' -> - (try destApp (Retyping.expand_projection curenv sigma p (EConstr.of_constr t) (Array.map_to_list EConstr.of_constr l)) + (try destApp sigma (EConstr.of_constr (Retyping.expand_projection curenv sigma p t (Array.to_list l))) with RetypeError _ -> (** Unification can be called on ill-typed terms, due to FO and eta in particular, fail gracefully in that case *) (c, l)) @@ -890,8 +914,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb and unify_same_proj (curenv, nb as curenvnb) cv_pb opt substn c1 c2 = let substn = unirec_rec curenvnb CONV opt substn c1 c2 in try (* Force unification of the types to fill in parameters *) - let ty1 = get_type_of curenv ~lax:true sigma (EConstr.of_constr c1) in - let ty2 = get_type_of curenv ~lax:true sigma (EConstr.of_constr c2) in + let ty1 = get_type_of curenv ~lax:true sigma c1 in + let ty2 = get_type_of curenv ~lax:true sigma c2 in + let ty1 = EConstr.of_constr ty1 in + let ty2 = EConstr.of_constr ty2 in unify_0_with_initial_metas substn true curenv cv_pb { flags with modulo_conv_on_closed_terms = Some full_transparent_state; modulo_delta = full_transparent_state; @@ -900,7 +926,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb ty1 ty2 with RetypeError _ -> substn - and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn) cM cN = + and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN = try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> let sigma', b = constr_cmp cv_pb sigma flags cM cN in @@ -909,24 +935,24 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb try reduce curenvnb pb opt substn cM cN with ex when precatchable_exception ex -> let (f1,l1) = - match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in + match EConstr.kind sigma cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in let (f2,l2) = - match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in + match EConstr.kind sigma cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in expand curenvnb pb opt substn cM f1 l1 cN f2 l2 and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN = if use_full_betaiota flags && not (subterm_restriction opt flags) then let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in - if not (Term.eq_constr cM cM') then + if not (EConstr.eq_constr sigma cM cM') then unirec_rec curenvnb pb opt substn cM' cN else let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in - if not (Term.eq_constr cN cN') then + if not (EConstr.eq_constr sigma cN cN') then unirec_rec curenvnb pb opt substn cM cN' else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) - and expand (curenv,_ as curenvnb) pb opt (sigma,metasubst,evarsubst as substn) cM f1 l1 cN f2 l2 = + and expand (curenv,_ as curenvnb) pb opt (sigma,metasubst,evarsubst as substn : subst0) cM f1 l1 cN f2 l2 = let res = (* Try full conversion on meta-free terms. *) (* Back to 1995 (later on called trivial_unify in 2002), the @@ -945,24 +971,23 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | None -> None | Some convflags -> let subst = ((if flags.use_metas_eagerly_in_conv_on_closed_terms then metasubst else ms), (if flags.use_evars_eagerly_in_conv_on_closed_terms then evarsubst else es)) in - match subst_defined_metas_evars subst cM with + match subst_defined_metas_evars sigma subst cM with | None -> (* some undefined Metas in cM *) None | Some m1 -> - match subst_defined_metas_evars subst cN with + match subst_defined_metas_evars sigma subst cN with | None -> (* some undefined Metas in cN *) None | Some n1 -> (* No subterm restriction there, too much incompatibilities *) let sigma = if opt.with_types then try (* Ensure we call conversion on terms of the same type *) - let tyM = get_type_of curenv ~lax:true sigma (EConstr.of_constr m1) in - let tyN = get_type_of curenv ~lax:true sigma (EConstr.of_constr n1) in + let tyM = get_type_of curenv ~lax:true sigma m1 in + let tyN = get_type_of curenv ~lax:true sigma n1 in check_compatibility curenv CUMUL flags substn tyM tyN with RetypeError _ -> (* Renounce, maybe metas/evars prevents typing *) sigma else sigma in - let m1 = EConstr.of_constr m1 and n1 = EConstr.of_constr n1 in let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in if b then Some (sigma, metasubst, evarsubst) else @@ -973,40 +998,40 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb match res with | Some substn -> substn | None -> - let cf1 = key_of curenv opt flags f1 and cf2 = key_of curenv opt flags f2 in + let cf1 = key_of curenv sigma opt flags f1 and cf2 = key_of curenv sigma opt flags f2 in match oracle_order curenv cf1 cf2 with | None -> error_cannot_unify curenv sigma (cM,cN) | Some true -> (match expand_key flags.modulo_delta curenv sigma cf1 with | Some c -> unirec_rec curenvnb pb opt substn - (whd_betaiotazeta sigma (EConstr.of_constr (mkApp(c,l1)))) cN + (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l1)))) cN | None -> (match expand_key flags.modulo_delta curenv sigma cf2 with | Some c -> unirec_rec curenvnb pb opt substn cM - (whd_betaiotazeta sigma (EConstr.of_constr (mkApp(c,l2)))) + (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l2)))) | None -> error_cannot_unify curenv sigma (cM,cN))) | Some false -> (match expand_key flags.modulo_delta curenv sigma cf2 with | Some c -> unirec_rec curenvnb pb opt substn cM - (whd_betaiotazeta sigma (EConstr.of_constr (mkApp(c,l2)))) + (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l2)))) | None -> (match expand_key flags.modulo_delta curenv sigma cf1 with | Some c -> unirec_rec curenvnb pb opt substn - (whd_betaiotazeta sigma (EConstr.of_constr (mkApp(c,l1)))) cN + (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l1)))) cN | None -> error_cannot_unify curenv sigma (cM,cN))) and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) = let f1 () = - if isApp cM then - let f1l1 = whd_nored_state sigma (EConstr.of_constr cM,Stack.empty) in + if isApp sigma cM then + let f1l1 = whd_nored_state sigma (cM,Stack.empty) in if is_open_canonical_projection curenv sigma f1l1 then - let f2l2 = whd_nored_state sigma (EConstr.of_constr cN,Stack.empty) in + let f2l2 = whd_nored_state sigma (cN,Stack.empty) in solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -1019,10 +1044,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb error_cannot_unify (fst curenvnb) sigma (cM,cN) else try f1 () with e when precatchable_exception e -> - if isApp cN then - let f2l2 = whd_nored_state sigma (EConstr.of_constr cN, Stack.empty) in + if isApp sigma cN then + let f2l2 = whd_nored_state sigma (cN, Stack.empty) in if is_open_canonical_projection curenv sigma f2l2 then - let f1l1 = whd_nored_state sigma (EConstr.of_constr cM, Stack.empty) in + let f1l1 = whd_nored_state sigma (cM, Stack.empty) in solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -1038,26 +1063,25 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb List.fold_left (fun (evd,ks,m) b -> if match n with Some n -> Int.equal m n | None -> false then - (evd,EConstr.Unsafe.to_constr t2::ks, m-1) + (evd,t2::ks, m-1) else let mv = new_meta () in - let evd' = meta_declare mv (substl ks b) evd in + let evd' = meta_declare mv (EConstr.Unsafe.to_constr (substl ks b)) evd in (evd', mkMeta mv :: ks, m - 1)) - (sigma,[],List.length bs) (List.map EConstr.Unsafe.to_constr bs) + (sigma,[],List.length bs) bs in try let opt' = {opt with with_types = false} in - let inj = EConstr.Unsafe.to_constr in let (substn,_,_) = Reductionops.Stack.fold2 - (fun s u1 u -> unirec_rec curenvnb pb opt' s (inj u1) (substl ks (inj u))) + (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) (evd,ms,es) us2 us in let (substn,_,_) = Reductionops.Stack.fold2 - (fun s u1 u -> unirec_rec curenvnb pb opt' s (inj u1) (substl ks (inj u))) + (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) substn params1 params in - let (substn,_,_) = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s (inj u1) (inj u2)) substn ts ts1 in - let app = mkApp (EConstr.Unsafe.to_constr c, Array.rev_of_list ks) in + let (substn,_,_) = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in + let app = mkApp (c, Array.rev_of_list ks) in (* let substn = unirec_rec curenvnb pb b false substn t cN in *) - unirec_rec curenvnb pb opt' substn (EConstr.Unsafe.to_constr c1) app + unirec_rec curenvnb pb opt' substn c1 app with Invalid_argument "Reductionops.Stack.fold2" -> error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -1073,7 +1097,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb None else let sigma, b = match flags.modulo_conv_on_closed_terms with - | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma (EConstr.of_constr m) (EConstr.of_constr n) + | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n | _ -> constr_cmp cv_pb sigma flags m n in if b then Some sigma else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with @@ -1101,7 +1125,9 @@ let right = false let rec unify_with_eta keptside flags env sigma c1 c2 = (* Question: try whd_all on ci if not two lambdas? *) - match kind_of_term c1, kind_of_term c2 with + let open EConstr in + let open Vars in + match EConstr.kind sigma c1, EConstr.kind sigma c2 with | (Lambda (na,t1,c1'), Lambda (_,t2,c2')) -> let env' = push_rel_assum (na,t1) env in let sigma,metas,evars = unify_0 env sigma CONV flags t1 t2 in @@ -1205,32 +1231,39 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * since other metavars might also need to be resolved. *) let applyHead env (type r) (evd : r Sigma.t) n c = + let open EConstr in + let open Vars in let rec apprec : type s. _ -> _ -> _ -> (r, s) Sigma.le -> s Sigma.t -> (constr, r) Sigma.sigma = fun n c cty p evd -> if Int.equal n 0 then Sigma (c, evd, p) else - match kind_of_term (whd_all env (Sigma.to_evar_map evd) (EConstr.of_constr cty)) with + let sigma = Sigma.to_evar_map evd in + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma cty)) with | Prod (_,c1,c2) -> - let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) (EConstr.of_constr c1) in + let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in + let evar = EConstr.of_constr evar in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' | _ -> error "Apply_Head_Then" in - apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) (EConstr.of_constr c)) Sigma.refl evd + apprec n c (EConstr.of_constr (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c)) Sigma.refl evd -let is_mimick_head ts f = - match kind_of_term f with +let is_mimick_head sigma ts f = + match EConstr.kind sigma f with | Const (c,u) -> not (CClosure.is_transparent_constant ts c) | Var id -> not (CClosure.is_transparent_variable ts id) | (Rel _|Construct _|Ind _) -> true | _ -> false +let make_judge c t = + make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t) + let try_to_coerce env evd c cty tycon = let j = make_judge c cty in - let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j (EConstr.of_constr tycon) in + let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in let evd' = Evarconv.consider_remaining_unif_problems env evd' in let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in - (evd',j'.uj_val) + (evd',EConstr.of_constr j'.uj_val) let w_coerce_to_type env evd c cty mvty = let evd,tycon = pose_all_metas_as_evars env evd mvty in @@ -1239,19 +1272,19 @@ let w_coerce_to_type env evd c cty mvty = (* inh_conv_coerce_rigid_to should have reasoned modulo reduction but there are cases where it though it was not rigid (like in fst (nat,nat)) and stops while it could have seen that it is rigid *) - let cty = Tacred.hnf_constr env evd (EConstr.of_constr cty) in - try_to_coerce env evd c cty tycon + let cty = Tacred.hnf_constr env evd cty in + try_to_coerce env evd c (EConstr.of_constr cty) tycon let w_coerce env evd mv c = - let cty = get_type_of env evd (EConstr.of_constr c) in + let cty = get_type_of env evd c in let mvty = Typing.meta_type evd mv in - w_coerce_to_type env evd c cty mvty + w_coerce_to_type env evd c (EConstr.of_constr cty) (EConstr.of_constr mvty) let unify_to_type env sigma flags c status u = - let sigma, c = refresh_universes (Some false) env sigma (EConstr.of_constr c) in + let sigma, c = refresh_universes (Some false) env sigma 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 + unify_0 env sigma CUMUL flags (EConstr.of_constr t) (EConstr.of_constr u) let unify_type env sigma flags mv status c = let mvty = Typing.meta_type sigma mv in @@ -1274,9 +1307,10 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) let solve_simple_evar_eqn ts env evd ev rhs = - match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,EConstr.of_constr rhs) with + let open EConstr in + match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> - error_cannot_unify env evd ~reason (EConstr.Unsafe.to_constr (EConstr.mkEvar ev),rhs); + error_cannot_unify env evd ~reason (mkEvar ev,rhs); | Success evd -> Evarconv.consider_remaining_unif_problems env evd @@ -1284,25 +1318,27 @@ let solve_simple_evar_eqn ts env evd ev rhs = or in evars, possibly generating new unification problems; if [b] is true, unification of types of metas is required *) -let w_merge env with_types flags (evd,metas,evars) = +let w_merge env with_types flags (evd,metas,evars : subst0) = + let open EConstr in + let open Vars in let rec w_merge_rec evd metas evars eqns = (* Process evars *) match evars with | (curenv,(evk,_ as ev),rhs)::evars' -> if Evd.is_defined evd evk then - let v = Evd.existential_value evd ev in + let v = mkEvar ev in let (evd,metas',evars'') = unify_0 curenv evd CONV flags rhs v in w_merge_rec evd (metas'@metas) (evars''@evars') eqns else begin (* This can make rhs' ill-typed if metas are *) - let rhs' = subst_meta_instances metas rhs in - match kind_of_term rhs with - | App (f,cl) when occur_meta evd (EConstr.of_constr rhs') -> - if occur_evar evd evk (EConstr.of_constr rhs') then + let rhs' = subst_meta_instances evd metas rhs in + match EConstr.kind evd rhs with + | App (f,cl) when occur_meta evd rhs' -> + if occur_evar evd evk rhs' then error_occur_check curenv evd evk rhs'; - if is_mimick_head flags.modulo_delta f then + if is_mimick_head evd flags.modulo_delta f then let evd' = mimick_undefined_evar evd flags f (Array.length cl) evk in (* let evd' = Evarconv.consider_remaining_unif_problems env evd' in *) @@ -1310,14 +1346,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' (fst ev, Array.map EConstr.of_constr (snd ev)) rhs'' + try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' 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' (fst ev, Array.map EConstr.of_constr (snd ev)) rhs'' + try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'' with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev, rhs'') in w_merge_rec evd' metas evars' eqns @@ -1343,20 +1379,20 @@ let w_merge env with_types flags (evd,metas,evars) = if meta_defined evd mv then let {rebus=c'},(status',_) = meta_fvalue evd mv in let (take_left,st,(evd,metas',evars')) = - merge_instances env evd flags status' status c' c + merge_instances env evd flags status' status (EConstr.of_constr c') c in let evd' = if take_left then evd - else meta_reassign mv (c,(st,TypeProcessed)) evd + else meta_reassign mv (EConstr.Unsafe.to_constr c,(st,TypeProcessed)) evd in w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns else let evd' = if occur_meta_evd evd mv c then - if isMetaOf mv (whd_all env evd (EConstr.of_constr c)) then evd + if isMetaOf mv (whd_all env evd c) then evd else error_cannot_unify env evd (mkMeta mv,c) else - meta_assign mv (c,(status,TypeProcessed)) evd in + meta_assign mv (EConstr.Unsafe.to_constr c,(status,TypeProcessed)) evd in w_merge_rec evd' (metas''@metas) evars'' eqns | [] -> (* Process type eqns *) @@ -1382,17 +1418,17 @@ let w_merge env with_types flags (evd,metas,evars) = let evd' = Sigma.to_evar_map evd' in let (evd'',mc,ec) = unify_0 sp_env evd' CUMUL flags - (get_type_of sp_env evd' (EConstr.of_constr c)) ev.evar_concl in + (EConstr.of_constr (get_type_of sp_env evd' c)) (EConstr.of_constr ev.evar_concl) in let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' - then Evd.define sp c evd''' - else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in + then Evd.define sp (EConstr.Unsafe.to_constr c) evd''' + else Evd.define sp (Evarutil.nf_evar evd''' (EConstr.Unsafe.to_constr c)) evd''' in let check_types evd = let metas = Evd.meta_list evd in let eqns = List.fold_left (fun acc (mv, b) -> match b with - | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, t.rebus) :: acc + | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, EConstr.of_constr t.rebus) :: acc | _ -> acc) [] metas in w_merge_rec evd [] [] eqns in @@ -1404,6 +1440,11 @@ let w_merge env with_types flags (evd,metas,evars) = if with_types then check_types res else res +let retract_coercible_metas evd = + let (metas, evd) = retract_coercible_metas evd in + let map (mv, c, st) = (mv, EConstr.of_constr c, st) in + (List.map map metas, evd) + let w_unify_meta_types env ?(flags=default_unify_flags ()) evd = let metas,evd = retract_coercible_metas evd in w_merge env true flags.merge_unify_flags (evd,metas,[]) @@ -1419,19 +1460,23 @@ let w_unify_meta_types env ?(flags=default_unify_flags ()) evd = types of metavars are unifiable with the types of their instances *) let head_app sigma m = - EConstr.Unsafe.to_constr (fst (whd_nored_state sigma (EConstr.of_constr m, Stack.empty))) + fst (whd_nored_state sigma (m, Stack.empty)) + +let isEvar_or_Meta sigma c = match EConstr.kind sigma c with +| Evar _ | Meta _ -> true +| _ -> false let check_types env flags (sigma,_,_ as subst) m n = - if isEvar_or_Meta (head_app sigma m) then + if isEvar_or_Meta sigma (head_app sigma m) then unify_0_with_initial_metas subst true env CUMUL flags - (get_type_of env sigma (EConstr.of_constr n)) - (get_type_of env sigma (EConstr.of_constr m)) - else if isEvar_or_Meta (head_app sigma n) then + (EConstr.of_constr (get_type_of env sigma n)) + (EConstr.of_constr (get_type_of env sigma m)) + else if isEvar_or_Meta sigma (head_app sigma n) then unify_0_with_initial_metas subst true env CUMUL flags - (get_type_of env sigma (EConstr.of_constr m)) - (get_type_of env sigma (EConstr.of_constr n)) + (EConstr.of_constr (get_type_of env sigma m)) + (EConstr.of_constr (get_type_of env sigma n)) else subst let try_resolve_typeclasses env evd flag m n = @@ -1453,6 +1498,11 @@ let w_unify_core_0 env evd with_types cv_pb flags m n = let w_typed_unify env evd = w_unify_core_0 env evd true let w_typed_unify_array env evd flags f1 l1 f2 l2 = + let open EConstr in + let f1 = EConstr.of_constr f1 in + let f2 = EConstr.of_constr f2 in + let l1 = Array.map EConstr.of_constr l1 in + let l2 = Array.map EConstr.of_constr l2 in let f1,l1,f2,l2 = adjust_app_array_size f1 l1 f2 l2 in let (mc1,evd') = retract_coercible_metas evd in let fold_subst subst m n = unify_0_with_initial_metas subst true env CONV flags.core_unify_flags m n in @@ -1479,7 +1529,8 @@ let iter_fail f a = contexts, with evars, and possibly with occurrences *) let indirectly_dependent sigma c d decls = - not (isVar c) && + let open EConstr in + not (isVar sigma c) && (* This test is not needed if the original term is a variable, but it is needed otherwise, as e.g. when abstracting over "2" in "forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious @@ -1493,7 +1544,8 @@ let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sig let current_sigma = Sigma.to_evar_map current_sigma in let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in let sigma, subst = nf_univ_variables sigma in - Sigma.Unsafe.of_pair (subst_univs_constr subst (nf_evar sigma c), sigma) + let c = EConstr.Unsafe.to_constr c in + Sigma.Unsafe.of_pair (EConstr.of_constr (CVars.subst_univs_constr subst (nf_evar sigma c)), sigma) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1538,6 +1590,7 @@ let default_matching_flags (sigma,_) = exception PatternNotFound let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = + let open EConstr in let flags = if from_prefix_of_ind then let flags = default_matching_flags pending in @@ -1545,7 +1598,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = modulo_conv_on_closed_terms = Some Names.full_transparent_state; restrict_conv_on_strict_subterms = true } } else default_matching_flags pending in - let n = List.length (snd (decompose_app c)) in + let n = Array.length (snd (decompose_app_vect sigma c)) in let matching_fun _ t = let open EConstr in try @@ -1560,8 +1613,9 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = else applist (t,l1), l2 else t, [] in - let sigma = w_typed_unify env sigma Reduction.CONV flags c (EConstr.Unsafe.to_constr t') in + let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in let ty = Retyping.get_type_of env sigma t in + let ty = EConstr.of_constr ty in if not (is_correct_type ty) then raise (NotUnifiable None); Some(sigma, t, l2) with @@ -1582,19 +1636,20 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = (fun test -> match test.testing_state with | None -> None | Some (sigma,_,l) -> - let c = applist (nf_evar sigma (local_strong whd_meta sigma (EConstr.of_constr c)), List.map (EConstr.to_constr sigma) l) in + let c = applist (EConstr.of_constr (nf_evar sigma (local_strong whd_meta sigma c)), l) in let univs, subst = nf_univ_variables sigma in - Some (sigma,subst_univs_constr subst c)) + Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) let make_eq_test env evd c = let out cstr = - match cstr.last_found with None -> None | _ -> Some (cstr.testing_state, EConstr.Unsafe.to_constr c) + match cstr.last_found with None -> None | _ -> Some (cstr.testing_state, c) in (make_eq_univs_test env evd c, out) let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let id = - let t = match ty with Some t -> t | None -> get_type_of env sigma (EConstr.of_constr c) in + let ty = Option.map EConstr.Unsafe.to_constr ty in + let t = match ty with Some t -> t | None -> get_type_of env sigma c in let x = id_of_name_using_hdchar (Global.env()) t name in let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else @@ -1634,7 +1689,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = | NoOccurrences -> concl | occ -> let occ = if likefirst then LikeFirst else AtOccs occ in - replace_term_occ_modulo sigma occ test mkvarid (EConstr.of_constr concl) + EConstr.of_constr (replace_term_occ_modulo sigma occ test mkvarid concl) in let lastlhyp = if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in @@ -1660,6 +1715,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = type prefix_of_inductive_support_flag = bool +type pending_constr = Evd.pending * constr + type abstraction_request = | AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool | AbstractExact of Name.t * constr * types option * clause * bool @@ -1678,7 +1735,7 @@ let make_abstraction env evd ccl abs = env evd (snd c) None occs check_occs ccl | AbstractExact (name,c,ty,occs,check_occs) -> make_abstraction_core name - (make_eq_test env evd (EConstr.of_constr c)) + (make_eq_test env evd c) env evd c ty occs check_occs ccl let keyed_unify env evd kop = @@ -1688,7 +1745,7 @@ let keyed_unify env evd kop = | None -> fun _ -> true | Some kop -> fun cl -> - let kc = Keys.constr_key cl in + let kc = Keys.constr_key (EConstr.to_constr evd cl) in match kc with | None -> false | Some kc -> Keys.equiv_keys kop kc @@ -1697,23 +1754,25 @@ let keyed_unify env evd kop = Unifies [cl] to every subterm of [op] until it finds a match. Fails if no match is found *) let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = + let open EConstr in + let open Vars in let bestexn = ref None in - let kop = Keys.constr_key op in + let kop = Keys.constr_key (EConstr.to_constr evd op) in let rec matchrec cl = - let cl = strip_outer_cast evd (EConstr.of_constr cl) in + let cl = EConstr.of_constr (strip_outer_cast evd cl) in (try - if closed0 cl && not (isEvar cl) && keyed_unify env evd kop cl then + if closed0 evd cl && not (isEvar evd cl) && keyed_unify env evd kop cl then (try if !keyed_unification then - let f1, l1 = decompose_app_vect evd (EConstr.of_constr op) in - let f2, l2 = decompose_app_vect evd (EConstr.of_constr cl) in + let f1, l1 = decompose_app_vect evd op in + let f2, l2 = decompose_app_vect evd cl in w_typed_unify_array env evd flags f1 l1 f2 l2,cl else w_typed_unify env evd CONV flags op cl,cl with ex when Pretype_errors.unsatisfiable_exception ex -> bestexn := Some ex; error "Unsat") else error "Bound 1" with ex when precatchable_exception ex -> - (match kind_of_term cl with + (match EConstr.kind evd cl with | App (f,args) -> let n = Array.length args in assert (n>0); @@ -1772,9 +1831,11 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = Unifies [cl] to every subterm of [op] and return all the matches. Fails if no match is found *) let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = + let open EConstr in + let open Vars in let return a b = let (evd,c as a) = a () in - if List.exists (fun (evd',c') -> Term.eq_constr c c') b then b else a :: b + if List.exists (fun (evd',c') -> EConstr.eq_constr evd' c c') b then b else a :: b in let fail str _ = error str in let bind f g a = @@ -1793,12 +1854,13 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = in ffail 0 in let rec matchrec cl = - let cl = strip_outer_cast evd (EConstr.of_constr cl) in + let cl = strip_outer_cast evd cl in + let cl = EConstr.of_constr cl in (bind - (if closed0 cl + (if closed0 evd cl then return (fun () -> w_typed_unify env evd CONV flags op cl,cl) else fail "Bound 1") - (match kind_of_term cl with + (match EConstr.kind evd cl with | App (f,args) -> let n = Array.length args in assert (n>0); @@ -1835,16 +1897,18 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = | _ -> res let w_unify_to_subterm_list env evd flags hdmeta oplist t = + let open EConstr in List.fold_right (fun op (evd,l) -> - let op = whd_meta evd (EConstr.of_constr op) in - if isMeta op then + let op = whd_meta evd op in + let op = EConstr.of_constr op in + if isMeta evd op then if flags.allow_K_in_toplevel_higher_order_unification then (evd,op::l) - else error_abstraction_over_meta env evd hdmeta (destMeta op) + else error_abstraction_over_meta env evd hdmeta (destMeta evd op) else let allow_K = flags.allow_K_in_toplevel_higher_order_unification in let flags = - if occur_meta_or_existential evd (EConstr.of_constr op) || !keyed_unification then + if occur_meta_or_existential evd op || !keyed_unification then (* This is up to delta for subterms w/o metas ... *) flags else @@ -1853,7 +1917,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = unify pre-existing non frozen evars of the goal or of the pattern *) set_no_delta_flags flags in - let t' = (strip_outer_cast evd (EConstr.of_constr op),t) in + let t' = (EConstr.of_constr (strip_outer_cast evd op),t) in let (evd',cl) = try if is_keyed_unification () then @@ -1869,11 +1933,11 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = (* w_unify_to_subterm does not go through evars, so the next step, which was already in <= 8.4, is needed at least for compatibility of rewrite *) - dependent evd (EConstr.of_constr op) (EConstr.of_constr t) -> (evd,op) + dependent evd op t -> (evd,op) in if not allow_K && (* ensure we found a different instance *) - List.exists (fun op -> Term.eq_constr op cl) l + List.exists (fun op -> EConstr.eq_constr evd' op cl) l then error_non_linear_unification env evd hdmeta cl else (evd',cl::l)) oplist @@ -1884,8 +1948,9 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let flags = { flags with core_unify_flags = flags.subterm_unify_flags } in let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in let typp = Typing.meta_type evd' p in + let typp = EConstr.of_constr typp in let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in - let evd', b = infer_conv ~pb:CUMUL env evd' (EConstr.of_constr predtyp) (EConstr.of_constr typp) in + let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in if not b then error_wrong_abstraction_type env evd' (Evd.meta_name evd p) pred typp predtyp; @@ -1902,7 +1967,8 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let secondOrderDependentAbstraction env evd flags typ (p, oplist) = let typp = Typing.meta_type evd p in - let evd, pred = abstract_list_all_with_dependencies env evd (EConstr.of_constr typp) typ (List.map EConstr.of_constr oplist) in + let evd, pred = abstract_list_all_with_dependencies env evd (EConstr.of_constr typp) typ oplist in + let pred = EConstr.of_constr pred in w_merge env false flags.merge_unify_flags (evd,[p,pred,(Conv,TypeProcessed)],[]) @@ -1910,16 +1976,15 @@ let secondOrderAbstractionAlgo dep = if dep then secondOrderDependentAbstraction else secondOrderAbstraction let w_unify2 env evd flags dep cv_pb ty1 ty2 = - let inj = EConstr.Unsafe.to_constr in - let c1, oplist1 = whd_nored_stack evd (EConstr.of_constr ty1) in - let c2, oplist2 = whd_nored_stack evd (EConstr.of_constr ty2) in + let c1, oplist1 = whd_nored_stack evd ty1 in + let c2, oplist2 = whd_nored_stack evd ty2 in match EConstr.kind evd c1, EConstr.kind evd c2 with | Meta p1, _ -> (* Find the predicate *) - secondOrderAbstractionAlgo dep env evd flags ty2 (p1, List.map inj oplist1) + secondOrderAbstractionAlgo dep env evd flags ty2 (p1, oplist1) | _, Meta p2 -> (* Find the predicate *) - secondOrderAbstractionAlgo dep env evd flags ty1 (p2, List.map inj oplist2) + secondOrderAbstractionAlgo dep env evd flags ty1 (p2, oplist2) | _ -> error "w_unify2" (* The unique unification algorithm works like this: If the pattern is @@ -1943,8 +2008,9 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 = convertible and first-order otherwise. But if failed if e.g. the type of Meta(1) had meta-variables in it. *) let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = - let hd1,l1 = decompose_appvect (whd_nored evd (EConstr.of_constr ty1)) in - let hd2,l2 = decompose_appvect (whd_nored evd (EConstr.of_constr ty2)) in + let open EConstr in + let hd1,l1 = decompose_app_vect evd (EConstr.of_constr (whd_nored evd ty1)) in + let hd2,l2 = decompose_app_vect evd (EConstr.of_constr (whd_nored evd ty2)) in let is_empty1 = Array.is_empty l1 in let is_empty2 = Array.is_empty l2 in match kind_of_term hd1, not is_empty1, kind_of_term hd2, not is_empty2 with diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0ad882a9f..41dcb8ed3 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -7,6 +7,7 @@ (************************************************************************) open Term +open EConstr open Environ open Evd @@ -70,6 +71,8 @@ exception PatternNotFound type prefix_of_inductive_support_flag = bool +type pending_constr = Evd.pending * constr + type abstraction_request = | AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool @@ -97,28 +100,29 @@ val abstract_list_all : (* For tracing *) -val w_merge : env -> bool -> core_unify_flags -> evar_map * - (metavariable * constr * (instance_constraint * instance_typing_status)) list * - (env * types pexistential * types) list -> evar_map +type metabinding = (metavariable * constr * (instance_constraint * instance_typing_status)) + +type subst0 = + (evar_map * + metabinding list * + (Environ.env * existential * t) list) + +val w_merge : env -> bool -> core_unify_flags -> subst0 -> evar_map val unify_0 : Environ.env -> Evd.evar_map -> Evd.conv_pb -> core_unify_flags -> - Term.types -> - Term.types -> - Evd.evar_map * Evd.metabinding list * - (Environ.env * Term.types Term.pexistential * Term.constr) list + types -> + types -> + subst0 val unify_0_with_initial_metas : - Evd.evar_map * Evd.metabinding list * - (Environ.env * Term.types Term.pexistential * Term.constr) list -> + subst0 -> bool -> Environ.env -> Evd.conv_pb -> core_unify_flags -> - Term.types -> - Term.types -> - Evd.evar_map * Evd.metabinding list * - (Environ.env * Term.types Term.pexistential * Term.constr) list - + types -> + types -> + subst0 diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 68aeaef5e..2d621e97c 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -257,7 +257,7 @@ let clenv_dependent ce = clenv_dependent_gen false ce let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv = { clenv with - evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 } + evd = w_unify ~flags clenv.env clenv.evd cv_pb (EConstr.of_constr t1) (EConstr.of_constr t2) } let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } @@ -482,13 +482,15 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr u)))) then + let u = EConstr.of_constr u in + if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else (* Enough information so as to try a coercion now *) try - let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in + let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd (EConstr.of_constr c) (EConstr.of_constr t) u in + let c = EConstr.Unsafe.to_constr c in TypeProcessed, { clenv with evd = evd }, c with | PretypeError (_,_,ActualTypeNotCoercible (_,_, diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index d8a20e08b..bc5f17bf5 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -143,7 +143,7 @@ let unify ?(flags=fail_quick_unif_flags) m = let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in let evd = clear_metas (Tacmach.New.project gl) in try - let evd' = w_unify env evd CONV ~flags m n in + let evd' = w_unify env evd CONV ~flags (EConstr.of_constr m) (EConstr.of_constr n) in Proofview.Unsafe.tclEVARSADVANCE evd' with e when CErrors.noncritical e -> Proofview.tclZERO e end } diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index fd6528a1e..4be03af9a 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -26,7 +26,7 @@ let depends_on_evar evk _ (pbty,_,t1,t2) = let define_and_solve_constraints evk c env evd = if Termops.occur_evar evd evk (EConstr.of_constr c) then - Pretype_errors.error_occur_check env evd evk c; + Pretype_errors.error_occur_check env evd evk (EConstr.of_constr c); let evd = define evk c evd in let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in match diff --git a/proofs/goal.ml b/proofs/goal.ml index a141708c2..bcb14e2d6 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -87,7 +87,7 @@ module V82 = struct (* Check that the goal itself does not appear in the refined term *) let _ = if not (Evarutil.occur_evar_upto sigma evk c) then () - else Pretype_errors.error_occur_check Environ.empty_env sigma evk c + else Pretype_errors.error_occur_check Environ.empty_env sigma evk (EConstr.of_constr c) in Evd.define evk c sigma diff --git a/proofs/refine.ml b/proofs/refine.ml index 19134bfa3..0ed74c9b3 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -98,7 +98,7 @@ let make_refine_enter ?(unsafe = true) f = let self = Proofview.Goal.goal gl in let _ = if not (Evarutil.occur_evar_upto sigma self c) then () - else Pretype_errors.error_occur_check env sigma self c + else Pretype_errors.error_occur_check env sigma self (EConstr.of_constr c) in (** Proceed to the refinement *) let sigma = match evkmain with diff --git a/tactics/equality.ml b/tactics/equality.ml index be175937b..64b56b99b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -177,7 +177,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = w_unify_to_subterm_all ~flags env eqclause.evd - ((if l2r then c1 else c2),concl) + (EConstr.of_constr (if l2r then c1 else c2),EConstr.of_constr concl) in List.map try_occ occs let instantiate_lemma gl c ty l l2r concl = diff --git a/tactics/inv.ml b/tactics/inv.ml index 9282af759..9324d8e37 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -90,8 +90,8 @@ let make_inv_predicate env evd indf realargs id status concl = let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in let p = make_arity env true indf sort in let evd',(p,ptyp) = Unification.abstract_list_all env - !evd p concl (realargs@[mkVar id]) - in evd := evd'; p in + !evd (EConstr.of_constr p) (EConstr.of_constr concl) (List.map EConstr.of_constr realargs@[EConstr.mkVar id]) + in evd := evd'; EConstr.Unsafe.to_constr p in let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in (* We lift to make room for the equations *) (hyps,lift nrealargs bodypred) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3bb285aa8..2cb9e0864 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1204,10 +1204,12 @@ let map_destruction_arg f sigma = function let finish_delayed_evar_resolution with_evars env sigma f = let ((c, lbind), sigma') = run_delayed env sigma f in + let c = EConstr.of_constr c in let pending = (sigma,sigma') in let sigma' = Sigma.Unsafe.of_evar_map sigma' in let flags = tactic_infer_flags with_evars in let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (pending,c) in + let c = EConstr.Unsafe.to_constr c in (Sigma.to_evar_map sigma', (c, lbind)) let with_no_bindings (c, lbind) = @@ -2692,14 +2694,18 @@ let letin_tac with_eq id c ty occs = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let ccl = Proofview.Goal.concl gl in - let abs = AbstractExact (id,c,ty,occs,true) in + let c = EConstr.of_constr c in + let abs = AbstractExact (id,c,Option.map EConstr.of_constr ty,occs,true) in + let ccl = EConstr.of_constr ccl in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in + let ccl = EConstr.Unsafe.to_constr ccl in (* We keep the original term to match but record the potential side-effects of unifying universes. *) let Sigma (c, sigma, p) = match res with | None -> Sigma.here c sigma | Some (Sigma (_, sigma, p)) -> Sigma (c, sigma, p) in + let c = EConstr.Unsafe.to_constr c in let tac = letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty in Sigma (tac, sigma, p) end } @@ -2711,10 +2717,13 @@ let letin_pat_tac with_eq id c occs = let ccl = Proofview.Goal.concl gl in let check t = true in let abs = AbstractPattern (false,check,id,c,occs,false) in + let ccl = EConstr.of_constr ccl in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in + let ccl = EConstr.Unsafe.to_constr ccl in let Sigma (c, sigma, p) = match res with | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c | Some res -> res in + let c = EConstr.Unsafe.to_constr c in let tac = (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None) in @@ -4263,8 +4272,8 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ = if must_be_closed && occur_meta indclause.evd (EConstr.of_constr (clenv_value indclause)) then error "Need a fully applied argument."; (* We lose the possibility of coercions in with-bindings *) - let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in - Sigma.Unsafe.of_pair (c, sigma) + let (sigma, c) = pose_all_metas_as_evars env indclause.evd (EConstr.of_constr (clenv_value indclause)) in + Sigma.Unsafe.of_pair (EConstr.Unsafe.to_constr c, sigma) with e when catchable_exception e -> try find_clause (try_red_product env sigma (EConstr.of_constr typ)) with Redelimination -> raise e in @@ -4279,7 +4288,7 @@ let check_expected_type env sigma (elimc,bl) elimt = let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in let sigma = solve_evar_clause env sigma true cl bl in let (_,u,_) = destProd cl.cl_concl in - fun t -> Evarconv.e_cumul env (ref sigma) (EConstr.of_constr t) (EConstr.of_constr u) + fun t -> Evarconv.e_cumul env (ref sigma) t (EConstr.of_constr u) let check_enough_applied env sigma elim = let sigma = Sigma.to_evar_map sigma in @@ -4288,7 +4297,7 @@ let check_enough_applied env sigma elim = | None -> (* No eliminator given *) fun u -> - let t,_ = decompose_app (whd_all env sigma (EConstr.of_constr u)) in isInd t + let t,_ = decompose_app (whd_all env sigma u) in isInd t | Some elimc -> let elimt = Retyping.get_type_of env sigma (EConstr.of_constr (fst elimc)) in let scheme = compute_elim_sig ~elimc elimt in @@ -4314,8 +4323,11 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim let store = Proofview.Goal.extra gl in let check = check_enough_applied env sigma elim in let Sigma (c, sigma', p) = use_bindings env sigma elim false (c0,lbind) t0 in + let c = EConstr.of_constr c in let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in + let ccl = EConstr.of_constr ccl in let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in + let ccl = EConstr.Unsafe.to_constr ccl in match res with | None -> (* pattern not found *) @@ -4323,7 +4335,9 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim (* we restart using bindings after having tried type-class resolution etc. on the term given by the user *) let flags = tactic_infer_flags (with_evars && (* do not give a success semantics to edestruct on an open term yet *) false) in + let c0 = EConstr.of_constr c0 in let Sigma (c0, sigma, q) = finish_evar_resolution ~flags env sigma (pending,c0) in + let c0 = EConstr.Unsafe.to_constr c0 in let tac = (if isrec then (* Historically, induction has side conditions last *) @@ -4350,6 +4364,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim Sigma (tac, sigma, q) | Some (Sigma (c, sigma', q)) -> + let c = EConstr.Unsafe.to_constr c in (* pattern found *) let with_eq = Option.map (fun eq -> (false,eq)) eqname in (* TODO: if ind has predicate parameters, use JMeq instead of eq *) @@ -4386,7 +4401,7 @@ let induction_gen clear_flag isrec with_evars elim && lbind == NoBindings && not with_evars && Option.is_empty eqname && clear_flag == None && has_generic_occurrences_but_goal cls (destVar c) env (Sigma.to_evar_map sigma) ccl in - let enough_applied = check_enough_applied env sigma elim t in + let enough_applied = check_enough_applied env sigma elim (EConstr.of_constr t) in if is_arg_pure_hyp && enough_applied then (* First case: induction on a variable already in an inductive type and with maximal abstraction over the variable. @@ -4935,6 +4950,8 @@ let tclABSTRACT name_op tac = abstract_subproof s gk tac let unify ?(state=full_transparent_state) x y = + let x = EConstr.of_constr x in + let y = EConstr.of_constr y in Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in try diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 345eae9df..20cda947a 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -272,7 +272,7 @@ let explain_ill_formed_branch env sigma c ci actty expty = let explain_generalization env sigma (name,var) j = let pe = pr_ne_context_of (str "In environment") env sigma in let pv = pr_ltype_env env sigma var in - let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) sigma j in + let (pc,pt) = pr_ljudge_env (push_rel_assum (name,EConstr.of_constr var) env) sigma j in pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++ str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++ str "it has type" ++ spc () ++ pt ++ @@ -529,7 +529,7 @@ let explain_cant_find_case_type env sigma c = pe ++ str "." let explain_occur_check env sigma ev rhs = - let rhs = Evarutil.nf_evar sigma rhs in + let rhs = EConstr.to_constr sigma rhs in let env = make_all_name_different env in let pt = pr_lconstr_env env sigma rhs in str "Cannot define " ++ pr_existential_key sigma ev ++ str " with term" ++ @@ -637,6 +637,9 @@ let explain_cannot_unify env sigma m n e = str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "." let explain_cannot_unify_local env sigma m n subn = + let m = EConstr.to_constr sigma m in + let n = EConstr.to_constr sigma n in + let subn = EConstr.to_constr sigma subn in let pm = pr_lconstr_env env sigma m in let pn = pr_lconstr_env env sigma n in let psubn = pr_lconstr_env env sigma subn in @@ -649,6 +652,7 @@ let explain_refiner_cannot_generalize env sigma ty = pr_lconstr_env env sigma ty ++ str "." let explain_no_occurrence_found env sigma c id = + let c = EConstr.to_constr sigma c in str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++ str " in " ++ (match id with @@ -662,6 +666,7 @@ let explain_cannot_unify_binding_type env sigma m n = str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "." let explain_cannot_find_well_typed_abstraction env sigma p l e = + let p = EConstr.to_constr sigma p in str "Abstracting over the " ++ str (String.plural (List.length l) "term") ++ spc () ++ hov 0 (pr_enum (fun c -> pr_lconstr_env env sigma (EConstr.to_constr sigma c)) l) ++ spc () ++ @@ -670,6 +675,9 @@ let explain_cannot_find_well_typed_abstraction env sigma p l e = (match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e) let explain_wrong_abstraction_type env sigma na abs expected result = + let abs = EConstr.to_constr sigma abs in + let expected = EConstr.to_constr sigma expected in + let result = EConstr.to_constr sigma result in let ppname = match na with Name id -> pr_id id ++ spc () | _ -> mt () in str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++ pr_lconstr_env env sigma expected ++ strbrk " with abstraction " ++ @@ -681,6 +689,7 @@ let explain_abstraction_over_meta _ m n = pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "." let explain_non_linear_unification env sigma m t = + let t = EConstr.to_constr sigma t in strbrk "Cannot unambiguously instantiate " ++ pr_name m ++ str ":" ++ strbrk " which would require to abstract twice on " ++ @@ -742,7 +751,13 @@ let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1 str "Found nested occurrences of the pattern at positions " ++ int pos1 ++ strbrk " and " ++ pr_position (cl2,pos2) ++ str "." else - let ppreason = match e with None -> mt() | Some (c1,c2,e) -> explain_unification_error env sigma c1 c2 (Some e) in + let ppreason = match e with + | None -> mt() + | Some (c1,c2,e) -> + let c1 = EConstr.to_constr sigma c1 in + let c2 = EConstr.to_constr sigma c2 in + explain_unification_error env sigma c1 c2 (Some e) + in str "Found incompatible occurrences of the pattern" ++ str ":" ++ spc () ++ str "Matched term " ++ pr_lconstr_env env sigma (EConstr.to_constr sigma t2) ++ strbrk " at position " ++ pr_position (cl2,pos2) ++ @@ -819,6 +834,8 @@ let explain_pretype_error env sigma err = explain_unexpected_type env sigma actual expect | NotProduct c -> explain_not_product env sigma c | CannotUnify (m,n,e) -> + let m = EConstr.Unsafe.to_constr m in + let n = EConstr.Unsafe.to_constr n in let env, m, n = contract2 env m n in explain_cannot_unify env sigma m n e | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn |