From 05074a8ee576e155596cf0c8bb3c8372a4dfa086 Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 3 Sep 1999 09:53:11 +0000 Subject: modules Libobject et Summary (partiel) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@36 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 10 +++++++- Makefile | 12 ++++++---- kernel/doc.tex | 2 +- kernel/univ.mli | 5 ++++ lib/util.ml | 2 ++ lib/util.mli | 2 ++ library/doc.tex | 11 +++++++++ library/libobject.ml | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++ library/libobject.mli | 37 ++++++++++++++++++++++++++++++ library/summary.ml | 48 +++++++++++++++++++++++++++++++++++++++ library/summary.mli | 25 ++++++++++++++++++++ 11 files changed, 211 insertions(+), 6 deletions(-) create mode 100644 library/doc.tex create mode 100644 library/libobject.ml create mode 100644 library/libobject.mli create mode 100644 library/summary.ml create mode 100644 library/summary.mli diff --git a/.depend b/.depend index 080e11881..b674b479a 100644 --- a/.depend +++ b/.depend @@ -24,10 +24,12 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi \ kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi -kernel/univ.cmi: kernel/names.cmi +kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/coqast.cmi: lib/dyn.cmi lib/pp.cmi: lib/pp_control.cmi lib/util.cmi: lib/pp.cmi +library/libobject.cmi: kernel/names.cmi +library/summary.cmi: kernel/names.cmi config/coq_config.cmo: config/coq_config.cmi config/coq_config.cmx: config/coq_config.cmi kernel/abstraction.cmo: kernel/generic.cmi kernel/names.cmi kernel/sosub.cmi \ @@ -134,3 +136,9 @@ lib/pp_control.cmo: lib/pp_control.cmi lib/pp_control.cmx: lib/pp_control.cmi lib/util.cmo: lib/pp.cmi lib/util.cmi lib/util.cmx: lib/pp.cmx lib/util.cmi +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/summary.cmo: kernel/names.cmi library/summary.cmi +library/summary.cmx: kernel/names.cmx library/summary.cmi diff --git a/Makefile b/Makefile index 775cdc3c7..e062d3997 100644 --- a/Makefile +++ b/Makefile @@ -16,7 +16,7 @@ OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF) OCAMLDEP=ocamldep DEPFLAGS=$(INCLUDES) -INCLUDES=-I config -I lib -I kernel +INCLUDES=-I config -I lib -I kernel -I library # Objects files @@ -33,18 +33,22 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \ kernel/typing.cmo -OBJS=$(CONFIG) $(LIB) $(KERNEL) +LIBRARY=library/libobject.cmo library/summary.cmo + +OBJS=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) # Targets world: $(OBJS) - $(OCAMLC) -o coqtop.byte $(OBJS) + #$(OCAMLC) -o coqtop.byte $(OBJS) + ocamlmktop -o coqtop $(OBJS) # Literate programming (with ocamlweb) LPLIB = lib/doc.tex $(LIB:.cmo=.mli) LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli) -LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) +LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli) +LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) lp: doc/coq.ps doc/coq.ps: doc/coq.tex cd doc; make coq.ps diff --git a/kernel/doc.tex b/kernel/doc.tex index 78f1a267d..56debc102 100644 --- a/kernel/doc.tex +++ b/kernel/doc.tex @@ -1,7 +1,7 @@ \section*{The Coq kernel} -\ocwsection +\ocwsection \label{kernel} This section describes the \Coq\ kernel, which is a type checker for the \CCI. The modules of the kernel are organized as follows. diff --git a/kernel/univ.mli b/kernel/univ.mli index b262ad718..2104fa721 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -17,6 +17,8 @@ val prop_univ_univ_univ : universe val new_univ : section_path -> universe +(*s Graphs of universes. *) + type universes val initial_universes : universes @@ -34,3 +36,6 @@ val enforce_gt : constraint_function val enforce_geq : constraint_function val enforce_eq : constraint_function +(* pretty-printing. *) + +val pr_universes : universes -> Pp.std_ppcmds diff --git a/lib/util.ml b/lib/util.ml index 95a609378..698341097 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -61,6 +61,8 @@ let parse_section_path s = let id,k = decoupe_kind n in dirs,id,k +module Stringmap = Map.Make(struct type t = string let compare = compare end) + (* Lists *) let list_intersect l1 l2 = diff --git a/lib/util.mli b/lib/util.mli index 9517d8742..2d764d499 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -23,6 +23,8 @@ val implode : string list -> string val parse_section_path : string -> string list * string * string +module Stringmap : Map.S with type key = string + (*s Lists. *) val list_intersect : 'a list -> 'a list -> 'a list diff --git a/library/doc.tex b/library/doc.tex new file mode 100644 index 000000000..fd1a8bbf9 --- /dev/null +++ b/library/doc.tex @@ -0,0 +1,11 @@ + +\section*{The Coq library} + +\ocwsection \label{library} +This section 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; + \item a global environment for the CCI, with functions to export and + import compiled modules. +\end{itemize} diff --git a/library/libobject.ml b/library/libobject.ml new file mode 100644 index 000000000..f5e610704 --- /dev/null +++ b/library/libobject.ml @@ -0,0 +1,63 @@ + +(* $Id$ *) + +open Util +open Names + +type 'a object_declaration = { + load_function : 'a -> unit; + cache_function : section_path * '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_specification_function : obj -> obj } + +let object_tag lobj = Dyn.tag lobj + +let cache_tab = + (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) + +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) = + 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 spec_extractor lobj = + infun(odecl.specification_function (outfun lobj)) + in + Hashtbl.add cache_tab na { dyn_load_function = loader; + dyn_cache_function = cacher; + dyn_specification_function = spec_extractor }; + (infun,outfun) + + +let load_object 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) + +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 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) diff --git a/library/libobject.mli b/library/libobject.mli new file mode 100644 index 000000000..967e4c410 --- /dev/null +++ b/library/libobject.mli @@ -0,0 +1,37 @@ + +(* $Id$ *) + +(*i*) +open Names +(*i*) + +(* [Libobject] declares persistent objects given with three methods: + - 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; + - 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; + specification_function : 'a -> 'a } + +(*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. *) + +type obj + +val declare_object : + (string * 'a object_declaration) -> ('a -> obj) * (obj -> 'a) + +val object_tag : obj -> string + +val load_object : obj -> unit + +val cache_object : (section_path * obj) -> unit + +val extract_object_specification : obj -> obj diff --git a/library/summary.ml b/library/summary.ml new file mode 100644 index 000000000..f58917202 --- /dev/null +++ b/library/summary.ml @@ -0,0 +1,48 @@ + +(* $Id$ *) + +open Pp +open Util +open Names + +type 'a summary_declaration = { + freeze_function : unit -> 'a; + unfreeze_function : 'a -> unit; + init_function : unit -> unit } + +let summaries = + (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t) + +let declare_summary sumname sdecl = + let (infun,outfun) = Dyn.create (sumname^"-SUMMARY") in + let dyn_freeze () = infun (sdecl.freeze_function()) + and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) + and dyn_init = sdecl.init_function in + let ddecl = { + freeze_function = dyn_freeze; + unfreeze_function = dyn_unfreeze; + init_function = dyn_init} + in + if Hashtbl.mem summaries sumname then + anomalylabstrm "Summary.declare_summary" + [< 'sTR "Cannot declare a summary twice: " ; 'sTR sumname >]; + Hashtbl.add summaries sumname ddecl + +type frozen_summaries = Dyn.t Stringmap.t + +let freeze_summaries () = + let m = ref Stringmap.empty in + Hashtbl.iter + (fun id decl -> m := Stringmap.add id (decl.freeze_function()) !m) + summaries; + !m + +let unfreeze_summaries fs = + Hashtbl.iter + (fun id decl -> + try decl.unfreeze_function (Stringmap.find id fs) + with Not_found -> decl.init_function()) + summaries + +let init_summaries () = + Hashtbl.iter (fun _ decl -> decl.init_function()) summaries diff --git a/library/summary.mli b/library/summary.mli new file mode 100644 index 000000000..faa887f37 --- /dev/null +++ b/library/summary.mli @@ -0,0 +1,25 @@ + +(* $Id$ *) + +(*i*) +open Names +(*i*) + +(* This module registers the declaration of global tables, which will be kept + in synchronization during the various backtracks of the system. *) + +type 'a summary_declaration = { + freeze_function : unit -> 'a; + unfreeze_function : 'a -> unit; + init_function : unit -> unit } + +val declare_summary : string -> 'a summary_declaration -> unit + +type frozen_summaries + +val freeze_summaries : unit -> frozen_summaries +val unfreeze_summaries : frozen_summaries -> unit +val init_summaries : unit -> unit + + + -- cgit v1.2.3