diff options
-rw-r--r-- | contrib/fourier/fourierR.ml | 2 | ||||
-rw-r--r-- | contrib/jprover/jprover.ml4 | 2 | ||||
-rw-r--r-- | contrib/omega/coq_omega.ml | 2 | ||||
-rw-r--r-- | pretyping/clenv.ml | 126 | ||||
-rw-r--r-- | pretyping/clenv.mli | 35 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 98 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 30 | ||||
-rw-r--r-- | pretyping/evd.ml | 3 | ||||
-rw-r--r-- | pretyping/evd.mli | 4 | ||||
-rw-r--r-- | pretyping/pretyping.mli | 4 | ||||
-rw-r--r-- | pretyping/unification.ml | 74 | ||||
-rw-r--r-- | pretyping/unification.mli | 12 | ||||
-rw-r--r-- | proofs/clenvtac.ml | 26 | ||||
-rw-r--r-- | proofs/clenvtac.mli | 4 | ||||
-rw-r--r-- | tactics/auto.ml | 2 | ||||
-rw-r--r-- | tactics/equality.ml | 6 | ||||
-rw-r--r-- | tactics/evar_tactics.ml | 6 | ||||
-rw-r--r-- | tactics/inv.ml | 2 | ||||
-rw-r--r-- | tactics/leminv.ml | 2 | ||||
-rw-r--r-- | tactics/refine.ml | 4 | ||||
-rw-r--r-- | tactics/refine.mli | 3 | ||||
-rw-r--r-- | tactics/setoid_replace.ml | 10 | ||||
-rw-r--r-- | tactics/tactics.ml | 22 | ||||
-rw-r--r-- | tactics/tactics.mli | 4 |
24 files changed, 242 insertions, 241 deletions
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 695388130..de7d0b133 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -408,7 +408,7 @@ let tac_zero_infeq_false gl (n,d) = (tac_zero_inf_pos gl (-n,d))) ;; -let create_meta () = mkMeta(new_meta());; +let create_meta () = mkMeta(Evarutil.new_meta());; let my_cut c gl= let concl = pf_concl gl in diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4 index dd76438f6..8de7f37d3 100644 --- a/contrib/jprover/jprover.ml4 +++ b/contrib/jprover/jprover.ml4 @@ -361,7 +361,7 @@ let dyn_impl id gl = (TCL.tclTHENLAST (TCL.tclTHENS (T.cut b) [T.intro_using id2;TCL.tclIDTAC]) (T.apply_term (TR.mkVar (short_addr id)) - [TR.mkMeta (Clenv.new_meta())])) gl + [TR.mkMeta (Evarutil.new_meta())])) gl let dyn_allr c = (* [c] must be an eigenvariable which replaces [v] *) HT.h_intro (N.id_of_string c) diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index ad910b029..86c064098 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -567,7 +567,7 @@ let rec decompile af = in loop af.body -let mkNewMeta () = mkMeta (Clenv.new_meta()) +let mkNewMeta () = mkMeta (Evarutil.new_meta()) let clever_rewrite_base_poly typ p result theorem gl = let full = pf_concl gl in diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 45ead5a9f..5b4ed6571 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -27,65 +27,47 @@ open Evarutil open Unification (* *) -let w_coerce wc c ctyp target = +let w_coerce env c ctyp target evd = let j = make_judge c ctyp in - let env = Global.env_of_context wc.it in - let isevars = create_evar_defs wc.sigma in - let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in - (evars_of evd',j'.uj_val) + let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env evd j target in + (evd',j'.uj_val) let pf_env gls = Global.env_of_context gls.it.evar_hyps let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c let pf_hnf_constr gls c = hnf_constr (pf_env gls) gls.sigma c let pf_concl gl = gl.it.evar_concl -(* Generator of metavariables *) -let new_meta = - let meta_ctr = ref 0 in - fun () -> incr meta_ctr; !meta_ctr - -(* replaces a mapping of existentials into a mapping of metas. - Problem if an evar appears in the type of another one (pops anomaly) *) -let exist_to_meta sigma (emap, c) = - let metamap = ref [] in - let change_exist evar = - let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in - let n = new_meta() in - metamap := (n, ty) :: !metamap; - mkMeta n in - let rec replace c = - match kind_of_term c with - Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev - | _ -> map_constr replace c in - (!metamap, replace c) - (******************************************************************) (* Clausal environments *) -type wc = named_context sigma - type clausenv = { + templenv : env; + env : evar_defs; templval : constr freelisted; templtyp : constr freelisted; - namenv : identifier Metamap.t; - env : meta_map; - hook : wc } + namenv : identifier Metamap.t } + +let cl_env ce = ce.templenv +let cl_metas ce = metas_of ce.env +let cl_sigma ce = evars_of ce.env -let subst_clenv f sub clenv = +let subst_clenv sub clenv = { templval = map_fl (subst_mps sub) clenv.templval; templtyp = map_fl (subst_mps sub) clenv.templtyp; namenv = clenv.namenv; - env = Metamap.map (map_clb (subst_mps sub)) clenv.env; - hook = f sub clenv.hook } + env = reset_evd + (evars_of clenv.env, + Metamap.map (map_clb (subst_mps sub)) (cl_metas clenv)) + clenv.env; + templenv = clenv.templenv } -let clenv_nf_meta clenv c = nf_meta clenv.env c -let clenv_meta_type clenv mv = meta_type clenv.env mv -let clenv_value clenv = meta_instance clenv.env clenv.templval -let clenv_type clenv = meta_instance clenv.env clenv.templtyp +let clenv_nf_meta clenv c = nf_meta (cl_metas clenv) c +let clenv_meta_type clenv mv = meta_type (cl_metas clenv) mv +let clenv_value clenv = meta_instance (cl_metas clenv) clenv.templval +let clenv_type clenv = meta_instance (cl_metas clenv) clenv.templtyp -let cl_env ce = Global.env_of_context ce.hook.it -let clenv_hnf_constr ce t = hnf_constr (cl_env ce) ce.hook.sigma t +let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t let clenv_get_type_of ce c = let metamap = @@ -93,8 +75,8 @@ let clenv_get_type_of ce c = (function | (n,Clval(_,typ)) -> (n,typ.rebus) | (n,Cltyp typ) -> (n,typ.rebus)) - (metamap_to_list ce.env) in - Retyping.get_type_of_with_meta (cl_env ce) ce.hook.sigma metamap c + (metamap_to_list (cl_metas ce)) in + Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c @@ -120,7 +102,7 @@ let clenv_environments bound c = else ne in - let e' = Metamap.add mv (Cltyp (mk_freelisted c1)) e in + let e' = meta_declare mv c1 e in clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) c2) else c2) | (n, LetIn (na,b,_,c)) -> @@ -134,8 +116,8 @@ let mk_clenv_from_n gls n (c,cty) = { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); templtyp = mk_freelisted concl; namenv = namenv; - env = env; - hook = {it=gls.it.evar_hyps; sigma=gls.sigma} } + env = mk_evar_defs (gls.sigma,env); + templenv = Global.env_of_context gls.it.evar_hyps } let mk_clenv_from gls = mk_clenv_from_n gls None @@ -156,7 +138,7 @@ let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) let mentions clenv mv0 = let rec menrec mv1 = try - (match Metamap.find mv1 clenv.env with + (match Metamap.find mv1 (cl_metas clenv) with | Clval (b,_) -> Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas | Cltyp _ -> false) @@ -165,7 +147,7 @@ let mentions clenv mv0 = in menrec -let clenv_defined clenv mv = meta_defined clenv.env mv +let clenv_defined clenv mv = meta_defined (cl_metas clenv) mv (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *) let clenv_assign mv rhs clenv = @@ -173,11 +155,10 @@ let clenv_assign mv rhs clenv = if meta_exists (mentions clenv mv) rhs_fls.freemetas then error "clenv__assign: circularity in unification"; try - (match Metamap.find mv clenv.env with + (match Metamap.find mv (cl_metas clenv) with | Clval (fls,ty) -> if not (eq_constr fls.rebus rhs) then try - (* Streams are lazy, force evaluation of id to catch Not_found*) let id = Metamap.find mv clenv.namenv in errorlabstrm "clenv_assign" (str "An incompatible instantiation has already been found for " ++ @@ -187,19 +168,16 @@ let clenv_assign mv rhs clenv = else clenv | Cltyp bty -> - { templval = clenv.templval; - templtyp = clenv.templtyp; - namenv = clenv.namenv; - env = Metamap.add mv (Clval (rhs_fls,bty)) clenv.env; - hook = clenv.hook }) + { clenv with + env = reset_evd + (cl_sigma clenv, + Metamap.add mv (Clval (rhs_fls,bty)) (cl_metas clenv)) + clenv.env }) with Not_found -> error "clenv_assign" -let clenv_wtactic f clenv = - let (evd',mmap') = - f (create_evar_defs clenv.hook.sigma, clenv.env) in - {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=evars_of evd'}} +let clenv_wtactic f clenv = {clenv with env = f clenv.env } (* [clenv_dependent hyps_only clenv] @@ -225,7 +203,7 @@ let collect_metas c = * returns a list of the metavars which appear in the type of * the metavar mv. The list is unordered. *) -let clenv_metavars clenv mv = (meta_ftype clenv.env mv).freemetas +let clenv_metavars clenv mv = (meta_ftype (cl_metas clenv) mv).freemetas let dependent_metas clenv mvs conclmetas = List.fold_right @@ -247,8 +225,7 @@ let clenv_missing ce = clenv_dependent true ce (******************************************************************) let clenv_unify allow_K cv_pb t1 t2 clenv = - let env = cl_env clenv in - clenv_wtactic (w_unify allow_K env cv_pb t1 t2) clenv + { clenv with env = w_unify allow_K clenv.templenv cv_pb t1 t2 clenv.env } let clenv_unique_resolver allow_K clause gl = clenv_unify allow_K CUMUL (clenv_type clause) (pf_concl gl) clause @@ -279,8 +256,9 @@ let evar_clenv_unique_resolver clenv gls = (******************************************************************) let connect_clenv gls clenv = - let wc = {it=gls.it.evar_hyps; sigma=gls.sigma} in - { clenv with hook = wc } + { clenv with + env = evars_reset_evd gls.sigma clenv.env; + templenv = Global.env_of_context gls.it.evar_hyps } (* [clenv_fchain mv clenv clenv'] * @@ -308,9 +286,12 @@ let clenv_fchain mv clenv nextclenv = end else Metamap.add mv id ne) clenv.namenv (metamap_to_list nextclenv.namenv); - env = List.fold_left (fun m (n,v) -> Metamap.add n v m) - clenv.env (metamap_to_list nextclenv.env); - hook = nextclenv.hook } + env = reset_evd + (cl_sigma nextclenv, + List.fold_left (fun m (n,v) -> Metamap.add n v m) + (cl_metas clenv) (metamap_to_list (cl_metas nextclenv))) + nextclenv.env; + templenv = nextclenv.templenv } in (* unify the type of the template of [nextclenv] with the type of [mv] *) let clenv'' = @@ -390,11 +371,11 @@ let clenv_match_args s clause = with _ -> (* Try to coerce to the type of [k]; cannot merge with the previous case because Coercion does not handle Meta *) - let (_,c') = w_coerce clause.hook c c_typ k_typ in - try clenv_unify true CONV (mkMeta k) c' clause - with PretypeError (env,CannotUnify (m,n)) -> - Stdpp.raise_with_loc loc - (PretypeError (env,CannotUnifyBindingType (m,n))) + let (_,c') = w_coerce (cl_env clause) c c_typ k_typ clause.env in + try clenv_unify true CONV (mkMeta k) c' clause + with PretypeError (env,CannotUnify (m,n)) -> + Stdpp.raise_with_loc loc + (PretypeError (env,CannotUnifyBindingType (m,n))) in matchrec cl t in matchrec clause s @@ -435,14 +416,13 @@ let clenv_constrain_dep_args hyps_only clause = function if List.length occlist = List.length mlist then List.fold_left2 (fun clenv k c -> - let wc = clause.hook in try let k_typ = clenv_hnf_constr clause (clenv_meta_type clause k) in let c_typ = clenv_hnf_constr clause (clenv_get_type_of clause c) in (* faire quelque chose avec le sigma retourne ? *) - let (_,c') = w_coerce wc c c_typ k_typ in + let (_,c') = w_coerce (cl_env clenv) c c_typ k_typ clenv.env in clenv_unify true CONV (mkMeta k) c' clenv with _ -> clenv_unify true CONV (mkMeta k) c clenv) @@ -494,4 +474,4 @@ let pr_clenv clenv = in (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ - (prlist pr_meta_binding (metamap_to_list clenv.env))) + (prlist pr_meta_binding (metamap_to_list (cl_metas clenv)))) diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 375d84eac..30bc96338 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -13,40 +13,31 @@ open Util open Names open Term open Sign +open Environ open Evd open Evarutil (*i*) -(* [new_meta] is a generator of unique meta variables *) -val new_meta : unit -> metavariable - -(* [exist_to_meta] generates new metavariables for each existential - and performs the replacement in the given constr *) -val exist_to_meta : - evar_map -> Pretyping.open_constr -> (Termops.metamap * constr) - (***************************************************************) (* The Type of Constructions clausale environments. *) -(* [templval] is the template which we are trying to fill out. +(* [templenv] is the typing context + * [env] is the mapping from metavar and evar numbers to their types + * and values. + * [templval] is the template which we are trying to fill out. * [templtyp] is its type. * [namenv] is a mapping from metavar numbers to names, for * use in instanciating metavars by name. - * [evd] is the mapping from metavar and evar numbers to their types - * and values. - * [hook] is a signature (named_context) and a sigma: the - * typing context *) -type wc = named_context sigma (* for a better reading of the following *) type clausenv = { + templenv : env; + env : evar_defs; templval : constr freelisted; templtyp : constr freelisted; - namenv : identifier Metamap.t; - env : meta_map; - hook : wc } + namenv : identifier Metamap.t } -val subst_clenv : - (substitution -> wc -> wc) -> substitution -> clausenv -> clausenv +(* Substitution is not applied neither to the evar_map of evar_defs nor hook *) +val subst_clenv : substitution -> clausenv -> clausenv (* subject of clenv (instantiated) *) val clenv_value : clausenv -> constr @@ -118,9 +109,3 @@ val make_clenv_binding : (* Pretty-print *) val pr_clenv : clausenv -> Pp.std_ppcmds -(***************************************************************) -(* Old or unused stuff... *) - -val clenv_wtactic : - (evar_defs * meta_map -> evar_defs * meta_map) -> clausenv -> clausenv - diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 9a4c9cfed..cb4efd2e1 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -92,6 +92,63 @@ let nf_evar_info evc info = evar_body = info.evar_body} (**********************) +(* Creating new metas *) +(**********************) + +(* Generator of metavariables *) +let new_meta = + let meta_ctr = ref 0 in + fun () -> incr meta_ctr; !meta_ctr + +let mk_new_meta () = mkMeta(new_meta()) + +(* replaces a mapping of existentials into a mapping of metas. + Problem if an evar appears in the type of another one (pops anomaly) *) +let exist_to_meta sigma (emap, c) = + let metamap = ref [] in + let change_exist evar = + let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in + let n = new_meta() in + metamap := (n, ty) :: !metamap; + mkMeta n in + let rec replace c = + match kind_of_term c with + Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev + | _ -> map_constr replace c in + (!metamap, replace c) + +(*************************************) +(* Metas *) + +let meta_val_of env mv = + let rec valrec mv = + try + (match Metamap.find mv env with + | Cltyp _ -> mkMeta mv + | Clval(b,_) -> + instance (List.map (fun mv' -> (mv',valrec mv')) + (Metaset.elements b.freemetas)) b.rebus) + with Not_found -> + mkMeta mv + in + valrec mv + +let meta_instance env b = + let c_sigma = + List.map + (fun mv -> (mv,meta_val_of env mv)) (Metaset.elements b.freemetas) + in + instance c_sigma b.rebus + +let nf_meta env c = meta_instance env (mk_freelisted c) + +let meta_type env mv = + let ty = + try meta_ftype env mv + with Not_found -> error ("unknown meta ?"^string_of_int mv) in + meta_instance env ty + +(**********************) (* Creating new evars *) (**********************) @@ -216,15 +273,22 @@ let do_restrict_hyps sigma ev args = * operations on the evar constraints * *------------------------------------*) +type maps = evar_map * meta_map type evar_constraint = conv_pb * constr * constr type evar_defs = { evars : Evd.evar_map; conv_pbs : evar_constraint list; - history : (existential_key * (loc * Rawterm.hole_kind)) list } + history : (existential_key * (loc * Rawterm.hole_kind)) list; + metas : Evd.meta_map } -let create_evar_defs evd = { evars=evd; conv_pbs=[]; history=[] } +let mk_evar_defs (sigma,mmap) = + { evars=sigma; conv_pbs=[]; history=[]; metas=mmap } +let create_evar_defs sigma = + mk_evar_defs (sigma,Metamap.empty) let evars_of d = d.evars +let metas_of d = d.metas let evars_reset_evd evd d = {d with evars = evd} +let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap} let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source ev d = try List.assoc ev d.history @@ -594,33 +658,3 @@ let valcon_of_tycon x = x let lift_tycon = option_app (lift 1) -(*************************************) -(* Metas *) - -let meta_val_of env mv = - let rec valrec mv = - try - (match Metamap.find mv env with - | Cltyp _ -> mkMeta mv - | Clval(b,_) -> - instance (List.map (fun mv' -> (mv',valrec mv')) - (Metaset.elements b.freemetas)) b.rebus) - with Not_found -> - mkMeta mv - in - valrec mv - -let meta_instance env b = - let c_sigma = - List.map - (fun mv -> (mv,meta_val_of env mv)) (Metaset.elements b.freemetas) - in - instance c_sigma b.rebus - -let nf_meta env c = meta_instance env (mk_freelisted c) - -let meta_type env mv = - let ty = - try meta_ftype env mv - with Not_found -> error ("unknown meta ?"^string_of_int mv) in - meta_instance env ty diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 4223b0e78..6d264b718 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -40,19 +40,40 @@ exception Uninstantiated_evar of existential_key val whd_ise : evar_map -> constr -> constr val whd_castappevar : evar_map -> constr -> constr +(***********************************************************) +(* Metas *) + +(* [new_meta] is a generator of unique meta variables *) +val new_meta : unit -> metavariable +val mk_new_meta : unit -> constr +val nf_meta : meta_map -> constr -> constr +val meta_type : meta_map -> metavariable -> types +val meta_instance : meta_map -> constr freelisted -> constr + +(* [exist_to_meta] generates new metavariables for each existential + and performs the replacement in the given constr *) +val exist_to_meta : evar_map -> open_constr -> (Termops.metamap * constr) + (* Creating new existential variables *) val new_evar : unit -> evar val new_evar_in_sign : env -> constr val evar_env : evar_info -> env +(***********************************************************) + +type maps = evar_map * meta_map type evar_defs -val evars_of : evar_defs -> evar_map +val evars_of : evar_defs -> evar_map +val metas_of : evar_defs -> meta_map val non_instantiated : evar_map -> (evar * evar_info) list -val create_evar_defs : evar_map -> evar_defs +val mk_evar_defs : maps -> evar_defs +(* the same with empty meta map: *) +val create_evar_defs : evar_map -> evar_defs val evars_reset_evd : evar_map -> evar_defs -> evar_defs +val reset_evd : maps -> evar_defs -> evar_defs val evar_source : existential_key -> evar_defs -> loc * hole_kind type evar_constraint = conv_pb * constr * constr @@ -82,6 +103,7 @@ val solve_simple_eqn : val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts +(***********************************************************) (* Value/Type constraints *) val new_Type_sort : unit -> sorts @@ -105,7 +127,3 @@ val valcon_of_tycon : type_constraint -> val_constraint val lift_tycon : type_constraint -> type_constraint -(* Metas *) -val nf_meta : meta_map -> constr -> constr -val meta_type : meta_map -> metavariable -> types -val meta_instance : meta_map -> constr freelisted -> constr diff --git a/pretyping/evd.ml b/pretyping/evd.ml index be35cb947..d7468eded 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -118,6 +118,9 @@ let existential_opt_value sigma ev = with NotInstantiatedEvar -> None (*******************************************************************) +type open_constr = evar_map * constr + +(*******************************************************************) (* The type constructor ['a sigma] adds an evar map to an object of type ['a] *) type 'a sigma = { diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 3f9eaa5fa..df362a9bf 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -64,6 +64,10 @@ val existential_type : evar_map -> existential -> types val existential_opt_value : evar_map -> existential -> constr option (*************************) +(* constr with holes *) +type open_constr = evar_map * constr + +(*************************) (* The type constructor ['a sigma] adds an evar map to an object of type ['a] *) type 'a sigma = { diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 57a3d1be8..096c982c5 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -20,10 +20,6 @@ open Evarutil type var_map = (identifier * unsafe_judgment) list -(* constr with holes *) -type open_constr = evar_map * constr - - (* Generic call to the interpreter from rawconstr to constr, failing unresolved holes in the rawterm cannot be instantiated. diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 4a9cab206..33f09fd0a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -49,14 +49,12 @@ let abstract_list_all env sigma typ c l = (*******************************) -type maps = evar_defs * meta_map - -let w_Declare env sp ty (evd,mmap) = +let w_Declare env sp ty evd = let sigma = evars_of evd in let _ = Typing.type_of env sigma ty in (* Utile ?? *) let newdecl = { evar_hyps=named_context env; evar_concl=ty; evar_body=Evar_empty } in - (evars_reset_evd (Evd.add sigma sp newdecl) evd, mmap) + evars_reset_evd (Evd.add sigma sp newdecl) evd (* [w_Define evd sp c] * @@ -66,7 +64,7 @@ let w_Declare env sp ty (evd,mmap) = * No unification is performed in order to assert that [c] has the * correct type. *) -let w_Define sp c (evd,mmap) = +let w_Define sp c evd = let sigma = evars_of evd in if Evd.is_defined sigma sp then error "Unify.w_Define: cannot define evar twice"; @@ -82,7 +80,7 @@ let w_Define sp c (evd,mmap) = (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ str (string_of_existential sp)) in let spdecl' = { spdecl with evar_body = Evar_defined c } in - (evars_reset_evd (Evd.add sigma sp spdecl') evd, mmap) + evars_reset_evd (Evd.add sigma sp spdecl') evd (* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n] @@ -230,17 +228,17 @@ let is_mimick_head f = 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 metas evars maps = +let w_merge env with_types metas evars evd = let ty_metas = ref [] in let ty_evars = ref [] in - let rec w_merge_rec (evd,mmap as maps) metas evars = + let rec w_merge_rec evd metas evars = match (evars,metas) with - | ([], []) -> maps + | ([], []) -> evd | ((lhs,rhs)::t, metas) -> (match kind_of_term rhs with - | Meta k -> w_merge_rec maps ((k,lhs)::metas) t + | Meta k -> w_merge_rec evd ((k,lhs)::metas) t | krhs -> (match kind_of_term lhs with @@ -249,7 +247,7 @@ let w_merge env with_types metas evars maps = if is_defined_evar evd ev then let (metas',evars') = unify_0 env (evars_of evd) CONV rhs lhs in - w_merge_rec maps (metas'@metas) (evars'@t) + w_merge_rec evd (metas'@metas) (evars'@t) else begin let rhs' = if occur_meta rhs then subst_meta metas rhs else rhs @@ -259,23 +257,24 @@ let w_merge env with_types metas evars maps = match krhs with | App (f,cl) when is_mimick_head f -> (try - w_merge_rec (w_Define evn rhs' maps) metas t + w_merge_rec (w_Define evn rhs' evd) metas t with ex when precatchable_exception ex -> - let maps' = - mimick_evar maps f (Array.length cl) evn in - w_merge_rec maps' metas evars) + let evd' = + mimick_evar evd f (Array.length cl) evn in + w_merge_rec evd' metas evars) | _ -> (* ensure tail recursion in non-mimickable case! *) - w_merge_rec (w_Define evn rhs' maps) metas t + w_merge_rec (w_Define evn rhs' evd) metas t end | _ -> anomaly "w_merge_rec")) | ([], (mv,n)::t) -> + let mmap = metas_of evd in if meta_defined mmap mv then let (metas',evars') = unify_0 env (evars_of evd) CONV (meta_fvalue mmap mv).rebus n in - w_merge_rec maps (metas'@t) evars' + w_merge_rec evd (metas'@t) evars' else begin if with_types (* or occur_meta mvty *) then @@ -288,30 +287,31 @@ let w_merge env with_types metas evars maps = ty_metas := mc @ !ty_metas; ty_evars := ec @ !ty_evars with e when precatchable_exception e -> ()); - let mmap' = meta_assign mv n mmap in - w_merge_rec (evd,mmap') t [] + let evd' = + reset_evd (evars_of evd,meta_assign mv n mmap) evd in + w_merge_rec evd' t [] end - and mimick_evar (evd,mmap) hdc nargs sp = + and mimick_evar evd hdc nargs sp = let ev = Evd.map (evars_of evd) sp in let sp_env = Global.env_of_context ev.evar_hyps in let (evd', c) = applyHead sp_env evd nargs hdc in let (mc,ec) = unify_0 sp_env (evars_of evd') CUMUL (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in - let maps' = w_merge_rec (evd',mmap) mc ec in - if (evars_of evd') == (evars_of (fst maps')) - then w_Define sp c maps' - else w_Define sp (Evarutil.nf_evar (evars_of (fst maps')) c) maps' in + let evd'' = w_merge_rec evd' mc ec in + if (evars_of evd') == (evars_of evd'') + then w_Define sp c evd'' + else w_Define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in (* merge constraints *) - let maps' = w_merge_rec maps metas evars in + let evd' = w_merge_rec evd metas evars in if with_types then (* merge constraints about types: if they fail, don't worry *) - try w_merge_rec maps' !ty_metas !ty_evars - with e when precatchable_exception e -> maps' + try w_merge_rec evd' !ty_metas !ty_evars + with e when precatchable_exception e -> evd' else - maps' + evd' (* [w_unify env evd M N] performs a unification of M and N, generating a bunch of @@ -324,7 +324,7 @@ let w_merge env with_types metas evars maps = types of metavars are unifiable with the types of their instances *) let w_unify_core_0 env with_types cv_pb m n evd = - let (mc,ec) = unify_0 env (evars_of (fst evd)) cv_pb m n in + let (mc,ec) = unify_0 env (evars_of evd) cv_pb m n in w_merge env with_types mc ec evd let w_unify_0 env = w_unify_core_0 env false @@ -418,19 +418,19 @@ let w_unify_to_subterm_list env allow_K oplist t evd = with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op) in (evd',cl::l) - else if not allow_K & not (dependent op t) then - (* This is not up to delta ... *) - raise (PretypeError (env,NoOccurrenceFound op)) + else if allow_K or dependent op t then + (evd,op::l) else - (evd,op::l)) + (* This is not up to delta ... *) + raise (PretypeError (env,NoOccurrenceFound op))) oplist (evd,[]) let secondOrderAbstraction env allow_K typ (p, oplist) evd = - let sigma = evars_of (fst evd) in + let sigma = evars_of evd in let (evd',cllist) = w_unify_to_subterm_list env allow_K oplist typ evd in - let typp = meta_type (snd evd') p in + let typp = meta_type (metas_of evd') p in let pred = abstract_list_all env sigma typp typ cllist in w_unify_0 env CONV (mkMeta p) pred evd' @@ -443,13 +443,13 @@ let w_unify2 env allow_K cv_pb ty1 ty2 evd = let evd' = secondOrderAbstraction env allow_K ty2 (p1,oplist1) evd in (* Resume first order unification *) - w_unify_0 env cv_pb (nf_meta (snd evd') ty1) ty2 evd' + w_unify_0 env cv_pb (nf_meta (metas_of evd') ty1) ty2 evd' | _, Meta p2 -> (* Find the predicate *) let evd' = secondOrderAbstraction env allow_K ty1 (p2, oplist2) evd in (* Resume first order unification *) - w_unify_0 env cv_pb ty1 (nf_meta (snd evd') ty2) evd' + w_unify_0 env cv_pb ty1 (nf_meta (metas_of evd') ty2) evd' | _ -> error "w_unify2" diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 02d1918be..d3007e69d 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -18,19 +18,19 @@ open Evd open Evarutil (*i*) -type maps = evar_defs * meta_map - -val w_Declare : env -> evar -> types -> maps -> maps -val w_Define : evar -> constr -> maps -> maps +val w_Declare : env -> evar -> types -> evar_defs -> evar_defs +val w_Define : evar -> constr -> evar_defs -> evar_defs (* The "unique" unification fonction *) val w_unify : - bool -> env -> Reductionops.conv_pb -> constr -> constr -> maps -> maps + bool -> env -> Reductionops.conv_pb -> constr -> constr -> + evar_defs -> evar_defs (* [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 -> constr * constr -> maps -> maps * constr +val w_unify_to_subterm : + env -> constr * constr -> evar_defs -> evar_defs * constr (*i This should be in another module i*) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 2d972068d..aa2ff18ce 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -48,7 +48,7 @@ let clenv_cast_meta clenv = match kind_of_term (strip_outer_cast u) with | Meta mv -> (try - match Metamap.find mv clenv.env with + match Metamap.find mv (metas_of clenv.env) with | Cltyp b -> let b' = clenv_nf_meta clenv b.rebus in if occur_meta b' then u else mkCast (mkMeta mv, b') @@ -62,26 +62,14 @@ let clenv_cast_meta clenv = in crec - let clenv_refine clenv gls = tclTHEN - (tclEVARS clenv.hook.sigma) - (refine (clenv_value clenv)) gls - -let clenv_refine_cast clenv gls = - tclTHEN - (tclEVARS clenv.hook.sigma) + (tclEVARS (evars_of clenv.env)) (refine (clenv_cast_meta clenv (clenv_value clenv))) gls -let res_pf clenv gls = - clenv_refine (clenv_unique_resolver false clenv gls) gls - -let res_pf_cast clenv gls = - clenv_refine_cast (clenv_unique_resolver false clenv gls) gls - -let elim_res_pf clenv allow_K gls = - clenv_refine_cast (clenv_unique_resolver allow_K clenv gls) gls +let res_pf clenv ?(allow_K=false) gls = + clenv_refine (clenv_unique_resolver allow_K clenv gls) gls let elim_res_pf_THEN_i clenv tac gls = let clenv' = (clenv_unique_resolver true clenv gls) in @@ -102,9 +90,9 @@ let e_res_pf clenv gls = (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) let unifyTerms m n gls = let env = pf_env gls in - let maps = (create_evar_defs (project gls), Evd.Metamap.empty) in - let maps' = Unification.w_unify false env CONV m n maps in - tclIDTAC {it = gls.it; sigma = evars_of (fst maps')} + let evd = create_evar_defs (project gls) in + let evd' = Unification.w_unify false env CONV m n evd in + tclIDTAC {it = gls.it; sigma = evars_of evd'} let unify m gls = let n = pf_concl gls in unifyTerms m n gls diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index c463d75e3..cc75af0fc 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -21,8 +21,6 @@ open Proof_type (* Tactics *) val unify : constr -> tactic val clenv_refine : clausenv -> tactic -val res_pf : clausenv -> tactic -val res_pf_cast : clausenv -> tactic -val elim_res_pf : clausenv -> bool -> tactic +val res_pf : clausenv -> ?allow_K:bool -> tactic val e_res_pf : clausenv -> tactic val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic diff --git a/tactics/auto.ml b/tactics/auto.ml index 66454059e..c32130d2c 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -323,7 +323,7 @@ let forward_subst_tactic = let set_extern_subst_tactic f = forward_subst_tactic := f let subst_autohint (_,subst,(local,name,hintlist as obj)) = - let trans_clenv clenv = Clenv.subst_clenv (fun _ a -> a) subst clenv in + let trans_clenv clenv = Clenv.subst_clenv subst clenv in let trans_data data code = { data with pat = option_smartmap (subst_pattern subst) data.pat ; diff --git a/tactics/equality.ml b/tactics/equality.ml index 38dc8f58e..f9834f522 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -821,7 +821,7 @@ let swap_equands gls eqn = let swapEquandsInConcl gls = let (lbeq,(t,e1,e2)) = find_eq_data_decompose (pf_concl gls) in let sym_equal = lbeq.sym in - refine (applist(sym_equal,[t;e2;e1;mkMeta (Clenv.new_meta())])) gls + refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls let swapEquandsInHyp id gls = ((tclTHENS (cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id))) @@ -880,8 +880,8 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls = else (build_non_dependent_rewrite_predicate (t,e1,e2) body gls) in - refine (applist(eq_elim,[t;e1;p;mkMeta(Clenv.new_meta()); - e2;mkMeta(Clenv.new_meta())])) gls + refine (applist(eq_elim,[t;e1;p;Evarutil.mk_new_meta(); + e2;Evarutil.mk_new_meta()])) gls (* [subst_tuple_term dep_pair B] diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index b5a0370c7..f2db79d1a 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -67,7 +67,7 @@ let instantiate_tac = function let let_evar nam typ gls = let sp = Evarutil.new_evar () in - let mm = (Evarutil.create_evar_defs gls.sigma, Metamap.empty) in - let (evd,_) = Unification.w_Declare (pf_env gls) sp typ mm in - let ngls = {gls with sigma = Evarutil.evars_of evd} in + let evd = Evarutil.create_evar_defs gls.sigma in + let evd' = Unification.w_Declare (pf_env gls) sp typ evd in + let ngls = {gls with sigma = Evarutil.evars_of evd'} in Tactics.forward true nam (mkEvar(sp,[||])) ngls diff --git a/tactics/inv.ml b/tactics/inv.ml index 0ac120327..1e4267421 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -475,7 +475,7 @@ let raw_inversion inv_kind indbinding id status names gl = (fun id -> (tclTHEN (apply_term (mkVar id) - (list_tabulate (fun _ -> mkMeta(Clenv.new_meta())) neqns)) + (list_tabulate (fun _ -> Evarutil.mk_new_meta()) neqns)) reflexivity))]) gl diff --git a/tactics/leminv.ml b/tactics/leminv.ml index aa980fd47..9fd54ee69 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -289,7 +289,7 @@ let lemInv id c gls = try let clause = mk_clenv_type_of gls c in let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in - Clenvtac.elim_res_pf clause true gls + Clenvtac.res_pf clause ~allow_K:true gls with | UserError (a,b) -> errorlabstrm "LemInv" diff --git a/tactics/refine.ml b/tactics/refine.ml index aa9cf2c57..88e2fcea8 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -92,7 +92,7 @@ and pp_sg sg = let replace_by_meta env gmm = function | TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp | (TH (c,mm,_)) as th -> - let n = Clenv.new_meta() in + let n = Evarutil.new_meta() in let m = mkMeta n in (* quand on introduit une mv on calcule son type *) let ty = match kind_of_term c with @@ -340,7 +340,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl = let refine oc gl = let sigma = project gl in let env = pf_env gl in - let (gmm,c) = Clenv.exist_to_meta sigma oc in + let (gmm,c) = Evarutil.exist_to_meta sigma oc in let th = compute_metamap env gmm c in tcc_aux [] th gl diff --git a/tactics/refine.mli b/tactics/refine.mli index 26cd04ef0..89e531675 100644 --- a/tactics/refine.mli +++ b/tactics/refine.mli @@ -8,7 +8,6 @@ (*i $Id$ i*) -open Term open Tacmach -val refine : Pretyping.open_constr -> tactic +val refine : Evd.open_constr -> tactic diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 905ca60b4..853b4e295 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -22,6 +22,8 @@ open Util open Pp open Printer open Environ +open Clenv +open Unification open Tactics open Tacticals open Vernacexpr @@ -919,7 +921,7 @@ let syntactic_but_representation_of_marked_but hole_relation = else let c_is_proper = let typ = mkApp (rel_out, [| c ; c |]) in - mkCast (mkMeta (Clenv.new_meta ()),typ) + mkCast (Evarutil.mk_new_meta (),typ) in mkApp ((Lazy.force coq_ProperElementToKeep), [| hole_relation ; Lazy.force coq_Left2Right; precise_out ; @@ -958,9 +960,7 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl = let but = pf_concl gl in let (hyp,c1,c2) = let cl' = - Clenv.clenv_wtactic - (fun evd-> fst (Unification.w_unify_to_subterm (pf_env gl) (c1,but) evd)) - cl in + {cl with env = fst (w_unify_to_subterm (pf_env gl) (c1,but) cl.env)} in let c1 = Clenv.clenv_nf_meta cl' c1 in let c2 = Clenv.clenv_nf_meta cl' c2 in (lft2rgt,Clenv.clenv_value cl'), c1, c2 @@ -974,7 +974,7 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl = let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in let th' = mkApp ((Lazy.force coq_proj2), [|impl1; impl2; th|]) in Tactics.refine - (mkApp (th', [| mkCast (mkMeta (Clenv.new_meta()), hyp1) |])) gl + (mkApp (th', [| mkCast (Evarutil.mk_new_meta(), hyp1) |])) gl let general_s_rewrite lft2rgt c gl = let ctype = pf_type_of gl c in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 57804f23a..e6b2f76ec 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -40,6 +40,7 @@ open Nametab open Genarg open Tacexpr open Decl_kinds +open Evarutil exception Bound @@ -421,7 +422,7 @@ let rec intros_rmove = function * of the type of a term. *) let apply_type hdcty argl gl = - refine (applist (mkCast (mkMeta (new_meta()),hdcty),argl)) gl + refine (applist (mkCast (Evarutil.mk_new_meta(),hdcty),argl)) gl let apply_term hdc argl gl = refine (applist (hdc,argl)) gl @@ -431,17 +432,12 @@ let bring_hyps hyps = else (fun gl -> let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in - let f = mkCast (mkMeta (new_meta()),newcl) in + let f = mkCast (Evarutil.mk_new_meta(),newcl) in refine_no_check (mkApp (f, instance_from_named_context hyps)) gl) (* Resolution with missing arguments *) let apply_with_bindings (c,lbind) gl = - let apply = - match kind_of_term c with - | Lambda _ -> Clenvtac.res_pf_cast - | _ -> Clenvtac.res_pf - in (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) @@ -451,7 +447,7 @@ let apply_with_bindings (c,lbind) gl = let n = nb_prod thm_ty - nb_prod (pf_concl gl) in if n<0 then error "Apply: theorem has not enough premisses."; let clause = make_clenv_binding_apply gl n (c,thm_ty) lbind in - apply clause gl + Clenvtac.res_pf clause gl with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn -> let red_thm = try red_product (pf_env gl) (project gl) thm_ty @@ -462,7 +458,7 @@ let apply_with_bindings (c,lbind) gl = (* Last chance: if the head is a variable, apply may try second order unification *) let clause = make_clenv_binding_apply gl (-1) (c,thm_ty0) lbind in - apply clause gl + Clenvtac.res_pf clause gl let apply c = apply_with_bindings (c,NoBindings) @@ -838,7 +834,7 @@ let new_hyp mopt (c,lbind) g = | Some m -> if m < nargs then list_firstn m tstack else tstack | None -> tstack) in - (tclTHENLAST (tclTHEN (tclEVARS clause.hook.sigma) + (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.env)) (cut (pf_type_of g cut_pf))) ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g @@ -905,7 +901,7 @@ let elimination_clause_scheme elimclause indclause allow_K gl = (str "The type of elimination clause is not well-formed")) in let elimclause' = clenv_fchain indmv elimclause indclause in - elim_res_pf elimclause' allow_K gl + res_pf elimclause' ~allow_K:allow_K gl (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and * refine fails *) @@ -986,7 +982,7 @@ let elimination_in_clause_scheme id elimclause indclause gl = errorlabstrm "general_rewrite_in" (str "Nothing to rewrite in " ++ pr_id id); tclTHEN - (tclEVARS elimclause''.hook.sigma) + (tclEVARS (evars_of elimclause''.env)) (tclTHENS (cut new_hyp_typ) [ (* Try to insert the new hyp at the same place *) @@ -1667,7 +1663,7 @@ let elim_scheme_type elim t gl = let clause' = (* t is inductive, then CUMUL or CONV is irrelevant *) clenv_unify true CUMUL t (clenv_meta_type clause mv) clause in - elim_res_pf clause' true gl + res_pf clause' ~allow_K:true gl | _ -> anomaly "elim_scheme_type" let elim_type t gl = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index d2a16dc8e..cbc690c92 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -164,8 +164,8 @@ val cut_and_apply : constr -> tactic (*s Elimination tactics. *) -val general_elim : constr with_bindings -> constr with_bindings -> - ?allow_K:bool -> tactic +val general_elim : + constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic val default_elim : constr with_bindings -> tactic val simplest_elim : constr -> tactic val elim : constr with_bindings -> constr with_bindings option -> tactic |