summaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/assumptions.ml18
-rw-r--r--library/declare.ml2
-rw-r--r--library/global.ml2
-rw-r--r--library/global.mli2
-rw-r--r--library/goptions.ml1
-rw-r--r--library/impargs.ml13
-rw-r--r--library/lib.ml111
-rw-r--r--library/lib.mli43
8 files changed, 58 insertions, 134 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml
index adc7f8ed..d2f8ad53 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -54,6 +54,16 @@ module ContextObjectMap = Map.Make (OrderedContextObject)
let modcache = ref (MPmap.empty : structure_body MPmap.t)
+let rec search_mod_label lab = function
+ | [] -> raise Not_found
+ | (l,SFBmodule mb) :: _ when l = lab -> mb
+ | _ :: fields -> search_mod_label lab fields
+
+let rec search_cst_label lab = function
+ | [] -> raise Not_found
+ | (l,SFBconst cb) :: _ when l = lab -> cb
+ | _ :: fields -> search_cst_label lab fields
+
let rec lookup_module_in_impl mp =
try Global.lookup_module mp
with Not_found ->
@@ -64,9 +74,7 @@ let rec lookup_module_in_impl mp =
raise Not_found (* should have been found by [lookup_module] *)
| MPdot (mp',lab') ->
let fields = memoize_fields_of_mp mp' in
- match List.assoc lab' fields with
- | SFBmodule mb -> mb
- | _ -> assert false (* same label for a non-module ?! *)
+ search_mod_label lab' fields
and memoize_fields_of_mp mp =
try MPmap.find mp !modcache
@@ -126,9 +134,7 @@ let lookup_constant_in_impl cst fallback =
let fields = memoize_fields_of_mp mp in
(* A module found this way is necessarily closed, in particular
our constant cannot be in an opened section : *)
- match List.assoc lab fields with
- | SFBconst cb -> cb
- | _ -> assert false (* label not pointing to a constant ?! *)
+ search_cst_label lab fields
with Not_found ->
(* Either:
- The module part of the constant isn't registered yet :
diff --git a/library/declare.ml b/library/declare.ml
index 28858085..066c97a4 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -116,7 +116,7 @@ let open_constant i ((sp,kn),_) =
Nametab.push (Nametab.Exactly i) sp (ConstRef con)
let exists_name id =
- variable_exists id or Global.exists_label (label_of_id id)
+ variable_exists id or Global.exists_objlabel (label_of_id id)
let check_exists sp =
let id = basename sp in
diff --git a/library/global.ml b/library/global.ml
index ab70bb7c..a0871f0c 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -133,7 +133,7 @@ let mind_of_delta_kn kn =
Mod_subst.mind_of_delta resolver_param
(Mod_subst.mind_of_delta_kn resolver kn)
-let exists_label id = exists_label id !global_env
+let exists_objlabel id = exists_objlabel id !global_env
let start_library dir =
let mp,newenv = start_library dir !global_env in
diff --git a/library/global.mli b/library/global.mli
index 1a0fabdc..77fd465c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -87,7 +87,7 @@ val lookup_module : module_path -> module_body
val lookup_modtype : module_path -> module_type_body
val constant_of_delta_kn : kernel_name -> constant
val mind_of_delta_kn : kernel_name -> mutual_inductive
-val exists_label : label -> bool
+val exists_objlabel : label -> bool
(** Compiled modules *)
val start_library : dir_path -> module_path
diff --git a/library/goptions.ml b/library/goptions.ml
index 90c8728c..5af18689 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -247,6 +247,7 @@ let declare_option cast uncast
declare_object {(default_object ("G "^nickname key)) with
cache_function = (fun (_,v) -> write v);
classify_function = (fun v -> Substitute v);
+ subst_function = (fun (_,v) -> v);
discharge_function = (fun (_,v) -> Some v);
load_function = (fun _ (_,v) -> write v)}
in
diff --git a/library/impargs.ml b/library/impargs.ml
index ef7f5921..73699a90 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -207,11 +207,10 @@ let rec is_rigid_head t = match kind_of_term t with
(* calcule la liste des arguments implicites *)
-let find_displayed_name_in all avoid na b =
- if all then
- compute_and_force_displayed_name_in (RenamingElsewhereFor b) avoid na b
- else
- compute_displayed_name_in (RenamingElsewhereFor b) avoid na b
+let find_displayed_name_in all avoid na (_,b as envnames_b) =
+ let flag = RenamingElsewhereFor envnames_b in
+ if all then compute_and_force_displayed_name_in flag avoid na b
+ else compute_displayed_name_in flag avoid na b
let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let rigid = ref true in
@@ -219,7 +218,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let t = whd_betadeltaiota env t in
match kind_of_term t with
| Prod (na,a,b) ->
- let na',avoid' = find_displayed_name_in all avoid na b in
+ let na',avoid' = find_displayed_name_in all avoid na (names,b) in
add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
(aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
| _ ->
@@ -232,7 +231,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
in
match kind_of_term (whd_betadeltaiota env t) with
| Prod (na,a,b) ->
- let na',avoid = find_displayed_name_in all [] na b in
+ let na',avoid = find_displayed_name_in all [] na ([],b) in
let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
!rigid, Array.to_list v
| _ -> true, []
diff --git a/library/lib.ml b/library/lib.ml
index 7554fd0b..bb3b5716 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -572,72 +572,16 @@ let reset_to_gen test =
let reset_to sp = reset_to_gen (fun x -> fst x = sp)
-(* LEM: TODO
- * We will need to muck with frozen states in after, too!
- * Not only FrozenState, but also those embedded in Opened(Section|Module)
- *)
-let delete_gen test =
- let (after,equal,before) = split_lib_gen test in
- let rec chop_at_dot = function
- | [] as l -> l
- | (_, Leaf o)::t when object_tag o = "DOT" -> t
- | _::t -> chop_at_dot t
- and chop_before_dot = function
- | [] as l -> l
- | (_, Leaf o)::t as l when object_tag o = "DOT" -> l
- | _::t -> chop_before_dot t
- in
- set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before))
-
-let delete sp = delete_gen (fun x -> fst x = sp)
-
-let reset_name (loc,id) =
- let (sp,_) =
- try
- find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
- with Not_found ->
- user_err_loc (loc,"reset_name",pr_id id ++ str ": no such entry")
- in
- reset_to sp
-
-let remove_name (loc,id) =
- let (sp,_) =
- try
- find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
- with Not_found ->
- user_err_loc (loc,"remove_name",pr_id id ++ str ": no such entry")
- in
- delete sp
+let first_command_label = 1
-let is_mod_node = function
- | OpenedModule _ | OpenedSection _
- | ClosedModule _ | ClosedSection _ -> true
- | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
- || t = "MODULE ALIAS"
- | _ -> false
-
-(* Reset on a module or section name in order to bypass constants with
- the same name *)
-
-let reset_mod (loc,id) =
- let (_,before) =
- try
- find_split_p (fun (sp,node) ->
- let (_,spi) = repr_path (fst sp) in id = spi
- && is_mod_node node)
- with Not_found ->
- user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry")
- in
- set_lib_stk before
-
-let mark_end_of_command, current_command_label, set_command_label =
- let n = ref 0 in
+let mark_end_of_command, current_command_label, reset_command_label =
+ let n = ref (first_command_label-1) in
(fun () ->
match !lib_stk with
(_,Leaf o)::_ when object_tag o = "DOT" -> ()
| _ -> incr n;add_anonymous_leaf (inLabel !n)),
(fun () -> !n),
- (fun x -> n:=x)
+ (fun x -> n:=x;add_anonymous_leaf (inLabel x))
let is_label_n n x =
match x with
@@ -650,21 +594,21 @@ let is_label_n n x =
let reset_label n =
if n >= current_command_label () then
error "Cannot backtrack to the current label or a future one";
- let res = reset_to_gen (is_label_n n) in
+ reset_to_gen (is_label_n n);
(* forget state numbers after n only if reset succeeded *)
- set_command_label (n-1);
- res
+ reset_command_label n
-let rec back_stk n stk =
- match stk with
- (sp,Leaf o)::tail when object_tag o = "DOT" ->
- if n=0 then sp else back_stk (n-1) tail
- | _::tail -> back_stk n tail
- | [] -> error "Reached begin of command history"
+(** Search the last label registered before defining [id] *)
-let back n =
- reset_to (back_stk n !lib_stk);
- set_command_label (current_command_label () - n - 1)
+let label_before_name (loc,id) =
+ let found = ref false in
+ let search = function
+ | (_,Leaf o) when !found && object_tag o = "DOT" -> true
+ | (sp,_) -> (if id = snd (repr_path (fst sp)) then found := true); false
+ in
+ match find_entry_p search with
+ | (_,Leaf o) -> outLabel o
+ | _ -> raise Not_found
(* State and initialization. *)
@@ -684,29 +628,6 @@ let init () =
path_prefix := initial_prefix;
init_summaries()
-(* Initial state. *)
-
-let initial_state = ref None
-
-let declare_initial_state () =
- let name = add_anonymous_entry (FrozenState (freeze_summaries())) in
- initial_state := Some name
-
-let reset_initial () =
- match !initial_state with
- | None ->
- error "Resetting to the initial state is possible only interactively"
- | Some sp ->
- begin match split_lib sp with
- | (_,[_,FrozenState fs as hd],before) ->
- lib_stk := hd::before;
- recalc_path_prefix ();
- set_command_label 0;
- unfreeze_summaries fs
- | _ -> assert false
- end
-
-
(* Misc *)
let mp_of_global ref =
diff --git a/library/lib.mli b/library/lib.mli
index 0d6eb34b..45c598aa 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -62,17 +62,6 @@ val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
val add_frozen_state : unit -> unit
-(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
-val mark_end_of_command : unit -> unit
-
-(** Returns the current label number *)
-val current_command_label : unit -> int
-
-(** [reset_label n] resets [lib_stk] to the label n registered by
- [mark_end_of_command()]. It forgets the label and anything
- registered after it. The label should be strictly in the past. *)
-val reset_label : int -> unit
-
(** {6 ... } *)
(** The function [contents_after] returns the current library segment,
starting from a given section path. If not given, the entire segment
@@ -151,16 +140,28 @@ val remove_section_part : Libnames.global_reference -> Names.dir_path
val open_section : Names.identifier -> unit
val close_section : unit -> unit
-(** {6 Backtracking (undo). } *)
+(** {6 Backtracking } *)
-val reset_to : Libnames.object_name -> unit
-val reset_name : Names.identifier Util.located -> unit
-val remove_name : Names.identifier Util.located -> unit
-val reset_mod : Names.identifier Util.located -> unit
+(** NB: The next commands are low-level ones, do not use them directly
+ otherwise the command history stack in [Backtrack] will be out-of-sync.
+ Also note that [reset_initial] is now [reset_label first_command_label] *)
-(** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of
- [mark_end_of_command] (counting backwards) *)
-val back : int -> unit
+(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
+val mark_end_of_command : unit -> unit
+
+(** Returns the current label number *)
+val current_command_label : unit -> int
+
+(** The first label number *)
+val first_command_label : int
+
+(** [reset_label n] resets [lib_stk] to the label n registered by
+ [mark_end_of_command()]. It forgets anything registered after
+ this label. The label should be strictly in the past. *)
+val reset_label : int -> unit
+
+(** search the label registered immediately before adding some definition *)
+val label_before_name : Names.identifier Util.located -> int
(** {6 We can get and set the state of the operations (used in [States]). } *)
@@ -171,10 +172,6 @@ val unfreeze : frozen -> unit
val init : unit -> unit
-val declare_initial_state : unit -> unit
-val reset_initial : unit -> unit
-
-
(** XML output hooks *)
val set_xml_open_section : (Names.identifier -> unit) -> unit
val set_xml_close_section : (Names.identifier -> unit) -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-09 13:51:14 +0000