diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/csymtable.ml | 39 | ||||
| -rw-r--r-- | kernel/environ.ml | 11 | ||||
| -rw-r--r-- | kernel/environ.mli | 3 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 61 | ||||
| -rw-r--r-- | kernel/pre_env.mli | 33 |
5 files changed, 66 insertions, 81 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index fc2d09254..d81b98ac4 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -121,31 +121,36 @@ let rec slot_for_getglobal env kn = rk := Some pos; pos -and slot_for_fv env fv= +and slot_for_fv env fv = match fv with | FVnamed id -> - let nv = lookup_named_val id env in + let nv = Pre_env.lookup_named_val id env in begin match !nv with - | VKvalue v -> v - | VKaxiom id -> - let v = val_of_named id in - nv := VKvalue v; v - | VKdef c -> - let v = val_of_constr (env_of_named id env) c in - nv := VKvalue v; v + | VKvalue (v,_) -> v + | VKnone -> + let (_, b, _) = Sign.lookup_named id env.env_named_context in + let v,d = + match b with + | None -> (val_of_named id, Idset.empty) + | Some c -> (val_of_constr env c, Environ.global_vars_set (Environ.env_of_pre_env env) c) + in + nv := VKvalue (v,d); v end | FVrel i -> - let rv = lookup_rel_val i env in + let rv = Pre_env.lookup_rel_val i env in begin match !rv with - | VKvalue v -> v - | VKaxiom k -> - let v = val_of_rel k in - rv := VKvalue v; v - | VKdef c -> - let v = val_of_constr (env_of_rel i env) c in - rv := VKvalue v; v + | VKvalue (v, _) -> v + | VKnone -> + let (_, b, _) = Sign.lookup_rel i env.env_rel_context in + let (v, d) = + match b with + | None -> (val_of_rel i, Idset.empty) + | Some c -> let renv = env_of_rel i env in + (val_of_constr renv c, Environ.global_vars_set (Environ.env_of_pre_env renv) c) + in + rv := VKvalue (v,d); v end and eval_to_patch env (buff,pl,fv) = diff --git a/kernel/environ.ml b/kernel/environ.ml index 56c057488..a9ba253b0 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -15,7 +15,6 @@ open Univ open Term open Declarations open Pre_env -open Csymtable (* The type of environments. *) @@ -24,6 +23,7 @@ type named_context_val = Pre_env.named_context_val type env = Pre_env.env let pre_env env = env +let env_of_pre_env env = env let empty_named_context_val = empty_named_context_val @@ -359,14 +359,15 @@ let insert_after_hyp (ctxt,vals) id d check = in aux ctxt vals (* To be used in Logic.clear_hyps *) -let remove_hyps ids check (ctxt, vals) = +let remove_hyps ids check_context check_value (ctxt, vals) = let ctxt,vals,rmv = - List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) -> + List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals,rmv) -> if List.mem id ids then (ctxt,vals,id::rmv) else - let nd = check d in - (nd::ctxt,v::vals,rmv)) + let nd = check_context d in + let nv = check_value v in + (nd::ctxt,(id',nv)::vals,rmv)) ctxt vals ([],[],[]) in ((ctxt,vals),rmv) diff --git a/kernel/environ.mli b/kernel/environ.mli index 8ba5962d3..96c2ba276 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -35,6 +35,7 @@ open Sign type env val pre_env : env -> Pre_env.env +val env_of_pre_env : Pre_env.env -> env type named_context_val val eq_named_context_val : named_context_val -> named_context_val -> bool @@ -216,5 +217,5 @@ val insert_after_hyp : named_context_val -> variable -> named_declaration -> (named_context -> unit) -> named_context_val -val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> named_context_val -> named_context_val * identifier list +val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val * identifier list diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 7bf7a8901..7a7e00e90 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -33,25 +33,20 @@ type stratification = { env_engagement : engagement option } -type 'a val_kind = - | VKvalue of values - | VKaxiom of 'a - | VKdef of constr +type val_kind = + | VKvalue of values * Idset.t + | VKnone -type 'a lazy_val = 'a val_kind ref +type lazy_val = val_kind ref -type rel_val = inv_rel_key lazy_val - -type named_val = identifier lazy_val - -type named_vals = (identifier * named_val) list +type named_vals = (identifier * lazy_val) list type env = { env_globals : globals; env_named_context : named_context; env_named_vals : named_vals; env_rel_context : rel_context; - env_rel_val : rel_val list; + env_rel_val : lazy_val list; env_nb_rel : int; env_stratification : stratification } @@ -78,18 +73,13 @@ let empty_env = { (* Rel context *) let nb_rel env = env.env_nb_rel - + let push_rel d env = - let _,body,_ = d in - let rval = - match body with - | None -> ref (VKaxiom env.env_nb_rel) - | Some c -> ref (VKdef c) - in - { env with - env_rel_context = add_rel_decl d env.env_rel_context; - env_rel_val = rval :: env.env_rel_val; - env_nb_rel = env.env_nb_rel + 1 } + let rval = ref VKnone in + { env with + env_rel_context = add_rel_decl d env.env_rel_context; + env_rel_val = rval :: env.env_rel_val; + env_nb_rel = env.env_nb_rel + 1 } let lookup_rel_val n env = try List.nth env.env_rel_val (n - 1) @@ -101,16 +91,13 @@ let env_of_rel n env = env_rel_val = Util.list_skipn n env.env_rel_val; env_nb_rel = env.env_nb_rel - n } - + (* Named context *) let push_named_context_val d (ctxt,vals) = - let id,body,_ = d in - let rval = - match body with - | None -> ref (VKaxiom id) - | Some c -> ref (VKdef c) - in Sign.add_named_decl d ctxt, (id,rval)::vals + let id,_,_ = d in + let rval = ref VKnone in + Sign.add_named_decl d ctxt, (id,rval)::vals exception ASSERT of Sign.rel_context @@ -118,18 +105,14 @@ let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); assert (env.env_rel_context = []); *) let id,body,_ = d in - let rval = - match body with - | None -> ref (VKaxiom id) - | Some c -> ref (VKdef c) - in - { env with - env_named_context = Sign.add_named_decl d env.env_named_context; - env_named_vals = (id,rval):: env.env_named_vals } + let rval = ref VKnone in + { env with + env_named_context = Sign.add_named_decl d env.env_named_context; + env_named_vals = (id,rval):: env.env_named_vals } let lookup_named_val id env = - snd(List.find (fun (id',_) -> id = id') env.env_named_vals) - + snd(List.find (fun (id',_) -> id = id') env.env_named_vals) + (* Warning all the names should be different *) let env_of_named id env = env diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 6144f20cb..728f28be0 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -33,27 +33,22 @@ type stratification = { env_engagement : engagement option } -type 'a val_kind = - | VKvalue of values - | VKaxiom of 'a - | VKdef of constr +type val_kind = + | VKvalue of values * Idset.t + | VKnone -type 'a lazy_val = 'a val_kind ref +type lazy_val = val_kind ref -type rel_val = inv_rel_key lazy_val - -type named_val = identifier lazy_val - -type named_vals = (identifier * named_val) list +type named_vals = (identifier * lazy_val) list type env = { - env_globals : globals; - env_named_context : named_context; - env_named_vals : named_vals; - env_rel_context : rel_context; - env_rel_val : rel_val list; - env_nb_rel : int; - env_stratification : stratification } + env_globals : globals; + env_named_context : named_context; + env_named_vals : named_vals; + env_rel_context : rel_context; + env_rel_val : lazy_val list; + env_nb_rel : int; + env_stratification : stratification } type named_context_val = named_context * named_vals @@ -65,14 +60,14 @@ val empty_env : env val nb_rel : env -> int val push_rel : rel_declaration -> env -> env -val lookup_rel_val : int -> env -> rel_val +val lookup_rel_val : int -> env -> lazy_val val env_of_rel : int -> env -> env (* Named context *) val push_named_context_val : named_declaration -> named_context_val -> named_context_val val push_named : named_declaration -> env -> env -val lookup_named_val : identifier -> env -> named_val +val lookup_named_val : identifier -> env -> lazy_val val env_of_named : identifier -> env -> env (* Global constants *) |