new cicEnvironment implementation

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.mli

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index c3ca6ef952f191c6c1c4fb9783b43557733ed143..9875f52acff94296b47b39cbeb0b0e2e292ef9f3 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -23,47 +23,45 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*****************************************************************************)
-(*                                                                           *)
-(*                              PROJECT HELM                                 *)
-(*                                                                           *)
-(*               Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                24/01/2000                                 *)
-(*                                                                           *)
-(* This module implements a trival cache system (an hash-table) for cic      *)
-(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml)        *)
-(*                                                                           *)
-(*****************************************************************************)
+(****************************************************************************)
+(*                                                                          *)
+(*                              PROJECT HELM                                *)
+(*                                                                          *)
+(*               Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>              *)
+(*                                24/01/2000                                *)
+(*                                                                          *)
+(* This module implements a trival cache system (an hash-table) for cic     *)
+(*                          ^^^^^^                                          *)
+(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml)       *)
+(*                                                                          *)
+(****************************************************************************)
 
 exception CircularDependency of string;;
 exception Term_not_found of UriManager.uri;;
 
-(* get_obj uri                                                               *)
-(* returns the cic object whose uri is uri. If the term is not just in cache,*)
-(* then it is parsed via CicParser.term_of_xml from the file whose name is   *)
-(* the result of Getter.get uri                                              *)
-(*                                                                           *)
-(* ~not_jet_cooked returns the object even if it is not in the               *)
-(* CacheOfCookedObjects searching it in the frozen list.                     *)
-(* This is necessary in cicUnivUtils.ml since (in the univ_maker phase       *)
-(* it has to traverse object before they are committed.                      *)
-(* see the .ml file for some reassuring invariants on this.                  *)
+(* as the get cooked, but if not present the object is only fetched,
+ * not unfreezed and committed 
+ *)
 val get_obj : 
-  ?not_jet_cooked:bool -> UriManager.uri -> CicUniv.universe_graph -> 
-  Cic.obj * CicUniv.universe_graph
+  CicUniv.universe_graph -> UriManager.uri ->   
+    Cic.obj * CicUniv.universe_graph
 
 type type_checked_obj =
    CheckedObj of (Cic.obj * CicUniv.universe_graph)    (* cooked obj *)
  | UncheckedObj of Cic.obj  (* uncooked obj *)
 
-(* is_type_checked uri cookingsno                                   *)
-(*CSC commento falso ed obsoleto *)
-(* returns (true,object) if the object has been type-checked        *)
-(* otherwise it returns (false,object) and freeze the object for    *)
-(* type-checking                                                    *)
-(* set_type_checking_info must be called to unfreeze the object     *)
+(*
+ * I think this should be the real semantic:
+ * 
+ * val is_type_checked: 
+ *  ?trust:bool -> UriManager.uri -> bool
+ *
+ *  but the old semantic is similar to get_cooked_obj, but 
+ *  returns an unchecked object intead of a Not_found
+ *)
 val is_type_checked : 
-  ?trust:bool -> UriManager.uri -> CicUniv.universe_graph -> type_checked_obj
+  ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->  
+    type_checked_obj
 
 (* set_type_checking_info uri                                         *)
 (* must be called once the type-checking of uri is finished           *)
@@ -94,8 +92,8 @@ val remove_term: UriManager.uri -> unit
 (* trusted (if [trust] = true and the trusting function accepts it) *)
 (* Otherwise it raises Not_found                                    *)
 val get_cooked_obj : 
-  ?trust:bool -> UriManager.uri ->
-   CicUniv.universe_graph -> Cic.obj * CicUniv.universe_graph
+  ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->
+    Cic.obj * CicUniv.universe_graph
 
 (* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
 
@@ -118,5 +116,6 @@ val empty : unit -> unit
 val set_trust: (UriManager.uri -> bool) -> unit
 
 (* for filtering in tacticChaser *)
-(* NEW *)
 val in_cache : UriManager.uri -> bool
+
+(* EOF *)