diff options
| -rw-r--r-- | .depend | 24 | ||||
| -rw-r--r-- | Makefile | 10 | ||||
| -rw-r--r-- | dev/TODO | 11 | ||||
| -rw-r--r-- | kernel/closure.mli | 22 | ||||
| -rw-r--r-- | kernel/constant.mli | 12 | ||||
| -rw-r--r-- | kernel/doc.tex | 8 | ||||
| -rw-r--r-- | kernel/generic.mli | 48 | ||||
| -rw-r--r-- | kernel/inductive.mli | 7 | ||||
| -rw-r--r-- | kernel/names.ml | 1 | ||||
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | kernel/sign.mli | 8 | ||||
| -rw-r--r-- | kernel/term.mli | 22 | ||||
| -rw-r--r-- | kernel/typing.ml | 15 | ||||
| -rw-r--r-- | kernel/typing.mli | 7 | ||||
| -rw-r--r-- | lib/doc.tex | 5 | ||||
| -rw-r--r-- | lib/hashcons.ml | 98 | ||||
| -rw-r--r-- | lib/hashcons.mli | 2 | ||||
| -rw-r--r-- | library/doc.tex | 9 | ||||
| -rw-r--r-- | library/global.ml | 2 | ||||
| -rw-r--r-- | library/global.mli | 3 | ||||
| -rw-r--r-- | library/impargs.ml | 87 | ||||
| -rw-r--r-- | library/impargs.mli | 26 | ||||
| -rw-r--r-- | library/lib.ml | 2 | ||||
| -rw-r--r-- | library/libobject.mli | 19 | ||||
| -rw-r--r-- | library/library.ml | 7 | ||||
| -rwxr-xr-x | library/nametab.ml | 44 | ||||
| -rwxr-xr-x | library/nametab.mli | 17 | ||||
| -rw-r--r-- | toplevel/himsg.mli | 2 |
28 files changed, 346 insertions, 173 deletions
@@ -30,9 +30,11 @@ lib/pp.cmi: lib/pp_control.cmi lib/util.cmi: lib/pp.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 + kernel/typing.cmi kernel/univ.cmi +library/impargs.cmi: kernel/names.cmi library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi library/libobject.cmi: kernel/names.cmi +library/nametab.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 @@ -153,6 +155,14 @@ lib/util.cmo: lib/pp.cmi lib/util.cmi lib/util.cmx: lib/pp.cmx lib/util.cmi library/global.cmo: library/summary.cmi kernel/typing.cmi library/global.cmi library/global.cmx: library/summary.cmx kernel/typing.cmx library/global.cmi +library/impargs.cmo: kernel/constant.cmi kernel/generic.cmi \ + library/global.cmi kernel/inductive.cmi kernel/names.cmi \ + kernel/reduction.cmi library/summary.cmi kernel/term.cmi \ + kernel/typing.cmi library/impargs.cmi +library/impargs.cmx: kernel/constant.cmx kernel/generic.cmx \ + library/global.cmx kernel/inductive.cmx kernel/names.cmx \ + kernel/reduction.cmx library/summary.cmx kernel/term.cmx \ + kernel/typing.cmx library/impargs.cmi library/lib.cmo: library/libobject.cmi kernel/names.cmi library/summary.cmi \ lib/util.cmi library/lib.cmi library/lib.cmx: library/libobject.cmx kernel/names.cmx library/summary.cmx \ @@ -161,10 +171,14 @@ 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/library.cmo: kernel/environ.cmi library/global.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/global.cmx library/lib.cmx \ + library/libobject.cmx kernel/names.cmx lib/system.cmx lib/util.cmx \ + library/library.cmi +library/nametab.cmo: kernel/names.cmi library/summary.cmi library/nametab.cmi +library/nametab.cmx: kernel/names.cmx library/summary.cmx library/nametab.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 \ @@ -42,7 +42,8 @@ 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/library.cmo + library/global.cmo library/states.cmo library/library.cmo \ + library/nametab.cmo library/impargs.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 \ @@ -95,8 +96,10 @@ LPTOPLEVEL = toplevel/doc.tex $(TOPLEVEL:.cmo=.mli) LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \ $(LPTOPLEVEL) -doc/coq.tex: $(LPFILES) - ocamlweb -o doc/coq.tex $(LPFILES) +doc/coq.tex: doc/preamble.tex $(LPFILES) + cat doc/preamble.tex > doc/coq.tex + ocamlweb --no-preamble $(LPFILES) >> doc/coq.tex + echo "\end{document}" >> doc/coq.tex # Emacs tags @@ -185,6 +188,7 @@ archclean:: cleanall:: archclean rm -f *~ + rm -f doc/*~ rm -f config/*.cm[io] config/*~ rm -f lib/*.cm[io] lib/*~ rm -f kernel/*.cm[io] kernel/*~ @@ -1,7 +1,16 @@ + o Lib + - écrire une fonction d'export qui supprimme les FrozenState, + vérifie qu'il n'y a pas de section ouvert, et présente les + déclarations dans l'ordre chronologique (y compris dans les + sections fermées). A utiliser dans Library pour sauver un module. + + o Convertibilité + - utiliser une exception plutôt qu'un type somme Convert. | Non Convert. + o Univers - définir un type d'ensemble de contraintes, et sauver cet ensemble - pour chaque module et non pas le graphe complet + pour chaque module et non pas le graphe complet o configure - il faut tester la version du programme correspondant à $bytecamlc diff --git a/kernel/closure.mli b/kernel/closure.mli index b64f2794b..62caafe55 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -10,12 +10,12 @@ open Evd open Environ (*i*) -(* flags for profiling... *) +(* Flags for profiling reductions. *) val stats : bool ref val share : bool ref -(* sets of reduction kinds *) +(*s The set of reduction kinds. *) type red_kind = BETA | DELTA of sorts oper | IOTA type reds = { @@ -31,16 +31,17 @@ val betadeltaiota_red : reds val red_set : reds -> red_kind -> bool -(* reduction function specification *) +(*s Reduction function specification. *) type red_mode = UNIFORM | SIMPL | WITHBACK type flags = red_mode * reds -(* (UNIFORM,r) == r-reduce in any context - * (SIMPL,r) == bdi-reduce under cases or fix, r otherwise (like hnf does) - * (WITHBACK,r) == internal use: means we are under a case - * or in rec. arg. of fix *) +(* [(UNIFORM,r)] == [r]-reduce in any context. + [(SIMPL,r)] == bdi-reduce under cases or fix, [r] otherwise + (like hnf does). + [(WITHBACK,r)] == internal use: means we are under a case + or in rec. arg. of fix. *) val flags_under : flags -> flags val red_top : flags -> red_kind -> bool @@ -54,7 +55,7 @@ val betadeltaiota : flags val hnf_flags : flags -(* Call by value functions *) +(*s Call by value functions *) type cbv_value = | VAL of int * constr | LAM of name * constr * constr * cbv_value subs @@ -96,11 +97,10 @@ val apply_stack : 'a cbv_infos -> constr -> stack -> constr val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr +(*s Lazy reduction. *) - - -(* Lazy reduction *) type 'a freeze + type 'a frterm = | FRel of int | FVAR of identifier diff --git a/kernel/constant.mli b/kernel/constant.mli index d8aeb7670..890e1f425 100644 --- a/kernel/constant.mli +++ b/kernel/constant.mli @@ -7,7 +7,7 @@ open Term open Sign (*i*) -(* Constants. *) +(* Constants (internal representation). *) type discharge_recipe @@ -15,10 +15,6 @@ type recipe = | Cooked of constr | Recipe of discharge_recipe -type constant_entry = { - const_entry_body : constr; - const_entry_type : constr option } - type constant_body = { const_kind : path_kind; const_body : recipe ref option; @@ -30,3 +26,9 @@ val is_defined : constant_body -> bool val is_opaque : constant_body -> bool +(*s Constant declaration. *) + +type constant_entry= { + const_entry_body : constr; + const_entry_type : constr option } + diff --git a/kernel/doc.tex b/kernel/doc.tex index 56debc102..4a9fc3550 100644 --- a/kernel/doc.tex +++ b/kernel/doc.tex @@ -1,9 +1,11 @@ +\newpage \section*{The Coq kernel} \ocwsection \label{kernel} -This section describes the \Coq\ kernel, which is a type checker for the \CCI. - +This chapter describes the \Coq\ kernel, which is a type checker for the \CCI. The modules of the kernel are organized as follows. -TODO +\bigskip +\begin{center}\epsfig{file=kernel.dep.ps,width=\linewidth}\end{center} + diff --git a/kernel/generic.mli b/kernel/generic.mli index dcd458f8b..b9eb9a512 100644 --- a/kernel/generic.mli +++ b/kernel/generic.mli @@ -6,13 +6,8 @@ open Util open Names (*i*) -(* A generic notion of terms with binders. *) - -exception FreeVar -exception Occur - -(* \label{generic_terms} - Generic terms, over any kind of operators. *) +(* \label{generic_terms} A generic notion of terms with binders, + over any kind of operators. *) type 'oper term = | DOP0 of 'oper (* atomic terms *) @@ -28,30 +23,42 @@ type 'oper term = val isRel : 'a term -> bool val isVAR : 'a term -> bool val free_rels : 'a term -> Intset.t + +exception FreeVar +exception Occur + val closedn : int -> 'a term -> unit val closed0 : 'a term -> bool val noccurn : int -> 'a term -> bool val noccur_bet : int -> int -> 'a term -> bool +(*s Lifts. [ELSHFT(l,n)] == lift of [n], then apply [lift l]. + [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *) -(* lifts *) type lift_spec = | ELID - | ELSHFT of lift_spec * int (* ELSHFT(l,n) == lift of n, then apply lift l *) - | ELLFT of int * lift_spec (* ELLFT(n,l) == apply l to de Bruijn > n *) - (* i.e under n binders *) + | ELSHFT of lift_spec * int + | ELLFT of int * lift_spec + val el_shft : int -> lift_spec -> lift_spec val el_lift : lift_spec -> lift_spec val el_liftn : int -> lift_spec -> lift_spec val reloc_rel: int -> lift_spec -> int +val exliftn : lift_spec -> 'a term -> 'a term +val liftn : int -> int -> 'a term -> 'a term +val lift : int -> 'a term -> 'a term +val pop : 'a term -> 'a term + +(*s Explicit substitutions of type ['a]. [ESID] = identity. + [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = + $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars. + [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *) -(* explicit substitutions of type 'a *) type 'a subs = - | ESID (* ESID = identity *) - | CONS of 'a * 'a subs (* CONS(t,S) = (S.t) parallel substitution *) - | SHIFT of int * 'a subs (* SHIFT(n,S)= (\^n o S) terms in S are relocated *) - (* with n vars *) - | LIFT of int * 'a subs (* LIFT(n,S)=(\%n S) stands for ((\^n o S).n...1) *) + | ESID + | CONS of 'a * 'a subs + | SHIFT of int * 'a subs + | LIFT of int * 'a subs val subs_cons : 'a * 'a subs -> 'a subs val subs_lift : 'a subs -> 'a subs @@ -62,10 +69,6 @@ val expand_rel : int -> 'a subs -> (int * 'a, int) union type info = Closed | Open | Unknown type 'a substituend = { mutable sinfo : info; sit : 'a } -val exliftn : lift_spec -> 'a term -> 'a term -val liftn : int -> int -> 'a term -> 'a term -val lift : int -> 'a term -> 'a term -val pop : 'a term -> 'a term val lift_substituend : int -> 'a term substituend -> 'a term val make_substituend : 'a term -> 'a term substituend val substn_many : 'a term substituend array -> int -> 'a term -> 'a term @@ -117,7 +120,8 @@ val rel_list : int -> int -> 'a term list val count_dlam : 'a term -> int -(* For hash-consing use *) +(*s For hash-consing. *) + val hash_term : ('a term -> 'a term) * (('a -> 'a) * (name -> name) * (identifier -> identifier)) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index a08136424..d0dee30b9 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -64,6 +64,9 @@ type mutual_inductive_entry = { mind_entry_finite : bool; mind_entry_inds : (identifier * constr * identifier list * constr) list } +(*s The different kinds of errors that may result of a malformed inductive + definition. *) + type inductive_error = | NonPos of int | NotEnoughArgs of int @@ -76,6 +79,9 @@ type inductive_error = exception InductiveError of inductive_error +(*s The following functions are utility functions to check and to + decompose a declaration. *) + (* [mind_check_names] checks the names of an inductive types declaration i.e. that all the types and constructors names are distinct. It raises an exception [InductiveError _] if it is not the case. *) @@ -92,5 +98,4 @@ val mind_extract_and_check_params : val mind_extract_params : int -> constr -> (name * constr) list * constr - val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit diff --git a/kernel/names.ml b/kernel/names.ml index 6e5835fbb..dc1350fa3 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -78,6 +78,7 @@ module IdOrdered = end module Idset = Set.Make(IdOrdered) +module Idmap = Map.Make(IdOrdered) (* Fresh names *) diff --git a/kernel/names.mli b/kernel/names.mli index c022a84a3..9a7822d11 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -24,6 +24,7 @@ val id_without_number : identifier -> bool val first_char : identifier -> string module Idset : Set.S with type elt = identifier +module Idmap : Map.S with type key = identifier val lift_ident : identifier -> identifier val next_ident_away_from : identifier -> identifier list -> identifier diff --git a/kernel/sign.mli b/kernel/sign.mli index 092e5c078..c67ab11d8 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -7,11 +7,9 @@ open Generic open Term (*i*) -(* Signatures (with named and de Bruijn variables). *) +(* Signatures of named variables. *) type 'a signature = identifier list * 'a list -type 'a db_signature = (name * 'a) list -type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature val nil_sign : 'a signature val add_sign : (identifier * 'a) -> 'a signature -> 'a signature @@ -53,6 +51,10 @@ val dunbindv : identifier -> 'a signature -> 'a -> 'b term val dbind : 'a signature -> 'b term -> 'a * 'b term val dbindv : 'a signature -> 'b term array -> 'a * 'b term +(*s Signatures with named and de Bruijn variables. *) + +type 'a db_signature = (name * 'a) list +type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature val gLOB : 'b signature -> ('b,'a) env diff --git a/kernel/term.mli b/kernel/term.mli index 7c1ee1d33..c36df1f65 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -7,25 +7,20 @@ open Generic (*i*) (*s The operators of the Calculus of Inductive Constructions. - ['a] is the type of sorts. *) + ['a] is the type of sorts. ([XTRA] is an extra slot, for putting in + whatever sort of operator we need for whatever sort of application.) *) type 'a oper = - (* DOP0 *) | Meta of int | Sort of 'a - (* DOP2 *) | Cast | Prod | Lambda - (* DOPN *) | AppL | Const of section_path | Abst of section_path | MutInd of section_path * int | MutConstruct of (section_path * int) * int | MutCase of case_info | Fix of int array * int | CoFix of int - | XTRA of string - (* an extra slot, for putting in whatever sort of - operator we need for whatever sort of application *) and case_info = (section_path * int) option @@ -45,7 +40,7 @@ val mk_Prop : sorts (*s The type [constr] of the terms of CCI is obtained by instanciating the generic terms (type [term], - see \citesec{generic_terms}) on the above operators, themselves instanciated + see \refsec{generic_terms}) on the above operators, themselves instanciated on the above sorts. *) type constr = sorts oper term @@ -295,12 +290,11 @@ val args_of_mconstr : constr -> constr array (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) val destCase : constr -> case_info * constr * constr * constr array -(* Destructs the ith function of the block - [Fixpoint f1 [ctx1] = b1 - with f2 [ctx2] = b2 - ... - with fn [ctxn] = bn.] - +(* Destructs the $i$th function of the block + $\mathit{Fixpoint} ~ f_1 ~ [ctx_1] = b_1 + \mathit{with} ~ f_2 ~ [ctx_2] = b_2 + \dots + \mathit{with} ~ f_n ~ [ctx_n] = b_n$, where the lenght of the $j$th context is $ij$. *) val destGralFix : diff --git a/kernel/typing.ml b/kernel/typing.ml index 1fcf340f3..4a029dfe3 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -304,18 +304,13 @@ let add_constant sp ce env = in add_constant sp cb env'' -let type_from_judgment env j = - match whd_betadeltaiota env j.uj_kind with - | DOP0(Sort s) -> { body = j.uj_type; typ = s } - | _ -> error_not_type CCI env j.uj_type (* shouldn't happen *) - -let add_parameter sp c env = - let (j,u) = safe_machine env c in +let add_parameter sp t env = + let (jt,u) = safe_machine env t in let env' = set_universes u env in let cb = { const_kind = kind_of_path sp; - const_body = Some (ref (Cooked c)); - const_type = type_from_judgment env' j; + const_body = None; + const_type = assumption_of_judgment env' jt; const_hyps = get_globals (context env); const_opaque = false } in @@ -424,6 +419,8 @@ let add_mind sp mie env = let export = export let import = import +let unsafe_env_of_env e = e + (*s Machines with information. *) type information = Logic | Inf of unsafe_judgment diff --git a/kernel/typing.mli b/kernel/typing.mli index 0167c8cd9..639772946 100644 --- a/kernel/typing.mli +++ b/kernel/typing.mli @@ -14,7 +14,10 @@ open Environ open Typeops (*i*) -(*s Safe environments. *) +(*s Safe environments. Since we are now able to type terms, we can define an + abstract type of safe environments, where objects are typed before being + added. Internally, the datatype is still [unsafe_env]. We re-export the + functions of [Environ] for the new type [environment]. *) type 'a environment @@ -44,6 +47,8 @@ val lookup_meta : int -> 'a environment -> constr val export : 'a environment -> string -> compiled_env val import : compiled_env -> 'a environment -> 'a environment +val unsafe_env_of_env : 'a environment -> 'a unsafe_env + (*s Typing without information. *) type judgment diff --git a/lib/doc.tex b/lib/doc.tex index 224da620a..35bd15fa1 100644 --- a/lib/doc.tex +++ b/lib/doc.tex @@ -1,4 +1,7 @@ +\newpage \section*{Utility libraries} - +\ocwsection \label{lib} +This chapter describes the various utility libraries used in the code +of \Coq. diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 301643dba..55405a7aa 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -1,45 +1,7 @@ -(****************************************************************************) -(* The Calculus of Inductive Constructions *) -(* *) -(* Projet Coq *) -(* *) -(* INRIA LRI-CNRS ENS-CNRS *) -(* Rocquencourt Orsay Lyon *) -(* *) -(* Coq V6.3 *) -(* July 1st 1999 *) -(* *) -(****************************************************************************) -(* hashcons.ml *) -(****************************************************************************) -(* Hash consing of datastructures *) -(* -open Pp;; -let acces = ref 0;; -let comparaison = ref 0;; -let succes = ref 0;; -let accesstr = ref 0;; -let comparaisonstr = ref 0;; -let successtr = ref 0;; -*)let stat() = ();; -(* - mSGNL [< 'sTR"acces="; 'iNT !acces; 'sPC; - 'sTR"comp="; 'iNT !comparaison; 'sPC; - 'sTR"succes="; 'iNT !succes; 'sPC >]; - comparaison:=0; - acces:=0; - succes:=0; - mSGNL [< 'sTR"String:"; 'sPC; - 'sTR"acces="; 'iNT !accesstr; 'sPC; - 'sTR"comp="; 'iNT !comparaisonstr; 'sPC; - 'sTR"succes="; 'iNT !successtr; 'sPC >]; - comparaisonstr:=0; - accesstr:=0; - successtr:=0 -;; -*) +(* $Id$ *) +(* Hash consing of datastructures *) (* The generic hash-consing functions (does not use Obj) *) @@ -54,6 +16,7 @@ let successtr = ref 0;; * * Note that this module type coerces to the argument of Hashtbl.Make. *) + module type Comp = sig type t @@ -72,6 +35,7 @@ module type Comp = * argument the sub-hcons functions (the tables are created at that moment), * and returns the hcons function for t. *) + module type S = sig type t @@ -79,7 +43,6 @@ module type S = val f : unit -> (u -> t -> t) end - module Make(X:Comp) = struct type t = X.t @@ -109,7 +72,7 @@ module Make(X:Comp) = (* incr acces;*) try let r = Htbl.find tab y in(* incr succes;*) r with Not_found -> Htbl.add tab y y; y) - end;; + end (* A few usefull wrappers: * takes as argument the function f above and build a function of type @@ -117,7 +80,7 @@ module Make(X:Comp) = * sub-hcons functions. *) (* For non-recursive types it is quite easy. *) -let simple_hcons h u = h () u;; +let simple_hcons h u = h () u (* For a recursive type T, we write the module of sig Comp with u equals * to (T -> T) * u0 @@ -128,8 +91,7 @@ let simple_hcons h u = h () u;; let recursive_hcons h u = let hc = h () in let rec hrec x = hc (hrec,u) x in - hrec -;; + hrec (* If the structure may contain loops, use this one. *) let recursive_loop_hcons h u = @@ -137,8 +99,8 @@ let recursive_loop_hcons h u = let rec hrec visited x = if List.memq x visited then x else hc (hrec (x::visited),u) x - in hrec [] -;; + in + hrec [] (* For 2 mutually recursive types *) let recursive2_hcons h1 h2 u1 u2 = @@ -147,14 +109,10 @@ let recursive2_hcons h1 h2 u1 u2 = let rec hrec1 x = hc1 (hrec1,hrec2,u1) x and hrec2 x = hc2 (hrec1,hrec2,u2) x in (hrec1,hrec2) -;; - - - (* A set of global hashcons functions *) -let hashcons_resets = ref [];; -let init() = List.iter (fun f -> f()) !hashcons_resets;; +let hashcons_resets = ref [] +let init() = List.iter (fun f -> f()) !hashcons_resets (* [register_hcons h u] registers the hcons function h, result of the above * wrappers. It returns another hcons function that always uses the same @@ -163,11 +121,8 @@ let init() = List.iter (fun f -> f()) !hashcons_resets;; let register_hcons h u = let hf = ref (h u) in let reset() = hf := h u in - hashcons_resets := reset :: !hashcons_resets; - (fun x -> !hf x) -;; - - + hashcons_resets := reset :: !hashcons_resets; + (fun x -> !hf x) (* Basic hashcons modules for string and obj. Integers do not need be hashconsed. *) @@ -181,14 +136,14 @@ module Hstring = Make( let equal s1 s2 =(* incr comparaisonstr; if*) s1=s2(* then (incr successtr; true) else false*) let hash = Hashtbl.hash - end);; + end) (* Obj.t *) -exception NotEq;; +exception NotEq (* From CAMLLIB/caml/mlvalues.h *) -let no_scan_tag = 251;; -let tuple_p obj = Obj.is_block obj & (Obj.tag obj < no_scan_tag);; +let no_scan_tag = 251 +let tuple_p obj = Obj.is_block obj & (Obj.tag obj < no_scan_tag) let comp_obj o1 o2 = if tuple_p o1 & tuple_p o2 then @@ -201,7 +156,6 @@ let comp_obj o1 o2 = with NotEq -> false else false else o1=o2 -;; let hash_obj hrec o = begin @@ -212,7 +166,6 @@ let hash_obj hrec o = done end; o -;; module Hobj = Make( struct @@ -221,24 +174,19 @@ module Hobj = Make( let hash_sub (hrec,_) = hash_obj hrec let equal = comp_obj let hash = Hashtbl.hash - end);; - - + end) (* Hashconsing functions for string and obj. Always use the same * global tables. The latter can be reinitialized with init() *) (* string : string -> string *) (* obj : Obj.t -> Obj.t *) -let string = register_hcons (simple_hcons Hstring.f) ();; -let obj = register_hcons (recursive_hcons Hobj.f) ();; +let string = register_hcons (simple_hcons Hstring.f) () +let obj = register_hcons (recursive_hcons Hobj.f) () (* The unsafe polymorphic hashconsing function *) -let magic_hash (c: 'a) = +let magic_hash (c : 'a) = init(); let r = obj (Obj.repr c) in - init(); - (Obj.magic r : 'a) -;; - -(* $Id$ *) + init(); + (Obj.magic r : 'a) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 917c063e1..9665e1a86 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -3,8 +3,6 @@ (* Generic hash-consing. *) -val stat : unit->unit - module type Comp = sig type t 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 + diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 5c5548c2a..ff3eac8ee 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -21,7 +21,7 @@ end (*s The result is a module which provides a function [explain_type_error] to explain a type error for a given kind in a given context, which are usually the three arguments carried by the exception [TypeError] - (see \citesec{typeerrors}). *) + (see \refsec{typeerrors}). *) module Make (P : Printer) : sig |