diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | contrib/cc/cctac.ml4 | 2 | ||||
| -rw-r--r-- | contrib/correctness/ptactic.ml | 2 | ||||
| -rw-r--r-- | contrib/field/field.ml4 | 4 | ||||
| -rw-r--r-- | contrib/fourier/fourierR.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/parse.ml | 2 | ||||
| -rw-r--r-- | contrib/omega/coq_omega.ml | 2 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 2 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 2 | ||||
| -rw-r--r-- | doc/preamble.tex | 2 | ||||
| -rw-r--r-- | interp/coqlib.ml | 21 | ||||
| -rw-r--r-- | interp/coqlib.mli | 3 | ||||
| -rw-r--r-- | library/library.ml | 262 | ||||
| -rw-r--r-- | library/library.mli | 88 | ||||
| -rw-r--r-- | library/states.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 5 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 4 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 100 |
19 files changed, 204 insertions, 308 deletions
@@ -12,11 +12,12 @@ Gallina Ltac +- New primitive "external" for communication with tool external to Coq - Semantics of "match t with" changed: if a clause returns a tactic, it is now applied to the current goal. If it fails, the next clause or next matching subterm is tried (i.e. it behaves as "match goal with"). -- New modifier "lazy" for "match t with" and "match goal with" telling +- New modifier "lazy" (TODO) for "match t with" and "match goal with" telling to delay the evaluation of tactic expression. Tactics diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4 index 9dce63191..98ea8e495 100644 --- a/contrib/cc/cctac.ml4 +++ b/contrib/cc/cctac.ml4 @@ -232,7 +232,7 @@ let discriminate_tac axioms cstr p gls = (* wrap everything *) let cc_tactic gls= - Library.check_required_library ["Coq";"Init";"Logic"]; + Coqlib.check_required_library ["Coq";"Init";"Logic"]; let (axioms,disaxioms,glo)=make_prb gls in match (cc_proof axioms disaxioms glo) with `Prove_goal p -> proof_tac axioms p gls diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index bb6e33011..bd742b9df 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -234,7 +234,7 @@ let correctness_hook _ ref = register pf_id None let correctness s p opttac = - Library.check_required_library ["Coq";"correctness";"Correctness"]; + Coqlib.check_required_library ["Coq";"correctness";"Correctness"]; Pmisc.reset_names(); let p,oc,cty,v = coqast_of_prog p in let env = Global.env () in diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 94044cf20..9f887fc75 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -150,7 +150,7 @@ END (* Guesses the type and calls field_gen with the right theory *) let field g = - Library.check_required_library ["Coq";"field";"Field"]; + Coqlib.check_required_library ["Coq";"field";"Field"]; let ist = { lfun=[]; debug=get_debug () } in let typ = match Hipattern.match_with_equation (pf_concl g) with @@ -173,7 +173,7 @@ let guess_theory env evc = function (* Guesses the type and calls Field_Term with the right theory *) let field_term l g = - Library.check_required_library ["Coq";"field";"Field"]; + Coqlib.check_required_library ["Coq";"field";"Field"]; let env = (pf_env g) and evc = (project g) in let th = valueIn (VConstr (guess_theory env evc l)) diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 33d6faad1..5e31d5675 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -458,7 +458,7 @@ let mkAppL a = (* Résolution d'inéquations linéaires dans R *) let rec fourier gl= - Library.check_required_library ["Coq";"fourier";"Fourier"]; + Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; let goal = strip_outer_cast (pf_concl gl) in let fhyp=id_of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index 6a99aedc8..a6a8937ba 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -401,7 +401,7 @@ let load_syntax_action reqid module_name = msg (str "loading " ++ str module_name ++ str "... "); try (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in - read_library (dummy_loc,qid); + require_library [dummy_loc,qid] None; msg (str "opening... "); Declaremods.import_module false (Nametab.locate_module qid); msgnl (str "done" ++ fnl ()); diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 1e02f23b5..41eec8dc8 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -1785,7 +1785,7 @@ let destructure_goal gl = let destructure_goal = all_time (destructure_goal) let omega_solver gl = - Library.check_required_library ["Coq";"omega";"Omega"]; + Coqlib.check_required_library ["Coq";"omega";"Omega"]; let result = destructure_goal gl in (* if !display_time_flag then begin text_time (); flush Pervasives.stdout end; *) diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 5a381b57c..fb0e66526 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -385,7 +385,7 @@ let rec sort_subterm gl l = [gl: goal sigma]\\ *) let quote_terms ivs lc gl = - Library.check_required_library ["Coq";"ring";"Quote"]; + Coqlib.check_required_library ["Coq";"ring";"Quote"]; let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 384784fdc..d3068c862 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -885,7 +885,7 @@ let match_with_equiv c = match (kind_of_term c) with | _ -> None let polynom lc gl = - Library.check_required_library ["Coq";"ring";"Ring"]; + Coqlib.check_required_library ["Coq";"ring";"Ring"]; match lc with (* If no argument is given, try to recognize either an equality or a declared relation with arguments c1 ... cn, diff --git a/doc/preamble.tex b/doc/preamble.tex index f849ac381..2cd21f022 100644 --- a/doc/preamble.tex +++ b/doc/preamble.tex @@ -1,4 +1,4 @@ -\documentclass[12pt]{article} +\documentclass[11pt]{article} \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{ocamlweb} diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 113cb9d3f..fa939d0aa 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -16,6 +16,9 @@ open Libnames open Pattern open Nametab +(************************************************************************) +(* Generic functions to find Coq objects *) + let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let gen_reference locstr dir s = @@ -58,6 +61,24 @@ let gen_constant_in_modules locstr dirs s = " in module"^(if List.length dirs > 1 then "s " else " ")) ++ prlist_with_sep pr_coma pr_dirpath dirs) + +(* For tactics/commands requiring vernacular libraries *) + +let check_required_library d = + let d' = List.map id_of_string d in + let dir = make_dirpath (List.rev d') in + if not (Library.library_is_loaded dir) then +(* Loading silently ... + let m, prefix = list_sep_last d' in + read_library + (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) +*) +(* or failing ...*) + error ("Library "^(list_last d)^" has to be required first") + +(************************************************************************) +(* Specific Coq objects *) + let init_reference dir s=gen_reference "Coqlib" ("Init"::dir) s let init_constant dir s=gen_constant "Coqlib" ("Init"::dir) s diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 6741e1a0a..64c83d7eb 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -31,6 +31,9 @@ val arith_modules : string list list val zarith_base_modules : string list list val init_modules : string list list +(* For tactics/commands requiring vernacular libraries *) +val check_required_library : string list -> unit + (*s Global references *) (* Modules *) diff --git a/library/library.ml b/library/library.ml index 388580eab..fee383233 100644 --- a/library/library.ml +++ b/library/library.ml @@ -25,9 +25,9 @@ open Declaremods type logical_path = dir_path -let load_path = ref ([],[] : System.physical_path list * logical_path list) +let load_paths = ref ([],[] : System.physical_path list * logical_path list) -let get_load_path () = fst !load_path +let get_load_paths () = fst !load_paths (* Hints to partially detects if two paths refer to the same repertory *) let rec remove_path_dot p = @@ -60,17 +60,17 @@ let canonical_path_name p = let find_logical_path phys_dir = let phys_dir = canonical_path_name phys_dir in - match list_filter2 (fun p d -> p = phys_dir) !load_path with + match list_filter2 (fun p d -> p = phys_dir) !load_paths with | _,[dir] -> dir | _,[] -> Nameops.default_root_prefix | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) -let remove_path dir = - load_path := list_filter2 (fun p d -> p <> dir) !load_path +let remove_load_path dir = + load_paths := list_filter2 (fun p d -> p <> dir) !load_paths -let add_load_path_entry (phys_path,coq_path) = +let add_load_path (phys_path,coq_path) = let phys_path = canonical_path_name phys_path in - match list_filter2 (fun p d -> p = phys_path) !load_path with + match list_filter2 (fun p d -> p = phys_path) !load_paths with | _,[dir] -> if coq_path <> dir (* If this is not the default -I . to coqtop *) @@ -85,19 +85,19 @@ let add_load_path_entry (phys_path,coq_path) = ^(string_of_dirpath dir) ^("\nIt is remapped to "^(string_of_dirpath coq_path))); flush_all ()); - remove_path phys_path; - load_path := (phys_path::fst !load_path, coq_path::snd !load_path) + remove_load_path phys_path; + load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) end | _,[] -> - load_path := (phys_path :: fst !load_path, coq_path :: snd !load_path) + load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) | _ -> anomaly ("Two logical paths are associated to "^phys_path) let physical_paths (dp,lp) = dp -let load_path_of_logical_path dir = - fst (list_filter2 (fun p d -> d = dir) !load_path) +let load_paths_of_dir_path dir = + fst (list_filter2 (fun p d -> d = dir) !load_paths) -let get_full_load_path () = List.combine (fst !load_path) (snd !load_path) +let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths) (************************************************************************) (*s Modules on disk contain the following informations (after the magic @@ -124,7 +124,7 @@ type library_t = { library_imports : compilation_unit_name list; library_digest : Digest.t } -module CompilingLibraryOrdered = +module LibraryOrdered = struct type t = dir_path let compare d1 d2 = @@ -132,12 +132,12 @@ module CompilingLibraryOrdered = (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) end -module CompilingLibraryMap = Map.Make(CompilingLibraryOrdered) +module LibraryMap = Map.Make(LibraryOrdered) -(* This is a map from names to libraries *) -let libraries_table = ref CompilingLibraryMap.empty +(* This is a map from names to loaded libraries *) +let libraries_table = ref LibraryMap.empty -(* These are the _ordered_ lists of loaded, imported and exported libraries *) +(* These are the _ordered_ sets of loaded, imported and exported libraries *) let libraries_loaded_list = ref [] let libraries_imports_list = ref [] let libraries_exports_list = ref [] @@ -155,7 +155,7 @@ let unfreeze (mt,mo,mi,me) = libraries_exports_list := me let init () = - libraries_table := CompilingLibraryMap.empty; + libraries_table := LibraryMap.empty; libraries_loaded_list := []; libraries_imports_list := []; libraries_exports_list := [] @@ -168,18 +168,32 @@ let _ = Summary.survive_module = false; Summary.survive_section = false } -let find_library s = - CompilingLibraryMap.find s !libraries_table +(* cache for libraries loaded in memory but not necessarily in environment *) +let compunit_cache = ref LibraryMap.empty -let try_find_library s = - try find_library s +let _ = + Summary.declare_summary "MODULES-CACHE" + { Summary.freeze_function = (fun () -> !compunit_cache); + Summary.unfreeze_function = (fun cu -> compunit_cache := cu); + Summary.init_function = + (fun () -> compunit_cache := LibraryMap.empty); + Summary.survive_module = true; + Summary.survive_section = true } + +(* various requests to the tables *) + +let find_library dir = + LibraryMap.find dir !libraries_table + +let try_find_library dir = + try find_library dir with Not_found -> - error ("Unknown library " ^ (string_of_dirpath s)) + error ("Unknown library " ^ (string_of_dirpath dir)) -let library_full_filename m = (find_library m).library_filename +let library_full_filename dir = (find_library dir).library_filename let library_is_loaded dir = - try let _ = CompilingLibraryMap.find dir !libraries_table in true + try let _ = LibraryMap.find dir !libraries_table in true with Not_found -> false let library_is_opened dir = @@ -203,7 +217,7 @@ let register_loaded_library m = | m'::_ as l when m'.library_name = m.library_name -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; - libraries_table := CompilingLibraryMap.add m.library_name m !libraries_table + libraries_table := LibraryMap.add m.library_name m !libraries_table (* ... while if a library is imported/exported several time, then only the last occurrence is really needed - though the imported @@ -225,10 +239,8 @@ let register_open_library export m = (************************************************************************) (*s Opening libraries *) -(*s [open_library s] opens a library. The library [s] and all - libraries needed by [s] are assumed to be already loaded. When - opening [s] we recursively open all the libraries needed by [s] - and tagged [exported]. *) +(* [open_library export explicit m] opens library [m] if not already + opened _or_ if explicitly asked to be (re)opened *) let eq_lib_name m1 m2 = m1.library_name = m2.library_name @@ -246,6 +258,9 @@ let open_library export explicit_libs m = 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 + a library that is re-exported many times *) + let open_libraries export modl = let to_open_list = List.fold_left @@ -288,6 +303,8 @@ let (in_import, out_import) = (************************************************************************) +(*s Low-level interning/externing of libraries to files *) + (*s Loading from disk to cache (preparation phase) *) let vo_magic_number7 = 07992 (* V8.0 final old syntax *) @@ -314,23 +331,16 @@ let raw_intern_library a = let raw_extern_library = if !Options.v7 then raw_extern_library7 else raw_extern_library8 -(* cache for loaded libraries *) -let compunit_cache = ref CompilingLibraryMap.empty - -let _ = - Summary.declare_summary "MODULES-CACHE" - { Summary.freeze_function = (fun () -> !compunit_cache); - Summary.unfreeze_function = (fun cu -> compunit_cache := cu); - Summary.init_function = - (fun () -> compunit_cache := CompilingLibraryMap.empty); - Summary.survive_module = true; - Summary.survive_section = true } +let with_magic_number_check f a = + try f a + with System.Bad_magic_number fname -> + errorlabstrm "with_magic_number_check" + (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ + spc () ++ str"It is corrupted" ++ spc () ++ + str"or was compiled with another version of Coq.") -(*s [load_library s] loads the library [s] from the disk, and [find_library s] - returns the library of name [s], loading it if necessary. - The boolean [doexp] specifies if we open the libraries which are declared - exported in the dependencies (it is [true] at the highest level; - then same value as for caller is reused in recursive loadings). *) +(************************************************************************) +(*s Locate absolute or partially qualified library names in the path *) exception LibUnmappedDir exception LibNotFound @@ -339,7 +349,7 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = load_path_of_logical_path pref in + let loadpath = load_paths_of_dir_path pref in if loadpath = [] then raise LibUnmappedDir; try let name = (string_of_id base)^".vo" in @@ -352,13 +362,29 @@ let locate_absolute_library dir = with Not_found -> raise LibNotFound -let with_magic_number_check f a = - try f a - with System.Bad_magic_number fname -> - errorlabstrm "with_magic_number_check" - (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ - spc () ++ str"It is corrupted" ++ spc () ++ - str"or was compiled with another version of Coq.") +let locate_qualified_library qid = + try + (* Search library in loadpath *) + let dir, base = repr_qualid qid in + let loadpath = + if repr_dirpath dir = [] then get_load_paths () + else + (* we assume dir is an absolute dirpath *) + load_paths_of_dir_path dir + in + if loadpath = [] then raise LibUnmappedDir; + let name = (string_of_id base)^".vo" in + let path, file = System.where_in_path loadpath name in + let dir = extend_dirpath (find_logical_path path) base in + (* Look if loaded *) + try + (LibLoaded, dir, library_full_filename dir) + with Not_found -> + (LibInPath, dir, file) + with Not_found -> raise LibNotFound + +(************************************************************************) +(* Internalise libraries *) let lighten_library m = if !Options.dont_load_proofs then lighten_library m else m @@ -382,11 +408,11 @@ let intern_from_file f = let rec intern_library (dir, f) = try (* Look if in the current logical environment *) - CompilingLibraryMap.find dir !libraries_table + LibraryMap.find dir !libraries_table with Not_found -> try (* Look if already loaded in cache and consequently its dependencies *) - CompilingLibraryMap.find dir !compunit_cache + LibraryMap.find dir !compunit_cache with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file f in @@ -398,12 +424,12 @@ let rec intern_library (dir, f) = intern_and_cache_library dir m and intern_and_cache_library dir m = - compunit_cache := CompilingLibraryMap.add dir m !compunit_cache; + compunit_cache := LibraryMap.add dir m !compunit_cache; try List.iter (intern_mandatory_library dir) m.library_deps; m with e -> - compunit_cache := CompilingLibraryMap.remove dir !compunit_cache; + compunit_cache := LibraryMap.remove dir !compunit_cache; raise e and intern_mandatory_library caller (dir,d) = @@ -443,7 +469,7 @@ let rec_intern_by_filename_only id f = check_library_short_name f m.library_name id; (* We check no other file containing same library is loaded *) try - let m' = CompilingLibraryMap.find m.library_name !libraries_table in + let m' = LibraryMap.find m.library_name !libraries_table in Options.if_verbose warning ((string_of_dirpath m.library_name)^" is already loaded from file "^ m'.library_filename); @@ -452,27 +478,6 @@ let rec_intern_by_filename_only id f = let m = intern_and_cache_library m.library_name m in m.library_name -let locate_qualified_library qid = - try - (* Search library in loadpath *) - let dir, base = repr_qualid qid in - let loadpath = - if repr_dirpath dir = [] then get_load_path () - else - (* we assume dir is an absolute dirpath *) - load_path_of_logical_path dir - in - if loadpath = [] then raise LibUnmappedDir; - let name = (string_of_id base)^".vo" in - let path, file = System.where_in_path loadpath name in - let dir = extend_dirpath (find_logical_path path) base in - (* Look if loaded *) - try - (LibLoaded, dir, library_full_filename dir) - with Not_found -> - (LibInPath, dir, file) - with Not_found -> raise LibNotFound - let rec_intern_qualified_library (loc,qid) = try let (_,dir,f) = locate_qualified_library qid in @@ -491,7 +496,7 @@ let rec_intern_qualified_library (loc,qid) = let rec_intern_library_from_file idopt f = (* A name is specified, we have to check it contains library id *) - let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in + let _, f = System.find_file_in_path (get_load_paths ()) (f^".vo") in rec_intern_by_filename_only idopt f (**********************************************************************) @@ -519,11 +524,11 @@ let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir)) let rec load_library dir = try (* Look if loaded in current env (and consequently its dependencies) *) - CompilingLibraryMap.find dir !libraries_table + LibraryMap.find dir !libraries_table with Not_found -> (* [dir] is an absolute name matching [f] which must be in loadpath *) let m = - try CompilingLibraryMap.find dir !compunit_cache + try LibraryMap.find dir !compunit_cache with Not_found -> anomaly ((string_of_dirpath dir)^" should be in cache") in @@ -556,57 +561,39 @@ let (in_require, out_require) = export_function = export_require; classify_function = (fun (_,o) -> Anticipate o) } +(* Require libraries, import them if [export <> None], mark them for export + if [export = Some true] *) + +(* read = require without opening *) + let xml_require = ref (fun d -> ()) let set_xml_require f = xml_require := f -let require_library spec qidl export = -(* - if sections_are_opened () && Options.verbose () then - warning ("Objets of "^(string_of_library modref)^ - " not surviving sections (e.g. Grammar \nand Hints)\n"^ - "will be removed at the end of the section"); -*) +let require_library qidl export = let modrefl = List.map rec_intern_qualified_library qidl in if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require (modrefl,None)); - List.iter - (fun dir -> - add_anonymous_leaf (in_import (dir, export))) - modrefl + option_iter (fun exp -> + List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) + export end else - add_anonymous_leaf (in_require (modrefl,Some export)); + add_anonymous_leaf (in_require (modrefl,export)); if !Options.xml_export then List.iter !xml_require modrefl; add_frozen_state () -let require_library_from_file spec idopt file export = +let require_library_from_file idopt file export = let modref = rec_intern_library_from_file idopt file in if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require ([modref],None)); - add_anonymous_leaf (in_import (modref, export)) + option_iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) + export end else - add_anonymous_leaf (in_require ([modref],Some export)); + add_anonymous_leaf (in_require ([modref],export)); if !Options.xml_export then !xml_require modref; add_frozen_state () - -(* read = require without opening *) - -let read_library qid = - let modref = rec_intern_qualified_library qid in - add_anonymous_leaf (in_require ([modref],None)); - if !Options.xml_export then !xml_require modref; - add_frozen_state () - -let read_library_from_file f = - let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in - let modref = rec_intern_by_filename_only None f in - add_anonymous_leaf (in_require ([modref],None)); - if !Options.xml_export then !xml_require modref; - add_frozen_state () - - (* called at end of section *) let reload_library modrefl = @@ -617,7 +604,7 @@ let reload_library modrefl = (* the function called by Vernacentries.vernac_import *) -let import_library export (loc,qid) = +let import_module export (loc,qid) = try match Nametab.locate_module qid with MPfile dir -> @@ -634,27 +621,30 @@ let import_library export (loc,qid) = str ((string_of_qualid qid)^" is not a module")) (************************************************************************) -(*s [save_library s] saves the library [m] to the disk. *) +(*s Initializing the compilation of a library. *) let start_library f = let _,longf = - System.find_file_in_path (get_load_path ()) (f^".v") in + System.find_file_in_path (get_load_paths ()) (f^".v") in let ldir0 = find_logical_path (Filename.dirname longf) in let id = id_of_string (Filename.basename f) in let ldir = extend_dirpath ldir0 id in Declaremods.start_library ldir; ldir,longf +(************************************************************************) +(*s [save_library dir] ends library [dir] and save it to the disk. *) + let current_deps () = List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list let current_reexports () = List.map (fun m -> m.library_name) !libraries_exports_list -let save_library_to s f = - let cenv, seg = Declaremods.end_library s in +let save_library_to dir f = + let cenv, seg = Declaremods.end_library dir in let md = { - md_name = s; + md_name = dir; md_compiled = cenv; md_objects = seg; md_deps = current_deps (); @@ -668,33 +658,7 @@ let save_library_to s f = close_out ch with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e) -(*s Pretty-printing of libraries state. *) - -(* this function is not used... *) -let fmt_libraries_state () = - let opened = opened_libraries () - and loaded = loaded_libraries () in - (str "Imported (open) Modules: " ++ - prlist_with_sep pr_spc pr_dirpath opened ++ fnl () ++ - str "Loaded Modules: " ++ - prlist_with_sep pr_spc pr_dirpath loaded ++ fnl ()) - - -(*s For tactics/commands requiring vernacular libraries *) - -let check_required_library d = - let d' = List.map id_of_string d in - let dir = make_dirpath (List.rev d') in - if not (library_is_loaded dir) then -(* Loading silently ... - let m, prefix = list_sep_last d' in - read_library - (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) -*) -(* or failing ...*) - error ("Library "^(list_last d)^" has to be required first") - - +(************************************************************************) (*s Display the memory use of a library. *) open Printf diff --git a/library/library.mli b/library/library.mli index 02f01967c..4ecc76809 100644 --- a/library/library.mli +++ b/library/library.mli @@ -15,65 +15,58 @@ open Libnames open Libobject (*i*) -(*s This module is the heart of the library. It provides low level - functions to load, open and save libraries. Libraries 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]. *) +(*s This module provides functions to load, open and save + libraries. Libraries correspond to the subclass of modules that + coincide with a file on disk (the ".vo" files). Libraries on the + disk comes with checksums (obtained with the [Digest] module), which + are checked at loading time to prevent inconsistencies between files + written at various dates. +*) + +(*s Require = load in the environment + open (if the optional boolean + is not [None]); mark also for export if the boolean is [Some true] *) +val require_library : qualid located list -> bool option -> unit +val require_library_from_file : + identifier option -> System.physical_path -> bool option -> unit -val read_library : qualid located -> unit +(*s Open a module (or a library); if the boolean is true then it's also + an export otherwise just a simple import *) +val import_module : bool -> qualid located -> unit -val read_library_from_file : System.physical_path -> unit +(*s Start the compilation of a library *) +val start_library : string -> dir_path * string -(* [import_library true qid] = [export qid] *) - -val import_library : bool -> qualid located -> unit +(*s End the compilation of a library and save it to a ".vo" file *) +val save_library_to : dir_path -> string -> unit +(*s Interrogate the status of libraries *) + + (* - Tell if a library is loaded or opened *) val library_is_loaded : dir_path -> bool val library_is_opened : dir_path -> bool + (* - Tell which libraries are loaded or imported *) val loaded_libraries : unit -> dir_path list val opened_libraries : unit -> dir_path list -val fmt_libraries_state : unit -> Pp.std_ppcmds - -(*s Require. The command [require_library spec m file export] loads and opens - a library [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 library must be - exported. *) - -val require_library : - bool option -> qualid located list -> bool -> unit - -val require_library_from_file : - bool option -> identifier option -> System.physical_path -> bool -> unit - -val set_xml_require : (dir_path -> unit) -> unit - -(*s [save_library_to s f] saves the current environment as a library [s] - in the file [f]. *) - -val start_library : string -> dir_path * string -val save_library_to : dir_path -> string -> unit - -(* [library_full_filename] returns the full filename of a loaded library. *) - + (* - Return the full filename of a loaded library. *) val library_full_filename : dir_path -> string +(*s Hook for the xml exportation of libraries *) +val set_xml_require : (dir_path -> unit) -> unit -(*s Global load path *) -type logical_path = dir_path +(*s Global load paths: a load path is a physical path in the file + system; to each load path is associated a Coq [dir_path] (the "logical" + path of the physical path) *) -val get_load_path : unit -> System.physical_path list -val get_full_load_path : unit -> (System.physical_path * logical_path) list -val add_load_path_entry : System.physical_path * logical_path -> unit -val remove_path : System.physical_path -> unit -val find_logical_path : System.physical_path -> logical_path -val load_path_of_logical_path : dir_path -> System.physical_path list +val get_load_paths : unit -> System.physical_path list +val get_full_load_paths : unit -> (System.physical_path * dir_path) list +val add_load_path : System.physical_path * dir_path -> unit +val remove_load_path : System.physical_path -> unit +val find_logical_path : System.physical_path -> dir_path +val load_paths_of_dir_path : dir_path -> System.physical_path list +(*s Locate a library in the load paths *) exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath @@ -81,13 +74,10 @@ type library_location = LibLoaded | LibInPath val locate_qualified_library : qualid -> library_location * dir_path * System.physical_path - -val check_required_library : string list -> unit - -(*s Displays the memory use of a library. *) +(*s Statistics: display the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds -(* For discharge *) +(*s For discharge *) type library_reference val out_require : Libobject.obj -> library_reference diff --git a/library/states.ml b/library/states.ml index 0fa62265a..2a34c8753 100644 --- a/library/states.ml +++ b/library/states.ml @@ -24,7 +24,7 @@ let state_magic_number = 19764 let (extern_state,intern_state) = let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in (fun s -> raw_extern s (get_state())), - (fun s -> set_state (raw_intern (Library.get_load_path ()) s)) + (fun s -> set_state (raw_intern (Library.get_load_paths ()) s)) (* Rollback. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 77c7e9793..cc3740501 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -91,12 +91,13 @@ let load_vernacular () = let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj let load_vernac_obj () = - List.iter Library.read_library_from_file (List.rev !load_vernacular_obj) + List.iter (fun f -> Library.require_library_from_file None f None) + (List.rev !load_vernacular_obj) let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list let require () = - List.iter (fun s -> Library.require_library_from_file None None s false) + List.iter (fun s -> Library.require_library_from_file None s (Some false)) (List.rev !require_list) let compile_list = ref ([] : (bool * string) list) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 8562038c5..4449137e8 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -137,7 +137,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = if exists_dir dir then begin add_ml_dir dir; - Library.add_load_path_entry (dir,coq_dirpath) + Library.add_load_path (dir,coq_dirpath) end else msg_warning [< str ("Cannot open " ^ dir) >] @@ -160,7 +160,7 @@ let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = let dirs = map_succeed convert_dirs dirs in begin List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs; - List.iter Library.add_load_path_entry dirs + List.iter Library.add_load_path dirs end else msg_warning [< str ("Cannot open " ^ dir) >] diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 3cc2ba4f8..6cdbfaf20 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -57,7 +57,7 @@ let real_error = function the file we parse seems a bit risky to me. B.B. *) let open_file_twice_if verbosely fname = - let _,longfname = find_file_in_path (Library.get_load_path ()) fname in + let _,longfname = find_file_in_path (Library.get_load_paths ()) fname in let in_chan = open_in longfname in let verb_ch = if verbosely then Some (open_in longfname) else None in let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in @@ -174,7 +174,7 @@ let rec vernac_com interpfun (loc,com) = (* coqdoc state *) let cds = Constrintern.coqdoc_freeze() in if !Options.translate_file then begin - let _,f = find_file_in_path (Library.get_load_path ()) + let _,f = find_file_in_path (Library.get_load_paths ()) (make_suffix fname ".v") in chan_translate := open_out (f^"8"); Pp.comments := [] diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 764009039..0389dae68 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -143,7 +143,7 @@ let print_path_entry (s,l) = (str s ++ str " " ++ tbrk (0,2) ++ str (string_of_dirpath l)) let print_loadpath () = - let l = Library.get_full_load_path () in + let l = Library.get_full_load_paths () in msgnl (Pp.t (str "Physical path: " ++ tab () ++ str "Logical Path:" ++ fnl () ++ prlist_with_sep pr_fnl print_path_entry l)) @@ -192,8 +192,7 @@ let dump_universes s = let locate_file f = try - let _,file = - System.where_in_path (Library.get_load_path()) f in + let _,file = System.where_in_path (Library.get_load_paths ()) f in msgnl (str file) with Not_found -> msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++ @@ -326,12 +325,9 @@ let vernac_scheme = build_scheme (* Modules *) let vernac_import export refl = - let import_one ref = - let qid = qualid_of_reference ref in - Library.import_library export qid - in - List.iter import_one refl; - Lib.add_frozen_state () + let import ref = Library.import_module export (qualid_of_reference ref) in + List.iter import refl; + Lib.add_frozen_state () (* else let import (loc,qid) = @@ -508,9 +504,7 @@ let test_renamed_module (_,qid) = let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in try - match import with - | None -> List.iter Library.read_library qidl - | Some b -> Library.require_library None qidl b + Library.require_library qidl import with e -> (* Compatibility message *) let qidl' = List.filter is_obsolete_module qidl in @@ -590,10 +584,7 @@ let vernac_set_end_tac tac = (* Auxiliary file management *) let vernac_require_from export spec filename = - match export with - Some exp -> - Library.require_library_from_file spec None filename exp - | None -> Library.read_library_from_file filename + Library.require_library_from_file None filename export let vernac_add_loadpath isrec pdir ldiropt = let alias = match ldiropt with @@ -601,7 +592,7 @@ let vernac_add_loadpath isrec pdir ldiropt = | Some ldir -> ldir in (if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias -let vernac_remove_loadpath = Library.remove_path +let vernac_remove_loadpath = Library.remove_load_path (* Coq syntax for ML or system commands *) @@ -1076,81 +1067,6 @@ let vernac_check_guard () = let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) - -(**************************) -(* Not supported commands *) -(*** -let _ = - add "ResetSection" - (function - | [VARG_IDENTIFIER id] -> - (fun () -> reset_section (string_of_id id)) - | _ -> bad_vernac_args "ResetSection") - -(* Modules *) - -let _ = - vinterp_add "BeginModule" - (function - | [VARG_IDENTIFIER id] -> - let s = string_of_id id in - let lpe,_ = System.find_file_in_path (Library.get_load_path ()) (s^".v") in - let dir = extend_dirpath (Library.find_logical_path lpe) id in - fun () -> - Lib.start_module dir - | _ -> bad_vernac_args "BeginModule") - -let _ = - vinterp_add "WriteModule" - (function - | [VARG_IDENTIFIER id] -> - let mid = Lib.end_module id in - fun () -> let m = string_of_id id in Library.save_module_to mid m - | [VARG_IDENTIFIER id; VARG_STRING f] -> - let mid = Lib.end_module id in - fun () -> Library.save_module_to mid f - | _ -> bad_vernac_args "WriteModule") - -let _ = - vinterp_add "CLASS" - (function - | [VARG_STRING kind; VARG_QUALID qid] -> - let stre = - if kind = "LOCAL" then - make_strength_0() - else - Nametab.NeverDischarge - in - fun () -> - let ref = Nametab.global (dummy_loc, qid) in - Class.try_add_new_class ref stre; - if_verbose message - ((string_of_qualid qid) ^ " is now a class") - | _ -> bad_vernac_args "CLASS") - -(* Meta-syntax commands *) -let _ = - add "TOKEN" - (function - | [VARG_STRING s] -> (fun () -> Metasyntax.add_token_obj s) - | _ -> bad_vernac_args "TOKEN") -***) - -(* Search commands *) - -(*** -let _ = - add "Searchisos" - (function - | [VARG_CONSTR com] -> - (fun () -> - let env = Global.env() in - let c = constr_of_com Evd.empty env com in - let cc = nf_betaiota env Evd.empty c in - Searchisos.type_search cc) - | _ -> bad_vernac_args "Searchisos") -***) - let interp c = match c with (* Control (done in vernac) *) | (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false |