(CoercDb.to_list ())
in
if not add_composites then
- (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
+ (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
CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
(* add the composites obj and they eventual lemmas *)
let lemmas =
- if add_composites then
List.fold_left
(fun acc (_,tgt,uri,saturations,obj,arity) ->
add_single_obj uri obj refinement_toolkit;
(uri,arity,saturations)::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 *)
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 []);
+ UriManager.UriHashtbl.add
+ coercion_hashtbl uri (composite_uris,composite_uris);
(*
prerr_endline ("lemmas:");
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
composites_in_db;*)
UriManager.UriHashtbl.remove coercion_hashtbl uri;
- CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u);
+ CoercDb.remove_coercion
+ (fun (_,_,u,_) -> UriManager.eq uri u);
(* remove from the DB *)
List.iter
(fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
(* remove composites from the lib *)
List.iter remove_single_obj composites_in_lib
with
- Not_found -> () (* mhh..... *)
+ Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *)
let generate_projections refinement_toolkit uri fields =