let cleanup_tmp = true;;
-let never_trust = function uri -> false;;
-let always_trust = function uri -> true;;
-let trust_obj = ref never_trust;;
+let trust_obj = function uri -> true;;
type type_checked_obj =
CheckedObj of Cic.obj (* cooked 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
end
=
struct
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;;
end
;;
(* The body does not exist ==> we consider it an axiom *)
None
in
- let obj = CicParser.obj_of_xml filename bodyfilename uri in
+ let obj = CicParser.obj_of_xml filename bodyfilename in
if cleanup_tmp then
begin
Unix.unlink filename ;
(* must be called once the type-checking of uri is finished *)
(* The object whose uri is uri is unfreezed *)
let set_type_checking_info uri =
- trust_obj := never_trust ;
Cache.frozen_to_cooked uri
;;
(* otherwise it freezes the term for type-checking and returns
it *)
(* set_type_checking_info must be called to unfreeze the term *)
-let is_type_checked uri =
+let is_type_checked ?(trust=true) uri =
try
CheckedObj (Cache.find_cooked uri)
with
Not_found ->
let obj = find_or_add_unchecked_to_cache uri in
Cache.unchecked_to_frozen uri ;
- if !trust_obj uri then
+ if trust && trust_obj uri then
begin
-prerr_endline ("### " ^ UriManager.string_of_uri uri ^ " TRUSTED!!!") ;
+ Logger.log (`Trusting uri) ;
set_type_checking_info uri ;
- trust_obj := always_trust ;
CheckedObj (Cache.find_cooked uri)
end
else
- begin
- trust_obj := always_trust ;
- UncheckedObj obj
- end
+ UncheckedObj obj
;;
-(* get_cooked_obj uri *)
-(* returns the cooked cic object whose uri is uri. The term must be present *)
-(* and cooked in cache *)
-let get_cooked_obj 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 *)
+let get_cooked_obj ?(trust=true) uri =
try
Cache.find_cooked uri
with Not_found ->
- if not (!trust_obj uri) then
- prerr_endline ("@@@ OOOOOOOPS: WE TRUST " ^ UriManager.string_of_uri uri ^ " EVEN IF WE SHOULD NOT DO THAT! THAT MEANS LOOKING FOR TROUBLES ;-(") ;
- match is_type_checked uri with
- CheckedObj obj -> obj
- | _ -> assert false
+ if trust && trust_obj uri then
+ begin
+ match is_type_checked uri with
+ CheckedObj obj -> obj
+ | _ -> assert false
+ end
+ else
+ begin
+ prerr_endline ("@@@ OOOOOOOPS: get_cooked_obj(" ^ UriManager.string_of_uri uri ^ ") raises Not_found since the object is not type-checked nor trusted.") ;
+ raise Not_found
+ end
;;
(* get_obj 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
+;;