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 --- library/doc.tex | 11 +++++++++ library/libobject.ml | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++ library/libobject.mli | 37 ++++++++++++++++++++++++++++++ library/summary.ml | 48 +++++++++++++++++++++++++++++++++++++++ library/summary.mli | 25 ++++++++++++++++++++ 5 files changed, 184 insertions(+) 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 (limited to 'library') 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