+(* 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 -> unit
+ val find_cooked : key:UriManager.uri -> Cic.obj
+ val add_cooked : key:UriManager.uri -> Cic.obj -> unit
+ end
+=
+ struct
+ module CacheOfCookedObjects :
+ sig
+ val mem : UriManager.uri -> bool
+ val find : UriManager.uri -> Cic.obj
+ val add : UriManager.uri -> Cic.obj -> unit
+ end
+ =
+ struct
+ module HashedType =
+ struct
+ type t = UriManager.uri
+ let equal = UriManager.eq
+ let hash = Hashtbl.hash
+ end
+ ;;
+ module HT = Hashtbl.Make(HashedType);;
+ let hashtable = HT.create 1009;;
+ let mem uri =
+ try
+ HT.mem hashtable uri
+ with
+ Not_found -> false
+ ;;
+ let find uri = HT.find hashtable uri
+ ;;
+ let add uri obj =
+ HT.add hashtable uri obj
+ ;;
+ 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 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 =
+ try
+ let obj = List.assq uri !frozen_list in
+ frozen_list := List.remove_assq uri !frozen_list ;
+ CacheOfCookedObjects.add uri obj
+ with
+ 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