From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- library/assumptions.ml | 18 +++++--- library/declare.ml | 2 +- library/global.ml | 2 +- library/global.mli | 2 +- library/goptions.ml | 1 + library/impargs.ml | 13 +++--- library/lib.ml | 111 +++++++------------------------------------------ library/lib.mli | 43 +++++++++---------- 8 files changed, 58 insertions(+), 134 deletions(-) (limited to 'library') 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 -- cgit v1.2.3