From 16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Dec 2013 15:08:06 +0100 Subject: Removing the need of evarmaps in constr internalization. Actually, this was wrong, as evars should not appear until interpretation. Evarmaps were only passed around uselessly, and often fed with dummy or irrelevant values. --- interp/constrintern.ml | 39 +++++++++++++++++------------------ interp/constrintern.mli | 10 ++++----- interp/genintern.ml | 1 - interp/genintern.mli | 1 - plugins/decl_mode/decl_proof_instr.ml | 3 +-- plugins/funind/indfun.ml | 2 +- plugins/funind/merge.ml | 2 +- proofs/evar_refiner.ml | 2 +- tactics/auto.ml | 2 +- tactics/tacintern.ml | 14 ++++++------- tactics/tacintern.mli | 1 - tactics/tacinterp.ml | 18 +++++++--------- toplevel/search.ml | 4 ++-- toplevel/vernacentries.ml | 4 ++-- 14 files changed, 47 insertions(+), 56 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0a2a459d3..e9ebcf39f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1329,7 +1329,7 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let internalize sigma globalenv env allow_patvar lvar c = +let internalize globalenv env allow_patvar lvar c = let rec intern env = function | CRef ref as x -> let (c,imp,subscopes,l),_ = @@ -1534,7 +1534,6 @@ let internalize sigma globalenv env allow_patvar lvar c = let ist = { Genintern.ltacvars = lvars; ltacrecvars = Id.Map.empty; - gsigma = sigma; genv = globalenv; } in let (_, glb) = Genintern.generic_intern ist gen in @@ -1715,18 +1714,18 @@ type ltac_sign = Id.Set.t * Id.Set.t let empty_ltac_sign = (Id.Set.empty, Id.Set.empty) -let intern_gen kind sigma env +let intern_gen kind env ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign) c = let tmp_scope = scope_of_type_kind kind in - internalize sigma env {ids = extract_ids env; unb = false; + internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; impls = impls} allow_patvar (ltacvars, Id.Map.empty) c -let intern_constr sigma env c = intern_gen WithoutTypeConstraint sigma env c +let intern_constr env c = intern_gen WithoutTypeConstraint env c -let intern_type sigma env c = intern_gen IsType sigma env c +let intern_type env c = intern_gen IsType env c let intern_pattern globalenv patt = try @@ -1744,7 +1743,7 @@ let intern_pattern globalenv patt = (* All evars resolved *) let interp_gen kind sigma env ?(impls=empty_internalization_env) c = - let c = intern_gen kind ~impls sigma env c in + let c = intern_gen kind ~impls env c in understand ~expected_type:kind sigma env c let interp_constr sigma env ?(impls=empty_internalization_env) c = @@ -1759,13 +1758,13 @@ let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ = (* Not all evars expected to be resolved *) let interp_open_constr sigma env c = - understand_tcc sigma env (intern_constr sigma env c) + understand_tcc sigma env (intern_constr env c) (* Not all evars expected to be resolved and computation of implicit args *) let interp_constr_evars_gen_impls evdref env ?(impls=empty_internalization_env) expected_type c = - let c = intern_gen expected_type ~impls !evdref env c in + let c = intern_gen expected_type ~impls env c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in understand_tcc_evars evdref env ~expected_type c, imps @@ -1781,7 +1780,7 @@ let interp_type_evars_impls evdref env ?(impls=empty_internalization_env) c = (* Not all evars expected to be resolved, with side-effect on evars *) let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) expected_type c = - let c = intern_gen expected_type ~impls !evdref env c in + let c = intern_gen expected_type ~impls env c in understand_tcc_evars evdref env ~expected_type c let interp_constr_evars evdref env ?(impls=empty_internalization_env) c = @@ -1795,16 +1794,16 @@ let interp_type_evars evdref env ?(impls=empty_internalization_env) c = (* Miscellaneous *) -let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = +let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let c = intern_gen (if as_type then IsType else WithoutTypeConstraint) - ~allow_patvar:true ~ltacvars sigma env c in + ~allow_patvar:true ~ltacvars env c in pattern_of_glob_constr c let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a = let env = Global.env () in (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = Id.Map.map (fun typ -> (ref None, typ)) vars in - let c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false; + let c = internalize (Global.env()) {ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impls} false (empty_ltac_sign, vl) a in (* Translate and check that [c] has all its free variables bound in [vars] *) @@ -1819,25 +1818,25 @@ let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a = (* Interpret binders and contexts *) let interp_binder sigma env na t = - let t = intern_gen IsType sigma env t in + let t = intern_gen IsType env t in let t' = locate_if_isevar (loc_of_glob_constr t) na t in understand ~expected_type:IsType sigma env t' let interp_binder_evars evdref env na t = - let t = intern_gen IsType !evdref env t in + let t = intern_gen IsType env t in let t' = locate_if_isevar (loc_of_glob_constr t) na t in understand_tcc_evars evdref env ~expected_type:IsType t' open Environ -let my_intern_constr sigma env lvar acc c = - internalize sigma env acc false lvar c +let my_intern_constr env lvar acc c = + internalize env acc false lvar c -let intern_context global_level sigma env impl_env binders = +let intern_context global_level env impl_env binders = try let lvar = (empty_ltac_sign, Id.Map.empty) in let lenv, bl = List.fold_left - (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) lvar) + (intern_local_binder_aux ~global_level (my_intern_constr env lvar) lvar) ({ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impl_env}, []) binders in (lenv.impls, List.map snd bl) @@ -1869,7 +1868,7 @@ let interp_rawcontext_evars evdref env bl = in (env, par), impls let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params = - let int_env,bl = intern_context global_level !evdref env impl_env params in + let int_env,bl = intern_context global_level env impl_env params in let x = interp_rawcontext_evars evdref env bl in int_env, x diff --git a/interp/constrintern.mli b/interp/constrintern.mli index a4f3e057f..bbee24957 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -74,18 +74,18 @@ type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) (** {6 Internalization performs interpretation of global names and notations } *) -val intern_constr : evar_map -> env -> constr_expr -> glob_constr +val intern_constr : env -> constr_expr -> glob_constr -val intern_type : evar_map -> env -> constr_expr -> glob_constr +val intern_type : env -> constr_expr -> glob_constr -val intern_gen : typing_constraint -> evar_map -> env -> +val intern_gen : typing_constraint -> env -> ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> Id.t list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list +val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list (** {6 Composing internalization with type inference (pretyping) } *) @@ -132,7 +132,7 @@ val interp_type_evars_impls : evar_map ref -> env -> (** Interprets constr patterns *) val intern_constr_pattern : - evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> + env -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) diff --git a/interp/genintern.ml b/interp/genintern.ml index d1bc28333..fef32a5ff 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -15,7 +15,6 @@ open Genarg type glob_sign = { ltacvars : Id.Set.t; ltacrecvars : Nametab.ltac_constant Id.Map.t; - gsigma : Evd.evar_map; genv : Environ.env } type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb diff --git a/interp/genintern.mli b/interp/genintern.mli index 7027315e7..970f27f66 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -13,7 +13,6 @@ open Genarg type glob_sign = { ltacvars : Id.Set.t; ltacrecvars : Nametab.ltac_constant Id.Map.t; - gsigma : Evd.evar_map; genv : Environ.env } (** {5 Internalization functions} *) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index b21037d25..6e53ae6a2 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1456,8 +1456,7 @@ let do_instr raw_instr pts = let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in let gl = { it=List.hd gls ; sigma=sigma; } in let env= pf_env gl in - let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; - gsigma = sigma; genv = env} in + let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) sigma env glob_instr in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3dc59b7ca..661e5e486 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -131,7 +131,7 @@ let rec abstract_glob_constr c = function (abstract_glob_constr c bl) let interp_casted_constr_with_implicits sigma env impls c = - Constrintern.intern_gen Pretyping.WithoutTypeConstraint sigma env ~impls + Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls ~allow_patvar:false ~ltacvars:(Id.Set.empty, Id.Set.empty) c (* diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b7c471f4a..ac54e44cc 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -71,7 +71,7 @@ let isVarf f x = let ident_global_exist id = try let ans = CRef (Libnames.Ident (Loc.ghost,id)) in - let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in + let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true with e when Errors.noncritical e -> false diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 36ba80202..8c2776789 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -63,7 +63,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let instantiate_pf_com evk com sigma = let evi = Evd.find sigma evk in let env = Evd.evar_filtered_env evi in - let rawc = Constrintern.intern_constr sigma env com in + let rawc = Constrintern.intern_constr env com in let ltac_vars = (Id.Map.empty, Id.Map.empty) in let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in sigma' diff --git a/tactics/auto.ml b/tactics/auto.ml index 9156e1f04..fc9a335e6 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -859,7 +859,7 @@ let interp_hints = let path, gr = fi c in (o, b, path, gr) in - let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in + let fp = Constrintern.intern_constr_pattern (Global.env()) in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 59bad5808..7f676c157 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -57,12 +57,10 @@ type glob_sign = Genintern.glob_sign = { (* ltac variables and the subset of vars introduced by Intro/Let/... *) ltacrecvars : ltac_constant Id.Map.t; (* ltac recursive names *) - gsigma : Evd.evar_map; genv : Environ.env } let fully_empty_glob_sign = - { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; - gsigma = Evd.empty; genv = Environ.empty_env } + { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = Environ.empty_env } let make_empty_glob_sign () = { fully_empty_glob_sign with genv = Global.env () } @@ -252,12 +250,12 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c = +let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = (lfun, Id.Set.empty) in let c' = - warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars sigma env) c + warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c in (c',if !strict_check then None else Some c) @@ -330,7 +328,7 @@ let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c) let intern_constr_pattern ist ~as_type ~ltacvars pc = let ltacvars = ltacvars, Id.Set.empty in let metas,pat = Constrintern.intern_constr_pattern - ist.gsigma ist.genv ~as_type ~ltacvars pc + ist.genv ~as_type ~ltacvars pc in let c = intern_constr_gen true false ist pc in metas,(c,pat) @@ -701,7 +699,7 @@ and intern_match_rule onlytac ist = function | (All tc)::tl -> All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl) | (Pat (rl,mp,tc))::tl -> - let {ltacvars=lfun; gsigma=sigma; genv=env} = ist in + let {ltacvars=lfun; genv=env} = ist in let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in let ido,metas2,pat = intern_pattern ist lfun mp in let fold accu x = Id.Set.add x accu in @@ -760,7 +758,7 @@ let glob_tactic_env l env x = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in Flags.with_option strict_check (intern_pure_tactic - { ltacvars; ltacrecvars = Id.Map.empty; gsigma = Evd.empty; genv = env }) + { ltacvars; ltacrecvars = Id.Map.empty; genv = env }) x let split_ltac_fun = function diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index c04b6f391..8473f585b 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -26,7 +26,6 @@ open Nametab type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; ltacrecvars : ltac_constant Id.Map.t; - gsigma : Evd.evar_map; genv : Environ.env } val fully_empty_glob_sign : glob_sign diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2e5465340..433322e4c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -485,7 +485,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let ltacvars = Id.Map.domain constrvars in let bndvars = Id.Map.domain ist.lfun in let ltacdata = (ltacvars, bndvars) in - intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c + intern_gen kind ~allow_patvar ~ltacvars:ltacdata env c in let trace = push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in @@ -2078,8 +2078,7 @@ let eval_tactic_ist ist t = let interp_tac_gen lfun avoid_ids debug t = Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in let extra = TacStore.set TacStore.empty f_debug debug in let extra = TacStore.set extra f_avoid_ids avoid_ids in let ist = { lfun = lfun; extra = extra } in @@ -2087,7 +2086,7 @@ let interp_tac_gen lfun avoid_ids debug t = interp_tactic ist (intern_pure_tactic { ltacvars; ltacrecvars = Id.Map.empty; - gsigma = sigma; genv = env } t) + genv = env } t) end let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t @@ -2101,9 +2100,9 @@ let eval_ltac_constr t = (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) let hide_interp global t ot = - let hide_interp env sigma = + let hide_interp env = let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; - gsigma = sigma; genv = env } in + genv = env } in let te = intern_pure_tactic ist t in let t = eval_tactic te in match ot with @@ -2112,11 +2111,10 @@ let hide_interp global t ot = in if global then Proofview.tclENV >= fun env -> - Proofview.tclEVARMAP >= fun sigma -> - hide_interp env sigma + hide_interp env else Proofview.Goal.enter begin fun gl -> - hide_interp (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) + hide_interp (Proofview.Goal.env gl) end (***************************************************************************) @@ -2170,7 +2168,7 @@ let () = let interp_redexp env sigma r = let ist = default_ist () in - let gist = { fully_empty_glob_sign with genv = env; gsigma = sigma } in + let gist = { fully_empty_glob_sign with genv = env; } in interp_red_expr ist sigma env (intern_red_expr gist r) (***************************************************************************) diff --git a/toplevel/search.ml b/toplevel/search.ml index 9e61bc7fb..91762c000 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -247,11 +247,11 @@ let interface_search flags = extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l | (Interface.Type_Pattern s, b) :: l -> let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in + let (_, pat) = Constrintern.intern_constr_pattern env constr in extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l | (Interface.SubType_Pattern s, b) :: l -> let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in + let (_, pat) = Constrintern.intern_constr_pattern env constr in extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l | (Interface.In_Module m, b) :: l -> let path = String.concat "." m in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index db51ff610..399471b74 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1431,7 +1431,7 @@ open Search let interp_search_about_item = function | SearchSubPattern pat -> - let _,pat = intern_constr_pattern Evd.empty (Global.env()) pat in + let _,pat = intern_constr_pattern (Global.env()) pat in GlobSearchSubPattern pat | SearchString (s,None) when Id.is_valid s -> GlobSearchString s @@ -1448,7 +1448,7 @@ let interp_search_about_item = function let vernac_search s r = let r = interp_search_restriction r in let env = Global.env () in - let get_pattern c = snd (Constrintern.intern_constr_pattern Evd.empty env c) in + let get_pattern c = snd (Constrintern.intern_constr_pattern env c) in match s with | SearchPattern c -> msg_notice (Search.search_pattern (get_pattern c) r) -- cgit v1.2.3