From bfc3e8cddd58cadc1bc907914a2ccd660be53912 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 11 Oct 2011 19:18:02 +0000 Subject: Moved to a more standard order of arguments (i.e. env followed by evar_map) for the functions of unification.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14547 85f007b7-540e-0410-9357-904b9bb8a0f7 --- dev/doc/changes.txt | 2 ++ plugins/decl_mode/decl_proof_instr.ml | 4 ++-- pretyping/unification.ml | 42 +++++++++++++++++------------------ pretyping/unification.mli | 6 ++--- proofs/clenv.ml | 2 +- proofs/clenvtac.ml | 2 +- tactics/autorewrite.ml | 2 +- tactics/equality.ml | 4 ++-- tactics/rewrite.ml4 | 6 ++--- tactics/tactics.ml | 4 ++-- 10 files changed, 38 insertions(+), 36 deletions(-) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 035b3ad24..322530e62 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,8 @@ = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = ========================================= +** Functions in unification.ml have now the evar_map coming just after the env + ** Removal of Tacinterp.constr_of_id ** Use instead either global_reference or construct_reference in constrintern.ml. diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 217a8fe4f..6bcda0097 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -370,8 +370,8 @@ let find_subsubgoal c ctyp skip submetas gls = let se = Stack.pop stack in try let unifier = - Unification.w_unify env Reduction.CUMUL ~flags:Unification.elim_flags - ctyp se.se_type se.se_evd in + Unification.w_unify env se.se_evd Reduction.CUMUL + ~flags:Unification.elim_flags ctyp se.se_type in if n <= 0 then {se with se_evd=meta_assign se.se_meta diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f1fdde390..01d75233b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -927,7 +927,7 @@ let try_resolve_typeclasses env evd flags m n = error_cannot_unify env evd (m, n) else evd -let w_unify_core_0 env with_types cv_pb flags m n evd = +let w_unify_core_0 env evd with_types cv_pb flags m n = let (mc1,evd') = retract_coercible_metas evd in let (sigma,ms,es) = check_types env flags (evd,mc1,[]) m n in let subst2 = @@ -936,10 +936,10 @@ let w_unify_core_0 env with_types cv_pb flags m n evd = let evd = w_merge env with_types flags subst2 in try_resolve_typeclasses env evd flags m n -let w_unify_0 env = w_unify_core_0 env false -let w_typed_unify env = w_unify_core_0 env true +let w_unify_0 env evd = w_unify_core_0 env evd false +let w_typed_unify env evd = w_unify_core_0 env evd true -let w_typed_unify_list env flags f1 l1 f2 l2 evd = +let w_typed_unify_list env evd flags f1 l1 f2 l2 = let flags' = { flags with resolve_evars = false } in let f1,l1,f2,l2 = adjust_app_list_size f1 l1 f2 l2 in let (mc1,evd') = retract_coercible_metas evd in @@ -966,12 +966,12 @@ let iter_fail f a = (* Tries to find an instance of term [cl] in term [op]. Unifies [cl] to every subterm of [op] until it finds a match. Fails if no match is found *) -let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd = +let w_unify_to_subterm env evd ?(flags=default_unify_flags) (op,cl) = let rec matchrec cl = let cl = strip_outer_cast cl in (try if closed0 cl && not (isEvar cl) - then w_typed_unify env CONV flags op cl evd,cl + then w_typed_unify env evd CONV flags op cl,cl else error "Bound 1" with ex when precatchable_exception ex -> (match kind_of_term cl with @@ -1026,7 +1026,7 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd = (* Tries to find all instances of term [cl] in term [op]. 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 ?(flags=default_unify_flags) (op,cl) evd = +let w_unify_to_subterm_all env evd ?(flags=default_unify_flags) (op,cl) = let return a b = let (evd,c as a) = a () in if List.exists (fun (evd',c') -> eq_constr c c') b then b else a :: b @@ -1051,7 +1051,7 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd = let cl = strip_outer_cast cl in (bind (if closed0 cl - then return (fun () -> w_typed_unify env CONV flags op cl 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 | App (f,args) -> @@ -1087,7 +1087,7 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd = else res -let w_unify_to_subterm_list env flags hdmeta oplist t evd = +let w_unify_to_subterm_list env evd flags hdmeta oplist t = List.fold_right (fun op (evd,l) -> let op = whd_meta evd op in @@ -1098,7 +1098,7 @@ let w_unify_to_subterm_list env flags hdmeta oplist t evd = let (evd',cl) = try (* This is up to delta for subterms w/o metas ... *) - w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd + w_unify_to_subterm env evd ~flags (strip_outer_cast op,t) with PretypeError (env,_,NoOccurrenceFound _) when flags.allow_K_in_toplevel_higher_order_unification -> (evd,op) in @@ -1116,24 +1116,24 @@ let w_unify_to_subterm_list env flags hdmeta oplist t evd = oplist (evd,[]) -let secondOrderAbstraction env flags typ (p, oplist) evd = +let secondOrderAbstraction env evd flags typ (p, oplist) = (* Remove delta when looking for a subterm *) let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in - let (evd',cllist) = w_unify_to_subterm_list env flags p oplist typ evd 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 pred = abstract_list_all env evd' typp typ cllist in w_merge env false flags (evd',[p,pred,(Conv,TypeProcessed)],[]) -let w_unify2 env flags cv_pb ty1 ty2 evd = +let w_unify2 env evd flags cv_pb ty1 ty2 = let c1, oplist1 = whd_stack evd ty1 in let c2, oplist2 = whd_stack evd ty2 in match kind_of_term c1, kind_of_term c2 with | Meta p1, _ -> (* Find the predicate *) - secondOrderAbstraction env flags ty2 (p1,oplist1) evd + secondOrderAbstraction env evd flags ty2 (p1,oplist1) | _, Meta p2 -> (* Find the predicate *) - secondOrderAbstraction env flags ty1 (p2, oplist2) evd + secondOrderAbstraction env evd flags ty1 (p2, oplist2) | _ -> error "w_unify2" (* The unique unification algorithm works like this: If the pattern is @@ -1156,7 +1156,7 @@ let w_unify2 env flags cv_pb ty1 ty2 evd = Before, second-order was used if the type of Meta(1) and [x:A]t was 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 cv_pb ?(flags=default_unify_flags) ty1 ty2 evd = +let w_unify env evd cv_pb ?(flags=default_unify_flags) ty1 ty2 = let hd1,l1 = whd_stack evd ty1 in let hd2,l2 = whd_stack evd ty2 in match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with @@ -1164,22 +1164,22 @@ let w_unify env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd = | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) when List.length l1 = List.length l2 -> (try - w_typed_unify_list env flags hd1 l1 hd2 l2 evd + w_typed_unify_list env evd flags hd1 l1 hd2 l2 with ex when precatchable_exception ex -> try - w_unify2 env flags cv_pb ty1 ty2 evd + w_unify2 env evd flags cv_pb ty1 ty2 with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e) (* Second order case *) | (Meta _, true, _, _ | _, _, Meta _, true) -> (try - w_unify2 env flags cv_pb ty1 ty2 evd + w_unify2 env evd flags cv_pb ty1 ty2 with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e | ex when precatchable_exception ex -> try - w_typed_unify_list env flags hd1 l1 hd2 l2 evd + w_typed_unify_list env evd flags hd1 l1 hd2 l2 with ex' when precatchable_exception ex' -> raise ex) (* General case: try first order *) - | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd + | _ -> w_typed_unify env evd cv_pb flags ty1 ty2 diff --git a/pretyping/unification.mli b/pretyping/unification.mli index cc781c871..d28451177 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -33,16 +33,16 @@ val elim_no_delta_flags : unify_flags (** The "unique" unification fonction *) val w_unify : - env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -> evar_map + env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map (** [w_unify_to_subterm env (c,t) m] performs unification of [c] with a subterm of [t]. Constraints are added to [m] and the matched subterm of [t] is also returned. *) val w_unify_to_subterm : - env -> ?flags:unify_flags -> constr * constr -> evar_map -> evar_map * constr + env -> evar_map -> ?flags:unify_flags -> constr * constr -> evar_map * constr val w_unify_to_subterm_all : - env -> ?flags:unify_flags -> constr * constr -> evar_map -> (evar_map * constr) list + env -> evar_map -> ?flags:unify_flags -> constr * constr -> (evar_map * constr) list val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 6e6fff96d..d06c6f2e6 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -267,7 +267,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 cv_pb t1 t2 clenv.evd } + evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 } let clenv_unify_meta_types ?(flags=default_unify_flags) clenv = { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ec9aada73..ff84a343b 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -119,7 +119,7 @@ let fail_quick_unif_flags = { let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in - let evd' = w_unify env CONV ~flags m n evd in + let evd' = w_unify env evd CONV ~flags m n in tclIDTAC {it = gls.it; sigma = evd'} let unify ?(flags=fail_quick_unif_flags) m gls = diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 8ccf751c4..13f8784f5 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -246,7 +246,7 @@ type hypinfo = { let evd_convertible env evd x y = try - ignore(Unification.w_unify ~flags:Unification.elim_flags env Reduction.CONV x y evd); true + ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true (* try ignore(Evarconv.the_conv_x env x y evd); true *) with _ -> false diff --git a/tactics/equality.ml b/tactics/equality.ml index d21d3e767..2d4268e60 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -131,8 +131,8 @@ let instantiate_lemma_all frzevars env sigma gl c ty l l2r concl = in let flags = make_flags frzevars sigma rewrite_unif_flags eqclause in let occs = - Unification.w_unify_to_subterm_all ~flags env - ((if l2r then c1 else c2),concl) eqclause.evd + Unification.w_unify_to_subterm_all ~flags env eqclause.evd + ((if l2r then c1 else c2),concl) in List.map try_occ occs let instantiate_lemma env sigma gl c ty l l2r concl = diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index c908f7188..1595ded2d 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1021,7 +1021,7 @@ module Strategies = with _ -> error "fold: the term is not unfoldable !" in try - let sigma = Unification.w_unify env CONV ~flags:Unification.elim_flags unfolded t sigma in + let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in let c' = Evarutil.nf_evar sigma c in Some (Some { rew_car = ty; rew_from = t; rew_to = c'; rew_prf = RewCast DEFAULTcast; @@ -1771,13 +1771,13 @@ let unification_rewrite flags l2r c1 c2 cl car rel but gl = (* ~flags:(false,true) to allow to mark occurrences that must not be rewritten simply by replacing them with let-defined definitions in the context *) - Unification.w_unify_to_subterm ~flags:rewrite_unif_flags env ((if l2r then c1 else c2),but) cl.evd + Unification.w_unify_to_subterm ~flags:rewrite_unif_flags env cl.evd ((if l2r then c1 else c2),but) with Pretype_errors.PretypeError _ -> (* ~flags:(true,true) to make Ring work (since it really exploits conversion) *) Unification.w_unify_to_subterm ~flags:flags - env ((if l2r then c1 else c2),but) cl.evd + env cl.evd ((if l2r then c1 else c2),but) in let evd' = Typeclasses.resolve_typeclasses ~fail:false env evd' in let cl' = {cl with evd = evd'} in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2f0eaf82e..692622f32 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1704,7 +1704,7 @@ let default_matching_flags sigma = { let make_pattern_test env sigma0 (sigma,c) = let flags = default_matching_flags sigma0 in let matching_fun t = - try let sigma = w_unify env Reduction.CONV ~flags c t sigma in Some(sigma,t) + try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma,t) with _ -> raise NotUnifiable in let merge_fun c1 c2 = match c1, c2 with @@ -3531,6 +3531,6 @@ let unify ?(state=full_transparent_state) x y gl = modulo_delta = state; modulo_conv_on_closed_terms = Some state} in - let evd = w_unify (pf_env gl) Reduction.CONV ~flags x y (project gl) + let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y in tclEVARS evd gl with _ -> tclFAIL 0 (str"Not unifiable") gl -- cgit v1.2.3