From 2034db684e1d295527afad07a94f2f3b6b4ed7e2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Nov 2005 10:11:00 +0000 Subject: [PATCH] Generation of auxiliary lemmas for inductive types and records moved from cic_proof_checking and matita to ocaml/library. --- helm/matita/matitaEngine.ml | 65 +------------- helm/matita/matitaSync.ml | 8 +- helm/ocaml/cic_proof_checking/.depend | 6 -- helm/ocaml/cic_proof_checking/Makefile | 3 +- helm/ocaml/library/.depend | 18 ++++ helm/ocaml/library/Makefile | 2 + .../cicElim.ml | 0 .../cicElim.mli | 0 .../cicRecord.ml | 0 .../cicRecord.mli | 0 helm/ocaml/library/librarySync.ml | 89 ++++++++++++++++++- helm/ocaml/library/librarySync.mli | 11 ++- 12 files changed, 121 insertions(+), 81 deletions(-) create mode 100644 helm/ocaml/library/.depend rename helm/ocaml/{cic_proof_checking => library}/cicElim.ml (100%) rename helm/ocaml/{cic_proof_checking => library}/cicElim.mli (100%) rename helm/ocaml/{cic_proof_checking => library}/cicRecord.ml (100%) rename helm/ocaml/{cic_proof_checking => library}/cicRecord.mli (100%) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 0fc5f6ab8..8f417485a 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -633,43 +633,6 @@ let eval_coercion status coercion = let status = add_moo_content moo_content status in { status with proof_status = No_proof } -let generate_elimination_principles uri status = - let status' = ref status in - let elim sort = - try - let uri,obj = CicElim.elim_of ~sort uri 0 in - status' := MatitaSync.add_obj uri obj !status' - with CicElim.Can_t_eliminate -> () - in - try - List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; - !status' - with exn -> - MatitaSync.time_travel ~present:!status' ~past:status; - raise exn - -let generate_projections uri fields status = - let projections = CicRecord.projections_of uri fields in - List.fold_left - (fun status (uri, name, bo) -> - 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 - MatitaSync.add_obj uri obj status - with - CicTypeChecker.TypeCheckerFailure s -> - HLog.message - ("Unable to create projection " ^ name ^ " cause: " ^ (Lazy.force s)); - status - | CicEnvironment.Object_not_found uri -> - let depend = UriManager.name_of_uri uri in - HLog.message - ("Unable to create projection " ^ name ^ " because it requires " ^ depend); - status - ) status projections - (* to avoid a long list of recursive functions *) let eval_from_moo_ref = ref (fun _ _ _ -> assert false);; @@ -793,7 +756,7 @@ let eval_command opts status cmd = command_error "Proof not completed! metasenv is not empty!"; let name = UriManager.name_of_uri uri in let obj = Cic.Constant (name,Some bo,ty,[],[]) in - MatitaSync.add_obj uri obj status + MatitaSync.add_obj uri obj {status with proof_status = No_proof} | GrafiteAst.Coercion (loc, coercion) -> eval_coercion status coercion | GrafiteAst.Alias (loc, spec) -> let diff = @@ -887,30 +850,8 @@ let eval_command opts status cmd = command_error ( "metasenv not empty while giving a definition with body: " ^ CicMetaSubst.ppmetasenv [] metasenv); - let status' = ref status in - (try - status' := MatitaSync.add_obj uri obj !status'; - (match obj with - | Cic.Constant _ -> () - | Cic.InductiveDefinition (_,_,_,attrs) -> - status' := generate_elimination_principles uri !status'; - 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 -> - status' := generate_projections uri fields !status') - | Cic.CurrentProof _ - | Cic.Variable _ -> assert false); - !status' - with exn -> - MatitaSync.time_travel ~present:!status' ~past:status; - raise exn) - + MatitaSync.add_obj uri obj {status with proof_status = No_proof} + let eval_executable opts status ex = match ex with | GrafiteAst.Tactical (_, tac, None) -> eval_tactical status tac diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 96ec76013..92999a49e 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -116,11 +116,9 @@ let add_aliases_for_object status uri = let add_obj uri obj status = let basedir = Helm_registry.get "matita.basedir" in - let status = - { add_aliases_for_object status uri obj with proof_status = No_proof} - in - LibrarySync.add_obj uri obj basedir; - status + let lemmas = LibrarySync.add_obj uri obj basedir in + List.fold_left add_alias_for_constant + (add_aliases_for_object status uri obj) lemmas let add_obj = let profiler = HExtlib.profile "add_obj" in diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index 630876902..06b9188a0 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -22,9 +22,3 @@ freshNamesGenerator.cmo: cicTypeChecker.cmi cicSubstitution.cmi \ freshNamesGenerator.cmi freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \ freshNamesGenerator.cmi -cicElim.cmo: freshNamesGenerator.cmi cicTypeChecker.cmi cicSubstitution.cmi \ - cicReduction.cmi cicPp.cmi cicEnvironment.cmi cicElim.cmi -cicElim.cmx: freshNamesGenerator.cmx cicTypeChecker.cmx cicSubstitution.cmx \ - cicReduction.cmx cicPp.cmx cicEnvironment.cmx cicElim.cmi -cicRecord.cmo: cicSubstitution.cmi cicEnvironment.cmi cicRecord.cmi -cicRecord.cmx: cicSubstitution.cmx cicEnvironment.cmx cicRecord.cmi diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index b5d1baa1a..3fbe90ddb 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -14,8 +14,7 @@ INTERFACE_FILES = \ cicReduction.mli \ cicTypeChecker.mli \ freshNamesGenerator.mli \ - cicElim.mli \ - cicRecord.mli + $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) # Metadata tools only need zeta-reduction diff --git a/helm/ocaml/library/.depend b/helm/ocaml/library/.depend new file mode 100644 index 000000000..34914e505 --- /dev/null +++ b/helm/ocaml/library/.depend @@ -0,0 +1,18 @@ +cicElim.cmo: cicElim.cmi +cicElim.cmx: cicElim.cmi +cicRecord.cmo: cicRecord.cmi +cicRecord.cmx: cicRecord.cmi +libraryMisc.cmo: libraryMisc.cmi +libraryMisc.cmx: libraryMisc.cmi +libraryDb.cmo: libraryDb.cmi +libraryDb.cmx: libraryDb.cmi +coercDb.cmo: coercDb.cmi +coercDb.cmx: coercDb.cmi +librarySync.cmo: libraryDb.cmi coercDb.cmi cicRecord.cmi cicElim.cmi \ + librarySync.cmi +librarySync.cmx: libraryDb.cmx coercDb.cmx cicRecord.cmx cicElim.cmx \ + librarySync.cmi +libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \ + libraryClean.cmi +libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \ + libraryClean.cmi diff --git a/helm/ocaml/library/Makefile b/helm/ocaml/library/Makefile index e50f03e93..d64c5020f 100644 --- a/helm/ocaml/library/Makefile +++ b/helm/ocaml/library/Makefile @@ -2,6 +2,8 @@ PACKAGE = library PREDICATES = INTERFACE_FILES = \ + cicElim.mli \ + cicRecord.mli \ libraryMisc.mli \ libraryDb.mli \ coercDb.mli \ diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/library/cicElim.ml similarity index 100% rename from helm/ocaml/cic_proof_checking/cicElim.ml rename to helm/ocaml/library/cicElim.ml diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/library/cicElim.mli similarity index 100% rename from helm/ocaml/cic_proof_checking/cicElim.mli rename to helm/ocaml/library/cicElim.mli diff --git a/helm/ocaml/cic_proof_checking/cicRecord.ml b/helm/ocaml/library/cicRecord.ml similarity index 100% rename from helm/ocaml/cic_proof_checking/cicRecord.ml rename to helm/ocaml/library/cicRecord.ml diff --git a/helm/ocaml/cic_proof_checking/cicRecord.mli b/helm/ocaml/library/cicRecord.mli similarity index 100% rename from helm/ocaml/cic_proof_checking/cicRecord.mli rename to helm/ocaml/library/cicRecord.mli diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index d853243dd..4aa966947 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -92,7 +92,7 @@ let index_obj = fun ~dbd ~uri -> profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri -let add_obj uri obj ~basedir = +let add_single_obj uri obj ~basedir = let dbd = LibraryDb.instance () in if CicEnvironment.in_library uri then raise (AlreadyDefined uri) @@ -119,7 +119,7 @@ let add_obj uri obj ~basedir = raise exc end -let remove_obj uri = +let remove_single_obj uri = let derived_uris_of_uri uri = let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u]) @@ -140,3 +140,88 @@ let remove_obj uri = CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri); CicEnvironment.remove_obj uri) to_remove + +(*** GENERATION OF AUXILIARY LEMMAS ***) + +let generate_elimination_principles ~basedir uri = + let uris = ref [] in + let elim sort = + try + let uri,obj = CicElim.elim_of ~sort uri 0 in + add_single_obj uri obj ~basedir; + uris := uri :: !uris + with CicElim.Can_t_eliminate -> () + in + try + List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; + !uris + with exn -> + List.iter remove_single_obj !uris; + raise exn + +let generate_projections ~basedir uri fields = + let uris = ref [] in + let projections = CicRecord.projections_of uri fields in + try + List.iter + (fun (uri, name, bo) -> + 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; + uris := uri :: !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; + !uris + with exn -> + List.iter remove_single_obj !uris; + raise exn + +let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 + +let add_obj uri obj ~basedir = + add_single_obj uri obj ~basedir; + let uris = ref [] in + try + begin + match obj with + | Cic.Constant _ -> () + | Cic.InductiveDefinition (_,_,_,attrs) -> + uris := !uris @ generate_elimination_principles ~basedir uri; + 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 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 + UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri + with + Not_found -> [] + in + List.iter remove_single_obj (uri::uris) diff --git a/helm/ocaml/library/librarySync.mli b/helm/ocaml/library/librarySync.mli index 0e0916e4d..89262e393 100644 --- a/helm/ocaml/library/librarySync.mli +++ b/helm/ocaml/library/librarySync.mli @@ -23,9 +23,12 @@ * http://helm.cs.unibo.it/ *) -(* returns a list of added URIs and their paths on disk *) -(*CSC: the path on disk should be computable from the URI!!! *) -val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> unit +(* adds an object to the library together with all auxiliary lemmas on it *) +(* (e.g. elimination principles, projections, etc.) *) +(* it returns the list of the uris of the auxiliary lemmas generated *) +val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> UriManager.uri list -(* inverse of add_obj; it does not remove the objects depending on it! *) +(* inverse of add_obj; *) +(* Warning: it does not remove the dependencies on the object and on its *) +(* auxiliary lemmas! *) val remove_obj: UriManager.uri -> unit -- 2.39.2