+(* 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
+ let equal = UriManager.eq
+ let hash = Hashtbl.hash
+ end
+ ;;
+ module HT = Hashtbl.Make(HashedType);;
+ let hashtable = HT.create 1009;;
+ let mem uri cookingsno =
+ try
+ let cooked_list =
+ HT.find hashtable uri
+ in
+ List.mem_assq cookingsno !cooked_list
+ with
+ Not_found -> false
+ ;;
+ let find uri cookingsno =
+ List.assq cookingsno !(HT.find hashtable uri)
+ ;;
+ let add uri cookingsno obj =
+ let cooked_list =
+ try
+ HT.find hashtable uri
+ with
+ Not_found ->
+ let newl = ref [] in
+ HT.add hashtable uri newl ;
+ newl
+ in
+ cooked_list := (cookingsno,obj)::!cooked_list
+ ;;
+ 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:(fun (uri,cookno) -> CacheOfCookedObjects.add uri cookno)
+ with
+ Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
+ ;;
+ let find_cooked ~key:(uri,cookingsno)= CacheOfCookedObjects.find uri cookingsno;;
+ end