It is a very UNSAFE solution to the problem of computing inner-types of
non-debrujined mutual inductive types (whose constructors referes to
the not-yet-defined inductive type block): you can use this function to
add the block to the environment; then you compute the inner-types; and
finally you save the object and register it to the getter.
val frozen_to_cooked :
uri:UriManager.uri -> unit
val find_cooked : key:UriManager.uri -> Cic.obj
val frozen_to_cooked :
uri:UriManager.uri -> unit
val find_cooked : key:UriManager.uri -> Cic.obj
+ val add_cooked : key:UriManager.uri -> Cic.obj -> unit
Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
;;
let find_cooked ~key:uri = CacheOfCookedObjects.find uri;;
Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
;;
let find_cooked ~key:uri = CacheOfCookedObjects.find uri;;
+ let add_cooked ~key:uri obj = CacheOfCookedObjects.add uri obj;;
Not_found ->
find_or_add_unchecked_to_cache uri
;;
Not_found ->
find_or_add_unchecked_to_cache uri
;;
+
+exception OnlyPutOfInductiveDefinitionsIsAllowed
+
+let put_inductive_definition uri obj =
+ match obj with
+ Cic.InductiveDefinition _ -> Cache.add_cooked uri obj
+ | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
+;;
(* again in the future (is_type_checked will return true) *)
val set_type_checking_info : UriManager.uri -> unit
(* again in the future (is_type_checked will return true) *)
val set_type_checking_info : UriManager.uri -> unit
-(* get_cooked_obj ~trust uri *)
+(* 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 -> Cic.obj
(* 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
+
+(* 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 -> unit