+ let src_carr, tgt_carr =
+ let get_classes arity saturations l =
+ (* this is the ackerman's function revisited *)
+ let rec aux = function
+ 0,0,None,tgt::src::_ -> src,Some (`Class tgt)
+ | 0,0,target,src::_ -> src,target
+ | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl)
+ | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl)
+ | arity,saturations,None,_::tl ->
+ aux (arity, saturations, Some `Funclass, tl)
+ | arity,saturations,target,_::tl ->
+ aux (arity - 1, saturations, target, tl)
+ | _ -> assert false
+ in
+ aux (arity,saturations,None,List.rev l)
+ in
+ let types = spine2list coer_ty in
+ let src,tgt = get_classes arity saturations types in
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+ match tgt with
+ None -> assert false
+ | Some `Funclass -> CoercDb.Fun arity
+ | Some (`Class tgt) ->
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+ in
+ let already_in_obj src_carr tgt_carr uri obj =