aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /library
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
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
Diffstat (limited to 'library')
-rw-r--r--library/decl_kinds.ml2
-rw-r--r--library/decl_kinds.mli2
-rw-r--r--library/declare.ml16
-rw-r--r--library/declare.mli4
-rw-r--r--library/declaremods.ml334
-rw-r--r--library/declaremods.mli22
-rw-r--r--library/decls.ml2
-rw-r--r--library/decls.mli2
-rw-r--r--library/dischargedhypsmap.ml4
-rw-r--r--library/global.ml20
-rw-r--r--library/global.mli8
-rw-r--r--library/goptions.ml74
-rw-r--r--library/goptions.mli10
-rw-r--r--library/heads.ml22
-rw-r--r--library/impargs.ml96
-rw-r--r--library/impargs.mli8
-rw-r--r--library/lib.ml172
-rw-r--r--library/lib.mli12
-rw-r--r--library/libnames.ml30
-rw-r--r--library/libnames.mli8
-rw-r--r--library/libobject.ml50
-rw-r--r--library/libobject.mli20
-rw-r--r--library/library.ml80
-rw-r--r--library/library.mllib2
-rw-r--r--library/nameops.ml32
-rw-r--r--library/nametab.ml132
-rwxr-xr-xlibrary/nametab.mli22
-rw-r--r--library/states.ml4
-rw-r--r--library/states.mli4
-rw-r--r--library/summary.ml10
30 files changed, 602 insertions, 602 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 20:48:14 +0000