+exception NotSimilar
+let alpha t1 t2 ref ref' =
+ let rec aux t1 t2 = match t1,t2 with
+ | NCic.Rel n, NCic.Rel m when n=m -> ()
+ | NCic.Appl l1, NCic.Appl l2 -> List.iter2 aux l1 l2
+ | NCic.Lambda (_,s1,t1), NCic.Lambda (_,s2,t2)
+ | NCic.Prod (_,s1,t1), NCic.Prod (_,s2,t2) -> aux s1 s2; aux t1 t2
+ | NCic.LetIn (_,s1,ty1,t1), NCic.LetIn (_,s2,ty2,t2) ->
+ aux s1 s2; aux ty1 ty2; aux t1 t2
+ | NCic.Const (NReference.Ref (uu1,xp1)),
+ NCic.Const (NReference.Ref (uu2,xp2)) when
+ let NReference.Ref (u1,_) = ref in
+ let NReference.Ref (u2,_) = ref' in
+ NUri.eq uu1 u1 && NUri.eq uu2 u2 && xp1 = xp2
+ -> ()
+ | NCic.Const r1, NCic.Const r2 when NReference.eq r1 r2 -> ()
+ | NCic.Meta _,NCic.Meta _ -> ()
+ | NCic.Implicit _,NCic.Implicit _ -> ()
+ | NCic.Sort x,NCic.Sort y when x=y -> ()
+ | NCic.Match (_,t1,t11,tl1), NCic.Match (_,t2,t22,tl2) ->
+ aux t1 t2;aux t11 t22;List.iter2 aux tl1 tl2
+ | _-> raise NotSimilar
+ in
+ try aux t1 t2; true with NotSimilar -> false
+;;
+
+exception Found of NReference.reference;;
+let cache = Hashtbl.create 313;;
+let same_obj ref ref' =
+ function
+ | (_,_,_,_,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 && b1=b2->
+ true
+ | _ -> false
+;;
+let find_in_cache name obj ref =
+ try
+ List.iter
+ (function (ref',obj') ->
+ 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 (
+(*
+prerr_endline ("!!!!!!!!!!! CACHE HIT !!!!!!!!!!\n" ^
+NReference.string_of_reference ref ^ "\n" ^
+NReference.string_of_reference ref' ^ "\n");
+ *)
+ raise (Found ref'));
+(*
+prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==> " ^ NReference.string_of_reference ref');
+ *)
+ ) (Hashtbl.find_all cache name);
+(* prerr_endline "<<< CACHE MISS >>>"; *)
+ begin
+ match obj, ref with
+ | (_,_,_,_,NCic.Fixpoint (true,fl,_)) ,
+ NReference.Ref (_,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 (_,NReference.CoFix _) ->
+ ignore(List.fold_left (fun i (_,name,_,_,_) ->
+ let ref = NReference.mk_cofix i ref in
+ Hashtbl.add cache name (ref,obj);
+ i+1
+ ) 0 fl)
+ | _ -> assert false
+ end;
+ None
+ with Found ref -> Some ref
+;;
+
+let cache1 = UriManager.UriHashtbl.create 313;;
+let rec get_height =
+ function u ->
+ try
+ UriManager.UriHashtbl.find cache1 u
+ with
+ Not_found ->
+ let h = ref 0 in
+ let res =
+ match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u) with
+ Cic.Constant (_,Some bo,ty,params,_)
+ | Cic.Variable (_,Some bo,ty,params,_) ->
+ ignore (height_of_term ~h bo);
+ ignore (height_of_term ~h ty);
+ List.iter (function uri -> h := max !h (get_height uri)) params;
+ 1 + !h
+ | _ -> 0
+ in
+ UriManager.UriHashtbl.add cache1 u res;
+ res
+and height_of_term ?(h=ref 0) t =
+ let rec aux =
+ function
+ Cic.Rel _
+ | Cic.Sort _ -> ()
+ | Cic.Implicit _ -> assert false
+ | Cic.Var (uri,exp_named_subst)
+ | Cic.Const (uri,exp_named_subst)
+ | Cic.MutInd (uri,_,exp_named_subst)
+ | Cic.MutConstruct (uri,_,_,exp_named_subst) ->
+ h := max !h (get_height uri);
+ List.iter (function (_,t) -> aux t) exp_named_subst
+ | Cic.Meta (_,l) -> List.iter (function None -> () | Some t -> aux t) l
+ | Cic.Cast (t1,t2)
+ | Cic.Prod (_,t1,t2)
+ | Cic.Lambda (_,t1,t2) -> aux t1; aux t2
+ | Cic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
+ | Cic.Appl l -> List.iter aux l
+ | Cic.MutCase (_,_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
+ | Cic.Fix (_, fl) -> List.iter (fun (_, _, ty, bo) -> aux ty; aux bo) fl; incr h
+ | Cic.CoFix (_, fl) -> List.iter (fun (_, ty, bo) -> aux ty; aux bo) fl; incr h
+ in
+ aux t;
+ 1 + !h
+;;
+
+ (* k=true if we are converting a term to be pushed in a ctx or if we are
+ converting the type of a fix;
+ k=false if we are converting a term to be put in the body of a fix;
+ in the latter case, we must permute Rels since the Fix abstraction will
+ preceed its lefts parameters; in the former case, there is nothing to
+ permute *)
+ let rec aux k octx (ctx : ctx list) n_fix uri = function
+ | Cic.CoFix _ as cofix ->
+ let octx,ctx,fix,rels = restrict octx ctx cofix in
+ let cofixno,fl =
+ match fix with Cic.CoFix (cofixno,fl)->cofixno,fl | _-> assert false in