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=f00a612006ac05f49a42ab507a95d3298bc1457a Merge branch 'declarative' into matita-lablgtk3 --- diff --git a/matita/components/content/.depend b/matita/components/content/.depend index e1dff0f85..6b7755819 100644 --- a/matita/components/content/.depend +++ b/matita/components/content/.depend @@ -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 -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 : -notationUtil.cmo : notationPt.cmo notationUtil.cmi -notationUtil.cmx : notationPt.cmx notationUtil.cmi -notationUtil.cmi : notationPt.cmo +notationUtil.cmo : \ + notationPt.cmo \ + notationUtil.cmi +notationUtil.cmx : \ + notationPt.cmx \ + notationUtil.cmi +notationUtil.cmi : \ + notationPt.cmo diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt index 9c0b365c6..4ef84ec5d 100644 --- a/matita/components/content/.depend.opt +++ b/matita/components/content/.depend.opt @@ -1,9 +1,22 @@ -content.cmx : content.cmi +content.cmx : \ + content.cmi content.cmi : -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 +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 : -notationUtil.cmx : notationPt.cmx notationUtil.cmi -notationUtil.cmi : notationPt.cmx +notationUtil.cmx : \ + notationPt.cmx \ + notationUtil.cmi +notationUtil.cmi : \ + notationPt.cmx diff --git a/matita/components/content_pres/.depend b/matita/components/content_pres/.depend index c4875d55f..0f1c00964 100644 --- a/matita/components/content_pres/.depend +++ b/matita/components/content_pres/.depend @@ -1,38 +1,92 @@ -box.cmo : renderingAttrs.cmi box.cmi -box.cmx : renderingAttrs.cmx box.cmi +box.cmo : \ + renderingAttrs.cmi \ + box.cmi +box.cmx : \ + renderingAttrs.cmx \ + box.cmi box.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 +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.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 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 --git a/matita/components/content_pres/.depend.opt b/matita/components/content_pres/.depend.opt index 211b4fc51..1e74dfbf4 100644 --- a/matita/components/content_pres/.depend.opt +++ b/matita/components/content_pres/.depend.opt @@ -1,24 +1,55 @@ -box.cmx : renderingAttrs.cmx box.cmi +box.cmx : \ + renderingAttrs.cmx \ + box.cmi box.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 +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.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 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 --git a/matita/components/disambiguation/.depend b/matita/components/disambiguation/.depend index a25280569..2f1e0bd9e 100644 --- a/matita/components/disambiguation/.depend +++ b/matita/components/disambiguation/.depend @@ -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 : -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 --git a/matita/components/disambiguation/.depend.opt b/matita/components/disambiguation/.depend.opt index 1f1711ae7..867ae4666 100644 --- a/matita/components/disambiguation/.depend.opt +++ b/matita/components/disambiguation/.depend.opt @@ -1,7 +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 : -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 --git a/matita/components/extlib/.depend b/matita/components/extlib/.depend index 36dd894f0..c4c6d7e8a 100644 --- a/matita/components/extlib/.depend +++ b/matita/components/extlib/.depend @@ -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 +trie.cmo : \ + trie.cmi +trie.cmx : \ + trie.cmi trie.cmi : diff --git a/matita/components/extlib/.depend.opt b/matita/components/extlib/.depend.opt index 12de49274..72b64d1cf 100644 --- a/matita/components/extlib/.depend.opt +++ b/matita/components/extlib/.depend.opt @@ -1,18 +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 +trie.cmx : \ + trie.cmi trie.cmi : diff --git a/matita/components/getter/.depend b/matita/components/getter/.depend index 13ca8cc29..aa9063835 100644 --- a/matita/components/getter/.depend +++ b/matita/components/getter/.depend @@ -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.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_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_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_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 --git a/matita/components/getter/.depend.opt b/matita/components/getter/.depend.opt index 1d016d277..cb0f289ac 100644 --- a/matita/components/getter/.depend.opt +++ b/matita/components/getter/.depend.opt @@ -1,23 +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.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_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_types.cmx : -http_getter_wget.cmx : http_getter_types.cmx http_getter_wget.cmi +http_getter_wget.cmx : \ + http_getter_types.cmx \ + http_getter_wget.cmi http_getter_wget.cmi : diff --git a/matita/components/grafite/.depend b/matita/components/grafite/.depend index 211eff733..bf8b5d3f5 100644 --- a/matita/components/grafite/.depend +++ b/matita/components/grafite/.depend @@ -1,5 +1,10 @@ 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 --git a/matita/components/grafite/.depend.opt b/matita/components/grafite/.depend.opt index 5dabb8012..be6de9f62 100644 --- a/matita/components/grafite/.depend.opt +++ b/matita/components/grafite/.depend.opt @@ -1,3 +1,6 @@ grafiteAst.cmx : -grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi -grafiteAstPp.cmi : grafiteAst.cmx +grafiteAstPp.cmx : \ + grafiteAst.cmx \ + grafiteAstPp.cmi +grafiteAstPp.cmi : \ + grafiteAst.cmx diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 5d138bbe0..7750dab27 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -36,6 +36,8 @@ type npattern = type auto_params = nterm list option * (string*string) list +type just = [`Term of nterm | `Auto of auto_params] + type ntactic = | NApply of loc * nterm | NSmartApply of loc * nterm @@ -75,6 +77,29 @@ type ntactic = | NAssumption of loc | NRepeat of loc * ntactic | NBlock of loc * ntactic list + (* Declarative langauge *) + (* Not the best idea to use a string directly, an abstract type for identifiers would be better *) + | Assume of loc * string * nterm (* loc, identifier, type *) + | Suppose of loc * nterm * string (* loc, assumption, identifier *) + | By_just_we_proved of loc * just * nterm * string option (* loc, justification, conclusion, identifier *) + | We_need_to_prove of loc * nterm * string option (* loc, newconclusion, identifier *) + | BetaRewritingStep of loc * nterm + | Bydone of loc * just + | ExistsElim of loc * just * string * nterm * nterm * string + | AndElim of loc * just * nterm * string * nterm * string + | RewritingStep of + loc * nterm * [ `Term of nterm | `Auto of auto_params | `Proof | `SolveWith of nterm ] * bool (* last step*) + | Obtain of + loc * string * nterm + | Conclude of + loc * nterm + | Thesisbecomes of loc * nterm + | We_proceed_by_induction_on of loc * nterm * nterm + | We_proceed_by_cases_on of loc * nterm * nterm + | Byinduction of loc * nterm * string + | Case of loc * string * (string * nterm) list + (* This is a debug tactic to print the stack to stdout, can be safely removed *) + | PrintStack of loc type nmacro = | NCheck of loc * nterm diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 2e088bd77..42d7df864 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -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 @@ * 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 @@ 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,6 +51,22 @@ let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) = 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 @@ -70,13 +86,13 @@ let rec pp_ntactic status ~map_unicode_to_tex = | 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..." ^ " 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 ^ "...to be implemented..." ^ " " ^ "...to be implemented..." | NId _ -> "nid" @@ -97,16 +113,58 @@ let rec pp_ntactic status ~map_unicode_to_tex = | 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 @@ -128,7 +186,7 @@ let pp_alias = function 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" @@ -144,18 +202,18 @@ let pp_argument_pattern = function 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 +222,22 @@ let pp_notation status dir_opt l1_pattern assoc prec l2_pattern = (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 +250,14 @@ let pp_ncommand status = function | 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 +267,5 @@ let pp_comment status ~map_unicode_to_tex = let pp_statement status = function - | Executable (_, ex) -> pp_executable status ex + | Executable (_, ex) -> pp_executable status ex | Comment (_, c) -> pp_comment status c diff --git a/matita/components/grafite_engine/.depend b/matita/components/grafite_engine/.depend index 627227c70..bffffc1b8 100644 --- a/matita/components/grafite_engine/.depend +++ b/matita/components/grafite_engine/.depend @@ -1,11 +1,23 @@ -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 --git a/matita/components/grafite_engine/.depend.opt b/matita/components/grafite_engine/.depend.opt index 696b45881..6e9ccb21a 100644 --- a/matita/components/grafite_engine/.depend.opt +++ b/matita/components/grafite_engine/.depend.opt @@ -1,7 +1,14 @@ -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 --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index bd9e76ff2..71f036904 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -404,6 +404,17 @@ let eval_add_constraint status acyclic u1 u2 = ;; 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 @@ let eval_ng_tac tac = NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l) |GrafiteAst.NRepeat (_,tac) -> NTactics.repeat_tac (f f (text, prefix_len, tac)) + |GrafiteAst.Assume (_,id,t) -> Declarative.assume id (text,prefix_len,t) + |GrafiteAst.Suppose (_,t,id) -> Declarative.suppose (text,prefix_len,t) id + |GrafiteAst.By_just_we_proved (_,j,t1,s) -> Declarative.by_just_we_proved + (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s + |GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove (text,prefix_len,t) id + |GrafiteAst.BetaRewritingStep (_, t) -> Declarative.beta_rewriting_step (text,prefix_len,t) + | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len) + | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) -> + Declarative.existselim (just_to_tacstatus_just just text prefix_len) id1 (text,prefix_len,t1) + (text,prefix_len,t2) id2 + | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just + text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2 + | GrafiteAst.Thesisbecomes (_, t1) -> Declarative.thesisbecomes (text,prefix_len,t1) + | GrafiteAst.RewritingStep (_,rhs,just,cont) -> + Declarative.rewritingstep (text,prefix_len,rhs) + (match just with + `Term _ + | `Auto _ -> just_to_tacstatus_just just text prefix_len + |`Proof -> `Proof + |`SolveWith t -> `SolveWith (text,prefix_len,t) + ) + cont + | GrafiteAst.Obtain (_,id,t1) -> + Declarative.obtain id (text,prefix_len,t1) + | GrafiteAst.Conclude (_,t1) -> + Declarative.conclude (text,prefix_len,t1) + | GrafiteAst.We_proceed_by_cases_on (_, t, t1) -> + Declarative.we_proceed_by_cases_on (text,prefix_len,t) (text,prefix_len,t1) + | GrafiteAst.We_proceed_by_induction_on (_, t, t1) -> + Declarative.we_proceed_by_induction_on (text,prefix_len,t) (text,prefix_len,t1) + | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction (text,prefix_len,t) id + | GrafiteAst.Case (_,id,params) -> Declarative.case id params + | GrafiteAst.PrintStack (_) -> Declarative.print_stack in aux aux tac (* trick for non uniform recursion call *) ;; diff --git a/matita/components/grafite_parser/.depend b/matita/components/grafite_parser/.depend index fcb901973..13f0fb882 100644 --- a/matita/components/grafite_parser/.depend +++ b/matita/components/grafite_parser/.depend @@ -1,6 +1,11 @@ -grafiteParser.cmo : grafiteParser.cmi -grafiteParser.cmx : grafiteParser.cmi +grafiteParser.cmo : \ + grafiteParser.cmi +grafiteParser.cmx : \ + grafiteParser.cmi 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 --git a/matita/components/grafite_parser/.depend.opt b/matita/components/grafite_parser/.depend.opt index e0e6dac9c..4b014236d 100644 --- a/matita/components/grafite_parser/.depend.opt +++ b/matita/components/grafite_parser/.depend.opt @@ -1,4 +1,7 @@ -grafiteParser.cmx : grafiteParser.cmi +grafiteParser.cmx : \ + grafiteParser.cmi grafiteParser.cmi : -print_grammar.cmx : print_grammar.cmi -print_grammar.cmi : grafiteParser.cmi +print_grammar.cmx : \ + print_grammar.cmi +print_grammar.cmi : \ + grafiteParser.cmi diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index be39556d8..b1e3cc733 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -81,8 +81,8 @@ let nnon_punct_of_punct = function type by_continuation = BYC_done - | BYC_weproved of N.term * string option * N.term option - | BYC_letsuchthat of string * N.term * string * N.term + | BYC_weproved of N.term * string option + | BYC_letsuchthat of string * N.term * N.term * string | BYC_wehaveand of string * N.term * string * N.term let mk_parser statement lstatus = @@ -239,6 +239,112 @@ EXTEND | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")]) | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")]) | SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)]) + | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)]) + | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN -> G.NTactic (loc,[G.Suppose (loc,t,id)]) + | "let"; name = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> + G.NTactic(loc,[G.NLetIn (loc,(None,[],Some N.UserInput),t,name)]) + | just = + [ IDENT "using"; t=tactic_term -> `Term t + | params = auto_params -> + let just,params = params in + `Auto + (match just with + | None -> (None,params) + | Some (`Univ univ) -> (Some univ,params) + (* `Trace behaves exaclty like None for the moment being *) + | Some (`Trace) -> (None,params) + ) + ]; + cont=by_continuation -> G.NTactic (loc,[ + (match cont with + BYC_done -> G.Bydone (loc, just) + | BYC_weproved (ty,id) -> + G.By_just_we_proved(loc, just, ty, id) + | BYC_letsuchthat (id1,t1,t2,id2) -> + G.ExistsElim (loc, just, id1, t1, t2, id2) + | BYC_wehaveand (id1,t1,id2,t2) -> + G.AndElim (loc, just, t1, id1, t2, id2)) + ]) + | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] -> + G.NTactic (loc,[G.We_need_to_prove (loc, t, id)]) + | IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t = tactic_term -> G.NTactic(loc,[G.BetaRewritingStep (loc,t)]) + | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term -> G.NTactic (loc,[G.Thesisbecomes(loc,t1)]) + | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> + G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)]) + | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> + G.NTactic (loc,[G.We_proceed_by_induction_on (loc, t, t1)]) + | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN -> + G.NTactic (loc,[G.Byinduction(loc, t, id)]) + | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; + SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> + G.NTactic (loc,[G.Case(loc,id,params)]) + | IDENT "print_stack" -> G.NTactic (loc,[G.PrintStack loc]) + (* DO NOT FACTORIZE with the two following, camlp5 sucks*) +(* + | IDENT "conclude"; + termine = tactic_term; + SYMBOL "=" ; + t1=tactic_term ; + t2 = + [ IDENT "using"; t=tactic_term -> `Term t + | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term + | IDENT "proof" -> `Proof + | params = auto_params -> `Auto + ( + let just,params = params in + match just with + | None -> (None,params) + | Some (`Univ univ) -> (Some univ,params) + (* `Trace behaves exaclty like None for the moment being *) + | Some (`Trace) -> (None,params) + ) + ]; + cont = rewriting_step_continuation -> + G.NTactic (loc,[G.RewritingStep(loc, Some (None,termine), t1, t2, cont)]) + | IDENT "obtain" ; name = IDENT; + termine = tactic_term; + SYMBOL "=" ; + t1=tactic_term ; + t2 = + [ IDENT "using"; t=tactic_term -> `Term t + | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term + | IDENT "proof" -> `Proof + | params = auto_params -> `Auto + ( + let just,params = params in + match just with + | None -> (None,params) + | Some (`Univ univ) -> (Some univ,params) + (* `Trace behaves exaclty like None for the moment being *) + | Some (`Trace) -> (None,params) + ) + ]; + cont = rewriting_step_continuation -> + G.NTactic(loc,[G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)]) +*) + | IDENT "obtain" ; name = IDENT; + termine = tactic_term -> + G.NTactic(loc,[G.Obtain(loc, name, termine)]) + | IDENT "conclude" ; termine = tactic_term -> + G.NTactic(loc,[G.Conclude(loc, termine)]) + | SYMBOL "=" ; + t1=tactic_term ; + t2 = + [ IDENT "using"; t=tactic_term -> `Term t + | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term + | IDENT "proof" -> `Proof + | params = auto_params -> `Auto + ( + let just,params = params in + match just with + | None -> (None,params) + | Some (`Univ univ) -> (Some univ,params) + (* `Trace behaves exaclty like None for the moment being *) + | Some (`Trace) -> (None,params) + ) + ]; + cont = rewriting_step_continuation -> + G.NTactic(loc,[G.RewritingStep(loc, t1, t2, cont)]) ] ]; auto_fixed_param: [ @@ -263,27 +369,23 @@ EXTEND ] ]; -(* MATITA 1.0 by_continuation: [ - [ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1) - | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ; - "done" -> BYC_weproved (ty,None,t1) + [ WEPROVED; ty = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id] -> BYC_weproved (ty,id) | "done" -> BYC_done | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ; IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; - id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2) + id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,t2,id2) | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN -> BYC_wehaveand (id1,t1,id2,t2) ] ]; -*) -(* MATITA 1.0 + rewriting_step_continuation : [ [ "done" -> true | -> false ] ]; -*) + (* MATITA 1.0 atomic_tactical: [ "sequence" LEFTA diff --git a/matita/components/library/.depend b/matita/components/library/.depend index 7af1a906e..2cf0d4213 100644 --- a/matita/components/library/.depend +++ b/matita/components/library/.depend @@ -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 +libraryClean.cmo : \ + libraryClean.cmi +libraryClean.cmx : \ + libraryClean.cmi libraryClean.cmi : -libraryMisc.cmo : libraryMisc.cmi -libraryMisc.cmx : libraryMisc.cmi +libraryMisc.cmo : \ + libraryMisc.cmi +libraryMisc.cmx : \ + libraryMisc.cmi libraryMisc.cmi : diff --git a/matita/components/library/.depend.opt b/matita/components/library/.depend.opt index 27ecf9383..d960dc9be 100644 --- a/matita/components/library/.depend.opt +++ b/matita/components/library/.depend.opt @@ -1,6 +1,9 @@ -librarian.cmx : librarian.cmi +librarian.cmx : \ + librarian.cmi librarian.cmi : -libraryClean.cmx : libraryClean.cmi +libraryClean.cmx : \ + libraryClean.cmi libraryClean.cmi : -libraryMisc.cmx : libraryMisc.cmi +libraryMisc.cmx : \ + libraryMisc.cmi libraryMisc.cmi : diff --git a/matita/components/logger/.depend b/matita/components/logger/.depend index a22bd16f1..26c231a99 100644 --- a/matita/components/logger/.depend +++ b/matita/components/logger/.depend @@ -1,3 +1,5 @@ -helmLogger.cmo : helmLogger.cmi -helmLogger.cmx : helmLogger.cmi +helmLogger.cmo : \ + helmLogger.cmi +helmLogger.cmx : \ + helmLogger.cmi helmLogger.cmi : diff --git a/matita/components/logger/.depend.opt b/matita/components/logger/.depend.opt index ed934897f..f68fdd43e 100644 --- a/matita/components/logger/.depend.opt +++ b/matita/components/logger/.depend.opt @@ -1,2 +1,3 @@ -helmLogger.cmx : helmLogger.cmi +helmLogger.cmx : \ + helmLogger.cmi helmLogger.cmi : diff --git a/matita/components/ng_cic_content/.depend b/matita/components/ng_cic_content/.depend index 579a21e33..d870b57dc 100644 --- a/matita/components/ng_cic_content/.depend +++ b/matita/components/ng_cic_content/.depend @@ -1,6 +1,12 @@ -interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi -interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi +interpretations.cmo : \ + ncic2astMatcher.cmi \ + interpretations.cmi +interpretations.cmx : \ + ncic2astMatcher.cmx \ + interpretations.cmi interpretations.cmi : -ncic2astMatcher.cmo : ncic2astMatcher.cmi -ncic2astMatcher.cmx : ncic2astMatcher.cmi +ncic2astMatcher.cmo : \ + ncic2astMatcher.cmi +ncic2astMatcher.cmx : \ + ncic2astMatcher.cmi ncic2astMatcher.cmi : diff --git a/matita/components/ng_cic_content/.depend.opt b/matita/components/ng_cic_content/.depend.opt index df8d6d635..b526a0df5 100644 --- a/matita/components/ng_cic_content/.depend.opt +++ b/matita/components/ng_cic_content/.depend.opt @@ -1,4 +1,7 @@ -interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi +interpretations.cmx : \ + ncic2astMatcher.cmx \ + interpretations.cmi interpretations.cmi : -ncic2astMatcher.cmx : ncic2astMatcher.cmi +ncic2astMatcher.cmx : \ + ncic2astMatcher.cmi ncic2astMatcher.cmi : diff --git a/matita/components/ng_disambiguation/.depend b/matita/components/ng_disambiguation/.depend index fa8349c58..7462feedb 100644 --- a/matita/components/ng_disambiguation/.depend +++ b/matita/components/ng_disambiguation/.depend @@ -1,14 +1,26 @@ -disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi -disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi +disambiguateChoices.cmo : \ + nnumber_notation.cmi \ + disambiguateChoices.cmi +disambiguateChoices.cmx : \ + nnumber_notation.cmx \ + disambiguateChoices.cmi disambiguateChoices.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 --git a/matita/components/ng_disambiguation/.depend.opt b/matita/components/ng_disambiguation/.depend.opt index d5eef6bc0..6904cfd3b 100644 --- a/matita/components/ng_disambiguation/.depend.opt +++ b/matita/components/ng_disambiguation/.depend.opt @@ -1,9 +1,15 @@ -disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi +disambiguateChoices.cmx : \ + nnumber_notation.cmx \ + disambiguateChoices.cmi disambiguateChoices.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 --git a/matita/components/ng_extraction/.depend b/matita/components/ng_extraction/.depend index 144c13d55..d5062ccd7 100644 --- a/matita/components/ng_extraction/.depend +++ b/matita/components/ng_extraction/.depend @@ -1,32 +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 -coq.cmo : coq.cmi -coq.cmx : coq.cmi +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 +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 --git a/matita/components/ng_extraction/.depend.opt b/matita/components/ng_extraction/.depend.opt index 3b0b9b57c..a527ad0c4 100644 --- a/matita/components/ng_extraction/.depend.opt +++ b/matita/components/ng_extraction/.depend.opt @@ -1,20 +1,61 @@ -common.cmx : ocamlExtractionTable.cmx mlutil.cmx coq.cmx common.cmi -common.cmi : ocamlExtractionTable.cmi coq.cmi -coq.cmx : coq.cmi +common.cmx : \ + ocamlExtractionTable.cmx \ + mlutil.cmx \ + coq.cmx \ + common.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 --git a/matita/components/ng_extraction/mlutil.ml b/matita/components/ng_extraction/mlutil.ml index 01a0cd85d..9f553762a 100644 --- a/matita/components/ng_extraction/mlutil.ml +++ b/matita/components/ng_extraction/mlutil.ml @@ -1242,7 +1242,7 @@ and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l*) 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 (-) cand c) [] v (* [merge] may duplicates some indices, but I don't mind. *) | MLmagic t -> non_stricts add cand t diff --git a/matita/components/ng_kernel/.depend b/matita/components/ng_kernel/.depend index ca1b782f6..aa395ccc3 100644 --- a/matita/components/ng_kernel/.depend +++ b/matita/components/ng_kernel/.depend @@ -1,39 +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 -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 \ +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 : \ + 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 -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 +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 --git a/matita/components/ng_kernel/.depend.opt b/matita/components/ng_kernel/.depend.opt index 97f4e283a..fe01e3cc1 100644 --- a/matita/components/ng_kernel/.depend.opt +++ b/matita/components/ng_kernel/.depend.opt @@ -1,24 +1,74 @@ -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 -nCicSubstitution.cmi : nCic.cmx -nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \ - nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.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 +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 -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 +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 --git a/matita/components/ng_library/.depend b/matita/components/ng_library/.depend index d10bc6762..72fc77177 100644 --- a/matita/components/ng_library/.depend +++ b/matita/components/ng_library/.depend @@ -1,3 +1,5 @@ -nCicLibrary.cmo : nCicLibrary.cmi -nCicLibrary.cmx : nCicLibrary.cmi +nCicLibrary.cmo : \ + nCicLibrary.cmi +nCicLibrary.cmx : \ + nCicLibrary.cmi nCicLibrary.cmi : diff --git a/matita/components/ng_library/.depend.opt b/matita/components/ng_library/.depend.opt index 07d53f5dd..ee5e8bd16 100644 --- a/matita/components/ng_library/.depend.opt +++ b/matita/components/ng_library/.depend.opt @@ -1,2 +1,3 @@ -nCicLibrary.cmx : nCicLibrary.cmi +nCicLibrary.cmx : \ + nCicLibrary.cmi nCicLibrary.cmi : diff --git a/matita/components/ng_paramodulation/.depend b/matita/components/ng_paramodulation/.depend index be0690e45..b9c453ab4 100644 --- a/matita/components/ng_paramodulation/.depend +++ b/matita/components/ng_paramodulation/.depend @@ -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 : diff --git a/matita/components/ng_paramodulation/.depend.opt b/matita/components/ng_paramodulation/.depend.opt index 9593d8958..32cbf605d 100644 --- a/matita/components/ng_paramodulation/.depend.opt +++ b/matita/components/ng_paramodulation/.depend.opt @@ -1,29 +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 : diff --git a/matita/components/ng_refiner/.depend b/matita/components/ng_refiner/.depend index 2bd075dfc..6d211ffe5 100644 --- a/matita/components/ng_refiner/.depend +++ b/matita/components/ng_refiner/.depend @@ -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 +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 +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 -nCicRefiner.cmi : nCicCoercion.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 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 --git a/matita/components/ng_refiner/.depend.opt b/matita/components/ng_refiner/.depend.opt index dab873890..a25cbdb11 100644 --- a/matita/components/ng_refiner/.depend.opt +++ b/matita/components/ng_refiner/.depend.opt @@ -1,17 +1,36 @@ -nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \ - nCicMetaSubst.cmx nCicCoercion.cmi -nCicCoercion.cmi : nCicUnifHint.cmi -nCicMetaSubst.cmx : nCicMetaSubst.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 +nCicRefineUtil.cmx : \ + nCicMetaSubst.cmx \ + nCicRefineUtil.cmi nCicRefineUtil.cmi : -nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicRefiner.cmi -nCicRefiner.cmi : nCicCoercion.cmi -nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \ +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.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 --git a/matita/components/ng_tactics/.depend b/matita/components/ng_tactics/.depend index 90de5733d..4d386aaa4 100644 --- a/matita/components/ng_tactics/.depend +++ b/matita/components/ng_tactics/.depend @@ -1,30 +1,94 @@ -continuationals.cmo : continuationals.cmi -continuationals.cmx : continuationals.cmi +continuationals.cmo : \ + continuationals.cmi +continuationals.cmx : \ + continuationals.cmi continuationals.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 --git a/matita/components/ng_tactics/.depend.opt b/matita/components/ng_tactics/.depend.opt index c8999df5a..ca420895d 100644 --- a/matita/components/ng_tactics/.depend.opt +++ b/matita/components/ng_tactics/.depend.opt @@ -1,19 +1,55 @@ -continuationals.cmx : continuationals.cmi +continuationals.cmx : \ + continuationals.cmi continuationals.cmi : -nCicElim.cmx : nCicElim.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 : -nCicTacReduction.cmx : nCicTacReduction.cmi +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.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 --git a/matita/components/ng_tactics/Makefile b/matita/components/ng_tactics/Makefile index 3a261d192..b7a98406f 100644 --- a/matita/components/ng_tactics/Makefile +++ b/matita/components/ng_tactics/Makefile @@ -7,6 +7,7 @@ INTERFACE_FILES = \ nCicElim.mli \ nTactics.mli \ nnAuto.mli \ + declarative.mli \ nDestructTac.mli \ nInversion.mli diff --git a/matita/components/ng_tactics/continuationals.ml b/matita/components/ng_tactics/continuationals.ml index b10877130..dc54c89dd 100644 --- a/matita/components/ng_tactics/continuationals.ml +++ b/matita/components/ng_tactics/continuationals.ml @@ -35,21 +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 -> 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 @@ struct 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 @@ struct 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 @@ struct 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 @@ struct 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 @@ struct 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 @@ struct 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 --git a/matita/components/ng_tactics/continuationals.mli b/matita/components/ng_tactics/continuationals.mli index 1dcf4aa7d..d3fdf716c 100644 --- a/matita/components/ng_tactics/continuationals.mli +++ b/matita/components/ng_tactics/continuationals.mli @@ -29,12 +29,15 @@ type goal = int (** {2 Goal stack} *) +(* Key value pairs *) +type parameters = (string * string) list + module Stack: sig 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 val empty: t diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml new file mode 100644 index 000000000..d96e66811 --- /dev/null +++ b/matita/components/ng_tactics/declarative.ml @@ -0,0 +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 -> + let goals = filter_open g1 in + match goals with + [] -> fail (lazy "No goals under focus") + | 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 + 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' -> + 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 + | 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 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 + 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 _ -> "" +;; + +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 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) +;; + +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) = 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 -> + 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 + | _ -> 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 --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli new file mode 100644 index 000000000..f6863be27 --- /dev/null +++ b/matita/components/ng_tactics/declarative.mli @@ -0,0 +1,48 @@ +(* 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/. + *) + +type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ] + +val assume : string -> NTacStatus.tactic_term -> 's NTacStatus.tactic +val suppose : NTacStatus.tactic_term -> string -> 's NTacStatus.tactic +val we_need_to_prove : NTacStatus.tactic_term -> string option -> 's NTacStatus.tactic +val beta_rewriting_step : NTacStatus.tactic_term -> 's NTacStatus.tactic +val bydone : just -> 's NTacStatus.tactic +val by_just_we_proved : just -> NTacStatus.tactic_term -> string option -> 's NTacStatus.tactic +val andelim : just -> NTacStatus.tactic_term -> string -> NTacStatus.tactic_term -> string -> 's +NTacStatus.tactic +val existselim : just -> string -> NTacStatus.tactic_term -> NTacStatus.tactic_term -> string -> 's +NTacStatus.tactic +val thesisbecomes : NTacStatus.tactic_term -> 's NTacStatus.tactic +val rewritingstep : NTacStatus.tactic_term -> [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params + | `Proof | `SolveWith of NTacStatus.tactic_term ] -> + bool (* last step *) -> 's NTacStatus.tactic +val we_proceed_by_cases_on: NTacStatus.tactic_term -> NTacStatus.tactic_term -> 's NTacStatus.tactic +val we_proceed_by_induction_on: NTacStatus.tactic_term -> NTacStatus.tactic_term -> 's NTacStatus.tactic +val byinduction: NTacStatus.tactic_term -> string -> 's NTacStatus.tactic +val case: string -> (string*NotationPt.term) list -> 's NTacStatus.tactic +val obtain: string -> NTacStatus.tactic_term -> 's NTacStatus.tactic +val conclude: NTacStatus.tactic_term -> 's NTacStatus.tactic +val print_stack : 's NTacStatus.tactic diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index fc525c84a..118261af0 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -232,6 +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 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 @@ -460,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 --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli index da50ea2ac..e47700484 100644 --- a/matita/components/ng_tactics/nTacStatus.mli +++ b/matita/components/ng_tactics/nTacStatus.mli @@ -75,7 +75,7 @@ val disambiguate: val analyse_indty: #pstatus as 'status -> cic_term -> - 'status * (NReference.reference * int * NCic.term list * NCic.term list) + 'status * (NReference.reference * int * NCic.term list * NCic.term list * NCic.constructor list) val ppterm: #pstatus -> cic_term -> string val ppcontext: #pstatus -> NCic.context -> string @@ -85,6 +85,8 @@ val whd: val normalize: #pstatus as 'status -> ?delta:int -> NCic.context -> cic_term -> 'status * cic_term +val are_convertible: + #pstatus as 'status -> NCic.context -> cic_term -> cic_term -> 'status * bool val typeof: #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term val unify: diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 1aba2be9d..721d9165b 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -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 @@ 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 @@ let branch_tac ?(force=false) status = 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 @@ 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 @@ 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 @@ let case_tac lab status = 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ let change_stack_type (status : 'a #NTacStatus.status) (stack: 'b) : 'b NTacStat ;; 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 @@ let exec tac (low_status : #lowtac_status) g = 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 @@ let distribute_tac tac (status : #tac_status) = 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 ;; @@ -492,6 +492,7 @@ type indtyinfo = { leftno: int; consno: int; reference: NReference.reference; + cl: NCic.constructor list; } ;; @@ -502,11 +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 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 @@ let sort_of_goal_tac sortref = distribute_tac (fun status goal -> 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 @@ 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 @@ 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 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> let assert_tac seqs status = match status#stack with | [] -> assert false - | (g,_,_,_) :: _s -> + | (g,_,_,_,_) :: _s -> assert (List.length g = List.length seqs); (match seqs with [] -> id_tac diff --git a/matita/components/ng_tactics/nTactics.mli b/matita/components/ng_tactics/nTactics.mli index 5290a322e..6fb14f7b8 100644 --- a/matita/components/ng_tactics/nTactics.mli +++ b/matita/components/ng_tactics/nTactics.mli @@ -13,6 +13,7 @@ val print_tac: bool -> string -> 's NTacStatus.tactic +val id_tac: 's NTacStatus.tactic val dot_tac: 's NTacStatus.tactic val branch_tac: ?force:bool -> 's NTacStatus.tactic val shift_tac: 's NTacStatus.tactic @@ -75,7 +76,14 @@ val atomic_tac : NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.tactic (*(NTacStatus.tac_status -> 'c #NTacStatus.status) -> (#NTacStatus.tac_status as 'f) -> 'f*) -type indtyinfo +(* type indtyinfo *) +type indtyinfo = { + rightno: int; + leftno: int; + consno: int; + reference: NReference.reference; + cl: NCic.constructor list; + } val ref_of_indtyinfo : indtyinfo -> NReference.reference @@ -89,3 +97,7 @@ val find_in_context : 'a -> ('a * 'b) list -> int val inversion_tac: what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic + +val exact_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic +val first_tac: 's NTacStatus.tactic list -> 's NTacStatus.tactic +val sort_of_goal_tac: NCic.term ref -> 's NTacStatus.tactic diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 0f11cab74..3ac6040dc 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -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 *) | _ -> () @@ -82,7 +82,7 @@ let print_stat _status tbl = "; 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 @@ 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 @@ let solve f status eq_cache goal = 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 @@ 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 @@ let index_local_equations eq_cache status = | 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 = noprint (lazy "indexing equations"); let eq_cache,lemmas = match lemmas with @@ -575,13 +579,13 @@ let saturate_to_ref status metasenv subst ctx nref ty = 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 [] @@ -598,9 +602,9 @@ let smart_apply t unit_eq status g = 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 @@ -892,6 +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 @@ 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 *) @@ -982,7 +987,7 @@ let sort_candidates status ctx candidates = 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 @@ let sort_candidates status ctx candidates = 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,12 +1005,12 @@ 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 @@ -1045,7 +1050,7 @@ let try_candidate ?(smart=0) _flags depth status eq_cache _ctx t = (* 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)) @@ -1065,14 +1070,14 @@ let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ") 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 @@ let get_cands retrieve_for diff empty gty weak_gty = 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 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 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 @@ let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gt 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 @@ let applicative_case ~pfailed depth signature status flags gty cache = 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 *) @@ -1294,7 +1323,7 @@ let is_subsumed depth filter_depth status gty cache = 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 = @@ -1358,11 +1387,11 @@ let rec intros_facts ~depth status facts = | _ -> 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 @@ let intros ~depth status cache = [(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 @@ 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 @@ let do_something signature flags status g depth gty cache = 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 @@ 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 @@ let sort_tac status = 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 @@ 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 @@ 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 @@ let deep_focus_tac level focus status = 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 = 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 @@ let rec auto_clusters ?(top=false) 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 @@ let rec auto_clusters ?(top=false) (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 @@ let rec auto_clusters ?(top=false) 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,18 +1673,18 @@ let rec auto_clusters ?(top=false) (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 ?(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 @@ -1671,7 +1699,7 @@ auto_main flags signature cache depth status: unit = | 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 @@ -1683,17 +1711,17 @@ auto_main flags signature cache depth status: unit = | 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 @@ auto_main flags signature cache depth status: unit = (* 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 @@ auto_main flags signature cache depth status: unit = (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 @@ auto_main flags signature cache depth status: unit = 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 @@ 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 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = (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 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = let flags = { last = true; candidates = candidates; + local_candidates = local_candidates; maxwidth = width; maxsize = size; maxdepth = depth; @@ -1847,7 +1887,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = 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 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = | 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 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = 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) 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 --git a/matita/components/ng_tactics/nnAuto.mli b/matita/components/ng_tactics/nnAuto.mli index 87b2e8e4b..d77d32085 100644 --- a/matita/components/ng_tactics/nnAuto.mli +++ b/matita/components/ng_tactics/nnAuto.mli @@ -9,29 +9,27 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +type auto_params = NTacStatus.tactic_term list option * (string * string) list + val is_a_fact_obj: #NTacStatus.pstatus -> NUri.uri -> bool -val fast_eq_check_tac: - params:(NTacStatus.tactic_term list option * (string * string) list) -> - 's NTacStatus.tactic +val fast_eq_check_tac: params:auto_params -> 's NTacStatus.tactic -val paramod_tac: - params:(NTacStatus.tactic_term list option * (string * string) list) -> - 's NTacStatus.tactic +val paramod_tac: params:auto_params -> 's NTacStatus.tactic -val demod_tac: - params:(NTacStatus.tactic_term list option* (string * string) list) -> - 's NTacStatus.tactic +val demod_tac: params:auto_params -> 's NTacStatus.tactic val smart_apply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic val auto_tac: - params:(NTacStatus.tactic_term list option * (string * string) list) -> + params:auto_params -> ?trace_ref:NotationPt.term list ref -> 's NTacStatus.tactic +val auto_lowtac: params:auto_params -> #NTacStatus.pstatus -> int -> 's NTacStatus.tactic + val keys_of_type: (#NTacStatus.pstatus as 'a) -> NTacStatus.cic_term -> 'a * NTacStatus.cic_term list diff --git a/matita/components/registry/.depend b/matita/components/registry/.depend index 2a8e36776..edb72af84 100644 --- a/matita/components/registry/.depend +++ b/matita/components/registry/.depend @@ -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 : diff --git a/matita/components/registry/.depend.opt b/matita/components/registry/.depend.opt index f28210446..c8aaec531 100644 --- a/matita/components/registry/.depend.opt +++ b/matita/components/registry/.depend.opt @@ -1,2 +1,3 @@ -helm_registry.cmx : helm_registry.cmi +helm_registry.cmx : \ + helm_registry.cmi helm_registry.cmi : diff --git a/matita/components/syntax_extensions/.depend.opt b/matita/components/syntax_extensions/.depend.opt index 98ac1d844..84b72a664 100644 --- a/matita/components/syntax_extensions/.depend.opt +++ b/matita/components/syntax_extensions/.depend.opt @@ -1,3 +1,5 @@ -utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmx : \ + utf8MacroTable.cmx \ + utf8Macro.cmi utf8Macro.cmi : utf8MacroTable.cmx : diff --git a/matita/components/thread/.depend b/matita/components/thread/.depend index e8bc4a106..7bf942ba0 100644 --- a/matita/components/thread/.depend +++ b/matita/components/thread/.depend @@ -1,6 +1,10 @@ -extThread.cmo : extThread.cmi -extThread.cmx : extThread.cmi +extThread.cmo : \ + extThread.cmi +extThread.cmx : \ + extThread.cmi extThread.cmi : -threadSafe.cmo : threadSafe.cmi -threadSafe.cmx : threadSafe.cmi +threadSafe.cmo : \ + threadSafe.cmi +threadSafe.cmx : \ + threadSafe.cmi threadSafe.cmi : diff --git a/matita/components/thread/.depend.opt b/matita/components/thread/.depend.opt index 8ee8dbbec..e022019db 100644 --- a/matita/components/thread/.depend.opt +++ b/matita/components/thread/.depend.opt @@ -1,4 +1,6 @@ -extThread.cmx : extThread.cmi +extThread.cmx : \ + extThread.cmi extThread.cmi : -threadSafe.cmx : threadSafe.cmi +threadSafe.cmx : \ + threadSafe.cmi threadSafe.cmi : diff --git a/matita/components/xml/.depend b/matita/components/xml/.depend index 60964e765..2ed17ef38 100644 --- a/matita/components/xml/.depend +++ b/matita/components/xml/.depend @@ -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 : diff --git a/matita/components/xml/.depend.opt b/matita/components/xml/.depend.opt index 36a543808..31b27a176 100644 --- a/matita/components/xml/.depend.opt +++ b/matita/components/xml/.depend.opt @@ -1,4 +1,6 @@ -xml.cmx : xml.cmi +xml.cmx : \ + xml.cmi xml.cmi : -xmlPushParser.cmx : xmlPushParser.cmi +xmlPushParser.cmx : \ + xmlPushParser.cmi xmlPushParser.cmi : diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml index 50d7d25bf..2ae27ee63 100644 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@ -96,3 +96,15 @@ class status = 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 --git a/matita/matita/help/C/sec_declarative_tactics.xml b/matita/matita/help/C/sec_declarative_tactics.xml index d77c276c4..9c1ed995c 100644 --- a/matita/matita/help/C/sec_declarative_tactics.xml +++ b/matita/matita/help/C/sec_declarative_tactics.xml @@ -1,5 +1,4 @@ - diff --git a/matita/matita/lib/didactic/natural_deduction.ma b/matita/matita/lib/didactic/natural_deduction.ma new file mode 100644 index 000000000..45ce24f91 --- /dev/null +++ b/matita/matita/lib/didactic/natural_deduction.ma @@ -0,0 +1,863 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +(* Logic system *) + +include "basics/pts.ma". +include "hints_declaration.ma". + +inductive Imply (A,B:Prop) : Prop ≝ +| Imply_intro: (A → B) → Imply A B. + +definition Imply_elim ≝ λA,B:Prop.λf:Imply A B. λa:A. + match f with [ Imply_intro g ⇒ g a]. + +inductive And (A,B:Prop) : Prop ≝ +| And_intro: A → B → And A B. + +definition And_elim_l ≝ λA,B.λc:And A B. + match c with [ And_intro a b ⇒ a ]. + +definition And_elim_r ≝ λA,B.λc:And A B. + match c with [ And_intro a b ⇒ b ]. + +inductive Or (A,B:Prop) : Prop ≝ +| Or_intro_l: A → Or A B +| Or_intro_r: B → Or A B. + +definition Or_elim ≝ λA,B,C:Prop.λc:Or A B.λfa: A → C.λfb: B → C. + match c with + [ Or_intro_l a ⇒ fa a + | Or_intro_r b ⇒ fb b]. + +inductive Top : Prop := +| Top_intro : Top. + +inductive Bot : Prop := . + +definition Bot_elim ≝ λP:Prop.λx:Bot. + match x in Bot return λx.P with []. + +definition Not := λA:Prop.Imply A Bot. + +definition Not_intro : ∀A.(A → Bot) → Not A ≝ λA. + Imply_intro A Bot. + +definition Not_elim : ∀A.Not A → A → Bot ≝ λA. + Imply_elim ? Bot. + +definition Discharge := λA:Prop.λa:A. + a. + +axiom Raa : ∀A.(Not A → Bot) → A. + +axiom sort : Type[0]. + +inductive Exists (A:Type[0]) (P:A→Prop) : Prop ≝ + Exists_intro: ∀w:A. P w → Exists A P. + +definition Exists_elim ≝ + λA:Type[0].λP:A→Prop.λC:Prop.λc:Exists A P.λH:(Πx.P x → C). + match c with [ Exists_intro w p ⇒ H w p ]. + +inductive Forall (A:Type[0]) (P:A→Prop) : Prop ≝ + Forall_intro: (∀n:A. P n) → Forall A P. + +definition Forall_elim ≝ + λA:Type[0].λP:A→Prop.λn:A.λf:Forall A P.match f with [ Forall_intro g ⇒ g n ]. + +(* Dummy proposition *) +axiom unit : Prop. + +(* Notations *) +notation "hbox(a break ⇒ b)" right associative with precedence 20 +for @{ 'Imply $a $b }. +interpretation "Imply" 'Imply a b = (Imply a b). +interpretation "constructive or" 'or x y = (Or x y). +interpretation "constructive and" 'and x y = (And x y). +notation "⊤" non associative with precedence 90 for @{'Top}. +interpretation "Top" 'Top = Top. +notation "⊥" non associative with precedence 90 for @{'Bot}. +interpretation "Bot" 'Bot = Bot. +interpretation "Not" 'not a = (Not a). +notation "✶" non associative with precedence 90 for @{'unit}. +interpretation "dummy prop" 'unit = unit. +notation > "\exists list1 ident x sep , . term 19 Px" with precedence 20 +for ${ fold right @{$Px} rec acc @{'myexists (λ${ident x}.$acc)} }. +notation < "hvbox(\exists ident i break . p)" with precedence 20 +for @{ 'myexists (\lambda ${ident i} : $ty. $p) }. +interpretation "constructive ex" 'myexists \eta.x = (Exists sort x). +notation > "\forall ident x.break term 19 Px" with precedence 20 +for @{ 'Forall (λ${ident x}.$Px) }. +notation < "\forall ident x.break term 19 Px" with precedence 20 +for @{ 'Forall (λ${ident x}:$tx.$Px) }. +interpretation "Forall" 'Forall \eta.Px = (Forall ? Px). + +(* Variables *) +axiom A : Prop. +axiom B : Prop. +axiom C : Prop. +axiom D : Prop. +axiom E : Prop. +axiom F : Prop. +axiom G : Prop. +axiom H : Prop. +axiom I : Prop. +axiom J : Prop. +axiom K : Prop. +axiom L : Prop. +axiom M : Prop. +axiom N : Prop. +axiom O : Prop. +axiom x: sort. +axiom y: sort. +axiom z: sort. +axiom w: sort. + +(* Every formula user provided annotates its proof: + `A` becomes `(show A ?)` *) +definition show : ΠA.A→A ≝ λA:Prop.λa:A.a. + +(* When something does not fit, this daemon is used *) +axiom cast: ΠA,B:Prop.B → A. + +(* begin a proof: draws the root *) +notation > "'prove' p" non associative with precedence 19 +for @{ 'prove $p }. +interpretation "prove KO" 'prove p = (cast ? ? (show p ?)). +interpretation "prove OK" 'prove p = (show p ?). + +(* Leaves *) +notation < "\infrule (t\atop ⋮) a ?" with precedence 19 +for @{ 'leaf_ok $a $t }. +interpretation "leaf OK" 'leaf_ok a t = (show a t). +notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 +for @{ 'leaf_ko $a $t }. +interpretation "leaf KO" 'leaf_ko a t = (cast ? ? (show a t)). + +(* discharging *) +notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 +for @{ 'discharge_ko_1 $a $H }. +interpretation "discharge_ko_1" 'discharge_ko_1 a H = + (show a (cast ? ? (Discharge ? H))). +notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19 +for @{ 'discharge_ko_2 $a $H }. +interpretation "discharge_ko_2" 'discharge_ko_2 a H = + (cast ? ? (show a (cast ? ? (Discharge ? H)))). + +notation < "[ a ] \sup H" with precedence 19 +for @{ 'discharge_ok_1 $a $H }. +interpretation "discharge_ok_1" 'discharge_ok_1 a H = + (show a (Discharge ? H)). +notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 +for @{ 'discharge_ok_2 $a $H }. +interpretation "discharge_ok_2" 'discharge_ok_2 a H = + (cast ? ? (show a (Discharge ? H))). + +notation > "'discharge' [H]" with precedence 19 +for @{ 'discharge $H }. +interpretation "discharge KO" 'discharge H = (cast ? ? (Discharge ? H)). +interpretation "discharge OK" 'discharge H = (Discharge ? H). + +(* ⇒ introduction *) +notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19 +for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }. +interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b = + (show ab (cast ? ? (Imply_intro ? ? b))). + +notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19 +for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }. +interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b = + (cast ? ? (show ab (cast ? ? (Imply_intro ? ? b)))). + +notation < "maction (\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) ) (\vdots)" with precedence 19 +for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }. +interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b = + (show ab (Imply_intro ? ? b)). + +notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19 +for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }. +interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b = + (cast ? ? (show ab (Imply_intro ? ? b))). + +notation > "⇒#'i' [ident H] term 90 b" with precedence 19 +for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }. + +interpretation "Imply_intro KO" 'Imply_intro b pb = + (cast ? (Imply unit b) (Imply_intro ? b pb)). +interpretation "Imply_intro OK" 'Imply_intro b pb = + (Imply_intro ? b pb). + +(* ⇒ elimination *) +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19 +for @{ 'Imply_elim_ko_1 $ab $a $b }. +interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b = + (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a)))). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 +for @{ 'Imply_elim_ko_2 $ab $a $b }. +interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b = + (cast ? ? (show b (cast ? ? (Imply_elim ? ? (cast ? ? ab) (cast ? ? a))))). + +notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" with precedence 19 +for @{ 'Imply_elim_ok_1 $ab $a $b }. +interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b = + (show b (Imply_elim ? ? ab a)). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19 +for @{ 'Imply_elim_ok_2 $ab $a $b }. +interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b = + (cast ? ? (show b (Imply_elim ? ? ab a))). + +notation > "⇒#'e' term 90 ab term 90 a" with precedence 19 +for @{ 'Imply_elim (show $ab ?) (show $a ?) }. +interpretation "Imply_elim KO" 'Imply_elim ab a = + (cast ? ? (Imply_elim ? ? (cast (Imply unit unit) ? ab) (cast unit ? a))). +interpretation "Imply_elim OK" 'Imply_elim ab a = + (Imply_elim ? ? ab a). + +(* ∧ introduction *) +notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 +for @{ 'And_intro_ko_1 $a $b $ab }. +interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab = + (show ab (cast ? ? (And_intro ? ? a b))). + +notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 +for @{ 'And_intro_ko_2 $a $b $ab }. +interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab = + (cast ? ? (show ab (cast ? ? (And_intro ? ? a b)))). + +notation < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" with precedence 19 +for @{ 'And_intro_ok_1 $a $b $ab }. +interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab = + (show ab (And_intro ? ? a b)). + +notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19 +for @{ 'And_intro_ok_2 $a $b $ab }. +interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab = + (cast ? ? (show ab (And_intro ? ? a b))). + +notation > "∧#'i' term 90 a term 90 b" with precedence 19 +for @{ 'And_intro (show $a ?) (show $b ?) }. +interpretation "And_intro KO" 'And_intro a b = (cast ? ? (And_intro ? ? a b)). +interpretation "And_intro OK" 'And_intro a b = (And_intro ? ? a b). + +(* ∧ elimination *) +notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 +for @{ 'And_elim_l_ko_1 $ab $a }. +interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a = + (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab)))). + +notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 +for @{ 'And_elim_l_ko_2 $ab $a }. +interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a = + (cast ? ? (show a (cast ? ? (And_elim_l ? ? (cast ? ? ab))))). + +notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" with precedence 19 +for @{ 'And_elim_l_ok_1 $ab $a }. +interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a = + (show a (And_elim_l ? ? ab)). + +notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19 +for @{ 'And_elim_l_ok_2 $ab $a }. +interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a = + (cast ? ? (show a (And_elim_l ? ? ab))). + +notation > "∧#'e_l' term 90 ab" with precedence 19 +for @{ 'And_elim_l (show $ab ?) }. +interpretation "And_elim_l KO" 'And_elim_l a = (cast ? ? (And_elim_l ? ? (cast (And unit unit) ? a))). +interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l ? ? a). + +notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 +for @{ 'And_elim_r_ko_1 $ab $a }. +interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a = + (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab)))). + +notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 +for @{ 'And_elim_r_ko_2 $ab $a }. +interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a = + (cast ? ? (show a (cast ? ? (And_elim_r ? ? (cast ? ? ab))))). + +notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" with precedence 19 +for @{ 'And_elim_r_ok_1 $ab $a }. +interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a = + (show a (And_elim_r ? ? ab)). + +notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19 +for @{ 'And_elim_r_ok_2 $ab $a }. +interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a = + (cast ? ? (show a (And_elim_r ? ? ab))). + +notation > "∧#'e_r' term 90 ab" with precedence 19 +for @{ 'And_elim_r (show $ab ?) }. +interpretation "And_elim_r KO" 'And_elim_r a = (cast ? ? (And_elim_r ? ? (cast (And unit unit) ? a))). +interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r ? ? a). + +(* ∨ introduction *) +notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 +for @{ 'Or_intro_l_ko_1 $a $ab }. +interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab = + (show ab (cast ? ? (Or_intro_l ? ? a))). + +notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 +for @{ 'Or_intro_l_ko_2 $a $ab }. +interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab = + (cast ? ? (show ab (cast ? ? (Or_intro_l ? ? a)))). + +notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" with precedence 19 +for @{ 'Or_intro_l_ok_1 $a $ab }. +interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab = + (show ab (Or_intro_l ? ? a)). + +notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 +for @{ 'Or_intro_l_ok_2 $a $ab }. +interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = + (cast ? ? (show ab (Or_intro_l ? ? a))). + +notation > "∨#'i_l' term 90 a" with precedence 19 +for @{ 'Or_intro_l (show $a ?) }. +interpretation "Or_intro_l KO" 'Or_intro_l a = (cast ? (Or ? unit) (Or_intro_l ? ? a)). +interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l ? ? a). + +notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 +for @{ 'Or_intro_r_ko_1 $a $ab }. +interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab = + (show ab (cast ? ? (Or_intro_r ? ? a))). + +notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 +for @{ 'Or_intro_r_ko_2 $a $ab }. +interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab = + (cast ? ? (show ab (cast ? ? (Or_intro_r ? ? a)))). + +notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" with precedence 19 +for @{ 'Or_intro_r_ok_1 $a $ab }. +interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab = + (show ab (Or_intro_r ? ? a)). + +notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19 +for @{ 'Or_intro_r_ok_2 $a $ab }. +interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = + (cast ? ? (show ab (Or_intro_r ? ? a))). + +notation > "∨#'i_r' term 90 a" with precedence 19 +for @{ 'Or_intro_r (show $a ?) }. +interpretation "Or_intro_r KO" 'Or_intro_r a = (cast ? (Or unit ?) (Or_intro_r ? ? a)). +interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r ? ? a). + +(* ∨ elimination *) +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19 +for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }. +interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc = + (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc)))). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19 +for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }. +interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c = + (cast ? ? (show c (cast ? ? (Or_elim ? ? ? (cast ? ? ab) (cast ? ? ac) (cast ? ? bc))))). + +notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)) (\vdots)" with precedence 19 +for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }. +interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c = + (show c (Or_elim ? ? ? ab ac bc)). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19 +for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }. +interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c = + (cast ? ? (show c (Or_elim ? ? ? ab ac bc))). + +definition unit_to ≝ λx:Prop.unit → x. + +notation > "∨#'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19 +for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }. +interpretation "Or_elim KO" 'Or_elim ab ac bc = + (cast ? ? (Or_elim ? ? ? + (cast (Or unit unit) ? ab) + (cast (unit_to unit) (unit_to ?) ac) + (cast (unit_to unit) (unit_to ?) bc))). +interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim ? ? ? ab ac bc). + +(* ⊤ introduction *) +notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19 +for @{'Top_intro_ko_1}. +interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = + (show ? (cast ? ? Top_intro)). + +notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19 +for @{'Top_intro_ko_2}. +interpretation "Top_intro_ko_2" 'Top_intro_ko_2 = + (cast ? ? (show ? (cast ? ? Top_intro))). + +notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19 +for @{'Top_intro_ok_1}. +interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show ? Top_intro). + +notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19 +for @{'Top_intro_ok_2 }. +interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast ? ? (show ? Top_intro)). + +notation > "⊤#'i'" with precedence 19 for @{ 'Top_intro }. +interpretation "Top_intro KO" 'Top_intro = (cast ? ? Top_intro). +interpretation "Top_intro OK" 'Top_intro = Top_intro. + +(* ⊥ introduction *) +notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 +for @{'Bot_elim_ko_1 $a $b}. +interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b = + (show a (Bot_elim ? (cast ? ? b))). + +notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19 +for @{'Bot_elim_ko_2 $a $b}. +interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b = + (cast ? ? (show a (Bot_elim ? (cast ? ? b)))). + +notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" with precedence 19 +for @{'Bot_elim_ok_1 $a $b}. +interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b = + (show a (Bot_elim ? b)). + +notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19 +for @{'Bot_elim_ok_2 $a $b}. +interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b = + (cast ? ? (show a (Bot_elim ? b))). + +notation > "⊥#'e' term 90 b" with precedence 19 +for @{ 'Bot_elim (show $b ?) }. +interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim ? (cast ? ? a)). +interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim ? a). + +(* ¬ introduction *) +notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19 +for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }. +interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b = + (show ab (cast ? ? (Not_intro ? (cast ? ? b)))). + +notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub(\emsp\i)) \emsp ident H)" with precedence 19 +for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }. +interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b = + (cast ? ? (show ab (cast ? ? (Not_intro ? (cast ? ? b))))). + +notation < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" with precedence 19 +for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }. +interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b = + (show ab (Not_intro ? b)). + +notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19 +for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }. +interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b = + (cast ? ? (show ab (Not_intro ? b))). + +notation > "¬#'i' [ident H] term 90 b" with precedence 19 +for @{ 'Not_intro (λ${ident H}.show $b ?) }. +interpretation "Not_intro KO" 'Not_intro a = (cast ? ? (Not_intro ? (cast ? ? a))). +interpretation "Not_intro OK" 'Not_intro a = (Not_intro ? a). + +(* ¬ elimination *) +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19 +for @{ 'Not_elim_ko_1 $ab $a $b }. +interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b = + (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a)))). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\e)) " with precedence 19 +for @{ 'Not_elim_ko_2 $ab $a $b }. +interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b = + (cast ? ? (show b (cast ? ? (Not_elim ? (cast ? ? ab) (cast ? ? a))))). + +notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" with precedence 19 +for @{ 'Not_elim_ok_1 $ab $a $b }. +interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b = + (show b (Not_elim ? ab a)). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19 +for @{ 'Not_elim_ok_2 $ab $a $b }. +interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b = + (cast ? ? (show b (Not_elim ? ab a))). + +notation > "¬#'e' term 90 ab term 90 a" with precedence 19 +for @{ 'Not_elim (show $ab ?) (show $a ?) }. +interpretation "Not_elim KO" 'Not_elim ab a = + (cast ? ? (Not_elim unit (cast ? ? ab) (cast ? ? a))). +interpretation "Not_elim OK" 'Not_elim ab a = + (Not_elim ? ab a). + +(* RAA *) +notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19 +for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn = + (show Pn (cast ? ? (Raa ? (cast ? ? Px)))). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19 +for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn = + (cast ? ? (show Pn (cast ? ? (Raa ? (cast ? ? Px))))). + +notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" with precedence 19 +for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn = + (show Pn (Raa ? Px)). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19 +for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn = + (cast ? ? (show Pn (Raa ? Px))). + +notation > "'RAA' [ident H] term 90 b" with precedence 19 +for @{ 'Raa (λ${ident H}.show $b ?) }. +interpretation "RAA KO" 'Raa p = (cast ? unit (Raa ? (cast ? (unit_to ?) p))). +interpretation "RAA OK" 'Raa p = (Raa ? p). + +(* ∃ introduction *) +notation < "\infrule hbox(\emsp Pn \emsp) Px mstyle color #ff0000 (∃\sub\i)" with precedence 19 +for @{ 'Exists_intro_ko_1 $Pn $Px }. +interpretation "Exists_intro_ko_1" 'Exists_intro_ko_1 Pn Px = + (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn)))). + +notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) mstyle color #ff0000 (∃\sub\i)" with precedence 19 +for @{ 'Exists_intro_ko_2 $Pn $Px }. +interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px = + (cast ? ? (show Px (cast ? ? (Exists_intro ? ? ? (cast ? ? Pn))))). + +notation < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" with precedence 19 +for @{ 'Exists_intro_ok_1 $Pn $Px }. +interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px = + (show Px (Exists_intro ? ? ? Pn)). + +notation < "\infrule hbox(\emsp Pn \emsp) mstyle color #ff0000 (Px) (∃\sub\i)" with precedence 19 +for @{ 'Exists_intro_ok_2 $Pn $Px }. +interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px = + (cast ? ? (show Px (Exists_intro ? ? ? Pn))). + +notation >"∃#'i' {term 90 t} term 90 Pt" non associative with precedence 19 +for @{'Exists_intro $t (λw.? w) (show $Pt ?)}. +interpretation "Exists_intro KO" 'Exists_intro t P Pt = + (cast ? ? (Exists_intro sort P t (cast ? ? Pt))). +interpretation "Exists_intro OK" 'Exists_intro t P Pt = + (Exists_intro sort P t Pt). + +(* ∃ elimination *) +notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19 +for @{ 'Exists_elim_ko_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }. +interpretation "Exists_elim_ko_1" 'Exists_elim_ko_1 ExPx Pc c = + (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc)))). + +notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∃\sub\e) \emsp ident n \emsp ident HPn)" with precedence 19 +for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }. +interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c = + (cast ? ? (show c (cast ? ? (Exists_elim ? ? ? (cast ? ? ExPx) (cast ? ? Pc))))). + +notation < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" with precedence 19 +for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }. +interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c = + (show c (Exists_elim ? ? ? ExPx Pc)). + +notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) mstyle color #ff0000 (c) (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19 +for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }. +interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c = + (cast ? ? (show c (Exists_elim ? ? ? ExPx Pc))). + +definition ex_concl := λx:sort → Prop.Πy:sort.unit → x y. +definition ex_concl_dummy := Πy:sort.unit → unit. +definition fake_pred := λx:sort.unit. + +notation >"∃#'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19 +for @{'Exists_elim (λx.? x) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}. +interpretation "Exists_elim KO" 'Exists_elim P ExPt c = + (cast ? ? (Exists_elim sort P ? + (cast (Exists ? P) ? ExPt) + (cast ex_concl_dummy (ex_concl ?) c))). +interpretation "Exists_elim OK" 'Exists_elim P ExPt c = + (Exists_elim sort P ? ExPt c). + +(* ∀ introduction *) + +notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19 +for @{ 'Forall_intro_ko_1 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "Forall_intro_ko_1" 'Forall_intro_ko_1 Px Pn = + (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px)))). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\i) \emsp ident x)" with precedence 19 +for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn = + (cast ? ? (show Pn (cast ? ? (Forall_intro ? ? (cast ? ? Px))))). + +notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" with precedence 19 +for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn = + (show Pn (Forall_intro ? ? Px)). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\i \emsp ident x)" with precedence 19 +for @{ 'Forall_intro_ok_2 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "Forall_intro_ok_2" 'Forall_intro_ok_2 Px Pn = + (cast ? ? (show Pn (Forall_intro ? ? Px))). + +notation > "∀#'i' {ident y} term 90 Px" non associative with precedence 19 +for @{ 'Forall_intro (λ_.?) (λ${ident y}.show $Px ?) }. +interpretation "Forall_intro KO" 'Forall_intro P Px = + (cast ? ? (Forall_intro sort P (cast ? ? Px))). +interpretation "Forall_intro OK" 'Forall_intro P Px = + (Forall_intro sort P Px). + +(* ∀ elimination *) +notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (∀\sub\e))" with precedence 19 +for @{ 'Forall_elim_ko_1 $Px $Pn }. +interpretation "Forall_elim_ko_1" 'Forall_elim_ko_1 Px Pn = + (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px)))). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000(Pn) (mstyle color #ff0000 (∀\sub\e))" with precedence 19 +for @{ 'Forall_elim_ko_2 $Px $Pn }. +interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn = + (cast ? ? (show Pn (cast ? ? (Forall_elim ? ? ? (cast ? ? Px))))). + +notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" with precedence 19 +for @{ 'Forall_elim_ok_1 $Px $Pn }. +interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn = + (show Pn (Forall_elim ? ? ? Px)). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (∀\sub\e)" with precedence 19 +for @{ 'Forall_elim_ok_2 $Px $Pn }. +interpretation "Forall_elim_ok_2" 'Forall_elim_ok_2 Px Pn = + (cast ? ? (show Pn (Forall_elim ? ? ? Px))). + +notation > "∀#'e' {term 90 t} term 90 Pn" non associative with precedence 19 +for @{ 'Forall_elim (λ_.?) $t (show $Pn ?) }. +interpretation "Forall_elim KO" 'Forall_elim P t Px = + (cast ? unit (Forall_elim sort P t (cast ? ? Px))). +interpretation "Forall_elim OK" 'Forall_elim P t Px = + (Forall_elim sort P t Px). + +(* already proved lemma *) +definition hide_args : ΠA:Type[0].A→A := λA:Type[0].λa:A.a. +notation < "t" non associative with precedence 90 for @{'hide_args $t}. +interpretation "hide 0 args" 'hide_args t = (hide_args ? t). +interpretation "hide 1 args" 'hide_args t = (hide_args ? t ?). +interpretation "hide 2 args" 'hide_args t = (hide_args ? t ? ?). +interpretation "hide 3 args" 'hide_args t = (hide_args ? t ? ? ?). +interpretation "hide 4 args" 'hide_args t = (hide_args ? t ? ? ? ?). +interpretation "hide 5 args" 'hide_args t = (hide_args ? t ? ? ? ? ?). +interpretation "hide 6 args" 'hide_args t = (hide_args ? t ? ? ? ? ? ?). +interpretation "hide 7 args" 'hide_args t = (hide_args ? t ? ? ? ? ? ? ?). + +(* more args crashes the pattern matcher *) + +(* already proved lemma, 0 assumptions *) +definition Lemma : ΠA.A→A ≝ λA:Prop.λa:A.a. + +notation < "\infrule + (\infrule + (\emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma_ko_1 $p ($H : $_) }. +interpretation "lemma_ko_1" 'lemma_ko_1 p H = + (show p (cast ? ? (Lemma ? (cast ? ? H)))). + +notation < "\infrule + (\infrule + (\emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma_ko_2 $p ($H : $_) }. +interpretation "lemma_ko_2" 'lemma_ko_2 p H = + (cast ? ? (show p (cast ? ? + (Lemma ? (cast ? ? H))))). + + +notation < "\infrule + (\infrule + (\emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma_ok_1 $p ($H : $_) }. +interpretation "lemma_ok_1" 'lemma_ok_1 p H = + (show p (Lemma ? H)). + +notation < "\infrule + (\infrule + (\emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma_ok_2 $p ($H : $_) }. +interpretation "lemma_ok_2" 'lemma_ok_2 p H = + (cast ? ? (show p (Lemma ? H))). + +notation > "'lem' 0 term 90 l" non associative with precedence 19 +for @{ 'Lemma (hide_args ? $l : ?) }. +interpretation "lemma KO" 'Lemma l = + (cast ? ? (Lemma unit (cast unit ? l))). +interpretation "lemma OK" 'Lemma l = (Lemma ? l). + + +(* already proved lemma, 1 assumption *) +definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝ + λA,B:Prop.λf:A⇒B.λa:A. + Imply_elim A B f a. + +notation < "\infrule + (\infrule + (\emsp a \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma1_ko_1 $a $p ($H : $_) }. +interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H = + (show p (cast ? ? (Lemma1 ? ? (cast ? ? H) (cast ? ? a)))). + +notation < "\infrule + (\infrule + (\emsp a \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma1_ko_2 $a $p ($H : $_) }. +interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H = + (cast ? ? (show p (cast ? ? + (Lemma1 ? ? (cast ? ? H) (cast ? ? a))))). + + +notation < "\infrule + (\infrule + (\emsp a \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma1_ok_1 $a $p ($H : $_) }. +interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H = + (show p (Lemma1 ? ? H a)). + +notation < "\infrule + (\infrule + (\emsp a \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma1_ok_2 $a $p ($H : $_) }. +interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H = + (cast ? ? (show p (Lemma1 ? ? H a))). + + +notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19 +for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }. +interpretation "lemma 1 KO" 'Lemma1 l p = + (cast ? ? (Lemma1 unit unit (cast (Imply unit unit) ? l) (cast unit ? p))). +interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 ? ? l p). + +(* already proved lemma, 2 assumptions *) +definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝ + λA,B,C:Prop.λf:A⇒B⇒C.λa:A.λb:B. + Imply_elim B C (Imply_elim A (B⇒C) f a) b. + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }. +interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H = + (show p (cast ? ? (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b)))). + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }. +interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H = + (cast ? ? (show p (cast ? ? + (Lemma2 ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b))))). + + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }. +interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H = + (show p (Lemma2 ? ? ? H a b)). + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }. +interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H = + (cast ? ? (show p (Lemma2 ? ? ? H a b))). + +notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19 +for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }. +interpretation "lemma 2 KO" 'Lemma2 l p q = + (cast ? ? (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) ? l) (cast unit ? p) (cast unit ? q))). +interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 ? ? ? l p q). + +(* already proved lemma, 3 assumptions *) +definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝ + λA,B,C,D:Prop.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C. + Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c. + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }. +interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H = + (show p (cast ? ? + (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c)))). + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) + (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }. +interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H = + (cast ? ? (show p (cast ? ? + (Lemma3 ? ? ? ? (cast ? ? H) (cast ? ? a) (cast ? ? b) (cast ? ? c))))). + + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + p \nbsp" +non associative with precedence 19 +for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }. +interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H = + (show p (Lemma3 ? ? ? ? H a b c)). + +notation < "\infrule + (\infrule + (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) + (╲ mstyle mathsize normal (H) ╱) \nbsp) + mstyle color #ff0000 (p) \nbsp" +non associative with precedence 19 +for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }. +interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H = + (cast ? ? (show p (Lemma3 ? ? ? ? H a b c))). + +notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19 +for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }. +interpretation "lemma 3 KO" 'Lemma3 l p q r = + (cast ? ? (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) ? l) (cast unit ? p) (cast unit ? q) (cast unit ? r))). +interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 ? ? ? ? l p q r). diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang index 3caf034a3..56cb0c411 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -106,6 +106,32 @@ inversion lapply destruct + assume + suppose + that + is + equivalent + to + we + need + prove + or + equivalently + by + done + proved + have + such + the + thesis + becomes + conclude + obtain + proceed + induction + case + hypothesis + know alias diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index 2963e71c4..fea7161c1 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -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,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 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 +45,105 @@ let debug_print = if debug then prerr_endline else ignore ;; 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 + 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 +;; + +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 + 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 +151,7 @@ let clean_exit baseuri exn = 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 +159,33 @@ let cut prefix s = 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,51 +201,51 @@ let pp_times ss fname rc big_bang big_bang_u big_bang_s = ;; 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)) ;; @@ -173,68 +263,68 @@ let read_include_paths ~include_paths:_ file = 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 +335,154 @@ and compile ~compiling ~asserted ~include_paths fname = 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 --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index ad34b7a57..5b7352d74 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -601,11 +601,15 @@ class gui () = 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 +626,9 @@ class gui () = 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);