+(* Cache that uses == instead of = for testing equality *)
+(* Invariant: an object is always in at most one of the *)
+(* following states: unchecked, frozen and cooked. *)
+module Cache :
+ sig
+ val find_or_add_unchecked :
+ UriManager.uri -> get_object_to_add:(unit -> Cic.obj) -> Cic.obj
+ val unchecked_to_frozen : UriManager.uri -> unit
+ val frozen_to_cooked :
+ uri:UriManager.uri ->
+ cooking_procedure:
+ (object_to_cook:Cic.obj ->
+ add_cooked:(UriManager.uri * int-> Cic.obj -> unit)
+ -> unit
+ )
+ -> unit
+ val find_cooked : key:(UriManager.uri * int) -> Cic.obj
+ end
+=
+ struct
+ module CacheOfCookedObjects :
+ sig
+ val mem : (UriManager.uri * int) -> bool
+ val find : (UriManager.uri * int) -> Cic.obj
+ val add : (UriManager.uri * int) -> Cic.obj -> unit
+ end
+ =
+ struct
+ module HashedType =
+ struct
+ type t = UriManager.uri * int (* uri, livello di cottura *)
+ let equal (u1,n1) (u2,n2) = UriManager.eq u1 u2 && n1 = n2
+ let hash = Hashtbl.hash
+ end
+ ;;
+ module HT = Hashtbl.Make(HashedType);;
+ let hashtable = HT.create 1009;;
+ let mem = HT.mem hashtable;;
+ let find = HT.find hashtable;;
+ let add = HT.add hashtable;;
+ end
+ ;;
+ let frozen_list = ref [];;
+ let unchecked_list = ref [];;
+
+ let find_or_add_unchecked uri ~get_object_to_add =
+ try
+ List.assq uri !unchecked_list
+ with
+ Not_found ->
+ if List.mem_assq uri !frozen_list then
+ raise (CircularDependency (UriManager.string_of_uri uri))
+ else
+ if CacheOfCookedObjects.mem (uri,0) then
+ raise (AlreadyCooked (UriManager.string_of_uri uri))
+ else
+ (* OK, it is not already frozen nor cooked *)
+ let obj = get_object_to_add () in
+ unchecked_list := (uri,obj)::!unchecked_list ;
+ obj
+ ;;
+ let unchecked_to_frozen uri =
+ try
+ let obj = List.assq uri !unchecked_list in
+ unchecked_list := List.remove_assq uri !unchecked_list ;
+ frozen_list := (uri,obj)::!frozen_list
+ with
+ Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
+ ;;
+ let frozen_to_cooked ~uri ~cooking_procedure =
+ try
+ let obj = List.assq uri !frozen_list in
+ frozen_list := List.remove_assq uri !frozen_list ;
+ cooking_procedure ~object_to_cook:obj ~add_cooked:CacheOfCookedObjects.add
+ with
+ Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
+ ;;
+ let find_cooked = CacheOfCookedObjects.find;;
+ end