-(* set_type_checking_info uri *)
-(* 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 =
- Cache.frozen_to_cooked uri
- (fun ~object_to_cook:obj ~add_cooked ->
- (* let's cook the object at every level *)
- let obj' = CicSubstitution.undebrujin_inductive_def uri obj in
- add_cooked (uri,0) obj' ;
- let cooked_objs = !cook_obj obj' uri in
- let last_cooked_level = ref 0 in
- let last_cooked_obj = ref obj' in
- List.iter
- (fun (n,cobj) ->
- for i = !last_cooked_level + 1 to n do
- add_cooked (uri,i) !last_cooked_obj
- done ;
- add_cooked (uri,n + 1) cobj ;
- last_cooked_level := n + 1 ;
- last_cooked_obj := cobj
- ) cooked_objs ;
- for i = !last_cooked_level + 1 to UriManager.depth_of_uri uri + 1 do
- add_cooked (uri,i) !last_cooked_obj
- done
- )
+(* 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 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 *)
+(* 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.getxml uri *)
+let get_obj uri =
+ try
+ get_cooked_obj uri
+ with
+ 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