From da5dd88bbcc43d9f4342e47c922b820abf91c92f Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 2 Oct 2009 14:50:12 +0000 Subject: [PATCH] Updated command ninverter. Syntax: ninverter for [] [: ] It is the same as the previous inverter except that: - is now optional (when it is omitted, every index is selected) - the user is allowed to specify a (when it is omitted, ninverter defaults to Prop, as it was the case for inverter) --- helm/software/components/acic_content/.depend | 3 - .../components/acic_content/.depend.opt | 3 - .../components/acic_procedural/.depend | 7 -- .../components/acic_procedural/.depend.opt | 7 -- .../components/binaries/extractor/.depend | 4 - .../components/binaries/extractor/.depend.opt | 4 - .../components/binaries/table_creator/.depend | 2 - .../binaries/table_creator/.depend.opt | 2 - helm/software/components/cic/.depend | 2 - helm/software/components/cic/.depend.opt | 2 - helm/software/components/cic_acic/.depend | 3 - helm/software/components/cic_acic/.depend.opt | 3 - .../components/cic_disambiguation/.depend | 2 - .../components/cic_disambiguation/.depend.opt | 2 - .../components/cic_exportation/.depend | 1 - .../components/cic_exportation/.depend.opt | 1 - .../components/cic_proof_checking/.depend | 10 --- .../components/cic_proof_checking/.depend.opt | 10 --- .../components/cic_unification/.depend | 7 -- .../components/cic_unification/.depend.opt | 7 -- helm/software/components/content_pres/.depend | 6 -- .../components/content_pres/.depend.opt | 6 -- .../components/disambiguation/.depend | 1 - .../components/disambiguation/.depend.opt | 1 - helm/software/components/extlib/.depend | 10 --- helm/software/components/extlib/.depend.opt | 10 --- helm/software/components/getter/.depend | 7 -- helm/software/components/getter/.depend.opt | 7 -- helm/software/components/grafite/.depend | 2 - helm/software/components/grafite/.depend.opt | 2 - .../software/components/grafite/grafiteAst.ml | 2 +- .../components/grafite/grafiteAstPp.ml | 2 +- .../components/grafite_engine/.depend | 1 - .../components/grafite_engine/.depend.opt | 1 - .../grafite_engine/grafiteEngine.ml | 32 +++++--- .../components/grafite_parser/.depend | 5 -- .../components/grafite_parser/.depend.opt | 5 -- .../grafite_parser/grafiteParser.ml | 6 +- helm/software/components/hgdome/.depend | 2 - helm/software/components/hgdome/.depend.opt | 2 - helm/software/components/hmysql/.depend | 5 -- helm/software/components/hmysql/.depend.opt | 5 -- helm/software/components/lexicon/.depend | 2 - helm/software/components/lexicon/.depend.opt | 2 - helm/software/components/library/.depend | 9 --- helm/software/components/library/.depend.opt | 9 --- helm/software/components/logger/.depend | 1 - helm/software/components/logger/.depend.opt | 1 - helm/software/components/metadata/.depend | 2 - helm/software/components/metadata/.depend.opt | 2 - .../components/ng_cic_content/.depend | 2 - .../components/ng_cic_content/.depend.opt | 2 - .../components/ng_disambiguation/.depend | 1 - .../components/ng_disambiguation/.depend.opt | 1 - helm/software/components/ng_kernel/.depend | 1 - .../software/components/ng_kernel/.depend.opt | 1 - .../components/ng_paramodulation/.depend | 2 - .../components/ng_paramodulation/.depend.opt | 2 - helm/software/components/ng_refiner/.depend | 3 - .../components/ng_refiner/.depend.opt | 3 - helm/software/components/ng_tactics/.depend | 7 +- .../components/ng_tactics/.depend.opt | 7 +- .../components/ng_tactics/nInversion.ml | 74 ++++++------------- .../components/ng_tactics/nInversion.mli | 5 +- helm/software/components/registry/.depend | 1 - helm/software/components/registry/.depend.opt | 1 - .../components/syntax_extensions/.depend | 3 - .../components/syntax_extensions/.depend.opt | 3 - helm/software/components/tactics/.depend | 11 --- helm/software/components/tactics/.depend.opt | 11 --- helm/software/components/thread/.depend | 2 - helm/software/components/thread/.depend.opt | 2 - helm/software/components/tptp_grafite/.depend | 3 - .../components/tptp_grafite/.depend.opt | 3 - helm/software/components/urimanager/.depend | 1 - .../components/urimanager/.depend.opt | 1 - helm/software/components/whelp/.depend | 2 - helm/software/components/whelp/.depend.opt | 2 - helm/software/components/xml/.depend | 2 - helm/software/components/xml/.depend.opt | 2 - helm/software/components/xmldiff/.depend | 1 - helm/software/components/xmldiff/.depend.opt | 1 - 82 files changed, 56 insertions(+), 337 deletions(-) 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/.depend.opt b/helm/software/components/acic_content/.depend.opt index 307fceaa0..fef879256 100644 --- a/helm/software/components/acic_content/.depend.opt +++ b/helm/software/components/acic_content/.depend.opt @@ -1,4 +1,3 @@ -content.cmi: acic2content.cmi: content.cmi content2cic.cmi: content.cmi cicNotationUtil.cmi: cicNotationPt.cmx @@ -6,8 +5,6 @@ cicNotationEnv.cmi: cicNotationPt.cmx cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi acic2astMatcher.cmi: cicNotationPt.cmx termAcicContent.cmi: cicNotationPt.cmx -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_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/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index 97238c4d8..8d0128744 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/components/acic_procedural/.depend.opt @@ -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/extractor/.depend.opt b/helm/software/components/binaries/extractor/.depend.opt index 0c39328ae..e69de29bb 100644 --- a/helm/software/components/binaries/extractor/.depend.opt +++ b/helm/software/components/binaries/extractor/.depend.opt @@ -1,4 +0,0 @@ -extractor.cmo: -extractor.cmx: -extractor_manager.cmo: -extractor_manager.cmx: 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/table_creator/.depend.opt b/helm/software/components/binaries/table_creator/.depend.opt index 33147b949..e69de29bb 100644 --- a/helm/software/components/binaries/table_creator/.depend.opt +++ b/helm/software/components/binaries/table_creator/.depend.opt @@ -1,2 +0,0 @@ -table_creator.cmo: -table_creator.cmx: 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/.depend.opt b/helm/software/components/cic/.depend.opt index 8cdd2a86a..76d19c1ff 100644 --- a/helm/software/components/cic/.depend.opt +++ b/helm/software/components/cic/.depend.opt @@ -1,10 +1,8 @@ -cicUniv.cmi: unshare.cmi: cic.cmx deannotate.cmi: cic.cmx cicParser.cmi: cic.cmx cicUtil.cmi: cic.cmx helmLibraryObjects.cmi: cic.cmx -libraryObjects.cmi: cic_indexable.cmi: cic.cmx path_indexing.cmi: cic.cmx cicInspect.cmi: cic.cmx 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_acic/.depend.opt b/helm/software/components/cic_acic/.depend.opt index 5449d50aa..3fc1e0dce 100644 --- a/helm/software/components/cic_acic/.depend.opt +++ b/helm/software/components/cic_acic/.depend.opt @@ -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/.depend.opt b/helm/software/components/cic_disambiguation/.depend.opt index a9ae65a5e..e9bd1168f 100644 --- a/helm/software/components/cic_disambiguation/.depend.opt +++ b/helm/software/components/cic_disambiguation/.depend.opt @@ -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_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_exportation/.depend.opt b/helm/software/components/cic_exportation/.depend.opt index 91be8d88d..288ea5f6c 100644 --- a/helm/software/components/cic_exportation/.depend.opt +++ b/helm/software/components/cic_exportation/.depend.opt @@ -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_proof_checking/.depend.opt b/helm/software/components/cic_proof_checking/.depend.opt index f8a16629e..5d83fd0f3 100644 --- a/helm/software/components/cic_proof_checking/.depend.opt +++ b/helm/software/components/cic_proof_checking/.depend.opt @@ -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/cic_unification/.depend.opt b/helm/software/components/cic_unification/.depend.opt index 2e054f73d..a7b23ceb4 100644 --- a/helm/software/components/cic_unification/.depend.opt +++ b/helm/software/components/cic_unification/.depend.opt @@ -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/.depend.opt b/helm/software/components/content_pres/.depend.opt index 8d74439eb..6dd0e78a1 100644 --- a/helm/software/components/content_pres/.depend.opt +++ b/helm/software/components/content_pres/.depend.opt @@ -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/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/disambiguation/.depend.opt b/helm/software/components/disambiguation/.depend.opt index 9fdbeeeaf..aba9ffea7 100644 --- a/helm/software/components/disambiguation/.depend.opt +++ b/helm/software/components/disambiguation/.depend.opt @@ -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/extlib/.depend.opt b/helm/software/components/extlib/.depend.opt index dcc6377a0..201cd0cba 100644 --- a/helm/software/components/extlib/.depend.opt +++ b/helm/software/components/extlib/.depend.opt @@ -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/.depend.opt b/helm/software/components/getter/.depend.opt index 64da37f13..554fb1ec7 100644 --- a/helm/software/components/getter/.depend.opt +++ b/helm/software/components/getter/.depend.opt @@ -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.cmx -http_getter_storage.cmi: http_getter_common.cmi: http_getter_types.cmx http_getter.cmi: http_getter_types.cmx -http_getter_types.cmo: -http_getter_types.cmx: http_getter_wget.cmo: http_getter_types.cmx 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/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/.depend.opt b/helm/software/components/grafite/.depend.opt index e01d5bbfa..0f64ba789 100644 --- a/helm/software/components/grafite/.depend.opt +++ b/helm/software/components/grafite/.depend.opt @@ -1,7 +1,5 @@ grafiteAstPp.cmi: grafiteAst.cmx grafiteMarshal.cmi: grafiteAst.cmx -grafiteAst.cmo: -grafiteAst.cmx: grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 86e657b6b..0cfdef148 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -220,7 +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 + | NInverter of loc * string * CicNotationPt.term * bool list option * CicNotationPt.term option | 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 8cb7538ba..83f3a36b6 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -371,7 +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 (_,_,_) + | 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/.depend.opt b/helm/software/components/grafite_engine/.depend.opt index 10236823a..a545f14e3 100644 --- a/helm/software/components/grafite_engine/.depend.opt +++ b/helm/software/components/grafite_engine/.depend.opt @@ -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 0806057ec..494701d2d 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -861,22 +861,32 @@ 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) -> + | GrafiteAst.NInverter (loc, name, indty, selection, sort) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else + let metasenv,subst,status,sort = match sort with + | None -> [],[],status,NCic.Sort NCic.Prop + | Some s -> GrafiteDisambiguate.disambiguate_nterm None status [] [] [] + (text,prefix_len,s) + in + assert (metasenv = []); + let sort = NCicReduction.whd ~subst [] sort in + let sort = match sort with + NCic.Sort s -> s + | _ -> raise (Invalid_argument (Printf.sprintf "ninverter: found target %s, which is not a sort" + (NCicPp.ppterm ~metasenv ~subst ~context:[] sort))) + in 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 + GrafiteDisambiguate.disambiguate_nterm None status [] [] subst (text,prefix_len,indty) in + let indtyno,(_,leftno,tys,_,_) = match indty with + NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) -> + indtyno, NCicEnvironment.get_checked_indtys r + | _ -> prerr_endline ("engine: indty =" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] indty) ; assert false in + let it = List.nth tys indtyno in + let status,obj = NInversion.mk_inverter name it leftno ?selection sort + status status#baseuri in let _,_,menv,_,_ = obj in (match menv with [] -> 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/.depend.opt b/helm/software/components/grafite_parser/.depend.opt index 2766b04d0..97bf4d7c2 100644 --- a/helm/software/components/grafite_parser/.depend.opt +++ b/helm/software/components/grafite_parser/.depend.opt @@ -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 8a418200d..2fbfe4179 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -803,8 +803,10 @@ 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) + | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ; + paramspec = OPT inverter_param_list ; + outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> + G.NInverter (loc,name,indty,paramspec,outsort) | 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/hgdome/.depend.opt b/helm/software/components/hgdome/.depend.opt index 072d9697a..bf9c09af7 100644 --- a/helm/software/components/hgdome/.depend.opt +++ b/helm/software/components/hgdome/.depend.opt @@ -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/hmysql/.depend.opt b/helm/software/components/hmysql/.depend.opt index c2289bff2..602c901b8 100644 --- a/helm/software/components/hmysql/.depend.opt +++ b/helm/software/components/hmysql/.depend.opt @@ -1,7 +1,2 @@ -hSql.cmi: -hSqlite3.cmo: -hSqlite3.cmx: -hMysql.cmo: -hMysql.cmx: hSql.cmo: hSqlite3.cmx hMysql.cmx 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/lexicon/.depend.opt b/helm/software/components/lexicon/.depend.opt index 0fee4b18e..463d8a7bc 100644 --- a/helm/software/components/lexicon/.depend.opt +++ b/helm/software/components/lexicon/.depend.opt @@ -3,8 +3,6 @@ lexiconMarshal.cmi: lexiconAst.cmx cicNotation.cmi: lexiconAst.cmx lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx -lexiconAst.cmo: -lexiconAst.cmx: lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx 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/library/.depend.opt b/helm/software/components/library/.depend.opt index cfa1295ed..a9f24f814 100644 --- a/helm/software/components/library/.depend.opt +++ b/helm/software/components/library/.depend.opt @@ -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/logger/.depend.opt b/helm/software/components/logger/.depend.opt index dfb4400ff..28268d29e 100644 --- a/helm/software/components/logger/.depend.opt +++ b/helm/software/components/logger/.depend.opt @@ -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/metadata/.depend.opt b/helm/software/components/metadata/.depend.opt index 78cd97a0d..492a34e3a 100644 --- a/helm/software/components/metadata/.depend.opt +++ b/helm/software/components/metadata/.depend.opt @@ -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_cic_content/.depend.opt b/helm/software/components/ng_cic_content/.depend.opt index 1316c8eab..b4e17fa99 100644 --- a/helm/software/components/ng_cic_content/.depend.opt +++ b/helm/software/components/ng_cic_content/.depend.opt @@ -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/.depend.opt b/helm/software/components/ng_disambiguation/.depend.opt index 2de54dc5e..6b4ef95c1 100644 --- a/helm/software/components/ng_disambiguation/.depend.opt +++ b/helm/software/components/ng_disambiguation/.depend.opt @@ -1,3 +1,2 @@ -nCicDisambiguate.cmi: nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index aeb011ffc..159cee382 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/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index 332deb32c..01056b468 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -1,4 +1,3 @@ -nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmx nCicSubstitution.cmi: nCic.cmx 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_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt index 369ed6b69..3ace51014 100644 --- a/helm/software/components/ng_paramodulation/.depend.opt +++ b/helm/software/components/ng_paramodulation/.depend.opt @@ -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 db7e52884..f30b906fd 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,6 +1,3 @@ -nDiscriminationTree.cmi: -nCicMetaSubst.cmi: -nCicUnifHint.cmi: nCicCoercion.cmi: nCicUnifHint.cmi nRstatus.cmi: nCicCoercion.cmi nCicUnification.cmi: nRstatus.cmi diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt index db7e52884..f30b906fd 100644 --- a/helm/software/components/ng_refiner/.depend.opt +++ b/helm/software/components/ng_refiner/.depend.opt @@ -1,6 +1,3 @@ -nDiscriminationTree.cmi: -nCicMetaSubst.cmi: -nCicUnifHint.cmi: nCicCoercion.cmi: nCicUnifHint.cmi nRstatus.cmi: nCicCoercion.cmi nCicUnification.cmi: nRstatus.cmi diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index 8d3bcd0c1..86ae2b375 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,6 +1,3 @@ -nCicTacReduction.cmi: -nTacStatus.cmi: -nCicElim.cmi: nTactics.cmi: nTacStatus.cmi nInversion.cmi: nTacStatus.cmi nCicTacReduction.cmo: nCicTacReduction.cmi @@ -11,5 +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 +nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi +nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt index 8d3bcd0c1..86ae2b375 100644 --- a/helm/software/components/ng_tactics/.depend.opt +++ b/helm/software/components/ng_tactics/.depend.opt @@ -1,6 +1,3 @@ -nCicTacReduction.cmi: -nTacStatus.cmi: -nCicElim.cmi: nTactics.cmi: nTacStatus.cmi nInversion.cmi: nTacStatus.cmi nCicTacReduction.cmo: nCicTacReduction.cmi @@ -11,5 +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 +nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi +nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index 366697ece..a93e7f513 100644 --- a/helm/software/components/ng_tactics/nInversion.ml +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -49,10 +49,14 @@ let rec mk_lambdas l 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 rec mk_arrows xs ys selection target = + match selection,xs,ys with + [],[],[] -> target + | false :: l,x::xs,y::ys -> mk_arrows xs ys l target + | true :: l,x::xs,y::ys -> + CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])), + mk_arrows xs ys l target) + | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type") ;; let subst_metasenv_and_fix_names status = @@ -64,7 +68,7 @@ let subst_metasenv_and_fix_names status = status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) ;; -let mk_inverter name it leftno status baseuri = +let mk_inverter name it leftno ?selection outsort 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); @@ -72,13 +76,13 @@ let mk_inverter name it leftno status baseuri = (*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 + 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 @@ -97,17 +101,11 @@ let mk_inverter name it leftno status baseuri = (* 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) + let selection = match selection with + None -> HExtlib.mk_list true (List.length ys) + | Some s -> s in + let prods = mk_arrows id_rs id_ys selection pred in let lambdas = mk_lambdas (ys@["p"]) prods in @@ -118,21 +116,21 @@ let mk_inverter name it leftno status baseuri = in (hypaux 1 ncons) in prerr_endline ("lunghezza ys = " ^ string_of_int (List.length ys)); + + let outsort, suffix = NCicElim.ast_of_sort outsort in let theorem = mk_prods xs - (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort `Prop))), + (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))), 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] @ + let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix); 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 @@ -140,21 +138,14 @@ let mk_inverter name it leftno status baseuri = 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 rs = List.map (fun x -> mk_id x) rs in + mk_arrows rs rs selection (mk_appl (mk_id "P"::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:: @@ -163,34 +154,13 @@ let mk_inverter name it leftno status baseuri = [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 index 4d6de91ed..b5ca8597d 100644 --- a/helm/software/components/ng_tactics/nInversion.mli +++ b/helm/software/components/ng_tactics/nInversion.mli @@ -11,5 +11,6 @@ (* $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 - +val mk_inverter: string -> NCic.inductiveType -> int -> ?selection:bool list -> + NCic.sort -> (#NTacStatus.tac_status as 's) -> string -> + 's * NCic.obj 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/registry/.depend.opt b/helm/software/components/registry/.depend.opt index 40c03891a..cf4f36b68 100644 --- a/helm/software/components/registry/.depend.opt +++ b/helm/software/components/registry/.depend.opt @@ -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/syntax_extensions/.depend.opt b/helm/software/components/syntax_extensions/.depend.opt index 3d7dfc21f..c0cd9c906 100644 --- a/helm/software/components/syntax_extensions/.depend.opt +++ b/helm/software/components/syntax_extensions/.depend.opt @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmx 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/.depend.opt b/helm/software/components/tactics/.depend.opt index d9d6034a1..169fc76b0 100644 --- a/helm/software/components/tactics/.depend.opt +++ b/helm/software/components/tactics/.depend.opt @@ -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/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/thread/.depend.opt b/helm/software/components/thread/.depend.opt index 6616a03d0..7759190c6 100644 --- a/helm/software/components/thread/.depend.opt +++ b/helm/software/components/thread/.depend.opt @@ -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/tptp_grafite/.depend.opt b/helm/software/components/tptp_grafite/.depend.opt index fb60fe8f2..c74300207 100644 --- a/helm/software/components/tptp_grafite/.depend.opt +++ b/helm/software/components/tptp_grafite/.depend.opt @@ -1,7 +1,4 @@ parser.cmi: ast.cmx -tptp2grafite.cmi: -ast.cmo: -ast.cmx: lexer.cmo: parser.cmi lexer.cmx: parser.cmx parser.cmo: ast.cmx 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/urimanager/.depend.opt b/helm/software/components/urimanager/.depend.opt index 9cac9aa78..482148423 100644 --- a/helm/software/components/urimanager/.depend.opt +++ b/helm/software/components/urimanager/.depend.opt @@ -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/whelp/.depend.opt b/helm/software/components/whelp/.depend.opt index 65dc07955..39f37dfa9 100644 --- a/helm/software/components/whelp/.depend.opt +++ b/helm/software/components/whelp/.depend.opt @@ -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/xml/.depend.opt b/helm/software/components/xml/.depend.opt index e7e7ffbd7..5ef59bdc9 100644 --- a/helm/software/components/xml/.depend.opt +++ b/helm/software/components/xml/.depend.opt @@ -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 diff --git a/helm/software/components/xmldiff/.depend.opt b/helm/software/components/xmldiff/.depend.opt index 65bd7b949..e2832de33 100644 --- a/helm/software/components/xmldiff/.depend.opt +++ b/helm/software/components/xmldiff/.depend.opt @@ -1,3 +1,2 @@ -xmlDiff.cmi: xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi -- 2.39.2