- let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
- if already_in then
- (* this if starts here just to be sure the closure function works fine *)
- begin
- assert (new_coercions = []);
- HLog.warn
- (UriManager.string_of_uri uri ^
- " is already declared as a coercion! skipping...");
- []
- end
- else
- begin
- (* update the DB *)
- List.iter
- (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
- new_coercions;
- CoercDb.add_coercion (src_carr, tgt_carr, uri);
- (* add the composites obj and they eventual lemmas *)
- let lemmas =
- if add_composites then
- List.fold_left
- (fun acc (_,tgt,uri,obj) ->
- add_single_obj uri obj refinement_toolkit;
- let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
- (uri,arity)::acc)
- [] new_coercions
- else
- []
- 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,if add_composites then composite_uris else []);
- (*
- prerr_endline ("lemmas:");
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- lemmas;
- prerr_endline ("lemmas END");*)
- lemmas
- end
+ 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