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;hp=-c Merge branch 'declarative' into matita-lablgtk3 --- 5b5dca0c118dfbe3ba8f0514ef07549544eb7810 diff --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined matita/components/grafite/grafiteAstPp.ml index 2e088bd77,60c466068..42d7df864 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@@ -1,14 -1,14 +1,14 @@@ (* Copyright (C) 2004, 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 @@@ -18,7 -18,7 +18,7 @@@ * 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://helm.cs.unibo.it/ *) @@@ -32,8 -32,8 +32,8 @@@ let tactical_terminator = " let tactic_terminator = tactical_terminator let command_terminator = tactical_terminator - let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) = - if what = None && hyp = [] && goal = None then "" else + let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) = + if what = None && hyp = [] && goal = None then "" else let what_text = match what with | None -> "" @@@ -51,11 -51,27 +51,27 @@@ in Printf.sprintf "%sin %s%s" what_text hyp_text goal_text + let pp_auto_params params status = + match params with + | (None,flags) -> String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags) + | (Some l,flags) -> (String.concat "," (List.map (NotationPp.pp_term status) l)) ^ + String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags) + ;; + + let pp_just status just = + match just with + `Term term -> "using (" ^ NotationPp.pp_term status term ^ ") " + | `Auto params -> + match params with + | (None,[]) -> "" + | params -> "by " ^ pp_auto_params params status ^ " " + ;; + let rec pp_ntactic status ~map_unicode_to_tex = let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in function | NApply (_,t) -> "@" ^ NotationPp.pp_term status t - | NSmartApply (_,t) -> "fixme" + | NSmartApply (_,_t) -> "fixme" | NAuto (_,(None,flgs)) -> "nautobatch" ^ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) @@@ -63,26 -79,26 +79,26 @@@ "nautobatch" ^ " by " ^ (String.concat "," (List.map (NotationPp.pp_term status) l)) ^ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) - | NCases (_,what,where) -> "ncases " ^ NotationPp.pp_term status what ^ + | NCases (_,what,_where) -> "ncases " ^ NotationPp.pp_term status what ^ "...to be implemented..." ^ " " ^ "...to be implemented..." | NConstructor (_,None,l) -> "@ " ^ String.concat " " (List.map (NotationPp.pp_term status) l) | 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 | NIntros (_,l) -> "#" ^ String.concat " " l - | NInversion (_,what,where) -> "ninversion " ^ NotationPp.pp_term status what ^ + | NInversion (_,what,_where) -> "ninversion " ^ NotationPp.pp_term status what ^ "...to be implemented..." ^ " " ^ "...to be implemented..." | NLApply (_,t) -> "lapply " ^ NotationPp.pp_term status t | NRewrite (_,dir,n,where) -> "nrewrite " ^ @@@ -97,23 -113,62 +113,65 @@@ | NPosbyname (_, s) -> s ^ ":" | NWildcard _ -> "*:" | NMerge _ -> "]" - | NFocus (_,l) -> - Printf.sprintf "focus %s" + | NFocus (_,l) -> + Printf.sprintf "focus %s" (String.concat " " (List.map string_of_int l)) | NUnfocus _ -> "unfocus" | 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 | NCheck (_, term) -> Printf.sprintf "ncheck %s" (NotationPp.pp_term status term) | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name + | NAutoInteractive _ + | NIntroGuess _ -> assert false (* TODO *) ;; let pp_l1_pattern = NotationPp.pp_term @@@ -128,7 -183,7 +186,7 @@@ let pp_alias = functio desc | Number_alias (instance,desc) -> sprintf "alias num (instance %d) = \"%s\"." instance desc - + let pp_associativity = function | Gramext.LeftA -> "left associative" | Gramext.RightA -> "right associative" @@@ -139,23 -194,23 +197,23 @@@ let pp_precedence i = sprintf "with pre let pp_argument_pattern = function | NotationPt.IdentArg (eta_depth, name) -> let eta_buf = Buffer.create 5 in - for i = 1 to eta_depth do + for _i = 1 to eta_depth do Buffer.add_string eta_buf "\\eta." done; sprintf "%s%s" (Buffer.contents eta_buf) name - let pp_interpretation dsc symbol arg_patterns cic_appl_pattern = + let pp_interpretation dsc symbol arg_patterns cic_appl_pattern = sprintf "interpretation \"%s\" '%s %s = %s." dsc symbol (String.concat " " (List.map pp_argument_pattern arg_patterns)) (NotationPp.pp_cic_appl_pattern cic_appl_pattern) - + let pp_dir_opt = function | None -> "" | Some `LeftToRight -> "> " | Some `RightToLeft -> "< " - let pp_notation status dir_opt l1_pattern assoc prec l2_pattern = + let pp_notation status dir_opt l1_pattern assoc prec l2_pattern = sprintf "notation %s\"%s\" %s %s for %s." (pp_dir_opt dir_opt) (pp_l1_pattern status l1_pattern) @@@ -164,22 -219,22 +222,22 @@@ (pp_l2_pattern status l2_pattern) let pp_ncommand status = function - | UnificationHint (_,t, n) -> + | UnificationHint (_,t, n) -> "unification hint " ^ string_of_int n ^ " " ^ NotationPp.pp_term status t | NDiscriminator (_,_) | NInverter (_,_,_,_,_) | NUnivConstraint (_) -> "not supported" | NCoercion (_) -> "not supported" - | NObj (_,obj,index) -> - (if not index then "-" else "") ^ + | NObj (_,obj,index) -> + (if not index then "-" else "") ^ NotationPp.pp_obj (NotationPp.pp_term status) obj | NQed (_,true) -> "qed" | NQed (_,false) -> "qed-" - | NCopy (_,name,uri,map) -> - "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ - String.concat " and " - (List.map - (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b) + | NCopy (_,name,uri,map) -> + "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ + String.concat " and " + (List.map + (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b) map) | Include (_,mode,path) -> (* not precise, since path is absolute *) if mode = WithPreferences then @@@ -192,14 -247,14 +250,14 @@@ | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) -> pp_notation status dir_opt l1_pattern assoc prec l2_pattern ;; - + let pp_executable status ~map_unicode_to_tex = function | NMacro (_, macro) -> pp_nmacro status macro ^ "." | NTactic (_,tacl) -> String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) tacl) | NCommand (_, cmd) -> pp_ncommand status cmd ^ "." - + let pp_comment status ~map_unicode_to_tex = function | Note (_,"") -> Printf.sprintf "\n" @@@ -209,5 -264,5 +267,5 @@@ let pp_statement status = function - | Executable (_, ex) -> pp_executable status ex + | Executable (_, ex) -> pp_executable status ex | Comment (_, c) -> pp_comment status c diff --combined 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 --combined 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 --combined matita/components/grafite_engine/grafiteEngine.ml index bd9e76ff2,93396d2bd..71f036904 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@@ -40,7 -40,7 +40,7 @@@ let basic_eval_unification_hint (t,n) s let inject_unification_hint = let basic_eval_unification_hint (t,n) - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe:_ ~refresh_uri_in_term ~refresh_uri_in_reference:_ ~alias_only status = if not alias_only then @@@ -88,7 -88,7 +88,7 @@@ let basic_eval_interpretation ~alias_on let inject_interpretation = let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_ ~alias_only = let rec refresh = @@@ -117,8 -117,8 +117,8 @@@ let basic_eval_alias (mode,diff) statu ;; let inject_alias = - let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term - ~refresh_uri_in_reference ~alias_only = + let basic_eval_alias (mode,diff) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ + ~refresh_uri_in_reference:_ ~alias_only:_ = basic_eval_alias (mode,diff) in GrafiteTypes.Serializer.register#run "alias" basic_eval_alias @@@ -138,7 -138,7 +138,7 @@@ let basic_eval_input_notation (l1,l2) s let inject_input_notation = let basic_eval_input_notation (l1,l2) - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe:_ ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status = if not alias_only then @@@ -169,7 -169,7 +169,7 @@@ let basic_eval_output_notation (l1,l2) let inject_output_notation = let basic_eval_output_notation (l1,l2) - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe:_ ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status = if not alias_only then @@@ -195,8 -195,8 +195,8 @@@ let eval_output_notation status data ;; let record_index_obj = - let aux l ~refresh_uri_in_universe - ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status + let aux l ~refresh_uri_in_universe:_ + ~refresh_uri_in_term ~refresh_uri_in_reference:_ ~alias_only status = let refresh_uri_in_term = refresh_uri_in_term (status:>NCic.status) in if not alias_only then @@@ -297,8 -297,8 +297,8 @@@ let basic_extract_ocaml_obj obj status let inject_extract_obj = let basic_extract_obj info - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference - ~alias_only status + ~refresh_uri_in_universe:__ ~refresh_uri_in_term:_ ~refresh_uri_in_reference + ~alias_only:_ status = let info= NCicExtraction.refresh_uri_in_info ~refresh_uri_in_reference info in status#set_extraction_db @@@ -309,8 -309,8 +309,8 @@@ let inject_extract_ocaml_obj = let basic_extract_ocaml_obj info - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference - ~alias_only status + ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference + ~alias_only:_ status = let info= OcamlExtractionTable.refresh_uri_in_info ~refresh_uri_in_reference ~refresh_uri:NCicLibrary.refresh_uri info in status#set_ocaml_extraction_db @@@ -358,7 -358,7 +358,7 @@@ let index_eq print uri (status:#NCic.st let record_index_eq = let basic_index_eq uri - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_ ~alias_only status = if not alias_only then index_eq false (NCicLibrary.refresh_uri uri) status else @@@ -381,7 -381,7 +381,7 @@@ let index_eq_for_auto status uri let inject_constraint = let basic_eval_add_constraint (acyclic,u1,u2) - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_ ~alias_only status = if not alias_only then @@@ -404,6 -404,17 +404,17 @@@ let eval_add_constraint status acyclic ;; let eval_ng_tac tac = + let just_to_tacstatus_just just text prefix_len = + match just with + | `Term t -> `Term (text,prefix_len,t) + | `Auto (l,params) -> + ( + match l with + | None -> `Auto (None,params) + | Some l -> `Auto (Some (List.map (fun t -> (text,prefix_len,t)) l),params) + ) + | _ -> assert false + in let rec aux f (text, prefix_len, tac) = match tac with | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) @@@ -481,6 -492,39 +492,39 @@@ 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 *) ;; @@@ -560,7 -604,7 +604,7 @@@ let extract_uris status uris let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = match cmd with - | GrafiteAst.Include (loc, mode, fname) -> + | GrafiteAst.Include (_loc, mode, fname) -> let _root, baseuri, fullpath, _rrelpath = Librarian.baseuri_of_script ~include_paths fname in let baseuri = NUri.uri_of_string baseuri in @@@ -571,7 -615,7 +615,7 @@@ ~alias_only ~baseuri ~fname:fullpath status in OcamlExtraction.print_open status (NCicLibrary.get_transitively_included status) - | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n + | GrafiteAst.UnificationHint (_loc, t, n) -> eval_unification_hint status t n | GrafiteAst.NCoercion (loc, name, compose, None) -> let status, t, ty, source, target = let o_t = NotationPt.Ident (name,None) in @@@ -602,7 -646,7 +646,7 @@@ GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) in eval_ncommand ~include_paths opts status (text,prefix_len,cmd) - | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) -> + | GrafiteAst.NCoercion (_loc, name, compose, Some (t, ty, source, target)) -> let status, composites = NCicCoercDeclaration.eval_ncoercion status name compose t ty source target in @@@ -610,11 -654,11 +654,11 @@@ let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *) let aliases = GrafiteDisambiguate.aliases_for_objs status composites in eval_alias status (mode,aliases) - | GrafiteAst.NQed (loc,index) -> + | GrafiteAst.NQed (_loc,index) -> if status#ng_mode <> `ProofMode then raise (GrafiteTypes.Command_error "Not in proof mode") else - let uri,height,menv,subst,obj_kind = status#obj in + let uri,_height,menv,subst,obj_kind = status#obj in if menv <> [] then raise (GrafiteTypes.Command_error"You can't Qed an incomplete theorem") @@@ -717,7 -761,7 +761,7 @@@ let status = match nobj with NCic.Inductive (is_ind,leftno,itl,_) -> List.fold_left (fun status it -> - (let _,ind_name,ty,cl = it in + (let _,ind_name,_ty,_cl = it in List.fold_left (fun status outsort -> let status = status#set_ng_mode `ProofMode in @@@ -743,11 -787,11 +787,11 @@@ | _ -> status in let status = match nobj with - NCic.Inductive (is_ind,leftno,itl,_) -> + NCic.Inductive (_is_ind,leftno,itl,_) -> (* first leibniz *) let status' = List.fold_left (fun status it -> - let _,ind_name,ty,cl = it in + let _,ind_name,_ty,_cl = it in let status = status#set_ng_mode `ProofMode in try (let status,invobj = @@@ -774,7 -818,7 +818,7 @@@ (* then JMeq *) List.fold_left (fun status it -> - let _,ind_name,ty,cl = it in + let _,ind_name,_ty,_cl = it in let status = status#set_ng_mode `ProofMode in try (let status,invobj = @@@ -829,7 -873,7 +873,7 @@@ exn -> NCicLibrary.time_travel old_status; raise exn) - | GrafiteAst.NCopy (log,tgt,src_uri, map) -> + | GrafiteAst.NCopy (_loc,tgt,src_uri, map) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else @@@ -860,14 -904,14 +904,14 @@@ let status = subst_metasenv_and_fix_names status in let status = status#set_ng_mode `ProofMode in eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) - | GrafiteAst.NObj (loc,obj,index) -> + | GrafiteAst.NObj (_loc,obj,index) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else let status,obj = GrafiteDisambiguate.disambiguate_nobj status ~baseuri:status#baseuri (text,prefix_len,obj) in - let uri,height,nmenv,nsubst,nobj = obj in + let _uri,_height,nmenv,_nsubst,_nobj = obj in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in let status = status#set_obj obj in let status = status#set_stack ninitial_stack in @@@ -878,12 -922,12 +922,12 @@@ eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,index)) | _ -> status) - | GrafiteAst.NDiscriminator (loc, indty) -> + | GrafiteAst.NDiscriminator (_loc, indty) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else let status = status#set_ng_mode `ProofMode in - let metasenv,subst,status,indty = + let _metasenv,_subst,status,indty = GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] [] (text,prefix_len,indty) in let indtyno, (_,_,tys,_,_),leftno = match indty with NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) -> @@@ -898,7 -942,7 +942,7 @@@ [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) | _ -> prerr_endline ("Discriminator: non empty metasenv"); status) - | GrafiteAst.NInverter (loc, name, indty, selection, sort) -> + | GrafiteAst.NInverter (_loc, name, indty, selection, sort) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else @@@ -918,7 -962,7 +962,7 @@@ "ninverter: found target %s, which is not a sort" (status#ppterm ~metasenv ~subst ~context:[] sort))) in let status = status#set_ng_mode `ProofMode in - let metasenv,subst,status,indty = + let _metasenv,_subst,status,indty = GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] subst (text,prefix_len,indty) in let indtyno,(_,leftno,tys,_,_) = @@@ -939,16 -983,16 +983,16 @@@ eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) | _ -> assert false) - | GrafiteAst.NUnivConstraint (loc,acyclic,u1,u2) -> + | GrafiteAst.NUnivConstraint (_loc,acyclic,u1,u2) -> eval_add_constraint status acyclic [`Type,u1] [`Type,u2] (* ex lexicon commands *) - | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> + | GrafiteAst.Interpretation (_loc, dsc, (symbol, args), cic_appl_pattern) -> let cic_appl_pattern = GrafiteDisambiguate.disambiguate_cic_appl_pattern status args cic_appl_pattern in eval_interpretation status (dsc,(symbol, args),cic_appl_pattern) - | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) -> + | GrafiteAst.Notation (_loc, dir, l1, associativity, precedence, l2) -> let l1 = CicNotationParser.check_l1_pattern l1 (dir = Some `RightToLeft) precedence associativity @@@ -959,23 -1003,23 +1003,23 @@@ in if dir <> Some `LeftToRight then eval_output_notation status (l1,l2) else status - | GrafiteAst.Alias (loc, spec) -> + | GrafiteAst.Alias (_loc, spec) -> let diff = (*CSC: Warning: this code should be factorized with the corresponding code in DisambiguatePp *) match spec with - | GrafiteAst.Ident_alias (id,uri) -> + | GrafiteAst.Ident_alias (id,_uri) -> [DisambiguateTypes.Id id,spec] - | GrafiteAst.Symbol_alias (symb, instance, desc) -> + | GrafiteAst.Symbol_alias (symb, instance, _desc) -> [DisambiguateTypes.Symbol (symb,instance),spec] - | GrafiteAst.Number_alias (instance,desc) -> + | GrafiteAst.Number_alias (instance,_desc) -> [DisambiguateTypes.Num instance,spec] in let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*) eval_alias status (mode,diff) ;; -let eval_comment opts status (text,prefix_len,c) = status +let eval_comment _opts status (_text,_prefix_len,_c) = status let rec eval_executable ~include_paths opts status (text,prefix_len,ex) = match ex with diff --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined matita/components/ng_extraction/mlutil.ml index 01a0cd85d,52881e183..9f553762a --- a/matita/components/ng_extraction/mlutil.ml +++ b/matita/components/ng_extraction/mlutil.ml @@@ -168,7 -168,7 +168,7 @@@ module Mlenv = struc let clean_free mle = let rem = ref Metaset.empty and add = ref Metaset.empty in - let clean m = match m.contents with + let clean m = match m.Miniml.contents with | None -> () | Some u -> rem := Metaset.add m !rem; add := find_free !add u in @@@ -238,18 -238,18 +238,18 @@@ let type_maxvar t (*s What are the type variables occurring in [t]. *) -let intset_union_map_list f l = - List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l +(*let intset_union_map_list f l = + List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l*) -let intset_union_map_array f a = - Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a +(*let intset_union_map_array f a = + Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a*) -let rec type_listvar = function +(*let rec type_listvar = function | Tmeta {contents = Some t} -> type_listvar t | Tvar i | Tvar' i -> Intset.singleton i | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b) | Tglob (_,l) -> intset_union_map_list type_listvar l - | _ -> Intset.empty + | _ -> Intset.empty*) (*s From [a -> b -> c] to [[a;b],c]. *) @@@ -467,12 -467,12 +467,12 @@@ let ast_occurs_itvl k k' t (*s Number of occurences of [Rel k] (resp. [Rel 1]) in [t]. *) -let nb_occur_k k t = +(*let nb_occur_k k t = let cpt = ref 0 in ast_iter_rel (fun i -> if i = k then incr cpt) t; - !cpt + !cpt*) -let nb_occur t = nb_occur_k 1 t +(*let nb_occur t = nb_occur_k 1 t*) (* Number of occurences of [Rel 1] in [t], with special treatment of match: occurences in different branches aren't added, but we rather use max. *) @@@ -596,7 -596,7 +596,7 @@@ let rec many_lams id a = functio | 0 -> a | n -> many_lams id (MLlam (id,a)) (pred n) -let anonym_lams a n = many_lams anonymous a n +(*let anonym_lams a n = many_lams anonymous a n*) let anonym_tmp_lams a n = many_lams (Tmp anonymous_name) a n let dummy_lams a n = many_lams Dummy a n @@@ -629,7 -629,7 +629,7 @@@ let rec test_eta_args_lift k n = functi (*s Computes an eta-reduction. *) -let eta_red e = +(*let eta_red e = let ids,t = collect_lams e in let n = List.length ids in if n = 0 then e @@@ -649,12 -649,12 +649,12 @@@ if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body) then named_lams ids (ast_lift (-p) body) else e - | _ -> e + | _ -> e*) (*s Computes all head linear beta-reductions possible in [(t a)]. Non-linear head beta-redex become let-in. *) -let rec linear_beta_red a t = match a,t with +(*let rec linear_beta_red a t = match a,t with | [], _ -> t | a0::a, MLlam (id,t) -> (match nb_occur_match t with @@@ -663,11 -663,11 +663,11 @@@ | _ -> let a = List.map (ast_lift 1) a in MLletin (id, a0, linear_beta_red a t)) - | _ -> MLapp (t, a) + | _ -> MLapp (t, a)*) -let rec tmp_head_lams = function +(*let rec tmp_head_lams = function | MLlam (id, t) -> MLlam (tmp_id id, tmp_head_lams t) - | e -> e + | e -> e*) (*s Applies a substitution [s] of constants by their body, plus linear beta reductions at modified positions. @@@ -675,7 -675,7 +675,7 @@@ reduction (this helps the inlining of recursors). *) -let rec ast_glob_subst _s _t = assert false (*CSC: reimplement match t with +let ast_glob_subst _s _t = assert false (*CSC: reimplement match t with | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in (try linear_beta_red a (Refmap'.find refe s) @@@ -789,7 -789,7 +789,7 @@@ let rec merge_ids ids ids' = match ids, let is_exn = function MLexn _ -> true | _ -> false -let rec permut_case_fun br _acc = +let permut_case_fun br _acc = let nb = ref max_int in Array.iter (fun (_,_,t) -> let ids, c = collect_lams t in @@@ -1168,7 -1168,7 +1168,7 @@@ let optimize_fix a (* Utility functions used in the decision of inlining. *) -let rec ml_size = function +(*let rec ml_size = function | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l | MLlam(_,t) -> 1 + ml_size t | MLcons(_,_,l) -> ml_size_list l @@@ -1181,14 -1181,14 +1181,14 @@@ and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l -and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l +and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l*) -let is_fix = function MLfix _ -> true | _ -> false +(*let is_fix = function MLfix _ -> true | _ -> false*) -let rec is_constr = function +(*let rec is_constr = function | MLcons _ -> true | MLlam(_,t) -> is_constr t - | _ -> false + | _ -> false*) (*s Strictness *) @@@ -1198,11 -1198,11 +1198,11 @@@ it begins by at least one non-strict lambda, since the corresponding argument to [t] might be unevaluated in the expanded code. *) -exception Toplevel +(*exception Toplevel*) -let lift n l = List.map ((+) n) l +(*let lift n l = List.map ((+) n) l*) -let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l +(*let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l*) (* This function returns a list of de Bruijn indices of non-strict variables, or raises [Toplevel] if it has an internal non-strict variable. @@@ -1212,7 -1212,7 +1212,7 @@@ variable to the candidates? We use this flag to check only the external lambdas, those that will correspond to arguments. *) -let rec non_stricts add cand = function +(*let rec non_stricts add cand = function | MLlam (_id,t) -> let cand = lift 1 cand in let cand = if add then 1::cand else cand in @@@ -1242,20 -1242,20 +1242,20 @@@ 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 | _ -> - cand + cand*) (* The real test: we are looking for internal non-strict variables, so we start with no candidates, and the only positive answer is via the [Toplevel] exception. *) -let is_not_strict t = +(*let is_not_strict t = try let _ = non_stricts true [] t in false - with Toplevel -> true + with Toplevel -> true*) (*s Inlining decision *) @@@ -1278,7 -1278,7 +1278,7 @@@ restriction for the moment. *) -let inline_test _r _t = +(*let inline_test _r _t = (*CSC:if not (auto_inline ()) then*) false (* else @@@ -1289,7 -1289,7 +1289,7 @@@ let t1 = eta_red t in let t2 = snd (collect_lams t1) in not (is_fix t2) && ml_size t < 12 && is_not_strict t -*) +*)*) (*CSC: (not) reimplemented let con_of_string s = @@@ -1313,9 -1313,9 +1313,9 @@@ let manual_inline_set ] Cset_env.empty*) -let manual_inline = function (*CSC: +(*let manual_inline = function (*CSC: | ConstRef c -> Cset_env.mem c manual_inline_set - |*) _ -> false + |*) _ -> false*) (* If the user doesn't say he wants to keep [t], we inline in two cases: \begin{itemize} diff --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined matita/components/ng_tactics/continuationals.ml index b10877130,5538a3c2d..dc54c89dd --- a/matita/components/ng_tactics/continuationals.ml +++ b/matita/components/ng_tactics/continuationals.ml @@@ -35,21 -35,23 +35,23 @@@ let fail msg = raise (Error msg type goal = int + type parameters = (string * string) list + module Stack = struct type switch = Open of goal | Closed of goal type locator = int * switch type tag = [ `BranchTag | `FocusTag | `NoTag ] - type entry = locator list * locator list * locator list * tag + type entry = locator list * locator list * locator list * tag * parameters type t = entry list - let empty = [ [], [], [], `NoTag ] + let empty = [ [], [], [], `NoTag , []] let fold ~env ~cont ~todo init stack = 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 @@@ -64,10 -66,10 +66,10 @@@ let map ~env ~cont ~todo = let depth = ref ~-1 in List.map - (fun (s, t, c, tag) -> + (fun (s, t, c, tag, p) -> incr depth; let d = !depth in - env d tag s, todo d tag t, cont d tag c, tag) + env d tag s, todo d tag t, cont d tag c, tag, p) let is_open = function _, Open _ -> true | _ -> false let close = function n, Open g -> n, Closed g | l -> l @@@ -103,39 -105,39 +105,39 @@@ let rec find_goal = function | [] -> raise (Failure "Continuationals.find_goal") - | (l :: _, _ , _ , _) :: _ -> goal_of_loc l - | ( _ , _ , l :: _, _) :: _ -> goal_of_loc l - | ( _ , l :: _, _ , _) :: _ -> goal_of_loc l + | (l :: _, _ , _ , _, _) :: _ -> goal_of_loc l + | ( _ , _ , l :: _, _, _) :: _ -> goal_of_loc l + | ( _ , l :: _, _ , _, _) :: _ -> goal_of_loc l | _ :: tl -> find_goal tl let is_empty = function | [] -> assert false - | [ [], [], [], `NoTag ] -> true + | [ [], [], [], `NoTag , _] -> true | _ -> false let of_nmetasenv metasenv = let goals = List.map (fun (g, _) -> g) metasenv in - [ zero_pos goals, [], [], `NoTag ] + [ zero_pos goals, [], [], `NoTag , []] let head_switches = function - | (locs, _, _, _) :: _ -> List.map switch_of_loc locs + | (locs, _, _, _, _) :: _ -> List.map switch_of_loc locs | [] -> assert false let head_goals = function - | (locs, _, _, _) :: _ -> List.map goal_of_loc locs + | (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs | [] -> assert false let head_tag = function - | (_, _, _, tag) :: _ -> tag + | (_, _, _, tag, _) :: _ -> tag | [] -> assert false let shift_goals = function - | _ :: (locs, _, _, _) :: _ -> List.map goal_of_loc locs + | _ :: (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs | [] -> assert false | _ -> [] @@@ -163,9 -165,10 +165,10 @@@ let pp_loc (i, s) = string_of_int i ^ pp_switch s in let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in - let pp_stack_entry (env, todo, cont, tag) = - sprintf "(%s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont) - (pp_tag tag) + let pp_par = function [] -> "" | _ as l -> List.fold_left (fun acc (k,v) -> acc ^ "K: " ^ k ^ " V: " ^ v ^ "; ") "" l in + let pp_stack_entry (env, todo, cont, tag, parameters) = + sprintf "(%s, %s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont) + (pp_tag tag) (pp_par parameters) in String.concat " :: " (List.map pp_stack_entry stack) end @@@ -270,7 -273,7 +273,7 @@@ struc let ostatus, stack = match cmd, stack with | _, [] -> assert false - | Tactical tac, (g, t, k, tag) :: s -> + | Tactical tac, (g, t, k, tag, p) :: s -> (* COMMENTED OUT TO ALLOW PARAMODULATION TO DO A * auto paramodulation.try assumption. * EVEN IF NO GOALS ARE LEFT OPEN BY AUTO. @@@ -300,49 -303,49 +303,49 @@@ debug_print (lazy ("closed: " ^ String.concat " " (List.map string_of_int gcn))); let stack = - (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s + (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s in sn, stack - | Dot, ([], _, [], _) :: _ -> + | Dot, ([], _, [], _, _) :: _ -> (* backward compatibility: do-nothing-dot *) new_stack stack - | Dot, (g, t, k, tag) :: s -> + | Dot, (g, t, k, tag, p) :: s -> (match filter_open g, k with - | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag) :: s) + | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag, p) :: s) | [], loc :: k -> assert (is_open loc); - new_stack (([ loc ], t, k, tag) :: s) + new_stack (([ loc ], t, k, tag, p) :: s) | _ -> fail (lazy "can't use \".\" here")) | Semicolon, _ -> new_stack stack - | Branch, (g, t, k, tag) :: s -> + | Branch, (g, t, k, tag, p) :: s -> (match init_pos g with | [] | [ _ ] -> fail (lazy "too few goals to branch"); | loc :: loc_tl -> new_stack - (([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s)) - | Shift, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s -> + (([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag,p) :: s)) + | Shift, (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s -> (match g' with | [] -> fail (lazy "no more goals to shift") | loc :: loc_tl -> new_stack - (([ loc ], t @+ filter_open g @+ k, [],`BranchTag) - :: (loc_tl, t', k', tag) :: s)) + (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p) + :: (loc_tl, t', k', tag, p') :: s)) | Shift, _ -> fail (lazy "can't shift goals here") - | Pos i_s, ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + | Pos i_s, ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in new_stack - ((l_js, t , [],`BranchTag) - :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + ((l_js, t , [],`BranchTag, p) + :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s) | Pos _, _ -> fail (lazy "can't use relative positioning here") - | Wildcard, ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s + | Wildcard, ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> new_stack - (([loc] @+ g', t, [], `BranchTag) - :: ([], t', k', tag) :: s) + (([loc] @+ g', t, [], `BranchTag, p) + :: ([], t', k', tag, p') :: s) | Wildcard, _ -> fail (lazy "can't use wildcard here") - | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s -> - new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s) + | Merge, (g, t, k,`BranchTag,_) :: (g', t', k', tag,p') :: s -> + new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag, p') :: s) | Merge, _ -> fail (lazy "can't merge goals here") | Focus [], _ -> assert false | Focus gs, s -> @@@ -355,8 -358,8 +358,8 @@@ if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then fail (lazy (sprintf "goal %d not found (or closed)" g))) gs; - new_stack ((zero_pos gs, [], [], `FocusTag) :: deep_close gs s) - | Unfocus, ([], [], [], `FocusTag) :: s -> new_stack s + new_stack ((zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s) + | Unfocus, ([], [], [], `FocusTag, _) :: s -> new_stack s | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open") in debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack))); diff --combined 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 --combined matita/components/ng_tactics/nTacStatus.ml index fc525c84a,1001d9808..118261af0 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@@ -97,24 -97,24 +97,24 @@@ let ctx_of (c,_) = c ; let mk_cic_term c t = c,t ;; let ppterm (status:#pstatus) t = - let uri,height,metasenv,subst,obj = status#obj in + let _uri,_height,metasenv,subst,_obj = status#obj in let context,t = t in status#ppterm ~metasenv ~subst ~context t ;; let ppcontext (status: #pstatus) c = - let uri,height,metasenv,subst,obj = status#obj in + let _uri,_height,metasenv,subst,_obj = status#obj in status#ppcontext ~metasenv ~subst c ;; let ppterm_and_context (status: #pstatus) t = - let uri,height,metasenv,subst,obj = status#obj in + let _uri,_height,metasenv,subst,_obj = status#obj in let context,t = t in status#ppcontext ~metasenv ~subst context ^ "\n ⊢ "^ status#ppterm ~metasenv ~subst ~context t ;; -let relocate status destination (source,t as orig) = +let relocate status destination (source,_t as orig) = pp(lazy("relocate:\n" ^ ppterm_and_context status orig)); pp(lazy("relocate in:\n" ^ ppcontext status destination)); let rc = @@@ -134,13 -134,13 +134,13 @@@ compute_ops (e::ctx) (cl1,cl2) else [ `Delift ctx; `Lift (List.rev ex) ] - | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 -> + | (n1, NCic.Def (_b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 -> if n1 = n2 && NCicReduction.are_convertible status ctx ~subst ~metasenv t1 t2 then compute_ops (e::ctx) (cl1,cl2) else [ `Delift ctx; `Lift (List.rev ex) ] - | (n1, NCic.Decl _)::cl1 as ex, (n2, NCic.Def _)::cl2 -> + | (_n1, NCic.Decl _)::_cl1 as ex, (_n2, NCic.Def _)::_cl2 -> [ `Delift ctx; `Lift (List.rev ex) ] | _::_ as ex, [] -> [ `Lift (List.rev ex) ] | [], _::_ -> [ `Delift ctx ] @@@ -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 @@@ -369,7 -378,7 +378,7 @@@ let select_ter else let _,_,_,subst,_ = status#obj in match t with - | NCic.Meta (i,lc) when List.mem_assoc i subst -> + | NCic.Meta (i,_lc) when List.mem_assoc i subst -> let _,_,t,_ = NCicUtils.lookup_subst i subst in aux ctx (status,already_found) t | NCic.Meta _ -> (status,already_found),t @@@ -460,7 -469,7 +469,7 @@@ let analyse_indty status ty let _,_,_,cl = List.nth tl i in let consno = List.length cl in let left, right = HExtlib.split_nth lno args in - status, (ref, consno, left, right) + status, (ref, consno, left, right, cl) ;; let apply_subst status ctx t = diff --combined matita/components/ng_tactics/nTactics.ml index 1aba2be9d,a8a78999a..721d9165b --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@@ -31,16 -31,16 +31,16 @@@ let dot_tac status let gstatus = match status#stack with | [] -> assert false - | ([], _, [], _) :: _ as stack -> + | ([], _, [], _, _) :: _ as stack -> (* backward compatibility: do-nothing-dot *) stack - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> match filter_open g, k with | loc :: loc_tl, _ -> - (([ loc ], t, loc_tl @+ k, tag) :: s) + (([ loc ], t, loc_tl @+ k, tag, p) :: s) | [], loc :: k -> assert (is_open loc); - (([ loc ], t, k, tag) :: s) + (([ loc ], t, k, tag, p) :: s) | _ -> fail (lazy "can't use \".\" here") in status#set_stack gstatus @@@ -50,12 -50,12 +50,12 @@@ let branch_tac ?(force=false) status let gstatus = match status#stack with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> match init_pos g with (* TODO *) | [] -> fail (lazy "empty goals") - | [_] when (not force) -> fail (lazy "too few goals to branch") + | [_] when (not force) -> fail (lazy "too few goals to branch") | loc :: loc_tl -> - ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s + ([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag, p) :: s in status#set_stack gstatus ;; @@@ -63,12 -63,12 +63,12 @@@ let shift_tac status = let gstatus = match status#stack with - | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s -> + | (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s -> (match g' with | [] -> fail (lazy "no more goals to shift") | loc :: loc_tl -> - (([ loc ], t @+ filter_open g @+ k, [],`BranchTag) - :: (loc_tl, t', k', tag) :: s)) + (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p) + :: (loc_tl, t', k', tag, p') :: s)) | _ -> fail (lazy "can't shift goals here") in status#set_stack gstatus @@@ -78,11 -78,11 +78,11 @@@ let pos_tac i_s status let gstatus = match status#stack with | [] -> assert false - | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in - ((l_js, t , [],`BranchTag) - :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + ((l_js, t , [],`BranchTag, p) + :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s) | _ -> fail (lazy "can't use relative positioning here") in status#set_stack gstatus @@@ -92,7 -92,7 +92,7 @@@ let case_tac lab status let gstatus = match status#stack with | [] -> assert false - | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> let l_js = List.filter @@@ -101,8 -101,8 +101,8 @@@ match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with attrs,_,_ when List.mem (`Name lab) attrs -> true | _ -> false) ([loc] @+ g') in - ((l_js, t , [],`BranchTag) - :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + ((l_js, t , [],`BranchTag, p) + :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s) | _ -> fail (lazy "can't use relative positioning here") in status#set_stack gstatus @@@ -112,9 -112,9 +112,9 @@@ let wildcard_tac status let gstatus = match status#stack with | [] -> assert false - | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s + | ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> - (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s) + (([loc] @+ g', t, [], `BranchTag, p) :: ([], t', k', tag, p') :: s) | _ -> fail (lazy "can't use wildcard here") in status#set_stack gstatus @@@ -124,8 -124,8 +124,8 @@@ let merge_tac status let gstatus = match status#stack with | [] -> assert false - | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s -> - ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s) + | (g, t, k,`BranchTag, _) :: (g', t', k', tag, p) :: s -> + ((t @+ filter_open g @+ g' @+ k, t', k', tag, p) :: s) | _ -> fail (lazy "can't merge goals here") in status#set_stack gstatus @@@ -145,7 -145,7 +145,7 @@@ let focus_tac gs status if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then fail (lazy (sprintf "goal %d not found (or closed)" g))) gs; - (zero_pos gs, [], [], `FocusTag) :: deep_close gs s + (zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s in status#set_stack gstatus ;; @@@ -154,7 -154,7 +154,7 @@@ let unfocus_tac status let gstatus = match status#stack with | [] -> assert false - | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s + | (g, [], [], `FocusTag, _) :: s when filter_open g = [] -> s | _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^ Continuationals.Stack.pp s)) in @@@ -165,12 -165,12 +165,12 @@@ let skip_tac status let gstatus = match status#stack with | [] -> assert false - | (gl, t, k, tag) :: s -> + | (gl, t, k, tag, p) :: s -> let gl = List.map switch_of_loc gl in if List.exists (function Open _ -> true | Closed _ -> false) gl then fail (lazy "cannot skip an open goal") else - ([],t,k,tag) :: s + ([],t,k,tag,p) :: s in status#set_stack gstatus ;; @@@ -219,7 -219,7 +219,7 @@@ let change_stack_type (status : 'a #NTa ;; let exec tac (low_status : #lowtac_status) g = - let stack = [ [0,Open g], [], [], `NoTag ] in + let stack = [ [0,Open g], [], [], `NoTag, [] ] in let status = change_stack_type low_status stack in let status = tac status in (low_status#set_pstatus status)#set_obj status#obj @@@ -228,7 -228,7 +228,7 @@@ let distribute_tac tac (status : #tac_status) = match status#stack with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> debug_print (lazy ("context length " ^string_of_int (List.length g))); let rec aux s go gc = function @@@ -258,7 -258,7 +258,7 @@@ debug_print (lazy ("closed: " ^ String.concat " " (List.map string_of_int gcn))); let stack = - (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s + (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s in ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn ;; @@@ -312,7 -312,7 +312,7 @@@ let assumption_tac status = distribute_ let find_in_context name context = let rec aux acc = function | [] -> raise Not_found - | (hd,_) :: tl when hd = name -> acc + | (hd,_) :: _ when hd = name -> acc | _ :: tl -> aux (acc + 1) tl in aux 1 context @@@ -492,6 -492,7 +492,7 @@@ type indtyinfo = leftno: int; consno: int; reference: NReference.reference; + cl: NCic.constructor list; } ;; @@@ -502,11 -503,12 +503,12 @@@ 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 { rightno = rightno; leftno = leftno; consno = consno; reference = r; + cl = cl; }; exec id_tac orig_status goal) ;; @@@ -522,6 -524,33 +524,33 @@@ let sort_of_goal_tac sortref = distribu status) ;; + let pp_ref reference = + let NReference.Ref (uri,spec) = reference in + let nstring = NUri.string_of_uri uri in + (*"Shareno: " ^ (string_of_int nuri) ^*) "Uri: " ^ nstring ^ + (match spec with + | NReference.Decl -> "Decl" + | NReference.Def n -> "Def " ^ (string_of_int n) + | NReference.Fix (n1,n2,n3) -> "Fix " ^ (string_of_int n1) ^ " " ^ (string_of_int n2) ^ " " ^ (string_of_int n3)(* fixno, recparamno, height *) + | NReference.CoFix n -> "CoFix " ^ (string_of_int n) + | NReference.Ind (b,n1,n2) -> "Ind " ^ (string_of_bool b) ^ " " ^ (string_of_int n1) ^ " " ^ (string_of_int n2)(* inductive, indtyno, leftno *) + | NReference.Con (n1,n2,n3) -> "Con " ^ (string_of_int n1) ^ " " ^ (string_of_int n2) ^ " " ^ (string_of_int n3)(* indtyno, constrno, leftno *) + ) ;; + + let pp_cl cl = + let rec pp_aux acc = + match acc with + | [] -> "" + | (_,consname,_) :: tl -> consname ^ ", " ^ pp_aux tl + in + pp_aux cl + ;; + + let pp_indtyinfo ity = "leftno: " ^ (string_of_int ity.leftno) ^ ", consno: " ^ (string_of_int + ity.consno) ^ ", rightno: " ^ + (string_of_int ity.rightno) ^ ", reference: " ^ (pp_ref ity.reference) ^ ", + cl: " ^ (pp_cl ity.cl);; + let elim_tac ~what:(txt,len,what) ~where = let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in let indtyinfo = ref None in @@@ -597,7 -626,7 +626,7 @@@ let cases ~what status goal let gty = get_goalty status goal in let status, what = disambiguate status (ctx_of gty) what `XTInd in let status, ty = typeof status (ctx_of what) what in - let status, (ref, consno, _, _) = analyse_indty status ty in + let status, (ref, consno, _, _,_) = analyse_indty status ty in let status, what = term_of_cic_term status what (ctx_of gty) in let t = NCic.Match (ref,NCic.Implicit `Term, what, @@@ -628,7 -657,7 +657,7 @@@ let case1_tac name let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal -> let gty = get_goalty status goal in - let status, (r,consno,_,_) = analyse_indty status gty in + let status, (r,consno,_,_,_) = analyse_indty status gty in if num < 1 || num > consno then fail (lazy "Non existant constructor"); let ref = NReference.mk_constructor num r in let t = @@@ -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 --combined matita/components/ng_tactics/nnAuto.ml index 0f11cab74,cb73e873e..3ac6040dc --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@@ -13,7 -13,7 +13,7 @@@ open Print let print ?(depth=0) s = prerr_endline (String.make (2*depth) ' '^Lazy.force s) -let noprint ?(depth=0) _ = () +let noprint ?depth:(_=0) _ = () let debug_print = noprint open Continuationals.Stack @@@ -54,7 -54,7 +54,7 @@@ let incr_uses tbl item let toref f tbl t = match t with | Ast.NRef n -> - f tbl n + f tbl n | Ast.NCic _ (* local candidate *) | _ -> () @@@ -66,7 -66,7 +66,7 @@@ let is_relevant tbl item else true with Not_found -> true -let print_stat status tbl = +let print_stat _status tbl = let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in let relevance v = float !(v.uses) /. float !(v.nominations) in let vcompare (_,v1) (_,v2) = @@@ -82,7 -82,7 +82,7 @@@ "; uses = " ^ (string_of_int !(v.uses)) ^ "; nom = " ^ (string_of_int !(v.nominations)) in lazy ("\n\nSTATISTICS:\n" ^ - String.concat "\n" (List.map vstring l)) + String.concat "\n" (List.map vstring l)) (* ======================= utility functions ========================= *) module IntSet = Set.Make(struct type t = int let compare = compare end) @@@ -238,7 -238,7 +238,7 @@@ let solve f status eq_cache goal debug_print (lazy ("refining: "^(status#ppterm ctx subst metasenv pt))); let stamp = Unix.gettimeofday () in let metasenv, subst, pt, pty = - (* NCicRefiner.typeof status + (* NCicRefiner.typeof status (* (status#set_coerc_db NCicCoercion.empty_db) *) metasenv subst ctx pt None in debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt))); @@@ -259,14 -259,14 +259,14 @@@ NCicRefiner.RefineFailure msg | NCicRefiner.Uncertain msg -> debug_print (lazy ("WARNING U: refining in fast_eq_check failed\n" ^ - snd (Lazy.force msg) ^ - "\n in the environment\n" ^ - status#ppmetasenv subst metasenv)); None + snd (Lazy.force msg) ^ + "\n in the environment\n" ^ + status#ppmetasenv subst metasenv)); None | NCicRefiner.AssertFailure msg -> debug_print (lazy ("WARNING F: refining in fast_eq_check failed" ^ Lazy.force msg ^ - "\n in the environment\n" ^ - status#ppmetasenv subst metasenv)); None + "\n in the environment\n" ^ + status#ppmetasenv subst metasenv)); None | Sys.Break as e -> raise e | _ -> None in @@@ -292,7 -292,10 +292,10 @@@ let auto_eq_check eq_cache status | Error _ -> debug_print (lazy ("no paramod proof found"));[] ;; - let index_local_equations eq_cache status = + let index_local_equations eq_cache ?(flag=false) status = + if flag then + NCicParamod.empty_state + else begin noprint (lazy "indexing equations"); let open_goals = head_goals status#stack in let open_goal = List.hd open_goals in @@@ -316,9 -319,10 +319,10 @@@ | 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 @@@ -356,7 -360,7 +360,7 @@@ eq_cache lemmas ;; -let fast_eq_check_tac ~params s = +let fast_eq_check_tac ~params:_ s = let unit_eq = index_local_equations s#eq_cache s in dist_fast_eq_check unit_eq s ;; @@@ -367,7 -371,7 +371,7 @@@ let paramod eq_cache status goal | s::_ -> s ;; -let paramod_tac ~params s = +let paramod_tac ~params:_ s = let unit_eq = index_local_equations s#eq_cache s in NTactics.distribute_tac (paramod unit_eq) s ;; @@@ -416,7 -420,7 +420,7 @@@ let close_wrt_context status (fun ty ctx_entry -> match ctx_entry with | name, NCic.Decl t -> NCic.Prod(name,t,ty) - | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty) + | _name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty) ;; let args_for_context ?(k=1) ctx = @@@ -424,8 -428,8 +428,8 @@@ List.fold_left (fun (n,l) ctx_entry -> match ctx_entry with - | name, NCic.Decl t -> n+1,NCic.Rel(n)::l - | name, NCic.Def(bo, _) -> n+1,l) + | _name, NCic.Decl _t -> n+1,NCic.Rel(n)::l + | _name, NCic.Def(_bo, _) -> n+1,l) (k,[]) ctx in args @@@ -444,7 -448,7 +448,7 @@@ let refresh metasenv List.fold_left (fun (metasenv,subst) (i,(iattr,ctx,ty)) -> let ikind = NCicUntrusted.kind_of_meta iattr in - let metasenv,j,instance,ty = + let metasenv,_j,instance,ty = NCicMetaSubst.mk_meta ~attrs:iattr metasenv ctx ~with_type:ty ikind in let s_entry = i,(iattr, ctx, instance, ty) in @@@ -460,12 -464,12 +464,12 @@@ let close_metasenv status metasenv subs *) let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in List.fold_left - (fun (subst,objs) (i,(iattr,ctx,ty)) -> + (fun (subst,objs) (i,(_iattr,ctx,ty)) -> let ty = NCicUntrusted.apply_subst status subst ctx ty in let ctx = NCicUntrusted.apply_subst_context status ~fix_projections:true subst ctx in - let (uri,_,_,_,obj) as okind = + let (uri,_,_,_,_obj) as okind = constant_for_meta status ctx ty i in try NCicEnvironment.check_and_add_obj status okind; @@@ -517,7 -521,7 +521,7 @@@ let replace_meta status i args target | _ -> let args = List.map (NCicSubstitution.subst_meta status lc) args in NCic.Appl(NCic.Rel k::args)) - | NCic.Meta (j,lc) as m -> + | NCic.Meta (_j,lc) as m -> (match lc with _,NCic.Irl _ -> m | n,NCic.Ctx l -> @@@ -532,7 -536,7 +536,7 @@@ let close_wrt_metasenv status subst = List.fold_left - (fun ty (i,(iattr,ctx,mty)) -> + (fun ty (i,(_iattr,ctx,mty)) -> let mty = NCicUntrusted.apply_subst status subst ctx mty in let ctx = NCicUntrusted.apply_subst_context status ~fix_projections:true @@@ -575,20 -579,20 +579,20 @@@ let saturate_to_ref status metasenv sub NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in match ty with | NCic.Const(NReference.Ref (_,NReference.Def _) as nre) - when nre<>nref -> - let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in - aux metasenv bo (args@moreargs) + when nre<>nref -> + let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in + aux metasenv bo (args@moreargs) | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl) - when nre<>nref -> - let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in - aux metasenv (NCic.Appl(bo::tl)) (args@moreargs) + when nre<>nref -> + let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in + aux metasenv (NCic.Appl(bo::tl)) (args@moreargs) | _ -> ty,metasenv,(args@moreargs) in aux metasenv ty [] let smart_apply t unit_eq status g = - let n,h,metasenv,subst,o = status#obj in - let gname, ctx, gty = List.assoc g metasenv in + let n,h,metasenv,_subst,o = status#obj in + let _gname, ctx, gty = List.assoc g metasenv in (* let ggty = mk_cic_term context gty in *) let status, t = disambiguate status ctx t `XTNone in let status,t = term_of_cic_term status t ctx in @@@ -598,9 -602,9 +602,9 @@@ match gty with | NCic.Const(nref) | NCic.Appl(NCic.Const(nref)::_) -> - saturate_to_ref status metasenv subst ctx nref ty + saturate_to_ref status metasenv subst ctx nref ty | _ -> - NCicMetaSubst.saturate status metasenv subst ctx ty 0 in + NCicMetaSubst.saturate status metasenv subst ctx ty 0 in let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in let status = status#set_obj (n,h,metasenv,subst,o) in let pterm = if args=[] then t else @@@ -629,7 -633,7 +633,7 @@@ debug_print(lazy("ritorno da fast_eq_check")); res with - | NCicEnvironment.ObjectNotFound s as e -> + | NCicEnvironment.ObjectNotFound _s as e -> raise (Error (lazy "eq_coerc non yet defined",Some e)) | Error _ as e -> debug_print (lazy "error"); raise e (* FG: for now we catch TypeCheckerFailure; to be understood *) @@@ -892,6 -896,7 +896,7 @@@ type flags = do_types : bool; (* solve goals in Type *) last : bool; (* last goal: take first solution only *) candidates: Ast.term list option; + local_candidates: bool; maxwidth : int; maxsize : int; maxdepth : int; @@@ -908,20 -913,20 +913,20 @@@ type cache let add_to_trace status ~depth cache t = match t with | Ast.NRef _ -> - debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t)); - {cache with trace = t::cache.trace} + debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t)); + {cache with trace = t::cache.trace} | Ast.NCic _ (* local candidate *) | _ -> (*not an application *) cache let pptrace status tr = (lazy ("Proof Trace: " ^ (String.concat ";" - (List.map (NotationPp.pp_term status) tr)))) + (List.map (NotationPp.pp_term status) tr)))) (* not used let remove_from_trace cache t = match t with | Ast.NRef _ -> - (match cache.trace with - | _::tl -> {cache with trace = tl} + (match cache.trace with + | _::tl -> {cache with trace = tl} | _ -> assert false) | Ast.NCic _ (* local candidate *) | _ -> (*not an application *) cache *) @@@ -952,7 -957,7 +957,7 @@@ let init_cache ?(facts=[]) ?(under_insp unit_eq = unit_eq; trace = trace} -let only signature _context candidate = true +let only _signature _context _candidate = true (* (* TASSI: nel trie ci mettiamo solo il body, non il ty *) let candidate_ty = @@@ -982,7 -987,7 +987,7 @@@ let sort_candidates status ctx candidat let ty = NCicTypeChecker.typeof status subst metasenv ctx t in let res = branch status (mk_cic_term ctx ty) in noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = " - ^ (string_of_int res))); + ^ (string_of_int res))); res in let candidates = List.map (fun t -> branch t,t) candidates in @@@ -990,7 -995,7 +995,7 @@@ List.sort (fun (a,_) (b,_) -> a - b) candidates in let candidates = List.map snd candidates in noprint (lazy ("candidates =\n" ^ (String.concat "\n" - (List.map (NotationPp.pp_term status) candidates)))); + (List.map (NotationPp.pp_term status) candidates)))); candidates let sort_new_elems l = @@@ -1000,20 -1005,20 +1005,20 @@@ let rec stack_goals level gs if level = 0 then [] else match gs with | [] -> assert false - | (g,_,_,_)::s -> + | (g,_,_,_,_)::s -> let is_open = function | (_,Continuationals.Stack.Open i) -> Some i | (_,Continuationals.Stack.Closed _) -> None in - HExtlib.filter_map is_open g @ stack_goals (level-1) s + HExtlib.filter_map is_open g @ stack_goals (level-1) s ;; let open_goals level status = stack_goals level status#stack ;; -let try_candidate ?(smart=0) flags depth status eq_cache ctx t = +let try_candidate ?(smart=0) _flags depth status eq_cache _ctx t = try - let old_og_no = List.length (open_goals (depth+1) status) in + (*let old_og_no = List.length (open_goals (depth+1) status) in*) debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : " ^ (NotationPp.pp_term status) t)); let status = @@@ -1045,11 -1050,11 +1050,11 @@@ (* some flexibility *) if og_no - old_og_no > res then (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " - ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no))); + ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no))); debug_print ~depth (lazy "strange application"); None) else *) (incr candidate_no; Some ((!candidate_no,t),status)) - with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None + with Error _ -> debug_print ~depth (lazy "failed"); None ;; let sort_of status subst metasenv ctx t = @@@ -1065,14 -1070,14 +1070,14 @@@ let type0= NUri.uri_of_string ("cic:/ma let perforate_small status subst metasenv context t = let rec aux = function | NCic.Appl (hd::tl) -> - let map t = - let s = sort_of status subst metasenv context t in - match s with - | NCic.Sort(NCic.Type [`Type,u]) - when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0)) - | _ -> aux t - in - NCic.Appl (hd::List.map map tl) + let map t = + let s = sort_of status subst metasenv context t in + match s with + | NCic.Sort(NCic.Type [`Type,u]) + when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0)) + | _ -> aux t + in + NCic.Appl (hd::List.map map tl) | t -> t in aux t @@@ -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 = @@@ -1106,46 -1119,62 +1119,62 @@@ let raw_weak_gty, weak_gty = if smart then match raw_gty with - | NCic.Appl _ - | NCic.Const _ - | NCic.Rel _ -> + | NCic.Appl _ + | NCic.Const _ + | NCic.Rel _ -> let raw_weak = perforate_small status subst metasenv context raw_gty in let weak = mk_cic_term context raw_weak in noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak)); Some raw_weak, Some (weak) - | _ -> None,None + | _ -> None,None else None,None in (* we now compute global candidates *) let global_cands, smart_global_cands = - let mapf s = - let to_ast = function - | NCic.Const r when true - (*is_relevant statistics r*) -> Some (Ast.NRef r) - (* | NCic.Const _ -> None *) - | _ -> assert false in - HExtlib.filter_map - to_ast (NDiscriminationTree.TermSet.elements s) in - let g,l = - get_cands - (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe) - NDiscriminationTree.TermSet.diff - NDiscriminationTree.TermSet.empty - raw_gty raw_weak_gty in - mapf g, mapf l in + let mapf s = + let to_ast = function + | NCic.Const r when true + (*is_relevant statistics r*) -> Some (Ast.NRef r) + (* | NCic.Const _ -> None *) + | _ -> assert false in + HExtlib.filter_map + to_ast (NDiscriminationTree.TermSet.elements s) in + let g,l = + get_cands + (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe) + NDiscriminationTree.TermSet.diff + NDiscriminationTree.TermSet.empty + raw_gty raw_weak_gty in + mapf g, mapf l + in + let global_cands,smart_global_cands = + if flags.local_candidates then global_cands,smart_global_cands + else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri + (NUri.string_of_uri + uri) | _ -> false) + in filter global_cands,filter smart_global_cands + in (* we now compute local candidates *) let local_cands,smart_local_cands = let mapf s = let to_ast t = - let _status, t = term_of_cic_term status t context - in Ast.NCic t in - List.map to_ast (Ncic_termSet.elements s) in + let _status, t = term_of_cic_term status t context + in Ast.NCic t in + List.map to_ast (Ncic_termSet.elements s) in let g,l = get_cands - (fun ty -> search_in_th ty cache) - Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in - mapf g, mapf l in + (fun ty -> search_in_th ty cache) + Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in + mapf g, mapf l + in + let local_cands,smart_local_cands = + if flags.local_candidates then local_cands,smart_local_cands + else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri + (NUri.string_of_uri + uri) | _ -> false) + in filter local_cands,filter smart_local_cands + in (* we now splits candidates in facts or not facts *) let test = is_a_fact_ast status subst metasenv context in let by,given_candidates = @@@ -1198,8 -1227,8 +1227,8 @@@ let applicative_case ~pfailed depth sig 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 + | NCic.Prod _ -> true, false + | _ -> false, NCicParamod.is_equation status metasenv subst context t in debug_print ~depth (lazy (string_of_bool is_eq)); (* new *) @@@ -1209,7 -1238,7 +1238,7 @@@ flags status tcache signature gty in let sm = if is_eq || is_prod then 0 else 2 in - let sm1 = if flags.last then 2 else 0 in + (*let sm1 = if flags.last then 2 else 0 in *) let maxd = (depth + 1 = flags.maxdepth) in let try_candidates only_one sm acc candidates = List.fold_left @@@ -1294,7 -1323,7 +1323,7 @@@ let is_subsumed depth filter_depth stat NCicMetaSubst.mk_meta metasenv ctx ~with_type:implication `IsType in let status = status#set_obj (n,h,metasenv,subst,obj) in - let status = status#set_stack [([1,Open j],[],[],`NoTag)] in + let status = status#set_stack [([1,Open j],[],[],`NoTag,[])] in try let status = NTactics.intro_tac "foo" status in let status = @@@ -1335,7 -1364,7 +1364,7 @@@ let is_prod status let intro ~depth status facts name = let status = NTactics.intro_tac name status in - let _, ctx, ngty = current_goal status in + let _, ctx, _ngty = current_goal status in let t = mk_cic_term ctx (NCic.Rel 1) in let status, keys = keys_of_term status t in let facts = List.fold_left (add_to_th t) facts keys in @@@ -1358,11 -1387,11 +1387,11 @@@ let rec intros_facts ~depth status fact | _ -> status, facts ;; - let intros ~depth status cache = + let intros ~depth status ?(use_given_only=false) cache = match is_prod status with | `Inductive _ | `Some _ -> - let trace = cache.trace in + let trace = cache.trace in let status,facts = intros_facts ~depth status cache.facts in @@@ -1371,7 -1400,7 +1400,7 @@@ [(0,Ast.Ident("__intros",None)),status], cache else (* we reindex the equation from scratch *) - 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 let status = NTactics.merge_tac status in [(0,Ast.Ident("__intros",None)),status], init_cache ~facts ~unit_eq () ~trace @@@ -1407,7 -1436,7 +1436,7 @@@ let is_meta status gty | _ -> false ;; - let do_something signature flags status g depth gty cache = + let do_something signature flags status g depth gty ?(use_given_only=false) cache = (* if the goal is meta we close it with I:True. This should work thanks to the toplogical sorting of goals. *) if is_meta status gty then @@@ -1416,7 -1445,7 +1445,7 @@@ let s = NTactics.apply_tac ("",0,t) status in [(0,t),s], cache else - let l0, cache = intros ~depth status cache in + let l0, cache = intros ~depth status cache ~use_given_only in if l0 <> [] then l0, cache else (* whd *) @@@ -1472,7 -1501,7 +1501,7 @@@ let sort_tac status let gstatus = match status#stack with | [] -> assert false - | (goals, t, k, tag) :: s -> + | (goals, t, k, tag, p) :: s -> let g = head_goals status#stack in let sortedg = (List.rev (MS.topological_sort g (deps status))) in @@@ -1487,7 -1516,7 +1516,7 @@@ let sorted_goals = List.map (fun i -> List.find (is_it i) goals) sortedg in - (sorted_goals, t, k, tag) :: s + (sorted_goals, t, k, tag, p) :: s in status#set_stack gstatus ;; @@@ -1496,13 -1525,13 +1525,13 @@@ let clean_up_tac status let gstatus = match status#stack with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> let is_open = function | (_,Continuationals.Stack.Open _) -> true | (_,Continuationals.Stack.Closed _) -> false in let g' = List.filter is_open g in - (g', t, k, tag) :: s + (g', t, k, tag, p) :: s in status#set_stack gstatus ;; @@@ -1532,12 -1561,12 +1561,12 @@@ let deep_focus_tac level focus status let rec slice level gs = if level = 0 then [],[],gs else match gs with - | [] -> assert false - | (g, t, k, tag) :: s -> + | [] -> assert false + | (g, t, k, tag,p) :: s -> let f,o,gs = slice (level-1) s in let f1,o1 = List.partition in_focus g in - (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs + (f1,[],[],`BranchTag, [])::f, (o1, t, k, tag, p)::o, gs in let gstatus = let f,o,s = slice level status#stack in f@o@s @@@ -1548,25 -1577,24 +1577,24 @@@ let move_to_side level status = match status#stack with | [] -> assert false - | (g,_,_,_)::tl -> + | (g,_,_,_,_)::tl -> let is_open = function | (_,Continuationals.Stack.Open i) -> Some i | (_,Continuationals.Stack.Closed _) -> None 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 - let rec auto_clusters ?(top=false) - flags signature cache depth status : unit = + let rec auto_clusters ?(top=false) flags signature cache depth ?(use_given_only=false) status : unit = debug_print ~depth (lazy ("entering auto clusters at depth " ^ - (string_of_int depth))); + (string_of_int depth))); debug_print ~depth (pptrace status cache.trace); (* ignore(Unix.select [] [] [] 0.01); *) let status = clean_up_tac status in @@@ -1577,15 -1605,15 +1605,15 @@@ 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} + 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 if List.length goals < 2 then - let cache = top_cache ~depth top status cache in - auto_main flags signature cache depth status + let cache = top_cache ~depth top status cache ~use_given_only in + auto_main flags signature cache depth status ~use_given_only else let all_goals = open_goals (depth+1) status in debug_print ~depth (lazy ("goals = " ^ @@@ -1596,17 -1624,17 +1624,17 @@@ (fun gl -> if List.length gl > flags.maxwidth then begin - debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); - HLog.warn (sprintf "global width (%u) exceeded: %u" - flags.maxwidth (List.length gl)); - raise (Gaveup cache.failures) - end else ()) classes; + debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); + HLog.warn (sprintf "global width (%u) exceeded: %u" + flags.maxwidth (List.length gl)); + raise (Gaveup cache.failures) + end else ()) classes; if List.length classes = 1 then let flags = {flags with last = (List.length all_goals = 1)} in - (* no need to cluster *) - let cache = top_cache ~depth top status cache in - auto_main flags signature cache depth status + (* no need to cluster *) + let cache = top_cache ~depth top status cache ~use_given_only in + auto_main flags signature cache depth status ~use_given_only else let classes = if top then List.rev classes else classes in debug_print ~depth @@@ -1623,21 -1651,21 +1651,21 @@@ let flags = {flags with last = (List.length gl = 1)} in let lold = List.length status#stack in - debug_print ~depth (lazy ("stack length = " ^ - (string_of_int lold))); + debug_print ~depth (lazy ("stack length = " ^ + (string_of_int lold))); let fstatus = deep_focus_tac (depth+1) gl status in - let cache = top_cache ~depth top fstatus cache in + let cache = top_cache ~depth top fstatus cache ~use_given_only in try debug_print ~depth (lazy ("focusing on" ^ String.concat "," (List.map string_of_int gl))); - auto_main flags signature cache depth fstatus; assert false + auto_main flags signature cache depth fstatus ~use_given_only; assert false with | Proved(status,trace) -> - let status = NTactics.merge_tac status in - let cache = {cache with trace = trace} in - let lnew = List.length status#stack in - assert (lold = lnew); - (status,cache,true) + let status = NTactics.merge_tac status in + let cache = {cache with trace = trace} in + let lnew = List.length status#stack in + assert (lold = lnew); + (status,cache,true) | Gaveup failures when top -> let cache = {cache with failures = failures} in (status,cache,b) @@@ -1645,55 -1673,55 +1673,55 @@@ (status,cache,false) classes in let rec final_merge n s = - if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s) + if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s) in let status = final_merge depth status in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures) 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 = " ^ - (string_of_int (List.length status#stack)))); + (string_of_int (List.length status#stack)))); (* ignore(Unix.select [] [] [] 0.01); *) let status = sort_tac (clean_up_tac status) in let goals = head_goals status#stack in 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 debug_print ~depth (lazy "FAIL LOCAL WIDTH"); - HLog.warn (sprintf "local width (%u) exceeded: %u" - flags.maxwidth ng); - raise (Gaveup cache.failures) + HLog.warn (sprintf "local width (%u) exceeded: %u" + flags.maxwidth ng); + raise (Gaveup cache.failures) end else if depth = flags.maxdepth then - raise (Gaveup cache.failures) + raise (Gaveup cache.failures) else let status = NTactics.branch_tac ~force:true status in let g,gctx, gty = current_goal status in @@@ -1713,7 -1741,7 +1741,7 @@@ (* for efficiency reasons, in this case we severely cripple the search depth *) (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1))); - auto_main flags signature cache (depth+1) status) + auto_main flags signature cache (depth+1) status ~use_given_only) (* check for loops *) else if is_subsumed depth false status closegty (snd cache.under_inspection) then (debug_print ~depth (lazy "SUBSUMED"); @@@ -1723,40 -1751,40 +1751,40 @@@ (debug_print ~depth (lazy "ALREADY MET"); raise (Gaveup cache.failures)) else - let new_sig = height_of_goal g status in + let new_sig = height_of_goal g status in if new_sig < signature then - (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig))); - debug_print ~depth (lazy ("olds = " ^ (string_of_int signature)))); + (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig))); + debug_print ~depth (lazy ("olds = " ^ (string_of_int signature)))); let alternatives, cache = - do_something signature flags status g depth gty cache in + do_something signature flags status g depth gty cache ~use_given_only in let loop_cache = if flags.last then - let l,tree = cache.under_inspection in - let l,tree = closegty::l, add_to_th closegty tree closegty in + let l,tree = cache.under_inspection in + let l,tree = closegty::l, add_to_th closegty tree closegty in {cache with under_inspection = l,tree} else cache in let failures = List.fold_left (fun allfailures ((_,t),status) -> debug_print ~depth - (lazy ("(re)considering goal " ^ - (string_of_int g) ^" : "^ppterm status gty)); + (lazy ("(re)considering goal " ^ + (string_of_int g) ^" : "^ppterm status gty)); debug_print (~depth:depth) (lazy ("Case: " ^ NotationPp.pp_term status t)); let depth,cache = - if t=Ast.Ident("__whd",None) || + if t=Ast.Ident("__whd",None) || t=Ast.Ident("__intros",None) then depth, cache - else depth+1,loop_cache in - let cache = add_to_trace status ~depth cache t in + else depth+1,loop_cache in + let cache = add_to_trace status ~depth cache t in let cache = {cache with failures = allfailures} in - try - auto_clusters flags signature cache depth status; + try + auto_clusters flags signature cache depth status ~use_given_only; assert false; - with Gaveup fail -> - debug_print ~depth (lazy "Failed"); - fail) - cache.failures alternatives in + with Gaveup fail -> + debug_print ~depth (lazy "Failed"); + fail) + cache.failures alternatives in let failures = if flags.last then let newfail = @@@ -1767,7 -1795,7 +1795,7 @@@ add_to_th newfail failures closegty else failures in debug_print ~depth (lazy "no more candidates"); - raise (Gaveup failures) + raise (Gaveup failures) ;; let int name l def = @@@ -1787,12 -1815,34 +1815,34 @@@ let cleanup_trace s trace (* filtering facts *) in List.filter (fun t -> - match t with - | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u) - | _ -> false) trace + match t with + | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u) + | _ -> false) trace ;; - let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = + (*CSC: TODO + + - auto_params e' una high tactic che prende in input i parametri e poi li + processa nel contesto vuoto calcolando i candidate + + - astrarla su una auto_params' che prende in input gia' i candidate e un + nuovo parametro per evitare il calcolo dei candidate locali che invece + diventano vuoti (ovvero: non usare automaticamente tutte le ipotesi, bensi' + nessuna) + + - reimplementi la auto_params chiamando la auto_params' con il flag a + false e il vecchio codice per andare da parametri a candiddati + OVVERO: usa tutti le ipotesi locali + candidati globali + + - crei un nuovo entry point lowtac che calcola i candidati usando il contesto + corrente e poi fa exec della auto_params' con i candidati e il flag a true + OVVERO: usa solo candidati globali che comprendono ipotesi locali + *) + + type auto_params = NTacStatus.tactic_term list option * (string * string) list + + (*let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =*) + let auto_tac' candidates ~local_candidates ?(use_given_only=false) flags ?(trace_ref=ref []) status = let oldstatus = status in let status = (status:> NTacStatus.tac_status) in let goals = head_goals status#stack in @@@ -1809,17 -1859,6 +1859,6 @@@ (NDiscriminationTree.TermSet.elements t)) ))); *) - let candidates = - match univ with - | None -> None - | Some l -> - let to_Ast t = - (* FG: `XTSort here? *) - let status, res = disambiguate status [] 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) - in let depth = int "depth" flags 3 in let size = int "size" flags 10 in let width = int "width" flags 4 (* (3+List.length goals)*) in @@@ -1829,6 -1868,7 +1868,7 @@@ let flags = { last = true; candidates = candidates; + local_candidates = local_candidates; maxwidth = width; maxsize = size; maxdepth = depth; @@@ -1847,7 -1887,7 +1887,7 @@@ let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in let flags = { flags with maxdepth = x } in - try auto_clusters (~top:true) flags signature cache 0 status;assert false + try auto_clusters (~top:true) flags signature cache 0 status ~use_given_only;assert false (* try auto_main flags signature cache 0 status;assert false *) @@@ -1855,12 -1895,12 +1895,12 @@@ | Gaveup _ -> up_to (x+1) y | Proved (s,trace) -> debug_print (lazy ("proved at depth " ^ string_of_int x)); - List.iter (toref incr_uses statistics) trace; + List.iter (toref incr_uses statistics) trace; let trace = cleanup_trace s trace in - let _ = debug_print (pptrace status trace) in + let _ = debug_print (pptrace status trace) in let stack = match s#stack with - | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest + | (g,t,k,f,p) :: rest -> (filter_open g,t,k,f,p):: rest | _ -> assert false in let s = s#set_stack stack in @@@ -1876,6 -1916,31 +1916,31 @@@ 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined 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 --combined matita/matita/applyTransformation.ml index 50d7d25bf,f761a153b..2ae27ee63 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@@ -66,7 -66,7 +66,7 @@@ let ntxt_of_cic_context ~metasenv ~subs Content2pres.ncontext2pres ((new NCicPp.status)#ppcontext ~metasenv ~subst) -let ntxt_of_cic_subst ~map_unicode_to_tex size status ~metasenv ?use_subst subst = +let ntxt_of_cic_subst ~map_unicode_to_tex:_ _size _status ~metasenv ?use_subst subst = [], "<<>>\n" ^ (new NCicPp.status)#ppsubst ~metasenv ?use_subst subst @@@ -75,11 -75,11 +75,11 @@@ class status object(self) inherit Interpretations.status inherit TermContentPres.status - method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t = + method ppterm ~context ~subst ~metasenv ?margin:(_) ?inside_fix:(_) t = snd (ntxt_of_cic_term ~map_unicode_to_tex:false 80 self ~metasenv ~subst ~context t) - method ppcontext ?sep ~subst ~metasenv context = + method ppcontext ?sep:(_) ~subst ~metasenv context = snd (ntxt_of_cic_context ~map_unicode_to_tex:false 80 self ~metasenv ~subst context) @@@ -96,3 -96,15 +96,15 @@@ method ppobj obj = snd (ntxt_of_cic_object ~map_unicode_to_tex:false 80 self obj) end + + let notation_pp_term status term = + let to_pres = Content2pres.nterm2pres ?prec:None in + let content = term in + let size = 80 in + let ids_to_nrefs = Hashtbl.create 1 in + let pres = to_pres status ~ids_to_nrefs content in + let pres = CicNotationPres.mpres_of_box pres in + BoxPp.render_to_string ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") + (function x::_ -> x | _ -> assert false) size pres + + let _ = NotationPp.set_pp_term (fun status y -> snd (notation_pp_term (Obj.magic status) y)) diff --combined matita/matita/matitaEngine.ml index 2963e71c4,cfd8c107a..fea7161c1 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@@ -1,14 -1,14 +1,14 @@@ (* Copyright (C) 2005, 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 @@@ -18,20 -18,22 +18,21 @@@ * 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://helm.cs.unibo.it/ - *) + *) (* $Id$ *) + module G = GrafiteAst -open GrafiteTypes open Printf class status baseuri = - object - inherit GrafiteTypes.status baseuri - inherit ApplyTransformation.status - end + object + inherit GrafiteTypes.status baseuri + inherit ApplyTransformation.status + end exception TryingToAdd of string Lazy.t exception EnrichedWithStatus of exn * status @@@ -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 = @@@ -61,7 -152,7 +151,7 @@@ raise (FailureCompiling (baseuri,exn)) ;; - let cut prefix s = + let cut prefix s = let lenp = String.length prefix in let lens = String.length s in assert (lens > lenp); @@@ -69,33 -160,33 +159,33 @@@ String.sub s lenp (lens-lenp) ;; - let print_string = - let indent = ref 0 in - let print_string ~right_justify s = - let ss = - match right_justify with - None -> "" - | Some (ss,len_ss) -> - let i = 80 - !indent - len_ss - String.length s in - if i > 0 then String.make i ' ' ^ ss else ss - in - assert (!indent >=0); - print_string (String.make !indent ' ' ^ s ^ ss) in - fun enter ?right_justify s -> - if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s) + let print_string = + let indent = ref 0 in + let print_string ~right_justify s = + let ss = + match right_justify with + None -> "" + | Some (ss,len_ss) -> + let i = 80 - !indent - len_ss - String.length s in + if i > 0 then String.make i ' ' ^ ss else ss + in + assert (!indent >=0); + print_string (String.make !indent ' ' ^ s ^ ss) in + fun enter ?right_justify s -> + if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s) ;; - let pp_times ss fname rc big_bang big_bang_u big_bang_s = + let pp_times ss fname rc big_bang big_bang_u big_bang_s = if not (Helm_registry.get_bool "matita.verbose") then let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in let r = Unix.gettimeofday () -. big_bang in let u = u -. big_bang_u in let s = s -. big_bang_s in let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in - let rc = + let rc = if rc then "OK" else "FAIL" in - let times = - let fmt t = + let times = + let fmt t = let seconds = int_of_float t in let cents = int_of_float ((t -. floor t) *. 100.0) in let minutes = seconds / 60 in @@@ -111,130 -202,130 +201,130 @@@ ;; let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = - let baseuri = status#baseuri in - let new_aliases,new_status = - GrafiteDisambiguate.eval_with_new_aliases status - (fun status -> - let time0 = Unix.gettimeofday () in - let status = - GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status - (text,prefix_len,ast) in - let time1 = Unix.gettimeofday () in - HLog.debug ("... grafite_engine done in " ^ string_of_float (time1 -. time0) ^ "s"); - status - ) in - let _,intermediate_states = - List.fold_left - (fun (status,acc) (k,value) -> - let v = GrafiteAst.description_of_alias value in - let b = - try - let NReference.Ref (uri,_) = NReference.reference_of_string v in - NUri.baseuri_of_uri uri = baseuri - with - NReference.IllFormedReference _ -> - false (* v is a description, not a URI *) - in - if b then - status,acc - else - let status = - GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false - GrafiteAst.WithPreferences [k,value] - in - status, (status ,Some (k,value))::acc - ) (status,[]) new_aliases (* WARNING: this must be the old status! *) - in + let baseuri = status#baseuri in + let new_aliases,new_status = + GrafiteDisambiguate.eval_with_new_aliases status + (fun status -> + let time0 = Unix.gettimeofday () in + let status = + GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status + (text,prefix_len,ast) in + let time1 = Unix.gettimeofday () in + HLog.debug ("... grafite_engine done in " ^ string_of_float (time1 -. time0) ^ "s"); + status + ) in + let _,intermediate_states = + List.fold_left + (fun (status,acc) (k,value) -> + let v = GrafiteAst.description_of_alias value in + let b = + try + let NReference.Ref (uri,_) = NReference.reference_of_string v in + NUri.baseuri_of_uri uri = baseuri + with + NReference.IllFormedReference _ -> + false (* v is a description, not a URI *) + in + if b then + status,acc + else + let status = + GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false + GrafiteAst.WithPreferences [k,value] + in + status, (status ,Some (k,value))::acc + ) (status,[]) new_aliases (* WARNING: this must be the old status! *) + in (new_status,None)::intermediate_states ;; let baseuri_of_script ~include_paths fname = - try Librarian.baseuri_of_script ~include_paths fname - with - Librarian.NoRootFor _ -> + try Librarian.baseuri_of_script ~include_paths fname + with + Librarian.NoRootFor _ -> HLog.error ("The included file '"^fname^"' has no root file,"); HLog.error "please create it."; raise (Failure ("No root file for "^fname)) - | Librarian.FileNotFound _ -> + | Librarian.FileNotFound _ -> raise (Failure ("File not found: "^fname)) ;; (* 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 = if List.mem fname compiling then raise (CircularDependency fname); let compiling = fname::compiling in let matita_debug = Helm_registry.get_bool "matita.debug" in - let root,baseuri,fname,_tgt = + let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in if Http_getter_storage.is_read_only baseuri then assert false; (* MATITA 1.0: debbo fare time_travel sulla ng_library? *) @@@ -245,154 -336,154 +335,154 @@@ let ocamldirname = Filename.dirname fname in let ocamlfname = Filename.chop_extension (Filename.basename fname) in let status,ocamlfname = - Common.modname_of_filename status false ocamlfname in + Common.modname_of_filename status false ocamlfname in let ocamlfname = ocamldirname ^ "/" ^ ocamlfname ^ ".ml" in let status = OcamlExtraction.open_file status ~baseuri ocamlfname in let big_bang = Unix.gettimeofday () in - let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = - Unix.times () + let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = + Unix.times () in let time = Unix.time () in - let cc = - let rex = Str.regexp ".*opt$" in - if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt" - else "matitac" in + let cc = + let rex = Str.regexp ".*opt$" in + if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt" + else "matitac" in let s = Printf.sprintf "%s %s" cc (cut (root^"/") fname) in try (* cleanup of previously compiled objects *) if (not (Http_getter_storage.is_empty ~local:true baseuri)) - then begin + then begin HLog.message ("baseuri " ^ baseuri ^ " is not empty"); HLog.message ("cleaning baseuri " ^ baseuri); LibraryClean.clean_baseuris [baseuri]; end; HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri); if not (Helm_registry.get_bool "matita.verbose") then - (print_string true (s ^ "\n"); flush stdout); + (print_string true (s ^ "\n"); flush stdout); (* we dalay this error check until we print 'matitac file ' *) assert (Http_getter_storage.is_empty ~local:true baseuri); (* create dir for XML files *) if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk" - ~default:false) + ~default:false) then - HExtlib.mkdir - (Filename.dirname - (Http_getter.filename ~local:true ~writable:true (baseuri ^ - "foo.con"))); + HExtlib.mkdir + (Filename.dirname + (Http_getter.filename ~local:true ~writable:true (baseuri ^ + "foo.con"))); let buf = - GrafiteParser.parsable_statement status - (Ulexing.from_utf8_channel (open_in fname)) + GrafiteParser.parsable_statement status + (Ulexing.from_utf8_channel (open_in fname)) in let print_cb = - if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ()) - else pp_ast_statement + if not (Helm_registry.get_bool "matita.verbose") then fun _ _ -> () + else pp_ast_statement ~fname in let asserted, status = - eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in + eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in let status = OcamlExtraction.close_file status in let elapsed = Unix.time () -. time in - (if Helm_registry.get_bool "matita.moo" then begin - GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - status - end; + (if Helm_registry.get_bool "matita.moo" then begin + GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) + status + end; let tm = Unix.gmtime elapsed in let sec = string_of_int tm.Unix.tm_sec ^ "''" in - let min = - if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min^"' ") else "" + let min = + if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min^"' ") else "" in - let hou = + let hou = if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour^"h ") else "" in - HLog.message + HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); pp_times s fname true big_bang big_bang_u big_bang_s; (*CSC: bad, one imperative bit is still there! to be moved into functional status *) NCicMetaSubst.pushmaxmeta (); - (* MATITA 1.0: debbo fare time_travel sulla ng_library? - LexiconSync.time_travel - ~present:lexicon_status ~past:initial_lexicon_status; - *) + (* MATITA 1.0: debbo fare time_travel sulla ng_library? + LexiconSync.time_travel + ~present:lexicon_status ~past:initial_lexicon_status; + *) asserted) - with + with (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *) | exn when not matita_debug -> - (* MATITA 1.0: debbo fare time_travel sulla ng_library? - LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status; - * *) - (*CSC: bad, one imperative bit is still there! - to be moved into functional status *) - NCicMetaSubst.pushmaxmeta (); - pp_times s fname false big_bang big_bang_u big_bang_s; - clean_exit baseuri exn + (* MATITA 1.0: debbo fare time_travel sulla ng_library? + LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status; + * *) + (*CSC: bad, one imperative bit is still there! + to be moved into functional status *) + NCicMetaSubst.pushmaxmeta (); + pp_times s fname false big_bang big_bang_u big_bang_s; + clean_exit baseuri exn and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath = - let root,baseuri,fullmapath,_ = - Librarian.baseuri_of_script ~include_paths mapath in - if List.mem fullmapath asserted then asserted,false - else - begin - let include_paths = - let includes = - try - Str.split (Str.regexp " ") - (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) - with Not_found -> [] - in - root::includes @ - Helm_registry.get_list Helm_registry.string "matita.includes" in - let baseuri = NUri.uri_of_string baseuri in - let ngtime_of baseuri = - let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in - try - Some (Unix.stat ngpath).Unix.st_mtime - with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in - let matime = - try (Unix.stat fullmapath).Unix.st_mtime - with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false - in - let ngtime = ngtime_of baseuri in - let asserted,to_be_compiled = - match ngtime with - Some ngtime -> - let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in - let asserted,children_bad = - List.fold_left - (fun (asserted,b) mapath -> - let asserted,b1 = - try - assert_ng ~already_included ~compiling ~asserted ~include_paths - mapath - with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> - asserted, true - in - asserted, b || b1 - || let _,baseuri,_,_ = - (*CSC: bug here? include_paths should be empty and - mapath should be absolute *) - Librarian.baseuri_of_script ~include_paths mapath in - let baseuri = NUri.uri_of_string baseuri in - (match ngtime_of baseuri with - Some child_ngtime -> child_ngtime > ngtime - | None -> assert false) - ) (asserted,false) preamble + let root,baseuri,fullmapath,_ = + Librarian.baseuri_of_script ~include_paths mapath in + if List.mem fullmapath asserted then asserted,false + else + begin + let include_paths = + let includes = + try + Str.split (Str.regexp " ") + (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) + with Not_found -> [] in - asserted, children_bad || matime > ngtime - | None -> asserted,true - in - if not to_be_compiled then fullmapath::asserted,false - else - if List.mem baseuri already_included then - (* maybe recompiling it I would get the same... *) - raise (AlreadyLoaded (lazy mapath)) - else - let asserted = compile ~compiling ~asserted ~include_paths fullmapath in - fullmapath::asserted,true - end + root::includes @ + Helm_registry.get_list Helm_registry.string "matita.includes" in + let baseuri = NUri.uri_of_string baseuri in + let ngtime_of baseuri = + let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in + try + Some (Unix.stat ngpath).Unix.st_mtime + with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in + let matime = + try (Unix.stat fullmapath).Unix.st_mtime + with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false + in + let ngtime = ngtime_of baseuri in + let asserted,to_be_compiled = + match ngtime with + Some ngtime -> + let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in + let asserted,children_bad = + List.fold_left + (fun (asserted,b) mapath -> + let asserted,b1 = + try + assert_ng ~already_included ~compiling ~asserted ~include_paths + mapath + with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> + asserted, true + in + asserted, b || b1 + || let _,baseuri,_,_ = + (*CSC: bug here? include_paths should be empty and + mapath should be absolute *) + Librarian.baseuri_of_script ~include_paths mapath in + let baseuri = NUri.uri_of_string baseuri in + (match ngtime_of baseuri with + Some child_ngtime -> child_ngtime > ngtime + | None -> assert false) + ) (asserted,false) preamble + in + asserted, children_bad || matime > ngtime + | None -> asserted,true + in + if not to_be_compiled then fullmapath::asserted,false + else + if List.mem baseuri already_included then + (* maybe recompiling it I would get the same... *) + raise (AlreadyLoaded (lazy mapath)) + else + let asserted = compile ~compiling ~asserted ~include_paths fullmapath in + fullmapath::asserted,true + end ;; let assert_ng ~include_paths mapath = - snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[] - mapath) + snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[] + mapath) let get_ast status ~include_paths strm = - snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm) + snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm) diff --combined matita/matita/matitaGui.ml index ad34b7a57,ce3dcc6fe..5b7352d74 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@@ -31,6 -31,8 +31,6 @@@ open MatitaGeneratedGu open MatitaGtkMisc open MatitaMisc -exception Found of int - let all_disambiguation_passes = ref false (* this is a shit and should be changed :-{ *) @@@ -39,7 -41,7 +39,7 @@@ let interactive_uri_choic ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO) ?copy_cb () - ~id uris + ~id:_ uris = if (selection_mode <> `SINGLE) && (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation") @@@ -95,8 -97,6 +95,8 @@@ | uris -> return (Some (List.map NReference.reference_of_string uris))); connect_button dialog#uriChoiceAbortButton (fun _ -> return None); dialog#uriChoiceDialog#show (); + (* CSC: old Gtk2 code. Use #run instead. Look for similar code handling + other dialogs *) GtkThread.main (); (match !choices with | None -> raise MatitaTypes.Cancel @@@ -178,7 -178,7 +178,7 @@@ class interpErrorModel (let loc_row = tree_store#append () in begin match lll with - [passes,envs_and_diffs,_,_] -> + [passes,_envs_and_diffs,_,_] -> tree_store#set ~row:loc_row ~column:id_col ("Error location " ^ string_of_int (!idx1+1) ^ ", error message " ^ string_of_int (!idx1+1) ^ ".1" ^ @@@ -255,7 -255,7 +255,7 @@@ exception UseLibrary;; let interactive_error_interp ~all_passes - (source_buffer:GSourceView2.source_buffer) notify_exn offset errorll filename + (source_buffer:GSourceView3.source_buffer) notify_exn offset errorll filename = (* hook to save a script for each disambiguation error *) if false then @@@ -318,12 -318,9 +318,12 @@@ (MultiPassDisambiguator.DisambiguationError (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]])); | _::_ -> + GtkThread.sync (fun _ -> let dialog = new disambiguationErrors () in - if all_passes then - dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false; + dialog#toplevel#add_button "Fix this interpretation" `OK; + dialog#toplevel#add_button "Close" `DELETE_EVENT; + if not all_passes then + dialog#toplevel#add_button "More errors" `HELP; (* HELP means MORE *) let model = new interpErrorModel dialog#treeview choices in dialog#disambiguationErrors#set_title "Disambiguation error"; dialog#disambiguationErrorsLabel#set_label @@@ -355,56 -352,64 +355,56 @@@ (MultiPassDisambiguator.DisambiguationError (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]])) )); - let return _ = - dialog#disambiguationErrors#destroy (); - GMain.Main.quit () + (match GtkThread.sync dialog#toplevel#run () with + | `OK -> + let tree_path = + match fst (dialog#treeview#get_cursor ()) with + None -> assert false + | Some tp -> tp in + let idx1,idx2,idx3 = model#get_interp_no tree_path in + let diff = + match idx2,idx3 with + Some idx2, Some idx3 -> + let _,lll = List.nth choices idx1 in + let _,envs_and_diffs,_,_ = List.nth lll idx2 in + let _,_,diff = List.nth envs_and_diffs idx3 in + diff + | _,_ -> assert false in - let fail _ = return () in - ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true)); - connect_button dialog#disambiguationErrorsOkButton - (fun _ -> - let tree_path = - match fst (dialog#treeview#get_cursor ()) with - None -> assert false - | Some tp -> tp in - let idx1,idx2,idx3 = model#get_interp_no tree_path in - let diff = - match idx2,idx3 with - Some idx2, Some idx3 -> - let _,lll = List.nth choices idx1 in - let _,envs_and_diffs,_,_ = List.nth lll idx2 in - let _,_,diff = List.nth envs_and_diffs idx3 in - diff - | _,_ -> assert false - in - let newtxt = - String.concat "\n" - ("" :: - List.map - (fun k,desc -> - let alias = - match k with - | DisambiguateTypes.Id id -> - GrafiteAst.Ident_alias (id, desc) - | DisambiguateTypes.Symbol (symb, i)-> - GrafiteAst.Symbol_alias (symb, i, desc) - | DisambiguateTypes.Num i -> - GrafiteAst.Number_alias (i, desc) - in - GrafiteAstPp.pp_alias alias) - diff) ^ "\n" - in - source_buffer#insert - ~iter: - (source_buffer#get_iter_at_mark - (`NAME "beginning_of_statement")) newtxt ; - return () - ); - connect_button dialog#disambiguationErrorsMoreErrors - (fun _ -> return () ; raise UseLibrary); - connect_button dialog#disambiguationErrorsCancelButton fail; - dialog#disambiguationErrors#show (); - GtkThread.main () - + let newtxt = + String.concat "\n" + ("" :: + List.map + (fun k,desc -> + let alias = + match k with + | DisambiguateTypes.Id id -> + GrafiteAst.Ident_alias (id, desc) + | DisambiguateTypes.Symbol (symb, i)-> + GrafiteAst.Symbol_alias (symb, i, desc) + | DisambiguateTypes.Num i -> + GrafiteAst.Number_alias (i, desc) + in + GrafiteAstPp.pp_alias alias) + diff) ^ "\n" + in + source_buffer#insert + ~iter: + (source_buffer#get_iter_at_mark + (`NAME "beginning_of_statement")) newtxt + | `HELP (* HELP MEANS MORE *) -> + dialog#toplevel#destroy () ; + raise UseLibrary + | `DELETE_EVENT -> () + | _ -> assert false) ; + dialog#toplevel#destroy () + ) () class gui () = (* creation order _is_ relevant for windows placement *) let main = new mainWin () in let sequents_viewer = MatitaMathView.sequentsViewer_instance main#sequentsNotebook in - let fileSel = new fileSelectionWin () in let findRepl = new findReplWin () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ main#mainWinEventBox ] @@@ -457,7 -462,6 +457,7 @@@ ~website:"http://matita.cs.unibo.it" () in + ignore(about_dialog#event#connect#delete (fun _ -> true)); ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ())); connect_menu_item main#contentsMenuItem (fun () -> if 0 = Sys.command "which gnome-help" then @@@ -513,10 -517,16 +513,10 @@@ ~callback:(fun _ -> hide_find_Repl ();true)); connect_menu_item main#undoMenuItem (fun () -> (MatitaScript.current ())#safe_undo); -(*CSC: XXX - ignore(source_view#source_buffer#connect#can_undo - ~callback:main#undoMenuItem#misc#set_sensitive); -*) main#undoMenuItem#misc#set_sensitive true; + main#undoMenuItem#misc#set_sensitive false; connect_menu_item main#redoMenuItem (fun () -> (MatitaScript.current ())#safe_redo); -(*CSC: XXX - ignore(source_view#source_buffer#connect#can_redo - ~callback:main#redoMenuItem#misc#set_sensitive); -*) main#redoMenuItem#misc#set_sensitive true; + main#redoMenuItem#misc#set_sensitive false; connect_menu_item main#editMenu (fun () -> main#copyMenuItem#misc#set_sensitive (MatitaScript.current ())#canCopy; @@@ -563,7 -573,7 +563,7 @@@ GtkThread.sync (fun () -> ()) () in let worker_thread = ref None in - let notify_exn (source_view : GSourceView2.source_view) exn = + let notify_exn (source_view : GSourceView3.source_view) exn = let floc, msg = MatitaExcPp.to_string exn in begin match floc with @@@ -601,11 -611,15 +601,15 @@@ let saved_use_library= !MultiPassDisambiguator.use_library in try MultiPassDisambiguator.use_library := !all_disambiguation_passes; + prerr_endline "PRIMA"; f script; MultiPassDisambiguator.use_library := saved_use_library; - unlock_world () + prerr_endline "DOPO"; + unlock_world () ; + prerr_endline "FINE"; with | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> + prerr_endline "EXC1"; (try interactive_error_interp ~all_passes:!all_disambiguation_passes source_view#source_buffer @@@ -622,7 -636,9 +626,9 @@@ notify_exn source_view exc); | exc -> notify_exn source_view exc); MultiPassDisambiguator.use_library := saved_use_library; - unlock_world () + prerr_endline "DOPO1"; + unlock_world (); + prerr_endline "FINE1" | exc -> (try notify_exn source_view exc with Sys.Break as e -> notify_exn source_view e); @@@ -656,6 -672,32 +662,6 @@@ with exc -> script#source_view#misc#grab_focus (); raise exc in - (* file selection win *) - ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true)); - ignore (fileSel#fileSelectionWin#connect#response (fun event -> - let return r = - chosen_file <- r; - fileSel#fileSelectionWin#misc#hide (); - GMain.Main.quit () - in - match event with - | `OK -> - let fname = fileSel#fileSelectionWin#filename in - if Sys.file_exists fname then - begin - if HExtlib.is_regular fname && not (_only_directory) then - return (Some fname) - else if _only_directory && HExtlib.is_dir fname then - return (Some fname) - end - else - begin - if _ok_not_exists then - return (Some fname) - end - | `CANCEL -> return None - | `HELP -> () - | `DELETE_EVENT -> return None)); (* menus *) List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ]; (* console *) @@@ -839,10 -881,6 +845,10 @@@ current_page <- page; let script = MatitaScript.at_page page in script#activate; + main#undoMenuItem#misc#set_sensitive + script#source_view#source_buffer#can_undo ; + main#redoMenuItem#misc#set_sensitive + script#source_view#source_buffer#can_redo ; main#saveMenuItem#misc#set_sensitive script#has_name)) method private externalEditor () = @@@ -929,7 -967,7 +935,7 @@@ save_moo script#status; true | `NO -> true - | `CANCEL -> false + | `DELETE_EVENT -> false else (save_moo script#status; true) @@@ -1009,10 -1047,11 +1015,10 @@@ console#message ("'"^file^"' loaded."); self#_enableSaveTo file - method private _enableSaveTo file = + method private _enableSaveTo _file = self#main#saveMenuItem#misc#set_sensitive true method private console = console - method private fileSel = fileSel method private findRepl = findRepl method main = main @@@ -1027,46 -1066,20 +1033,46 @@@ (fun _ -> callback ();true)); self#addKeyBinding GdkKeysyms._q callback + method private chooseFileOrDir ok_not_exists only_directory = + let fileSel = GWindow.file_chooser_dialog + ~action:`OPEN + ~title:"Select file" + ~modal:true + ~type_hint:`DIALOG + ~position:`CENTER + () in + fileSel#add_select_button_stock `OPEN `OK; + fileSel#add_button_stock `CANCEL `CANCEL; + ignore (fileSel#set_current_folder(Sys.getcwd ())) ; + let res = + let rec aux () = + match fileSel#run () with + | `OK -> + (match fileSel#filename with + None -> aux () + | Some fname -> + if Sys.file_exists fname then + begin + if HExtlib.is_regular fname && not (only_directory) then + Some fname + else if only_directory && HExtlib.is_dir fname then + Some fname + else + aux () + end + else if ok_not_exists then Some fname else aux ()) + | `CANCEL -> None + | `DELETE_EVENT -> None in + aux () in + fileSel#destroy () ; + res + method private chooseFile ?(ok_not_exists = false) () = - _ok_not_exists <- ok_not_exists; - _only_directory <- false; - fileSel#fileSelectionWin#show (); - GtkThread.main (); - chosen_file + self#chooseFileOrDir ok_not_exists false method private chooseDir ?(ok_not_exists = false) () = - _ok_not_exists <- ok_not_exists; - _only_directory <- true; - fileSel#fileSelectionWin#show (); - GtkThread.main (); (* we should check that this is a directory *) - chosen_file + self#chooseFileOrDir ok_not_exists true end @@@ -1131,9 -1144,8 +1137,9 @@@ class interpModel let interactive_string_choice - text prefix_len ?(title = "") ?(msg = "") () ~id locs uris + text prefix_len ?(title = "") ?msg:(_ = "") () ~id:_ locs uris = + GtkThread.sync (fun _ -> let dialog = new uriChoiceDialog () in dialog#uriEntryHBox#misc#hide (); dialog#uriChoiceSelectedButton#misc#hide (); @@@ -1142,7 -1154,7 +1148,7 @@@ dialog#uriChoiceTreeView#selection#set_mode (`SINGLE :> Gtk.Tags.selection_mode); let model = new stringListModel dialog#uriChoiceTreeView in - let choices = ref None in + let choices = ref [] in dialog#uriChoiceDialog#set_title title; let hack_len = MatitaGtkMisc.utf8_string_length text in let rec colorize acc_len = function @@@ -1177,19 -1189,22 +1183,19 @@@ in dialog#uriChoiceLabel#set_label txt; List.iter model#easy_append uris; - let return v = - choices := v; - dialog#uriChoiceDialog#destroy (); - GMain.Main.quit () - in - ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); connect_button dialog#uriChoiceForwardButton (fun _ -> match model#easy_selection () with | [] -> () - | uris -> return (Some uris)); - connect_button dialog#uriChoiceAbortButton (fun _ -> return None); + | uris -> choices := uris; dialog#toplevel#response `OK); + connect_button dialog#uriChoiceAbortButton (fun _ -> dialog#toplevel#response `DELETE_EVENT); dialog#uriChoiceDialog#show (); - GtkThread.main (); - (match !choices with - | None -> raise MatitaTypes.Cancel - | Some uris -> uris) + let res = + match dialog#toplevel#run () with + | `DELETE_EVENT -> dialog#toplevel#destroy() ; raise MatitaTypes.Cancel + | `OK -> !choices + | _ -> assert false in + dialog#toplevel#destroy () ; + res) () let interactive_interp_choice () text prefix_len choices = (*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*) @@@ -1256,8 -1271,10 +1262,8 @@@ let _ = (* disambiguator callbacks *) Disambiguate.set_choose_uris_callback - (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg -> + (fun ~selection_mode ?ok ?enable_button_for_non_vars:(_=false) ~title ~msg -> interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ()); Disambiguate.set_choose_interp_callback (interactive_interp_choice ()); (* gtk initialization *) - GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) - ignore (GMain.Main.init ()) - + GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file (* loads gtk rc *)