From bbae426407ba7df585c22ec687a79c0cf216a6a8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Mar 2017 00:17:06 +0100 Subject: [library] Don't recompute path_prefix on unfreeze. We instead save the current value. --- library/lib.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'library') diff --git a/library/lib.ml b/library/lib.ml index 4fd29a94de..1531d408f6 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -561,7 +561,7 @@ let close_section () = (* State and initialization. *) -type frozen = Names.DirPath.t option * library_segment +type frozen = Names.DirPath.t option * library_segment * (Names.DirPath.t * (Names.module_path * Names.DirPath.t)) let freeze ~marshallable = match marshallable with @@ -579,17 +579,17 @@ let freeze ~marshallable = | n, ClosedSection _ -> Some (n,ClosedSection []) | _, FrozenState _ -> None) !lib_stk in - !comp_name, lib_stk + !comp_name, lib_stk, !path_prefix | _ -> - !comp_name, !lib_stk + !comp_name, !lib_stk, !path_prefix -let unfreeze (mn,stk) = +let unfreeze (mn,stk,path_prfx) = comp_name := mn; lib_stk := stk; - recalc_path_prefix () + path_prefix := path_prfx let init () = - unfreeze (None,[]); + unfreeze (None,[],initial_prefix); Summary.init_summaries (); add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *) -- cgit v1.2.3 From addc1304de75800fa9301e97d3ae78539f511959 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Mar 2017 00:32:53 +0100 Subject: [library] Refactor state handling. This part of state is critical. We refactor it and make it into a record to ease handling. --- library/lib.ml | 84 +++++++++++++++++++++++++++++++--------------------------- 1 file changed, 45 insertions(+), 39 deletions(-) (limited to 'library') diff --git a/library/lib.ml b/library/lib.ml index 1531d408f6..ddd2ed6afa 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -97,21 +97,30 @@ let segment_of_objects prefix = let initial_prefix = default_library,(Names.initial_path,Names.DirPath.empty) -let lib_stk = ref ([] : library_segment) +type lib_state = { + comp_name : Names.DirPath.t option; + lib_stk : library_segment; + path_prefix : Names.DirPath.t * (Names.module_path * Names.DirPath.t); +} -let comp_name = ref None +let initial_lib_state = { + comp_name = None; + lib_stk = []; + path_prefix = initial_prefix; +} + +let lib_state = ref initial_lib_state let library_dp () = - match !comp_name with Some m -> m | None -> default_library + match !lib_state.comp_name with Some m -> m | None -> default_library (* [path_prefix] is a pair of absolute dirpath and a pair of current module path and relative section path *) -let path_prefix = ref initial_prefix -let cwd () = fst !path_prefix -let current_prefix () = snd !path_prefix -let current_mp () = fst (snd !path_prefix) -let current_sections () = snd (snd !path_prefix) +let cwd () = fst !lib_state.path_prefix +let current_prefix () = snd !lib_state.path_prefix +let current_mp () = fst (snd !lib_state.path_prefix) +let current_sections () = snd (snd !lib_state.path_prefix) let sections_depth () = List.length (Names.DirPath.repr (current_sections ())) let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ())) @@ -132,7 +141,7 @@ let make_kn id = let mp,dir = current_prefix () in Names.make_kn mp dir (Names.Label.of_id id) -let make_oname id = Libnames.make_oname !path_prefix id +let make_oname id = Libnames.make_oname !lib_state.path_prefix id let recalc_path_prefix () = let rec recalc = function @@ -142,18 +151,18 @@ let recalc_path_prefix () = | _::l -> recalc l | [] -> initial_prefix in - path_prefix := recalc !lib_stk + lib_state := { !lib_state with path_prefix = recalc !lib_state.lib_stk } let pop_path_prefix () = - let dir,(mp,sec) = !path_prefix in - path_prefix := pop_dirpath dir, (mp, pop_dirpath sec) + let dir,(mp,sec) = !lib_state.path_prefix in + lib_state := { !lib_state with path_prefix = pop_dirpath dir, (mp, pop_dirpath sec)} let find_entry_p p = let rec find = function | [] -> raise Not_found | ent::l -> if p ent then ent else find l in - find !lib_stk + find !lib_state.lib_stk let split_lib_gen test = let rec collect after equal = function @@ -174,7 +183,7 @@ let split_lib_gen test = | _ -> findeq (hd::after) before) | [] -> None in - match findeq [] !lib_stk with + match findeq [] !lib_state.lib_stk with | None -> error "no such entry" | Some r -> r @@ -199,10 +208,10 @@ let split_lib_at_opening sp = (* Adding operations. *) let add_entry sp node = - lib_stk := (sp,node) :: !lib_stk + lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk } let pull_to_head oname = - lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk + lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk } let anonymous_id = let n = ref 0 in @@ -277,7 +286,7 @@ let start_mod is_type export id mp fs = if exists then user_err ~hdr:"open_module" (pr_id id ++ str " already exists"); add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs)); - path_prefix := prefix; + lib_state := { !lib_state with path_prefix = prefix} ; prefix let start_module = start_mod false @@ -299,16 +308,16 @@ let end_mod is_type = with Not_found -> error "No opened modules." in let (after,mark,before) = split_lib_at_opening oname in - lib_stk := before; + lib_state := { !lib_state with lib_stk = before }; add_entry oname (ClosedModule (List.rev (mark::after))); - let prefix = !path_prefix in + let prefix = !lib_state.path_prefix in recalc_path_prefix (); (oname, prefix, fs, after) let end_module () = end_mod false let end_modtype () = end_mod true -let contents () = !lib_stk +let contents () = !lib_state.lib_stk let contents_after sp = let (after,_,_) = split_lib sp in after @@ -316,14 +325,14 @@ let contents_after sp = let (after,_,_) = split_lib sp in after (* TODO: use check_for_module ? *) let start_compilation s mp = - if !comp_name != None then + if !lib_state.comp_name != None then error "compilation unit is already started"; if not (Names.DirPath.is_empty (current_sections ())) then error "some sections are already opened"; let prefix = s, (mp, Names.DirPath.empty) in let () = add_anonymous_entry (CompilingLibrary prefix) in - comp_name := Some s; - path_prefix := prefix + lib_state := { !lib_state with comp_name = Some s; + path_prefix = prefix } let end_compilation_checks dir = let _ = @@ -344,7 +353,7 @@ let end_compilation_checks dir = with Not_found -> anomaly (Pp.str "No module declared") in let _ = - match !comp_name with + match !lib_state.comp_name with | None -> anomaly (Pp.str "There should be a module name...") | Some m -> if not (Names.DirPath.equal m dir) then anomaly @@ -355,8 +364,8 @@ let end_compilation_checks dir = let end_compilation oname = let (after,mark,before) = split_lib_at_opening oname in - comp_name := None; - !path_prefix,after + lib_state := { !lib_state with comp_name = None }; + !lib_state.path_prefix,after (* Returns true if we are inside an opened module or module type *) @@ -514,7 +523,7 @@ let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore () let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore () let open_section id = - let olddir,(mp,oldsec) = !path_prefix in + let olddir,(mp,oldsec) = !lib_state.path_prefix in let dir = add_dirpath_suffix olddir id in let prefix = dir, (mp, add_dirpath_suffix oldsec id) in if Nametab.exists_section dir then @@ -523,7 +532,7 @@ let open_section id = add_entry (make_oname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); - path_prefix := prefix; + lib_state := { !lib_state with path_prefix = prefix }; if !Flags.xml_export then Hook.get f_xml_open_section id; add_section () @@ -549,8 +558,8 @@ let close_section () = error "No opened section." in let (secdecls,mark,before) = split_lib_at_opening oname in - lib_stk := before; - let full_olddir = fst !path_prefix in + lib_state := { !lib_state with lib_stk = before }; + let full_olddir = fst !lib_state.path_prefix in pop_path_prefix (); add_entry oname (ClosedSection (List.rev (mark::secdecls))); if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname)); @@ -561,7 +570,7 @@ let close_section () = (* State and initialization. *) -type frozen = Names.DirPath.t option * library_segment * (Names.DirPath.t * (Names.module_path * Names.DirPath.t)) +type frozen = lib_state let freeze ~marshallable = match marshallable with @@ -578,18 +587,15 @@ let freeze ~marshallable = Some(n,OpenedSection(op,Summary.empty_frozen)) | n, ClosedSection _ -> Some (n,ClosedSection []) | _, FrozenState _ -> None) - !lib_stk in - !comp_name, lib_stk, !path_prefix + !lib_state.lib_stk in + { !lib_state with lib_stk } | _ -> - !comp_name, !lib_stk, !path_prefix + !lib_state -let unfreeze (mn,stk,path_prfx) = - comp_name := mn; - lib_stk := stk; - path_prefix := path_prfx +let unfreeze st = lib_state := st let init () = - unfreeze (None,[],initial_prefix); + unfreeze initial_lib_state; Summary.init_summaries (); add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *) -- cgit v1.2.3 From 7601ddc3500cae2da39883b339951205be19c41d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 03:48:50 +0100 Subject: [safe_string] library/nameops We add a more convenient API to create identifiers from mutable strings. We cannot solve the `String.copy` deprecation problem until we enable `-safe-string`. --- library/nameops.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'library') diff --git a/library/nameops.ml b/library/nameops.ml index 6020db33d9..098f5112fd 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -61,7 +61,7 @@ let make_ident sa = function if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n) else sa ^ "_" ^ (string_of_int n) in Id.of_string s - | None -> Id.of_string (String.copy sa) + | None -> Id.of_string sa let root_of_id id = let suffixstart = cut_ident true id in @@ -92,20 +92,20 @@ let increment_subscript id = add (carrypos-1) end else begin - let newid = String.copy id in - String.fill newid (carrypos+1) (len-1-carrypos) '0'; - newid.[carrypos] <- Char.chr (Char.code c + 1); + let newid = Bytes.of_string id in + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid carrypos (Char.chr (Char.code c + 1)); newid end else begin - let newid = id^"0" in + let newid = Bytes.of_string (id^"0") in if carrypos < len-1 then begin - String.fill newid (carrypos+1) (len-1-carrypos) '0'; - newid.[carrypos+1] <- '1' + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid (carrypos+1) '1' end; newid end - in Id.of_string (add (len-1)) + in Id.of_bytes (add (len-1)) let has_subscript id = let id = Id.to_string id in @@ -113,9 +113,9 @@ let has_subscript id = let forget_subscript id = let numstart = cut_ident false id in - let newid = String.make (numstart+1) '0' in + let newid = Bytes.make (numstart+1) '0' in String.blit (Id.to_string id) 0 newid 0 numstart; - (Id.of_string newid) + (Id.of_bytes newid) let add_suffix id s = Id.of_string (Id.to_string id ^ s) let add_prefix s id = Id.of_string (s ^ Id.to_string id) -- cgit v1.2.3 From f0341076aa60a84177a6b46db0d8d50df220536b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 6 Dec 2016 17:16:16 +0100 Subject: [error] Move back fatal_error to toplevel This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09 (the mllib dependencies that should be surely tweaked more). The logic for `fatal_error` has no place in `CErrors`, this is coqtop-specific code. What is more, a libobject caller should handle the exception correctly, I fail to see why the fix was needed on the first place. --- library/libobject.ml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) (limited to 'library') diff --git a/library/libobject.ml b/library/libobject.ml index caa03c85be..8757ca08c6 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -91,16 +91,8 @@ let declare_object_full odecl = dyn_rebuild_function = rebuild }; (infun,outfun) -(* The "try .. with .. " allows for correct printing when calling - declare_object a loading time. -*) - -let declare_object odecl = - try fst (declare_object_full odecl) - with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e) -let declare_object_full odecl = - try declare_object_full odecl - with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e) +let declare_object odecl = fst (declare_object_full odecl) +let declare_object_full odecl = declare_object_full odecl (* this function describes how the cache, load, open, and export functions are triggered. *) -- cgit v1.2.3 From 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Dec 2016 12:12:54 +0100 Subject: [pp] [ide] Minor cleanups in pp code. - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics. --- library/summary.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/summary.ml b/library/summary.ml index 6efa07f388..2ec4760d64 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -107,8 +107,10 @@ let unfreeze_summaries fs = try fold id decl state with e when CErrors.noncritical e -> let e = CErrors.push e in - Printf.eprintf "Error unfrezing summay %s\n%s\n%!" - (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e)); + Feedback.msg_error + Pp.(seq [str "Error unfrezing summay %s\n%s\n%!"; + str (name_of_summary id); + CErrors.iprint e]); iraise e in (** We rely on the order of the frozen list, and the order of folding *) -- cgit v1.2.3