diff options
| -rw-r--r-- | kernel/csymtable.ml | 2 | ||||
| -rw-r--r-- | kernel/environ.ml | 108 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 | ||||
| -rw-r--r-- | kernel/nativecode.ml | 2 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 42 | ||||
| -rw-r--r-- | kernel/pre_env.mli | 14 |
6 files changed, 86 insertions, 86 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index e195618b6..6f1ace25a 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -191,7 +191,7 @@ and slot_for_fv env fv = | None -> let open Context.Named in let open Declaration in - env.env_named_context |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun + env.env_named_context.env_named_ctx |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> diff --git a/kernel/environ.ml b/kernel/environ.ml index 7351a87d4..cfdd93284 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -56,14 +56,14 @@ let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded let universes env = env.env_stratification.env_universes -let named_context env = env.env_named_context -let named_context_val env = env.env_named_context,env.env_named_vals +let named_context env = env.env_named_context.env_named_ctx +let named_context_val env = env.env_named_context let rel_context env = env.env_rel_context let opaque_tables env = env.indirect_pterms let set_opaque_tables env indirect_pterms = { env with indirect_pterms } let empty_context env = - match env.env_rel_context, env.env_named_context with + match env.env_rel_context, env.env_named_context.env_named_ctx with | [], [] -> true | _ -> false @@ -99,14 +99,18 @@ let fold_rel_context f env ~init = (* Named context *) -let named_context_of_val = fst -let named_vals_of_val = snd +let named_context_of_val c = c.env_named_ctx +let named_vals_of_val c = c.env_named_val (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] should be convertible with t *) -let map_named_val f = - on_fst (Context.Named.map f) +let rec map_named_val f ctx = match match_named_context_val ctx with +| None -> empty_named_context_val +| Some (d, v, ctx) -> + let d = Context.Named.Declaration.map_constr f d in + let ctx = map_named_val f ctx in + push_named_context_val_val d v ctx let empty_named_context = Context.Named.empty @@ -118,8 +122,8 @@ let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named id env = Context.Named.lookup id env.env_named_context -let lookup_named_val id (ctxt,_) = Context.Named.lookup id ctxt +let lookup_named id env = Context.Named.lookup id env.env_named_context.env_named_ctx +let lookup_named_val id ctxt = Context.Named.lookup id ctxt.env_named_ctx let eq_named_context_val c1 c2 = c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) @@ -139,10 +143,9 @@ let evaluable_named id env = | Some _ -> true | _ -> false -let reset_with_named_context (ctxt,ctxtv) env = +let reset_with_named_context ctxt env = { env with env_named_context = ctxt; - env_named_vals = ctxtv; env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0 } @@ -157,11 +160,11 @@ let pop_rel_context n env = let fold_named_context f env ~init = let rec fold_right env = - match env.env_named_context with - | [] -> init - | d::ctxt -> + match match_named_context_val env.env_named_context with + | None -> init + | Some (d, v, rem) -> let env = - reset_with_named_context (ctxt,List.tl env.env_named_vals) env in + reset_with_named_context rem env in f env d (fold_right env) in fold_right env @@ -493,66 +496,47 @@ let compile_constant_body = Cbytegen.compile_constant_body false exception Hyp_not_found -let apply_to_hyp (ctxt,vals) id f = - let rec aux rtail ctxt vals = - match ctxt, vals with - | d::ctxt, v::vals -> +let apply_to_hyp ctxt id f = + let rec aux rtail ctxt = + match match_named_context_val ctxt with + | Some (d, v, ctxt) -> if Id.equal (get_id d) id then - (f ctxt d rtail)::ctxt, v::vals + push_named_context_val_val (f ctxt.env_named_ctx d rtail) v ctxt else - let ctxt',vals' = aux (d::rtail) ctxt vals in - d::ctxt', v::vals' - | [],[] -> raise Hyp_not_found - | _, _ -> assert false - in aux [] ctxt vals - -let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = - let rec aux ctxt vals = - match ctxt,vals with - | d::ctxt, v::vals -> + let ctxt' = aux (d::rtail) ctxt in + push_named_context_val_val d v ctxt' + | None -> raise Hyp_not_found + in aux [] ctxt + +let apply_to_hyp_and_dependent_on ctxt id f g = + let rec aux sign = + match match_named_context_val sign with + | Some (d, v, sign) -> if Id.equal (get_id d) id then - let sign = ctxt,vals in push_named_context_val (f d sign) sign else - let (ctxt,vals as sign) = aux ctxt vals in + let sign = aux sign in push_named_context_val (g d sign) sign - | [],[] -> raise Hyp_not_found - | _,_ -> assert false - in aux ctxt vals - -let insert_after_hyp (ctxt,vals) id d check = - let rec aux ctxt vals = - match ctxt, vals with - | decl::ctxt', v::vals' -> - if Id.equal (get_id decl) id then begin - check ctxt; - push_named_context_val d (ctxt,vals) - end else - let ctxt,vals = aux ctxt vals in - d::ctxt, v::vals - | [],[] -> raise Hyp_not_found - | _, _ -> assert false - in aux ctxt vals - + | None -> raise Hyp_not_found + in aux ctxt (* To be used in Logic.clear_hyps *) -let remove_hyps ids check_context check_value (ctxt, vals) = - let rec remove_hyps ctxt vals = match ctxt, vals with - | [], [] -> ([], []), false - | d :: rctxt, (nid, v) :: rvals -> - let (ans, seen) = remove_hyps rctxt rvals in +let remove_hyps ids check_context check_value ctxt = + let rec remove_hyps ctxt = match match_named_context_val ctxt with + | None -> empty_named_context_val, false + | Some (d, v, rctxt) -> + let (ans, seen) = remove_hyps rctxt in if Id.Set.mem (get_id d) ids then (ans, true) - else if not seen then (ctxt, vals), false + else if not seen then ctxt, false else - let (rctxt', rvals') = ans in + let rctxt' = ans in let d' = check_context d in let v' = check_value v in - if d == d' && v == v' && rctxt == rctxt' && rvals == rvals' then - (ctxt, vals), true - else (d' :: rctxt', (nid, v') :: rvals'), true - | _ -> assert false + if d == d' && v == v' && rctxt == rctxt' then + ctxt, true + else push_named_context_val_val d' v' rctxt', true in - fst (remove_hyps ctxt vals) + fst (remove_hyps ctxt) (*spiwack: the following functions assemble the pieces of the retroknowledge note that the "consistent" register function is available in the module diff --git a/kernel/environ.mli b/kernel/environ.mli index b5e576435..cb4a94d45 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -273,10 +273,6 @@ val apply_to_hyp_and_dependent_on : named_context_val -> variable -> (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) -> named_context_val -val insert_after_hyp : named_context_val -> variable -> - Context.Named.Declaration.t -> - (Context.Named.t -> unit) -> named_context_val - val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 87302dcf5..79930f6ad 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1845,7 +1845,7 @@ and compile_rel env sigma univ auxdefs n = and compile_named env sigma univ auxdefs id = let open Context.Named.Declaration in - match Context.Named.lookup id env.env_named_context with + match Context.Named.lookup id env.env_named_context.env_named_ctx with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 5afefeebd..47d003fe9 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -63,10 +63,14 @@ let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) type named_vals = (Id.t * lazy_val) list +type named_context_val = { + env_named_ctx : Context.Named.t; + env_named_val : named_vals; +} + type env = { env_globals : globals; - env_named_context : Context.Named.t; - env_named_vals : named_vals; + env_named_context : named_context_val; env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; @@ -77,9 +81,10 @@ type env = { indirect_pterms : Opaqueproof.opaquetab; } -type named_context_val = Context.Named.t * named_vals - -let empty_named_context_val = [],[] +let empty_named_context_val = { + env_named_ctx = []; + env_named_val = []; +} let empty_env = { env_globals = { @@ -87,8 +92,7 @@ let empty_env = { env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; - env_named_context = Context.Named.empty; - env_named_vals = []; + env_named_context = empty_named_context_val; env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0; @@ -125,17 +129,27 @@ let env_of_rel n env = (* Named context *) -let push_named_context_val d (ctxt,vals) = - let rval = ref VKnone in - Context.Named.add d ctxt, (get_id d,rval)::vals +let push_named_context_val_val d rval ctxt = + { + env_named_ctx = Context.Named.add d ctxt.env_named_ctx; + env_named_val = (get_id d, rval) :: ctxt.env_named_val; + } + +let push_named_context_val d ctxt = + push_named_context_val_val d (ref VKnone) ctxt + +let match_named_context_val c = match c.env_named_ctx, c.env_named_val with +| [], [] -> None +| decl :: ctx, (_, v) :: vls -> + let cval = { env_named_ctx = ctx; env_named_val = vls } in + Some (decl, v, cval) +| _ -> assert false let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); assert (env.env_rel_context = []); *) - let rval = ref VKnone in { env_globals = env.env_globals; - env_named_context = Context.Named.add d env.env_named_context; - env_named_vals = (get_id d, rval) :: env.env_named_vals; + 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; @@ -147,7 +161,7 @@ let push_named d env = } let lookup_named_val id env = - snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals) + snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_context.env_named_val) (* 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 e551d22c8..928a8009e 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -42,10 +42,14 @@ val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit type named_vals = (Id.t * lazy_val) list +type named_context_val = private { + env_named_ctx : Context.Named.t; + env_named_val : named_vals; +} + type env = { env_globals : globals; - env_named_context : Context.Named.t; - env_named_vals : named_vals; + env_named_context : named_context_val; env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; @@ -56,8 +60,6 @@ type env = { indirect_pterms : Opaqueproof.opaquetab; } -type named_context_val = Context.Named.t * named_vals - val empty_named_context_val : named_context_val val empty_env : env @@ -73,6 +75,10 @@ val env_of_rel : int -> env -> env val push_named_context_val : Context.Named.Declaration.t -> named_context_val -> named_context_val +val push_named_context_val_val : + Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val +val match_named_context_val : + named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option val push_named : Context.Named.Declaration.t -> env -> env val lookup_named_val : Id.t -> env -> lazy_val val env_of_named : Id.t -> env -> env |