From 20dacdd66818f115aab029824b7408c0d4f804c4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 13 Dec 2001 12:09:17 +0000 Subject: [PATCH] The hash-table used in the implementation was of "type" (UriManager.uri * int) -> Cic.obj Is is now of type UriManager.uri -> (int * Cic.obj) list where the list is ordered from the most cooked to the less cooked. There is almost no difference at all in the performance of big files (limit_plus). The new design is easier to extend to a real cache with rollback. --- .../cic_proof_checking/cicEnvironment.ml | 45 ++++++++++++++----- 1 file changed, 34 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 436474ea5..5d4261c90 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -75,24 +75,45 @@ module Cache : 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 + 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 + 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 = HT.mem hashtable;; - let find = HT.find hashtable;; - let add = HT.add hashtable;; + 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 [];; @@ -106,7 +127,7 @@ module Cache : if List.mem_assq uri !frozen_list then raise (CircularDependency (UriManager.string_of_uri uri)) else - if CacheOfCookedObjects.mem (uri,0) then + if CacheOfCookedObjects.mem uri 0 then raise (AlreadyCooked (UriManager.string_of_uri uri)) else (* OK, it is not already frozen nor cooked *) @@ -126,11 +147,13 @@ module Cache : 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 + 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 = CacheOfCookedObjects.find;; + let find_cooked (uri,cookingsno)= CacheOfCookedObjects.find uri cookingsno;; end ;; -- 2.39.2