From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 25 Jan 2005 09:28:50 +0000 (+0000)
Subject: added list_obj and list_uri
X-Git-Tag: V_0_1_0~90
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=de36c6322dde3866f3da822f1795cc518233c79f;p=helm.git

added list_obj and list_uri
---

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 461c3edc6..5c1daa137 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -99,6 +99,7 @@ module Cache :
    val is_in_frozen: UriManager.uri -> bool
    val is_in_unchecked: UriManager.uri -> bool
    val is_in_cooked: UriManager.uri -> bool
+   val list_all_cooked_uris: unit -> UriManager.uri list
   end 
 =
   struct
@@ -458,6 +459,10 @@ module Cache :
        HT.remove cacheOfCookedObjects uri 
    ;;
    
+   let  list_all_cooked_uris () =
+     HT.fold (fun u _ l -> u::l) cacheOfCookedObjects []
+   ;;
+   
   end
 ;;
 
@@ -675,4 +680,19 @@ let in_library uri =
   with Http_getter_types.Key_not_found _ -> false)
 
 let remove_term = Cache.remove
+  
+let list_uri () = 
+  Cache.list_all_cooked_uris ()
+;;
 
+let list_obj () =
+  try 
+    List.map (fun u -> 
+      let o,ug = get_obj CicUniv.empty_ugraph u in
+        (u,o,ug)) 
+    (list_uri ())
+  with
+    Not_found -> 
+      prerr_endline "Who has removed the uri in the meanwhile?";
+      raise Not_found
+;;
diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index 77f97ed96..5c10c81a3 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -120,6 +120,10 @@ val set_trust: (UriManager.uri -> bool) -> unit
   * otherwise (i.e. objects already parsed from XML) *)
 val in_cache : UriManager.uri -> bool
 
+(* to debug the matitac batch compiler *)
+val list_obj: unit -> (UriManager.uri * Cic.obj * CicUniv.universe_graph) list
+val list_uri: unit -> UriManager.uri list
+
   (** @return true for objects available in the library *)
 val in_library: UriManager.uri -> bool