X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=5d4261c90a68a957697652ba6a7daf21fdc24844;hb=20dacdd66818f115aab029824b7408c0d4f804c4;hp=436474ea559f4485bf287797939aba872950c0bb;hpb=4fcebf318b866ce041b31d7ac4ddb0fdb29d098d;p=helm.git

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