* 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. *)
+exception Object_not_found of UriManager.uri;;
+
+(* 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 *)
(* 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 :
+(* 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) -> unit
- (** remove a type checked term
- * @raise Term_not_found when given term is not in the environment
+ (** 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 *)
(* 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 *)
-exception OnlyPutOfInductiveDefinitionsIsAllowed
-
-(* 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
-
(* (de)serialization *)
val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
(** Set trust function. Per default this function is set to (fun _ -> true) *)
val set_trust: (UriManager.uri -> bool) -> unit
-(* for filtering in tacticChaser *)
-(* NEW *)
+ (** @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 *)