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 --- .depend | 93 +++++++++++++------------------ Makefile | 8 +-- configure | 6 +- dev/TODO | 20 ++++++- kernel/typing.ml | 2 + kernel/typing.mli | 3 + lib/system.ml | 58 ++++++++++++------- lib/system.mli | 11 ++++ 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 ++++++++++ 16 files changed, 347 insertions(+), 124 deletions(-) create mode 100644 library/library.ml create mode 100644 library/library.mli diff --git a/.depend b/.depend index 630144ee2..f6060aaf2 100644 --- a/.depend +++ b/.depend @@ -28,18 +28,17 @@ kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi lib/util.cmi: lib/pp.cmi -library/global.cmi: kernel/constant.cmi kernel/evd.cmi kernel/inductive.cmi \ - kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi +library/global.cmi: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ + kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/univ.cmi library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi library/libobject.cmi: kernel/names.cmi library/summary.cmi: kernel/names.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/pcoq.cmi lib/pp.cmi parsing/coqast.cmi: lib/dyn.cmi -parsing/g_minicoq.cmi: /usr/local/lib/camlp4/grammar.cmi kernel/names.cmi \ - lib/pp.cmi kernel/term.cmi -parsing/lexer.cmi: /usr/local/lib/camlp4/token.cmi -parsing/pcoq.cmi: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \ - /usr/local/lib/camlp4/grammar.cmi /usr/local/lib/camlp4/token.cmi +parsing/g_minicoq.cmi: kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ + kernel/term.cmi +parsing/pcoq.cmi: parsing/coqast.cmi toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi config/coq_config.cmo: config/coq_config.cmi @@ -162,6 +161,10 @@ library/libobject.cmo: lib/dyn.cmi kernel/names.cmi lib/util.cmi \ library/libobject.cmi library/libobject.cmx: lib/dyn.cmx kernel/names.cmx lib/util.cmx \ library/libobject.cmi +library/library.cmo: kernel/environ.cmi library/lib.cmi library/libobject.cmi \ + kernel/names.cmi lib/system.cmi lib/util.cmi library/library.cmi +library/library.cmx: kernel/environ.cmx library/lib.cmx library/libobject.cmx \ + kernel/names.cmx lib/system.cmx lib/util.cmx library/library.cmi library/states.cmo: library/lib.cmi library/summary.cmi lib/system.cmi \ library/states.cmi library/states.cmx: library/lib.cmx library/summary.cmx lib/system.cmx \ @@ -171,11 +174,9 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ library/summary.cmi parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \ - parsing/pcoq.cmi lib/pp.cmi /usr/local/lib/camlp4/stdpp.cmi lib/util.cmi \ - parsing/ast.cmi + parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \ - parsing/pcoq.cmi lib/pp.cmx /usr/local/lib/camlp4/stdpp.cmi lib/util.cmx \ - parsing/ast.cmi + parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi @@ -187,54 +188,38 @@ toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \ - kernel/generic.cmi /usr/local/lib/camlp4/grammar.cmi toplevel/himsg.cmi \ - kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ - /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmi kernel/type_errors.cmi \ - kernel/typing.cmi lib/util.cmi + kernel/generic.cmi toplevel/himsg.cmi kernel/inductive.cmi \ + kernel/names.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/type_errors.cmi kernel/typing.cmi lib/util.cmi toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \ - kernel/generic.cmx /usr/local/lib/camlp4/grammar.cmi toplevel/himsg.cmx \ - kernel/inductive.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \ - /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmx kernel/type_errors.cmx \ - kernel/typing.cmx lib/util.cmx -parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi \ - /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi -parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx \ - /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi -parsing/g_command.cmo: parsing/ast.cmi parsing/coqast.cmi \ - /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi -parsing/g_command.cmx: parsing/ast.cmx parsing/coqast.cmx \ - /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi -parsing/g_minicoq.cmo: kernel/generic.cmi /usr/local/lib/camlp4/gramext.cmi \ - /usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmi kernel/names.cmi \ - lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ + kernel/generic.cmx toplevel/himsg.cmx kernel/inductive.cmx \ + kernel/names.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/type_errors.cmx kernel/typing.cmx lib/util.cmx +parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi +parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi +parsing/g_command.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi +parsing/g_command.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi +parsing/g_minicoq.cmo: kernel/generic.cmi parsing/lexer.cmi kernel/names.cmi \ + lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ parsing/g_minicoq.cmi -parsing/g_minicoq.cmx: kernel/generic.cmx /usr/local/lib/camlp4/gramext.cmi \ - /usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmx kernel/names.cmx \ - lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ +parsing/g_minicoq.cmx: kernel/generic.cmx parsing/lexer.cmx kernel/names.cmx \ + lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ parsing/g_minicoq.cmi parsing/g_multiple_case.cmo: parsing/ast.cmi parsing/coqast.cmi \ - /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi -parsing/g_multiple_case.cmx: parsing/ast.cmx parsing/coqast.cmx \ - /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi -parsing/g_prim.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \ - parsing/pcoq.cmi -parsing/g_prim.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \ parsing/pcoq.cmi -parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi \ - /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi lib/pp.cmi -parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx \ - /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi lib/pp.cmx -parsing/g_vernac.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \ - parsing/pcoq.cmi -parsing/g_vernac.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \ +parsing/g_multiple_case.cmx: parsing/ast.cmx parsing/coqast.cmx \ parsing/pcoq.cmi -parsing/pcoq.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \ - /usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmi lib/pp.cmi \ +parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi +parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmi +parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ + lib/pp.cmi +parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi \ + lib/pp.cmx +parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi +parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmi +parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \ lib/util.cmi parsing/pcoq.cmi -parsing/pcoq.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \ - /usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmx lib/pp.cmx \ +parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \ lib/util.cmx parsing/pcoq.cmi -parsing/q_coqast.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/mLast.cmi \ - parsing/pcoq.cmi /usr/local/lib/camlp4/quotation.cmi -parsing/q_coqast.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/mLast.cmi \ - parsing/pcoq.cmi /usr/local/lib/camlp4/quotation.cmi +parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi +parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmi diff --git a/Makefile b/Makefile index 6ee0156d8..80d6cfc53 100644 --- a/Makefile +++ b/Makefile @@ -10,13 +10,13 @@ noargument: @echo " make cleanall" @echo or make archclean -INCLUDES=-I config -I lib -I kernel -I library -I parsing -I toplevel \ - -I $(CAMLP4LIB) +LOCALINCLUDES=-I config -I lib -I kernel -I library -I parsing -I toplevel +INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB) BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG) OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF) OCAMLDEP=ocamldep -DEPFLAGS=$(INCLUDES) +DEPFLAGS=$(LOCALINCLUDES) CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS) @@ -42,7 +42,7 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ kernel/typing.cmo LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \ - library/global.cmo library/states.cmo + library/global.cmo library/states.cmo library/library.cmo PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \ diff --git a/configure b/configure index 8da11ae6c..0cdd5f36a 100755 --- a/configure +++ b/configure @@ -237,15 +237,15 @@ esac # Objective Caml programs -CAMLC=`which ocamlc` +CAMLC=`which $bytecamlc` case $CAMLC in - "") echo "ocamlc is not present in your path !" + "") echo "$bytecamlc is not present in your path !" echo "Give me manually the path to the ocamlc executable [/usr/local/bin by default]: " read CAMLC case $CAMLC in "") CAMLC=/usr/local/bin/ocamlc;; - */ocamlc) true;; + */ocamlc|*/ocamlc.opt) true;; */) CAMLC=${CAMLC}ocamlc;; *) CAMLC=${CAMLC}/ocamlc;; esac;; diff --git a/dev/TODO b/dev/TODO index 136ca5879..5a6e5b70e 100644 --- a/dev/TODO +++ b/dev/TODO @@ -1,11 +1,25 @@ - o Minicoq - utilisation de Himsg + o Univers + - définir un type d'ensemble de contraintes, et sauver cet ensemble + pour chaque module et non pas le graphe complet + + o configure + - il faut tester la version du programme correspondant à $bytecamlc + qui peut être ocamlc ou ocamlc.opt, et non pas la version de "ocamlc" + seulement + + o Environnements compilés (type Environ.compiled_env) + - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?) + + o Efficacité + - utiliser DOPL plutôt que DOPN (sauf pour Case) + - batch mode => pas de undo, ni de reset + - conversion : déplier la constante la plus récente o Lexer à compléter o Toplevel - boucle principale, affichage des erreur, du prompt - - parsing de la ligne de commande (Arg ?) + - parsing de la ligne de commande (utiliser Arg) diff --git a/kernel/typing.ml b/kernel/typing.ml index 7cd127cf6..1fcf340f3 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -421,6 +421,8 @@ let add_mind sp mie env = in add_mind sp mib (set_universes (universes env_arities') env) +let export = export +let import = import (*s Machines with information. *) diff --git a/kernel/typing.mli b/kernel/typing.mli index d9d410c54..0167c8cd9 100644 --- a/kernel/typing.mli +++ b/kernel/typing.mli @@ -41,6 +41,9 @@ val lookup_mind : section_path -> 'a environment -> mutual_inductive_body val lookup_mind_specif : constr -> 'a environment -> mind_specif val lookup_meta : int -> 'a environment -> constr +val export : 'a environment -> string -> compiled_env +val import : compiled_env -> 'a environment -> 'a environment + (*s Typing without information. *) type judgment diff --git a/lib/system.ml b/lib/system.ml index 016a6f97e..ab24f734c 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -46,33 +46,51 @@ let open_trapping_failure open_fun name suffix = let rname = make_suffix name suffix in try open_fun rname with _ -> error ("Can't open " ^ rname) +let try_remove f = + try Sys.remove f + with _ -> mSGNL [< 'sTR"Warning: " ; 'sTR"Could not remove file " ; + 'sTR f ; 'sTR" which is corrupted !!" >] + +exception Bad_magic_number of string + +let (raw_extern_intern : + int -> string -> + (string -> string * out_channel) * (string -> string * in_channel)) + = fun magic suffix -> + + let extern_state name = + let (_,channel) as filec = + open_trapping_failure (fun n -> n,open_out_bin n) name suffix in + output_binary_int channel magic; + filec + and intern_state name = + let fname = find_file_in_path (make_suffix name suffix) in + let channel = open_in_bin fname in + if input_binary_int channel <> magic then + raise (Bad_magic_number fname); + (fname,channel) + in + (extern_state,intern_state) + let (extern_intern : - int -> string -> ((string -> 'a -> unit) * (string -> 'a))) + int -> string -> (string -> 'a -> unit) * (string -> 'a)) = fun magic suffix -> - let extern_state name val_0 = - try - let (expname,channel) = - open_trapping_failure (fun n -> n,open_out_bin n) name suffix in + let (raw_extern,raw_intern) = raw_extern_intern magic suffix in + let extern_state name val_0 = try - output_binary_int channel magic; - output_value channel val_0; - close_out channel - with e -> begin - (try Sys.remove expname - with _ -> mSGNL [< 'sTR"Warning: " ; 'sTR"Could not remove file " ; - 'sTR expname ; 'sTR" which is corrupted !!" >]); - raise e - end - with Sys_error s -> error ("System error: " ^ s) + let (fname,channel) = raw_extern name in + try + output_value channel val_0; + close_out channel + with e -> + begin try_remove fname; raise e end + with Sys_error s -> error ("System error: " ^ s) and intern_state name = try - let fname = find_file_in_path (make_suffix name suffix) in - let channel = open_in_bin fname in - if input_binary_int channel <> magic then - error (fname^" not compiled with the current version of Coq"); - let v = input_value(channel) in + let (fname,channel) = raw_intern name in + let v = input_value channel in close_in channel; v with Sys_error s -> error("System error: " ^ s) diff --git a/lib/system.mli b/lib/system.mli index b887f5eb5..f89e128cb 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -6,6 +6,17 @@ val add_path : string -> unit val del_path : string -> unit +val find_file_in_path : string -> string + +(*s Generic input and output functions, parameterized by a magic number + and a suffix. The intern functions raise the exception [Bad_magic_number] + when the check fails, with the full file name. *) + +exception Bad_magic_number of string + +val raw_extern_intern : int -> string -> + (string -> string * out_channel) * (string -> string * in_channel) + val extern_intern : int -> string -> (string -> 'a -> unit) * (string -> 'a) (*s Time stamps. *) 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