From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 13 Dec 2001 12:09:17 +0000 (+0000)
Subject: The hash-table used in the implementation was of "type"
X-Git-Tag: mlminidom_0_2_2~9
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20dacdd66818f115aab029824b7408c0d4f804c4;p=helm.git

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.
---

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
 ;;