From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/decl_kinds.ml | 2 +- library/decl_kinds.mli | 2 +- library/declare.ml | 16 +-- library/declare.mli | 4 +- library/declaremods.ml | 334 +++++++++++++++++++++---------------------- library/declaremods.mli | 22 +-- library/decls.ml | 2 +- library/decls.mli | 2 +- library/dischargedhypsmap.ml | 4 +- library/global.ml | 20 +-- library/global.mli | 8 +- library/goptions.ml | 74 +++++----- library/goptions.mli | 10 +- library/heads.ml | 22 +-- library/impargs.ml | 96 ++++++------- library/impargs.mli | 8 +- library/lib.ml | 172 +++++++++++----------- library/lib.mli | 12 +- library/libnames.ml | 30 ++-- library/libnames.mli | 8 +- library/libobject.ml | 50 +++---- library/libobject.mli | 20 +-- library/library.ml | 80 +++++------ library/library.mllib | 2 +- library/nameops.ml | 32 ++--- library/nametab.ml | 132 ++++++++--------- library/nametab.mli | 22 +-- library/states.ml | 4 +- library/states.mli | 4 +- library/summary.ml | 10 +- 30 files changed, 602 insertions(+), 602 deletions(-) (limited to 'library') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 03b14e31c..5fd27f467 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -44,7 +44,7 @@ type definition_object_kind = type assumption_object_kind = Definitional | Logical | Conjectural -(* [assumption_kind] +(* [assumption_kind] | Local | Global ------------------------------------ diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index e42cb9621..0ebab9ca0 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -44,7 +44,7 @@ type definition_object_kind = type assumption_object_kind = Definitional | Logical | Conjectural -(* [assumption_kind] +(* [assumption_kind] | Local | Global ------------------------------------ diff --git a/library/declare.ml b/library/declare.ml index 44536ce5b..49b7d7ba2 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -62,7 +62,7 @@ let cache_variable ((sp,_),o) = let cst = Global.push_named_assum (id,ty) in let impl = if impl then Lib.Implicit else Lib.Explicit in impl, true, cst - | SectionLocalDef (c,t,opaq) -> + | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in Lib.Explicit, opaq, cst in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); @@ -98,7 +98,7 @@ type constant_declaration = constant_entry * logical_kind (* section (if Remark or Fact) is needed to access a construction *) let load_constant i ((sp,kn),(_,_,kind)) = if Nametab.exists_cci sp then - errorlabstrm "cache_constant" + errorlabstrm "cache_constant" (pr_id (basename sp) ++ str " already exists"); Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn)); add_constant_kind (constant_of_kn kn) kind @@ -150,7 +150,7 @@ let (inConstant,_) = classify_function = classify_constant; subst_function = ident_subst_function; discharge_function = discharge_constant; - export_function = export_constant } + export_function = export_constant } let hcons_constant_declaration = function | DefinitionEntry ce when !Flags.hash_cons_proofs -> @@ -158,7 +158,7 @@ let hcons_constant_declaration = function DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; const_entry_type = Option.map hcons1_constr ce.const_entry_type; - const_entry_opaque = ce.const_entry_opaque; + const_entry_opaque = ce.const_entry_opaque; const_entry_boxed = ce.const_entry_boxed } | cd -> cd @@ -190,14 +190,14 @@ let declare_inductive_argument_scopes kn mie = let inductive_names sp kn mie = let (dp,_) = repr_path sp in - let names, _ = + let names, _ = List.fold_left (fun (names, n) ind -> let ind_p = (kn,n) in let names, _ = List.fold_left (fun (names, p) l -> - let sp = + let sp = Libnames.make_path dp l in ((sp, ConstructRef (ind_p,p)) :: names, p+1)) @@ -262,14 +262,14 @@ let dummy_inductive_entry (_,m) = ([],{ let export_inductive x = Some (dummy_inductive_entry x) let (inInductive,_) = - declare_object {(default_object "INDUCTIVE") with + declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; open_function = open_inductive; classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; discharge_function = discharge_inductive; - export_function = export_inductive } + export_function = export_inductive } (* for initial declaration *) let declare_mind isrecord mie = diff --git a/library/declare.mli b/library/declare.mli index 94457a9f8..1a68f8e20 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -21,11 +21,11 @@ open Nametab open Decl_kinds (*i*) -(* This module provides the official functions to declare new variables, +(* This module provides the official functions to declare new variables, parameters, constants and inductive types. Using the following functions will add the entries in the global environment (module [Global]), will register the declarations in the library (module [Lib]) --- so that the - reset works properly --- and will fill some global tables such as + reset works properly --- and will fill some global tables such as [Nametab] and [Impargs]. *) open Nametab diff --git a/library/declaremods.ml b/library/declaremods.ml index 6275c4b77..37ee34d1f 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -40,63 +40,63 @@ open Mod_subst therefore must be substitued with valid names before use. *) -type substitutive_objects = +type substitutive_objects = substitution * mod_bound_id list * mod_self_id * lib_objects (* For each module, we store the following things: - In modtab_substobjs: substitutive_objects - when we will do Module M:=N, the objects of N will be reloaded + In modtab_substobjs: substitutive_objects + when we will do Module M:=N, the objects of N will be reloaded with M after substitution In modtab_objects: "substituted objects" @ "keep objects" - substituted objects - - roughly the objects above after the substitution - we need to + substituted objects - + roughly the objects above after the substitution - we need to keep them to call open_object when the module is opened (imported) - + keep objects - - The list of non-substitutive objects - as above, for each of - them we will call open_object when the module is opened - + The list of non-substitutive objects - as above, for each of + them we will call open_object when the module is opened + (Some) Invariants: * If the module is a functor, the two latter lists are empty. - * Module objects in substitutive_objects part have empty substituted + * Module objects in substitutive_objects part have empty substituted objects. - * Modules which where created with Module M:=mexpr or with + * Modules which where created with Module M:=mexpr or with Module M:SIG. ... End M. have the keep list empty. *) -let modtab_substobjs = +let modtab_substobjs = ref (MPmap.empty : substitutive_objects MPmap.t) -let modtab_objects = +let modtab_objects = ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t) (* currently started interactive module (if any) - its arguments (if it is a functor) and declared output type *) -let openmod_info = - ref (([],None,None) : mod_bound_id list * module_struct_entry option - * struct_expr_body option) +let openmod_info = + ref (([],None,None) : mod_bound_id list * module_struct_entry option + * struct_expr_body option) (* The library_cache here is needed to avoid recalculations of substituted modules object during "reloading" of libraries *) let library_cache = ref Dirmap.empty let _ = Summary.declare_summary "MODULE-INFO" - { Summary.freeze_function = (fun () -> + { Summary.freeze_function = (fun () -> !modtab_substobjs, !modtab_objects, !openmod_info, !library_cache); - Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) -> + Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) -> modtab_substobjs := sobjs; modtab_objects := objs; openmod_info := info; library_cache := libcache); - Summary.init_function = (fun () -> + Summary.init_function = (fun () -> modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; openmod_info := ([],None,None); @@ -105,14 +105,14 @@ let _ = Summary.declare_summary "MODULE-INFO" (* auxiliary functions to transform full_path and kernel_name given by Lib into module_path and dir_path needed for modules *) -let mp_of_kn kn = - let mp,sec,l = repr_kn kn in - if sec=empty_dirpath then - MPdot (mp,l) +let mp_of_kn kn = + let mp,sec,l = repr_kn kn in + if sec=empty_dirpath then + MPdot (mp,l) else anomaly ("Non-empty section in module name!" ^ string_of_kn kn) -let dir_of_sp sp = +let dir_of_sp sp = let dir,id = repr_path sp in add_dirpath_suffix dir id @@ -120,34 +120,34 @@ let msid_of_mp = function MPself msid -> msid | _ -> anomaly "'Self' module path expected!" -let msid_of_prefix (_,(mp,sec)) = - if sec=empty_dirpath then +let msid_of_prefix (_,(mp,sec)) = + if sec=empty_dirpath then msid_of_mp mp else - anomaly ("Non-empty section in module name!" ^ + anomaly ("Non-empty section in module name!" ^ string_of_mp mp ^ "." ^ string_of_dirpath sec) let scrape_alias mp = Environ.scrape_alias mp (Global.env()) - + (* This function checks if the type calculated for the module [mp] is a subtype of [sub_mtb]. Uses only the global environment. *) let check_subtypes mp sub_mtb = let env = Global.env () in let mtb = Environ.lookup_modtype mp env in - let sub_mtb = + let sub_mtb = {typ_expr = sub_mtb; typ_strength = None; typ_alias = empty_subst} in - let _ = Environ.add_constraints - (Subtyping.check_subtypes env mtb sub_mtb) + let _ = Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) in - () (* The constraints are checked and forgot immediately! *) + () (* The constraints are checked and forgot immediately! *) let compute_subst_objects mp (subst,mbids,msid,objs) = match mbids with - | [] -> + | [] -> let subst' = join_alias (map_msid msid mp) subst in Some (join (map_msid msid mp) (join subst' subst), objs) | _ -> @@ -164,15 +164,15 @@ let subst_substobjs dir mp substobjs = through its components. They are called by plenty module functions *) let compute_visibility exists what i dir dirinfo = - if exists then - if - try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo - with Not_found -> false + if exists then + if + try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo + with Not_found -> false then Nametab.Exactly i else errorlabstrm (what^"_module") - (pr_dirpath dir ++ str " should already exist!") + (pr_dirpath dir ++ str " should already exist!") else if Nametab.exists_dir dir then errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists") @@ -202,12 +202,12 @@ let do_module exists what iter_objects i dir mp substobjs objects = Nametab.push_dir vis dir dirinfo; modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs; match objects with - Some seg -> + Some seg -> modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects; - iter_objects (i+1) prefix seg + iter_objects (i+1) prefix seg | None -> () -let conv_names_do_module exists what iter_objects i +let conv_names_do_module exists what iter_objects i (sp,kn) substobjs substituted = let dir,mp = dir_of_sp sp, mp_of_kn kn in do_module exists what iter_objects i dir mp substobjs substituted @@ -222,19 +222,19 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = | None -> anomaly "You must not recache interactive modules!" | Some (me,sub_mte_o) -> - let sub_mtb_o = match sub_mte_o with + let sub_mtb_o = match sub_mte_o with None -> None | Some mte -> Some (Mod_typing.translate_struct_entry (Global.env()) mte) in - + let mp = Global.add_module (basename sp) me in if mp <> mp_of_kn kn then anomaly "Kernel and Library names do not match"; - + match sub_mtb_o with None -> () - | Some (sub_mtb,sub) -> + | Some (sub_mtb,sub) -> check_subtypes mp sub_mtb in @@ -246,7 +246,7 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = (* TODO: This check is not essential *) let check_empty s = function | None -> () - | Some _ -> + | Some _ -> anomaly ("We should never have full info in " ^ s^"!") @@ -302,9 +302,9 @@ let (in_module,out_module) = let rec replace_alias modalias_obj obj = let rec put_alias (id_alias,obj_alias) l = - match l with + match l with [] -> [] - | (id,o)::r + | (id,o)::r when ( object_tag o = "MODULE") -> if id = id_alias then (* let (entry,subst_o,substed_o) = out_module_alias obj_alias in @@ -312,7 +312,7 @@ let rec replace_alias modalias_obj obj = begin match substed_o,substed_o' with Some a,Some b -> - (id,in_module_alias + (id,in_module_alias (entry,subst_o',Some (dump_alias_object a b)))::r*) (id_alias,obj_alias)::r (* | _,_ -> (id,o)::r @@ -324,20 +324,20 @@ let rec replace_alias modalias_obj obj = | [] -> list_obj | o::r ->choose_obj_alias r (put_alias o list_obj) in choose_obj_alias modalias_obj obj - + and dump_alias_object alias_obj obj = let rec alias_in_obj seg = match seg with | [] -> [] - | (id,o)::r when (object_tag o = "MODULE ALIAS") -> + | (id,o)::r when (object_tag o = "MODULE ALIAS") -> (id,o)::(alias_in_obj r) | e::r -> (alias_in_obj r) in let modalias_obj = alias_in_obj alias_obj in replace_alias modalias_obj obj - + and do_module_alias exists what iter_objects i dir mp alias substobjs objects = let prefix = (dir,(alias,empty_dirpath)) in - let alias_objects = + let alias_objects = try Some (MPmap.find alias !modtab_objects) with Not_found -> None in let dirinfo = DirModule (dir,(mp,empty_dirpath)) in @@ -345,10 +345,10 @@ and do_module_alias exists what iter_objects i dir mp alias substobjs objects = Nametab.push_dir vis dir dirinfo; modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs; match alias_objects,objects with - Some (_,seg), Some seg' -> + Some (_,seg), Some seg' -> let new_seg = dump_alias_object seg seg' in modtab_objects := MPmap.add mp (prefix,new_seg) !modtab_objects; - iter_objects (i+1) prefix new_seg + iter_objects (i+1) prefix new_seg | _,_-> () and cache_module_alias ((sp,kn),(entry,substobjs,substituted)) = @@ -356,36 +356,36 @@ and cache_module_alias ((sp,kn),(entry,substobjs,substituted)) = | None -> anomaly "You must not recache interactive modules!" | Some (me,sub_mte_o) -> - let sub_mtb_o = match sub_mte_o with + let sub_mtb_o = match sub_mte_o with None -> None | Some mte -> Some (Mod_typing.translate_struct_entry (Global.env()) mte) in - let mp' = match me with + let mp' = match me with | {mod_entry_type = None; mod_entry_expr = Some (MSEident mp)} -> - Global.add_alias (basename sp) mp + Global.add_alias (basename sp) mp | _ -> anomaly "cache module alias" in if mp' <> mp_of_kn kn then anomaly "Kernel and Library names do not match"; - + let _ = match sub_mtb_o with None -> () - | Some (sub_mtb,sub) -> + | Some (sub_mtb,sub) -> check_subtypes mp' sub_mtb in match me with | {mod_entry_type = None; mod_entry_expr = Some (MSEident mp)} -> - dir_of_sp sp,mp_of_kn kn,scrape_alias mp + dir_of_sp sp,mp_of_kn kn,scrape_alias mp | _ -> anomaly "cache module alias" in do_module_alias false "cache" load_objects 1 dir mp alias substobjs substituted and load_module_alias i ((sp,kn),(entry,substobjs,substituted)) = - let dir,mp,alias= - match entry with + let dir,mp,alias= + match entry with | Some (me,_)-> begin match me with @@ -400,7 +400,7 @@ and load_module_alias i ((sp,kn),(entry,substobjs,substituted)) = and open_module_alias i ((sp,kn),(entry,substobjs,substituted)) = let dir,mp,alias= - match entry with + match entry with | Some (me,_)-> begin match me with @@ -423,7 +423,7 @@ and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = let substobjs = (subst',mbids,msid,objs) in (* if we are not a functor - calculate substitued. We add "msid |-> mp" to the substitution *) - match entry with + match entry with | Some (me,sub)-> begin match me with @@ -432,46 +432,46 @@ and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = let mp' = subst_mp subst' mp' in let mp' = scrape_alias mp' in (Some ({mod_entry_type = None; - mod_entry_expr = + mod_entry_expr = Some (MSEident mp')},sub), substobjs, match mbids with | [] -> let subst = update_subst subst' (map_mp mp' mp) in - Some (subst_objects (dir,(mp',empty_dirpath)) + Some (subst_objects (dir,(mp',empty_dirpath)) (join (join subst' subst) (join (map_msid msid mp') (map_mp mp mp'))) objs) | _ -> None) - + | _ -> anomaly "Modops: Not an alias" end | None -> anomaly "Modops: Empty info" and classify_module_alias (entry,substobjs,_) = Substitute (entry,substobjs,None) - + let (in_module_alias,out_module_alias) = declare_object {(default_object "MODULE ALIAS") with cache_function = cache_module_alias; open_function = open_module_alias; classify_function = classify_module_alias; subst_function = subst_module_alias; - load_function = load_module_alias; + load_function = load_module_alias; export_function = (fun _ -> anomaly "No modules in sections!") } - + let cache_keep _ = anomaly "This module should not be cached!" -let load_keep i ((sp,kn),seg) = +let load_keep i ((sp,kn),seg) = let mp = mp_of_kn kn in let prefix = dir_of_sp sp, (mp,empty_dirpath) in - begin + begin try let prefix',objects = MPmap.find mp !modtab_objects in - if prefix' <> prefix then + if prefix' <> prefix then anomaly "Two different modules with the same path!"; modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects; with @@ -479,7 +479,7 @@ let load_keep i ((sp,kn),seg) = end; load_objects i prefix seg -let open_keep i ((sp,kn),seg) = +let open_keep i ((sp,kn),seg) = let dirpath,mp = dir_of_sp sp, mp_of_kn kn in open_objects i (dirpath,(mp,empty_dirpath)) seg @@ -514,7 +514,7 @@ let _ = Summary.declare_summary "MODTYPE-INFO" let cache_modtype ((sp,kn),(entry,modtypeobjs)) = - let _ = + let _ = match entry with | None -> anomaly "You must not recache interactive module types!" @@ -541,18 +541,18 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs)) = (pr_path sp ++ str " already exists") ; Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn); - + modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab let open_modtype i ((sp,kn),(entry,_)) = check_empty "open_modtype" entry; - if - try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn) + if + try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn) with Not_found -> true then - errorlabstrm ("open_modtype") + errorlabstrm ("open_modtype") (pr_path sp ++ str " should already exist!"); Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) @@ -581,12 +581,12 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp = let rec mp_rec = function | [] -> MPself msid | i::r -> MPdot(mp_rec r,label_of_id i) - in - if mbids<>[] then + in + if mbids<>[] then error "Unexpected functor objects" else - let rec replace_idl = function - | _,[] -> [] + let rec replace_idl = function + | _,[] -> [] | id::idl,(id',obj)::tail when id = id' -> let tag = object_tag obj in if tag = "MODULE" or tag ="MODULE ALIAS" then @@ -608,7 +608,7 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp = | idl,lobj::tail -> lobj::replace_idl (idl,tail) in (join (map_mp (mp_rec (List.rev idl)) mp) subst, mbids, msid, replace_idl (idl,lib_stack)) - + let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) = (subst, mbids1@mbids2, msid, lib_stack) @@ -618,19 +618,19 @@ let rec get_modtype_substobjs env = function let (subst, mbids, msid, objs) = get_modtype_substobjs env mte in (subst, mbid::mbids, msid, objs) | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty - | MSEwith (mty, With_Module (idl,mp)) -> + | MSEwith (mty, With_Module (idl,mp)) -> let substobjs = get_modtype_substobjs env mty in let mp = Environ.scrape_alias mp env in let modobjs = MPmap.find mp !modtab_substobjs in replace_module_object idl substobjs modobjs mp | MSEapply (mexpr, MSEident mp) -> let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in - let farg_id, farg_b, fbody_b = Modops.destr_functor env + let farg_id, farg_b, fbody_b = Modops.destr_functor env (Modops.eval_struct env ftb) in let mp = Environ.scrape_alias mp env in let sub_alias = (Environ.lookup_modtype mp env).typ_alias in let sub_alias = match Modops.eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> join_alias + | SEBstruct (msid,sign) -> join_alias (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in @@ -650,7 +650,7 @@ let rec get_modtype_substobjs env = function let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in (* application outside the kernel, only for substitutive objects (that are all non-logical objects) *) - ((join + ((join (join subst sub3) (map_mbid mbid mp (Some resolve))) , mbids, msid, objs) @@ -660,7 +660,7 @@ let rec get_modtype_substobjs env = function | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr - + (* push names of bound modules (and their components) to Nametab *) (* add objects associated to them *) let process_module_bindings argids args = @@ -672,14 +672,14 @@ let process_module_bindings argids args = in List.iter2 process_arg argids args -let intern_args interp_modtype (idl,arg) = +let intern_args interp_modtype (idl,arg) = let lib_dir = Lib.library_dp() in let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in let mty = interp_modtype (Global.env()) arg in let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in let substobjs = get_modtype_substobjs (Global.env()) mty in List.map2 - (fun dir mbid -> + (fun dir mbid -> Global.add_module_parameter mbid mty; let mp = MPbound mbid in ignore (do_load_and_subst_module 1 dir mp substobjs []); @@ -701,9 +701,9 @@ let start_module interp_modtype export id args res_o = Some mte, None else let mtb,_ = Mod_typing.translate_struct_entry (Global.env()) mte in - let sub_mtb = - List.fold_right - (fun (arg_id,arg_t) mte -> + let sub_mtb = + List.fold_right + (fun (arg_id,arg_t) mte -> let arg_t,sub = Mod_typing.translate_struct_entry (Global.env()) arg_t in let arg_t = {typ_expr = arg_t; @@ -733,13 +733,13 @@ let end_module () = let substobjs, keep, special = try match res_o with - | None -> + | None -> (empty_subst, mbids, msid, substitute), keep, special | Some (MSEident ln) -> abstract_substobjs mbids (MPmap.find ln (!modtypetab)), [], [] | Some (MSEwith _ as mty) -> abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] - | Some (MSEfunctor _) -> + | Some (MSEfunctor _) -> anomaly "Funsig cannot be here..." | Some (MSEapply _ as mty) -> abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] @@ -759,8 +759,8 @@ let end_module () = let substituted = subst_substobjs dir mp substobjs in let node = in_module (None,substobjs,substituted) in - let objects = - if keep = [] || mbids <> [] then + let objects = + if keep = [] || mbids <> [] then special@[node] (* no keep objects or we are defining a functor *) else special@[node;in_modkeep keep] (* otherwise *) @@ -769,7 +769,7 @@ let end_module () = if (fst newoname) <> (fst oldoname) then anomaly "Names generated on start_ and end_module do not match"; - if mp_of_kn (snd newoname) <> mp then + if mp_of_kn (snd newoname) <> mp then anomaly "Kernel and Library names do not match"; Lib.add_frozen_state () (* to prevent recaching *); @@ -777,7 +777,7 @@ let end_module () = -let module_objects mp = +let module_objects mp = let prefix,objects = MPmap.find mp !modtab_objects in segment_of_objects prefix objects @@ -789,13 +789,13 @@ let module_objects mp = type library_name = dir_path (* The first two will form substitutive_objects, the last one is keep *) -type library_objects = +type library_objects = mod_self_id * lib_objects * lib_objects let register_library dir cenv objs digest = let mp = MPfile dir in - try + try ignore(Global.lookup_module mp); (* if it's in the environment, the cached objects should be correct *) let substobjs, objects = Dirmap.find dir !library_cache in @@ -809,7 +809,7 @@ let register_library dir cenv objs digest = let modobjs = substobjs, objects in library_cache := Dirmap.add dir modobjs !library_cache -let start_library dir = +let start_library dir = let mp = Global.start_library dir in openmod_info:=[],None,None; Lib.start_compilation dir mp; @@ -818,7 +818,7 @@ let start_library dir = let end_library_hook = ref ignore let set_end_library_hook f = end_library_hook := f -let end_library dir = +let end_library dir = !end_library_hook(); let prefix, lib_stack = Lib.end_compilation dir in let cenv = Global.export dir in @@ -830,24 +830,24 @@ let end_library dir = (* implementation of Export M and Import M *) -let really_import_module mp = +let really_import_module mp = let prefix,objects = MPmap.find mp !modtab_objects in open_objects 1 prefix objects -let cache_import (_,(_,mp)) = -(* for non-substitutive exports: +let cache_import (_,(_,mp)) = +(* for non-substitutive exports: let mp = Nametab.locate_module (qualid_of_dirpath dir) in *) really_import_module mp -let classify_import (export,_ as obj) = +let classify_import (export,_ as obj) = if export then Substitute obj else Dispose let subst_import (_,subst,(export,mp as obj)) = let mp' = subst_mp subst mp in if mp'==mp then obj else (export,mp') - + let (in_import,_) = declare_object {(default_object "IMPORT MODULE") with cache_function = cache_import; @@ -856,7 +856,7 @@ let (in_import,_) = classify_function = classify_import } -let import_module export mp = +let import_module export mp = Lib.add_anonymous_leaf (in_import (export,mp)) (************************************************************************) @@ -898,7 +898,7 @@ let end_modtype () = ln -let declare_modtype interp_modtype id args mty = +let declare_modtype interp_modtype id args mty = let fs = Summary.freeze_summaries () in try @@ -906,8 +906,8 @@ let declare_modtype interp_modtype id args mty = let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let base_mty = interp_modtype (Global.env()) mty in - let entry = - List.fold_right + let entry = + List.fold_right (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) arg_entries base_mty @@ -916,27 +916,27 @@ let declare_modtype interp_modtype id args mty = (* Undo the simulated interactive building of the module type *) (* and declare the module type as a whole *) Summary.unfreeze_summaries fs; - + ignore (add_leaf id (in_modtype (Some entry, substobjs))); mmp with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e - + let rec get_module_substobjs env = function - | MSEident mp -> MPmap.find mp !modtab_substobjs + | MSEident mp -> MPmap.find mp !modtab_substobjs | MSEfunctor (mbid,mty,mexpr) -> let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (subst, mbid::mbids, msid, objs) | MSEapply (mexpr, MSEident mp) -> let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in - let farg_id, farg_b, fbody_b = Modops.destr_functor env + let farg_id, farg_b, fbody_b = Modops.destr_functor env (Modops.eval_struct env ftb) in let mp = Environ.scrape_alias mp env in let sub_alias = (Environ.lookup_modtype mp env).typ_alias in let sub_alias = match Modops.eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> join_alias + | SEBstruct (msid,sign) -> join_alias (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in @@ -956,7 +956,7 @@ let rec get_module_substobjs env = function let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in (* application outside the kernel, only for substitutive objects (that are all non-logical objects) *) - ((join + ((join (join subst sub3) (map_mbid mbid mp (Some resolve))) , mbids, msid, objs) @@ -966,7 +966,7 @@ let rec get_module_substobjs env = function | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty - | MSEwith (mty, With_Module (idl,mp)) -> + | MSEwith (mty, With_Module (idl,mp)) -> let substobjs = get_module_substobjs env mty in let modobjs = MPmap.find mp !modtab_substobjs in replace_module_object idl substobjs modobjs mp @@ -984,9 +984,9 @@ let rec subst_inc_expr subst me = let const1 = Mod_subst.from_val const in let force = Mod_subst.force subst_mps in MSEwith (subst_inc_expr subst me, - With_Definition(idl,force (subst_substituted + With_Definition(idl,force (subst_substituted subst const1))) - | MSEapply (me1,me2) -> + | MSEapply (me1,me2) -> MSEapply (subst_inc_expr subst me1, subst_inc_expr subst me2) | _ -> anomaly "You cannot Include a high-order structure" @@ -1001,16 +1001,16 @@ let cache_include (oname,((me,is_mod),substobjs,substituted)) = let prefix = (dir,(mp1,empty_dirpath)) in Global.add_include me; match substituted with - Some seg -> + Some seg -> load_objects 1 prefix seg; - open_objects 1 prefix seg; + open_objects 1 prefix seg; | None -> () - + let load_include i (oname,((me,is_mod),substobjs,substituted)) = let dir,mp1 = lift_oname oname in let prefix = (dir,(mp1,empty_dirpath)) in match substituted with - Some seg -> + Some seg -> load_objects i prefix seg | None -> () @@ -1018,11 +1018,11 @@ let open_include i (oname,((me,is_mod),substobjs,substituted)) = let dir,mp1 = lift_oname oname in let prefix = (dir,(mp1,empty_dirpath)) in match substituted with - Some seg -> + Some seg -> if is_mod then open_objects i prefix seg - else - if i = 1 then + else + if i = 1 then open_objects i prefix seg | None -> () @@ -1048,7 +1048,7 @@ let (in_include,out_include) = let rec update_include (sub,mbids,msid,objs) = let rec replace_include = function - | [] -> [] + | [] -> [] | (id,obj)::tail -> if object_tag obj = "INCLUDE" then let ((me,is_mod),substobjs,substituted) = out_include obj in @@ -1059,10 +1059,10 @@ let rec update_include (sub,mbids,msid,objs) = (id,obj)::(replace_include tail) in (sub,mbids,msid,replace_include objs) - - + + let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = - + let fs = Summary.freeze_summaries () in try @@ -1071,29 +1071,29 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = let mty_entry_o, mty_sub_o = match mty_o with None -> None, None - | (Some (mty, true)) -> - Some (List.fold_right + | (Some (mty, true)) -> + Some (List.fold_right (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) - arg_entries - (interp_modtype (Global.env()) mty)), + arg_entries + (interp_modtype (Global.env()) mty)), None - | (Some (mty, false)) -> - None, - Some (List.fold_right + | (Some (mty, false)) -> + None, + Some (List.fold_right (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) - arg_entries + arg_entries (interp_modtype (Global.env()) mty)) in let mexpr_entry_o = match mexpr_o with None -> None - | Some mexpr -> - Some (List.fold_right + | Some mexpr -> + Some (List.fold_right (fun (mbid,mte) me -> MSEfunctor(mbid,mte,me)) arg_entries (interp_modexpr (Global.env()) mexpr)) in - let entry = - {mod_entry_type = mty_entry_o; + let entry = + {mod_entry_type = mty_entry_o; mod_entry_expr = mexpr_entry_o } in let env = Global.env() in @@ -1107,23 +1107,23 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = (* Undo the simulated interactive building of the module *) (* and declare the module as a whole *) Summary.unfreeze_summaries fs; - match entry with - |{mod_entry_type = None; + match entry with + |{mod_entry_type = None; mod_entry_expr = Some (MSEident mp) } -> let dir,mp' = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in let (sub,mbids,msid,objs) = substobjs in let mp1 = Environ.scrape_alias mp env in let prefix = dir,(mp1,empty_dirpath) in - let substituted = + let substituted = match mbids with - | [] -> - Some (subst_objects prefix + | [] -> + Some (subst_objects prefix (join sub (join (map_msid msid mp1) (map_mp mp' mp1))) objs) | _ -> None in ignore (add_leaf id - (in_module_alias (Some ({mod_entry_type = None; - mod_entry_expr = Some (MSEident mp1) }, mty_sub_o), + (in_module_alias (Some ({mod_entry_type = None; + mod_entry_expr = Some (MSEident mp1) }, mty_sub_o), substobjs, substituted))); mmp | _ -> @@ -1136,20 +1136,20 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = id (in_module (Some (entry, mty_sub_o), substobjs, substituted))); mmp - - with e -> + + with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e - + let declare_include interp_struct me_ast is_mod = let fs = Summary.freeze_summaries () in - try + try let env = Global.env() in - let me = interp_struct env me_ast in - let substobjs = + let me = interp_struct env me_ast in + let substobjs = if is_mod then get_module_substobjs env me else @@ -1158,20 +1158,20 @@ let declare_include interp_struct me_ast is_mod = let dir = dir_of_sp (Lib.path_of_include()) in let substituted = subst_substobjs dir mp1 substobjs in let id = current_mod_id() in - + ignore (add_leaf id (in_include ((me,is_mod), substobjs, substituted))) - with e -> + with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e - - + + (*s Iterators. *) - + let iter_all_segments f = - let _ = - MPmap.iter - (fun _ (prefix,objects) -> + let _ = + MPmap.iter + (fun _ (prefix,objects) -> let apply_obj (id,obj) = f (make_oname prefix id) obj in List.iter apply_obj objects) !modtab_objects diff --git a/library/declaremods.mli b/library/declaremods.mli index 058bfa6ad..5cda0d28d 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -30,19 +30,19 @@ open Lib constructed by [interp_modtype] from functor arguments [fargs] and by [interp_modexpr] from [expr]. At least one of [typ], [expr] must be non-empty. - + The [bool] in [typ] tells if the module must be abstracted [true] with respect to the module type or merely matched without any restriction [false]. *) -val declare_module : +val declare_module : (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) -> - identifier -> - (identifier located list * 'modtype) list -> ('modtype * bool) option -> + identifier -> + (identifier located list * 'modtype) list -> ('modtype * bool) option -> 'modexpr option -> module_path - -val start_module : (env -> 'modtype -> module_struct_entry) -> + +val start_module : (env -> 'modtype -> module_struct_entry) -> bool option -> identifier -> (identifier located list * 'modtype) list -> ('modtype * bool) option -> module_path @@ -52,10 +52,10 @@ val end_module : unit -> module_path (*s Module types *) -val declare_modtype : (env -> 'modtype -> module_struct_entry) -> +val declare_modtype : (env -> 'modtype -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> 'modtype -> module_path -val start_modtype : (env -> 'modtype -> module_struct_entry) -> +val start_modtype : (env -> 'modtype -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> module_path val end_modtype : unit -> module_path @@ -73,8 +73,8 @@ type library_name = dir_path type library_objects -val register_library : - library_name -> +val register_library : + library_name -> Safe_typing.compiled_library -> library_objects -> Digest.t -> unit val start_library : library_name -> unit @@ -99,7 +99,7 @@ val import_module : bool -> module_path -> unit (* Include *) -val declare_include : (env -> 'struct_expr -> module_struct_entry) -> +val declare_include : (env -> 'struct_expr -> module_struct_entry) -> 'struct_expr -> bool -> unit (*s [iter_all_segments] iterate over all segments, the modules' diff --git a/library/decls.ml b/library/decls.ml index d5d0cb096..251c86aba 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -55,7 +55,7 @@ let constant_kind kn = Cmap.find kn !csttab let clear_proofs sign = List.fold_right - (fun (id,c,t as d) signv -> + (fun (id,c,t as d) signv -> let d = if variable_opacity id then (id,None,t) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val diff --git a/library/decls.mli b/library/decls.mli index 3ccff1f27..a9000604f 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -27,7 +27,7 @@ open Decl_kinds (** Registration and access to the table of variable *) -type variable_data = +type variable_data = dir_path * bool (* opacity *) * Univ.constraints * logical_kind val add_variable_data : variable -> variable_data -> unit diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index ed375a831..85de6ab8f 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -24,7 +24,7 @@ type discharged_hyps = full_path list let discharged_hyps_map = ref Spmap.empty -let set_discharged_hyps sp hyps = +let set_discharged_hyps sp hyps = discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map let get_discharged_hyps sp = @@ -42,7 +42,7 @@ let freeze () = !discharged_hyps_map let unfreeze dhm = discharged_hyps_map := dhm -let _ = +let _ = Summary.declare_summary "discharged_hypothesis" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; diff --git a/library/global.ml b/library/global.ml index ec41c0706..e228de23a 100644 --- a/library/global.ml +++ b/library/global.ml @@ -27,7 +27,7 @@ let env () = env_of_safe_env !global_env let env_is_empty () = is_empty !global_env -let _ = +let _ = declare_summary "Global environment" { freeze_function = (fun () -> !global_env); unfreeze_function = (fun fr -> global_env := fr); @@ -57,12 +57,12 @@ let push_named_def d = anomaly "Kernel names do not match." *) -let add_thing add dir id thing = +let add_thing add dir id thing = let kn, newenv = add dir (label_of_id id) thing !global_env in global_env := newenv; kn -let add_constant = add_thing add_constant +let add_constant = add_thing add_constant let add_mind = add_thing add_mind let add_modtype = add_thing (fun _ -> add_modtype) () let add_module = add_thing (fun _ -> add_module) () @@ -120,16 +120,16 @@ let lookup_modtype kn = lookup_modtype kn (env()) -let start_library dir = +let start_library dir = let mp,newenv = start_library dir !global_env in - global_env := newenv; + global_env := newenv; mp let export s = snd (export !global_env s) -let import cenv digest = - let mp,newenv = import cenv digest !global_env in - global_env := newenv; +let import cenv digest = + let mp,newenv = import cenv digest !global_env in + global_env := newenv; mp @@ -137,13 +137,13 @@ let import cenv digest = (*s Function to get an environment from the constants part of the global environment and a given context. *) -let env_of_context hyps = +let env_of_context hyps = reset_with_named_context hyps (env()) open Libnames let type_of_reference env = function - | VarRef id -> Environ.named_type id env + | VarRef id -> Environ.named_type id env | ConstRef c -> Typeops.type_of_constant env c | IndRef ind -> let specif = Inductive.lookup_mind_specif env ind in diff --git a/library/global.mli b/library/global.mli index deafacba2..3c2317122 100644 --- a/library/global.mli +++ b/library/global.mli @@ -44,9 +44,9 @@ val push_named_def : (identifier * constr * types option) -> Univ.constraints (*s Adding constants, inductives, modules and module types. All these functions verify that given names match those generated by kernel *) -val add_constant : +val add_constant : dir_path -> identifier -> global_declaration -> constant -val add_mind : +val add_mind : dir_path -> identifier -> mutual_inductive_entry -> kernel_name val add_module : identifier -> module_entry -> module_path @@ -59,7 +59,7 @@ val add_constraints : constraints -> unit val set_engagement : engagement -> unit (*s Interactive modules and module types *) -(* Both [start_*] functions take the [dir_path] argument to create a +(* Both [start_*] functions take the [dir_path] argument to create a [mod_self_id]. This should be the name of the compilation unit. *) (* [start_*] functions return the [module_path] valid for components @@ -91,7 +91,7 @@ val import : compiled_library -> Digest.t -> module_path (*s Function to get an environment from the constants part of the global * environment and a given context. *) - + val type_of_global : Libnames.global_reference -> types val env_of_context : Environ.named_context_val -> Environ.env diff --git a/library/goptions.ml b/library/goptions.ml index 86012b113..e4c5a6155 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -75,7 +75,7 @@ module MakeTable = let t = ref (MySet.empty : MySet.t) - let _ = + let _ = if A.synchronous then let freeze () = !t in let unfreeze c = t := c in @@ -91,7 +91,7 @@ module MakeTable = | GOadd -> t := MySet.add p !t | GOrmv -> t := MySet.remove p !t in let load_options i o = if i=1 then cache_options o in - let subst_options (_,subst,(f,p as obj)) = + let subst_options (_,subst,(f,p as obj)) = let p' = A.subst subst p in if p' == p then obj else (f,p') @@ -113,8 +113,8 @@ module MakeTable = (fun c -> t := MySet.remove c !t)) let print_table table_name printer table = - msg (str table_name ++ - (hov 0 + msg (str table_name ++ + (hov 0 (if MySet.is_empty table then str "None" ++ fnl () else MySet.fold (fun a b -> printer a ++ spc () ++ b) @@ -124,11 +124,11 @@ module MakeTable = object method add x = add_option (A.encode x) method remove x = remove_option (A.encode x) - method mem x = + method mem x = let y = A.encode x in let answer = MySet.mem y !t in msg (A.member_message y answer ++ fnl ()) - method print = print_table A.title A.printer !t + method print = print_table A.title A.printer !t end let _ = A.table := (nick,new table_of_A ())::!A.table @@ -181,7 +181,7 @@ sig val synchronous : bool end -module RefConvert = functor (A : RefConvertArg) -> +module RefConvert = functor (A : RefConvertArg) -> struct type t = A.t type key = reference @@ -208,7 +208,7 @@ type 'a option_sig = { optread : unit -> 'a; optwrite : 'a -> unit } -type option_type = bool * (unit -> value) -> (value -> unit) +type option_type = bool * (unit -> value) -> (value -> unit) module OptionMap = Map.Make (struct type t = option_name let compare = compare end) @@ -219,7 +219,7 @@ let value_tab = ref OptionMap.empty let get_option key = OptionMap.find key !value_tab -let check_key key = try +let check_key key = try let _ = get_option key in error "Sorry, this option name is already used" with Not_found -> @@ -231,25 +231,25 @@ open Summary open Libobject open Lib -let declare_option cast uncast +let declare_option cast uncast { optsync=sync; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in (* spiwack: I use two spaces in the nicknames of "local" and "global" objects. That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are lists of strings *without* spaces. *) - let (write,lwrite,gwrite) = if sync then + let (write,lwrite,gwrite) = if sync then let (ldecl_obj,_) = (* "Local": doesn't survive section or modules. *) declare_object {(default_object ("L "^nickname key)) with cache_function = (fun (_,v) -> write v); classify_function = (fun _ -> Dispose)} - in + in let (decl_obj,_) = (* default locality: survives sections but not modules. *) declare_object {(default_object (nickname key)) with cache_function = (fun (_,v) -> write v); classify_function = (fun _ -> Dispose); discharge_function = (fun (_,v) -> Some v)} - in + in let (gdecl_obj,_) = (* "Global": survives section and modules. *) declare_object {(default_object ("G "^nickname key)) with cache_function = (fun (_,v) -> write v); @@ -258,28 +258,28 @@ let declare_option cast uncast load_function = (fun _ (_,v) -> write v); (* spiwack: I'm unsure whether this function does anyting *) export_function = (fun v -> Some v)} - in - let _ = declare_summary (nickname key) + in + let _ = declare_summary (nickname key) { freeze_function = read; unfreeze_function = write; init_function = (fun () -> write default) } - in + in begin fun v -> add_anonymous_leaf (decl_obj v) end , begin fun v -> add_anonymous_leaf (ldecl_obj v) end , begin fun v -> add_anonymous_leaf (gdecl_obj v) end else write,write,write - in + in let cread () = cast (read ()) in - let cwrite v = write (uncast v) in - let clwrite v = lwrite (uncast v) in - let cgwrite v = gwrite (uncast v) in - value_tab := OptionMap.add key (name,(sync,cread,cwrite,clwrite,cgwrite)) !value_tab; - write + let cwrite v = write (uncast v) in + let clwrite v = lwrite (uncast v) in + let cgwrite v = gwrite (uncast v) in + value_tab := OptionMap.add key (name,(sync,cread,cwrite,clwrite,cgwrite)) !value_tab; + write type 'a write_function = 'a -> unit let declare_int_option = - declare_option + declare_option (fun v -> IntValue v) (function IntValue v -> v | _ -> anomaly "async_option") let declare_bool_option = @@ -310,15 +310,15 @@ let set_option_value locality check_and_cast key v = let bad_type_error () = error "Bad type of value for this option" let set_int_option_value_gen locality = set_option_value locality - (fun v -> function + (fun v -> function | (IntValue _) -> IntValue v | _ -> bad_type_error ()) let set_bool_option_value_gen locality = set_option_value locality - (fun v -> function + (fun v -> function | (BoolValue _) -> BoolValue v | _ -> bad_type_error ()) let set_string_option_value_gen locality = set_option_value locality - (fun v -> function + (fun v -> function | (StringValue _) -> StringValue v | _ -> bad_type_error ()) @@ -339,10 +339,10 @@ let msg_option_value (name,v) = let print_option_value key = let (name,(_,read,_,_,_)) = get_option key in - let s = read () in + let s = read () in match s with - | BoolValue b -> - msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++ + | BoolValue b -> + msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++ fnl ()) | _ -> msg (str ("Current value of "^name^" is ") ++ @@ -352,20 +352,20 @@ let print_option_value key = let print_tables () = msg (str "Synchronous options:" ++ fnl () ++ - OptionMap.fold - (fun key (name,(sync,read,_,_,_)) p -> - if sync then + OptionMap.fold + (fun key (name,(sync,read,_,_,_)) p -> + if sync then p ++ str (" "^(nickname key)^": ") ++ msg_option_value (name,read()) ++ fnl () - else + else p) !value_tab (mt ()) ++ str "Asynchronous options:" ++ fnl () ++ - OptionMap.fold - (fun key (name,(sync,read,_,_,_)) p -> - if sync then + OptionMap.fold + (fun key (name,(sync,read,_,_,_)) p -> + if sync then p - else + else p ++ str (" "^(nickname key)^": ") ++ msg_option_value (name,read()) ++ fnl ()) !value_tab (mt ()) ++ diff --git a/library/goptions.mli b/library/goptions.mli index eba44a896..511986a57 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -16,11 +16,11 @@ [declare_int_option], [declare_bool_option], ... functions. Each table/option is uniquely identified by a key of type [option_name] - which consists in a list of strings. Note that for parsing constraints, + which consists in a list of strings. Note that for parsing constraints, table names must not be made of more than 2 strings while option names can be of arbitrary length. - The declaration of a table, say of name [["Toto";"Titi"]] + The declaration of a table, say of name [["Toto";"Titi"]] automatically makes available the following vernacular commands: Add Toto Titi foo. @@ -116,18 +116,18 @@ module MakeRefTable : (*s Options. *) (* These types and function are for declaring a new option of name [key] - and access functions [read] and [write]; the parameter [name] is the option name + and access functions [read] and [write]; the parameter [name] is the option name used when printing the option value (command "Print Toto Titi." *) type 'a option_sig = { - optsync : bool; + optsync : bool; optname : string; optkey : option_name; optread : unit -> 'a; optwrite : 'a -> unit } -(* When an option is declared synchronous ([optsync] is [true]), the output is +(* When an option is declared synchronous ([optsync] is [true]), the output is a synchronous write function. Otherwise it is [optwrite] *) type 'a write_function = 'a -> unit diff --git a/library/heads.ml b/library/heads.ml index c63634458..bca6b6502 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -22,8 +22,8 @@ open Lib (** Characterization of the head of a term *) (* We only compute an approximation to ensure the computation is not - arbitrary long (e.g. the head constant of [h] defined to be - [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch + arbitrary long (e.g. the head constant of [h] defined to be + [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch the evaluation of [phi(0)] and the head of [h] is declared unknown). *) type rigid_head_kind = @@ -50,7 +50,7 @@ let freeze () = !head_map let unfreeze hm = head_map := hm -let _ = +let _ = Summary.declare_summary "Head_decl" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; @@ -63,7 +63,7 @@ let kind_of_head env t = let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta t) with | Rel n when n > k -> NotImmediatelyComputableHead | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) - | Var id -> + | Var id -> (try on_subterm k l b (variable_head id) with Not_found -> (* a goal variable *) @@ -71,7 +71,7 @@ let kind_of_head env t = | Some c -> aux k l c b | None -> NotImmediatelyComputableHead) | Const cst -> on_subterm k l b (constant_head cst) - | Construct _ | CoFix _ -> + | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead | Sort _ | Ind _ | Prod _ -> RigidHead RigidType | Cast (c,_,_) -> aux k l c b @@ -88,7 +88,7 @@ let kind_of_head env t = and on_subterm k l with_case = function | FlexibleHead (n,i,q,with_subcase) -> let m = List.length l in - let k',rest,a = + let k',rest,a = if n > m then (* eta-expansion *) let a = @@ -115,12 +115,12 @@ let compute_head = function | Some c -> kind_of_head (Global.env()) c) | EvalVarRef id -> (match pi2 (Global.lookup_named id) with - | Some c when not (Decls.variable_opacity id) -> + | Some c when not (Decls.variable_opacity id) -> kind_of_head (Global.env()) c - | _ -> + | _ -> RigidHead (RigidVar id)) -let is_rigid env t = +let is_rigid env t = match kind_of_head env t with | RigidHead _ | ConstructorHead -> true | _ -> false @@ -129,7 +129,7 @@ let is_rigid env t = let load_head _ (_,(ref,(k:head_approximation))) = head_map := Evalrefmap.add ref k !head_map - + let cache_head o = load_head 1 o @@ -158,7 +158,7 @@ let rebuild_head (ref,k) = let export_head o = Some o let (inHead, _) = - declare_object {(default_object "HEAD") with + declare_object {(default_object "HEAD") with cache_function = cache_head; load_function = load_head; subst_function = subst_head; diff --git a/library/impargs.ml b/library/impargs.ml index aedb2d5a8..edd0aba0e 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -36,7 +36,7 @@ type implicits_flags = { (* les implicites sont stricts par défaut en v8 *) -let implicit_args = ref { +let implicit_args = ref { auto = false; strict = true; strongly_strict = false; @@ -72,7 +72,7 @@ let is_maximal_implicit_args () = !implicit_args.maximal let with_implicits flags f x = let oflags = !implicit_args in - try + try implicit_args := flags; let rslt = f x in implicit_args := oflags; @@ -169,7 +169,7 @@ let is_flexible_reference env bound depth f = let push_lift d (e,n) = (push_rel d e,n+1) let is_reversible_pattern bound depth f l = - isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) & + isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) & array_for_all (fun c -> isRel c & destRel c < depth) l & array_distinct l @@ -194,7 +194,7 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc = | Evar _ -> () | _ -> iter_constr_with_full_binders push_lift (frec rig) ed c - in + in frec true (env,1) m; acc (* calcule la liste des arguments implicites *) @@ -215,14 +215,14 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = let na',avoid' = concrete_name None avoid names na all 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) - | _ -> + | _ -> let names = List.rev names in let v = Array.map (fun na -> na,None) (Array.of_list names) in if contextual then add_free_rels_until strict strongly_strict revpat n env t Conclusion v else v - in - match kind_of_term (whd_betadeltaiota env t) with + in + match kind_of_term (whd_betadeltaiota env t) with | Prod (na,a,b) -> let na',avoid = concrete_name None [] [] na all b in let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in @@ -232,16 +232,16 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rec prepare_implicits f = function | [] -> [] | (Anonymous, Some _)::_ -> anomaly "Unnamed implicit" - | (Name id, Some imp)::imps -> + | (Name id, Some imp)::imps -> let imps' = prepare_implicits f imps in Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -let compute_implicits_flags env f all t = - compute_implicits_gen +let compute_implicits_flags env f all t = + compute_implicits_gen (f.strict or f.strongly_strict) f.strongly_strict f.reversible_pattern f.contextual all env t - + let set_implicit id imp insmax = (id,(match imp with None -> Manual | Some imp -> imp),insmax) @@ -256,7 +256,7 @@ let compute_manual_implicits env flags t enriching l = else compute_implicits_gen false false false true true env t in let n = List.length autoimps in let try_forced k l = - try + try let (id, (b, fi, fo)), l' = assoc_by_pos k l in if fo then let id = match id with Some id -> id | None -> id_of_string ("arg_" ^ string_of_int k) in @@ -264,17 +264,17 @@ let compute_manual_implicits env flags t enriching l = else l, None with Not_found -> l, None in - if not (list_distinct l) then + if not (list_distinct l) then error ("Some parameters are referred more than once"); (* Compare with automatic implicits to recover printing data and names *) let rec merge k l = function | (Name id,imp)::imps -> let l',imp,m = - try + try let (b, fi, fo) = List.assoc (ExplByName id) l in List.remove_assoc (ExplByName id) l, (Some Manual), (Some (b, fi)) with Not_found -> - try + try let (id, (b, fi, fo)), l' = assoc_by_pos k l in l', (Some Manual), (Some (b,fi)) with Not_found -> @@ -288,12 +288,12 @@ let compute_manual_implicits env flags t enriching l = forced :: merge (k+1) l' imps | [] when l = [] -> [] | [] -> - List.iter (function - | ExplByName id,(b,fi,forced) -> + List.iter (function + | ExplByName id,(b,fi,forced) -> if not forced then error ("Wrong or not dependent implicit argument name: "^(string_of_id id)) | ExplByPos (i,_id),_t -> - if i<1 or i>n then + if i<1 or i>n then error ("Bad implicit argument number: "^(string_of_int i)) else errorlabstrm "" @@ -307,12 +307,12 @@ let const v _ = v let compute_implicits_auto env f manual t = match manual with - | [] -> + | [] -> if not f.auto then [] else let l = compute_implicits_flags env f false t in prepare_implicits f l | _ -> compute_manual_implicits env f t f.auto manual - + let compute_implicits env t = compute_implicits_auto env !implicit_args [] t type maximal_insertion = bool (* true = maximal contextual insertion *) @@ -366,7 +366,7 @@ let compute_constant_implicits flags manual cst = (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where - $i$ are the implicit arguments of the inductive and $v$ the array of + $i$ are the implicit arguments of the inductive and $v$ the array of implicit arguments of the constructors. *) let compute_mib_implicits flags manual kn = @@ -391,7 +391,7 @@ let compute_mib_implicits flags manual kn = let compute_all_mib_implicits flags manual kn = let imps = compute_mib_implicits flags manual kn in - List.flatten + List.flatten (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) @@ -406,18 +406,18 @@ let compute_var_implicits flags manual id = let compute_global_implicits flags manual = function | VarRef id -> compute_var_implicits flags manual id | ConstRef kn -> compute_constant_implicits flags manual kn - | IndRef (kn,i) -> + | IndRef (kn,i) -> let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps - | ConstructRef ((kn,i),j) -> + | ConstructRef ((kn,i),j) -> let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1) (* Merge a manual explicitation with an implicit_status list *) - + let merge_impls oldimpls newimpls = - let (before, news), olds = + let (before, news), olds = let len = List.length newimpls - List.length oldimpls in if len >= 0 then list_split_at len newimpls, oldimpls - else + else let before, after = list_split_at (-len) oldimpls in (before, newimpls), after in @@ -436,7 +436,7 @@ type implicit_discharge_request = | ImplLocal | ImplConstant of constant * implicits_flags | ImplMutualInductive of kernel_name * implicits_flags - | ImplInteractive of global_reference * implicits_flags * + | ImplInteractive of global_reference * implicits_flags * implicit_interactive_request let implicits_table = ref Refmap.empty @@ -471,7 +471,7 @@ let section_segment_of_reference = function let discharge_implicits (_,(req,l)) = match req with | ImplLocal -> None - | ImplInteractive (ref,flags,exp) -> + | ImplInteractive (ref,flags,exp) -> let vars = section_segment_of_reference ref in let ref' = pop_global_reference ref in let l' = [ref', impls_of_context vars @ snd (List.hd l)] in @@ -481,22 +481,22 @@ let discharge_implicits (_,(req,l)) = let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] in Some (ImplConstant (con',flags),l') | ImplMutualInductive (kn,flags) -> - let l' = List.map (fun (gr, l) -> + let l' = List.map (fun (gr, l) -> let vars = section_segment_of_reference gr in - (pop_global_reference gr, impls_of_context vars @ l)) l + (pop_global_reference gr, impls_of_context vars @ l)) l in Some (ImplMutualInductive (pop_kn kn,flags),l') let rebuild_implicits (req,l) = let l' = match req with | ImplLocal -> assert false - | ImplConstant (con,flags) -> + | ImplConstant (con,flags) -> let oldimpls = snd (List.hd l) in let newimpls = compute_constant_implicits flags [] con in [ConstRef con, merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> let newimpls = compute_all_mib_implicits flags [] kn in - let rec aux olds news = + let rec aux olds news = match olds, news with | (_, oldimpls) :: old, (gr, newimpls) :: tl -> (gr, merge_impls oldimpls newimpls) :: aux old tl @@ -506,13 +506,13 @@ let rebuild_implicits (req,l) = | ImplInteractive (ref,flags,o) -> match o with - | ImplAuto -> + | ImplAuto -> let oldimpls = snd (List.hd l) in let newimpls = compute_global_implicits flags [] ref in [ref,merge_impls oldimpls newimpls] - | ImplManual m -> + | ImplManual m -> let oldimpls = snd (List.hd l) in - let auto = + let auto = if flags.auto then let newimpls = compute_global_implicits flags [] ref in merge_impls oldimpls newimpls @@ -521,11 +521,11 @@ let rebuild_implicits (req,l) = let l' = merge_impls auto m in [ref,l'] in (req,l') -let export_implicits (req,_ as x) = +let export_implicits (req,_ as x) = if req = ImplLocal then None else Some x let (inImplicits, _) = - declare_object {(default_object "IMPLICITS") with + declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; load_function = load_implicits; subst_function = subst_implicits; @@ -540,10 +540,10 @@ let declare_implicits_gen req flags ref = let declare_implicits local ref = let flags = { !implicit_args with auto = true } in - let req = + let req = if local then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in declare_implicits_gen req flags ref - + let declare_var_implicits id = let flags = !implicit_args in declare_implicits_gen ImplLocal flags (VarRef id) @@ -559,11 +559,11 @@ let declare_mib_implicits kn = (compute_mib_implicits flags [] kn) in add_anonymous_leaf (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) - + (* Declare manual implicits *) -type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) - -let compute_implicits_with_manual env typ enriching l = +type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) + +let compute_implicits_with_manual env typ enriching l = compute_manual_implicits env !implicit_args typ enriching l let declare_manual_implicits local ref ?enriching l = @@ -582,9 +582,9 @@ let maybe_declare_manual_implicits local ref ?enriching l = if l = [] then () else declare_manual_implicits local ref ?enriching l -let lift_implicits n = - List.map (fun x -> - match fst x with +let lift_implicits n = + List.map (fun x -> + match fst x with ExplByPos (k, id) -> ExplByPos (k + n, id), snd x | _ -> x) @@ -594,7 +594,7 @@ let init () = implicits_table := Refmap.empty let freeze () = !implicits_table let unfreeze t = implicits_table := t -let _ = +let _ = Summary.declare_summary "implicits" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; diff --git a/library/impargs.mli b/library/impargs.mli index 9f67eb462..6d2b01e8f 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -16,7 +16,7 @@ open Environ open Nametab (*i*) -(*s Implicit arguments. Here we store the implicit arguments. Notice that we +(*s Implicit arguments. Here we store the implicit arguments. Notice that we are outside the kernel, which knows nothing about implicit arguments. *) val make_implicit_args : bool -> unit @@ -66,11 +66,11 @@ val positions_of_implicits : implicits_list -> int list val compute_implicits : env -> types -> implicits_list (* A [manual_explicitation] is a tuple of a positional or named explicitation with - maximal insertion, force inference and force usage flags. Forcing usage makes + maximal insertion, force inference and force usage flags. Forcing usage makes the argument implicit even if the automatic inference considers it not inferable. *) type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) -val compute_implicits_with_manual : env -> types -> bool -> +val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list (*s Computation of implicits (done using the global environment). *) @@ -109,6 +109,6 @@ type implicit_discharge_request = | ImplLocal | ImplConstant of constant * implicits_flags | ImplMutualInductive of kernel_name * implicits_flags - | ImplInteractive of global_reference * implicits_flags * + | ImplInteractive of global_reference * implicits_flags * implicit_interactive_request diff --git a/library/lib.ml b/library/lib.ml index 197e4c3f1..20c6bf1e4 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -17,7 +17,7 @@ open Summary -type node = +type node = | Leaf of obj | CompilingLibrary of object_prefix | OpenedModule of bool option * object_prefix * Summary.frozen @@ -40,7 +40,7 @@ let iter_objects f i prefix = let load_objects = iter_objects load_object let open_objects = iter_objects open_object -let subst_objects prefix subst seg = +let subst_objects prefix subst seg = let subst_one = fun (id,obj as node) -> let obj' = subst_object (make_oname prefix id, subst, obj) in if obj' == obj then node else @@ -58,13 +58,13 @@ let load_and_subst_objects i prefix subst seg = let classify_segment seg = let rec clean ((substl,keepl,anticipl) as acc) = function | (_,CompilingLibrary _) :: _ | [] -> acc - | ((sp,kn),Leaf o) :: stk -> + | ((sp,kn),Leaf o) :: stk -> let id = Names.id_of_label (Names.label kn) in - (match classify_object o with + (match classify_object o with | Dispose -> clean acc stk - | Keep o' -> + | Keep o' -> clean (substl, (id,o')::keepl, anticipl) stk - | Substitute o' -> + | Substitute o' -> clean ((id,o')::substl, keepl, anticipl) stk | Anticipate o' -> clean (substl, keepl, o'::anticipl) stk) @@ -84,12 +84,12 @@ let classify_segment seg = let segment_of_objects prefix = List.map (fun (id,obj) -> (make_oname prefix id, Leaf obj)) -(* We keep trace of operations in the stack [lib_stk]. - [path_prefix] is the current path of sections, where sections are stored in - ``correct'' order, the oldest coming first in the list. It may seems +(* We keep trace of operations in the stack [lib_stk]. + [path_prefix] is the current path of sections, where sections are stored in + ``correct'' order, the oldest coming first in the list. It may seems costly, but in practice there is not so many openings and closings of sections, but on the contrary there are many constructions of section - paths based on the library path. *) + paths based on the library path. *) let initial_prefix = default_library,(Names.initial_path,Names.empty_dirpath) @@ -115,10 +115,10 @@ let sections_are_opened () = let cwd () = fst !path_prefix let current_dirpath sec = - Libnames.drop_dirpath_prefix (library_dp ()) - (if sec then cwd () + Libnames.drop_dirpath_prefix (library_dp ()) + (if sec then cwd () else Libnames.pop_dirpath_n (sections_depth ()) (cwd ())) - + let make_path id = Libnames.make_path (cwd ()) id let path_of_include () = @@ -129,11 +129,11 @@ let path_of_include () = let current_prefix () = snd !path_prefix -let make_kn id = +let make_kn id = let mp,dir = current_prefix () in Names.make_kn mp dir (Names.label_of_id id) -let make_con id = +let make_con id = let mp,dir = current_prefix () in Names.make_con mp dir (Names.label_of_id id) @@ -151,25 +151,25 @@ let recalc_path_prefix () = in path_prefix := recalc !lib_stk -let pop_path_prefix () = +let pop_path_prefix () = let dir,(mp,sec) = !path_prefix in path_prefix := fst (split_dirpath dir), (mp, fst (split_dirpath sec)) -let find_entry_p p = +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 -let find_split_p p = +let find_split_p p = let rec find = function | [] -> raise Not_found | ent::l -> if p ent then ent,l else find l in find !lib_stk -let split_lib_gen test = +let split_lib_gen test = let rec collect after equal = function | hd::strict_before as before -> if test hd then collect after (hd::equal) strict_before else after,equal,before @@ -201,7 +201,7 @@ let split_lib sp = split_lib_gen (fun x -> (fst x) = sp) let add_entry sp node = lib_stk := (sp,node) :: !lib_stk -let anonymous_id = +let anonymous_id = let n = ref 0 in fun () -> incr n; Names.id_of_string ("_" ^ (string_of_int !n)) @@ -212,7 +212,7 @@ let add_anonymous_entry node = name let add_leaf id obj = - if fst (current_prefix ()) = Names.initial_path then + if fst (current_prefix ()) = Names.initial_path then error ("No session module started (use -top dir)"); let oname = make_oname id in cache_object (oname,obj); @@ -227,9 +227,9 @@ let add_discharged_leaf id obj = let add_leaves id objs = let oname = make_oname id in - let add_obj obj = + let add_obj obj = add_entry oname (Leaf obj); - load_object 1 (oname,obj) + load_object 1 (oname,obj) in List.iter add_obj objs; oname @@ -246,28 +246,28 @@ let add_frozen_state () = (* Modules. *) -let is_opened id = function +let is_opened id = function oname,(OpenedSection _ | OpenedModule _ | OpenedModtype _) when basename (fst oname) = id -> true | _ -> false -let is_opening_node = function +let is_opening_node = function _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true | _ -> false -let current_mod_id () = +let current_mod_id () = try match find_entry_p is_opening_node with - | oname,OpenedModule (_,_,fs) -> + | oname,OpenedModule (_,_,fs) -> basename (fst oname) - | oname,OpenedModtype (_,fs) -> + | oname,OpenedModtype (_,fs) -> basename (fst oname) | _ -> error "you are not in a module" with Not_found -> error "no opened modules" -let start_module export id mp fs = +let start_module export id mp fs = let dir = add_dirpath_suffix (fst !path_prefix) id in let prefix = dir,(mp,Names.empty_dirpath) in let oname = make_path id, make_kn id in @@ -281,9 +281,9 @@ let start_module export id mp fs = let error_still_opened string oname = let id = basename (fst oname) in errorlabstrm "" (str string ++ spc () ++ pr_id id ++ str " is still opened.") - -let end_module () = - let oname,fs = + +let end_module () = + let oname,fs = try match find_entry_p is_opening_node with | oname,OpenedModule (_,_,fs) -> oname,fs | oname,OpenedModtype _ -> error_still_opened "Module Type" oname @@ -302,11 +302,11 @@ let end_module () = TODO *) recalc_path_prefix (); - (* add_frozen_state must be called after processing the module, - because we cannot recache interactive modules *) + (* add_frozen_state must be called after processing the module, + because we cannot recache interactive modules *) (oname, prefix, fs, after) -let start_modtype id mp fs = +let start_modtype id mp fs = let dir = add_dirpath_suffix (fst !path_prefix) id in let prefix = dir,(mp,Names.empty_dirpath) in let sp = make_path id in @@ -317,8 +317,8 @@ let start_modtype id mp fs = path_prefix := prefix; prefix -let end_modtype () = - let oname,fs = +let end_modtype () = + let oname,fs = try match find_entry_p is_opening_node with | oname,OpenedModtype (_,fs) -> oname,fs | oname,OpenedModule _ -> error_still_opened "Module" oname @@ -333,7 +333,7 @@ let end_modtype () = let dir = !path_prefix in recalc_path_prefix (); (* add_frozen_state must be called after processing the module type. - This is because we cannot recache interactive module types *) + This is because we cannot recache interactive module types *) (oname,dir,fs,after) @@ -369,24 +369,24 @@ let end_compilation dir = | OpenedModtype _ -> error "There are some open module types." | _ -> assert false with - Not_found -> () + Not_found -> () in let module_p = function (_,CompilingLibrary _) -> true | x -> is_opening_node x in - let oname = + let oname = try match find_entry_p module_p with (oname, CompilingLibrary prefix) -> oname | _ -> assert false with Not_found -> anomaly "No module declared" in - let _ = + let _ = match !comp_name with | None -> anomaly "There should be a module name..." | Some m -> - if m <> dir then anomaly - ("The current open module has name "^ (Names.string_of_dirpath m) ^ + if m <> dir then anomaly + ("The current open module has name "^ (Names.string_of_dirpath m) ^ " and not " ^ (Names.string_of_dirpath m)); in let (after,_,before) = split_lib oname in @@ -394,23 +394,23 @@ let end_compilation dir = !path_prefix,after (* Returns true if we are inside an opened module type *) -let is_modtype () = +let is_modtype () = let opened_p = function - | _, OpenedModtype _ -> true + | _, OpenedModtype _ -> true | _ -> false in - try + try let _ = find_entry_p opened_p in true with Not_found -> false (* Returns true if we are inside an opened module *) -let is_module () = +let is_module () = let opened_p = function - | _, OpenedModule _ -> true + | _, OpenedModule _ -> true | _ -> false in - try + try let _ = find_entry_p opened_p in true with Not_found -> false @@ -419,7 +419,7 @@ let is_module () = (* Returns the opening node of a given name *) let find_opening_node id = try snd (find_entry_p (is_opened id)) - with Not_found -> + with Not_found -> try ignore (find_entry_p is_opening_node); error "There is nothing to end." with Not_found -> error "Nothing to end of this name." @@ -429,7 +429,7 @@ let find_opening_node id = - the list of variables in this section - the list of variables on which each constant depends in this section - the list of variables on which each inductive depends in this section - - the list of substitution to do at section closing + - the list of substitution to do at section closing *) type binding_kind = Explicit | Implicit @@ -472,7 +472,7 @@ let add_section_replacement f g hyps = let sechyps = extract_hyps (vars,hyps) in let args = instance_from_variable_context (List.rev sechyps) in sectab := (vars,f args exps,g sechyps abs)::sl - + let add_section_kn kn = let f x (l1,l2) = (l1,Names.KNmap.add kn x l2) in add_section_replacement f f @@ -511,7 +511,7 @@ let init_sectab () = sectab := [] let freeze_sectab () = !sectab let unfreeze_sectab s = sectab := s -let _ = +let _ = Summary.declare_summary "section-context" { Summary.freeze_function = freeze_sectab; Summary.unfreeze_function = unfreeze_sectab; @@ -556,10 +556,10 @@ let discharge_item ((sp,_ as oname),e) = anomaly "discharge_item" let close_section () = - let oname,fs = + let oname,fs = try match find_entry_p is_opening_node with | oname,OpenedSection (_,fs) -> oname,fs - | _ -> assert false + | _ -> assert false with Not_found -> error "No opened section." in @@ -597,7 +597,7 @@ let has_top_frozen_state () = | (sp, FrozenState _)::_ -> Some sp | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t | _ -> None - in aux !lib_stk + in aux !lib_stk let set_lib_stk new_lib_stk = lib_stk := new_lib_stk; @@ -646,7 +646,7 @@ let delete_gen test = let delete sp = delete_gen (fun x -> (fst x) = sp) let reset_name (loc,id) = - let (sp,_) = + let (sp,_) = try find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi) with Not_found -> @@ -663,21 +663,21 @@ let remove_name (loc,id) = in delete sp -let is_mod_node = function - | OpenedModule _ | OpenedModtype _ | OpenedSection _ - | ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true - | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" +let is_mod_node = function + | OpenedModule _ | OpenedModtype _ | OpenedSection _ + | ClosedModule _ | ClosedModtype _ | 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 *) +(* Reset on a module or section name in order to bypass constants with + the same name *) let reset_mod (loc,id) = - let (_,before) = + let (_,before) = try - find_split_p (fun (sp,node) -> - let (_,spi) = repr_path (fst sp) in id = spi + 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") @@ -699,7 +699,7 @@ let is_label_n n x = | _ -> false (* Reset the label registered by [mark_end_of_command()] with number n. *) -let reset_label n = +let reset_label n = let current = current_command_label() in if n < current then let res = reset_to_gen (is_label_n n) in @@ -709,7 +709,7 @@ let reset_label n = match !lib_stk with | [] -> () | x :: ls -> (lib_stk := ls;set_command_label (n-1)) - + let rec back_stk n stk = match stk with (sp,Leaf o)::tail when object_tag o = "DOT" -> @@ -741,15 +741,15 @@ let init () = let initial_state = ref None -let declare_initial_state () = +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 -> + | None -> error "Resetting to the initial state is possible only interactively" - | Some sp -> + | Some sp -> begin match split_lib sp with | (_,[_,FrozenState fs as hd],before) -> lib_stk := hd::before; @@ -762,7 +762,7 @@ let reset_initial () = (* Misc *) -let mp_of_global ref = +let mp_of_global ref = match ref with | VarRef id -> fst (current_prefix ()) | ConstRef cst -> Names.con_modpath cst @@ -775,11 +775,11 @@ let rec dp_of_mp modp = | Names.MPbound _ | Names.MPself _ -> library_dp () | Names.MPdot (mp,_) -> dp_of_mp mp -let rec split_mp mp = - match mp with +let rec split_mp mp = + match mp with | Names.MPfile dp -> dp, Names.empty_dirpath - | Names.MPdot (prfx, lbl) -> - let mprec, dprec = split_mp prfx in + | Names.MPdot (prfx, lbl) -> + let mprec, dprec = split_mp prfx in mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec)) | Names.MPself msid -> let (_, id, dp) = Names.repr_msid msid in library_dp(), Names.make_dirpath [Names.id_of_string id] | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [Names.id_of_string id] @@ -787,17 +787,17 @@ let rec split_mp mp = let split_modpath mp = let rec aux = function | Names.MPfile dp -> dp, [] - | Names.MPbound mbid -> + | Names.MPbound mbid -> library_dp (), [Names.id_of_mbid mbid] | Names.MPself msid -> library_dp (), [Names.id_of_msid msid] | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in (mp', Names.id_of_label l :: lab) - in + in let (mp, l) = aux mp in mp, l - + let library_part ref = - match ref with + match ref with | VarRef id -> library_dp () | _ -> dp_of_mp (mp_of_global ref) @@ -805,7 +805,7 @@ let remove_section_part ref = let sp = Nametab.path_of_global ref in let dir,_ = repr_path sp in match ref with - | VarRef id -> + | VarRef id -> anomaly "remove_section_part not supported on local variables" | _ -> if is_dirpath_prefix_of dir (cwd ()) then @@ -822,15 +822,15 @@ let pop_kn kn = let (mp,dir,l) = Names.repr_kn kn in Names.make_kn mp (pop_dirpath dir) l -let pop_con con = +let pop_con con = let (mp,dir,l) = Names.repr_con con in Names.make_con mp (pop_dirpath dir) l -let con_defined_in_sec kn = +let con_defined_in_sec kn = let _,dir,_ = Names.repr_con kn in dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) -let defined_in_sec kn = +let defined_in_sec kn = let _,dir,_ = Names.repr_kn kn in dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) @@ -843,10 +843,10 @@ let discharge_global = function ConstructRef ((pop_kn kn,i),j) | r -> r -let discharge_kn kn = +let discharge_kn kn = if defined_in_sec kn then pop_kn kn else kn -let discharge_con cst = +let discharge_con cst = if con_defined_in_sec cst then pop_con cst else cst let discharge_inductive (kn,i) = diff --git a/library/lib.mli b/library/lib.mli index f4d4900c3..0e2e304cd 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -13,7 +13,7 @@ and to backtrack (undo) those operations. It provides also the section mechanism (at a low level; discharge is not known at this step). *) -type node = +type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen @@ -40,7 +40,7 @@ val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitu to their answers to the [classify_object] function in three groups: [Substitute], [Keep], [Anticipate] respectively. The order of each returned list is the same as in the input list. *) -val classify_segment : +val classify_segment : library_segment -> lib_objects * lib_objects * Libobject.obj list (* [segment_of_objects prefix objs] forms a list of Leafs *) @@ -69,7 +69,7 @@ val current_command_label : unit -> int registered after it. *) val reset_label : int -> unit -(*s The function [contents_after] returns the current library segment, +(*s The function [contents_after] returns the current library segment, starting from a given section path. If not given, the entire segment is returned. *) @@ -102,12 +102,12 @@ val find_opening_node : Names.identifier -> node (*s Modules and module types *) -val start_module : +val start_module : bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix val end_module : unit -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment -val start_modtype : +val start_modtype : Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix val end_modtype : unit -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment @@ -144,7 +144,7 @@ val reset_to_state : Libnames.object_name -> unit val has_top_frozen_state : unit -> Libnames.object_name option -(* [back n] resets to the place corresponding to the $n$-th call of +(* [back n] resets to the place corresponding to the $n$-th call of [mark_end_of_command] (counting backwards) *) val back : int -> unit diff --git a/library/libnames.ml b/library/libnames.ml index 0404d7cd8..2b335ea6c 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -33,10 +33,10 @@ let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef" let subst_constructor subst ((kn,i),j as ref) = - let kn' = subst_kn subst kn in + let kn' = subst_kn subst kn in if kn==kn' then ref, mkConstruct ref else ((kn',i),j), mkConstruct ((kn',i),j) - + let subst_global subst ref = match ref with | VarRef var -> ref, mkVar var | ConstRef kn -> @@ -125,12 +125,12 @@ let parse_dir s = if n >= len then dirs else let pos = try - String.index_from s n '.' + String.index_from s n '.' with Not_found -> len in if pos = n then error (s ^ " is an invalid path."); let dir = String.sub s n (pos-n) in - decoupe_dirs ((id_of_string dir)::dirs) (pos+1) + decoupe_dirs ((id_of_string dir)::dirs) (pos+1) in decoupe_dirs [] 0 @@ -184,7 +184,7 @@ let path_of_string s = with | Invalid_argument _ -> invalid_arg "path_of_string" -let pr_path sp = str (string_of_path sp) +let pr_path sp = str (string_of_path sp) let restrict_path n sp = let dir, s = repr_path sp in @@ -195,17 +195,17 @@ let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id) let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id) -let decode_kn kn = +let decode_kn kn = let rec dirpath_of_module = function | MPfile dir -> repr_dirpath dir - | MPbound mbid -> + | MPbound mbid -> let _,_,dp = repr_mbid mbid in let id = id_of_mbid mbid in id::(repr_dirpath dp) - | MPself msid -> + | MPself msid -> let _,_,dp = repr_msid msid in let id = id_of_msid msid in - id::(repr_dirpath dp) + id::(repr_dirpath dp) | MPdot(mp,l) -> (id_of_label l)::(dirpath_of_module mp) in let mp,sec_dir,l = repr_kn kn in @@ -214,7 +214,7 @@ let decode_kn kn = else anomaly "Section part should be empty!" -let decode_con kn = +let decode_con kn = let mp,sec_dir,l = repr_con kn in match mp,(repr_dirpath sec_dir) with MPfile dir,[] -> (dir,id_of_label l) @@ -234,7 +234,7 @@ let qualid_of_string = path_of_string let qualid_of_path sp = sp let qualid_of_ident id = make_qualid empty_dirpath id -let qualid_of_dirpath dir = +let qualid_of_dirpath dir = let (l,a) = split_dirpath dir in make_qualid l a @@ -242,11 +242,11 @@ type object_name = full_path * kernel_name type object_prefix = dir_path * (module_path * dir_path) -let make_oname (dirpath,(mp,dir)) id = +let make_oname (dirpath,(mp,dir)) id = make_path dirpath id, make_kn mp dir (label_of_id id) (* to this type are mapped dir_path's in the nametab *) -type global_dir_reference = +type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix | DirOpenSection of object_prefix @@ -262,7 +262,7 @@ type global_dir_reference = ModTypeRef kn' *) -type reference = +type reference = | Qualid of qualid located | Ident of identifier located @@ -274,7 +274,7 @@ let string_of_reference = function | Qualid (loc,qid) -> string_of_qualid qid | Ident (loc,id) -> string_of_id id -let pr_reference = function +let pr_reference = function | Qualid (_,qid) -> pr_qualid qid | Ident (_,id) -> pr_id id diff --git a/library/libnames.mli b/library/libnames.mli index b93ee87ee..43ca252c1 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -47,7 +47,7 @@ val global_of_constr : constr -> global_reference val constr_of_reference : global_reference -> constr val reference_of_constr : constr -> global_reference -module Refset : Set.S with type elt = global_reference +module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference (*s Extended global references *) @@ -65,7 +65,7 @@ val dirpath_of_string : string -> dir_path val string_of_dirpath : dir_path -> string (* Pop the suffix of a [dir_path] *) -val pop_dirpath : dir_path -> dir_path +val pop_dirpath : dir_path -> dir_path (* Pop the suffix n times *) val pop_dirpath_n : int -> dir_path -> dir_path @@ -146,7 +146,7 @@ type object_prefix = dir_path * (module_path * dir_path) val make_oname : object_prefix -> identifier -> object_name (* to this type are mapped [dir_path]'s in the nametab *) -type global_dir_reference = +type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix | DirOpenSection of object_prefix @@ -158,7 +158,7 @@ type global_dir_reference = global name (referred either by a qualified name or by a single name) or a variable *) -type reference = +type reference = | Qualid of qualid located | Ident of identifier located diff --git a/library/libobject.ml b/library/libobject.ml index 504c1ffdd..95894294b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -25,7 +25,7 @@ let relax_flag = ref false;; let relax b = relax_flag := b;; -type 'a substitutivity = +type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a type 'a object_declaration = { @@ -46,12 +46,12 @@ let default_object s = { cache_function = (fun _ -> ()); load_function = (fun _ _ -> ()); open_function = (fun _ _ -> ()); - subst_function = (fun _ -> + subst_function = (fun _ -> yell ("The object "^s^" does not know how to substitute!")); classify_function = (fun obj -> Keep obj); discharge_function = (fun _ -> None); rebuild_function = (fun x -> x); - export_function = (fun _ -> None)} + export_function = (fun _ -> None)} (* The suggested object declaration is the following: @@ -59,7 +59,7 @@ let default_object s = { declare_object { (default_object "MY OBJECT") with cache_function = fun (sp,a) -> Mytbl.add sp a} - and the listed functions are only those which definitions accually + and the listed functions are only those which definitions accually differ from the default. This helps introducing new functions in objects. @@ -81,7 +81,7 @@ type dynamic_object_declaration = { let object_tag lobj = Dyn.tag lobj -let cache_tab = +let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) let declare_object odecl = @@ -96,34 +96,34 @@ let declare_object odecl = and opener i (oname,lobj) = if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the openfun" - and substituter (oname,sub,lobj) = - if Dyn.tag lobj = na then + and substituter (oname,sub,lobj) = + if Dyn.tag lobj = na then infun (odecl.subst_function (oname,sub,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the substfun" - and classifier lobj = - if Dyn.tag lobj = na then + and classifier lobj = + if Dyn.tag lobj = na then match odecl.classify_function (outfun lobj) with | Dispose -> Dispose | Substitute obj -> Substitute (infun obj) | Keep obj -> Keep (infun obj) | Anticipate (obj) -> Anticipate (infun obj) - else + else anomaly "somehow we got the wrong dynamic object in the classifyfun" - and discharge (oname,lobj) = - if Dyn.tag lobj = na then + and discharge (oname,lobj) = + if Dyn.tag lobj = na then Option.map infun (odecl.discharge_function (oname,outfun lobj)) - else + else anomaly "somehow we got the wrong dynamic object in the dischargefun" - and rebuild lobj = + and rebuild lobj = if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the rebuildfun" - and exporter lobj = - if Dyn.tag lobj = na then + and exporter lobj = + if Dyn.tag lobj = na then Option.map infun (odecl.export_function (outfun lobj)) - else + else anomaly "somehow we got the wrong dynamic object in the exportfun" - in + in Hashtbl.add cache_tab na { dyn_cache_function = cacher; dyn_load_function = loader; dyn_open_function = opener; @@ -144,13 +144,13 @@ let apply_dyn_fun deflt f lobj = let dodecl = try Hashtbl.find cache_tab tag - with Not_found -> + with Not_found -> if !relax_flag then failwith "local to_apply_dyn_fun" else error ("Cannot find library functions for an object with tag "^tag^ - " (maybe a plugin is missing)") in + " (maybe a plugin is missing)") in f dodecl with Failure "local to_apply_dyn_fun" -> deflt;; @@ -158,19 +158,19 @@ let apply_dyn_fun deflt f lobj = let cache_object ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj -let load_object i ((_,lobj) as node) = +let load_object i ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj -let open_object i ((_,lobj) as node) = +let open_object i ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj -let subst_object ((_,_,lobj) as node) = +let subst_object ((_,_,lobj) as node) = apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj -let classify_object lobj = +let classify_object lobj = apply_dyn_fun Dispose (fun d -> d.dyn_classify_function lobj) lobj -let discharge_object ((_,lobj) as node) = +let discharge_object ((_,lobj) as node) = apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj let rebuild_object lobj = diff --git a/library/libobject.mli b/library/libobject.mli index 41442fe53..6211ab378 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -18,7 +18,7 @@ open Mod_subst * a caching function specifying how to add the object in the current scope; - If the object wishes to register its visibility in the Nametab, + If the object wishes to register its visibility in the Nametab, it should do so for all possible sufixes. * a loading function, specifying what to do when the module @@ -26,9 +26,9 @@ open Mod_subst If the object wishes to register its visibility in the Nametab, it should do so for all sufixes no shorter than the "int" argument - * an opening function, specifying what to do when the module + * an opening function, specifying what to do when the module containing the object is opened (imported); - If the object wishes to register its visibility in the Nametab, + If the object wishes to register its visibility in the Nametab, it should do so for the suffix of the length the "int" argument * a classification function, specifying what to do with the object, @@ -44,11 +44,11 @@ open Mod_subst and Read markers) The classification function is also an occasion for a cleanup - (if this function returns Keep or Substitute of some object, the + (if this function returns Keep or Substitute of some object, the cache method is never called for it) - * a substitution function, performing the substitution; - this function should be declared for substitutive objects + * a substitution function, performing the substitution; + this function should be declared for substitutive objects only (see above) * a discharge function, that is applied at section closing time to @@ -63,12 +63,12 @@ open Mod_subst to disk (.vo). This function is also the opportunity to remove redundant information in order to keep .vo size small - The export function is a little obsolete and will be removed - in the near future... + The export function is a little obsolete and will be removed + in the near future... *) -type 'a substitutivity = +type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a type 'a object_declaration = { @@ -82,7 +82,7 @@ type 'a object_declaration = { rebuild_function : 'a -> 'a; export_function : 'a -> 'a option } -(* The default object is a "Keep" object with empty methods. +(* The default object is a "Keep" object with empty methods. Object creators are advised to use the construction [{(default_object "MY_OBJECT") with cache_function = ... diff --git a/library/library.ml b/library/library.ml index 831687723..9604a990c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -39,7 +39,7 @@ let is_in_load_paths phys_dir = let dir = System.canonical_path_name phys_dir in let lp = get_load_paths () in let check_p = fun p -> (String.compare dir p) == 0 in - List.exists check_p lp + List.exists check_p lp let remove_load_path dir = load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths @@ -48,7 +48,7 @@ let add_load_path isroot (phys_path,coq_path) = let phys_path = System.canonical_path_name phys_path in match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with | [_,dir,_] -> - if coq_path <> dir + if coq_path <> dir (* If this is not the default -I . to coqtop *) && not (phys_path = System.canonical_path_name Filename.current_dir_name @@ -71,7 +71,7 @@ let add_load_path isroot (phys_path,coq_path) = let physical_paths (dp,lp) = dp let extend_path_with_dirpath p dir = - List.fold_left Filename.concat p + List.fold_left Filename.concat p (List.map string_of_id (List.rev (repr_dirpath dir))) let root_paths_matching_dir_path dir = @@ -112,12 +112,12 @@ let loadpaths_matching_dir_path dir = let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths (************************************************************************) -(*s Modules on disk contain the following informations (after the magic +(*s Modules on disk contain the following informations (after the magic number, and before the digest). *) type compilation_unit_name = dir_path -type library_disk = { +type library_disk = { md_name : compilation_unit_name; md_compiled : compiled_library; md_objects : Declaremods.library_objects; @@ -135,7 +135,7 @@ type library_t = { library_imports : compilation_unit_name list; library_digest : Digest.t } -module LibraryOrdered = +module LibraryOrdered = struct type t = dir_path let compare d1 d2 = @@ -164,7 +164,7 @@ let freeze () = !libraries_imports_list, !libraries_exports_list -let unfreeze (mt,mo,mi,me) = +let unfreeze (mt,mo,mi,me) = libraries_table := mt; libraries_loaded_list := mo; libraries_imports_list := mi; @@ -176,7 +176,7 @@ let init () = libraries_imports_list := []; libraries_exports_list := [] -let _ = +let _ = Summary.declare_summary "MODULES" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; @@ -195,7 +195,7 @@ let try_find_library dir = let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) (* from a previous play of the session *) - libraries_filename_table := + libraries_filename_table := LibraryFilenameMap.add dir f !libraries_filename_table let library_full_filename dir = @@ -212,13 +212,13 @@ let library_is_loaded dir = try let _ = find_library dir in true with Not_found -> false -let library_is_opened dir = +let library_is_opened dir = List.exists (fun m -> m.library_name = dir) !libraries_imports_list let library_is_exported dir = List.exists (fun m -> m.library_name = dir) !libraries_exports_list -let loaded_libraries () = +let loaded_libraries () = List.map (fun m -> m.library_name) !libraries_loaded_list let opened_libraries () = @@ -249,7 +249,7 @@ let rec remember_last_of_each l m = let register_open_library export m = libraries_imports_list := remember_last_of_each !libraries_imports_list m; - if export then + if export then libraries_exports_list := remember_last_of_each !libraries_exports_list m (************************************************************************) @@ -271,14 +271,14 @@ let open_library export explicit_libs m = Declaremods.really_import_module (MPfile m.library_name) end else - if export then + if export then libraries_exports_list := remember_last_of_each !libraries_exports_list m -(* open_libraries recursively open a list of libraries but opens only once +(* open_libraries recursively open a list of libraries but opens only once a library that is re-exported many times *) let open_libraries export modl = - let to_open_list = + let to_open_list = List.fold_left (fun l m -> let subimport = @@ -299,19 +299,19 @@ let open_import i (_,(dir,export)) = (* if not (library_is_opened dir) then *) open_libraries export [try_find_library dir] -let cache_import obj = +let cache_import obj = open_import 1 obj let subst_import (_,_,o) = o let export_import o = Some o -let classify_import (_,export as obj) = +let classify_import (_,export as obj) = if export then Substitute obj else Dispose let (in_import, out_import) = - declare_object {(default_object "IMPORT LIBRARY") with + declare_object {(default_object "IMPORT LIBRARY") with cache_function = cache_import; open_function = open_import; subst_function = subst_import; @@ -376,7 +376,7 @@ let explain_locate_library_error qid = function | LibUnmappedDir -> let prefix, _ = repr_qualid qid in errorlabstrm "load_absolute_library_from" - (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ + (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) | LibNotFound -> errorlabstrm "load_absolute_library_from" @@ -393,14 +393,14 @@ let try_locate_qualified_library (loc,qid) = try let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in dir,f - with e -> + with e -> explain_locate_library_error qid e (************************************************************************) (* Internalise libraries *) -let lighten_library m = +let lighten_library m = if !Flags.dont_load_proofs then lighten_library m else m let mk_library md digest = { @@ -464,7 +464,7 @@ let rec_intern_by_filename_only id f = (* We check no other file containing same library is loaded *) if library_is_loaded m.library_name then begin - Flags.if_verbose warning + Flags.if_verbose warning ((string_of_dirpath m.library_name)^" is already loaded from file "^ library_full_filename m.library_name); m.library_name, [] @@ -476,15 +476,15 @@ let rec_intern_by_filename_only id f = let rec_intern_library_from_file idopt f = (* A name is specified, we have to check it contains library id *) let paths = get_load_paths () in - let _, f = + let _, f = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in rec_intern_by_filename_only idopt f (**********************************************************************) -(*s [require_library] loads and possibly opens a library. This is a +(*s [require_library] loads and possibly opens a library. This is a synchronized operation. It is performed as follows: - preparation phase: (functions require_library* ) the library and its + preparation phase: (functions require_library* ) the library and its dependencies are read from to disk (using intern_* ) [they are read from disk to ensure that at section/module discharging time, the physical library referred to outside the @@ -492,8 +492,8 @@ let rec_intern_library_from_file idopt f = the section/module] execution phase: (through add_leaf and cache_require) - the library is loaded in the environment and Nametab, the objects are - registered etc, using functions from Declaremods (via load_library, + the library is loaded in the environment and Nametab, the objects are + registered etc, using functions from Declaremods (via load_library, which recursively loads its dependencies) *) @@ -501,14 +501,14 @@ type library_reference = dir_path list * bool option let register_library (dir,m) = Declaremods.register_library - m.library_name - m.library_compiled - m.library_objects + m.library_name + m.library_compiled + m.library_objects m.library_digest; register_loaded_library m (* Follow the semantics of Anticipate object: - - called at module or module type closing when a Require occurs in + - called at module or module type closing when a Require occurs in the module or module type - not called from a library (i.e. a module identified with a file) *) let load_require _ (_,(needed,modl,_)) = @@ -529,7 +529,7 @@ let export_require (_,l,e) = Some ([],l,e) let discharge_require (_,o) = Some o -(* open_function is never called from here because an Anticipate object *) +(* open_function is never called from here because an Anticipate object *) let (in_require, out_require) = declare_object {(default_object "REQUIRE") with @@ -549,7 +549,7 @@ let set_xml_require f = xml_require := f let require_library_from_dirpath modrefl export = let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in let modrefl = List.map fst modrefl in - if Lib.is_modtype () || Lib.is_module () then + if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> @@ -583,7 +583,7 @@ let require_library_from_file idopt file export = let import_module export (loc,qid) = try match Nametab.locate_module qid with - | MPfile dir -> + | MPfile dir -> if Lib.is_modtype () || Lib.is_module () || not export then add_anonymous_leaf (in_import (dir, export)) else @@ -595,7 +595,7 @@ let import_module export (loc,qid) = user_err_loc (loc,"import_library", str ((string_of_qualid qid)^" is not a module")) - + (************************************************************************) (*s Initializing the compilation of a library. *) @@ -606,7 +606,7 @@ let check_coq_overwriting p id = (strbrk ("Cannot build module "^string_of_dirpath p^"."^string_of_id id^ ": it starts with prefix \"Coq\" which is reserved for the Coq library.")) -let start_library f = +let start_library f = let paths = get_load_paths () in let _,longf = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in @@ -628,15 +628,15 @@ let current_reexports () = let error_recursively_dependent_library dir = errorlabstrm "" - (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ + (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") (* Security weakness: file might have been changed on disk between - writing the content and computing the checksum... *) + writing the content and computing the checksum... *) let save_library_to dir f = let cenv, seg = Declaremods.end_library dir in - let md = { + let md = { md_name = dir; md_compiled = cenv; md_objects = seg; @@ -661,5 +661,5 @@ open Printf let mem s = let m = try_find_library s in h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" - (size_kb m) (size_kb m.library_compiled) + (size_kb m) (size_kb m.library_compiled) (size_kb m.library_objects))) diff --git a/library/library.mllib b/library/library.mllib index 1fc63929f..4efb69a21 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,7 +1,7 @@ Nameops Libnames Libobject -Summary +Summary Nametab Global Lib diff --git a/library/nameops.ml b/library/nameops.ml index 563fa0210..bc28ed98c 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -30,14 +30,14 @@ let cut_ident skip_quote s = let slen = String.length s in (* [n'] is the position of the first non nullary digit *) let rec numpart n n' = - if n = 0 then + if n = 0 then (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *) slen - else + else let c = Char.code (String.get s (n-1)) in - if c = code_of_0 && n <> slen then - numpart (n-1) n' - else if code_of_0 <= c && c <= code_of_9 then + if c = code_of_0 && n <> slen then + numpart (n-1) n' + else if code_of_0 <= c && c <= code_of_9 then numpart (n-1) (n-1) else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then numpart (n-1) (n-1) @@ -50,14 +50,14 @@ let repr_ident s = let numstart = cut_ident false s in let s = string_of_id s in let slen = String.length s in - if numstart = slen then + if numstart = slen then (s, None) else (String.sub s 0 numstart, Some (int_of_string (String.sub s numstart (slen - numstart)))) let make_ident sa = function - | Some n -> + | Some n -> let c = Char.code (String.get sa (String.length sa -1)) in let s = if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n) @@ -116,21 +116,21 @@ let atompart_of_id id = fst (repr_ident id) let lift_ident = lift_subscript -let next_ident_away id avoid = +let next_ident_away id avoid = if List.mem id avoid then - let id0 = if not (has_subscript id) then id else - (* Ce serait sans doute mieux avec quelque chose inspiré de + let id0 = if not (has_subscript id) then id else + (* Ce serait sans doute mieux avec quelque chose inspiré de *** make_ident id (Some 0) *** mais ça brise la compatibilité... *) forget_subscript id in let rec name_rec id = - if List.mem id avoid then name_rec (lift_ident id) else id in + if List.mem id avoid then name_rec (lift_ident id) else id in name_rec id0 else id -let next_ident_away_from id avoid = +let next_ident_away_from id avoid = let rec name_rec id = - if List.mem id avoid then name_rec (lift_ident id) else id in - name_rec id + if List.mem id avoid then name_rec (lift_ident id) else id in + name_rec id (* Names *) @@ -147,7 +147,7 @@ let name_iter f na = name_fold (fun x () -> f x) na () let name_cons na l = match na with - | Anonymous -> l + | Anonymous -> l | Name id -> id::l let name_app f = function @@ -158,7 +158,7 @@ let name_fold_map f e = function | Name id -> let (e,id) = f e id in (e,Name id) | Anonymous -> e,Anonymous -let next_name_away_with_default default name l = +let next_name_away_with_default default name l = match name with | Name str -> next_ident_away str l | Anonymous -> next_ident_away (id_of_string default) l diff --git a/library/nametab.ml b/library/nametab.ml index 074386417..31915c95a 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -31,12 +31,12 @@ let error_global_not_found q = raise (GlobalizationError q) type ltac_constant = kernel_name -(* The visibility can be registered either +(* The visibility can be registered either - for all suffixes not shorter then a given int - when the object is loaded inside a module or - for a precise suffix, when the module containing (the module - containing ...) the object is open (imported) + containing ...) the object is open (imported) *) type visibility = Until of int | Exactly of int @@ -46,7 +46,7 @@ type visibility = Until of int | Exactly of int (* This module type will be instantiated by [full_path] of [dir_path] *) (* The [repr] function is assumed to return the reversed list of idents. *) -module type UserName = sig +module type UserName = sig type t val to_string : t -> string val repr : t -> identifier * module_ident list @@ -57,15 +57,15 @@ end partially qualified names of type [qualid]. The mapping of partially qualified names to ['a] is determined by the [visibility] parameter of [push]. - + The [shortest_qualid] function given a user_name Coq.A.B.x, tries to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes - the same object. + the same object. *) module type NAMETREE = sig type 'a t type user_name - + val empty : 'a t val push : visibility -> user_name -> 'a -> 'a t -> 'a t val locate : qualid -> 'a t -> 'a @@ -76,15 +76,15 @@ module type NAMETREE = sig val find_prefixes : qualid -> 'a t -> 'a list end -module Make(U:UserName) : NAMETREE with type user_name = U.t - = +module Make(U:UserName) : NAMETREE with type user_name = U.t + = struct type user_name = U.t - type 'a path_status = - Nothing - | Relative of user_name * 'a + type 'a path_status = + Nothing + | Relative of user_name * 'a | Absolute of user_name * 'a (* Dictionaries of short names *) @@ -93,38 +93,38 @@ struct type 'a t = 'a nametree Idmap.t let empty = Idmap.empty - - (* [push_until] is used to register [Until vis] visibility and + + (* [push_until] is used to register [Until vis] visibility and [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*) let rec push_until uname o level (current,dirmap) = function | modid :: path -> - let mc = + let mc = try ModIdmap.find modid dirmap with Not_found -> (Nothing, ModIdmap.empty) in let this = if level <= 0 then match current with - | Absolute (n,_) -> - (* This is an absolute name, we must keep it + | Absolute (n,_) -> + (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) Flags.if_verbose - warning ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!"); + warning ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!"); current | Nothing | Relative _ -> Relative (uname,o) - else current + else current in let ptab' = push_until uname o (level-1) mc path in (this, ModIdmap.add modid ptab' dirmap) - | [] -> + | [] -> match current with - | Absolute (uname',o') -> + | Absolute (uname',o') -> if o'=o then begin assert (uname=uname'); - current, dirmap + current, dirmap (* we are putting the same thing for the second time :) *) end else @@ -139,15 +139,15 @@ struct let rec push_exactly uname o level (current,dirmap) = function | modid :: path -> - let mc = + let mc = try ModIdmap.find modid dirmap with Not_found -> (Nothing, ModIdmap.empty) in if level = 0 then let this = match current with - | Absolute (n,_) -> - (* This is an absolute name, we must keep it + | Absolute (n,_) -> + (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) Flags.if_verbose warning ("Trying to mask the absolute name \"" @@ -160,7 +160,7 @@ let rec push_exactly uname o level (current,dirmap) = function else (* not right level *) let ptab' = push_exactly uname o (level-1) mc path in (current, ModIdmap.add modid ptab' dirmap) - | [] -> + | [] -> anomaly "Prefix longer than path! Impossible!" @@ -168,7 +168,7 @@ let push visibility uname o tab = let id,dir = U.repr uname in let ptab = try Idmap.find id tab - with Not_found -> (Nothing, ModIdmap.empty) + with Not_found -> (Nothing, ModIdmap.empty) in let ptab' = match visibility with | Until i -> push_until uname o (i-1) ptab dir @@ -180,46 +180,46 @@ let push visibility uname o tab = let rec search (current,modidtab) = function | modid :: path -> search (ModIdmap.find modid modidtab) path | [] -> current - + let find_node qid tab = let (dir,id) = repr_qualid qid in search (Idmap.find id tab) (repr_dirpath dir) -let locate qid tab = +let locate qid tab = let o = match find_node qid tab with | Absolute (uname,o) | Relative (uname,o) -> o - | Nothing -> raise Not_found + | Nothing -> raise Not_found in o let user_name qid tab = let uname = match find_node qid tab with | Absolute (uname,o) | Relative (uname,o) -> uname - | Nothing -> raise Not_found + | Nothing -> raise Not_found in uname - -let find uname tab = + +let find uname tab = let id,l = U.repr uname in match search (Idmap.find id tab) l with Absolute (_,o) -> o | _ -> raise Not_found let exists uname tab = - try + try let _ = find uname tab in true with Not_found -> false -let shortest_qualid ctx uname tab = +let shortest_qualid ctx uname tab = let id,dir = U.repr uname in let hidden = Idset.mem id ctx in let rec find_uname pos dir (path,tab) = match path with | Absolute (u,_) | Relative (u,_) when u=uname && not(pos=[] && hidden) -> List.rev pos - | _ -> - match dir with + | _ -> + match dir with [] -> raise Not_found | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tab) in @@ -239,7 +239,7 @@ let rec flatten_idmap tab l = let rec search_prefixes (current,modidtab) = function | modid :: path -> search_prefixes (ModIdmap.find modid modidtab) path | [] -> List.rev (flatten_idmap modidtab (push_node current [])) - + let find_prefixes qid tab = try let (dir,id) = repr_qualid qid in @@ -252,10 +252,10 @@ end (* Global name tables *************************************************) -module SpTab = Make (struct +module SpTab = Make (struct type t = full_path let to_string = string_of_path - let repr sp = + let repr sp = let dir,id = repr_path sp in id, (repr_dirpath dir) end) @@ -271,7 +271,7 @@ type mptab = module_path SpTab.t let the_modtypetab = ref (SpTab.empty : mptab) -module DirTab = Make(struct +module DirTab = Make(struct type t = dir_path let to_string = string_of_dirpath let repr dir = match repr_dirpath dir with @@ -288,9 +288,9 @@ let the_dirtab = ref (DirTab.empty : dirtab) (* Reversed name tables ***************************************************) (* This table translates extended_global_references back to section paths *) -module Globrevtab = Map.Make(struct - type t=extended_global_reference - let compare = compare +module Globrevtab = Map.Make(struct + type t=extended_global_reference + let compare = compare end) type globrevtab = full_path Globrevtab.t @@ -316,7 +316,7 @@ let the_tacticrevtab = ref (KNmap.empty : knrevtab) let push_xref visibility sp xref = the_ccitab := SpTab.push visibility sp xref !the_ccitab; match visibility with - | Until _ -> + | Until _ -> if Globrevtab.mem xref !the_globrevtab then () else @@ -332,19 +332,19 @@ let push_syndef visibility sp kn = let push = push_cci -let push_modtype vis sp kn = +let push_modtype vis sp kn = the_modtypetab := SpTab.push vis sp kn !the_modtypetab; the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab (* This is for tactic definition names *) -let push_tactic vis sp kn = +let push_tactic vis sp kn = the_tactictab := SpTab.push vis sp kn !the_tactictab; the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab (* This is to remember absolute Section/Module names and to avoid redundancy *) -let push_dir vis dir dir_ref = +let push_dir vis dir dir_ref = the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; match dir_ref with DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab @@ -375,23 +375,23 @@ let full_name_tactic qid = SpTab.user_name qid !the_tactictab let locate_dir qid = DirTab.locate qid !the_dirtab -let locate_module qid = +let locate_module qid = match locate_dir qid with | DirModule (_,(mp,_)) -> mp | _ -> raise Not_found -let full_name_module qid = +let full_name_module qid = match locate_dir qid with | DirModule (dir,_) -> dir | _ -> raise Not_found let locate_section qid = match locate_dir qid with - | DirOpenSection (dir, _) + | DirOpenSection (dir, _) | DirClosedSection dir -> dir | _ -> raise Not_found -let locate_all qid = +let locate_all qid = List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l) (SpTab.find_prefixes qid !the_ccitab) [] @@ -404,7 +404,7 @@ let locate_constant qid = | TrueGlobal (ConstRef kn) -> kn | _ -> raise Not_found -let locate_mind qid = +let locate_mind qid = match locate_extended qid with | TrueGlobal (IndRef (kn,0)) -> kn | _ -> raise Not_found @@ -423,7 +423,7 @@ let global r = let (loc,qid) = qualid_of_reference r in try match locate_extended qid with | TrueGlobal ref -> ref - | SynDef _ -> + | SynDef _ -> user_err_loc (loc,"global", str "Unexpected reference to a notation: " ++ pr_qualid qid) @@ -433,7 +433,7 @@ let global r = (* Exists functions ********************************************************) let exists_cci sp = SpTab.exists sp !the_ccitab - + let exists_dir dir = DirTab.exists dir !the_dirtab let exists_section = exists_dir @@ -446,18 +446,18 @@ let exists_tactic sp = SpTab.exists sp !the_tactictab (* Reverse locate functions ***********************************************) -let path_of_global ref = +let path_of_global ref = match ref with | VarRef id -> make_path empty_dirpath id | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab -let dirpath_of_global ref = +let dirpath_of_global ref = fst (repr_path (path_of_global ref)) -let basename_of_global ref = +let basename_of_global ref = snd (repr_path (path_of_global ref)) -let path_of_syndef kn = +let path_of_syndef kn = Globrevtab.find (SynDef kn) !the_globrevtab let dirpath_of_module mp = @@ -466,18 +466,18 @@ let dirpath_of_module mp = (* Shortest qualid functions **********************************************) -let shortest_qualid_of_global ctx ref = +let shortest_qualid_of_global ctx ref = match ref with | VarRef id -> make_qualid empty_dirpath id | _ -> let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in SpTab.shortest_qualid ctx sp !the_ccitab -let shortest_qualid_of_syndef ctx kn = +let shortest_qualid_of_syndef ctx kn = let sp = path_of_syndef kn in SpTab.shortest_qualid ctx sp !the_ccitab -let shortest_qualid_of_module mp = +let shortest_qualid_of_module mp = let dir = MPmap.find mp !the_modrevtab in DirTab.shortest_qualid Idset.empty dir !the_dirtab @@ -512,8 +512,8 @@ let global_inductive r = type frozen = ccitab * dirtab * kntab * kntab * globrevtab * mprevtab * knrevtab * knrevtab -let init () = - the_ccitab := SpTab.empty; +let init () = + the_ccitab := SpTab.empty; the_dirtab := DirTab.empty; the_modtypetab := SpTab.empty; the_tactictab := SpTab.empty; @@ -525,7 +525,7 @@ let init () = let freeze () = - !the_ccitab, + !the_ccitab, !the_dirtab, !the_modtypetab, !the_tactictab, @@ -544,7 +544,7 @@ let unfreeze (ccit,dirt,mtyt,tact,globr,modr,mtyr,tacr) = the_modtyperevtab := mtyr; the_tacticrevtab := tacr -let _ = +let _ = Summary.declare_summary "names" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; diff --git a/library/nametab.mli b/library/nametab.mli index 774b148a5..98a482896 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -35,15 +35,15 @@ open Libnames (* Most functions in this module fall into one of the following categories: \begin{itemize} \item [push : visibility -> full_user_name -> object_reference -> unit] - + Registers the [object_reference] to be referred to by the [full_user_name] (and its suffixes according to [visibility]). [full_user_name] can either be a [full_path] or a [dir_path]. - \item [exists : full_user_name -> bool] - + \item [exists : full_user_name -> bool] + Is the [full_user_name] already atributed as an absolute user name - of some object? + of some object? \item [locate : qualid -> object_reference] @@ -52,16 +52,16 @@ open Libnames \item [full_name : qualid -> full_user_name] Finds the full user name referred to by [qualid] or raises [Not_found] - + \item [shortest_qualid_of : object_reference -> user_name] - The [user_name] can be for example the shortest non ambiguous [qualid] or - the [full_user_name] or [identifier]. Such a function can also have a - local context argument. + The [user_name] can be for example the shortest non ambiguous [qualid] or + the [full_user_name] or [identifier]. Such a function can also have a + local context argument. \end{itemize} *) - - + + exception GlobalizationError of qualid exception GlobalizationConstantError of qualid @@ -79,7 +79,7 @@ val error_global_constant_not_found_loc : loc -> qualid -> 'a object is loaded inside a module -- or \item for a precise suffix, when the module containing (the module - containing ...) the object is opened (imported) + containing ...) the object is opened (imported) \end{itemize} *) diff --git a/library/states.ml b/library/states.ml index 4fbc4c886..c4e766095 100644 --- a/library/states.ml +++ b/library/states.ml @@ -31,14 +31,14 @@ let (extern_state,intern_state) = let with_heavy_rollback f x = let st = freeze () in - try + try f x with reraise -> (unfreeze st; raise reraise) let with_state_protection f x = let st = freeze () in - try + try let a = f x in unfreeze st; a with reraise -> (unfreeze st; raise reraise) diff --git a/library/states.mli b/library/states.mli index 17f62b512..782e41ca7 100644 --- a/library/states.mli +++ b/library/states.mli @@ -10,7 +10,7 @@ (*s States of the system. In that module, we provide functions to get and set the state of the whole system. Internally, it is done by - freezing the states of both [Lib] and [Summary]. We provide functions + freezing the states of both [Lib] and [Summary]. We provide functions to write and restore state to and from a given file. *) val intern_state : string -> unit @@ -21,7 +21,7 @@ val freeze : unit -> state val unfreeze : state -> unit (*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the - state of the whole system as it was before the evaluation if an exception + state of the whole system as it was before the evaluation if an exception is raised. *) val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b diff --git a/library/summary.ml b/library/summary.ml index 784d79d87..e9b0bbd36 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -16,7 +16,7 @@ type 'a summary_declaration = { unfreeze_function : 'a -> unit; init_function : unit -> unit } -let summaries = +let summaries = (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t) let internal_declare_summary sumname sdecl = @@ -34,22 +34,22 @@ let internal_declare_summary sumname sdecl = (str "Cannot declare a summary twice: " ++ str sumname); Hashtbl.add summaries sumname ddecl -let declare_summary sumname decl = +let declare_summary sumname decl = internal_declare_summary (sumname^"-SUMMARY") decl type frozen = Dyn.t Stringmap.t let freeze_summaries () = let m = ref Stringmap.empty in - Hashtbl.iter + Hashtbl.iter (fun id decl -> m := Stringmap.add id (decl.freeze_function()) !m) summaries; !m -let unfreeze_summaries fs = +let unfreeze_summaries fs = Hashtbl.iter - (fun id decl -> + (fun id decl -> try decl.unfreeze_function (Stringmap.find id fs) with Not_found -> decl.init_function()) summaries -- cgit v1.2.3