-
-let generate_projections 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 uri obj refinement_toolkit;
- let composites =
- if coercion then
- begin
-(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
- let x = add_coercion ~add_composites:true refinement_toolkit uri
- in
-(*prerr_endline ("are: ");
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
- prerr_endline "---";
-*)
- x
- end
- 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 uri obj =
- match !build_inversion_principle uri obj with
- None -> []
- | Some (ind_uri,ind_obj) ->
- add_single_obj ind_uri ind_obj refinement_toolkit;
- [ind_uri]
-
-let add_obj refinement_toolkit uri obj =
- add_single_obj uri obj refinement_toolkit;
- let uris = ref [] in
- try
- begin
- match obj with
- | Cic.Constant _ -> ()
- | Cic.InductiveDefinition (_,_,_,attrs) ->
- uris := !uris @
- generate_elimination_principles uri refinement_toolkit;
- uris := !uris @ generate_inversion refinement_toolkit 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 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)
-