ficed fixpoint cache usage for mutual fix

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 876f6a261670692977b2cb34d1d50726bcdfcffc..9751fa7bfb0a623058e552b89b9e11de1b661022 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -276,8 +276,8 @@ exception Found of NReference.reference;;
 let cache = Hashtbl.create 313;; 
 let same_obj =
  function
-    (_,_,_,_,NCic.Fixpoint (_,[_,_,_,ty1,_],_)),
-    (_,_,_,_,NCic.Fixpoint (_,[_,_,_,ty2,_],_))
+    (_,_,_,_,NCic.Fixpoint (_,(_,_,_,ty1,_)::_,_)),
+    (_,_,_,_,NCic.Fixpoint (_,(_,_,_,ty2,_)::_,_))
      when ty1 = ty2 -> true
   | _ -> false
 ;;
@@ -293,19 +293,25 @@ let find_in_cache name obj ref =
       match ref' with
          NReference.Ref (_,_,NReference.Fix (_,recno)) -> recno
        | _ -> assert false in
-     if recno = recno' && same_obj (obj,obj') then
-(*(prerr_endline "!!!!!!!!!!! CACHE HIT !!!!!!!!!!";*)
+     if recno = recno' && same_obj (obj,obj') then (
+(* prerr_endline "!!!!!!!!!!! CACHE HIT !!!!!!!!!!"; *)
        raise (Found ref')
-(*);*)
+);
 (*
-     else
-(prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==> " ^ NReference.string_of_reference ref');
-      raise Not_found
-)
+prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==> " ^ NReference.string_of_reference ref');
 *)
   ) (Hashtbl.find_all cache name);
-(*prerr_endline "<<< CACHE MISS >>>";*)
-  Hashtbl.add cache name (ref,obj);
+(* prerr_endline "<<< CACHE MISS >>>"; *)
+  begin
+    match obj, ref with 
+    | (_,_,_,_,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)
+    | _ -> assert false
+  end;
   None
  with Found ref -> Some ref
 ;;