diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-30 23:08:19 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-05-03 20:05:57 +0200 |
commit | 9262f440e8d8b8559c5488b1333c023f7305d811 (patch) | |
tree | f09ec49bd38357d949876ca4e494fe22ff2b6a0c /plugins/ltac | |
parent | 267c880c5e8b73770316518a2a820e779c121fdb (diff) |
Allowing to pass arbitrary data in internalization environments.
Diffstat (limited to 'plugins/ltac')
-rw-r--r-- | plugins/ltac/g_obligations.ml4 | 2 | ||||
-rw-r--r-- | plugins/ltac/tacintern.ml | 24 | ||||
-rw-r--r-- | plugins/ltac/tacintern.mli | 4 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.ml | 7 |
4 files changed, 22 insertions, 15 deletions
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 3e6e2db60..a301daa57 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -31,7 +31,7 @@ let () = Obligations.default_tactic := tac let with_tac f tac = - let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in + let env = Genintern.empty_glob_sign (Global.env ()) in let tac = match tac with | None -> None | Some tac -> diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 75227def0..40a299f76 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -41,13 +41,12 @@ let error_tactic_expected ?loc = type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; (* ltac variables and the subset of vars introduced by Intro/Let/... *) - genv : Environ.env } + genv : Environ.env; + extra : Genintern.Store.t; +} -let fully_empty_glob_sign = - { ltacvars = Id.Set.empty; genv = Environ.empty_env } - -let make_empty_glob_sign () = - { fully_empty_glob_sign with genv = Global.env () } +let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env +let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ()) (* We have identifier <| global_reference <| constr *) @@ -192,12 +191,13 @@ 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; genv=env} c = +let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} 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 = { Constrintern.ltac_vars = lfun; ltac_bound = Id.Set.empty; + ltac_extra = extra; } in let c' = warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c @@ -313,6 +313,7 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = let ltacvars = { Constrintern.ltac_vars = ltacvars; ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; } in let metas,pat = Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars pc @@ -344,7 +345,11 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let r = match r with | AN r -> r | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in - let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in + let sign = { + Constrintern.ltac_vars = ist.ltacvars; + ltac_bound = Id.Set.empty; + ltac_extra = ist.extra; + } in let c = Constrintern.interp_reference sign r in match c with | GRef (_,r,None) -> @@ -708,8 +713,7 @@ let glob_tactic_env l env x = let ltacvars = 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; genv = env }) + (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars }) x let split_ltac_fun = function diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 71ca354fa..8ad52ca02 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -18,7 +18,9 @@ open Misctypes type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; - genv : Environ.env } + genv : Environ.env; + extra : Genintern.Store.t; +} val fully_empty_glob_sign : glob_sign diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b8c021f18..5f831f326 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -587,6 +587,7 @@ let interp_uconstr ist env sigma = function let ltacvars = { Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped)); ltac_bound = Id.Map.domain ist.lfun; + ltac_extra = Genintern.Store.empty; } in { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } @@ -614,6 +615,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let ltacvars = { ltac_vars = constr_context; ltac_bound = Id.Map.domain ist.lfun; + ltac_extra = Genintern.Store.empty; } in let kind_for_intern = match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in @@ -1966,8 +1968,7 @@ let interp_tac_gen lfun avoid_ids debug t = let ist = { lfun = lfun; extra = extra } in let ltacvars = Id.Map.domain lfun in interp_tactic ist - (intern_pure_tactic { - ltacvars; genv = env } t) + (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) end } let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t @@ -1976,7 +1977,7 @@ let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t (* [global] means that [t] should be internalized outside of goals. *) let hide_interp global t ot = let hide_interp env = - let ist = { ltacvars = Id.Set.empty; genv = env } in + let ist = Genintern.empty_glob_sign env in let te = intern_pure_tactic ist t in let t = eval_tactic te in match ot with |