From 76e3b2928b766a76ee7e29dd3f6867cd48f95a52 Mon Sep 17 00:00:00 2001 From: filliatr Date: Sun, 19 Sep 1999 14:17:35 +0000 Subject: - un effort sur la doc (ocamlweb) - module Nametab - module Impargs - correction bug : Parameter id : t => vérification que t est bien un type MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/doc.tex | 9 ++++-- library/global.ml | 2 ++ library/global.mli | 3 ++ library/impargs.ml | 87 +++++++++++++++++++++++++++++++++++++++++++++++++++ library/impargs.mli | 26 +++++++++++++++ library/lib.ml | 2 +- library/libobject.mli | 19 ++++++----- library/library.ml | 7 +++-- library/nametab.ml | 44 ++++++++++++++++++++++++++ library/nametab.mli | 17 ++++++++++ 10 files changed, 200 insertions(+), 16 deletions(-) create mode 100644 library/impargs.ml create mode 100644 library/impargs.mli create mode 100755 library/nametab.ml create mode 100755 library/nametab.mli (limited to 'library') diff --git a/library/doc.tex b/library/doc.tex index fd1a8bbf9..33af59336 100644 --- a/library/doc.tex +++ b/library/doc.tex @@ -1,11 +1,16 @@ +\newpage \section*{The Coq library} \ocwsection \label{library} -This section describes the \Coq\ library, which is made of two parts: +This chapter describes the \Coq\ library, which is made of two parts: \begin{itemize} \item a general mechanism to keep a trace of all operations and of - the state of the system, with backtrack possibilities; + the state of the system, with backtrack capabilities; \item a global environment for the CCI, with functions to export and import compiled modules. \end{itemize} +The modules of the library are organized as follows. + +\bigskip +\begin{center}\epsfig{file=library.dep.ps}\end{center} diff --git a/library/global.ml b/library/global.ml index d7267a96d..7ffbd2110 100644 --- a/library/global.ml +++ b/library/global.ml @@ -9,6 +9,8 @@ open Summary let global_env = ref empty_environment +let env () = !global_env + let _ = declare_summary "Global environment" { freeze_function = (fun () -> !global_env); diff --git a/library/global.mli b/library/global.mli index d21509e32..9436e446b 100644 --- a/library/global.mli +++ b/library/global.mli @@ -10,12 +10,15 @@ open Evd open Constant open Inductive open Environ +open Typing (*i*) (* This module defines the global environment of Coq. The functions below are the exactly the same as the ones in [Typing], operating on that global environment. *) +val env : unit -> unit environment + val evar_map : unit -> unit evar_map val universes : unit -> universes val metamap : unit -> (int * constr) list diff --git a/library/impargs.ml b/library/impargs.ml new file mode 100644 index 000000000..95b322e4e --- /dev/null +++ b/library/impargs.ml @@ -0,0 +1,87 @@ + +(* $Id$ *) + +open Names +open Generic +open Term +open Reduction +open Constant +open Inductive +open Typing + +type implicits = + | Impl_auto of int list + | Impl_manual of int list + | No_impl + +let implicit_args = ref false + +let auto_implicits ty = + if !implicit_args then + let genv = unsafe_env_of_env (Global.env()) in + Impl_auto (poly_args genv ty) + else + No_impl + +(* Constants. *) + +let constants_table = ref Spmap.empty + +let declare_constant_implicits sp = + let cb = Global.lookup_constant sp in + let imps = auto_implicits cb.const_type.body in + constants_table := Spmap.add sp imps !constants_table + +let declare_constant_manual_implicits sp imps = + constants_table := Spmap.add sp (Impl_manual imps) !constants_table + +let constant_implicits sp = + Spmap.find sp !constants_table + +(* 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 + implicit arguments of the constructors. *) + +let inductives_table = ref Spmap.empty + +let declare_inductive_implicits sp = + let mib = Global.lookup_mind sp in + let imps_one_inductive mip = + (auto_implicits mip.mind_arity.body, + let (_,lc) = decomp_all_DLAMV_name mip.mind_lc in + Array.map auto_implicits lc) + in + let imps = Array.map imps_one_inductive mib.mind_packets in + inductives_table := Spmap.add sp imps !inductives_table + +let inductive_implicits (sp,i) = + let imps = Spmap.find sp !inductives_table in + fst imps.(i) + +let constructor_implicits ((sp,i),j) = + let imps = Spmap.find sp !inductives_table in + (snd imps.(i)).(pred j) + +(* Registration as global tables and roolback. *) + +type frozen = implicits Spmap.t + +let init () = + constants_table := Spmap.empty + +let freeze () = + !constants_table + +let unfreeze ct = + constants_table := ct + +let _ = + Summary.declare_summary "names" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init } + +let rollback f x = + let fs = freeze () in + try f x with e -> begin unfreeze fs; raise e end diff --git a/library/impargs.mli b/library/impargs.mli new file mode 100644 index 000000000..84ea98da3 --- /dev/null +++ b/library/impargs.mli @@ -0,0 +1,26 @@ + +(* $Id$ *) + +(*i*) +open Names +(*i*) + +(* Implicit arguments. Here we store the implicit arguments. Notice that we + are outside the kernel, which knows nothing about implicit arguments. *) + +type implicits = + | Impl_auto of int list + | Impl_manual of int list + | No_impl + +val implicit_args : bool ref + +val declare_constant_implicits : section_path -> unit +val declare_constant_manual_implicits : section_path -> int list -> unit +val constant_implicits : section_path -> implicits + +val declare_inductive_implicits : section_path -> unit +val inductive_implicits : section_path * int -> implicits +val constructor_implicits : (section_path * int) * int -> implicits + + diff --git a/library/lib.ml b/library/lib.ml index 42850bc05..9c434fdf1 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -126,7 +126,7 @@ let close_section s = in let (after,_,before) = split_lib sp in lib_stk := before; - add_entry sp (ClosedSection (s,modp,List.rev after)); + add_entry sp (ClosedSection (s,modp,after)); add_frozen_state (); pop_path_prefix () diff --git a/library/libobject.mli b/library/libobject.mli index 7ddac57b2..ff076ee39 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -6,14 +6,14 @@ open Names (*i*) (* [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; - - 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) *) + 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; + 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 = { cache_function : section_path * 'a -> unit; @@ -21,8 +21,7 @@ type 'a object_declaration = { open_function : 'a -> unit; specification_function : 'a -> 'a } -(*s Given the object-name, the "loading" function, the "caching" function, - and the "specification" function, the function [declare_object] +(*s Given an object name and a declaration, the function [declare_object] will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects. *) diff --git a/library/library.ml b/library/library.ml index 7de5a845d..0bd0b895c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -76,9 +76,8 @@ let open_module s = 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 load_objects decls = + segment_iter load_object decls let rec load_module_from doexp s f = let (fname,ch) = raw_intern_module f in @@ -95,6 +94,8 @@ let rec load_module_from doexp s f = 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; + Global.import m.module_compiled_env; + load_objects m.module_declarations; Hashtbl.add modules_table s m; m diff --git a/library/nametab.ml b/library/nametab.ml new file mode 100755 index 000000000..b84eda23a --- /dev/null +++ b/library/nametab.ml @@ -0,0 +1,44 @@ + +(* $Id$ *) + +open Names + +let cci_tab = ref Idmap.empty +let fw_tab = ref Idmap.empty + +let fw_sp_of_id id = + Idmap.find id !fw_tab + +let sp_of_id kind id = + match kind with + | FW -> Idmap.find id !fw_tab + | CCI -> Idmap.find id !cci_tab + | OBJ -> invalid_arg "Nametab.sp_of_id" + +let push id sp = + match kind_of_path sp with + | FW -> fw_tab := Idmap.add id sp !fw_tab + | CCI -> cci_tab := Idmap.add id sp !cci_tab + | OBJ -> invalid_arg "Nametab.push" + +(* Registration as a global table and roolback. *) + +let init () = + cci_tab := Idmap.empty; + cci_tab := Idmap.empty + +type frozen = section_path Idmap.t * section_path Idmap.t + +let freeze () = (!cci_tab, !fw_tab) + +let unfreeze (cci,fw) = cci_tab := cci; fw_tab := fw + +let _ = + Summary.declare_summary "names" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init } + +let rollback f x = + let fs = freeze () in + try f x with e -> begin unfreeze fs; raise e end diff --git a/library/nametab.mli b/library/nametab.mli new file mode 100755 index 000000000..2d0cd62eb --- /dev/null +++ b/library/nametab.mli @@ -0,0 +1,17 @@ + +(* $Id$ *) + +(*i*) +open Names +(*i*) + +(* This module contains the table for globalization, which associates global + names (section paths) to identifiers. *) + +val push : identifier -> section_path -> unit + +val sp_of_id : path_kind -> identifier -> section_path +val fw_sp_of_id : identifier -> section_path + +val rollback : ('a -> 'b) -> 'a -> 'b + -- cgit v1.2.3