+ let src_carr, tgt_carr, no_args =
+ 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) 0,
+ (match tgt with
+ | None -> assert false
+ | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity
+ | Some (`Class tgt) ->
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0),
+ List.length types - 1
+ in
+ let already_in_obj src_carr tgt_carr uri obj =
+ List.exists
+ (fun (s,t,ul) ->
+ if not (CoercDb.eq_carr s src_carr &&
+ CoercDb.eq_carr t tgt_carr)
+ then false
+ else
+ List.exists
+ (fun u,_,_ ->
+ let bo, ty =
+ match obj with
+ | Cic.Constant (_, Some bo, ty, _, _) -> bo, ty
+ | _ ->
+ (* this is not a composite coercion, thus the uri is valid *)
+ let bo = CicUtil.term_of_uri uri in
+ bo,
+ fst (CicTypeChecker.type_of_aux' [] [] bo
+ CicUniv.oblivion_ugraph)
+ in
+ let are_body_convertible =
+ fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
+ CicUniv.oblivion_ugraph)
+ in
+ if not are_body_convertible then
+ (HLog.warn
+ ("Coercions " ^
+ UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
+ uri^" are not convertible, but are between the same nodes.\n"^
+ "From now on unification can fail randomly.");
+ false)
+ else
+ match t, tgt_carr with
+ | CoercDb.Sort (Cic.Type i), CoercDb.Sort (Cic.Type j)
+ | CoercDb.Sort (Cic.CProp i), CoercDb.Sort (Cic.CProp j)
+ when not (CicUniv.eq i j) ->
+ (HLog.warn
+ ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^
+ "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^
+ "different universe : " ^
+ CicUniv.string_of_universe j ^ " <> " ^
+ CicUniv.string_of_universe i); false)
+ | CoercDb.Sort Cic.Prop , CoercDb.Sort Cic.Prop
+ | CoercDb.Sort (Cic.Type _) , CoercDb.Sort (Cic.Type _)
+ | CoercDb.Sort (Cic.CProp _), CoercDb.Sort (Cic.CProp _) ->
+ (HLog.warn
+ ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
+ "it is a duplicate of " ^ UriManager.string_of_uri u);
+ true)
+ | CoercDb.Sort s1, CoercDb.Sort s2 ->
+ (HLog.warn
+ ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^
+ "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^
+ "different universe : " ^
+ CicPp.ppterm (Cic.Sort s1) ^ " <> " ^
+ CicPp.ppterm (Cic.Sort s2)); false)
+ | _ ->
+ let ty', _ =
+ CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u)
+ CicUniv.oblivion_ugraph
+ in
+ if CicUtil.alpha_equivalence ty ty' then
+ (HLog.warn
+ ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
+ "it is a duplicate of " ^ UriManager.string_of_uri u);
+ true)
+ else false
+
+ )
+ ul)