From f3d068d8bd33a511397576533b1190be9b544a07 Mon Sep 17 00:00:00 2001 From: filliatr Date: Sun, 19 Sep 1999 18:01:50 +0000 Subject: module Declare git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@77 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 133 ++++++++++++++++++++++++++++++++++++++++++++++++++ library/declare.mli | 25 ++++++++++ library/lib.ml | 4 +- library/lib.mli | 2 +- library/libobject.ml | 24 ++++----- library/libobject.mli | 10 ++-- library/library.ml | 2 +- 7 files changed, 179 insertions(+), 21 deletions(-) create mode 100644 library/declare.ml create mode 100644 library/declare.mli (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml new file mode 100644 index 000000000..1af5ad6a8 --- /dev/null +++ b/library/declare.ml @@ -0,0 +1,133 @@ + +(* $Id$ *) + +open Util +open Names +open Inductive +open Libobject +open Lib +open Impargs + +(* Variables. *) + +let cache_variable (_,obj) = + Global.push_var obj + +let load_variable _ = + anomaly "we shouldn't load a variable" + +let open_variable _ = + anomaly "we shouldn't open a variable" + +let specification_variable _ = + anomaly "we shouldn't extract the specification of a variable" + +let (in_variable, out_variable) = + let od = { + cache_function = cache_variable; + load_function = load_variable; + open_function = open_variable; + specification_function = specification_variable } in + declare_object ("Variable", od) + +let declare_variable id c = + let obj = (id,c) in + Global.push_var obj; + let _ = add_leaf id CCI (in_variable obj) in + () + +(* Parameters. *) + +let cache_parameter (sp,c) = + Global.add_parameter sp c; + Nametab.push (basename sp) sp + +let load_parameter _ = () + +let open_parameter (sp,_) = + Nametab.push (basename sp) sp + +let specification_parameter obj = obj + +let (in_parameter, out_parameter) = + let od = { + cache_function = cache_parameter; + load_function = load_parameter; + open_function = open_parameter; + specification_function = specification_parameter } in + declare_object ("Parameter", od) + +let declare_parameter id c = + let sp = add_leaf id CCI (in_parameter c) in + Global.add_parameter sp c; + Nametab.push (basename sp) sp + +(* Constants. *) + +let cache_constant (sp,ce) = + Global.add_constant sp ce; + Nametab.push (basename sp) sp; + declare_constant_implicits sp + +let load_constant _ = () + +let open_constant (sp,_) = + Nametab.push (basename sp) sp; + declare_constant_implicits sp + +let specification_constant obj = obj + +let (in_constant, out_constant) = + let od = { + cache_function = cache_constant; + load_function = load_constant; + open_function = open_constant; + specification_function = specification_constant } in + declare_object ("Parameter", od) + +let declare_constant id ce = + let sp = add_leaf id CCI (in_constant ce) in + Global.add_constant sp ce; + Nametab.push (basename sp) sp; + declare_constant_implicits sp + +(* Inductives. *) + +let push_inductive_names sp mie = + List.iter + (fun (id,_,cnames,_) -> + Nametab.push id sp; + List.iter (fun x -> Nametab.push x sp) cnames) + mie.mind_entry_inds + +let cache_inductive (sp,mie) = + Global.add_mind sp mie; + push_inductive_names sp mie; + declare_inductive_implicits sp + +let load_inductive _ = () + +let open_inductive (sp,mie) = + push_inductive_names sp mie; + declare_inductive_implicits sp + +let specification_inductive obj = obj + +let (in_inductive, out_inductive) = + let od = { + cache_function = cache_inductive; + load_function = load_inductive; + open_function = open_inductive; + specification_function = specification_inductive } in + declare_object ("Parameter", od) + +let declare_mind mie = + let id = match mie.mind_entry_inds with + | (id,_,_,_)::_ -> id + | [] -> anomaly "cannot declare an empty list of inductives" + in + let sp = add_leaf id CCI (in_inductive mie) in + Global.add_mind sp mie; + push_inductive_names sp mie; + declare_inductive_implicits sp + diff --git a/library/declare.mli b/library/declare.mli new file mode 100644 index 000000000..21486c250 --- /dev/null +++ b/library/declare.mli @@ -0,0 +1,25 @@ + +(* $Id$ *) + +(*i*) +open Names +open Term +open Constant +open Inductive +(*i*) + +(* This module provides the official functions to declare new variables, + parameters, constants and inductive types. Using the following functions + will add the entries in the global environment (module [Global]), will + register the declarations in the library (module [Lib]) --- so that the + reset works properly --- and will fill some global tables as [Nametab] and + [Impargs]. *) + +val declare_variable : identifier -> constr -> unit + +val declare_parameter : identifier -> constr -> unit + +val declare_constant : identifier -> constant_entry -> unit + +val declare_mind : mutual_inductive_entry -> unit + diff --git a/library/lib.ml b/library/lib.ml index 9c434fdf1..254134710 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -80,8 +80,8 @@ let add_anonymous_entry node = let sp = make_path (anonymous_id()) OBJ in add_entry sp node -let add_leaf id obj = - let sp = make_path id OBJ in +let add_leaf id kind obj = + let sp = make_path id kind in add_entry sp (Leaf obj); sp diff --git a/library/lib.mli b/library/lib.mli index a38fb4cef..92c2937b4 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -27,7 +27,7 @@ type library_entry = section_path * node (*s Adding operations, and getting the current list of operations (most recent ones coming first). *) -val add_leaf : identifier -> obj -> section_path +val add_leaf : identifier -> path_kind -> obj -> section_path val add_anonymous_leaf : obj -> unit val contents_after : section_path option -> library_segment diff --git a/library/libobject.ml b/library/libobject.ml index 1096ac43a..31fb81c57 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,16 +6,16 @@ open Names type 'a object_declaration = { cache_function : section_path * 'a -> unit; - load_function : 'a -> unit; - open_function : 'a -> unit; + load_function : section_path * 'a -> unit; + open_function : section_path * 'a -> unit; specification_function : 'a -> 'a } type obj = Dyn.t (* persistent dynamic objects *) type dynamic_object_declaration = { dyn_cache_function : section_path * obj -> unit; - dyn_load_function : obj -> unit; - dyn_open_function : obj -> unit; + dyn_load_function : section_path * obj -> unit; + dyn_open_function : section_path * obj -> unit; dyn_specification_function : obj -> obj } let object_tag lobj = Dyn.tag lobj @@ -28,11 +28,11 @@ let declare_object (na,odecl) = let 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 loader lobj = - if Dyn.tag lobj = na then odecl.load_function (outfun lobj) + and loader (spopt,lobj) = + if Dyn.tag lobj = na then odecl.load_function (spopt,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the loadfun" - and opener lobj = - if Dyn.tag lobj = na then odecl.open_function (outfun lobj) + and opener (spopt,lobj) = + if Dyn.tag lobj = na then odecl.open_function (spopt,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the openfun" and spec_extractor lobj = infun(odecl.specification_function (outfun lobj)) @@ -53,11 +53,11 @@ let apply_dyn_fun f lobj = let cache_object ((_,lobj) as node) = apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj -let load_object lobj = - apply_dyn_fun (fun d -> d.dyn_load_function lobj) lobj +let load_object ((_,lobj) as node) = + apply_dyn_fun (fun d -> d.dyn_load_function node) lobj -let open_object lobj = - apply_dyn_fun (fun d -> d.dyn_open_function lobj) lobj +let open_object ((_,lobj) as node) = + apply_dyn_fun (fun d -> d.dyn_open_function node) lobj let extract_object_specification lobj = apply_dyn_fun (fun d -> d.dyn_specification_function lobj) lobj diff --git a/library/libobject.mli b/library/libobject.mli index ff076ee39..d855059fa 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -17,8 +17,8 @@ open Names type 'a object_declaration = { cache_function : section_path * 'a -> unit; - load_function : 'a -> unit; - open_function : 'a -> unit; + load_function : section_path * 'a -> unit; + open_function : section_path * 'a -> unit; specification_function : 'a -> 'a } (*s Given an object name and a declaration, the function [declare_object] @@ -32,7 +32,7 @@ val declare_object : val object_tag : obj -> string -val cache_object : (section_path * obj) -> unit -val load_object : obj -> unit -val open_object : obj -> unit +val cache_object : section_path * obj -> unit +val load_object : section_path * obj -> unit +val open_object : section_path * obj -> unit val extract_object_specification : obj -> obj diff --git a/library/library.ml b/library/library.ml index 0bd0b895c..b48d7cfee 100644 --- a/library/library.ml +++ b/library/library.ml @@ -50,7 +50,7 @@ let (raw_extern_module, raw_intern_module) = let segment_iter f = let rec apply = function - | _,Leaf obj -> f obj + | sp,Leaf obj -> f (sp,obj) | _,ClosedSection (_,_,mseg) -> iter mseg | _,OpenedSection _ -> assert false | _,FrozenState _ -> () -- cgit v1.2.3