diff options
author | 2016-11-30 23:08:19 +0100 | |
---|---|---|
committer | 2017-05-03 20:05:57 +0200 | |
commit | 9262f440e8d8b8559c5488b1333c023f7305d811 (patch) | |
tree | f09ec49bd38357d949876ca4e494fe22ff2b6a0c /interp | |
parent | 267c880c5e8b73770316518a2a820e779c121fdb (diff) |
Allowing to pass arbitrary data in internalization environments.
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrintern.ml | 10 | ||||
-rw-r--r-- | interp/constrintern.mli | 2 | ||||
-rw-r--r-- | interp/genintern.ml | 12 | ||||
-rw-r--r-- | interp/genintern.mli | 8 |
4 files changed, 27 insertions, 5 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3f99a3c7c..df7568c7a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -68,6 +68,7 @@ type internalization_env = type ltac_sign = { ltac_vars : Id.Set.t; ltac_bound : Id.Set.t; + ltac_extra : Genintern.Store.t; } let interning_grammar = ref false @@ -1735,12 +1736,14 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | Some gen -> let (ltacvars, ntnvars) = lvar in let ntnvars = Id.Map.domain ntnvars in + let extra = ltacvars.ltac_extra in let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in let lvars = Id.Set.union lvars ntnvars in - let lvars = Id.Set.union lvars env.ids in + let ltacvars = Id.Set.union lvars env.ids in let ist = { - Genintern.ltacvars = lvars; - genv = globalenv; + Genintern.genv = globalenv; + ltacvars; + extra; } in let (_, glb) = Genintern.generic_intern ist gen in Some glb @@ -1931,6 +1934,7 @@ let scope_of_type_kind = function let empty_ltac_sign = { ltac_vars = Id.Set.empty; ltac_bound = Id.Set.empty; + ltac_extra = Genintern.Store.empty; } let intern_gen kind env diff --git a/interp/constrintern.mli b/interp/constrintern.mli index fdd50c6a1..644cafe57 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -70,6 +70,8 @@ type ltac_sign = { (** Variables of Ltac which may be bound to a term *) ltac_bound : Id.Set.t; (** Other variables of Ltac *) + ltac_extra : Genintern.Store.t; + (** Arbitrary payload *) } val empty_ltac_sign : ltac_sign diff --git a/interp/genintern.ml b/interp/genintern.ml index be7abfa99..e443824bd 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -10,9 +10,19 @@ open Names open Mod_subst open Genarg +module Store = Store.Make(struct end) + type glob_sign = { ltacvars : Id.Set.t; - genv : Environ.env } + genv : Environ.env; + extra : Store.t; +} + +let empty_glob_sign env = { + ltacvars = Id.Set.empty; + genv = env; + extra = Store.empty; +} type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb type 'glb subst_fun = substitution -> 'glb -> 'glb diff --git a/interp/genintern.mli b/interp/genintern.mli index 4b0354be3..658caa08c 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -10,9 +10,15 @@ open Names open Mod_subst open Genarg +module Store : Store.S + type glob_sign = { ltacvars : Id.Set.t; - genv : Environ.env } + genv : Environ.env; + extra : Store.t; +} + +val empty_glob_sign : Environ.env -> glob_sign (** {5 Internalization functions} *) |