From ddd6560f4e70ec3306d223738a441d5f1dd3eac9 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 30 Sep 2009 13:35:06 +0000 Subject: [PATCH] Added initial support for inversion principles in Matita NG. Added a case_tac tactical, performing goal selection matching metavariables by means of their associated tag. Added tagged implicits, which are refined as tagged metavariables. --- helm/software/components/Makefile | 2 + helm/software/components/acic_content/.depend | 3 - .../components/acic_content/cicNotationPt.ml | 2 +- .../components/acic_procedural/.depend | 7 - .../components/binaries/extractor/.depend | 4 - .../components/binaries/matitaprover/Makefile | 1 + .../components/binaries/table_creator/.depend | 2 - .../components/binaries/transcript/.depend | 5 - .../binaries/transcript/.depend.opt | 5 - helm/software/components/cic/.depend | 2 - helm/software/components/cic_acic/.depend | 3 - .../components/cic_disambiguation/.depend | 2 - .../cic_disambiguation/cicDisambiguate.ml | 2 +- .../components/cic_exportation/.depend | 1 - .../components/cic_proof_checking/.depend | 10 - .../components/cic_unification/.depend | 7 - helm/software/components/content_pres/.depend | 6 - .../components/content_pres/content2pres.ml | 3 +- .../components/disambiguation/.depend | 1 - helm/software/components/extlib/.depend | 10 - helm/software/components/getter/.depend | 7 - .../components/getter/http_getter_wget.ml | 3 +- helm/software/components/grafite/.depend | 2 - .../software/components/grafite/grafiteAst.ml | 3 +- .../components/grafite/grafiteAstPp.ml | 1 + .../components/grafite_engine/.depend | 1 - .../grafite_engine/grafiteEngine.ml | 21 ++ .../grafite_engine/grafiteEngine.mli | 3 +- .../components/grafite_parser/.depend | 5 - .../grafite_parser/grafiteParser.ml | 2 + helm/software/components/hgdome/.depend | 2 - helm/software/components/hmysql/.depend | 5 - helm/software/components/lexicon/.depend | 2 - helm/software/components/library/.depend | 9 - helm/software/components/logger/.depend | 1 - helm/software/components/metadata/.depend | 2 - .../components/ng_cic_content/.depend | 2 - .../components/ng_disambiguation/.depend | 1 - .../ng_disambiguation/nCicDisambiguate.ml | 1 + helm/software/components/ng_kernel/.depend | 1 - helm/software/components/ng_kernel/nCic.ml | 3 +- helm/software/components/ng_kernel/nCicPp.ml | 1 + .../components/ng_paramodulation/.depend | 2 - helm/software/components/ng_refiner/.depend | 15 +- .../components/ng_refiner/nCicRefiner.ml | 1 + helm/software/components/ng_tactics/.depend | 6 +- helm/software/components/ng_tactics/Makefile | 3 +- .../components/ng_tactics/nInversion.ml | 196 ++++++++++++++++++ .../components/ng_tactics/nInversion.mli | 15 ++ .../components/ng_tactics/nTactics.ml | 19 ++ .../components/ng_tactics/nTactics.mli | 1 + helm/software/components/registry/.depend | 1 - .../components/syntax_extensions/.depend | 3 - helm/software/components/tactics/.depend | 11 - helm/software/components/tactics/tactics.mli | 2 +- helm/software/components/thread/.depend | 2 - helm/software/components/tptp_grafite/.depend | 3 - helm/software/components/urimanager/.depend | 1 - helm/software/components/whelp/.depend | 2 - helm/software/components/xml/.depend | 2 - helm/software/components/xmldiff/.depend | 1 - 61 files changed, 283 insertions(+), 159 deletions(-) create mode 100644 helm/software/components/ng_tactics/nInversion.ml create mode 100644 helm/software/components/ng_tactics/nInversion.mli diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index b7c105fc0..7035411f3 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -42,6 +42,8 @@ MODULES = \ ng_tactics \ grafite_engine \ tptp_grafite \ + ng_kernel \ + ng_refiner \ $(NULL) METAS = $(MODULES:%=METAS/META.helm-%) diff --git a/helm/software/components/acic_content/.depend b/helm/software/components/acic_content/.depend index 89dca0e44..8ade458af 100644 --- a/helm/software/components/acic_content/.depend +++ b/helm/software/components/acic_content/.depend @@ -1,4 +1,3 @@ -content.cmi: acic2content.cmi: content.cmi content2cic.cmi: content.cmi cicNotationUtil.cmi: cicNotationPt.cmo @@ -6,8 +5,6 @@ cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi acic2astMatcher.cmi: cicNotationPt.cmo termAcicContent.cmi: cicNotationPt.cmo -cicNotationPt.cmo: -cicNotationPt.cmx: content.cmo: content.cmi content.cmx: content.cmi acic2content.cmo: content.cmi acic2content.cmi diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index 75e580d00..0480c3d26 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -83,7 +83,7 @@ type term = (* literal, substitutions. * Some [] -> user has given an empty explicit substitution list * None -> user has given no explicit substitution list *) - | Implicit of [`Vector | `JustOne] + | Implicit of [`Vector | `JustOne | `Tagged of string] | Meta of int * meta_subst list | Num of string * int (* literal, instance *) | Sort of sort_kind diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index 97238c4d8..8d0128744 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/components/acic_procedural/.depend @@ -1,13 +1,6 @@ -proceduralHelpers.cmi: -proceduralClassify.cmi: -proceduralOptimizer.cmi: -proceduralTypes.cmi: -proceduralMode.cmi: -proceduralConversion.cmi: procedural1.cmi: proceduralTypes.cmi procedural2.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi -acic2Procedural.cmi: proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi diff --git a/helm/software/components/binaries/extractor/.depend b/helm/software/components/binaries/extractor/.depend index 0c39328ae..e69de29bb 100644 --- a/helm/software/components/binaries/extractor/.depend +++ b/helm/software/components/binaries/extractor/.depend @@ -1,4 +0,0 @@ -extractor.cmo: -extractor.cmx: -extractor_manager.cmo: -extractor_manager.cmx: diff --git a/helm/software/components/binaries/matitaprover/Makefile b/helm/software/components/binaries/matitaprover/Makefile index 2b35935d9..edae652ae 100644 --- a/helm/software/components/binaries/matitaprover/Makefile +++ b/helm/software/components/binaries/matitaprover/Makefile @@ -11,6 +11,7 @@ clean: dist: mkdir -p $(DIST)/Sources + cp ReadMe $(DIST) cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources cd $(DIST); ln -s Sources/matitaprover.native matitaprover tar -cvzf $(DIST).tgz $(DIST) diff --git a/helm/software/components/binaries/table_creator/.depend b/helm/software/components/binaries/table_creator/.depend index 33147b949..e69de29bb 100644 --- a/helm/software/components/binaries/table_creator/.depend +++ b/helm/software/components/binaries/table_creator/.depend @@ -1,2 +0,0 @@ -table_creator.cmo: -table_creator.cmx: diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 87d1ed25c..bb6f22a64 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,11 +1,6 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index f17459162..efadc681e 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,11 +1,6 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend index a835b247f..c2c7105c7 100644 --- a/helm/software/components/cic/.depend +++ b/helm/software/components/cic/.depend @@ -1,10 +1,8 @@ -cicUniv.cmi: unshare.cmi: cic.cmo deannotate.cmi: cic.cmo cicParser.cmi: cic.cmo cicUtil.cmi: cic.cmo helmLibraryObjects.cmi: cic.cmo -libraryObjects.cmi: cic_indexable.cmi: cic.cmo path_indexing.cmi: cic.cmo cicInspect.cmi: cic.cmo diff --git a/helm/software/components/cic_acic/.depend b/helm/software/components/cic_acic/.depend index 5449d50aa..3fc1e0dce 100644 --- a/helm/software/components/cic_acic/.depend +++ b/helm/software/components/cic_acic/.depend @@ -1,6 +1,3 @@ -eta_fixing.cmi: -doubleTypeInference.cmi: -cic2acic.cmi: cic2Xml.cmi: cic2acic.cmi eta_fixing.cmo: eta_fixing.cmi eta_fixing.cmx: eta_fixing.cmi diff --git a/helm/software/components/cic_disambiguation/.depend b/helm/software/components/cic_disambiguation/.depend index a9ae65a5e..e9bd1168f 100644 --- a/helm/software/components/cic_disambiguation/.depend +++ b/helm/software/components/cic_disambiguation/.depend @@ -1,5 +1,3 @@ -cicDisambiguate.cmi: -disambiguateChoices.cmi: cicDisambiguate.cmo: cicDisambiguate.cmi cicDisambiguate.cmx: cicDisambiguate.cmi disambiguateChoices.cmo: disambiguateChoices.cmi diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index e52db62dd..db305e5d5 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -485,7 +485,7 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri CicEnvironment.CircularDependency _ -> raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment"))))) | CicNotationPt.Implicit `Vector -> assert false - | CicNotationPt.Implicit `JustOne -> Cic.Implicit None + | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) | CicNotationPt.Num (num, i) -> Disambiguate.resolve ~mk_choice ~env diff --git a/helm/software/components/cic_exportation/.depend b/helm/software/components/cic_exportation/.depend index 91be8d88d..288ea5f6c 100644 --- a/helm/software/components/cic_exportation/.depend +++ b/helm/software/components/cic_exportation/.depend @@ -1,3 +1,2 @@ -cicExportation.cmi: cicExportation.cmo: cicExportation.cmi cicExportation.cmx: cicExportation.cmi diff --git a/helm/software/components/cic_proof_checking/.depend b/helm/software/components/cic_proof_checking/.depend index f8a16629e..5d83fd0f3 100644 --- a/helm/software/components/cic_proof_checking/.depend +++ b/helm/software/components/cic_proof_checking/.depend @@ -1,13 +1,3 @@ -cicLogger.cmi: -cicEnvironment.cmi: -cicPp.cmi: -cicUnivUtils.cmi: -cicSubstitution.cmi: -cicMiniReduction.cmi: -cicReduction.cmi: -cicTypeChecker.cmi: -freshNamesGenerator.cmi: -cicDischarge.cmi: cicLogger.cmo: cicLogger.cmi cicLogger.cmx: cicLogger.cmi cicEnvironment.cmo: cicEnvironment.cmi diff --git a/helm/software/components/cic_unification/.depend b/helm/software/components/cic_unification/.depend index 2e054f73d..a7b23ceb4 100644 --- a/helm/software/components/cic_unification/.depend +++ b/helm/software/components/cic_unification/.depend @@ -1,10 +1,3 @@ -cicMetaSubst.cmi: -cicMkImplicit.cmi: -termUtil.cmi: -coercGraph.cmi: -cicUnification.cmi: -cicReplace.cmi: -cicRefine.cmi: cicMetaSubst.cmo: cicMetaSubst.cmi cicMetaSubst.cmx: cicMetaSubst.cmi cicMkImplicit.cmo: cicMkImplicit.cmi diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend index 8d74439eb..6dd0e78a1 100644 --- a/helm/software/components/content_pres/.depend +++ b/helm/software/components/content_pres/.depend @@ -1,9 +1,3 @@ -renderingAttrs.cmi: -cicNotationLexer.cmi: -cicNotationParser.cmi: -mpresentation.cmi: -box.cmi: -content2presMatcher.cmi: termContentPres.cmi: cicNotationParser.cmi boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi cicNotationPres.cmi: mpresentation.cmi box.cmi diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 9c389467c..c88f87535 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -136,7 +136,8 @@ let rec justification ~for_rewriting_step ~ignore_atoms term2pres p = make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in [B.H([], - (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by")):: + (*(if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::*) + (B.b_kw "by"):: B.b_space:: B.Text([],"(")::pres_args@[B.Text([],")")])], None else diff --git a/helm/software/components/disambiguation/.depend b/helm/software/components/disambiguation/.depend index 9fdbeeeaf..aba9ffea7 100644 --- a/helm/software/components/disambiguation/.depend +++ b/helm/software/components/disambiguation/.depend @@ -1,4 +1,3 @@ -disambiguateTypes.cmi: disambiguate.cmi: disambiguateTypes.cmi multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi disambiguateTypes.cmo: disambiguateTypes.cmi diff --git a/helm/software/components/extlib/.depend b/helm/software/components/extlib/.depend index dcc6377a0..201cd0cba 100644 --- a/helm/software/components/extlib/.depend +++ b/helm/software/components/extlib/.depend @@ -1,13 +1,3 @@ -componentsConf.cmi: -hExtlib.cmi: -hMarshal.cmi: -patternMatcher.cmi: -hLog.cmi: -trie.cmi: -discrimination_tree.cmi: -hTopoSort.cmi: -refCounter.cmi: -graphvizPp.cmi: componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi hExtlib.cmo: hExtlib.cmi diff --git a/helm/software/components/getter/.depend b/helm/software/components/getter/.depend index ca64d8ec0..20f69cf0c 100644 --- a/helm/software/components/getter/.depend +++ b/helm/software/components/getter/.depend @@ -1,13 +1,6 @@ -http_getter_wget.cmi: -http_getter_logger.cmi: -http_getter_misc.cmi: -http_getter_const.cmi: http_getter_env.cmi: http_getter_types.cmo -http_getter_storage.cmi: http_getter_common.cmi: http_getter_types.cmo http_getter.cmi: http_getter_types.cmo -http_getter_types.cmo: -http_getter_types.cmx: http_getter_wget.cmo: http_getter_types.cmo http_getter_wget.cmi http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi http_getter_logger.cmo: http_getter_logger.cmi diff --git a/helm/software/components/getter/http_getter_wget.ml b/helm/software/components/getter/http_getter_wget.ml index 90e60b404..571479d78 100644 --- a/helm/software/components/getter/http_getter_wget.ml +++ b/helm/software/components/getter/http_getter_wget.ml @@ -68,5 +68,6 @@ let exists url = true with Http_user_agent.Http_error _ -> false - | Not_found -> prerr_endline "An object has metadata but no XML. This is an internal bug of ocaml-http: Zack, please fix it!"; assert false + | Not_found -> prerr_endline (Printf.sprintf "An object %s has metadata but no XML. This is an internal bug of ocaml-http: Zack, please fix it!" + url); assert false diff --git a/helm/software/components/grafite/.depend b/helm/software/components/grafite/.depend index f305b1580..dc225e221 100644 --- a/helm/software/components/grafite/.depend +++ b/helm/software/components/grafite/.depend @@ -1,7 +1,5 @@ grafiteAstPp.cmi: grafiteAst.cmo grafiteMarshal.cmi: grafiteAst.cmo -grafiteAst.cmo: -grafiteAst.cmx: grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmo grafiteMarshal.cmi diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 8fc37e4c5..86e657b6b 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -197,7 +197,7 @@ type nmacro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 28 +let magic = 30 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) @@ -220,6 +220,7 @@ type ('term,'obj) command = type ncommand = | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *) | NObj of loc * CicNotationPt.term CicNotationPt.obj + | NInverter of loc * string * CicNotationPt.term | NUnivConstraint of loc * NUri.uri * NUri.uri | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list | NCoercion of loc * string * diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 76651753f..8cb7538ba 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -371,6 +371,7 @@ let pp_coercion ~term_pp t do_composites arity saturations= let pp_ncommand = function | UnificationHint (_,t, n) -> "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t + | NInverter (_,_,_) | NObj (_,_) | NUnivConstraint (_) -> "not supported" | NCoercion (_) -> "not supported" diff --git a/helm/software/components/grafite_engine/.depend b/helm/software/components/grafite_engine/.depend index 10236823a..a545f14e3 100644 --- a/helm/software/components/grafite_engine/.depend +++ b/helm/software/components/grafite_engine/.depend @@ -1,4 +1,3 @@ -grafiteTypes.cmi: grafiteSync.cmi: grafiteTypes.cmi nCicCoercDeclaration.cmi: grafiteTypes.cmi grafiteEngine.cmi: grafiteTypes.cmi diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 482a138a6..0806057ec 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -861,6 +861,27 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | _ -> status,`New []) + | GrafiteAst.NInverter (loc, name, indty) -> + if status#ng_mode <> `CommandMode then + raise (GrafiteTypes.Command_error "Not in command mode") + else + let status = status#set_ng_mode `ProofMode in + let metasenv,subst,status,indty = + GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in + let _,leftno,tys,_,_ = match indty with + NCic.Const r -> NCicEnvironment.get_checked_indtys r + | _ -> assert false in + let it = match tys with + hd::tl -> hd + | _ -> assert false + in + let status,obj = + NInversion.mk_inverter name it leftno status status#baseuri in + let _,_,menv,_,_ = obj in + (match menv with + [] -> + eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + | _ -> assert false) | GrafiteAst.NUnivConstraint (loc,u1,u2) -> eval_add_constraint status [`Type,u1] [`Type,u2] ;; diff --git a/helm/software/components/grafite_engine/grafiteEngine.mli b/helm/software/components/grafite_engine/grafiteEngine.mli index 6993afcb2..0b263157f 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.mli +++ b/helm/software/components/grafite_engine/grafiteEngine.mli @@ -31,7 +31,7 @@ exception Macro of exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a - + val eval_ast : disambiguate_tactic: (GrafiteTypes.status -> @@ -57,4 +57,3 @@ val eval_ast : disambiguator_input -> (* the new status and generated objects, if any *) GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] - diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend index 2766b04d0..97bf4d7c2 100644 --- a/helm/software/components/grafite_parser/.depend +++ b/helm/software/components/grafite_parser/.depend @@ -1,9 +1,4 @@ -dependenciesParser.cmi: -grafiteParser.cmi: -cicNotation2.cmi: -nEstatus.cmi: grafiteDisambiguate.cmi: nEstatus.cmi -print_grammar.cmi: dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 52f151fc2..8a418200d 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -803,6 +803,8 @@ EXTEND G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body)) | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term -> G.NObj (loc, N.Theorem (`Axiom, name, typ, None)) + | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = term -> + G.NInverter (loc,name,indty) | NLETCOREC ; defs = let_defs -> nmk_rec_corec `CoInductive defs loc | NLETREC ; defs = let_defs -> diff --git a/helm/software/components/hgdome/.depend b/helm/software/components/hgdome/.depend index 072d9697a..bf9c09af7 100644 --- a/helm/software/components/hgdome/.depend +++ b/helm/software/components/hgdome/.depend @@ -1,5 +1,3 @@ -domMisc.cmi: -xml2Gdome.cmi: domMisc.cmo: domMisc.cmi domMisc.cmx: domMisc.cmi xml2Gdome.cmo: xml2Gdome.cmi diff --git a/helm/software/components/hmysql/.depend b/helm/software/components/hmysql/.depend index ce439d961..16e6e9da7 100644 --- a/helm/software/components/hmysql/.depend +++ b/helm/software/components/hmysql/.depend @@ -1,7 +1,2 @@ -hSql.cmi: -hSqlite3.cmo: -hSqlite3.cmx: -hMysql.cmo: -hMysql.cmx: hSql.cmo: hSqlite3.cmo hMysql.cmo hSql.cmi hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi diff --git a/helm/software/components/lexicon/.depend b/helm/software/components/lexicon/.depend index 16c114516..847a4a807 100644 --- a/helm/software/components/lexicon/.depend +++ b/helm/software/components/lexicon/.depend @@ -3,8 +3,6 @@ lexiconMarshal.cmi: lexiconAst.cmo cicNotation.cmi: lexiconAst.cmo lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmo -lexiconAst.cmo: -lexiconAst.cmx: lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi diff --git a/helm/software/components/library/.depend b/helm/software/components/library/.depend index cfa1295ed..a9f24f814 100644 --- a/helm/software/components/library/.depend +++ b/helm/software/components/library/.depend @@ -1,13 +1,4 @@ -librarian.cmi: -libraryMisc.cmi: -libraryDb.cmi: -coercDb.cmi: cicCoercion.cmi: coercDb.cmi -librarySync.cmi: -cicElim.cmi: -cicRecord.cmi: -cicFix.cmi: -libraryClean.cmi: librarian.cmo: librarian.cmi librarian.cmx: librarian.cmi libraryMisc.cmo: libraryMisc.cmi diff --git a/helm/software/components/logger/.depend b/helm/software/components/logger/.depend index dfb4400ff..28268d29e 100644 --- a/helm/software/components/logger/.depend +++ b/helm/software/components/logger/.depend @@ -1,3 +1,2 @@ -helmLogger.cmi: helmLogger.cmo: helmLogger.cmi helmLogger.cmx: helmLogger.cmi diff --git a/helm/software/components/metadata/.depend b/helm/software/components/metadata/.depend index 78cd97a0d..492a34e3a 100644 --- a/helm/software/components/metadata/.depend +++ b/helm/software/components/metadata/.depend @@ -1,5 +1,3 @@ -sqlStatements.cmi: -metadataTypes.cmi: metadataExtractor.cmi: metadataTypes.cmi metadataPp.cmi: metadataTypes.cmi metadataConstraints.cmi: metadataTypes.cmi diff --git a/helm/software/components/ng_cic_content/.depend b/helm/software/components/ng_cic_content/.depend index 1316c8eab..b4e17fa99 100644 --- a/helm/software/components/ng_cic_content/.depend +++ b/helm/software/components/ng_cic_content/.depend @@ -1,5 +1,3 @@ -ncic2astMatcher.cmi: -nTermCicContent.cmi: ncic2astMatcher.cmo: ncic2astMatcher.cmi ncic2astMatcher.cmx: ncic2astMatcher.cmi nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi diff --git a/helm/software/components/ng_disambiguation/.depend b/helm/software/components/ng_disambiguation/.depend index 2de54dc5e..6b4ef95c1 100644 --- a/helm/software/components/ng_disambiguation/.depend +++ b/helm/software/components/ng_disambiguation/.depend @@ -1,3 +1,2 @@ -nCicDisambiguate.cmi: nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 4ea6e5ac3..ff74d233a 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -331,6 +331,7 @@ let interpretate_term_and_interpretate_term_option | CicNotationPt.NRef nref -> NCic.Const nref | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term + | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s) | CicNotationPt.UserInput -> NCic.Implicit `Hole | CicNotationPt.Num (num, i) -> Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num) diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index a41138342..4b11d9af6 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,4 +1,3 @@ -nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index f39cf868e..fead92210 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -22,7 +22,8 @@ type universe = (univ_algebra * NUri.uri) list type sort = Prop | Type of universe type implicit_annotation = - [ `Closed | `Type | `Hole | `Term | `Typeof of int | `Vector ] + [ `Closed | `Type | `Hole | `Tagged of string | `Term | `Typeof of int | `Vector ] + type lc_kind = Irl of int | Ctx of term list diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 12227b4b1..ddecb4dfb 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -57,6 +57,7 @@ let string_of_implicit_annotation = function | `Closed -> "▪" | `Type -> "" | `Hole -> "□" + | `Tagged s -> "[\"" ^ s ^ "\"]" | `Term -> "Term" | `Typeof x -> "Ty("^string_of_int x^")" | `Vector -> "…" diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 369ed6b69..3ace51014 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,4 +1,3 @@ -terms.cmi: pp.cmi: terms.cmi foSubst.cmi: terms.cmi orderings.cmi: terms.cmi @@ -11,7 +10,6 @@ paramod.cmi: terms.cmi orderings.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi nCicProof.cmi: terms.cmi -nCicParamod.cmi: terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: terms.cmi pp.cmi diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index dc9a46fb3..f30b906fd 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,8 +1,5 @@ -nDiscriminationTree.cmi: -nCicMetaSubst.cmi: -nCicUnifHint.cmi: nCicCoercion.cmi: nCicUnifHint.cmi -nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi +nRstatus.cmi: nCicCoercion.cmi nCicUnification.cmi: nRstatus.cmi nCicRefiner.cmi: nRstatus.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi @@ -15,12 +12,10 @@ nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \ nCicCoercion.cmi nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ nCicCoercion.cmi -nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi -nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi -nCicUnification.cmo: nRstatus.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \ - nCicCoercion.cmi nCicUnification.cmi -nCicUnification.cmx: nRstatus.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicUnification.cmi +nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi +nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi +nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi +nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicCoercion.cmi \ nCicRefiner.cmi nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicCoercion.cmx \ diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 6664a5b97..03de06d1c 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -42,6 +42,7 @@ let exp_implicit ~localise metasenv context expty t = | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term) | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type) | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term) + | `Tagged s -> NCicMetaSubst.mk_meta ~name:s metasenv context (foo `Term) | `Vector -> raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^ "can only be used in argument position"))) diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index 7c97b8cfa..0be1ac3f0 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,7 +1,5 @@ -nCicTacReduction.cmi: -nTacStatus.cmi: -nCicElim.cmi: nTactics.cmi: nTacStatus.cmi +nInversion.cmi: nTacStatus.cmi nCicTacReduction.cmo: nCicTacReduction.cmi nCicTacReduction.cmx: nCicTacReduction.cmi nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi @@ -10,3 +8,5 @@ nCicElim.cmo: nCicElim.cmi nCicElim.cmx: nCicElim.cmi nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi +nInversion.cmo: nTactics.cmi nInversion.cmi +nInversion.cmx: nTactics.cmx nInversion.cmi diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile index e5a613439..e99dd2422 100644 --- a/helm/software/components/ng_tactics/Makefile +++ b/helm/software/components/ng_tactics/Makefile @@ -4,7 +4,8 @@ INTERFACE_FILES = \ nCicTacReduction.mli \ nTacStatus.mli \ nCicElim.mli \ - nTactics.mli + nTactics.mli \ + nInversion.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml new file mode 100644 index 000000000..366697ece --- /dev/null +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -0,0 +1,196 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +let fresh_name = + let i = ref 0 in + function () -> + incr i; + "z" ^ string_of_int !i +;; + +let mk_id id = + let id = if id = "_" then fresh_name () else id in + CicNotationPt.Ident (id,None) +;; + +let rec split_arity ~subst context te = + match NCicReduction.whd ~subst context te with + | NCic.Prod (name,so,ta) -> + split_arity ~subst ((name, (NCic.Decl so))::context) ta + | t -> context, t +;; + +let mk_appl = + function + [] -> assert false + | [x] -> x + | l -> CicNotationPt.Appl l +;; + +let rec mk_prods l t = + match l with + [] -> t + | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t) +;; + +let rec mk_lambdas l t = + match l with + [] -> t + | hd::tl -> CicNotationPt.Binder (`Lambda, (mk_id hd, None), mk_lambdas tl t) +;; + +let rec mk_arrows l t = + match l with + [] -> t + | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id "_", Some hd), mk_arrows tl t) +;; + +let subst_metasenv_and_fix_names status = + let u,h,metasenv, subst,o = status#obj in + let o = + NCicUntrusted.map_obj_kind ~skip_body:true + (NCicUntrusted.apply_subst subst []) o + in + status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) +;; + +let mk_inverter name it leftno status baseuri = + prerr_endline ("leftno = " ^ string_of_int leftno); + let _,ind_name,ty,cl = it in + prerr_endline ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty); + let ncons = List.length cl in + (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in + let params = List.rev_map (function name,_ -> mk_id name) params in + prerr_endline ("lunghezza params = " ^ string_of_int (List.length params));*) + let args,sort = split_arity ~subst:[] [] ty in + prerr_endline ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort); + (*let args = List.rev_map (function name,_ -> mk_id name) args in + prerr_endline ("lunghezza args = " ^ string_of_int (List.length args));*) + let nparams = List.length args in + prerr_endline ("nparams = " ^ string_of_int nparams); + + let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in + prerr_endline ("lunghezza xs = " ^ string_of_int (List.length xs)); + let ls, rs = HExtlib.split_nth leftno xs in + prerr_endline ("lunghezza ls = " ^ string_of_int (List.length ls)); + prerr_endline ("lunghezza rs = " ^ string_of_int (List.length rs)); + let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in + + let id_xs = List.map mk_id xs in + let id_ls = List.map mk_id ls in + let id_rs = List.map mk_id rs in + let id_ys = List.map mk_id ys in + + (* pseudocode let t = Lambda y1 ... yr. xs_ = ys_ -> pred *) + + (* check: assuming we have more than one right parameter *) + (* pred := P yr- *) + let pred = mk_appl ((mk_id "P")::id_ys) in + + let selection = HExtlib.mk_list true (List.length ys) in + let prods = + let rec prodaux = function + [],[],[] -> pred + | false :: l,x::xs,y::ys -> prodaux (l,xs,ys) + | true :: l,x::xs,y::ys -> + CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])), + prodaux (l,xs,ys)) + | _ -> assert false + in prodaux (selection,id_rs,id_ys) + in + + let lambdas = mk_lambdas (ys@["p"]) prods in + + let hyplist = + let rec hypaux k = function + 0 -> [] + | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1) + in (hypaux 1 ncons) + in + prerr_endline ("lunghezza ys = " ^ string_of_int (List.length ys)); + let theorem = mk_prods xs + (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort `Prop))), + mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *) + Some (CicNotationPt.Implicit `JustOne)), + mk_appl (mk_id "P"::id_rs))))) + in + let t = mk_appl ( [mk_id (ind_name ^ "_ind"); lambdas] @ + List.map mk_id hyplist @ + CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in + + prerr_endline ("NINVERTER 0"); + let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri + (baseuri ^ name ^ ".def", + 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some (CicNotationPt.Implicit (`Tagged "inv")))) in + prerr_endline ("NINVERTER 1"); + let uri,height,nmenv,nsubst,nobj = theorem in + let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in + let status = status#set_obj theorem in + let status = status#set_stack ninitial_stack in + let status = subst_metasenv_and_fix_names status in + + let cut_theorem = + mk_arrows (List.map + (fun x -> let x = mk_id x in mk_appl [mk_id "eq"; + CicNotationPt.Implicit `JustOne; + x;x]) rs) (mk_appl (mk_id "P"::List.map mk_id rs)) in + let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem), + CicNotationPt.Implicit (`Tagged "end")); + CicNotationPt.Implicit (`Tagged "cut")] in + + let intros = List.map (fun x -> NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in + (*let branches = + let rec branch_aux k = function + 0 -> [NTactics.apply_tac ("",0,mk_id "H")] + | n -> NTactics.apply_tac ("",0,mk_id ("H"^(string_of_int k)))::(branch_aux (k+1) (n-1)) + in branch_aux 1 ncons + in*) + + let status = NTactics.block_tac + (NTactics.branch_tac:: + NTactics.case_tac "inv":: + (intros @ + [NTactics.apply_tac ("",0,cut); + NTactics.branch_tac; + NTactics.case_tac "end"; + (*NTactics.intro_tac "Hcut";*) + NTactics.apply_tac ("",0,mk_id "Hcut"); + NTactics.apply_tac ("",0,mk_id "refl_eq"); + NTactics.shift_tac; + NTactics.case_tac "cut"; + NTactics.apply_tac ("",0,t); + (* NTactics.branch_tac] + @ branches @ + [NTactics.merge_tac; *) + NTactics.merge_tac; + NTactics.merge_tac; + NTactics.skip_tac])) status in + status,status#obj +;; + + +let ast_of_sort s = + match s with + NCic.Prop -> `Prop,"ind" + | NCic.Type u -> + let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in + (try + if String.sub u 0 4 = "Type" then + `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u + else if String.sub u 0 5 = "CProp" then + `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u + else + (prerr_endline u; + assert false) + with Failure _ -> assert false) +;; diff --git a/helm/software/components/ng_tactics/nInversion.mli b/helm/software/components/ng_tactics/nInversion.mli new file mode 100644 index 000000000..4d6de91ed --- /dev/null +++ b/helm/software/components/ng_tactics/nInversion.mli @@ -0,0 +1,15 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +val mk_inverter: string -> NCic.inductiveType -> int -> (#NTacStatus.tac_status as 's) -> string -> 's * NCic.obj + diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 01a57f0c4..8887175b4 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -87,6 +87,25 @@ let pos_tac i_s status = status#set_stack gstatus ;; +let case_tac lab status = + let gstatus = + match status#stack with + | [] -> assert false + | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + when is_fresh loc -> + let l_js = List.filter + (fun curloc -> + let _,_,metasenv,_,_ = status#obj in + match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with + Some s,_,_ when s = lab -> true + | _ -> false) ([loc] @+ g') in + ((l_js, t , [],`BranchTag) + :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + | _ -> fail (lazy "can't use relative positioning here") + in + status#set_stack gstatus +;; + let wildcard_tac status = let gstatus = match status#stack with diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 9afd918ea..8211adb37 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -15,6 +15,7 @@ val dot_tac: 's NTacStatus.tactic val branch_tac: 's NTacStatus.tactic val shift_tac: 's NTacStatus.tactic val pos_tac: int list -> 's NTacStatus.tactic +val case_tac: string -> 's NTacStatus.tactic val wildcard_tac: 's NTacStatus.tactic val merge_tac: 's NTacStatus.tactic val focus_tac: int list -> 's NTacStatus.tactic diff --git a/helm/software/components/registry/.depend b/helm/software/components/registry/.depend index 40c03891a..cf4f36b68 100644 --- a/helm/software/components/registry/.depend +++ b/helm/software/components/registry/.depend @@ -1,3 +1,2 @@ -helm_registry.cmi: helm_registry.cmo: helm_registry.cmi helm_registry.cmx: helm_registry.cmi diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index d9d6034a1..169fc76b0 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -1,19 +1,11 @@ -proofEngineTypes.cmi: proofEngineHelpers.cmi: proofEngineTypes.cmi -proofEngineReduction.cmi: continuationals.cmi: proofEngineTypes.cmi tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi -hashtbl_equiv.cmi: metadataQuery.cmi: proofEngineTypes.cmi -universe.cmi: autoTypes.cmi: proofEngineTypes.cmi -autoCache.cmi: -paramodulation/utils.cmi: -closeCoercionGraph.cmi: -paramodulation/subst.cmi: paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/founif.cmi: paramodulation/subst.cmi @@ -35,13 +27,10 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: proofEngineTypes.cmi automationCache.cmi destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi -inversion_principle.cmi: ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi -fourier.cmi: fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi -history.cmi: statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index 310cf42ef..4d143fd2a 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Apr 28 17:14:45 CEST 2009 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Mon May 18 11:04:27 CEST 2009 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyP : term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/software/components/thread/.depend b/helm/software/components/thread/.depend index 6616a03d0..7759190c6 100644 --- a/helm/software/components/thread/.depend +++ b/helm/software/components/thread/.depend @@ -1,5 +1,3 @@ -threadSafe.cmi: -extThread.cmi: threadSafe.cmo: threadSafe.cmi threadSafe.cmx: threadSafe.cmi extThread.cmo: extThread.cmi diff --git a/helm/software/components/tptp_grafite/.depend b/helm/software/components/tptp_grafite/.depend index a8972f4cf..bc310327f 100644 --- a/helm/software/components/tptp_grafite/.depend +++ b/helm/software/components/tptp_grafite/.depend @@ -1,7 +1,4 @@ parser.cmi: ast.cmo -tptp2grafite.cmi: -ast.cmo: -ast.cmx: lexer.cmo: parser.cmi lexer.cmx: parser.cmx parser.cmo: ast.cmo parser.cmi diff --git a/helm/software/components/urimanager/.depend b/helm/software/components/urimanager/.depend index 9cac9aa78..482148423 100644 --- a/helm/software/components/urimanager/.depend +++ b/helm/software/components/urimanager/.depend @@ -1,3 +1,2 @@ -uriManager.cmi: uriManager.cmo: uriManager.cmi uriManager.cmx: uriManager.cmi diff --git a/helm/software/components/whelp/.depend b/helm/software/components/whelp/.depend index 65dc07955..39f37dfa9 100644 --- a/helm/software/components/whelp/.depend +++ b/helm/software/components/whelp/.depend @@ -1,5 +1,3 @@ -whelp.cmi: -fwdQueries.cmi: whelp.cmo: whelp.cmi whelp.cmx: whelp.cmi fwdQueries.cmo: fwdQueries.cmi diff --git a/helm/software/components/xml/.depend b/helm/software/components/xml/.depend index e7e7ffbd7..5ef59bdc9 100644 --- a/helm/software/components/xml/.depend +++ b/helm/software/components/xml/.depend @@ -1,5 +1,3 @@ -xml.cmi: -xmlPushParser.cmi: xml.cmo: xml.cmi xml.cmx: xml.cmi xmlPushParser.cmo: xmlPushParser.cmi diff --git a/helm/software/components/xmldiff/.depend b/helm/software/components/xmldiff/.depend index 65bd7b949..e2832de33 100644 --- a/helm/software/components/xmldiff/.depend +++ b/helm/software/components/xmldiff/.depend @@ -1,3 +1,2 @@ -xmlDiff.cmi: xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi -- 2.39.2