- prerr_endline ("removing: " ^UriManager.string_of_uri uri);
- 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);
- (* remove from the DB *)
- List.iter
- (fun u -> CoercDb.remove_coercion (fun (_,_,u1) -> UriManager.eq u u1))
- composites_in_db;
- (* remove composites from the lib *)
- List.iter remove_single_obj composites_in_lib
- with
- Not_found -> () (* mhh..... *)
-
-
-let generate_projections ~basedir refinement_toolkit uri fields =
- let uris = ref [] in
- let projections = CicRecord.projections_of uri (List.map fst fields) in
- try
- List.iter2
- (fun (uri, name, bo) (_name, coercion) ->
- try
- let ty, ugraph =
- CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
- let attrs = [`Class `Projection; `Generated] in
- let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
- add_single_obj ~basedir uri obj refinement_toolkit;
- let composites =
- if coercion then
- add_coercion ~basedir ~add_composites:true refinement_toolkit uri
- else
- []
- in
- uris := uri :: composites @ !uris
- with
- CicTypeChecker.TypeCheckerFailure s ->
- HLog.message
- ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s);
- | CicEnvironment.Object_not_found uri ->
- let depend = UriManager.name_of_uri uri in
- HLog.message
- ("Unable to create projection " ^ name ^ " because it requires " ^
- depend)
- ) projections fields;
- !uris
- with exn ->
- List.iter remove_single_obj !uris;
- raise exn
-
-
-let build_inversion_principle = ref (fun a b -> assert false);;
-
-let generate_inversion refinement_toolkit ~basedir uri obj =
- match !build_inversion_principle uri obj with
- None -> []
- | Some (ind_uri,ind_obj) ->
- add_single_obj ind_uri ind_obj refinement_toolkit ~basedir;
- [ind_uri]
-
-
-let add_obj refinement_toolkit uri obj ~basedir =
- add_single_obj uri obj refinement_toolkit ~basedir;
- let uris = ref [] in
- try
- begin
- match obj with
- | Cic.Constant _ -> ()
- | Cic.InductiveDefinition (_,_,_,attrs) ->
- uris := !uris @
- generate_elimination_principles ~basedir uri refinement_toolkit;
- uris := !uris @ generate_inversion refinement_toolkit ~basedir uri obj;
- let rec get_record_attrs =
- function
- | [] -> None
- | (`Class (`Record fields))::_ -> Some fields
- | _::tl -> get_record_attrs tl
- in
- (match get_record_attrs attrs with
- | None -> () (* not a record *)
- | Some fields ->
- uris := !uris @
- (generate_projections ~basedir refinement_toolkit uri fields))
- | Cic.CurrentProof _
- | Cic.Variable _ -> assert false
- end;
- UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
- !uris
- with exn ->
- List.iter remove_single_obj !uris;
- raise exn
-
-let remove_obj uri =
- let uris =
- try
- let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in
- UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
- res
- with
- Not_found -> [] (*assert false*)
- in
- List.iter remove_single_obj (uri::uris)
+ 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
+ (* update the DB *)
+ let lemmas =
+ List.fold_left
+ (fun acc (src,tgt,uri,saturations,obj,arity,cpos) ->
+ CoercDb.add_coercion (src,tgt,uri,saturations,cpos);
+ let acc = add_obj uri obj pack_coercion_obj @ uri::acc in
+ acc)
+ [] new_coercions
+ in
+ CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
+(* CoercDb.prefer uri; *)
+ lemmas
+;;