* 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 *)
-val get_obj : UriManager.uri -> Cic.obj
+(* 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. *)
+val get_obj :
+ ?not_jet_cooked:bool -> UriManager.uri -> CicUniv.universe_graph ->
+ Cic.obj * CicUniv.universe_graph
type type_checked_obj =
- CheckedObj of Cic.obj (* cooked obj *)
+ CheckedObj of (Cic.obj * CicUniv.universe_graph) (* cooked obj *)
| UncheckedObj of Cic.obj (* uncooked obj *)
(* is_type_checked uri cookingsno *)
(* otherwise it returns (false,object) and freeze the object for *)
(* type-checking *)
(* set_type_checking_info must be called to unfreeze the object *)
-val is_type_checked : ?trust:bool -> UriManager.uri -> type_checked_obj
+val is_type_checked :
+ ?trust:bool -> UriManager.uri -> CicUniv.universe_graph -> type_checked_obj
(* set_type_checking_info uri *)
(* must be called once the type-checking of uri is finished *)
(* The object whose uri is uri is unfreezed and won't be type-checked *)
(* again in the future (is_type_checked will return true) *)
-val set_type_checking_info : UriManager.uri -> unit
+(* *)
+(* Since the universes are not exported directly, but generated *)
+(* typecheking the library, we can't find them in the library as we *)
+(* do for the types. This means that when we commit uris during *)
+(* univ generation we can't associate the uri with the universe graph *)
+(* 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 *)
+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 -> unit
+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
(* 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 -> Cic.obj
+val get_cooked_obj :
+ ?trust:bool -> UriManager.uri ->
+ CicUniv.universe_graph -> Cic.obj * CicUniv.universe_graph
(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
(* 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 -> unit
+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
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 *)
(* NEW *)
val in_cache : UriManager.uri -> bool