diff options
Diffstat (limited to 'kernel/pre_env.ml')
-rw-r--r-- | kernel/pre_env.ml | 99 |
1 files changed, 57 insertions, 42 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 7be8606e..8ebe48e2 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Benjamin Grégoire out of environ.ml for better @@ -15,9 +17,9 @@ open Util open Names -open Term open Declarations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* The type of environments. *) @@ -49,7 +51,7 @@ type stratification = { } type val_kind = - | VKvalue of (values * Id.Set.t) CEphemeron.key + | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key | VKnone type lazy_val = val_kind ref @@ -66,15 +68,18 @@ type named_context_val = { env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; } +type rel_context_val = { + 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_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_named_context : named_context_val; (* section variables *) + env_rel_context : rel_context_val; env_nb_rel : int; env_stratification : stratification; env_typing_flags : typing_flags; - env_conv_oracle : Conv_oracle.oracle; retroknowledge : Retroknowledge.retroknowledge; indirect_pterms : Opaqueproof.opaquetab; } @@ -84,6 +89,11 @@ let empty_named_context_val = { env_named_map = Id.Map.empty; } +let empty_rel_context_val = { + env_rel_ctx = []; + env_rel_map = Range.empty; +} + let empty_env = { env_globals = { env_constants = Cmap_env.empty; @@ -91,14 +101,12 @@ let empty_env = { env_modules = MPmap.empty; env_modtypes = MPmap.empty}; env_named_context = empty_named_context_val; - env_rel_context = Context.Rel.empty; - env_rel_val = []; + env_rel_context = empty_rel_context_val; env_nb_rel = 0; env_stratification = { env_universes = UGraph.initial_universes; env_engagement = PredicativeSet }; - env_typing_flags = Declareops.safe_flags; - env_conv_oracle = Conv_oracle.empty; + env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.initial_retroknowledge; indirect_pterms = Opaqueproof.empty_opaquetab } @@ -107,31 +115,49 @@ let empty_env = { let nb_rel env = env.env_nb_rel +let push_rel_context_val d ctx = { + env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx; + env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map; +} + +let match_rel_context_val ctx = match ctx.env_rel_ctx with +| [] -> None +| decl :: rem -> + let (_, lval) = Range.hd ctx.env_rel_map in + let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in + Some (decl, lval, ctx) + let push_rel d env = - let rval = ref VKnone in { env with - env_rel_context = Context.Rel.add d env.env_rel_context; - env_rel_val = rval :: env.env_rel_val; + env_rel_context = push_rel_context_val d env.env_rel_context; env_nb_rel = env.env_nb_rel + 1 } +let lookup_rel n env = + try fst (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + let lookup_rel_val n env = - try List.nth env.env_rel_val (n - 1) - with Failure _ -> raise Not_found + try snd (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + +let rel_skipn n ctx = { + env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx; + env_rel_map = Range.skipn n ctx.env_rel_map; +} let env_of_rel n env = { env with - env_rel_context = Util.List.skipn n env.env_rel_context; - env_rel_val = Util.List.skipn n env.env_rel_val; + env_rel_context = rel_skipn n env.env_rel_context; env_nb_rel = env.env_nb_rel - n } (* Named context *) let push_named_context_val_val d rval ctxt = -(* assert (not (Id.Map.mem (get_id d) ctxt.env_named_map)); *) +(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) { env_named_ctx = Context.Named.add d ctxt.env_named_ctx; - env_named_map = Id.Map.add (get_id d) (d, rval) ctxt.env_named_map; + env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; } let push_named_context_val d ctxt = @@ -140,8 +166,8 @@ let push_named_context_val d ctxt = let match_named_context_val c = match c.env_named_ctx with | [] -> None | decl :: ctx -> - let (_, v) = Id.Map.find (get_id decl) c.env_named_map in - let map = Id.Map.remove (get_id decl) c.env_named_map in + let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in + let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in let cval = { env_named_ctx = ctx; env_named_map = map } in Some (decl, v, cval) @@ -155,23 +181,12 @@ let map_named_val f ctxt = in (accu, d') in - let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in - { env_named_ctx = ctx; env_named_map = map } + let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in + if map == ctxt.env_named_map then ctxt + else { env_named_ctx = ctx; env_named_map = map } let push_named d env = -(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); - assert (env.env_rel_context = []); *) - { env_globals = env.env_globals; - env_named_context = push_named_context_val d env.env_named_context; - env_rel_context = env.env_rel_context; - env_rel_val = env.env_rel_val; - env_nb_rel = env.env_nb_rel; - env_stratification = env.env_stratification; - env_typing_flags = env.env_typing_flags; - env_conv_oracle = env.env_conv_oracle; - retroknowledge = env.retroknowledge; - indirect_pterms = env.indirect_pterms; - } + {env with env_named_context = push_named_context_val d env.env_named_context} let lookup_named id env = fst (Id.Map.find id env.env_named_context.env_named_map) |