-
-let generate_projections refinement_toolkit uri fields =
- let uris = ref [] in
- let projections =
- CicRecord.projections_of uri
- (List.map (fun (x,_,_) -> x) fields)
- in
- try
- List.iter2
- (fun (uri, name, bo) (_name, coercion, arity) ->
- let saturations = 0 in
- try
- let ty, _ =
- CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_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);*)
- (*CSC: I think there is a bug here. The composite coercions
- are not remembered in the .moo file. Thus they are re-generated
- every time. Right? *)
- let x =
- add_coercion ~add_composites:true refinement_toolkit uri arity
- saturations (UriManager.buri_of_uri uri)
- in
-(*prerr_endline ("are: ");
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
- prerr_endline "---";
-*)
- (*CSC: I throw the arity away. See comment above *)
- List.map (fun u,_,_,_ -> u) 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 =
- List.map
- (fun (ind_uri,ind_obj) ->
- add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
- (!build_inversion_principle uri obj)
-
-let
- generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
-=
- function
- Cic.Fix (_,funs) ->
- snd (
- List.fold_right
- (fun (name,idx,ty,bo) (n,uris) ->
- if name = name_to_avoid then
- (n-1,uris)
- else
- let uri =
- UriManager.uri_of_string
- (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
- let bo = Cic.Fix (n-1,funs) in
- let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
- (add_single_obj uri obj refinement_toolkit;
- (n-1,uri::uris)))
- funs (List.length funs,[]))
- | Cic.CoFix (_,funs) ->
- snd (
- List.fold_right
- (fun (name,ty,bo) (n,uris) ->
- if name = name_to_avoid then
- (n-1,uris)
- else
- let uri =
- UriManager.uri_of_string
- (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
- let bo = Cic.CoFix (n-1,funs) in
- let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
- add_single_obj uri obj refinement_toolkit;
- (n-1,uri::uris)
- ) funs (List.length funs,[]))
- | _ -> assert false
-
-let add_obj refinement_toolkit uri obj =
- add_single_obj uri obj refinement_toolkit;
- let uris = ref [] in
- let not_debug = not (Helm_registry.get_bool "matita.debug") in
- try
- begin
- match obj with
- | Cic.Constant (name,Some bo,_,_,attrs) when
- List.mem (`Flavour `MutualDefinition) attrs ->
- uris :=
- !uris @
- generate_sibling_mutual_definitions refinement_toolkit uri attrs
- name bo
- | Cic.Constant _ -> ()
- | Cic.InductiveDefinition (inductivefuns,_,_,attrs) ->
- let _,inductive,_,_ = List.hd inductivefuns in
- if inductive then
- begin
- uris := !uris @
- generate_elimination_principles uri refinement_toolkit;
- uris := !uris @ generate_inversion refinement_toolkit uri obj;
- end ;
- 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 when not_debug ->
- 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)
-