From 3386a50c15ddc367cd247f288ff84f288a0c42af Mon Sep 17 00:00:00 2001 From: filliatr Date: Sat, 18 Sep 1999 16:13:36 +0000 Subject: module Library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@74 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/global.ml | 2 + library/global.mli | 3 + library/lib.ml | 8 ++- library/lib.mli | 5 +- library/libobject.ml | 56 +++++++++---------- library/libobject.mli | 18 +++--- library/library.ml | 150 ++++++++++++++++++++++++++++++++++++++++++++++++++ library/library.mli | 28 ++++++++++ 8 files changed, 230 insertions(+), 40 deletions(-) create mode 100644 library/library.ml create mode 100644 library/library.mli (limited to 'library') diff --git a/library/global.ml b/library/global.ml index d669410b8..d7267a96d 100644 --- a/library/global.ml +++ b/library/global.ml @@ -35,3 +35,5 @@ let lookup_mind sp = lookup_mind sp !global_env let lookup_mind_specif c = lookup_mind_specif c !global_env let lookup_meta n = lookup_meta n !global_env +let export s = export !global_env s +let import cenv = global_env := import cenv !global_env diff --git a/library/global.mli b/library/global.mli index 4f04d2e51..d21509e32 100644 --- a/library/global.mli +++ b/library/global.mli @@ -9,6 +9,7 @@ open Sign open Evd open Constant open Inductive +open Environ (*i*) (* This module defines the global environment of Coq. @@ -33,3 +34,5 @@ val lookup_mind : section_path -> mutual_inductive_body val lookup_mind_specif : constr -> mind_specif val lookup_meta : int -> constr +val export : string -> compiled_env +val import : compiled_env -> unit diff --git a/library/lib.ml b/library/lib.ml index a8ab156c5..42850bc05 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -20,7 +20,11 @@ type library_entry = section_path * node (* We keep trace of operations in a stack [lib_stk]. - [path_prefix] is the current path of sections (in correct order). *) + [path_prefix] is the current path of sections. 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. *) let lib_stk = ref ([] : (section_path * node) list) @@ -122,7 +126,7 @@ let close_section s = in let (after,_,before) = split_lib sp in lib_stk := before; - add_entry sp (ClosedSection (s,modp,after)); + add_entry sp (ClosedSection (s,modp,List.rev after)); add_frozen_state (); pop_path_prefix () diff --git a/library/lib.mli b/library/lib.mli index 80f61ef40..a38fb4cef 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -25,7 +25,7 @@ type library_entry = section_path * node (*s Adding operations, and getting the current list of operations (most - recent ones come first). *) + recent ones coming first). *) val add_leaf : identifier -> obj -> section_path val add_anonymous_leaf : obj -> unit @@ -33,7 +33,8 @@ val add_anonymous_leaf : obj -> unit val contents_after : section_path option -> library_segment -(*s Opening and closing a section. *) +(*s Opening and closing a section. The boolean in [open_section] indicates + a module. *) val open_section : string -> bool -> section_path val close_section : string -> unit diff --git a/library/libobject.ml b/library/libobject.ml index f5e610704..1096ac43a 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -5,15 +5,17 @@ open Util open Names type 'a object_declaration = { - load_function : 'a -> unit; cache_function : section_path * 'a -> unit; + load_function : 'a -> unit; + open_function : 'a -> unit; specification_function : 'a -> 'a } type obj = Dyn.t (* persistent dynamic objects *) type dynamic_object_declaration = { - dyn_load_function : obj -> unit; dyn_cache_function : section_path * obj -> unit; + dyn_load_function : obj -> unit; + dyn_open_function : obj -> unit; dyn_specification_function : obj -> obj } let object_tag lobj = Dyn.tag lobj @@ -23,41 +25,39 @@ let cache_tab = let declare_object (na,odecl) = let (infun,outfun) = Dyn.create na in - let loader lobj = - if Dyn.tag lobj = na then odecl.load_function (outfun lobj) - else anomaly "somehow we got the wrong dynamic object in the loadfun" - and cacher (spopt,lobj) = + let cacher (spopt,lobj) = if Dyn.tag lobj = na then odecl.cache_function(spopt,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the cachefun" + and loader lobj = + if Dyn.tag lobj = na then odecl.load_function (outfun lobj) + else anomaly "somehow we got the wrong dynamic object in the loadfun" + and opener lobj = + if Dyn.tag lobj = na then odecl.open_function (outfun lobj) + else anomaly "somehow we got the wrong dynamic object in the openfun" and spec_extractor lobj = infun(odecl.specification_function (outfun lobj)) in - Hashtbl.add cache_tab na { dyn_load_function = loader; - dyn_cache_function = cacher; + Hashtbl.add cache_tab na { dyn_cache_function = cacher; + dyn_load_function = loader; + dyn_open_function = opener; dyn_specification_function = spec_extractor }; (infun,outfun) - -let load_object lobj = +let apply_dyn_fun f lobj = let tag = object_tag lobj in - try - let dodecl = Hashtbl.find cache_tab tag in - dodecl.dyn_load_function lobj - with Not_found -> - anomaly ("Cannot find loadfun for an object with tag "^tag) + try + let dodecl = Hashtbl.find cache_tab tag in f dodecl + with Not_found -> + anomaly ("Cannot find library functions for an object with tag "^tag) -let cache_object (spopt,lobj) = - let tag = object_tag lobj in - try - let dodecl = Hashtbl.find cache_tab tag in - dodecl.dyn_cache_function(spopt,lobj) - with Not_found -> - anomaly ("Cannot find cachefun for an object with tag "^tag) +let cache_object ((_,lobj) as node) = + apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj + +let load_object lobj = + apply_dyn_fun (fun d -> d.dyn_load_function lobj) lobj + +let open_object lobj = + apply_dyn_fun (fun d -> d.dyn_open_function lobj) lobj let extract_object_specification lobj = - let tag = object_tag lobj in - try - let dodecl = Hashtbl.find cache_tab tag in - dodecl.dyn_specification_function lobj - with Not_found -> - anomaly ("Cannot find specification extractor for an object with tag "^tag) + apply_dyn_fun (fun d -> d.dyn_specification_function lobj) lobj diff --git a/library/libobject.mli b/library/libobject.mli index 967e4c410..7ddac57b2 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -5,20 +5,23 @@ open Names (*i*) -(* [Libobject] declares persistent objects given with three methods: +(* [Libobject] declares persistent objects, given with three methods: + - a caching function specifying how to add the object in the current + scope of theory modules; - a loading function, specifying what to do when the object is loaded from the disk; - - a caching function specifying how to import the object in the current - scope of theory modules; + - an opening function, specifying what to do when the module containing + the object is opened; - a specification function, to extract its specification when writing the specification of a module to the disk (.vi) *) type 'a object_declaration = { - load_function : 'a -> unit; cache_function : section_path * 'a -> unit; + load_function : 'a -> unit; + open_function : 'a -> unit; specification_function : 'a -> 'a } -(*s given the object-name, the "loading" function, the "caching" function, +(*s Given the object-name, the "loading" function, the "caching" function, and the "specification" function, the function [declare_object] will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects. *) @@ -30,8 +33,7 @@ val declare_object : val object_tag : obj -> string -val load_object : obj -> unit - val cache_object : (section_path * obj) -> unit - +val load_object : obj -> unit +val open_object : obj -> unit val extract_object_specification : obj -> obj diff --git a/library/library.ml b/library/library.ml new file mode 100644 index 000000000..7de5a845d --- /dev/null +++ b/library/library.ml @@ -0,0 +1,150 @@ + +(* $Id$ *) + +open Util +open Names +open Environ +open Libobject +open Lib + +(* Modules on disk contain the following informations (after the magic + number, and before the digest). *) + +type module_disk = { + md_name : string; + md_compiled_env : compiled_env; + md_declarations : library_segment; + md_deps : (string * Digest.t * bool) list } + +(* Modules loaded in memory contain the following informations. They are + kept in the hash table [modules_table]. *) + +type module_t = { + module_name : string; + module_compiled_env : compiled_env; + module_declarations : library_segment; + mutable module_opened : bool; + mutable module_exported : bool; + module_deps : (string * Digest.t * bool) list; + module_digest : Digest.t } + +let modules_table = + (Hashtbl.create 17 : (string, module_t) Hashtbl.t) + +let find_module s = + try + Hashtbl.find modules_table s + with Not_found -> + error ("Unknown module " ^ s) + +let module_is_loaded s = + try let _ = Hashtbl.find modules_table s in true with Not_found -> false + +let module_is_opened s = + (find_module s).module_opened + +let vo_magic_number = 0700 + +let (raw_extern_module, raw_intern_module) = + System.raw_extern_intern vo_magic_number ".vo" + +let segment_iter f = + let rec apply = function + | _,Leaf obj -> f obj + | _,ClosedSection (_,_,mseg) -> iter mseg + | _,OpenedSection _ -> assert false + | _,FrozenState _ -> () + and iter seg = + List.iter apply seg + in + iter + + +(* [open_module s] opens a module which is assumed to be already loaded. *) + +let open_module s = + let m = find_module s in + if not m.module_opened then begin + segment_iter open_object m.module_declarations; + m.module_opened <- true + end + + +(* [load_module s] loads the module [s] from the disk, and [find_module s] + returns the module of name [s], loading it if necessary. + The boolean [doexp] specifies if we open the modules which are declared + exported in the dependencies (usually it is [true] at the highest level; + it is always [false] in recursive loadings). *) + +let load_objects s = + let m = find_module s in + segment_iter load_object m.module_declarations + +let rec load_module_from doexp s f = + let (fname,ch) = raw_intern_module f in + let md = input_value ch in + let digest = input_value ch in + close_in ch; + let m = { module_name = md.md_name; + module_compiled_env = md.md_compiled_env; + module_declarations = md.md_declarations; + module_opened = false; + module_exported = false; + module_deps = md.md_deps; + module_digest = digest } in + if s <> md.md_name then + error ("The file " ^ fname ^ " does not contain module " ^ s); + List.iter (load_mandatory_module doexp s) m.module_deps; + Hashtbl.add modules_table s m; + m + +and load_mandatory_module doexp caller (s,d,export) = + let m = find_module false s s in + if d <> m.module_digest then + error ("module "^caller^" makes inconsistent assumptions over module "^s); + if doexp && export then open_module s + +and find_module doexp s f = + try Hashtbl.find modules_table s with Not_found -> load_module_from doexp s f + + +let load_module s = function + | None -> let _ = load_module_from true s s in () + | Some f -> let _ = load_module_from true s f in () + + +(* [require_module] loads and opens a module. *) + +let require_module spec name fileopt export = + let file = match fileopt with + | None -> name + | Some f -> f in + let m = load_module_from true name file in + open_module name; + if export then m.module_exported <- true + + +(* [save_module s] saves the module [m] to the disk. *) + +let current_imports () = + let l = ref [] in + Hashtbl.iter + (fun _ m -> l := (m.module_name, m.module_digest, m.module_exported) :: !l) + modules_table; + !l + +let save_module_to s f = + let seg = contents_after None in + let md = { + md_name = s; + md_compiled_env = Global.export s; + md_declarations = seg; + md_deps = current_imports () } in + let (_,ch) = raw_extern_module f in + output_value ch md; + flush ch; + let di = Digest.file f in + output_value ch di; + close_out ch + + diff --git a/library/library.mli b/library/library.mli new file mode 100644 index 000000000..2c54aec2e --- /dev/null +++ b/library/library.mli @@ -0,0 +1,28 @@ + +(* $Id$ *) + +(* This module is the heart of the library. It provides low level functions to + load, open and save modules. Modules are saved onto the disk with checksums + (obtained with the [Digest] module), which are checked at loading time to + prevent inconsistencies between files written at various dates. It also + provides a high level function [require] which corresponds to the + vernacular command [Require]. *) + +val load_module : string -> string option -> unit +val open_module : string -> unit + +val module_is_loaded : string -> bool +val module_is_opened : string -> bool + +(*s Require. The command [require_module spec m file export] loads and opens + a module [m]. [file] specifies the filename, if not [None]. [spec] + specifies to look for a specification ([true]) or for an implementation + ([false]), if not [None]. And [export] specifies if the module must be + exported. *) + +val require_module : bool option -> string -> string option -> bool -> unit + +(*s [save_module_to s f] saves the current environment as a module [s] + in the file [f]. *) + +val save_module_to : string -> string -> unit -- cgit v1.2.3