X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.mli;h=55566a614493de9ae8b872a0a9347d2cf6a37073;hb=af364f229a858464cc557e60e314b6ffb20b6625;hp=9875f52acff94296b47b39cbeb0b0e2e292ef9f3;hpb=218c0062f93dd3221b0266cfbc26fd9cf787ad18;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index 9875f52ac..55566a614 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -36,8 +36,8 @@
 (*                                                                          *)
 (****************************************************************************)
 
-exception CircularDependency of string;;
-exception Term_not_found of UriManager.uri;;
+exception CircularDependency of string Lazy.t;;
+exception Object_not_found of UriManager.uri;;
 
 (* as the get cooked, but if not present the object is only fetched,
  * not unfreezed and committed 
@@ -75,17 +75,23 @@ val is_type_checked :
 (* we find in the library, we have to calculate it and then inject it *)
 (* in the cacke. This is an orrible backdoor used by univ_maker.      *)
 (* see the .ml file for some reassuring invariants                    *)
+(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
 val set_type_checking_info : 
-  ?replace_ugraph:(CicUniv.universe_graph option) -> UriManager.uri -> unit
-
-(* We need this in the Qed. *)
-val add_type_checked_term : 
-  UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
-
-  (** remove a type checked term
-  * @raise Term_not_found when given term is not in the environment
+  ?replace_ugraph_and_univlist:
+    ((CicUniv.universe_graph * CicUniv.universe list) option) -> 
+    UriManager.uri -> unit
+
+(* this function is called by CicTypeChecker.typecheck_obj to add to the *)
+(* environment a new well typed object that is not yet in the library    *)
+(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
+val add_type_checked_obj : 
+  UriManager.uri -> 
+  (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit
+
+  (** remove a type checked object
+  * @raise Object_not_found when given term is not in the environment
   * @raise Failure when remove_term is invoked while type checking *)
-val remove_term: UriManager.uri -> unit
+val remove_obj: UriManager.uri -> unit
 
 (* get_cooked_obj ~trust uri                                        *)
 (* returns the object if it is already type-checked or if it can be *)
@@ -95,17 +101,15 @@ val get_cooked_obj :
   ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->
     Cic.obj * CicUniv.universe_graph
 
-(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
-
-exception OnlyPutOfInductiveDefinitionsIsAllowed
+(* get_cooked_obj_with_univlist ~trust uri                          *)
+(* returns the object if it is already type-checked or if it can be *)
+(* trusted (if [trust] = true and the trusting function accepts it) *)
+(* Otherwise it raises Not_found                                    *)
+val get_cooked_obj_with_univlist : 
+  ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->
+    Cic.obj * CicUniv.universe_graph * CicUniv.universe list
 
-(* put_inductive_definition uri obj                                      *)
-(* put [obj] (that must be an InductiveDefinition and show URI is [uri]) *)
-(* in the environment.                                                   *)
-(* WARNING: VERY UNSAFE.                                                 *)
-(* This function should be called only on a well-typed definition.       *)
-val put_inductive_definition : 
-  UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
+(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
 
 (* (de)serialization *)
 val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
@@ -115,7 +119,18 @@ val empty : unit -> unit
 (** Set trust function. Per default this function is set to (fun _ -> true) *)
 val set_trust: (UriManager.uri -> bool) -> unit
 
-(* for filtering in tacticChaser *)
+  (** @return true for objects currently cooked/frozend/unchecked, false
+  * 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
+
+  (** total parsing time, only to benchmark the parser *)
+val total_parsing_time: float ref
+
 (* EOF *)