portage Astterm (partiellement)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@159 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 66 insertions, 4 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 909895612e..5d7d624121 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -135,12 +135,48 @@ let declare_mind mie =
   push_inductive_names sp mie;
   declare_inductive_implicits sp
 
+(* Syntax constants. *)
+
+let syntax_table = ref (Idmap.empty : constr Idmap.t)
+
+let _ = Summary.declare_summary
+	  "SYNTAXCONSTANT"
+	  { Summary.freeze_function = (fun () -> !syntax_table);
+	    Summary.unfreeze_function = (fun ft -> syntax_table := ft);
+	    Summary.init_function = (fun () -> syntax_table := Idmap.empty) }
+
+let add_syntax_constant id c =
+  syntax_table := Idmap.add id c !syntax_table
+
+let cache_syntax_constant (sp,c) = 
+  add_syntax_constant (basename sp) c;
+  Nametab.push (basename sp) sp
+
+let open_syntax_constant (sp,_) =
+  Nametab.push (basename sp) sp
+
+let (in_syntax_constant, out_syntax_constant) =
+  let od = {
+    cache_function = cache_syntax_constant;
+    load_function = (fun _ -> ());
+    open_function = open_syntax_constant;
+    specification_function = (fun x -> x) } in
+  declare_object ("SYNTAXCONSTANT", od)
+
+let declare_syntax_constant id c =
+  let sp = add_leaf id CCI (in_syntax_constant c) in
+  add_syntax_constant id c;
+  Nametab.push (basename sp) sp
+
+let out_syntax_constant id = Idmap.find id !syntax_table
+
 (* Test and access functions. *)
 
 let is_constant sp = failwith "TODO"
 let constant_strength sp = failwith "TODO"
 
 let is_variable id = failwith "TODO"
+let out_variable sp = failwith "TODO"
 let variable_strength id = failwith "TODO"
 
 (* Global references. *)
@@ -181,6 +217,17 @@ let global_reference kind id =
   let ids = ids_of_sign hyps in
   DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
 
+let global_reference_imps kind id =
+  let c = global_reference kind id in
+  match c with
+    | DOPN (Const sp,_) -> 
+	c, list_of_implicits (constant_implicits sp)
+    | DOPN (MutInd (sp,i),_) -> 
+	c, list_of_implicits (inductive_implicits (sp,i))
+    | DOPN (MutConstruct ((sp,i),j),_) ->
+	c, list_of_implicits (constructor_implicits ((sp,i),j))
+    | _ -> assert false
+
 let is_global id =
   try 
     let osp = Nametab.sp_of_id CCI id in
diff --git a/library/declare.mli b/library/declare.mli
index 1b3b842cfb..c32ce46ac8 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -30,6 +30,8 @@ val declare_mind : mutual_inductive_entry -> unit
 
 val declare_eliminations : section_path -> unit
 
+val declare_syntax_constant : identifier -> constr -> unit
+
 
 (*s Corresponding test and access functions. *)
 
@@ -37,8 +39,11 @@ val is_constant : section_path -> bool
 val constant_strength : section_path -> strength
 
 val is_variable : identifier -> bool
+val out_variable : section_path -> identifier * typed_type * strength
 val variable_strength : identifier -> strength
 
+val out_syntax_constant : identifier -> constr
+
 (*s It also provides a function [global_reference] to construct a global
   constr (a constant, an inductive or a constructor) from an identifier.
   To do so, it first looks for the section path using [Nametab.sp_of_id] and
@@ -47,6 +52,7 @@ val variable_strength : identifier -> strength
 
 val global_operator : section_path -> identifier -> sorts oper * var_context
 val global_reference : path_kind -> identifier -> constr
+val global_reference_imps : path_kind -> identifier -> constr * int list
 
 val is_global : identifier -> bool
 
diff --git a/library/lib.ml b/library/lib.ml
index 07d4049ce7..46a2833f57 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -26,6 +26,8 @@ type library_entry = section_path * node
 
 let lib_stk = ref ([] : (section_path * node) list)
 
+let lib_tab = Hashtbl.create 353
+
 let module_name = ref None
 let path_prefix = ref ([] : string list)
 
@@ -69,7 +71,8 @@ let split_lib sp =
 (* Adding operations. *)
 
 let add_entry sp node =
-  lib_stk := (sp,node) :: !lib_stk
+  lib_stk := (sp,node) :: !lib_stk;
+  Hashtbl.add lib_tab sp node
 
 let anonymous_id = 
   let n = ref 0 in
@@ -77,7 +80,8 @@ let anonymous_id =
 
 let add_anonymous_entry node =
   let sp = make_path (anonymous_id()) OBJ in
-  add_entry sp node
+  add_entry sp node;
+  sp
 
 let add_leaf id kind obj =
   let sp = make_path id kind in
@@ -88,12 +92,16 @@ let add_anonymous_leaf obj =
   add_anonymous_entry (Leaf obj)
 
 let add_frozen_state () =
-  add_anonymous_entry (FrozenState (freeze_summaries()))
+  let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()
 
 let contents_after = function
   | None -> !lib_stk
   | Some sp -> let (after,_,_) = split_lib sp in after
 
+let map_leaf sp = 
+  match Hashtbl.find lib_tab sp with
+    | Leaf obj -> obj
+    | _ -> anomaly "Lib.map_leaf: not a leaf"
 
 (* Sections. *)
 
diff --git a/library/lib.mli b/library/lib.mli
index d8b3def299..d87c4573a8 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -26,10 +26,11 @@ type library_entry = section_path * node
   recent ones coming first). *)
 
 val add_leaf : identifier -> path_kind -> obj -> section_path
-val add_anonymous_leaf : obj -> unit
+val add_anonymous_leaf : obj -> section_path
 
 val contents_after : section_path option -> library_segment
 
+val map_leaf : section_path -> obj
 
 (*s Opening and closing a section. *)