diff options
-rw-r--r-- | engine/termops.ml | 7 | ||||
-rw-r--r-- | engine/termops.mli | 2 | ||||
-rw-r--r-- | kernel/cClosure.ml | 10 | ||||
-rw-r--r-- | kernel/csymtable.ml | 2 | ||||
-rw-r--r-- | kernel/environ.ml | 102 | ||||
-rw-r--r-- | kernel/environ.mli | 5 | ||||
-rw-r--r-- | kernel/nativecode.ml | 2 | ||||
-rw-r--r-- | kernel/pre_env.ml | 60 | ||||
-rw-r--r-- | kernel/pre_env.mli | 18 | ||||
-rw-r--r-- | pretyping/unification.ml | 2 | ||||
-rw-r--r-- | proofs/logic.ml | 2 | ||||
-rw-r--r-- | proofs/tacmach.ml | 4 | ||||
-rw-r--r-- | tactics/leminv.ml | 4 | ||||
-rw-r--r-- | tactics/tactics.ml | 24 |
14 files changed, 125 insertions, 119 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index a047bf53c..17e56ec31 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -975,11 +975,8 @@ let smash_rel_context sign = let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init -let rec mem_named_context id ctxt = - match ctxt with - | decl :: _ when Id.equal id (NamedDecl.get_id decl) -> true - | _ :: sign -> mem_named_context id sign - | [] -> false +let mem_named_context_val id ctxt = + try Environ.lookup_named_val id ctxt; true with Not_found -> false let compact_named_context_reverse sign = let compact l decl = diff --git a/engine/termops.mli b/engine/termops.mli index 5d85088f8..0a7ac1f26 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -237,7 +237,7 @@ val map_rel_context_with_binders : val fold_named_context_both_sides : ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> Context.Named.t -> init:'a -> 'a -val mem_named_context : Id.t -> Context.Named.t -> bool +val mem_named_context_val : Id.t -> named_context_val -> bool val compact_named_context : Context.Named.t -> Context.NamedList.t val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index d475f097c..fe9ec5794 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -270,11 +270,9 @@ let info_env info = info.i_cache.i_env open Context.Named.Declaration -let rec assoc_defined id = function -| [] -> raise Not_found -| LocalAssum _ :: ctxt -> assoc_defined id ctxt -| LocalDef (id', c, _) :: ctxt -> - if Id.equal id id' then c else assoc_defined id ctxt +let assoc_defined id env = match Environ.lookup_named id env with +| LocalDef (_, c, _) -> c +| _ -> raise Not_found let ref_value_cache ({i_cache = cache} as infos) ref = try @@ -291,7 +289,7 @@ let ref_value_cache ({i_cache = cache} as infos) ref = | None -> raise Not_found | Some t -> lift n t end - | VarKey id -> assoc_defined id (named_context cache.i_env) + | VarKey id -> assoc_defined id cache.i_env | ConstKey cst -> constant_value_in cache.i_env cst in let v = cache.i_repr infos body in 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..54898320d 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,12 @@ 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 (* [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 map_named_val = map_named_val let empty_named_context = Context.Named.empty @@ -118,8 +116,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 = lookup_named +let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) let eq_named_context_val c1 c2 = c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) @@ -139,10 +137,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 +154,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 +490,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..235ba2fd1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -78,7 +78,6 @@ val fold_rel_context : (** {5 Context of variables (section variables and goal assumptions) } *) val named_context_of_val : named_context_val -> Context.Named.t -val named_vals_of_val : named_context_val -> Pre_env.named_vals val val_of_named_context : Context.Named.t -> named_context_val val empty_named_context_val : named_context_val @@ -273,10 +272,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 ad5b04f3d..eaddace4b 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1861,7 +1861,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 lookup_named id env 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..7be8606ef 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -61,12 +61,14 @@ let force_lazy_val vk = match !vk with let dummy_lazy_val () = ref VKnone 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_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} 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 +79,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_map = Id.Map.empty; +} let empty_env = { env_globals = { @@ -87,8 +90,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 +127,42 @@ 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 = +(* assert (not (Id.Map.mem (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; + } + +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 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 cval = { env_named_ctx = ctx; env_named_map = map } in + Some (decl, v, cval) + +let map_named_val f ctxt = + let open Context.Named.Declaration in + let fold accu d = + let d' = map_constr f d in + let accu = + if d == d' then accu + else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu + 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 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; @@ -146,8 +173,11 @@ let push_named d env = indirect_pterms = env.indirect_pterms; } +let lookup_named id env = + fst (Id.Map.find id env.env_named_context.env_named_map) + let lookup_named_val id env = - snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals) + snd(Id.Map.find id env.env_named_context.env_named_map) (* 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..866790367 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -40,12 +40,14 @@ val force_lazy_val : lazy_val -> (values * Id.Set.t) option val dummy_lazy_val : unit -> lazy_val 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_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} 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 +58,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,7 +73,15 @@ 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 map_named_val : + (constr -> constr) -> named_context_val -> named_context_val + val push_named : Context.Named.Declaration.t -> env -> env +val lookup_named : Id.t -> env -> Context.Named.Declaration.t val lookup_named_val : Id.t -> env -> lazy_val val env_of_named : Id.t -> env -> env diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6573bd238..e6f4090f4 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1587,7 +1587,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let x = id_of_name_using_hdchar (Global.env()) t name in let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else - if mem_named_context x (named_context env) then + if mem_named_context_val x (named_context_val env) then errorlabstrm "Unification.make_abstraction_core" (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") else diff --git a/proofs/logic.ml b/proofs/logic.ml index e4c833627..65497c80d 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -538,7 +538,7 @@ let prim_refiner r sigma goal = nexthyp, t,cl,sigma else - (if !check && mem_named_context id (named_context_of_val sign) then + (if !check && mem_named_context_val id sign then errorlabstrm "Logic.prim_refiner" (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index b9330ff00..2b129ad89 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -187,9 +187,9 @@ module New = struct next_ident_away id ids let pf_get_hyp id gl = - let hyps = Proofview.Goal.hyps gl in + let hyps = Proofview.Goal.env gl in let sign = - try Context.Named.lookup id hyps + try Environ.lookup_named id hyps with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 642bf520b..40b600c89 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -202,11 +202,11 @@ let inversion_scheme env sigma t sort dep_option inv_op = tclTHEN intro (onLastHypId inv_op)) pf) in let pfterm = List.hd (Proof.partial_proof pf) in - let global_named_context = Global.named_context () in + let global_named_context = Global.named_context_val () in let ownSign = ref begin fold_named_context (fun env d sign -> - if mem_named_context (get_id d) global_named_context then sign + if mem_named_context_val (get_id d) global_named_context then sign else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c8cdae53b..0629935e1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -179,10 +179,10 @@ let introduction ?(check=true) id = let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in - let hyps = Proofview.Goal.hyps gl in + let hyps = named_context_val (Proofview.Goal.env gl) in let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in - let () = if check && mem_named_context id hyps then + let () = if check && mem_named_context_val id hyps then errorlabstrm "Tactics.introduction" (str "Variable " ++ pr_id id ++ str " is already declared.") in @@ -518,7 +518,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl -> let (sp', u') = check_mutind env sigma n ar in if not (eq_mind sp sp') then error "Fixpoints should be on the same mutual inductive declaration."; - if mem_named_context f (named_context_of_val sign) then + if mem_named_context_val f sign then errorlabstrm "Logic.prim_refiner" (str "Name " ++ pr_id f ++ str " already used in the environment"); mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth @@ -571,7 +571,7 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl -> | [] -> sign | (f, ar) :: oth -> let open Context.Named.Declaration in - if mem_named_context f (named_context_of_val sign) then + if mem_named_context_val f sign then error "Name already used in the environment."; mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth in @@ -2791,7 +2791,7 @@ let old_generalize_dep ?(with_let=false) c gl = let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in let tothin' = match kind_of_term c with - | Var id when mem_named_context id sign && not (Id.List.mem id init_ids) + | Var id when mem_named_context_val id (val_of_named_context sign) && not (Id.List.mem id init_ids) -> id::tothin | _ -> tothin in @@ -2945,8 +2945,8 @@ let unfold_body x = let open Context.Named.Declaration in Proofview.Goal.enter { enter = begin fun gl -> (** We normalize the given hypothesis immediately. *) - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let xval = match Context.Named.lookup x hyps with + let env = Proofview.Goal.env (Proofview.Goal.assume gl) in + let xval = match Environ.lookup_named x env with | LocalAssum _ -> errorlabstrm "unfold_body" (pr_id x ++ str" is not a defined hypothesis.") | LocalDef (_,xval,_) -> xval @@ -4368,7 +4368,7 @@ let induction_gen clear_flag isrec with_evars elim let cls = Option.default allHypsAndConcl cls in let t = typ_of env sigma c in let is_arg_pure_hyp = - isVar c && not (mem_named_context (destVar c) (Global.named_context())) + isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ())) && lbind == NoBindings && not with_evars && Option.is_empty eqname && clear_flag == None && has_generic_occurrences_but_goal cls (destVar c) env ccl in @@ -4415,7 +4415,7 @@ let induction_gen_l isrec with_evars elim names lc = | [] -> Proofview.tclUNIT () | c::l' -> match kind_of_term c with - | Var id when not (mem_named_context id (Global.named_context())) + | Var id when not (mem_named_context_val id (Global.named_context_val ())) && not with_evars -> let _ = newlc:= id::!newlc in atomize_list l' @@ -4837,7 +4837,7 @@ let abstract_subproof id gk tac = let open Context.Named.Declaration in Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let current_sign = Global.named_context() + let current_sign = Global.named_context_val () and global_sign = Proofview.Goal.hyps gl in let sigma = Sigma.to_evar_map sigma in let evdref = ref sigma in @@ -4845,8 +4845,8 @@ let abstract_subproof id gk tac = List.fold_right (fun d (s1,s2) -> let id = get_id d in - if mem_named_context id current_sign && - interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d + if mem_named_context_val id current_sign && + interpretable_as_section_decl evdref (lookup_named_val id current_sign) d then (s1,push_named_context_val d s2) else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, empty_named_context_val) in |