+ let already_in_obj src_carr tgt_carr uri obj =
+ List.exists
+ (fun (s,t,ul) ->
+ List.exists
+ (fun u,_ ->
+ let bo =
+ match obj with
+ | Cic.Constant (_, Some bo, _, _, _) -> bo
+ | _ -> assert false
+ in
+ CoercDb.eq_carr s src_carr &&
+ CoercDb.eq_carr t tgt_carr &&
+ if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
+ CicUniv.oblivion_ugraph)
+ then true else
+ (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))
+ ul)
+ (CoercDb.to_list ())
+ in
+ if not add_composites then
+ (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+ UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
+ [])
+ else
+ let new_coercions =
+ CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
+ baseuri
+ in
+ let new_coercions =
+ List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
+ new_coercions
+ in
+ let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
+ (* update the DB *)
+ List.iter
+ (fun (src,tgt,uri,saturations,_,_) ->
+ CoercDb.add_coercion (src,tgt,uri,saturations))
+ new_coercions;
+ CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+ (* add the composites obj and they eventual lemmas *)
+ let lemmas =
+ List.fold_left
+ (fun acc (_,tgt,uri,saturations,obj,arity) ->
+ add_single_obj uri obj refinement_toolkit;
+ (uri,arity,saturations)::acc)
+ [] new_coercions
+ in
+ (* store that composite_uris are related to uri. the first component is
+ * the stuff in the DB while the second is stuff for remove_obj *)
+ (*
+ prerr_endline ("adding: " ^
+ string_of_bool add_composites ^ UriManager.string_of_uri uri);
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ composite_uris;
+ *)
+ UriManager.UriHashtbl.add
+ coercion_hashtbl uri (composite_uris,composite_uris);
+ (*
+ prerr_endline ("lemmas:");
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ lemmas;
+ prerr_endline ("lemmas END");*)
+ lemmas
+;;