From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 5 May 2008 16:41:39 +0000 (+0000)
Subject: CoFix cache implemented
X-Git-Tag: make_still_working~5252
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c0495bcd403a681e3abf1261068984f4e4e00128;p=helm.git

CoFix cache implemented
---

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 0aafc58c7..77b9a897f 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -321,9 +321,9 @@ exception Found of NReference.reference;;
 let cache = Hashtbl.create 313;; 
 let same_obj ref ref' =
  function
-  | (_,_,_,_,NCic.Fixpoint (_,l1,_)), (_,_,_,_,NCic.Fixpoint (_,l2,_))
+  | (_,_,_,_,NCic.Fixpoint (b1,l1,_)), (_,_,_,_,NCic.Fixpoint (b2,l2,_))
     when List.for_all2 (fun (_,_,_,ty1,bo1) (_,_,_,ty2,bo2) -> 
-       alpha ty1 ty2 ref ref' && alpha bo1 bo2 ref ref') l1 l2 ->
+       alpha ty1 ty2 ref ref' && alpha bo1 bo2 ref ref') l1 l2 && b1=b2->
      true
   | _ -> false
 ;;
@@ -334,10 +334,12 @@ let find_in_cache name obj ref =
      let recno, fixno =
       match ref with
          NReference.Ref (_,_,NReference.Fix (fixno,recno)) -> recno,fixno
+       | NReference.Ref (_,_,NReference.CoFix (fixno)) -> ~-1,fixno
        | _ -> assert false in
      let recno',fixno' =
       match ref' with
          NReference.Ref (_,_,NReference.Fix (fixno',recno)) -> recno,fixno'
+       | NReference.Ref (_,_,NReference.CoFix (fixno')) -> ~-1,fixno'
        | _ -> assert false in
      if recno = recno' && fixno = fixno' && same_obj ref ref' (obj,obj') then (
 (*
@@ -353,12 +355,20 @@ prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==>
 (*   prerr_endline "<<< CACHE MISS >>>";   *)
   begin
     match obj, ref with 
-    | (_,_,_,_,NCic.Fixpoint (true,fl,_)) , NReference.Ref (x,y,NReference.Fix _) ->
+    | (_,_,_,_,NCic.Fixpoint (true,fl,_)) , 
+      NReference.Ref (x,y,NReference.Fix _) ->
        ignore(List.fold_left (fun i (_,name,rno,_,_) ->
          let ref = NReference.mk_fix i rno ref in
          Hashtbl.add cache name (ref,obj);
          i+1
        ) 0 fl)
+    | (_,_,_,_,NCic.Fixpoint (false,fl,_)) , 
+      NReference.Ref (x,y,NReference.CoFix _) ->
+       ignore(List.fold_left (fun i (_,name,rno,_,_) ->
+         let ref = NReference.mk_cofix i ref in
+         Hashtbl.add cache name (ref,obj);
+         i+1
+       ) 0 fl)
     | _ -> assert false
   end;
   None
@@ -416,10 +426,14 @@ let convert_term uri t =
           NUri.nuri_of_ouri buri,0,[],[],
             NCic.Fixpoint (false, fl, (`Generated, `Definition)) 
         in
-        splat_args ctx 
-         (NCic.Const (Ref.reference_of_ouri buri (Ref.CoFix cofixno)))
-         n_fix rels,
-        fixpoints @ [obj]
+        let r = Ref.reference_of_ouri buri (Ref.CoFix cofixno) in
+        let obj,r =
+         let _,name,_,_,_ = List.nth fl cofixno in
+         match find_in_cache name obj r with
+            Some r' -> [],r'
+          | None -> [obj],r
+        in
+        splat_args ctx (NCic.Const r) n_fix rels, fixpoints @ obj
     | Cic.Fix _ as fix ->
         let octx,ctx,fix,rels = restrict octx ctx fix in
         let fixno,fl =