diff options
| author | Pierre-Marie Pédrot | 2016-09-30 12:33:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-12-29 14:46:32 +0100 |
| commit | a4c8ee5ccffd2b56acf5e6719213e9799e077601 (patch) | |
| tree | 73a81385bae814c274bb96850857f736035b7fbe /kernel/pre_env.mli | |
| parent | 90a246c9c0bd93c442ae74b4c3f0f3519ce7f306 (diff) | |
Fast environment lookup for rels.
We take advantage of the range structure to get a O(log n) retrieval of values
bound to a rel in an environment.
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 054ae17437..563acb0a25 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -45,11 +45,15 @@ type named_context_val = private { env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; } +type rel_context_val = private { + env_rel_ctx : Context.Rel.t; + env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; +} + type env = { env_globals : globals; env_named_context : named_context_val; - env_rel_context : Context.Rel.t; - env_rel_val : lazy_val list; + env_rel_context : rel_context_val; env_nb_rel : int; env_stratification : stratification; env_typing_flags : typing_flags; @@ -64,8 +68,15 @@ val empty_env : env (** Rel context *) +val empty_rel_context_val : rel_context_val +val push_rel_context_val : + Context.Rel.Declaration.t -> rel_context_val -> rel_context_val +val match_rel_context_val : + rel_context_val -> (Context.Rel.Declaration.t * lazy_val * rel_context_val) option + val nb_rel : env -> int val push_rel : Context.Rel.Declaration.t -> env -> env +val lookup_rel : int -> env -> Context.Rel.Declaration.t val lookup_rel_val : int -> env -> lazy_val val env_of_rel : int -> env -> env |