From: Claudio Sacerdoti Coen Date: Fri, 27 Sep 2019 14:52:38 +0000 (+0200) Subject: Merge branch 'declarative' into matita-lablgtk3 X-Git-Tag: make_still_working~229^2~1^2~1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5b5dca0c118dfbe3ba8f0514ef07549544eb7810 Merge branch 'declarative' into matita-lablgtk3 --- 5b5dca0c118dfbe3ba8f0514ef07549544eb7810 diff --cc matita/components/content/.depend index e1dff0f85,369dbbdc4..6b7755819 --- a/matita/components/content/.depend +++ b/matita/components/content/.depend @@@ -1,14 -1,14 +1,36 @@@ - content.cmo : content.cmi - content.cmx : content.cmi ++content.cmo : \ ++ content.cmi ++content.cmx : \ ++ content.cmi content.cmi : - notationEnv.cmo : notationUtil.cmi notationPt.cmo notationEnv.cmi - notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi -notationUtil.cmi : notationPt.cmo --notationEnv.cmi : notationPt.cmo - notationPp.cmo : notationPt.cmo notationEnv.cmi notationPp.cmi - notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi --notationPp.cmi : notationPt.cmo notationEnv.cmi ++notationEnv.cmo : \ ++ notationUtil.cmi \ ++ notationPt.cmo \ ++ notationEnv.cmi ++notationEnv.cmx : \ ++ notationUtil.cmx \ ++ notationPt.cmx \ ++ notationEnv.cmi ++notationEnv.cmi : \ ++ notationPt.cmo ++notationPp.cmo : \ ++ notationPt.cmo \ ++ notationEnv.cmi \ ++ notationPp.cmi ++notationPp.cmx : \ ++ notationPt.cmx \ ++ notationEnv.cmx \ ++ notationPp.cmi ++notationPp.cmi : \ ++ notationPt.cmo \ ++ notationEnv.cmi notationPt.cmo : notationPt.cmx : -content.cmo : content.cmi -content.cmx : content.cmi --notationUtil.cmo : notationPt.cmo notationUtil.cmi --notationUtil.cmx : notationPt.cmx notationUtil.cmi - notationUtil.cmi : notationPt.cmo -notationEnv.cmo : notationUtil.cmi notationPt.cmo notationEnv.cmi -notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi -notationPp.cmo : notationPt.cmo notationEnv.cmi notationPp.cmi -notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi ++notationUtil.cmo : \ ++ notationPt.cmo \ ++ notationUtil.cmi ++notationUtil.cmx : \ ++ notationPt.cmx \ ++ notationUtil.cmi ++notationUtil.cmi : \ ++ notationPt.cmo diff --cc matita/components/content/.depend.opt index 9c0b365c6,7bb00ba9b..4ef84ec5d --- a/matita/components/content/.depend.opt +++ b/matita/components/content/.depend.opt @@@ -1,9 -1,14 +1,22 @@@ - content.cmx : content.cmi ++content.cmx : \ ++ content.cmi content.cmi : - notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi -notationUtil.cmi : notationPt.cmx --notationEnv.cmi : notationPt.cmx - notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi --notationPp.cmi : notationPt.cmx notationEnv.cmi -notationPt.cmo : ++notationEnv.cmx : \ ++ notationUtil.cmx \ ++ notationPt.cmx \ ++ notationEnv.cmi ++notationEnv.cmi : \ ++ notationPt.cmx ++notationPp.cmx : \ ++ notationPt.cmx \ ++ notationEnv.cmx \ ++ notationPp.cmi ++notationPp.cmi : \ ++ notationPt.cmx \ ++ notationEnv.cmi notationPt.cmx : -content.cmo : content.cmi -content.cmx : content.cmi -notationUtil.cmo : notationPt.cmx notationUtil.cmi --notationUtil.cmx : notationPt.cmx notationUtil.cmi - notationUtil.cmi : notationPt.cmx -notationEnv.cmo : notationUtil.cmi notationPt.cmx notationEnv.cmi -notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi -notationPp.cmo : notationPt.cmx notationEnv.cmi notationPp.cmi -notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi ++notationUtil.cmx : \ ++ notationPt.cmx \ ++ notationUtil.cmi ++notationUtil.cmi : \ ++ notationPt.cmx diff --cc matita/components/content_pres/.depend index c4875d55f,4deb6e591..0f1c00964 --- a/matita/components/content_pres/.depend +++ b/matita/components/content_pres/.depend @@@ -1,38 -1,38 +1,92 @@@ - box.cmo : renderingAttrs.cmi box.cmi - box.cmx : renderingAttrs.cmx box.cmi -renderingAttrs.cmi : -cicNotationLexer.cmi : -cicNotationParser.cmi : -mpresentation.cmi : ++box.cmo : \ ++ renderingAttrs.cmi \ ++ box.cmi ++box.cmx : \ ++ renderingAttrs.cmx \ ++ box.cmi box.cmi : -content2presMatcher.cmi : -termContentPres.cmi : cicNotationParser.cmi -boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi -cicNotationPres.cmi : mpresentation.cmi box.cmi -content2pres.cmi : termContentPres.cmi cicNotationPres.cmi -renderingAttrs.cmo : renderingAttrs.cmi -renderingAttrs.cmx : renderingAttrs.cmi -cicNotationLexer.cmo : cicNotationLexer.cmi -cicNotationLexer.cmx : cicNotationLexer.cmi -cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi -cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi -mpresentation.cmo : mpresentation.cmi -mpresentation.cmx : mpresentation.cmi -box.cmo : renderingAttrs.cmi box.cmi -box.cmx : renderingAttrs.cmx box.cmi -content2presMatcher.cmo : content2presMatcher.cmi -content2presMatcher.cmx : content2presMatcher.cmi -termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \ - cicNotationParser.cmi termContentPres.cmi -termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \ - cicNotationParser.cmx termContentPres.cmi --boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \ ++boxPp.cmo : \ ++ renderingAttrs.cmi \ ++ mpresentation.cmi \ ++ cicNotationPres.cmi \ ++ box.cmi \ boxPp.cmi --boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ ++boxPp.cmx : \ ++ renderingAttrs.cmx \ ++ mpresentation.cmx \ ++ cicNotationPres.cmx \ ++ box.cmx \ boxPp.cmi - boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi - cicNotationLexer.cmo : cicNotationLexer.cmi - cicNotationLexer.cmx : cicNotationLexer.cmi -cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \ ++boxPp.cmi : \ ++ mpresentation.cmi \ ++ cicNotationPres.cmi \ ++ box.cmi ++cicNotationLexer.cmo : \ ++ cicNotationLexer.cmi ++cicNotationLexer.cmx : \ ++ cicNotationLexer.cmi +cicNotationLexer.cmi : - cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi - cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi ++cicNotationParser.cmo : \ ++ cicNotationLexer.cmi \ ++ cicNotationParser.cmi ++cicNotationParser.cmx : \ ++ cicNotationLexer.cmx \ ++ cicNotationParser.cmi +cicNotationParser.cmi : - cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \ ++cicNotationPres.cmo : \ ++ renderingAttrs.cmi \ ++ mpresentation.cmi \ ++ box.cmi \ + cicNotationPres.cmi - cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \ ++cicNotationPres.cmx : \ ++ renderingAttrs.cmx \ ++ mpresentation.cmx \ ++ box.cmx \ cicNotationPres.cmi - cicNotationPres.cmi : mpresentation.cmi box.cmi - content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ - cicNotationPres.cmi box.cmi content2pres.cmi - content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ - cicNotationPres.cmx box.cmx content2pres.cmi - content2pres.cmi : termContentPres.cmi cicNotationPres.cmi - content2presMatcher.cmo : content2presMatcher.cmi - content2presMatcher.cmx : content2presMatcher.cmi -cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \ ++cicNotationPres.cmi : \ ++ mpresentation.cmi \ ++ box.cmi ++content2pres.cmo : \ ++ termContentPres.cmi \ ++ renderingAttrs.cmi \ ++ mpresentation.cmi \ ++ cicNotationPres.cmi \ ++ box.cmi \ ++ content2pres.cmi ++content2pres.cmx : \ ++ termContentPres.cmx \ ++ renderingAttrs.cmx \ ++ mpresentation.cmx \ ++ cicNotationPres.cmx \ ++ box.cmx \ ++ content2pres.cmi ++content2pres.cmi : \ ++ termContentPres.cmi \ + cicNotationPres.cmi -content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ - cicNotationPres.cmi box.cmi content2pres.cmi -content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ - cicNotationPres.cmx box.cmx content2pres.cmi ++content2presMatcher.cmo : \ ++ content2presMatcher.cmi ++content2presMatcher.cmx : \ ++ content2presMatcher.cmi +content2presMatcher.cmi : - mpresentation.cmo : mpresentation.cmi - mpresentation.cmx : mpresentation.cmi ++mpresentation.cmo : \ ++ mpresentation.cmi ++mpresentation.cmx : \ ++ mpresentation.cmi +mpresentation.cmi : - renderingAttrs.cmo : renderingAttrs.cmi - renderingAttrs.cmx : renderingAttrs.cmi ++renderingAttrs.cmo : \ ++ renderingAttrs.cmi ++renderingAttrs.cmx : \ ++ renderingAttrs.cmi +renderingAttrs.cmi : - termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \ - cicNotationParser.cmi termContentPres.cmi - termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \ - cicNotationParser.cmx termContentPres.cmi - termContentPres.cmi : cicNotationParser.cmi ++termContentPres.cmo : \ ++ renderingAttrs.cmi \ ++ content2presMatcher.cmi \ ++ cicNotationParser.cmi \ ++ termContentPres.cmi ++termContentPres.cmx : \ ++ renderingAttrs.cmx \ ++ content2presMatcher.cmx \ ++ cicNotationParser.cmx \ ++ termContentPres.cmi ++termContentPres.cmi : \ ++ cicNotationParser.cmi diff --cc matita/components/content_pres/.depend.opt index 211b4fc51,4deb6e591..1e74dfbf4 --- a/matita/components/content_pres/.depend.opt +++ b/matita/components/content_pres/.depend.opt @@@ -1,24 -1,38 +1,55 @@@ - box.cmx : renderingAttrs.cmx box.cmi -renderingAttrs.cmi : -cicNotationLexer.cmi : -cicNotationParser.cmi : -mpresentation.cmi : ++box.cmx : \ ++ renderingAttrs.cmx \ ++ box.cmi box.cmi : -content2presMatcher.cmi : -termContentPres.cmi : cicNotationParser.cmi -boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi -cicNotationPres.cmi : mpresentation.cmi box.cmi -content2pres.cmi : termContentPres.cmi cicNotationPres.cmi -renderingAttrs.cmo : renderingAttrs.cmi -renderingAttrs.cmx : renderingAttrs.cmi -cicNotationLexer.cmo : cicNotationLexer.cmi -cicNotationLexer.cmx : cicNotationLexer.cmi -cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi -cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi -mpresentation.cmo : mpresentation.cmi -mpresentation.cmx : mpresentation.cmi -box.cmo : renderingAttrs.cmi box.cmi -box.cmx : renderingAttrs.cmx box.cmi -content2presMatcher.cmo : content2presMatcher.cmi -content2presMatcher.cmx : content2presMatcher.cmi -termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \ - cicNotationParser.cmi termContentPres.cmi -termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \ - cicNotationParser.cmx termContentPres.cmi -boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \ - boxPp.cmi --boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ ++boxPp.cmx : \ ++ renderingAttrs.cmx \ ++ mpresentation.cmx \ ++ cicNotationPres.cmx \ ++ box.cmx \ boxPp.cmi - boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi - cicNotationLexer.cmx : cicNotationLexer.cmi -cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \ ++boxPp.cmi : \ ++ mpresentation.cmi \ ++ cicNotationPres.cmi \ ++ box.cmi ++cicNotationLexer.cmx : \ ++ cicNotationLexer.cmi +cicNotationLexer.cmi : - cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi ++cicNotationParser.cmx : \ ++ cicNotationLexer.cmx \ ++ cicNotationParser.cmi +cicNotationParser.cmi : - cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \ ++cicNotationPres.cmx : \ ++ renderingAttrs.cmx \ ++ mpresentation.cmx \ ++ box.cmx \ cicNotationPres.cmi - cicNotationPres.cmi : mpresentation.cmi box.cmi - content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ - cicNotationPres.cmx box.cmx content2pres.cmi - content2pres.cmi : termContentPres.cmi cicNotationPres.cmi - content2presMatcher.cmx : content2presMatcher.cmi -cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \ ++cicNotationPres.cmi : \ ++ mpresentation.cmi \ ++ box.cmi ++content2pres.cmx : \ ++ termContentPres.cmx \ ++ renderingAttrs.cmx \ ++ mpresentation.cmx \ ++ cicNotationPres.cmx \ ++ box.cmx \ ++ content2pres.cmi ++content2pres.cmi : \ ++ termContentPres.cmi \ + cicNotationPres.cmi -content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ - cicNotationPres.cmi box.cmi content2pres.cmi -content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ - cicNotationPres.cmx box.cmx content2pres.cmi ++content2presMatcher.cmx : \ ++ content2presMatcher.cmi +content2presMatcher.cmi : - mpresentation.cmx : mpresentation.cmi ++mpresentation.cmx : \ ++ mpresentation.cmi +mpresentation.cmi : - renderingAttrs.cmx : renderingAttrs.cmi ++renderingAttrs.cmx : \ ++ renderingAttrs.cmi +renderingAttrs.cmi : - termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \ - cicNotationParser.cmx termContentPres.cmi - termContentPres.cmi : cicNotationParser.cmi ++termContentPres.cmx : \ ++ renderingAttrs.cmx \ ++ content2presMatcher.cmx \ ++ cicNotationParser.cmx \ ++ termContentPres.cmi ++termContentPres.cmi : \ ++ cicNotationParser.cmi diff --cc matita/components/disambiguation/.depend index a25280569,735bea7f7..2f1e0bd9e --- a/matita/components/disambiguation/.depend +++ b/matita/components/disambiguation/.depend @@@ -1,11 -1,11 +1,24 @@@ - disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi - disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi - disambiguate.cmi : disambiguateTypes.cmi - disambiguateTypes.cmo : disambiguateTypes.cmi - disambiguateTypes.cmx : disambiguateTypes.cmi ++disambiguate.cmo : \ ++ disambiguateTypes.cmi \ ++ disambiguate.cmi ++disambiguate.cmx : \ ++ disambiguateTypes.cmx \ ++ disambiguate.cmi ++disambiguate.cmi : \ ++ disambiguateTypes.cmi ++disambiguateTypes.cmo : \ ++ disambiguateTypes.cmi ++disambiguateTypes.cmx : \ ++ disambiguateTypes.cmi disambiguateTypes.cmi : -disambiguate.cmi : disambiguateTypes.cmi -multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi -disambiguateTypes.cmo : disambiguateTypes.cmi -disambiguateTypes.cmx : disambiguateTypes.cmi -disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi -disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi --multiPassDisambiguator.cmo : disambiguateTypes.cmi disambiguate.cmi \ ++multiPassDisambiguator.cmo : \ ++ disambiguateTypes.cmi \ ++ disambiguate.cmi \ multiPassDisambiguator.cmi --multiPassDisambiguator.cmx : disambiguateTypes.cmx disambiguate.cmx \ ++multiPassDisambiguator.cmx : \ ++ disambiguateTypes.cmx \ ++ disambiguate.cmx \ multiPassDisambiguator.cmi - multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi ++multiPassDisambiguator.cmi : \ ++ disambiguateTypes.cmi \ ++ disambiguate.cmi diff --cc matita/components/disambiguation/.depend.opt index 1f1711ae7,735bea7f7..867ae4666 --- a/matita/components/disambiguation/.depend.opt +++ b/matita/components/disambiguation/.depend.opt @@@ -1,7 -1,11 +1,15 @@@ - disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi - disambiguate.cmi : disambiguateTypes.cmi - disambiguateTypes.cmx : disambiguateTypes.cmi ++disambiguate.cmx : \ ++ disambiguateTypes.cmx \ ++ disambiguate.cmi ++disambiguate.cmi : \ ++ disambiguateTypes.cmi ++disambiguateTypes.cmx : \ ++ disambiguateTypes.cmi disambiguateTypes.cmi : -disambiguate.cmi : disambiguateTypes.cmi -multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi -disambiguateTypes.cmo : disambiguateTypes.cmi -disambiguateTypes.cmx : disambiguateTypes.cmi -disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi -disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi -multiPassDisambiguator.cmo : disambiguateTypes.cmi disambiguate.cmi \ - multiPassDisambiguator.cmi --multiPassDisambiguator.cmx : disambiguateTypes.cmx disambiguate.cmx \ ++multiPassDisambiguator.cmx : \ ++ disambiguateTypes.cmx \ ++ disambiguate.cmx \ multiPassDisambiguator.cmi - multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi ++multiPassDisambiguator.cmi : \ ++ disambiguateTypes.cmi \ ++ disambiguate.cmi diff --cc matita/components/extlib/.depend index 36dd894f0,e7b0a3bc7..c4c6d7e8a --- a/matita/components/extlib/.depend +++ b/matita/components/extlib/.depend @@@ -1,27 -1,27 +1,51 @@@ - componentsConf.cmo : componentsConf.cmi - componentsConf.cmx : componentsConf.cmi ++componentsConf.cmo : \ ++ componentsConf.cmi ++componentsConf.cmx : \ ++ componentsConf.cmi componentsConf.cmi : - discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi - discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi ++discrimination_tree.cmo : \ ++ trie.cmi \ ++ hExtlib.cmi \ ++ discrimination_tree.cmi ++discrimination_tree.cmx : \ ++ trie.cmx \ ++ hExtlib.cmx \ ++ discrimination_tree.cmi +discrimination_tree.cmi : - graphvizPp.cmo : graphvizPp.cmi - graphvizPp.cmx : graphvizPp.cmi ++graphvizPp.cmo : \ ++ graphvizPp.cmi ++graphvizPp.cmx : \ ++ graphvizPp.cmi +graphvizPp.cmi : - hExtlib.cmo : hExtlib.cmi - hExtlib.cmx : hExtlib.cmi ++hExtlib.cmo : \ ++ hExtlib.cmi ++hExtlib.cmx : \ ++ hExtlib.cmi hExtlib.cmi : - hLog.cmo : hLog.cmi - hLog.cmx : hLog.cmi ++hLog.cmo : \ ++ hLog.cmi ++hLog.cmx : \ ++ hLog.cmi +hLog.cmi : - hMarshal.cmo : hExtlib.cmi hMarshal.cmi - hMarshal.cmx : hExtlib.cmx hMarshal.cmi ++hMarshal.cmo : \ ++ hExtlib.cmi \ ++ hMarshal.cmi ++hMarshal.cmx : \ ++ hExtlib.cmx \ ++ hMarshal.cmi hMarshal.cmi : - hTopoSort.cmo : hTopoSort.cmi - hTopoSort.cmx : hTopoSort.cmi ++hTopoSort.cmo : \ ++ hTopoSort.cmi ++hTopoSort.cmx : \ ++ hTopoSort.cmi +hTopoSort.cmi : - patternMatcher.cmo : patternMatcher.cmi - patternMatcher.cmx : patternMatcher.cmi ++patternMatcher.cmo : \ ++ patternMatcher.cmi ++patternMatcher.cmx : \ ++ patternMatcher.cmi patternMatcher.cmi : - trie.cmo : trie.cmi - trie.cmx : trie.cmi -hLog.cmi : ++trie.cmo : \ ++ trie.cmi ++trie.cmx : \ ++ trie.cmi trie.cmi : -discrimination_tree.cmi : -hTopoSort.cmi : -graphvizPp.cmi : -componentsConf.cmo : componentsConf.cmi -componentsConf.cmx : componentsConf.cmi -hExtlib.cmo : hExtlib.cmi -hExtlib.cmx : hExtlib.cmi -hMarshal.cmo : hExtlib.cmi hMarshal.cmi -hMarshal.cmx : hExtlib.cmx hMarshal.cmi -patternMatcher.cmo : patternMatcher.cmi -patternMatcher.cmx : patternMatcher.cmi -hLog.cmo : hLog.cmi -hLog.cmx : hLog.cmi -trie.cmo : trie.cmi -trie.cmx : trie.cmi -discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi -discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi -hTopoSort.cmo : hTopoSort.cmi -hTopoSort.cmx : hTopoSort.cmi -graphvizPp.cmo : graphvizPp.cmi -graphvizPp.cmx : graphvizPp.cmi diff --cc matita/components/extlib/.depend.opt index 12de49274,e7b0a3bc7..72b64d1cf --- a/matita/components/extlib/.depend.opt +++ b/matita/components/extlib/.depend.opt @@@ -1,18 -1,27 +1,30 @@@ - componentsConf.cmx : componentsConf.cmi ++componentsConf.cmx : \ ++ componentsConf.cmi componentsConf.cmi : - discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi ++discrimination_tree.cmx : \ ++ trie.cmx \ ++ hExtlib.cmx \ ++ discrimination_tree.cmi +discrimination_tree.cmi : - graphvizPp.cmx : graphvizPp.cmi ++graphvizPp.cmx : \ ++ graphvizPp.cmi +graphvizPp.cmi : - hExtlib.cmx : hExtlib.cmi ++hExtlib.cmx : \ ++ hExtlib.cmi hExtlib.cmi : - hLog.cmx : hLog.cmi ++hLog.cmx : \ ++ hLog.cmi +hLog.cmi : - hMarshal.cmx : hExtlib.cmx hMarshal.cmi ++hMarshal.cmx : \ ++ hExtlib.cmx \ ++ hMarshal.cmi hMarshal.cmi : - hTopoSort.cmx : hTopoSort.cmi ++hTopoSort.cmx : \ ++ hTopoSort.cmi +hTopoSort.cmi : - patternMatcher.cmx : patternMatcher.cmi ++patternMatcher.cmx : \ ++ patternMatcher.cmi patternMatcher.cmi : - trie.cmx : trie.cmi -hLog.cmi : ++trie.cmx : \ ++ trie.cmi trie.cmi : -discrimination_tree.cmi : -hTopoSort.cmi : -graphvizPp.cmi : -componentsConf.cmo : componentsConf.cmi -componentsConf.cmx : componentsConf.cmi -hExtlib.cmo : hExtlib.cmi -hExtlib.cmx : hExtlib.cmi -hMarshal.cmo : hExtlib.cmi hMarshal.cmi -hMarshal.cmx : hExtlib.cmx hMarshal.cmi -patternMatcher.cmo : patternMatcher.cmi -patternMatcher.cmx : patternMatcher.cmi -hLog.cmo : hLog.cmi -hLog.cmx : hLog.cmi -trie.cmo : trie.cmi -trie.cmx : trie.cmi -discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi -discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi -hTopoSort.cmo : hTopoSort.cmi -hTopoSort.cmx : hTopoSort.cmi -graphvizPp.cmo : graphvizPp.cmi -graphvizPp.cmx : graphvizPp.cmi diff --cc matita/components/getter/.depend index 13ca8cc29,59c0b896e..aa9063835 --- a/matita/components/getter/.depend +++ b/matita/components/getter/.depend @@@ -1,38 -1,38 +1,89 @@@ - http_getter.cmo : http_getter_wget.cmi http_getter_types.cmo \ - http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \ - http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \ -http_getter_wget.cmi : ++http_getter.cmo : \ ++ http_getter_wget.cmi \ ++ http_getter_types.cmo \ ++ http_getter_storage.cmi \ ++ http_getter_misc.cmi \ ++ http_getter_logger.cmi \ ++ http_getter_env.cmi \ ++ http_getter_const.cmi \ ++ http_getter_common.cmi \ + http_getter.cmi - http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ - http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ ++http_getter.cmx : \ ++ http_getter_wget.cmx \ ++ http_getter_types.cmx \ ++ http_getter_storage.cmx \ ++ http_getter_misc.cmx \ ++ http_getter_logger.cmx \ ++ http_getter_env.cmx \ ++ http_getter_const.cmx \ ++ http_getter_common.cmx \ + http_getter.cmi - http_getter.cmi : http_getter_types.cmo - http_getter_common.cmo : http_getter_types.cmo http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi - http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi - http_getter_common.cmi : http_getter_types.cmo - http_getter_const.cmo : http_getter_const.cmi - http_getter_const.cmx : http_getter_const.cmi ++http_getter.cmi : \ ++ http_getter_types.cmo ++http_getter_common.cmo : \ ++ http_getter_types.cmo \ ++ http_getter_misc.cmi \ ++ http_getter_logger.cmi \ ++ http_getter_env.cmi \ ++ http_getter_common.cmi ++http_getter_common.cmx : \ ++ http_getter_types.cmx \ ++ http_getter_misc.cmx \ ++ http_getter_logger.cmx \ ++ http_getter_env.cmx \ ++ http_getter_common.cmi ++http_getter_common.cmi : \ ++ http_getter_types.cmo ++http_getter_const.cmo : \ ++ http_getter_const.cmi ++http_getter_const.cmx : \ ++ http_getter_const.cmi +http_getter_const.cmi : - http_getter_env.cmo : http_getter_types.cmo http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi - http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi - http_getter_env.cmi : http_getter_types.cmo - http_getter_logger.cmo : http_getter_logger.cmi - http_getter_logger.cmx : http_getter_logger.cmi ++http_getter_env.cmo : \ ++ http_getter_types.cmo \ ++ http_getter_misc.cmi \ ++ http_getter_logger.cmi \ ++ http_getter_const.cmi \ ++ http_getter_env.cmi ++http_getter_env.cmx : \ ++ http_getter_types.cmx \ ++ http_getter_misc.cmx \ ++ http_getter_logger.cmx \ ++ http_getter_const.cmx \ ++ http_getter_env.cmi ++http_getter_env.cmi : \ ++ http_getter_types.cmo ++http_getter_logger.cmo : \ ++ http_getter_logger.cmi ++http_getter_logger.cmx : \ ++ http_getter_logger.cmi http_getter_logger.cmi : - http_getter_misc.cmo : http_getter_logger.cmi http_getter_misc.cmi - http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi ++http_getter_misc.cmo : \ ++ http_getter_logger.cmi \ ++ http_getter_misc.cmi ++http_getter_misc.cmx : \ ++ http_getter_logger.cmx \ ++ http_getter_misc.cmi http_getter_misc.cmi : - http_getter_storage.cmo : http_getter_wget.cmi http_getter_types.cmo \ - http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi - http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi -http_getter_const.cmi : -http_getter_env.cmi : http_getter_types.cmo ++http_getter_storage.cmo : \ ++ http_getter_wget.cmi \ ++ http_getter_types.cmo \ ++ http_getter_misc.cmi \ ++ http_getter_env.cmi \ ++ http_getter_storage.cmi ++http_getter_storage.cmx : \ ++ http_getter_wget.cmx \ ++ http_getter_types.cmx \ ++ http_getter_misc.cmx \ ++ http_getter_env.cmx \ ++ http_getter_storage.cmi 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 -http_getter_logger.cmx : http_getter_logger.cmi -http_getter_misc.cmo : http_getter_logger.cmi http_getter_misc.cmi -http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi -http_getter_const.cmo : http_getter_const.cmi -http_getter_const.cmx : http_getter_const.cmi -http_getter_env.cmo : http_getter_types.cmo http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi -http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi -http_getter_storage.cmo : http_getter_wget.cmi http_getter_types.cmo \ - http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi -http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi -http_getter_common.cmo : http_getter_types.cmo http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi -http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi -http_getter.cmo : http_getter_wget.cmi http_getter_types.cmo \ - http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \ - http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \ - http_getter.cmi -http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ - http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ - http_getter.cmi ++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_wget.cmi : diff --cc matita/components/getter/.depend.opt index 1d016d277,7c2b60586..cb0f289ac --- a/matita/components/getter/.depend.opt +++ b/matita/components/getter/.depend.opt @@@ -1,23 -1,38 +1,50 @@@ - http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ - http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ -http_getter_wget.cmi : ++http_getter.cmx : \ ++ http_getter_wget.cmx \ ++ http_getter_types.cmx \ ++ http_getter_storage.cmx \ ++ http_getter_misc.cmx \ ++ http_getter_logger.cmx \ ++ http_getter_env.cmx \ ++ http_getter_const.cmx \ ++ http_getter_common.cmx \ + http_getter.cmi - http_getter.cmi : http_getter_types.cmx - http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi - http_getter_common.cmi : http_getter_types.cmx - http_getter_const.cmx : http_getter_const.cmi ++http_getter.cmi : \ ++ http_getter_types.cmx ++http_getter_common.cmx : \ ++ http_getter_types.cmx \ ++ http_getter_misc.cmx \ ++ http_getter_logger.cmx \ ++ http_getter_env.cmx \ ++ http_getter_common.cmi ++http_getter_common.cmi : \ ++ http_getter_types.cmx ++http_getter_const.cmx : \ ++ http_getter_const.cmi +http_getter_const.cmi : - http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi - http_getter_env.cmi : http_getter_types.cmx - http_getter_logger.cmx : http_getter_logger.cmi ++http_getter_env.cmx : \ ++ http_getter_types.cmx \ ++ http_getter_misc.cmx \ ++ http_getter_logger.cmx \ ++ http_getter_const.cmx \ ++ http_getter_env.cmi ++http_getter_env.cmi : \ ++ http_getter_types.cmx ++http_getter_logger.cmx : \ ++ http_getter_logger.cmi http_getter_logger.cmi : - http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi ++http_getter_misc.cmx : \ ++ http_getter_logger.cmx \ ++ http_getter_misc.cmi http_getter_misc.cmi : - http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi -http_getter_const.cmi : -http_getter_env.cmi : http_getter_types.cmx ++http_getter_storage.cmx : \ ++ http_getter_wget.cmx \ ++ http_getter_types.cmx \ ++ http_getter_misc.cmx \ ++ http_getter_env.cmx \ ++ http_getter_storage.cmi 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 -http_getter_logger.cmx : http_getter_logger.cmi -http_getter_misc.cmo : http_getter_logger.cmi http_getter_misc.cmi -http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi -http_getter_const.cmo : http_getter_const.cmi -http_getter_const.cmx : http_getter_const.cmi -http_getter_env.cmo : http_getter_types.cmx http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi -http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi -http_getter_storage.cmo : http_getter_wget.cmi http_getter_types.cmx \ - http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi -http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi -http_getter_common.cmo : http_getter_types.cmx http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi -http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi -http_getter.cmo : http_getter_wget.cmi http_getter_types.cmx \ - http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \ - http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \ - http_getter.cmi -http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ - http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ - http_getter.cmi ++http_getter_wget.cmx : \ ++ http_getter_types.cmx \ ++ http_getter_wget.cmi +http_getter_wget.cmi : diff --cc matita/components/grafite/.depend index 211eff733,e70c83c77..bf8b5d3f5 --- a/matita/components/grafite/.depend +++ b/matita/components/grafite/.depend @@@ -1,5 -1,5 +1,10 @@@ -grafiteAstPp.cmi : grafiteAst.cmo grafiteAst.cmo : grafiteAst.cmx : --grafiteAstPp.cmo : grafiteAst.cmo grafiteAstPp.cmi --grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi - grafiteAstPp.cmi : grafiteAst.cmo ++grafiteAstPp.cmo : \ ++ grafiteAst.cmo \ ++ grafiteAstPp.cmi ++grafiteAstPp.cmx : \ ++ grafiteAst.cmx \ ++ grafiteAstPp.cmi ++grafiteAstPp.cmi : \ ++ grafiteAst.cmo diff --cc matita/components/grafite/.depend.opt index 5dabb8012,4a1ca42e9..be6de9f62 --- a/matita/components/grafite/.depend.opt +++ b/matita/components/grafite/.depend.opt @@@ -1,3 -1,5 +1,6 @@@ -grafiteAstPp.cmi : grafiteAst.cmx -grafiteAst.cmo : grafiteAst.cmx : -grafiteAstPp.cmo : grafiteAst.cmx grafiteAstPp.cmi --grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi - grafiteAstPp.cmi : grafiteAst.cmx ++grafiteAstPp.cmx : \ ++ grafiteAst.cmx \ ++ grafiteAstPp.cmi ++grafiteAstPp.cmi : \ ++ grafiteAst.cmx diff --cc matita/components/grafite/grafiteAstPp.ml index 2e088bd77,60c466068..42d7df864 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@@ -70,14 -86,14 +86,14 @@@ let rec pp_ntactic status ~map_unicode_ | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^ String.concat " " (List.map (NotationPp.pp_term status) l) | NCase1 (_,n) -> "*" ^ n ^ ":" - | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^ - | NChange (_,what,wwhat) -> "nchange " ^ "...to be implemented..." ^ ++ | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^ " with " ^ NotationPp.pp_term status wwhat | NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t (*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t | NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *) | NClear (_,l) -> "nclear " ^ String.concat " " l - | NDestruct (_,_dom,_skip) -> "ndestruct ..." - | NDestruct (_,dom,skip) -> "ndestruct ..." - | NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term status what ^ ++ | NDestruct (_,_dom,_skip) -> "ndestruct ..." + | NElim (_,what,_where) -> "nelim " ^ NotationPp.pp_term status what ^ "...to be implemented..." ^ " " ^ "...to be implemented..." | NId _ -> "nid" | NIntro (_,n) -> "#" ^ n @@@ -104,9 -120,50 +120,51 @@@ | NSkip _ -> "skip" | NTry (_,tac) -> "ntry " ^ pp_ntactic status ~map_unicode_to_tex tac | NAssumption _ -> "nassumption" - | NBlock (_,l) -> + | NBlock (_,l) -> "(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")" | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t + | Assume (_, ident, term) -> "assume " ^ ident ^ ":(" ^ (NotationPp.pp_term status term) ^ ")" + | Suppose (_,term,ident) -> "suppose (" ^ (NotationPp.pp_term status term) ^ ") (" ^ ident ^ ") " + | By_just_we_proved (_, just, term1, ident) -> pp_just status just ^ " we proved (" ^ + (NotationPp.pp_term status term1) ^ ")" ^ (match ident with + None -> "" | Some ident -> "(" ^ident^ ")") + | We_need_to_prove (_,term,ident) -> "we need to prove (" ^ (NotationPp.pp_term status term) ^ ") " ^ + (match ident with None -> "" | Some id -> "(" ^ id ^ ")") + | BetaRewritingStep (_,t) -> "that is equivalent to (" ^ (NotationPp.pp_term status t) ^ ")" + | Bydone (_, just) -> pp_just status just ^ "done" + | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ": (" + ^ (NotationPp.pp_term status term) ^ ") such that (" ^ (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ")" + | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ " we have (" ^ + (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ") " ^ "and (" ^ (NotationPp.pp_term status + term2) + ^ ") (" ^ ident2 ^ ")" + | Thesisbecomes (_, t) -> "the thesis becomes (" ^ (NotationPp.pp_term status t) ^ ")" + | RewritingStep (_, rhs, just, cont) -> + "= (" ^ + (NotationPp.pp_term status rhs) ^ ")" ^ + (match just with + | `Auto params -> let s = pp_auto_params params status in + if s <> "" then " by " ^ s + else "" + | `Term t -> " exact (" ^ (NotationPp.pp_term status t) ^ ")" + | `Proof -> " proof" + | `SolveWith t -> " using (" ^ (NotationPp.pp_term status t) ^ ")" + ) + ^ (if cont then " done" else "") + | Obtain (_,id,t1) -> "obtain (" ^ id ^ ")" ^ " (" ^ (NotationPp.pp_term status t1) ^ ")" + | Conclude (_,t1) -> "conclude (" ^ (NotationPp.pp_term status t1) ^ ")" + | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on (" ^ NotationPp.pp_term + status term ^ ") to prove (" ^ NotationPp.pp_term status term1 ^ ")" + | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on (" ^ + NotationPp.pp_term status term ^ ") to prove (" ^ NotationPp.pp_term status term1 ^ ")" + | Byinduction (_, term, ident) -> "by induction hypothesis we know (" ^ NotationPp.pp_term status + term ^ ") (" ^ ident ^ ")" + | Case (_, id, args) -> + "case " ^ id ^ + String.concat " " + (List.map (function (id,term) -> "(" ^ id ^ ": (" ^ NotationPp.pp_term status term ^ "))") + args) ++ | PrintStack _ -> "print_stack" ;; let pp_nmacro status = function diff --cc matita/components/grafite_engine/.depend index 627227c70,e6d4942c6..bffffc1b8 --- a/matita/components/grafite_engine/.depend +++ b/matita/components/grafite_engine/.depend @@@ -1,11 -1,11 +1,23 @@@ -grafiteTypes.cmi : -nCicCoercDeclaration.cmi : grafiteTypes.cmi -grafiteEngine.cmi : grafiteTypes.cmi -grafiteTypes.cmo : grafiteTypes.cmi -grafiteTypes.cmx : grafiteTypes.cmi -nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi -nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi --grafiteEngine.cmo : nCicCoercDeclaration.cmi grafiteTypes.cmi \ ++grafiteEngine.cmo : \ ++ nCicCoercDeclaration.cmi \ ++ grafiteTypes.cmi \ grafiteEngine.cmi --grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \ ++grafiteEngine.cmx : \ ++ nCicCoercDeclaration.cmx \ ++ grafiteTypes.cmx \ grafiteEngine.cmi - grafiteEngine.cmi : grafiteTypes.cmi - grafiteTypes.cmo : grafiteTypes.cmi - grafiteTypes.cmx : grafiteTypes.cmi ++grafiteEngine.cmi : \ ++ grafiteTypes.cmi ++grafiteTypes.cmo : \ ++ grafiteTypes.cmi ++grafiteTypes.cmx : \ ++ grafiteTypes.cmi +grafiteTypes.cmi : - nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi - nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi - nCicCoercDeclaration.cmi : grafiteTypes.cmi ++nCicCoercDeclaration.cmo : \ ++ grafiteTypes.cmi \ ++ nCicCoercDeclaration.cmi ++nCicCoercDeclaration.cmx : \ ++ grafiteTypes.cmx \ ++ nCicCoercDeclaration.cmi ++nCicCoercDeclaration.cmi : \ ++ grafiteTypes.cmi diff --cc matita/components/grafite_engine/.depend.opt index 696b45881,e6d4942c6..6e9ccb21a --- a/matita/components/grafite_engine/.depend.opt +++ b/matita/components/grafite_engine/.depend.opt @@@ -1,7 -1,11 +1,14 @@@ -grafiteTypes.cmi : -nCicCoercDeclaration.cmi : grafiteTypes.cmi -grafiteEngine.cmi : grafiteTypes.cmi -grafiteTypes.cmo : grafiteTypes.cmi -grafiteTypes.cmx : grafiteTypes.cmi -nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi -nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi -grafiteEngine.cmo : nCicCoercDeclaration.cmi grafiteTypes.cmi \ - grafiteEngine.cmi --grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \ ++grafiteEngine.cmx : \ ++ nCicCoercDeclaration.cmx \ ++ grafiteTypes.cmx \ grafiteEngine.cmi - grafiteEngine.cmi : grafiteTypes.cmi - grafiteTypes.cmx : grafiteTypes.cmi ++grafiteEngine.cmi : \ ++ grafiteTypes.cmi ++grafiteTypes.cmx : \ ++ grafiteTypes.cmi +grafiteTypes.cmi : - nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi - nCicCoercDeclaration.cmi : grafiteTypes.cmi ++nCicCoercDeclaration.cmx : \ ++ grafiteTypes.cmx \ ++ nCicCoercDeclaration.cmi ++nCicCoercDeclaration.cmi : \ ++ grafiteTypes.cmi diff --cc matita/components/grafite_engine/grafiteEngine.ml index bd9e76ff2,93396d2bd..71f036904 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@@ -481,6 -492,39 +492,39 @@@ let eval_ng_tac tac NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l) |GrafiteAst.NRepeat (_,tac) -> NTactics.repeat_tac (f f (text, prefix_len, tac)) + |GrafiteAst.Assume (_,id,t) -> Declarative.assume id (text,prefix_len,t) + |GrafiteAst.Suppose (_,t,id) -> Declarative.suppose (text,prefix_len,t) id + |GrafiteAst.By_just_we_proved (_,j,t1,s) -> Declarative.by_just_we_proved + (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s + |GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove (text,prefix_len,t) id + |GrafiteAst.BetaRewritingStep (_, t) -> Declarative.beta_rewriting_step (text,prefix_len,t) + | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len) + | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) -> + Declarative.existselim (just_to_tacstatus_just just text prefix_len) id1 (text,prefix_len,t1) + (text,prefix_len,t2) id2 + | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just + text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2 + | GrafiteAst.Thesisbecomes (_, t1) -> Declarative.thesisbecomes (text,prefix_len,t1) + | GrafiteAst.RewritingStep (_,rhs,just,cont) -> + Declarative.rewritingstep (text,prefix_len,rhs) + (match just with - `Term t -> just_to_tacstatus_just just text prefix_len - | `Auto params -> just_to_tacstatus_just just text prefix_len ++ `Term _ ++ | `Auto _ -> just_to_tacstatus_just just text prefix_len + |`Proof -> `Proof + |`SolveWith t -> `SolveWith (text,prefix_len,t) + ) + cont + | GrafiteAst.Obtain (_,id,t1) -> + Declarative.obtain id (text,prefix_len,t1) + | GrafiteAst.Conclude (_,t1) -> + Declarative.conclude (text,prefix_len,t1) + | GrafiteAst.We_proceed_by_cases_on (_, t, t1) -> + Declarative.we_proceed_by_cases_on (text,prefix_len,t) (text,prefix_len,t1) + | GrafiteAst.We_proceed_by_induction_on (_, t, t1) -> + Declarative.we_proceed_by_induction_on (text,prefix_len,t) (text,prefix_len,t1) + | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction (text,prefix_len,t) id + | GrafiteAst.Case (_,id,params) -> Declarative.case id params + | GrafiteAst.PrintStack (_) -> Declarative.print_stack in aux aux tac (* trick for non uniform recursion call *) ;; diff --cc matita/components/grafite_parser/.depend index fcb901973,752b0d88d..13f0fb882 --- a/matita/components/grafite_parser/.depend +++ b/matita/components/grafite_parser/.depend @@@ -1,6 -1,6 +1,11 @@@ - grafiteParser.cmo : grafiteParser.cmi - grafiteParser.cmx : grafiteParser.cmi ++grafiteParser.cmo : \ ++ grafiteParser.cmi ++grafiteParser.cmx : \ ++ grafiteParser.cmi grafiteParser.cmi : -print_grammar.cmi : grafiteParser.cmi -grafiteParser.cmo : grafiteParser.cmi -grafiteParser.cmx : grafiteParser.cmi --print_grammar.cmo : print_grammar.cmi --print_grammar.cmx : print_grammar.cmi - print_grammar.cmi : grafiteParser.cmi ++print_grammar.cmo : \ ++ print_grammar.cmi ++print_grammar.cmx : \ ++ print_grammar.cmi ++print_grammar.cmi : \ ++ grafiteParser.cmi diff --cc matita/components/grafite_parser/.depend.opt index e0e6dac9c,752b0d88d..4b014236d --- a/matita/components/grafite_parser/.depend.opt +++ b/matita/components/grafite_parser/.depend.opt @@@ -1,4 -1,6 +1,7 @@@ - grafiteParser.cmx : grafiteParser.cmi ++grafiteParser.cmx : \ ++ grafiteParser.cmi grafiteParser.cmi : - print_grammar.cmx : print_grammar.cmi --print_grammar.cmi : grafiteParser.cmi -grafiteParser.cmo : grafiteParser.cmi -grafiteParser.cmx : grafiteParser.cmi -print_grammar.cmo : print_grammar.cmi -print_grammar.cmx : print_grammar.cmi ++print_grammar.cmx : \ ++ print_grammar.cmi ++print_grammar.cmi : \ ++ grafiteParser.cmi diff --cc matita/components/library/.depend index 7af1a906e,6f2769b94..2cf0d4213 --- a/matita/components/library/.depend +++ b/matita/components/library/.depend @@@ -1,9 -1,9 +1,15 @@@ - librarian.cmo : librarian.cmi - librarian.cmx : librarian.cmi ++librarian.cmo : \ ++ librarian.cmi ++librarian.cmx : \ ++ librarian.cmi librarian.cmi : - libraryClean.cmo : libraryClean.cmi - libraryClean.cmx : libraryClean.cmi -libraryMisc.cmi : ++libraryClean.cmo : \ ++ libraryClean.cmi ++libraryClean.cmx : \ ++ libraryClean.cmi libraryClean.cmi : -librarian.cmo : librarian.cmi -librarian.cmx : librarian.cmi --libraryMisc.cmo : libraryMisc.cmi --libraryMisc.cmx : libraryMisc.cmi -libraryClean.cmo : libraryClean.cmi -libraryClean.cmx : libraryClean.cmi ++libraryMisc.cmo : \ ++ libraryMisc.cmi ++libraryMisc.cmx : \ ++ libraryMisc.cmi +libraryMisc.cmi : diff --cc matita/components/library/.depend.opt index 27ecf9383,6f2769b94..d960dc9be --- a/matita/components/library/.depend.opt +++ b/matita/components/library/.depend.opt @@@ -1,6 -1,9 +1,9 @@@ - librarian.cmx : librarian.cmi ++librarian.cmx : \ ++ librarian.cmi librarian.cmi : - libraryClean.cmx : libraryClean.cmi -libraryMisc.cmi : ++libraryClean.cmx : \ ++ libraryClean.cmi libraryClean.cmi : -librarian.cmo : librarian.cmi -librarian.cmx : librarian.cmi -libraryMisc.cmo : libraryMisc.cmi --libraryMisc.cmx : libraryMisc.cmi -libraryClean.cmo : libraryClean.cmi -libraryClean.cmx : libraryClean.cmi ++libraryMisc.cmx : \ ++ libraryMisc.cmi +libraryMisc.cmi : diff --cc matita/components/logger/.depend index a22bd16f1,d1b4c3716..26c231a99 --- a/matita/components/logger/.depend +++ b/matita/components/logger/.depend @@@ -1,3 -1,3 +1,5 @@@ - helmLogger.cmo : helmLogger.cmi - helmLogger.cmx : helmLogger.cmi ++helmLogger.cmo : \ ++ helmLogger.cmi ++helmLogger.cmx : \ ++ helmLogger.cmi helmLogger.cmi : -helmLogger.cmo : helmLogger.cmi -helmLogger.cmx : helmLogger.cmi diff --cc matita/components/logger/.depend.opt index ed934897f,d1b4c3716..f68fdd43e --- a/matita/components/logger/.depend.opt +++ b/matita/components/logger/.depend.opt @@@ -1,2 -1,3 +1,3 @@@ - helmLogger.cmx : helmLogger.cmi ++helmLogger.cmx : \ ++ helmLogger.cmi helmLogger.cmi : -helmLogger.cmo : helmLogger.cmi -helmLogger.cmx : helmLogger.cmi diff --cc matita/components/ng_cic_content/.depend index 579a21e33,01e2f5b1e..d870b57dc --- a/matita/components/ng_cic_content/.depend +++ b/matita/components/ng_cic_content/.depend @@@ -1,6 -1,6 +1,12 @@@ - interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi - interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi -ncic2astMatcher.cmi : ++interpretations.cmo : \ ++ ncic2astMatcher.cmi \ ++ interpretations.cmi ++interpretations.cmx : \ ++ ncic2astMatcher.cmx \ ++ interpretations.cmi interpretations.cmi : --ncic2astMatcher.cmo : ncic2astMatcher.cmi --ncic2astMatcher.cmx : ncic2astMatcher.cmi -interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi -interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi ++ncic2astMatcher.cmo : \ ++ ncic2astMatcher.cmi ++ncic2astMatcher.cmx : \ ++ ncic2astMatcher.cmi +ncic2astMatcher.cmi : diff --cc matita/components/ng_cic_content/.depend.opt index df8d6d635,01e2f5b1e..b526a0df5 --- a/matita/components/ng_cic_content/.depend.opt +++ b/matita/components/ng_cic_content/.depend.opt @@@ -1,4 -1,6 +1,7 @@@ - interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi -ncic2astMatcher.cmi : ++interpretations.cmx : \ ++ ncic2astMatcher.cmx \ ++ interpretations.cmi interpretations.cmi : -ncic2astMatcher.cmo : ncic2astMatcher.cmi --ncic2astMatcher.cmx : ncic2astMatcher.cmi -interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi -interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi ++ncic2astMatcher.cmx : \ ++ ncic2astMatcher.cmi +ncic2astMatcher.cmi : diff --cc matita/components/ng_disambiguation/.depend index fa8349c58,79fd839b2..7462feedb --- a/matita/components/ng_disambiguation/.depend +++ b/matita/components/ng_disambiguation/.depend @@@ -1,14 -1,14 +1,26 @@@ - disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi - disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi -nnumber_notation.cmi : ++disambiguateChoices.cmo : \ ++ nnumber_notation.cmi \ ++ disambiguateChoices.cmi ++disambiguateChoices.cmx : \ ++ nnumber_notation.cmx \ ++ disambiguateChoices.cmi disambiguateChoices.cmi : -nCicDisambiguate.cmi : -grafiteDisambiguate.cmi : -nnumber_notation.cmo : nnumber_notation.cmi -nnumber_notation.cmx : nnumber_notation.cmi -disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi -disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi -nCicDisambiguate.cmo : nCicDisambiguate.cmi -nCicDisambiguate.cmx : nCicDisambiguate.cmi --grafiteDisambiguate.cmo : nCicDisambiguate.cmi disambiguateChoices.cmi \ ++grafiteDisambiguate.cmo : \ ++ nCicDisambiguate.cmi \ ++ disambiguateChoices.cmi \ grafiteDisambiguate.cmi --grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \ ++grafiteDisambiguate.cmx : \ ++ nCicDisambiguate.cmx \ ++ disambiguateChoices.cmx \ grafiteDisambiguate.cmi +grafiteDisambiguate.cmi : - nCicDisambiguate.cmo : nCicDisambiguate.cmi - nCicDisambiguate.cmx : nCicDisambiguate.cmi ++nCicDisambiguate.cmo : \ ++ nCicDisambiguate.cmi ++nCicDisambiguate.cmx : \ ++ nCicDisambiguate.cmi +nCicDisambiguate.cmi : - nnumber_notation.cmo : nnumber_notation.cmi - nnumber_notation.cmx : nnumber_notation.cmi ++nnumber_notation.cmo : \ ++ nnumber_notation.cmi ++nnumber_notation.cmx : \ ++ nnumber_notation.cmi +nnumber_notation.cmi : diff --cc matita/components/ng_disambiguation/.depend.opt index d5eef6bc0,79fd839b2..6904cfd3b --- a/matita/components/ng_disambiguation/.depend.opt +++ b/matita/components/ng_disambiguation/.depend.opt @@@ -1,9 -1,14 +1,15 @@@ - disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi -nnumber_notation.cmi : ++disambiguateChoices.cmx : \ ++ nnumber_notation.cmx \ ++ disambiguateChoices.cmi disambiguateChoices.cmi : -nCicDisambiguate.cmi : -grafiteDisambiguate.cmi : -nnumber_notation.cmo : nnumber_notation.cmi -nnumber_notation.cmx : nnumber_notation.cmi -disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi -disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi -nCicDisambiguate.cmo : nCicDisambiguate.cmi -nCicDisambiguate.cmx : nCicDisambiguate.cmi -grafiteDisambiguate.cmo : nCicDisambiguate.cmi disambiguateChoices.cmi \ - grafiteDisambiguate.cmi --grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \ ++grafiteDisambiguate.cmx : \ ++ nCicDisambiguate.cmx \ ++ disambiguateChoices.cmx \ grafiteDisambiguate.cmi +grafiteDisambiguate.cmi : - nCicDisambiguate.cmx : nCicDisambiguate.cmi ++nCicDisambiguate.cmx : \ ++ nCicDisambiguate.cmi +nCicDisambiguate.cmi : - nnumber_notation.cmx : nnumber_notation.cmi ++nnumber_notation.cmx : \ ++ nnumber_notation.cmi +nnumber_notation.cmi : diff --cc matita/components/ng_extraction/.depend index 144c13d55,c2ad6ff86..d5062ccd7 --- a/matita/components/ng_extraction/.depend +++ b/matita/components/ng_extraction/.depend @@@ -1,32 -1,34 +1,101 @@@ - common.cmo : ocamlExtractionTable.cmi mlutil.cmi coq.cmi common.cmi - common.cmx : ocamlExtractionTable.cmx mlutil.cmx coq.cmx common.cmi - common.cmi : ocamlExtractionTable.cmi coq.cmi -nCicExtraction.cmi : -coq.cmi : -ocamlExtractionTable.cmi : miniml.cmo coq.cmi -mlutil.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi -common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi -extraction.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi -ocaml.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi -ocamlExtraction.cmi : ocamlExtractionTable.cmi -miniml.cmo : coq.cmi -miniml.cmx : coq.cmx -nCicExtraction.cmo : nCicExtraction.cmi -nCicExtraction.cmx : nCicExtraction.cmi --coq.cmo : coq.cmi --coq.cmx : coq.cmi -ocamlExtractionTable.cmo : miniml.cmo coq.cmi ocamlExtractionTable.cmi -ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi -mlutil.cmo : ocamlExtractionTable.cmi miniml.cmo coq.cmi mlutil.cmi -mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi -common.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \ ++common.cmo : \ ++ ocamlExtractionTable.cmi \ ++ mlutil.cmi \ ++ coq.cmi \ + common.cmi -common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ ++common.cmx : \ ++ ocamlExtractionTable.cmx \ ++ mlutil.cmx \ ++ coq.cmx \ + common.cmi -extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \ - common.cmi extraction.cmi -extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx extraction.cmi -ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \ - common.cmi ocaml.cmi -ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx ocaml.cmi -ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \ - coq.cmi ocamlExtraction.cmi -ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \ - coq.cmx ocamlExtraction.cmi ++common.cmi : \ ++ ocamlExtractionTable.cmi \ ++ coq.cmi ++coq.cmo : \ ++ coq.cmi ++coq.cmx : \ ++ coq.cmi +coq.cmi : - extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \ - common.cmi extraction.cmi - extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx extraction.cmi - extraction.cmi : ocamlExtractionTable.cmi miniml.cmo - miniml.cmo : coq.cmi - miniml.cmx : coq.cmx - mlutil.cmo : ocamlExtractionTable.cmi miniml.cmo coq.cmi mlutil.cmi - mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi - mlutil.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi - nCicExtraction.cmo : nCicExtraction.cmi - nCicExtraction.cmx : nCicExtraction.cmi ++extraction.cmo : \ ++ ocamlExtractionTable.cmi \ ++ mlutil.cmi \ ++ miniml.cmo \ ++ coq.cmi \ ++ common.cmi \ ++ extraction.cmi ++extraction.cmx : \ ++ ocamlExtractionTable.cmx \ ++ mlutil.cmx \ ++ miniml.cmx \ ++ coq.cmx \ ++ common.cmx \ ++ extraction.cmi ++extraction.cmi : \ ++ ocamlExtractionTable.cmi \ ++ miniml.cmo ++miniml.cmo : \ ++ coq.cmi ++miniml.cmx : \ ++ coq.cmx ++mlutil.cmo : \ ++ ocamlExtractionTable.cmi \ ++ miniml.cmo \ ++ coq.cmi \ ++ mlutil.cmi ++mlutil.cmx : \ ++ ocamlExtractionTable.cmx \ ++ miniml.cmx \ ++ coq.cmx \ ++ mlutil.cmi ++mlutil.cmi : \ ++ ocamlExtractionTable.cmi \ ++ miniml.cmo \ ++ coq.cmi ++nCicExtraction.cmo : \ ++ nCicExtraction.cmi ++nCicExtraction.cmx : \ ++ nCicExtraction.cmi +nCicExtraction.cmi : - ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \ - common.cmi ocaml.cmi - ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx ocaml.cmi - ocaml.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi - ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \ - coq.cmi ocamlExtraction.cmi - ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \ - coq.cmx ocamlExtraction.cmi - ocamlExtraction.cmi : ocamlExtractionTable.cmi - ocamlExtractionTable.cmo : miniml.cmo coq.cmi ocamlExtractionTable.cmi - ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi - ocamlExtractionTable.cmi : miniml.cmo coq.cmi ++ocaml.cmo : \ ++ ocamlExtractionTable.cmi \ ++ mlutil.cmi \ ++ miniml.cmo \ ++ coq.cmi \ ++ common.cmi \ ++ ocaml.cmi ++ocaml.cmx : \ ++ ocamlExtractionTable.cmx \ ++ mlutil.cmx \ ++ miniml.cmx \ ++ coq.cmx \ ++ common.cmx \ ++ ocaml.cmi ++ocaml.cmi : \ ++ ocamlExtractionTable.cmi \ ++ miniml.cmo \ ++ coq.cmi ++ocamlExtraction.cmo : \ ++ ocamlExtractionTable.cmi \ ++ ocaml.cmi \ ++ extraction.cmi \ ++ coq.cmi \ ++ ocamlExtraction.cmi ++ocamlExtraction.cmx : \ ++ ocamlExtractionTable.cmx \ ++ ocaml.cmx \ ++ extraction.cmx \ ++ coq.cmx \ ++ ocamlExtraction.cmi ++ocamlExtraction.cmi : \ ++ ocamlExtractionTable.cmi ++ocamlExtractionTable.cmo : \ ++ miniml.cmo \ ++ coq.cmi \ ++ ocamlExtractionTable.cmi ++ocamlExtractionTable.cmx : \ ++ miniml.cmx \ ++ coq.cmx \ ++ ocamlExtractionTable.cmi ++ocamlExtractionTable.cmi : \ ++ miniml.cmo \ ++ coq.cmi diff --cc matita/components/ng_extraction/.depend.opt index 3b0b9b57c,968d8ffe9..a527ad0c4 --- a/matita/components/ng_extraction/.depend.opt +++ b/matita/components/ng_extraction/.depend.opt @@@ -1,20 -1,34 +1,61 @@@ - common.cmx : ocamlExtractionTable.cmx mlutil.cmx coq.cmx common.cmi - common.cmi : ocamlExtractionTable.cmi coq.cmi -nCicExtraction.cmi : -coq.cmi : -ocamlExtractionTable.cmi : miniml.cmx coq.cmi -mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi -common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi -extraction.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi -ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi -ocamlExtraction.cmi : ocamlExtractionTable.cmi -miniml.cmo : coq.cmi -miniml.cmx : coq.cmx -nCicExtraction.cmo : nCicExtraction.cmi -nCicExtraction.cmx : nCicExtraction.cmi -coq.cmo : coq.cmi --coq.cmx : coq.cmi -ocamlExtractionTable.cmo : miniml.cmx coq.cmi ocamlExtractionTable.cmi -ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi -mlutil.cmo : ocamlExtractionTable.cmi miniml.cmx coq.cmi mlutil.cmi -mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi -common.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \ - common.cmi -common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ ++common.cmx : \ ++ ocamlExtractionTable.cmx \ ++ mlutil.cmx \ ++ coq.cmx \ + common.cmi -extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \ - common.cmi extraction.cmi -extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx extraction.cmi -ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \ - common.cmi ocaml.cmi -ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx ocaml.cmi -ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \ - coq.cmi ocamlExtraction.cmi -ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \ - coq.cmx ocamlExtraction.cmi ++common.cmi : \ ++ ocamlExtractionTable.cmi \ ++ coq.cmi ++coq.cmx : \ ++ coq.cmi +coq.cmi : - extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx extraction.cmi - extraction.cmi : ocamlExtractionTable.cmi miniml.cmx - miniml.cmx : coq.cmx - mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi - mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi - nCicExtraction.cmx : nCicExtraction.cmi ++extraction.cmx : \ ++ ocamlExtractionTable.cmx \ ++ mlutil.cmx \ ++ miniml.cmx \ ++ coq.cmx \ ++ common.cmx \ ++ extraction.cmi ++extraction.cmi : \ ++ ocamlExtractionTable.cmi \ ++ miniml.cmx ++miniml.cmx : \ ++ coq.cmx ++mlutil.cmx : \ ++ ocamlExtractionTable.cmx \ ++ miniml.cmx \ ++ coq.cmx \ ++ mlutil.cmi ++mlutil.cmi : \ ++ ocamlExtractionTable.cmi \ ++ miniml.cmx \ ++ coq.cmi ++nCicExtraction.cmx : \ ++ nCicExtraction.cmi +nCicExtraction.cmi : - ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx ocaml.cmi - ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi - ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \ - coq.cmx ocamlExtraction.cmi - ocamlExtraction.cmi : ocamlExtractionTable.cmi - ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi - ocamlExtractionTable.cmi : miniml.cmx coq.cmi ++ocaml.cmx : \ ++ ocamlExtractionTable.cmx \ ++ mlutil.cmx \ ++ miniml.cmx \ ++ coq.cmx \ ++ common.cmx \ ++ ocaml.cmi ++ocaml.cmi : \ ++ ocamlExtractionTable.cmi \ ++ miniml.cmx \ ++ coq.cmi ++ocamlExtraction.cmx : \ ++ ocamlExtractionTable.cmx \ ++ ocaml.cmx \ ++ extraction.cmx \ ++ coq.cmx \ ++ ocamlExtraction.cmi ++ocamlExtraction.cmi : \ ++ ocamlExtractionTable.cmi ++ocamlExtractionTable.cmx : \ ++ miniml.cmx \ ++ coq.cmx \ ++ ocamlExtractionTable.cmi ++ocamlExtractionTable.cmi : \ ++ miniml.cmx \ ++ coq.cmi diff --cc matita/components/ng_extraction/mlutil.ml index 01a0cd85d,52881e183..9f553762a --- a/matita/components/ng_extraction/mlutil.ml +++ b/matita/components/ng_extraction/mlutil.ml @@@ -1242,7 -1242,7 +1242,7 @@@ and ml_size_array l = Array.fold_left ( let n = List.length i in let cand = lift n cand in let cand = pop n (non_stricts add cand t) in - List.merge (compare) cand c) [] v - List.merge (fun c1 c2 -> c1 - c2) cand c) [] v ++ List.merge (-) cand c) [] v (* [merge] may duplicates some indices, but I don't mind. *) | MLmagic t -> non_stricts add cand t diff --cc matita/components/ng_kernel/.depend index ca1b782f6,a55f87284..aa395ccc3 --- a/matita/components/ng_kernel/.depend +++ b/matita/components/ng_kernel/.depend @@@ -1,39 -1,41 +1,126 @@@ - nCic.cmo : nUri.cmi nReference.cmi - nCic.cmx : nUri.cmx nReference.cmx - nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi - nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi -nUri.cmi : -nReference.cmi : nUri.cmi -nCicUtils.cmi : nCic.cmo -nCicSubstitution.cmi : nCic.cmo --nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmo - nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ - nCicEnvironment.cmi nCic.cmo nCicPp.cmi - nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi - nCicPp.cmi : nReference.cmi nCic.cmo - nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicEnvironment.cmi nCic.cmo nCicReduction.cmi - nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi --nCicReduction.cmi : nCic.cmo - nCicSubstitution.cmo : nCicUtils.cmi nCic.cmo nCicSubstitution.cmi - nCicSubstitution.cmx : nCicUtils.cmx nCic.cmx nCicSubstitution.cmi - nCicSubstitution.cmi : nCic.cmo - nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \ - nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmo \ -nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmo -nCicUntrusted.cmi : nCic.cmo -nCicPp.cmi : nReference.cmi nCic.cmo -nCic.cmo : nUri.cmi nReference.cmi -nCic.cmx : nUri.cmx nReference.cmx -nUri.cmo : nUri.cmi -nUri.cmx : nUri.cmi -nReference.cmo : nUri.cmi nReference.cmi -nReference.cmx : nUri.cmx nReference.cmi -nCicUtils.cmo : nReference.cmi nCic.cmo nCicUtils.cmi -nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi -nCicSubstitution.cmo : nReference.cmi nCicUtils.cmi nCic.cmo \ ++nCic.cmo : \ ++ nUri.cmi \ ++ nReference.cmi ++nCic.cmx : \ ++ nUri.cmx \ ++ nReference.cmx ++nCicEnvironment.cmo : \ ++ nUri.cmi \ ++ nReference.cmi \ ++ nCic.cmo \ ++ nCicEnvironment.cmi ++nCicEnvironment.cmx : \ ++ nUri.cmx \ ++ nReference.cmx \ ++ nCic.cmx \ ++ nCicEnvironment.cmi ++nCicEnvironment.cmi : \ ++ nUri.cmi \ ++ nReference.cmi \ ++ nCic.cmo ++nCicPp.cmo : \ ++ nUri.cmi \ ++ nReference.cmi \ ++ nCicSubstitution.cmi \ ++ nCicReduction.cmi \ ++ nCicEnvironment.cmi \ ++ nCic.cmo \ ++ nCicPp.cmi ++nCicPp.cmx : \ ++ nUri.cmx \ ++ nReference.cmx \ ++ nCicSubstitution.cmx \ ++ nCicReduction.cmx \ ++ nCicEnvironment.cmx \ ++ nCic.cmx \ ++ nCicPp.cmi ++nCicPp.cmi : \ ++ nReference.cmi \ ++ nCic.cmo ++nCicReduction.cmo : \ ++ nReference.cmi \ ++ nCicUtils.cmi \ ++ nCicSubstitution.cmi \ ++ nCicEnvironment.cmi \ ++ nCic.cmo \ ++ nCicReduction.cmi ++nCicReduction.cmx : \ ++ nReference.cmx \ ++ nCicUtils.cmx \ ++ nCicSubstitution.cmx \ ++ nCicEnvironment.cmx \ ++ nCic.cmx \ ++ nCicReduction.cmi ++nCicReduction.cmi : \ ++ nCic.cmo ++nCicSubstitution.cmo : \ ++ nCicUtils.cmi \ ++ nCic.cmo \ + nCicSubstitution.cmi -nCicSubstitution.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \ ++nCicSubstitution.cmx : \ ++ nCicUtils.cmx \ ++ nCic.cmx \ + nCicSubstitution.cmi -nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi -nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi -nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicEnvironment.cmi nCic.cmo nCicReduction.cmi -nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi -nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \ - nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmo \ ++nCicSubstitution.cmi : \ ++ nCic.cmo ++nCicTypeChecker.cmo : \ ++ nUri.cmi \ ++ nReference.cmi \ ++ nCicUtils.cmi \ ++ nCicSubstitution.cmi \ ++ nCicReduction.cmi \ ++ nCicEnvironment.cmi \ ++ nCic.cmo \ nCicTypeChecker.cmi --nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \ -- nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ ++nCicTypeChecker.cmx : \ ++ nUri.cmx \ ++ nReference.cmx \ ++ nCicUtils.cmx \ ++ nCicSubstitution.cmx \ ++ nCicReduction.cmx \ ++ nCicEnvironment.cmx \ ++ nCic.cmx \ nCicTypeChecker.cmi - nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmo --nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ -- nCicReduction.cmi nCicEnvironment.cmi nCic.cmo nCicUntrusted.cmi --nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ -- nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi - nCicUntrusted.cmi : nCic.cmo - nCicUtils.cmo : nCic.cmo nCicUtils.cmi - nCicUtils.cmx : nCic.cmx nCicUtils.cmi - nCicUtils.cmi : nCic.cmo - nReference.cmo : nUri.cmi nReference.cmi - nReference.cmx : nUri.cmx nReference.cmi - nReference.cmi : nUri.cmi - nUri.cmo : nUri.cmi - nUri.cmx : nUri.cmi -nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ - nCicEnvironment.cmi nCic.cmo nCicPp.cmi -nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi ++nCicTypeChecker.cmi : \ ++ nUri.cmi \ ++ nReference.cmi \ ++ nCic.cmo ++nCicUntrusted.cmo : \ ++ nReference.cmi \ ++ nCicUtils.cmi \ ++ nCicSubstitution.cmi \ ++ nCicReduction.cmi \ ++ nCicEnvironment.cmi \ ++ nCic.cmo \ ++ nCicUntrusted.cmi ++nCicUntrusted.cmx : \ ++ nReference.cmx \ ++ nCicUtils.cmx \ ++ nCicSubstitution.cmx \ ++ nCicReduction.cmx \ ++ nCicEnvironment.cmx \ ++ nCic.cmx \ ++ nCicUntrusted.cmi ++nCicUntrusted.cmi : \ ++ nCic.cmo ++nCicUtils.cmo : \ ++ nCic.cmo \ ++ nCicUtils.cmi ++nCicUtils.cmx : \ ++ nCic.cmx \ ++ nCicUtils.cmi ++nCicUtils.cmi : \ ++ nCic.cmo ++nReference.cmo : \ ++ nUri.cmi \ ++ nReference.cmi ++nReference.cmx : \ ++ nUri.cmx \ ++ nReference.cmi ++nReference.cmi : \ ++ nUri.cmi ++nUri.cmo : \ ++ nUri.cmi ++nUri.cmx : \ ++ nUri.cmi +nUri.cmi : diff --cc matita/components/ng_kernel/.depend.opt index 97f4e283a,5b0507784..fe01e3cc1 --- a/matita/components/ng_kernel/.depend.opt +++ b/matita/components/ng_kernel/.depend.opt @@@ -1,24 -1,41 +1,74 @@@ - nCic.cmx : nUri.cmx nReference.cmx - nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi -nUri.cmi : -nReference.cmi : nUri.cmi -nCicUtils.cmi : nCic.cmx -nCicSubstitution.cmi : nCic.cmx --nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmx - nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi - nCicPp.cmi : nReference.cmi nCic.cmx - nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi --nCicReduction.cmi : nCic.cmx - nCicSubstitution.cmx : nCicUtils.cmx nCic.cmx nCicSubstitution.cmi - nCicSubstitution.cmi : nCic.cmx - nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \ - nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ -nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx -nCicUntrusted.cmi : nCic.cmx -nCicPp.cmi : nReference.cmi nCic.cmx -nCic.cmo : nUri.cmi nReference.cmi -nCic.cmx : nUri.cmx nReference.cmx -nUri.cmo : nUri.cmi -nUri.cmx : nUri.cmi -nReference.cmo : nUri.cmi nReference.cmi -nReference.cmx : nUri.cmx nReference.cmi -nCicUtils.cmo : nReference.cmi nCic.cmx nCicUtils.cmi -nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi -nCicSubstitution.cmo : nReference.cmi nCicUtils.cmi nCic.cmx \ - nCicSubstitution.cmi -nCicSubstitution.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \ ++nCic.cmx : \ ++ nUri.cmx \ ++ nReference.cmx ++nCicEnvironment.cmx : \ ++ nUri.cmx \ ++ nReference.cmx \ ++ nCic.cmx \ ++ nCicEnvironment.cmi ++nCicEnvironment.cmi : \ ++ nUri.cmi \ ++ nReference.cmi \ ++ nCic.cmx ++nCicPp.cmx : \ ++ nUri.cmx \ ++ nReference.cmx \ ++ nCicSubstitution.cmx \ ++ nCicReduction.cmx \ ++ nCicEnvironment.cmx \ ++ nCic.cmx \ ++ nCicPp.cmi ++nCicPp.cmi : \ ++ nReference.cmi \ ++ nCic.cmx ++nCicReduction.cmx : \ ++ nReference.cmx \ ++ nCicUtils.cmx \ ++ nCicSubstitution.cmx \ ++ nCicEnvironment.cmx \ ++ nCic.cmx \ ++ nCicReduction.cmi ++nCicReduction.cmi : \ ++ nCic.cmx ++nCicSubstitution.cmx : \ ++ nCicUtils.cmx \ ++ nCic.cmx \ + nCicSubstitution.cmi -nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi -nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi -nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicEnvironment.cmi nCic.cmx nCicReduction.cmi -nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi -nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \ - nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \ ++nCicSubstitution.cmi : \ ++ nCic.cmx ++nCicTypeChecker.cmx : \ ++ nUri.cmx \ ++ nReference.cmx \ ++ nCicUtils.cmx \ ++ nCicSubstitution.cmx \ ++ nCicReduction.cmx \ ++ nCicEnvironment.cmx \ ++ nCic.cmx \ nCicTypeChecker.cmi - nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx -nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \ - nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ - nCicTypeChecker.cmi -nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi --nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ -- nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi - nCicUntrusted.cmi : nCic.cmx - nCicUtils.cmx : nCic.cmx nCicUtils.cmi - nCicUtils.cmi : nCic.cmx - nReference.cmx : nUri.cmx nReference.cmi - nReference.cmi : nUri.cmi - nUri.cmx : nUri.cmi -nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ - nCicEnvironment.cmi nCic.cmx nCicPp.cmi -nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi ++nCicTypeChecker.cmi : \ ++ nUri.cmi \ ++ nReference.cmi \ ++ nCic.cmx ++nCicUntrusted.cmx : \ ++ nReference.cmx \ ++ nCicUtils.cmx \ ++ nCicSubstitution.cmx \ ++ nCicReduction.cmx \ ++ nCicEnvironment.cmx \ ++ nCic.cmx \ ++ nCicUntrusted.cmi ++nCicUntrusted.cmi : \ ++ nCic.cmx ++nCicUtils.cmx : \ ++ nCic.cmx \ ++ nCicUtils.cmi ++nCicUtils.cmi : \ ++ nCic.cmx ++nReference.cmx : \ ++ nUri.cmx \ ++ nReference.cmi ++nReference.cmi : \ ++ nUri.cmi ++nUri.cmx : \ ++ nUri.cmi +nUri.cmi : diff --cc matita/components/ng_library/.depend index d10bc6762,a571a865c..72fc77177 --- a/matita/components/ng_library/.depend +++ b/matita/components/ng_library/.depend @@@ -1,3 -1,3 +1,5 @@@ - nCicLibrary.cmo : nCicLibrary.cmi - nCicLibrary.cmx : nCicLibrary.cmi ++nCicLibrary.cmo : \ ++ nCicLibrary.cmi ++nCicLibrary.cmx : \ ++ nCicLibrary.cmi nCicLibrary.cmi : -nCicLibrary.cmo : nCicLibrary.cmi -nCicLibrary.cmx : nCicLibrary.cmi diff --cc matita/components/ng_library/.depend.opt index 07d53f5dd,a571a865c..ee5e8bd16 --- a/matita/components/ng_library/.depend.opt +++ b/matita/components/ng_library/.depend.opt @@@ -1,2 -1,3 +1,3 @@@ - nCicLibrary.cmx : nCicLibrary.cmi ++nCicLibrary.cmx : \ ++ nCicLibrary.cmi nCicLibrary.cmi : -nCicLibrary.cmo : nCicLibrary.cmi -nCicLibrary.cmx : nCicLibrary.cmi diff --cc matita/components/ng_paramodulation/.depend index be0690e45,5f4f1cc56..b9c453ab4 --- a/matita/components/ng_paramodulation/.depend +++ b/matita/components/ng_paramodulation/.depend @@@ -1,45 -1,45 +1,164 @@@ - foSubst.cmo : terms.cmi foSubst.cmi - foSubst.cmx : terms.cmx foSubst.cmi - foSubst.cmi : terms.cmi - foUnif.cmo : terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi - foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi - foUnif.cmi : terms.cmi orderings.cmi - foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi - foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi - foUtils.cmi : terms.cmi orderings.cmi - index.cmo : terms.cmi orderings.cmi foUtils.cmi index.cmi - index.cmx : terms.cmx orderings.cmx foUtils.cmx index.cmi - index.cmi : terms.cmi orderings.cmi - nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi - nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi - nCicBlob.cmi : terms.cmi - nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \ - nCicBlob.cmi nCicParamod.cmi - nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ - nCicBlob.cmx nCicParamod.cmi - nCicParamod.cmi : terms.cmi - nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi - nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi - nCicProof.cmi : terms.cmi - orderings.cmo : terms.cmi foSubst.cmi orderings.cmi - orderings.cmx : terms.cmx foSubst.cmx orderings.cmi - orderings.cmi : terms.cmi - paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ - foUtils.cmi paramod.cmi - paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx paramod.cmi - paramod.cmi : terms.cmi orderings.cmi - pp.cmo : terms.cmi pp.cmi - pp.cmx : terms.cmx pp.cmi - pp.cmi : terms.cmi - stats.cmo : terms.cmi stats.cmi - stats.cmx : terms.cmx stats.cmi - stats.cmi : terms.cmi orderings.cmi - superposition.cmo : terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ - foUnif.cmi foSubst.cmi superposition.cmi - superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ - foUnif.cmx foSubst.cmx superposition.cmi - superposition.cmi : terms.cmi orderings.cmi index.cmi - terms.cmo : terms.cmi - terms.cmx : terms.cmi ++foSubst.cmo : \ ++ terms.cmi \ ++ foSubst.cmi ++foSubst.cmx : \ ++ terms.cmx \ ++ foSubst.cmi ++foSubst.cmi : \ ++ terms.cmi ++foUnif.cmo : \ ++ terms.cmi \ ++ orderings.cmi \ ++ foUtils.cmi \ ++ foSubst.cmi \ ++ foUnif.cmi ++foUnif.cmx : \ ++ terms.cmx \ ++ orderings.cmx \ ++ foUtils.cmx \ ++ foSubst.cmx \ ++ foUnif.cmi ++foUnif.cmi : \ ++ terms.cmi \ ++ orderings.cmi ++foUtils.cmo : \ ++ terms.cmi \ ++ orderings.cmi \ ++ foSubst.cmi \ ++ foUtils.cmi ++foUtils.cmx : \ ++ terms.cmx \ ++ orderings.cmx \ ++ foSubst.cmx \ ++ foUtils.cmi ++foUtils.cmi : \ ++ terms.cmi \ ++ orderings.cmi ++index.cmo : \ ++ terms.cmi \ ++ orderings.cmi \ ++ foUtils.cmi \ ++ index.cmi ++index.cmx : \ ++ terms.cmx \ ++ orderings.cmx \ ++ foUtils.cmx \ ++ index.cmi ++index.cmi : \ ++ terms.cmi \ ++ orderings.cmi ++nCicBlob.cmo : \ ++ terms.cmi \ ++ foUtils.cmi \ ++ nCicBlob.cmi ++nCicBlob.cmx : \ ++ terms.cmx \ ++ foUtils.cmx \ ++ nCicBlob.cmi ++nCicBlob.cmi : \ ++ terms.cmi ++nCicParamod.cmo : \ ++ terms.cmi \ ++ pp.cmi \ ++ paramod.cmi \ ++ orderings.cmi \ ++ nCicProof.cmi \ ++ nCicBlob.cmi \ ++ nCicParamod.cmi ++nCicParamod.cmx : \ ++ terms.cmx \ ++ pp.cmx \ ++ paramod.cmx \ ++ orderings.cmx \ ++ nCicProof.cmx \ ++ nCicBlob.cmx \ ++ nCicParamod.cmi ++nCicParamod.cmi : \ ++ terms.cmi ++nCicProof.cmo : \ ++ terms.cmi \ ++ pp.cmi \ ++ nCicBlob.cmi \ ++ foSubst.cmi \ ++ nCicProof.cmi ++nCicProof.cmx : \ ++ terms.cmx \ ++ pp.cmx \ ++ nCicBlob.cmx \ ++ foSubst.cmx \ ++ nCicProof.cmi ++nCicProof.cmi : \ ++ terms.cmi ++orderings.cmo : \ ++ terms.cmi \ ++ foSubst.cmi \ ++ orderings.cmi ++orderings.cmx : \ ++ terms.cmx \ ++ foSubst.cmx \ ++ orderings.cmi ++orderings.cmi : \ ++ terms.cmi ++paramod.cmo : \ ++ terms.cmi \ ++ superposition.cmi \ ++ pp.cmi \ ++ orderings.cmi \ ++ index.cmi \ ++ foUtils.cmi \ ++ paramod.cmi ++paramod.cmx : \ ++ terms.cmx \ ++ superposition.cmx \ ++ pp.cmx \ ++ orderings.cmx \ ++ index.cmx \ ++ foUtils.cmx \ ++ paramod.cmi ++paramod.cmi : \ ++ terms.cmi \ ++ orderings.cmi ++pp.cmo : \ ++ terms.cmi \ ++ pp.cmi ++pp.cmx : \ ++ terms.cmx \ ++ pp.cmi ++pp.cmi : \ ++ terms.cmi ++stats.cmo : \ ++ terms.cmi \ ++ stats.cmi ++stats.cmx : \ ++ terms.cmx \ ++ stats.cmi ++stats.cmi : \ ++ terms.cmi \ ++ orderings.cmi ++superposition.cmo : \ ++ terms.cmi \ ++ pp.cmi \ ++ orderings.cmi \ ++ index.cmi \ ++ foUtils.cmi \ ++ foUnif.cmi \ ++ foSubst.cmi \ ++ superposition.cmi ++superposition.cmx : \ ++ terms.cmx \ ++ pp.cmx \ ++ orderings.cmx \ ++ index.cmx \ ++ foUtils.cmx \ ++ foUnif.cmx \ ++ foSubst.cmx \ ++ superposition.cmi ++superposition.cmi : \ ++ terms.cmi \ ++ orderings.cmi \ ++ index.cmi ++terms.cmo : \ ++ terms.cmi ++terms.cmx : \ ++ terms.cmi terms.cmi : -pp.cmi : terms.cmi -foSubst.cmi : terms.cmi -orderings.cmi : terms.cmi -foUtils.cmi : terms.cmi orderings.cmi -foUnif.cmi : terms.cmi orderings.cmi -index.cmi : terms.cmi orderings.cmi -superposition.cmi : terms.cmi orderings.cmi index.cmi -stats.cmi : terms.cmi orderings.cmi -paramod.cmi : terms.cmi orderings.cmi -nCicBlob.cmi : terms.cmi -nCicProof.cmi : terms.cmi -nCicParamod.cmi : terms.cmi -terms.cmo : terms.cmi -terms.cmx : terms.cmi -pp.cmo : terms.cmi pp.cmi -pp.cmx : terms.cmx pp.cmi -foSubst.cmo : terms.cmi foSubst.cmi -foSubst.cmx : terms.cmx foSubst.cmi -orderings.cmo : terms.cmi pp.cmi foSubst.cmi orderings.cmi -orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi -foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi -foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi -foUnif.cmo : terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi -foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi -index.cmo : terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi -index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi -superposition.cmo : terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ - foUnif.cmi foSubst.cmi superposition.cmi -superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ - foUnif.cmx foSubst.cmx superposition.cmi -stats.cmo : terms.cmi stats.cmi -stats.cmx : terms.cmx stats.cmi -paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ - foUtils.cmi foUnif.cmi paramod.cmi -paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi -nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi -nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi -nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi -nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi -nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \ - nCicBlob.cmi nCicParamod.cmi -nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ - nCicBlob.cmx nCicParamod.cmi diff --cc matita/components/ng_paramodulation/.depend.opt index 9593d8958,5f4f1cc56..32cbf605d --- a/matita/components/ng_paramodulation/.depend.opt +++ b/matita/components/ng_paramodulation/.depend.opt @@@ -1,29 -1,45 +1,98 @@@ - foSubst.cmx : terms.cmx foSubst.cmi - foSubst.cmi : terms.cmi - foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi - foUnif.cmi : terms.cmi orderings.cmi - foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi - foUtils.cmi : terms.cmi orderings.cmi - index.cmx : terms.cmx orderings.cmx foUtils.cmx index.cmi - index.cmi : terms.cmi orderings.cmi - nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi - nCicBlob.cmi : terms.cmi - nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ - nCicBlob.cmx nCicParamod.cmi - nCicParamod.cmi : terms.cmi - nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi - nCicProof.cmi : terms.cmi - orderings.cmx : terms.cmx foSubst.cmx orderings.cmi - orderings.cmi : terms.cmi - paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx paramod.cmi - paramod.cmi : terms.cmi orderings.cmi - pp.cmx : terms.cmx pp.cmi - pp.cmi : terms.cmi - stats.cmx : terms.cmx stats.cmi - stats.cmi : terms.cmi orderings.cmi - superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ - foUnif.cmx foSubst.cmx superposition.cmi - superposition.cmi : terms.cmi orderings.cmi index.cmi - terms.cmx : terms.cmi ++foSubst.cmx : \ ++ terms.cmx \ ++ foSubst.cmi ++foSubst.cmi : \ ++ terms.cmi ++foUnif.cmx : \ ++ terms.cmx \ ++ orderings.cmx \ ++ foUtils.cmx \ ++ foSubst.cmx \ ++ foUnif.cmi ++foUnif.cmi : \ ++ terms.cmi \ ++ orderings.cmi ++foUtils.cmx : \ ++ terms.cmx \ ++ orderings.cmx \ ++ foSubst.cmx \ ++ foUtils.cmi ++foUtils.cmi : \ ++ terms.cmi \ ++ orderings.cmi ++index.cmx : \ ++ terms.cmx \ ++ orderings.cmx \ ++ foUtils.cmx \ ++ index.cmi ++index.cmi : \ ++ terms.cmi \ ++ orderings.cmi ++nCicBlob.cmx : \ ++ terms.cmx \ ++ foUtils.cmx \ ++ nCicBlob.cmi ++nCicBlob.cmi : \ ++ terms.cmi ++nCicParamod.cmx : \ ++ terms.cmx \ ++ pp.cmx \ ++ paramod.cmx \ ++ orderings.cmx \ ++ nCicProof.cmx \ ++ nCicBlob.cmx \ ++ nCicParamod.cmi ++nCicParamod.cmi : \ ++ terms.cmi ++nCicProof.cmx : \ ++ terms.cmx \ ++ pp.cmx \ ++ nCicBlob.cmx \ ++ foSubst.cmx \ ++ nCicProof.cmi ++nCicProof.cmi : \ ++ terms.cmi ++orderings.cmx : \ ++ terms.cmx \ ++ foSubst.cmx \ ++ orderings.cmi ++orderings.cmi : \ ++ terms.cmi ++paramod.cmx : \ ++ terms.cmx \ ++ superposition.cmx \ ++ pp.cmx \ ++ orderings.cmx \ ++ index.cmx \ ++ foUtils.cmx \ ++ paramod.cmi ++paramod.cmi : \ ++ terms.cmi \ ++ orderings.cmi ++pp.cmx : \ ++ terms.cmx \ ++ pp.cmi ++pp.cmi : \ ++ terms.cmi ++stats.cmx : \ ++ terms.cmx \ ++ stats.cmi ++stats.cmi : \ ++ terms.cmi \ ++ orderings.cmi ++superposition.cmx : \ ++ terms.cmx \ ++ pp.cmx \ ++ orderings.cmx \ ++ index.cmx \ ++ foUtils.cmx \ ++ foUnif.cmx \ ++ foSubst.cmx \ ++ superposition.cmi ++superposition.cmi : \ ++ terms.cmi \ ++ orderings.cmi \ ++ index.cmi ++terms.cmx : \ ++ terms.cmi terms.cmi : -pp.cmi : terms.cmi -foSubst.cmi : terms.cmi -orderings.cmi : terms.cmi -foUtils.cmi : terms.cmi orderings.cmi -foUnif.cmi : terms.cmi orderings.cmi -index.cmi : terms.cmi orderings.cmi -superposition.cmi : terms.cmi orderings.cmi index.cmi -stats.cmi : terms.cmi orderings.cmi -paramod.cmi : terms.cmi orderings.cmi -nCicBlob.cmi : terms.cmi -nCicProof.cmi : terms.cmi -nCicParamod.cmi : terms.cmi -terms.cmo : terms.cmi -terms.cmx : terms.cmi -pp.cmo : terms.cmi pp.cmi -pp.cmx : terms.cmx pp.cmi -foSubst.cmo : terms.cmi foSubst.cmi -foSubst.cmx : terms.cmx foSubst.cmi -orderings.cmo : terms.cmi pp.cmi foSubst.cmi orderings.cmi -orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi -foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi -foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi -foUnif.cmo : terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi -foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi -index.cmo : terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi -index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi -superposition.cmo : terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ - foUnif.cmi foSubst.cmi superposition.cmi -superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ - foUnif.cmx foSubst.cmx superposition.cmi -stats.cmo : terms.cmi stats.cmi -stats.cmx : terms.cmx stats.cmi -paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ - foUtils.cmi foUnif.cmi paramod.cmi -paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi -nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi -nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi -nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi -nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi -nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \ - nCicBlob.cmi nCicParamod.cmi -nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ - nCicBlob.cmx nCicParamod.cmi diff --cc matita/components/ng_refiner/.depend index 2bd075dfc,d8295760a..6d211ffe5 --- a/matita/components/ng_refiner/.depend +++ b/matita/components/ng_refiner/.depend @@@ -1,27 -1,27 +1,62 @@@ - nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \ - nCicMetaSubst.cmi nCicCoercion.cmi - nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \ - nCicMetaSubst.cmx nCicCoercion.cmi - nCicCoercion.cmi : nCicUnifHint.cmi - nCicMetaSubst.cmo : nCicMetaSubst.cmi - nCicMetaSubst.cmx : nCicMetaSubst.cmi -nDiscriminationTree.cmi : ++nCicCoercion.cmo : \ ++ nDiscriminationTree.cmi \ ++ nCicUnifHint.cmi \ ++ nCicMetaSubst.cmi \ ++ nCicCoercion.cmi ++nCicCoercion.cmx : \ ++ nDiscriminationTree.cmx \ ++ nCicUnifHint.cmx \ ++ nCicMetaSubst.cmx \ ++ nCicCoercion.cmi ++nCicCoercion.cmi : \ ++ nCicUnifHint.cmi ++nCicMetaSubst.cmo : \ ++ nCicMetaSubst.cmi ++nCicMetaSubst.cmx : \ ++ nCicMetaSubst.cmi nCicMetaSubst.cmi : - nCicRefineUtil.cmo : nCicMetaSubst.cmi nCicRefineUtil.cmi - nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi -nCicUnifHint.cmi : -nCicCoercion.cmi : nCicUnifHint.cmi ++nCicRefineUtil.cmo : \ ++ nCicMetaSubst.cmi \ ++ nCicRefineUtil.cmi ++nCicRefineUtil.cmx : \ ++ nCicMetaSubst.cmx \ ++ nCicRefineUtil.cmi nCicRefineUtil.cmi : - nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \ - nCicCoercion.cmi nCicRefiner.cmi - nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicRefiner.cmi -nCicUnification.cmi : nCicCoercion.cmi --nCicRefiner.cmi : nCicCoercion.cmi -nDiscriminationTree.cmo : nDiscriminationTree.cmi -nDiscriminationTree.cmx : nDiscriminationTree.cmi -nCicMetaSubst.cmo : nCicMetaSubst.cmi -nCicMetaSubst.cmx : nCicMetaSubst.cmi --nCicUnifHint.cmo : nDiscriminationTree.cmi nCicMetaSubst.cmi \ ++nCicRefiner.cmo : \ ++ nCicUnification.cmi \ ++ nCicRefineUtil.cmi \ ++ nCicMetaSubst.cmi \ ++ nCicCoercion.cmi \ ++ nCicRefiner.cmi ++nCicRefiner.cmx : \ ++ nCicUnification.cmx \ ++ nCicRefineUtil.cmx \ ++ nCicMetaSubst.cmx \ ++ nCicCoercion.cmx \ ++ nCicRefiner.cmi ++nCicRefiner.cmi : \ ++ nCicCoercion.cmi ++nCicUnifHint.cmo : \ ++ nDiscriminationTree.cmi \ ++ nCicMetaSubst.cmi \ nCicUnifHint.cmi --nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \ ++nCicUnifHint.cmx : \ ++ nDiscriminationTree.cmx \ ++ nCicMetaSubst.cmx \ nCicUnifHint.cmi -nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \ - nCicMetaSubst.cmi nCicCoercion.cmi -nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \ - nCicMetaSubst.cmx nCicCoercion.cmi -nCicRefineUtil.cmo : nCicMetaSubst.cmi nCicRefineUtil.cmi -nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi -nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi -nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi -nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \ - nCicCoercion.cmi nCicRefiner.cmi -nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicRefiner.cmi +nCicUnifHint.cmi : - nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi - nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi - nCicUnification.cmi : nCicCoercion.cmi - nDiscriminationTree.cmo : nDiscriminationTree.cmi - nDiscriminationTree.cmx : nDiscriminationTree.cmi ++nCicUnification.cmo : \ ++ nCicUnifHint.cmi \ ++ nCicMetaSubst.cmi \ ++ nCicUnification.cmi ++nCicUnification.cmx : \ ++ nCicUnifHint.cmx \ ++ nCicMetaSubst.cmx \ ++ nCicUnification.cmi ++nCicUnification.cmi : \ ++ nCicCoercion.cmi ++nDiscriminationTree.cmo : \ ++ nDiscriminationTree.cmi ++nDiscriminationTree.cmx : \ ++ nDiscriminationTree.cmi +nDiscriminationTree.cmi : diff --cc matita/components/ng_refiner/.depend.opt index dab873890,d8295760a..a25cbdb11 --- a/matita/components/ng_refiner/.depend.opt +++ b/matita/components/ng_refiner/.depend.opt @@@ -1,17 -1,27 +1,36 @@@ - nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \ - nCicMetaSubst.cmx nCicCoercion.cmi - nCicCoercion.cmi : nCicUnifHint.cmi - nCicMetaSubst.cmx : nCicMetaSubst.cmi -nDiscriminationTree.cmi : ++nCicCoercion.cmx : \ ++ nDiscriminationTree.cmx \ ++ nCicUnifHint.cmx \ ++ nCicMetaSubst.cmx \ ++ nCicCoercion.cmi ++nCicCoercion.cmi : \ ++ nCicUnifHint.cmi ++nCicMetaSubst.cmx : \ ++ nCicMetaSubst.cmi nCicMetaSubst.cmi : - nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi -nCicUnifHint.cmi : -nCicCoercion.cmi : nCicUnifHint.cmi ++nCicRefineUtil.cmx : \ ++ nCicMetaSubst.cmx \ ++ nCicRefineUtil.cmi nCicRefineUtil.cmi : - nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicRefiner.cmi -nCicUnification.cmi : nCicCoercion.cmi --nCicRefiner.cmi : nCicCoercion.cmi - nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \ -nDiscriminationTree.cmo : nDiscriminationTree.cmi -nDiscriminationTree.cmx : nDiscriminationTree.cmi -nCicMetaSubst.cmo : nCicMetaSubst.cmi -nCicMetaSubst.cmx : nCicMetaSubst.cmi -nCicUnifHint.cmo : nDiscriminationTree.cmi nCicMetaSubst.cmi \ ++nCicRefiner.cmx : \ ++ nCicUnification.cmx \ ++ nCicRefineUtil.cmx \ ++ nCicMetaSubst.cmx \ ++ nCicCoercion.cmx \ ++ nCicRefiner.cmi ++nCicRefiner.cmi : \ ++ nCicCoercion.cmi ++nCicUnifHint.cmx : \ ++ nDiscriminationTree.cmx \ ++ nCicMetaSubst.cmx \ nCicUnifHint.cmi -nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \ - nCicUnifHint.cmi -nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \ - nCicMetaSubst.cmi nCicCoercion.cmi -nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \ - nCicMetaSubst.cmx nCicCoercion.cmi -nCicRefineUtil.cmo : nCicMetaSubst.cmi nCicRefineUtil.cmi -nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi -nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi -nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi -nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \ - nCicCoercion.cmi nCicRefiner.cmi -nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicRefiner.cmi +nCicUnifHint.cmi : - nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi - nCicUnification.cmi : nCicCoercion.cmi - nDiscriminationTree.cmx : nDiscriminationTree.cmi ++nCicUnification.cmx : \ ++ nCicUnifHint.cmx \ ++ nCicMetaSubst.cmx \ ++ nCicUnification.cmi ++nCicUnification.cmi : \ ++ nCicCoercion.cmi ++nDiscriminationTree.cmx : \ ++ nDiscriminationTree.cmi +nDiscriminationTree.cmi : diff --cc matita/components/ng_tactics/.depend index 90de5733d,57784f373..4d386aaa4 --- a/matita/components/ng_tactics/.depend +++ b/matita/components/ng_tactics/.depend @@@ -1,30 -1,35 +1,94 @@@ --continuationals.cmo : continuationals.cmi --continuationals.cmx : continuationals.cmi ++continuationals.cmo : \ ++ continuationals.cmi ++continuationals.cmx : \ ++ continuationals.cmi continuationals.cmi : -declarative.cmo : nnAuto.cmi nTactics.cmi nTacStatus.cmi nCicElim.cmi \ - continuationals.cmi declarative.cmi -declarative.cmx : nnAuto.cmx nTactics.cmx nTacStatus.cmx nCicElim.cmx \ - continuationals.cmx declarative.cmi -declarative.cmi : nnAuto.cmi nTacStatus.cmi --nCicElim.cmo : nCicElim.cmi --nCicElim.cmx : nCicElim.cmi ++declarative.cmo : \ ++ nnAuto.cmi \ ++ nTactics.cmi \ ++ nTacStatus.cmi \ ++ nCicElim.cmi \ ++ continuationals.cmi \ ++ declarative.cmi ++declarative.cmx : \ ++ nnAuto.cmx \ ++ nTactics.cmx \ ++ nTacStatus.cmx \ ++ nCicElim.cmx \ ++ continuationals.cmx \ ++ declarative.cmi ++declarative.cmi : \ ++ nnAuto.cmi \ ++ nTacStatus.cmi ++nCicElim.cmo : \ ++ nCicElim.cmi ++nCicElim.cmx : \ ++ nCicElim.cmi nCicElim.cmi : --nCicTacReduction.cmo : nCicTacReduction.cmi --nCicTacReduction.cmx : nCicTacReduction.cmi ++nCicTacReduction.cmo : \ ++ nCicTacReduction.cmi ++nCicTacReduction.cmx : \ ++ nCicTacReduction.cmi nCicTacReduction.cmi : --nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \ ++nDestructTac.cmo : \ ++ nTactics.cmi \ ++ nTacStatus.cmi \ ++ continuationals.cmi \ nDestructTac.cmi --nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ ++nDestructTac.cmx : \ ++ nTactics.cmx \ ++ nTacStatus.cmx \ ++ continuationals.cmx \ nDestructTac.cmi --nDestructTac.cmi : nTacStatus.cmi --nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \ -- continuationals.cmi nInversion.cmi --nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \ -- continuationals.cmx nInversion.cmi --nInversion.cmi : nTacStatus.cmi --nTacStatus.cmo : nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi --nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi --nTacStatus.cmi : continuationals.cmi --nTactics.cmo : nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi --nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi --nTactics.cmi : nTacStatus.cmi --nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \ -- continuationals.cmi nnAuto.cmi --nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ -- continuationals.cmx nnAuto.cmi --nnAuto.cmi : nTacStatus.cmi ++nDestructTac.cmi : \ ++ nTacStatus.cmi ++nInversion.cmo : \ ++ nTactics.cmi \ ++ nTacStatus.cmi \ ++ nCicElim.cmi \ ++ continuationals.cmi \ ++ nInversion.cmi ++nInversion.cmx : \ ++ nTactics.cmx \ ++ nTacStatus.cmx \ ++ nCicElim.cmx \ ++ continuationals.cmx \ ++ nInversion.cmi ++nInversion.cmi : \ ++ nTacStatus.cmi ++nTacStatus.cmo : \ ++ nCicTacReduction.cmi \ ++ continuationals.cmi \ ++ nTacStatus.cmi ++nTacStatus.cmx : \ ++ nCicTacReduction.cmx \ ++ continuationals.cmx \ ++ nTacStatus.cmi ++nTacStatus.cmi : \ ++ continuationals.cmi ++nTactics.cmo : \ ++ nTacStatus.cmi \ ++ nCicElim.cmi \ ++ continuationals.cmi \ ++ nTactics.cmi ++nTactics.cmx : \ ++ nTacStatus.cmx \ ++ nCicElim.cmx \ ++ continuationals.cmx \ ++ nTactics.cmi ++nTactics.cmi : \ ++ nTacStatus.cmi ++nnAuto.cmo : \ ++ nTactics.cmi \ ++ nTacStatus.cmi \ ++ nCicTacReduction.cmi \ ++ continuationals.cmi \ ++ nnAuto.cmi ++nnAuto.cmx : \ ++ nTactics.cmx \ ++ nTacStatus.cmx \ ++ nCicTacReduction.cmx \ ++ continuationals.cmx \ ++ nnAuto.cmi ++nnAuto.cmi : \ ++ nTacStatus.cmi diff --cc matita/components/ng_tactics/.depend.opt index c8999df5a,420a5dbc6..ca420895d --- a/matita/components/ng_tactics/.depend.opt +++ b/matita/components/ng_tactics/.depend.opt @@@ -1,19 -1,33 +1,55 @@@ - continuationals.cmx : continuationals.cmi ++continuationals.cmx : \ ++ continuationals.cmi continuationals.cmi : - nCicElim.cmx : nCicElim.cmi -nCicTacReduction.cmi : -nTacStatus.cmi : continuationals.cmi ++declarative.cmx : \ ++ nnAuto.cmx \ ++ nTactics.cmx \ ++ nTacStatus.cmx \ ++ nCicElim.cmx \ ++ continuationals.cmx \ ++ declarative.cmi ++declarative.cmi : \ ++ nnAuto.cmi \ ++ nTacStatus.cmi ++nCicElim.cmx : \ ++ nCicElim.cmi nCicElim.cmi : -nTactics.cmi : nTacStatus.cmi -declarative.cmi : nTacStatus.cmi -nnAuto.cmi : nTacStatus.cmi -nDestructTac.cmi : nTacStatus.cmi -nInversion.cmi : nTacStatus.cmi -continuationals.cmo : continuationals.cmi -continuationals.cmx : continuationals.cmi -nCicTacReduction.cmo : nCicTacReduction.cmi --nCicTacReduction.cmx : nCicTacReduction.cmi -nTacStatus.cmo : nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi -nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi -nCicElim.cmo : nCicElim.cmi -nCicElim.cmx : nCicElim.cmi -nTactics.cmo : nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi -nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi -declarative.cmo : nTactics.cmi declarative.cmi -declarative.cmx : nTactics.cmx declarative.cmi -nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \ - continuationals.cmi nnAuto.cmi -nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ - continuationals.cmx nnAuto.cmi -nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \ - nDestructTac.cmi -nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ ++nCicTacReduction.cmx : \ ++ nCicTacReduction.cmi +nCicTacReduction.cmi : - nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ ++nDestructTac.cmx : \ ++ nTactics.cmx \ ++ nTacStatus.cmx \ ++ continuationals.cmx \ nDestructTac.cmi - nDestructTac.cmi : nTacStatus.cmi -nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \ - continuationals.cmi nInversion.cmi --nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \ -- continuationals.cmx nInversion.cmi - nInversion.cmi : nTacStatus.cmi - nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi - nTacStatus.cmi : continuationals.cmi - nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi - nTactics.cmi : nTacStatus.cmi - nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ - continuationals.cmx nnAuto.cmi - nnAuto.cmi : nTacStatus.cmi ++nDestructTac.cmi : \ ++ nTacStatus.cmi ++nInversion.cmx : \ ++ nTactics.cmx \ ++ nTacStatus.cmx \ ++ nCicElim.cmx \ ++ continuationals.cmx \ ++ nInversion.cmi ++nInversion.cmi : \ ++ nTacStatus.cmi ++nTacStatus.cmx : \ ++ nCicTacReduction.cmx \ ++ continuationals.cmx \ ++ nTacStatus.cmi ++nTacStatus.cmi : \ ++ continuationals.cmi ++nTactics.cmx : \ ++ nTacStatus.cmx \ ++ nCicElim.cmx \ ++ continuationals.cmx \ ++ nTactics.cmi ++nTactics.cmi : \ ++ nTacStatus.cmi ++nnAuto.cmx : \ ++ nTactics.cmx \ ++ nTacStatus.cmx \ ++ nCicTacReduction.cmx \ ++ continuationals.cmx \ ++ nnAuto.cmi ++nnAuto.cmi : \ ++ nTacStatus.cmi diff --cc matita/components/ng_tactics/continuationals.ml index b10877130,5538a3c2d..dc54c89dd --- a/matita/components/ng_tactics/continuationals.ml +++ b/matita/components/ng_tactics/continuationals.ml @@@ -49,7 -51,7 +51,7 @@@ struc let rec aux acc depth = function | [] -> acc - | (locs, todos, conts, tag) :: tl -> - | (locs, todos, conts, tag, p) :: tl -> ++ | (locs, todos, conts, tag, _p) :: tl -> let acc = List.fold_left (fun acc -> env acc depth tag) acc locs in let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in diff --cc matita/components/ng_tactics/declarative.ml index 000000000,4fa6b5bcb..d96e66811 mode 000000,100644..100644 --- a/matita/components/ng_tactics/declarative.ml +++ b/matita/components/ng_tactics/declarative.ml @@@ -1,0 -1,638 +1,636 @@@ + (* Copyright (C) 2019, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + open Continuationals.Stack + module Ast = NotationPt + open NTactics + open NTacStatus + + type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ] + + let mk_just status goal = + function + `Auto (l,params) -> NnAuto.auto_lowtac ~params:(l,params) status goal + | `Term t -> apply_tac t + + exception NotAProduct + exception FirstTypeWrong + exception NotEquivalentTypes + + let extract_first_goal_from_status status = + let s = status#stack in + match s with + | [] -> fail (lazy "There's nothing to prove") - | (g1, _, k, tag1, _) :: tl -> ++ | (g1, _, _k, _tag1, _) :: _tl -> + let goals = filter_open g1 in + match goals with + [] -> fail (lazy "No goals under focus") - | loc::tl -> ++ | loc::_tl -> + let goal = goal_of_loc (loc) in + goal ;; + + let extract_conclusion_type status goal = + let gty = get_goalty status goal in + let ctx = ctx_of gty in - let status,gty = term_of_cic_term status gty ctx in - gty ++ term_of_cic_term status gty ctx + ;; + + let alpha_eq_tacterm_kerterm ty t status goal = + let gty = get_goalty status goal in + let ctx = ctx_of gty in + let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in + let (_,_,metasenv,subst,_) = status#obj in + let status,ty = term_of_cic_term status cicterm ctx in + if NCicReduction.alpha_eq status metasenv subst ctx t ty then + true + else + false + ;; + + let are_convertible ty1 ty2 status goal = + let gty = get_goalty status goal in + let ctx = ctx_of gty in + let status,cicterm1 = disambiguate status ctx ty1 `XTNone in + let status,cicterm2 = disambiguate status ctx ty2 `XTNone in + NTacStatus.are_convertible status ctx cicterm1 cicterm2 + + let clear_volatile_params_tac status = + match status#stack with + [] -> fail (lazy "Empty stack") + | (g,t,k,tag,p)::tl -> + let rec remove_volatile = function + [] -> [] - | (k,v as hd')::tl' -> ++ | (k,_v as hd')::tl' -> + let re = Str.regexp "volatile_.*" in + if Str.string_match re k 0 then + remove_volatile tl' + else + hd'::(remove_volatile tl') + in + let newp = remove_volatile p in + status#set_stack ((g,t,k,tag,newp)::tl) + ;; + + let add_parameter_tac key value status = + match status#stack with + [] -> status + | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl) + ;; + + + (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that + the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with + \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ? + *) + let lambda_abstract_tac id t1 status goal = + match extract_conclusion_type status goal with - | NCic.Prod (_,t,_) -> ++ | status,NCic.Prod (_,t,_) -> + if alpha_eq_tacterm_kerterm t1 t status goal then + let (_,_,t1) = t1 in + block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit + `JustOne))); clear_volatile_params_tac; + add_parameter_tac "volatile_newhypo" id] status + else + raise FirstTypeWrong + | _ -> raise NotAProduct + + let assume name ty status = + let goal = extract_first_goal_from_status status in + try lambda_abstract_tac name ty status goal + with + | NotAProduct -> fail (lazy "You can't assume without an universal quantification") + | FirstTypeWrong -> fail (lazy "The assumed type is wrong") + | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent") + ;; + + let suppose t1 id status = + let goal = extract_first_goal_from_status status in + try lambda_abstract_tac id t1 status goal + with + | NotAProduct -> fail (lazy "You can't suppose without a logical implication") + | FirstTypeWrong -> fail (lazy "The supposed proposition is different from the premise") + | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent") + ;; + + let assert_tac t1 t2 status goal continuation = - let t = extract_conclusion_type status goal in ++ let status,t = extract_conclusion_type status goal in + if alpha_eq_tacterm_kerterm t1 t status goal then + match t2 with + | None -> continuation + | Some t2 -> - let status,res = are_convertible t1 t2 status goal in ++ let _status,res = are_convertible t1 t2 status goal in + if res then continuation + else + raise NotEquivalentTypes + else + raise FirstTypeWrong + + let branch_dot_tac status = + match status#stack with + ([],t,k,tag,p) :: tl -> + if List.length t > 0 then + status#set_stack (([List.hd t],List.tl t,k,tag,p)::tl) + else + status + | _ -> status + ;; + + let status_parameter key status = + match status#stack with + [] -> "" - | (g,t,k,tag,p)::_ -> try List.assoc key p with _ -> "" ++ | (_g,_t,_k,_tag,p)::_ -> try List.assoc key p with _ -> "" + ;; + + let beta_rewriting_step t status = + let ctx = status_parameter "volatile_context" status in + if ctx <> "beta_rewrite" then + ( + let newhypo = status_parameter "volatile_newhypo" status in + if newhypo = "" then + fail (lazy "Invalid use of 'or equivalently'") + else + change_tac ~where:("",0,(None,[newhypo,Ast.UserInput],None)) ~with_what:t status + ) + else + change_tac ~where:("",0,(None,[],Some + Ast.UserInput)) ~with_what:t status + ;; + + let done_continuation status = + let rec continuation l = + match l with + [] -> [] + | (_,t,_,tag,p)::tl -> + if tag = `BranchTag then + if List.length t > 0 then + let continue = + let ctx = + try List.assoc "context" p + with Not_found -> "" + in + ctx <> "induction" && ctx <> "cases" + in + if continue then [clear_volatile_params_tac;branch_dot_tac] else + [clear_volatile_params_tac] + else + [merge_tac] @ (continuation tl) + else + [] + in + continuation status#stack + ;; + + let bydone just status = + let goal = extract_first_goal_from_status status in + let continuation = done_continuation status in + let l = [mk_just status goal just] @ continuation in + block_tac l status + ;; + + let push_goals_tac status = + match status#stack with + [] -> fail (lazy "Error pushing goals") + | (g1,t1,k1,tag1,p1) :: (g2,t2,k2,tag2,p2) :: tl -> + if List.length g2 > 0 then + status#set_stack ((g1,t1 @+ g2,k1,tag1,p1) :: ([],t2,k2,tag2,p2) :: tl) + else status (* Nothing to push *) + | _ -> status + + let we_need_to_prove t id status = + let goal = extract_first_goal_from_status status in + match id with + | None -> + ( + try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" status) + with + | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion") + ) + | Some id -> + ( + block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac; + push_goals_tac; add_parameter_tac "volatile_context" "beta_rewrite" + ] status + ) + ;; + + let by_just_we_proved just ty id status = + let goal = extract_first_goal_from_status status in - let wrappedjust = just in + let just = mk_just status goal just in + match id with + | None -> + assert_tac ty None status goal (block_tac [clear_volatile_params_tac; add_parameter_tac + "volatile_context" "beta_rewrite"] status) + | Some id -> + ( + block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac; + clear_volatile_params_tac; add_parameter_tac "volatile_newhypo" id] status + ) + ;; + + let existselim just id1 t1 t2 id2 status = + let goal = extract_first_goal_from_status status in + let (_,_,t1) = t1 in + let (_,_,t2) = t2 in + let just = mk_just status goal just in + (block_tac [ + cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident + (id1,None), Some t1),t2)])); + branch_tac ~force:false; + just; + shift_tac; + case1_tac "_"; + intros_tac ~names_ref:(ref []) [id1;id2]; + merge_tac; + clear_volatile_params_tac + ]) status + ;; + + let andelim just t1 id1 t2 id2 status = + let goal = extract_first_goal_from_status status in + let (_,_,t1) = t1 in + let (_,_,t2) = t2 in + let just = mk_just status goal just in + (block_tac [ + cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2])); + branch_tac ~force:false; + just; + shift_tac; + case1_tac "_"; + intros_tac ~names_ref:(ref []) [id1;id2]; + merge_tac; + clear_volatile_params_tac + ]) status + ;; + + let type_of_tactic_term status ctx t = + let status,cicterm = disambiguate status ctx t `XTNone in + let (_,cicty) = typeof status ctx cicterm in + cicty + + let swap_first_two_goals_tac status = + let gstatus = + match status#stack with + | [] -> assert false + | (g,t,k,tag,p) :: s -> + match g with + | (loc1) :: (loc2) :: tl -> + ([loc2;loc1] @+ tl,t,k,tag,p) :: s + | _ -> assert false + in + status#set_stack gstatus + + let thesisbecomes t1 = we_need_to_prove t1 None + ;; + + let obtain id t1 status = + let goal = extract_first_goal_from_status status in + let cicgty = get_goalty status goal in + let ctx = ctx_of cicgty in + let cicty = type_of_tactic_term status ctx t1 in + let _,ty = term_of_cic_term status cicty ctx in + let (_,_,t1) = t1 in + block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit + `JustOne])); + swap_first_two_goals_tac; + branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac; + add_parameter_tac "volatile_context" "rewrite" + ] + status + ;; + + let conclude t1 status = + let goal = extract_first_goal_from_status status in + let cicgty = get_goalty status goal in + let ctx = ctx_of cicgty in + let _,gty = term_of_cic_term status cicgty ctx in + match gty with + (* The first term of this Appl should probably be "eq" *) + NCic.Appl [_;_;plhs;_] -> + if alpha_eq_tacterm_kerterm t1 plhs status goal then + add_parameter_tac "volatile_context" "rewrite" status + else + fail (lazy "The given conclusion is different from the left-hand side of the current conclusion") + | _ -> fail (lazy "Your conclusion needs to be an equality") + ;; + + let rewritingstep rhs just last_step status = + let ctx = status_parameter "volatile_context" status in + if ctx = "rewrite" then + ( + let goal = extract_first_goal_from_status status in + let cicgty = get_goalty status goal in + let ctx = ctx_of cicgty in + let _,gty = term_of_cic_term status cicgty ctx in + let cicty = type_of_tactic_term status ctx rhs in + let _,ty = term_of_cic_term status cicty ctx in + let just' = (* Extraction of the ""justification"" from the ad hoc justification *) + match just with + `Auto (univ, params) -> + let params = + if not (List.mem_assoc "timeout" params) then + ("timeout","3")::params + else params + in + let params' = + if not (List.mem_assoc "paramodulation" params) then + ("paramodulation","1")::params + else params + in + if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal + else + first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac + ~params:(univ, params') status goal] + | `Term just -> apply_tac just + | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"]) + | `Proof -> id_tac + in + let plhs,prhs,prepare = + match gty with (* Extracting the lhs and rhs of the previous equality *) + NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status) + | _ -> fail (lazy "You are not building an equaility chain") + in + let continuation = + if last_step then + let todo = [just'] @ (done_continuation status) in + block_tac todo + else + let (_,_,rhs) = rhs in + block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs; + rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac] + in + prepare continuation + ) + else + fail (lazy "You are not building an equality chain") + ;; + + let rec pp_metasenv_names (metasenv:NCic.metasenv) = + match metasenv with + [] -> "" + | hd :: tl -> + let n,conj = hd in + let meta_attrs,_,_ = conj in + let rec find_name_aux meta_attrs = match meta_attrs with + [] -> "Anonymous" + | hd :: tl -> match hd with + `Name n -> n + | _ -> find_name_aux tl + in + let name = find_name_aux meta_attrs + in + "[Goal: " ^ (string_of_int n) ^ ", Name: " ^ name ^ "]; " ^ (pp_metasenv_names tl) + ;; + + let print_goals_names_tac s (status:#NTacStatus.tac_status) = + let (_,_,metasenv,_,_) = status#obj in + prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status + + (* Useful as it does not change the order in the list *) + let rec list_change_assoc k v = function + [] -> [] - | (k',v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl) ++ | (k',_v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl) + ;; + + let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) = + let add_name_to_goal name goal metasenv = - let (mattrs,ctx,t as conj) = try List.assoc goal metasenv with _ -> assert false in ++ let (mattrs,ctx,t) = try List.assoc goal metasenv with _ -> assert false in + let mattrs = (`Name name) :: (List.filter (function `Name _ -> false | _ -> true) mattrs) in + let newconj = (mattrs,ctx,t) in + list_change_assoc goal newconj metasenv + in + let new_goals = + (* It's important that this tactic is called before branching and right after the creation of + * the new goals, when they are still under focus *) + match status#stack with + [] -> fail (lazy "Can not add names to an empty stack") - | (g,_,_,_,_) :: tl -> ++ | (g,_,_,_,_) :: _tl -> + let rec sublist n = function + [] -> [] + | hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl) + in + List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g) + in + let rec add_names_to_goals g cl metasenv = + match g,cl with + [],[] -> metasenv + | hd::tl, (_,consname,_)::tl' -> + add_names_to_goals tl tl' (add_name_to_goal consname hd metasenv) + | _,_ -> fail (lazy "There are less goals than constructors") + in + let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in + let newmetasenv = add_names_to_goals new_goals !cl metasenv + in status#set_obj(olduri,oldint,newmetasenv,oldsubst,oldkind) + ;; + (* + let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in + let remove_name_from_metaattrs = + List.filter (function `Name _ -> false | _ -> true) in + let rec add_names_to_metasenv cl metasenv = + match cl,metasenv with + [],_ -> metasenv + | hd :: tl, mhd :: mtl -> + let _,consname,_ = hd in + let gnum,conj = mhd in + let mattrs,ctx,t = conj in + let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs) + in + let newconj = mattrs,ctx,t in + let newmeta = gnum,newconj in + newmeta :: (add_names_to_metasenv tl mtl) + | _,[] -> assert false + in + let newmetasenv = add_names_to_metasenv !cl metasenv in + status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind) + *) + + let unfocus_branch_tac status = + match status#stack with + [] -> status + | (g,t,k,tag,p) :: tl -> status#set_stack (([],g @+ t,k,tag,p)::tl) + ;; + + let we_proceed_by_induction_on t1 t2 status = + let goal = extract_first_goal_from_status status in + let txt,len,t1 = t1 in + let t1 = txt, len, Ast.Appl [t1; Ast.Implicit `Vector] in + let indtyinfo = ref None in + let sort = ref (NCic.Rel 1) in + let cl = ref [] in (* this is a ref on purpose, as the block of code after sort_of_goal_tac in + block_tac acts as a block of asynchronous code, in which cl gets modified with the info retrieved + with analize_indty_tac, and later used to label each new goal with a costructor name. Using a + plain list this doesn't seem to work, as add_names_to_goals_tac would immediately act on an empty + list, instead of acting on the list of constructors *) + try + assert_tac t2 None status goal (block_tac [ + analyze_indty_tac ~what:t1 indtyinfo; + sort_of_goal_tac sort; + (fun status -> + let ity = HExtlib.unopt !indtyinfo in + let NReference.Ref (uri, _) = ref_of_indtyinfo ity in + let name = + NUri.name_of_uri uri ^ "_" ^ + snd (NCicElim.ast_of_sort + (match !sort with NCic.Sort x -> x | _ -> assert false)) + in + let eliminator = + let l = [Ast.Ident (name,None)] in + (* Generating an implicit for each argument of the inductive type, plus one the + * predicate, plus an implicit for each constructor of the inductive type *) + let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) (ity.leftno+1+ity.consno) in + let _,_,t1 = t1 in + let l = l @ [t1] in + Ast.Appl l + in + cl := ity.cl; + exact_tac ("",0,eliminator) status); + add_names_to_goals_tac cl; + branch_tac; + push_goals_tac; + unfocus_branch_tac; + add_parameter_tac "context" "induction" + ] status) + with + | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion") + ;; + + let we_proceed_by_cases_on ((txt,len,ast1) as t1) t2 status = + let goal = extract_first_goal_from_status status in + let npt1 = txt, len, Ast.Appl [ast1; Ast.Implicit `Vector] in + let indtyinfo = ref None in + let cl = ref [] in + try + assert_tac t2 None status goal (block_tac [ + analyze_indty_tac ~what:npt1 indtyinfo; + cases_tac ~what:t1 ~where:("",0,(None,[],Some + Ast.UserInput)); + ( + fun status -> + let ity = HExtlib.unopt !indtyinfo in + cl := ity.cl; add_names_to_goals_tac cl status + ); + branch_tac; push_goals_tac; + unfocus_branch_tac; + add_parameter_tac "context" "cases" + ] status) + with + | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion") + ;; + + let byinduction t1 id = suppose t1 id ;; + + let name_of_conj conj = + let mattrs,_,_ = conj in + let rec search_name mattrs = + match mattrs with + [] -> "Anonymous" + | hd::tl -> + match hd with + `Name n -> n + | _ -> search_name tl + in + search_name mattrs + + let rec loc_of_goal goal l = + match l with + [] -> fail (lazy "Reached the end") + | hd :: tl -> + let _,sw = hd in + let g = goal_of_switch sw in + if g = goal then hd + else loc_of_goal goal tl + ;; + + let has_focused_goal status = + match status#stack with + [] -> false - | ([],_,_,_,_) :: tl -> false ++ | ([],_,_,_,_) :: _tl -> false + | _ -> true + ;; + + let focus_on_case_tac case status = + let (_,_,metasenv,_,_) = status#obj in + let rec goal_of_case case metasenv = + match metasenv with + [] -> fail (lazy "The given case does not exist") + | (goal,conj) :: tl -> + if name_of_conj conj = case then goal + else goal_of_case case tl + in + let goal_to_focus = goal_of_case case metasenv in + let gstatus = + match status#stack with + [] -> fail (lazy "There is nothing to prove") + | (g,t,k,tag,p) :: s -> + let loc = + try + loc_of_goal goal_to_focus t + with _ -> fail (lazy "The given case is not part of the current induction/cases analysis + context") + in + let curloc = if has_focused_goal status then + let goal = extract_first_goal_from_status status in + [loc_of_goal goal g] + else [] + in + (((g @- curloc) @+ [loc]),(curloc @+ (t @- [loc])),k,tag,p) :: s + in + status#set_stack gstatus + ;; + + let case id l status = + let ctx = status_parameter "context" status in + if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an + induction/cases analysis context") + else + ( + if has_focused_goal status then fail (lazy "Finish the current case before switching") + else + ( + (* + let goal = extract_first_goal_from_status status in + let (_,_,metasenv,_,_) = status#obj in + let conj = NCicUtils.lookup_meta goal metasenv in + let name = name_of_conj conj in + *) + let continuation = + let rec aux l = + match l with + [] -> [id_tac] + | (id,ty)::tl -> + (try_tac (assume id ("",0,ty))) :: (aux tl) + in + aux l + in + (* if name = id then block_tac continuation status *) + (* else *) + block_tac ([focus_on_case_tac id] @ continuation) status + ) + ) + ;; + + let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;; + + (* vim: ts=2: sw=0: et: + * *) diff --cc matita/components/ng_tactics/nTacStatus.ml index fc525c84a,1001d9808..118261af0 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@@ -232,6 -232,15 +232,15 @@@ let normalize status ?delta ctx t status, (ctx, t) ;; + let are_convertible status ctx a b = + let status, (_,a) = relocate status ctx a in + let status, (_,b) = relocate status ctx b in - let n,h,metasenv,subst,o = status#obj in ++ let _n,_h,metasenv,subst,_o = status#obj in + let res = NCicReduction.are_convertible status metasenv subst ctx a b in + status, res + ;; + let are_convertible a b c d = wrap "are_convertible" (are_convertible a b c) d;; + let unify status ctx a b = let status, (_,a) = relocate status ctx a in let status, (_,b) = relocate status ctx b in diff --cc matita/components/ng_tactics/nTactics.ml index 1aba2be9d,a8a78999a..721d9165b --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@@ -502,7 -503,7 +503,7 @@@ let analyze_indty_tac ~what indtyref let goalty = get_goalty status goal in let status, what = disambiguate status (ctx_of goalty) what `XTInd in let status, ty_what = typeof status (ctx_of what) what in - let _status, (r,consno,lefts,rights) = analyse_indty status ty_what in - let status, (r,consno,lefts,rights,cl) = analyse_indty status ty_what in ++ let _status, (r,consno,lefts,rights,cl) = analyse_indty status ty_what in let leftno = List.length lefts in let rightno = List.length rights in indtyref := Some { @@@ -675,7 -704,7 +704,7 @@@ let assert0_tac (hyps,concl) = distribu let assert_tac seqs status = match status#stack with | [] -> assert false - | (g,_,_,_) :: _s -> - | (g,_,_,_,_) :: s -> ++ | (g,_,_,_,_) :: _s -> assert (List.length g = List.length seqs); (match seqs with [] -> id_tac diff --cc matita/components/ng_tactics/nnAuto.ml index 0f11cab74,cb73e873e..3ac6040dc --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@@ -316,9 -319,10 +319,10 @@@ let index_local_equations eq_cache ?(fl | NCicTypeChecker.TypeCheckerFailure _ | NCicTypeChecker.AssertFailure _ -> eq_cache) eq_cache ctx + end ;; - let index_local_equations2 eq_cache status open_goal lemmas nohyps = -let index_local_equations2 eq_cache status open_goal lemmas ?(flag=false) nohyps = ++let index_local_equations2 eq_cache status open_goal lemmas ?flag:(_=false) nohyps = noprint (lazy "indexing equations"); let eq_cache,lemmas = match lemmas with @@@ -1087,17 -1092,25 +1092,25 @@@ let get_cands retrieve_for diff empty g cands, diff more_cands cands ;; + let is_a_needed_uri s = + s = "cic:/matita/basics/logic/eq.ind" || + s = "cic:/matita/basics/logic/sym_eq.con" || + s = "cic:/matita/basics/logic/trans_eq.con" || + s = "cic:/matita/basics/logic/eq_f3.con" || + s = "cic:/matita/basics/logic/eq_f2.con" || + s = "cic:/matita/basics/logic/eq_f.con" + -let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty = +let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gty = let universe = status#auto_cache in let _,_,metasenv,subst,_ = status#obj in let context = ctx_of gty in let _, raw_gty = term_of_cic_term status gty context in - let is_prod, is_eq = + let is_prod, _is_eq = - let status, t = term_of_cic_term status gty context in - let t = NCicReduction.whd status subst context t in - match t with - | NCic.Prod _ -> true, false - | _ -> false, NCicParamod.is_equation status metasenv subst context t + let status, t = term_of_cic_term status gty context in + let t = NCicReduction.whd status subst context t in + match t with + | NCic.Prod _ -> true, false + | _ -> false, NCicParamod.is_equation status metasenv subst context t in debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty)); let is_eq = @@@ -1555,11 -1584,11 +1584,11 @@@ match status#stack wit in let others = menv_closure status (stack_goals (level-1) tl) in List.for_all (fun i -> IntSet.mem i others) - (HExtlib.filter_map is_open g) + (HExtlib.filter_map is_open g) - let top_cache ~depth:_ top status cache = -let top_cache ~depth top status ?(use_given_only=false) cache = ++let top_cache ~depth:_ top status ?(use_given_only=false) cache = if top then - let unit_eq = index_local_equations status#eq_cache status in + let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in {cache with unit_eq = unit_eq} else cache @@@ -1652,7 -1680,7 +1680,7 @@@ let rec auto_clusters ?(top=false) flag and (* BRAND NEW VERSION *) - auto_main flags signature cache depth status: unit = -auto_main flags signature cache depth status ?(use_given_only=false): unit= ++auto_main flags signature cache depth ?(use_given_only=false) status: unit= debug_print ~depth (lazy "entering auto main"); debug_print ~depth (pptrace status cache.trace); debug_print ~depth (lazy ("stack length = " ^ @@@ -1663,28 -1691,28 +1691,28 @@@ match goals with | [] when depth = 0 -> raise (Proved (status,cache.trace)) | [] -> - let status = NTactics.merge_tac status in - let cache = - let l,tree = cache.under_inspection in - match l with - | [] -> cache (* possible because of intros that cleans the cache *) - | a::tl -> let tree = rm_from_th a tree a in - {cache with under_inspection = tl,tree} - in - auto_clusters flags signature cache (depth-1) status ~use_given_only - | orig::_ -> - if depth > 0 && move_to_side depth status - then - let status = NTactics.merge_tac status in - let cache = - let l,tree = cache.under_inspection in - match l with - | [] -> cache (* possible because of intros that cleans the cache*) - | a::tl -> let tree = rm_from_th a tree a in - {cache with under_inspection = tl,tree} - in - auto_clusters flags signature cache (depth-1) status ~use_given_only - else + let status = NTactics.merge_tac status in + let cache = + let l,tree = cache.under_inspection in + match l with + | [] -> cache (* possible because of intros that cleans the cache *) + | a::tl -> let tree = rm_from_th a tree a in + {cache with under_inspection = tl,tree} + in - auto_clusters flags signature cache (depth-1) status ++ auto_clusters flags signature cache (depth-1) status ~use_given_only + | _orig::_ -> + if depth > 0 && move_to_side depth status + then + let status = NTactics.merge_tac status in + let cache = + let l,tree = cache.under_inspection in + match l with + | [] -> cache (* possible because of intros that cleans the cache*) + | a::tl -> let tree = rm_from_th a tree a in + {cache with under_inspection = tl,tree} + in - auto_clusters flags signature cache (depth-1) status ++ auto_clusters flags signature cache (depth-1) status ~use_given_only + else let ng = List.length goals in (* moved inside auto_clusters *) if ng > flags.maxwidth then begin @@@ -1876,6 -1916,31 +1916,31 @@@ let auto_tac' candidates ~local_candida s ;; + let candidates_from_ctx univ ctx status = + match univ with + | None -> None + | Some l -> + let to_Ast t = + (* FG: `XTSort here? *) + let status, res = disambiguate status ctx t `XTNone in + let _,res = term_of_cic_term status res (ctx_of res) + in Ast.NCic res + in Some ((List.map to_Ast l) @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None); + Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None); + Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None); + Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None) + ]) + -let auto_lowtac ~params:(univ,flags as params) status goal = ++let auto_lowtac ~params:(univ,flags) status goal = + let gty = get_goalty status goal in + let ctx = ctx_of gty in + let candidates = candidates_from_ctx univ ctx status in + auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref []) + + let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = + let candidates = candidates_from_ctx univ [] status in + auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref status + let auto_tac ~params:(_,flags as params) ?trace_ref = if List.mem_assoc "demod" flags then demod_tac ~params diff --cc matita/components/registry/.depend index 2a8e36776,67113e67f..edb72af84 --- a/matita/components/registry/.depend +++ b/matita/components/registry/.depend @@@ -1,3 -1,3 +1,5 @@@ - helm_registry.cmo : helm_registry.cmi - helm_registry.cmx : helm_registry.cmi ++helm_registry.cmo : \ ++ helm_registry.cmi ++helm_registry.cmx : \ ++ helm_registry.cmi helm_registry.cmi : -helm_registry.cmo : helm_registry.cmi -helm_registry.cmx : helm_registry.cmi diff --cc matita/components/registry/.depend.opt index f28210446,67113e67f..c8aaec531 --- a/matita/components/registry/.depend.opt +++ b/matita/components/registry/.depend.opt @@@ -1,2 -1,3 +1,3 @@@ - helm_registry.cmx : helm_registry.cmi ++helm_registry.cmx : \ ++ helm_registry.cmi helm_registry.cmi : -helm_registry.cmo : helm_registry.cmi -helm_registry.cmx : helm_registry.cmi diff --cc matita/components/syntax_extensions/.depend.opt index 98ac1d844,24f371ca7..84b72a664 --- a/matita/components/syntax_extensions/.depend.opt +++ b/matita/components/syntax_extensions/.depend.opt @@@ -1,3 -1,5 +1,5 @@@ - utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi ++utf8Macro.cmx : \ ++ utf8MacroTable.cmx \ ++ utf8Macro.cmi utf8Macro.cmi : -utf8MacroTable.cmo : utf8MacroTable.cmx : -utf8Macro.cmo : utf8MacroTable.cmx utf8Macro.cmi -utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi diff --cc matita/components/thread/.depend index e8bc4a106,d68336af1..7bf942ba0 --- a/matita/components/thread/.depend +++ b/matita/components/thread/.depend @@@ -1,6 -1,6 +1,10 @@@ - extThread.cmo : extThread.cmi - extThread.cmx : extThread.cmi -threadSafe.cmi : ++extThread.cmo : \ ++ extThread.cmi ++extThread.cmx : \ ++ extThread.cmi extThread.cmi : --threadSafe.cmo : threadSafe.cmi --threadSafe.cmx : threadSafe.cmi -extThread.cmo : extThread.cmi -extThread.cmx : extThread.cmi ++threadSafe.cmo : \ ++ threadSafe.cmi ++threadSafe.cmx : \ ++ threadSafe.cmi +threadSafe.cmi : diff --cc matita/components/thread/.depend.opt index 8ee8dbbec,d68336af1..e022019db --- a/matita/components/thread/.depend.opt +++ b/matita/components/thread/.depend.opt @@@ -1,4 -1,6 +1,6 @@@ - extThread.cmx : extThread.cmi -threadSafe.cmi : ++extThread.cmx : \ ++ extThread.cmi extThread.cmi : -threadSafe.cmo : threadSafe.cmi --threadSafe.cmx : threadSafe.cmi -extThread.cmo : extThread.cmi -extThread.cmx : extThread.cmi ++threadSafe.cmx : \ ++ threadSafe.cmi +threadSafe.cmi : diff --cc matita/components/xml/.depend index 60964e765,fd3f626b9..2ed17ef38 --- a/matita/components/xml/.depend +++ b/matita/components/xml/.depend @@@ -1,6 -1,6 +1,10 @@@ - xml.cmo : xml.cmi - xml.cmx : xml.cmi ++xml.cmo : \ ++ xml.cmi ++xml.cmx : \ ++ xml.cmi xml.cmi : - xmlPushParser.cmo : xmlPushParser.cmi - xmlPushParser.cmx : xmlPushParser.cmi ++xmlPushParser.cmo : \ ++ xmlPushParser.cmi ++xmlPushParser.cmx : \ ++ xmlPushParser.cmi xmlPushParser.cmi : -xml.cmo : xml.cmi -xml.cmx : xml.cmi -xmlPushParser.cmo : xmlPushParser.cmi -xmlPushParser.cmx : xmlPushParser.cmi diff --cc matita/components/xml/.depend.opt index 36a543808,fd3f626b9..31b27a176 --- a/matita/components/xml/.depend.opt +++ b/matita/components/xml/.depend.opt @@@ -1,4 -1,6 +1,6 @@@ - xml.cmx : xml.cmi ++xml.cmx : \ ++ xml.cmi xml.cmi : - xmlPushParser.cmx : xmlPushParser.cmi ++xmlPushParser.cmx : \ ++ xmlPushParser.cmi xmlPushParser.cmi : -xml.cmo : xml.cmi -xml.cmx : xml.cmi -xmlPushParser.cmo : xmlPushParser.cmi -xmlPushParser.cmx : xmlPushParser.cmi diff --cc matita/matita/matitaEngine.ml index 2963e71c4,cfd8c107a..fea7161c1 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@@ -25,6 -25,8 +25,7 @@@ (* $Id$ *) + module G = GrafiteAst -open GrafiteTypes open Printf class status baseuri = @@@ -44,16 -46,105 +45,105 @@@ let debug_print = if debug then prerr_e let slash_n_RE = Pcre.regexp "\\n" ;; - let pp_ast_statement status stm = - let stm = GrafiteAstPp.pp_statement status stm - ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") + let first_line = ref true ;; + + let cases_or_induction_context stack = + match stack with + [] -> false - | (g,t,k,tag,p)::tl -> try ++ | (_g,_t,_k,_tag,p)::_tl -> try + let s = List.assoc "context" p in + s = "cases" || s = "induction" + with + Not_found -> false + ;; + + let has_focused_goal stack = + match stack with + [] -> false - | (g,t,k,tag,p)::tl -> (List.length g) > 0 ++ | (g,_t,_k,_tag,_p)::_tl -> (List.length g) > 0 + ;; + -let get_indentation status statement = ++let get_indentation status _statement = + let base_ind = + match status#stack with + [] -> 0 + | s -> List.length(s) * 2 in - let stm = Pcre.replace ~rex:slash_n_RE stm in - let stm = + if cases_or_induction_context status#stack then + ( + if has_focused_goal status#stack then + base_ind + 2 + else + base_ind + ) + else + base_ind + ;; + + let pp_ind s n = + let rec aux s n = + match n with + 0 -> s + | n -> " " ^ (aux s (n-1)) + in + aux s n + + let write_ast_to_file status fname statement = + let indentation = get_indentation status statement in + let str = match statement with + G.Comment _ -> GrafiteAstPp.pp_statement status statement + ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") + | G.Executable (_,code) -> + ( + match code with + G.NTactic _ -> GrafiteAstPp.pp_statement status statement + ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") + | G.NCommand (_,cmd) -> + ( + match cmd with + | G.NObj (_,obj,_) -> + ( + match obj with - Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement ++ NotationPt.Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement + ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") + | _ -> "" + ) + | G.NQed _ -> GrafiteAstPp.pp_statement status statement + ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") + | _ -> "" + ) + | _ -> "" + ) + in + if str <> "" then + ( + let s = pp_ind str indentation in + let flaglist = if !first_line = false then [Open_wronly; Open_append; Open_creat] + else (first_line := false; [Open_wronly; Open_trunc; Open_creat]) + in + let out_channel = + Stdlib.open_out_gen flaglist 0o0644 fname in + let _ = Stdlib.output_string out_channel ((if str.[0] <> '\n' then s else str) ^ "\n") in + let _ = Stdlib.close_out out_channel in + str + ) + else + str + ;; + + let pp_ast_statement status stm ~fname = + let stm = write_ast_to_file status (fname ^ ".parsed.ma") stm in + if stm <> "" then + ( + let stm = Pcre.replace ~rex:slash_n_RE stm in + let stm = if String.length stm > 50 then String.sub stm 0 50 ^ " ..." else stm - in + in HLog.debug ("Executing: ``" ^ stm ^ "''") + ) + else + HLog.debug ("Executing: `` Unprintable statement ''") ;; let clean_exit baseuri exn = @@@ -161,73 -252,73 +251,73 @@@ let baseuri_of_script ~include_paths fn (* given a path to a ma file inside the include_paths, returns the new include_paths associated to that file *) -let read_include_paths ~include_paths file = - try - let root, _buri, _fname, _tgt = - Librarian.baseuri_of_script ~include_paths:[] file in - let includes = - try - Str.split (Str.regexp " ") - (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) - with Not_found -> [] - in - let rc = root :: includes in +let read_include_paths ~include_paths:_ file = + try + let root, _buri, _fname, _tgt = + Librarian.baseuri_of_script ~include_paths:[] file in + let includes = + try + Str.split (Str.regexp " ") + (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) + with Not_found -> [] + in + let rc = root :: includes in List.iter (HLog.debug) rc; rc - with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> - [] + with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> + [] ;; - let rec get_ast status ~compiling ~asserted ~include_paths strm = + let rec get_ast status ~compiling ~asserted ~include_paths strm = match GrafiteParser.parse_statement status strm with - (GrafiteAst.Executable + (GrafiteAst.Executable (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd - -> - let already_included = NCicLibrary.get_transitively_included status in - let asserted,_ = - assert_ng ~already_included ~compiling ~asserted ~include_paths - mafilename - in - asserted,cmd - | cmd -> asserted,cmd + -> + let already_included = NCicLibrary.get_transitively_included status in + let asserted,_ = + assert_ng ~already_included ~compiling ~asserted ~include_paths + mafilename + in + asserted,cmd + | cmd -> asserted,cmd and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb = - let matita_debug = Helm_registry.get_bool "matita.debug" in - let rec loop asserted status str = - let asserted,stop,status,str = - try - let cont = - try Some (get_ast status ~compiling ~asserted ~include_paths str) - with End_of_file -> None in - match cont with - | None -> asserted, true, status, str - | Some (asserted,ast) -> - cb status ast; - let new_statuses = - eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in - let status = - match new_statuses with - [s,None] -> s - | _::(_,Some (_,value))::_ -> - raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value))) - | _ -> assert false in - (* CSC: complex patch to re-build the lexer since the tokens may - have changed. Note: this way we loose look-ahead tokens. - Hence the "include" command must be terminated (no look-ahead) *) - let str = - match ast with - (GrafiteAst.Executable - (_,GrafiteAst.NCommand - (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) -> + let matita_debug = Helm_registry.get_bool "matita.debug" in + let rec loop asserted status str = + let asserted,stop,status,str = + try + let cont = + try Some (get_ast status ~compiling ~asserted ~include_paths str) + with End_of_file -> None in + match cont with + | None -> asserted, true, status, str + | Some (asserted,ast) -> + cb status ast; + let new_statuses = + eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in + let status = + match new_statuses with + [s,None] -> s + | _::(_,Some (_,value))::_ -> + raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value))) + | _ -> assert false in + (* CSC: complex patch to re-build the lexer since the tokens may + have changed. Note: this way we loose look-ahead tokens. + Hence the "include" command must be terminated (no look-ahead) *) + let str = + match ast with + (GrafiteAst.Executable + (_,GrafiteAst.NCommand + (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) -> GrafiteParser.parsable_statement status - (GrafiteParser.strm_of_parsable str) - | _ -> str - in - asserted, false, status, str - with exn when not matita_debug -> - raise (EnrichedWithStatus (exn, status)) + (GrafiteParser.strm_of_parsable str) + | _ -> str + in + asserted, false, status, str + with exn when not matita_debug -> + raise (EnrichedWithStatus (exn, status)) + in + if stop then asserted,status else loop asserted status str in - if stop then asserted,status else loop asserted status str - in loop asserted status str and compile ~compiling ~asserted ~include_paths fname =