-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
-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
-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
-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
-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
-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
-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 :
-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 :
-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 :
-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 :
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
grafiteAst.cmx :
-grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi
-grafiteAstPp.cmi : grafiteAst.cmx
+grafiteAstPp.cmx : \
+ grafiteAst.cmx \
+ grafiteAstPp.cmi
+grafiteAstPp.cmi : \
+ grafiteAst.cmx
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
| 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
(* 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
* 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/
*)
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 -> ""
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
| 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"
| 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
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"
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)
(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
| 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"
let pp_statement status =
function
- | Executable (_, ex) -> pp_executable status ex
+ | Executable (_, ex) -> pp_executable status ex
| Comment (_, c) -> pp_comment status c
-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
-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
;;
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)
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 *)
;;
-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
-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
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 =
| 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<def>> ; 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: [
]
];
-(* 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
-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 :
-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 :
-helmLogger.cmo : helmLogger.cmi
-helmLogger.cmx : helmLogger.cmi
+helmLogger.cmo : \
+ helmLogger.cmi
+helmLogger.cmx : \
+ helmLogger.cmi
helmLogger.cmi :
-helmLogger.cmx : helmLogger.cmi
+helmLogger.cmx : \
+ helmLogger.cmi
helmLogger.cmi :
-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 :
-interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
+interpretations.cmx : \
+ ncic2astMatcher.cmx \
+ interpretations.cmi
interpretations.cmi :
-ncic2astMatcher.cmx : ncic2astMatcher.cmi
+ncic2astMatcher.cmx : \
+ ncic2astMatcher.cmi
ncic2astMatcher.cmi :
-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 :
-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 :
-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
-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
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
-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 :
-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 :
-nCicLibrary.cmo : nCicLibrary.cmi
-nCicLibrary.cmx : nCicLibrary.cmi
+nCicLibrary.cmo : \
+ nCicLibrary.cmi
+nCicLibrary.cmx : \
+ nCicLibrary.cmi
nCicLibrary.cmi :
-nCicLibrary.cmx : nCicLibrary.cmi
+nCicLibrary.cmx : \
+ nCicLibrary.cmi
nCicLibrary.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
+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 :
-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 :
-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 :
-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 :
-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
-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
nCicElim.mli \
nTactics.mli \
nnAuto.mli \
+ declarative.mli \
nDestructTac.mli \
nInversion.mli
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
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
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
| _ -> []
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
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.
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 ->
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)));
(** {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
--- /dev/null
+(* 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:
+ * *)
--- /dev/null
+(* 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
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
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 =
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
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:
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
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
;;
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
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
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
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
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
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
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
;;
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
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
;;
;;
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
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
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
;;
leftno: int;
consno: int;
reference: NReference.reference;
+ cl: NCic.constructor list;
}
;;
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)
;;
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
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,
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 =
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
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
(*(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
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
let toref f tbl t =
match t with
| Ast.NRef n ->
- f tbl n
+ f tbl n
| Ast.NCic _ (* local candidate *)
| _ -> ()
"; 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)
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)));
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
| 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
| 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
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 []
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
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;
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 *)
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
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 =
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
(* 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))
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
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 =
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 =
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 *)
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 =
| _ -> 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
[(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
| _ -> 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
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 *)
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
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
;;
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
;;
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
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
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 = " ^
(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
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)
(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
| 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
| 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
(* 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");
(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 =
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 =
(* 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
(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
let flags = {
last = true;
candidates = candidates;
+ local_candidates = local_candidates;
maxwidth = width;
maxsize = size;
maxdepth = depth;
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
*)
| 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
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
\ / 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
-helm_registry.cmo : helm_registry.cmi
-helm_registry.cmx : helm_registry.cmi
+helm_registry.cmo : \
+ helm_registry.cmi
+helm_registry.cmx : \
+ helm_registry.cmi
helm_registry.cmi :
-helm_registry.cmx : helm_registry.cmi
+helm_registry.cmx : \
+ helm_registry.cmi
helm_registry.cmi :
-utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmx : \
+ utf8MacroTable.cmx \
+ utf8Macro.cmi
utf8Macro.cmi :
utf8MacroTable.cmx :
-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 :
-extThread.cmx : extThread.cmi
+extThread.cmx : \
+ extThread.cmi
extThread.cmi :
-threadSafe.cmx : threadSafe.cmi
+threadSafe.cmx : \
+ threadSafe.cmi
threadSafe.cmi :
-xml.cmo : xml.cmi
-xml.cmx : xml.cmi
+xml.cmo : \
+ xml.cmi
+xml.cmx : \
+ xml.cmi
xml.cmi :
-xmlPushParser.cmo : xmlPushParser.cmi
-xmlPushParser.cmx : xmlPushParser.cmi
+xmlPushParser.cmo : \
+ xmlPushParser.cmi
+xmlPushParser.cmx : \
+ xmlPushParser.cmi
xmlPushParser.cmi :
-xml.cmx : xml.cmi
+xml.cmx : \
+ xml.cmi
xml.cmi :
-xmlPushParser.cmx : xmlPushParser.cmi
+xmlPushParser.cmx : \
+ xmlPushParser.cmi
xmlPushParser.cmi :
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))
<!-- ================= Tactics ========================= -->
-<!--
<chapter id="sec_declarative_tactics">
<title>Declarative Tactics</title>
<sect1 id="tac_assume">
<title>assume</title>
<titleabbrev>assume</titleabbrev>
- <para><userinput>assume x : t</userinput></para>
+ <para><userinput>assume x : T that is equivalent to T'</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">assume</emphasis> &id; <emphasis role="bold"> : </emphasis> &sterm;</para>
+ <para><emphasis role="bold">assume</emphasis> &id; <emphasis role="bold"> : </emphasis>
+ &sterm; [ <emphasis role="bold">that is equivalent to</emphasis> &term; ]</para>
</listitem>
</varlistentry>
<varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>It adds to the context of the current sequent to prove a new
- declaration <command>x : T </command>. The new conclusion becomes
- <command>P</command>.</para>
+ <para>It adds to the context of the current sequent to prove a new declaration <command>x : T
+ </command>. The new conclusion becomes <command>P</command>. Alternatively, if a type
+ <command>T'</command> is supplied and <command>T</command> and <command>T'</command> are beta equivalent the new declaration that is added to the context is
+ <command>x:T'</command>.</para>
</listitem>
</varlistentry>
<varlistentry>
</para>
</sect1>
- <sect1 id="tac_byinduction">
- <title>by induction hypothesis we know</title>
- <titleabbrev>by induction hypothesis we know</titleabbrev>
- <para><userinput>by induction hypothesis we know t (id)</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>To be used in a proof by induction to state the inductive
- hypothesis.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para> Introduces the inductive hypothesis. </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
+ <sect1 id="tac_suppose">
+ <title>suppose</title>
+ <titleabbrev>suppose</titleabbrev>
+ <para><userinput>suppose T (x) that is equivalent to T'</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
+ <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term; ]</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>The conclusion of the current proof must be
+ <command>∀x:T.P</command> or
+ <command>T→P</command> where <command>T</command> is
+ a proposition (i.e. <command>T</command> has type
+ <command>Prop</command> or <command>CProp</command>).</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It adds to the context of the current sequent to prove a new declaration <command>x : T
+ </command>. The new conclusion becomes <command>P</command>. Alternatively, if a type
+ <command>T'</command> is supplied and <command>T</command> and <command>T'</command> are beta equivalent the new declaration that is added to the context is
+ <command>x:T'</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
- <sect1 id="tac_case">
- <title>case</title>
- <titleabbrev>case</titleabbrev>
- <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>
+<sect1 id="tac_let">
+ <title>letin</title>
+ <titleabbrev>letin</titleabbrev>
+ <para><userinput>let x := T </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">let</emphasis> &id; <emphasis role="bold"> = </emphasis> &term;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>None</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It adds a new local definition <command>x := T</command> to the context of the sequent to prove.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_bytermweproved">
+ <title>we proved</title>
+ <titleabbrev>we proved</titleabbrev>
+ <para><userinput>justification we proved T (id) that is equivalent to T'</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">)</emphasis>] … </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>To be used in a proof by induction or by cases to start
- a new case</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>Starts the new case <command>id</command> declaring
- the local parameters <command>(id1:t1) … (idn:tn)</command></para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None</para>
+ <para>&justification; <emphasis role="bold">we proved</emphasis> &term;
+ <emphasis role="bold">(</emphasis> &id;
+ <emphasis role="bold">)</emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term;] [ <emphasis role="bold">done</emphasis>]</para>
</listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para><command>T</command> must have type <command>Prop</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It derives <command>T</command>
+ using the justification and labels the conclusion with
+ <command>id</command>. Alternatively, if a proposition
+ <command>T'</command> is supplied and <command>T</command> and <command>T'</command> are beta equivalent the new hypothesis that is added to the context is
+ <command>id:T'</command>.
+
+ If the user does not supply a label and ends the command with <command>done</command> then if T is alpha equivalent to the conclusion of the current sequent then it closes it (if <command>T'</command> is supplied this must be alpha equivalent to the conclusion, but in this case <command>T</command> does not need to).
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
<sect1 id="tac_bydone">
<title>done</title>
</para>
</sect1>
-
- <sect1 id="tac_exitselim">
+ <sect1 id="tac_existselim">
<title>let such that</title>
<titleabbrev>let such that</titleabbrev>
<para><userinput>justification let x:t such that p (id)</userinput>
</para>
</sect1>
- <sect1 id="tac_obtain">
- <title>obtain</title>
- <titleabbrev>obtain</titleabbrev>
- <para><userinput>obtain H t1 = t2 justification</userinput></para>
+ <sect1 id="tac_andelim">
+ <title>we have</title>
+ <titleabbrev>we have</titleabbrev>
+ <para><userinput>justification we have t1 (id1) and t2 (id2)</userinput>
+ </para>
<para>
<variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">using once</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para><command>conclude</command> can be used only if the current
- sequent is stating an equality. The left hand side must be omitted
- in an equality chain.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>Starts or continues an equality chain. If the chain starts
- with <command>obtain H</command> a new subproof named
- <command>H</command> is started.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequent to prove:</term>
- <listitem>
- <para>If the chain starts
- with <command>obtain H</command> a nre sequent for
- <command>t2 = ?</command> is opened.
- </para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_suppose">
- <title>suppose</title>
- <titleabbrev>suppose</titleabbrev>
- <para><userinput>suppose t1 (x) that is equivalent to t2</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
- <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term; ]</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>The conclusion of the current proof must be
- <command>∀x:T.P</command> or
- <command>T→P</command> where <command>T</command> is
- a proposition (i.e. <command>T</command> has type
- <command>Prop</command> or <command>CProp</command>).</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
+ <varlistentry role="tactic_synopsis">
+ <term>Synopsis:</term>
<listitem>
- <para>It adds to the context of the current sequent to prove a new
- declaration <command>x : T </command>. The new conclusion becomes
- <command>P</command>.</para>
+ <para>&justification; <emphasis role="bold">we have</emphasis> &term;
+ <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term;
+ <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para></para>
</listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It derives <command>t1∧t2</command> using the
+ <command>justification</command> then it introduces in the context
+ <command>t1</command> labelled with <command>id1</command> and
+ <command>t2</command> labelled with <command>id2</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
</sect1>
- <sect1 id="tac_thesisbecomes">
- <title>the thesis becomes</title>
- <titleabbrev>the thesis becomes</titleabbrev>
- <para><userinput>the thesis becomes t</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>The provided term <command>t</command> must be convertible with
- current sequent.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It changes the current goal to the one provided.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequent to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
<sect1 id="tac_weneedtoprove">
<title>we need to prove</title>
<titleabbrev>we need to prove</titleabbrev>
</para>
</sect1>
-
- <sect1 id="tac_andelim">
- <title>we have</title>
- <titleabbrev>we have</titleabbrev>
- <para><userinput>justification we have t1 (id1) and t2 (id2)</userinput>
- </para>
+ <sect1 id="tac_weproceedbyinduction">
+ <title>we proceed by induction on</title>
+ <titleabbrev>we proceed by induction on</titleabbrev>
+ <para><userinput>we proceed by induction on t to prove th</userinput></para>
<para>
<variablelist>
- <varlistentry role="tactic_synopsis">
+ <varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para>&justification; <emphasis role="bold">we have</emphasis> &term;
- <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term;
- <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
- </listitem>
+ <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
+ </listitem>
</varlistentry>
- <varlistentry>
+ <varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para></para>
+ <para><command>t</command> must inhabitant of an inductive type and
+ <command>th</command> must be the conclusion to be proved by induction.
+ </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
- <listitem>
- <para>It derives <command>t1∧t2</command> using the
- <command>justification</command> then it introduces in the context
- <command>t1</command> labelled with <command>id1</command> and
- <command>t2</command> labelled with <command>id2</command>.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequent to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
+ <listitem>
+ <para>It proceed by induction on <command>t</command>.</para>
+ </listitem>
</varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens one new sequent for each constructor of the
+ type of <command>t</command>.</para>
+ </listitem>
+ </varlistentry>
</variablelist>
</para>
</sect1>
</variablelist>
</para>
</sect1>
-
- <sect1 id="tac_weproceedbyinduction">
- <title>we proceed by induction on</title>
- <titleabbrev>we proceed by induction on</titleabbrev>
- <para><userinput>we proceed by induction on t to prove th</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para><command>t</command> must inhabitant of an inductive type and
- <command>th</command> must be the conclusion to be proved by induction.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It proceed by induction on <command>t</command>.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>It opens one new sequent for each constructor of the
- type of <command>t</command>.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_bytermweproved">
- <title>we proved</title>
- <titleabbrev>we proved</titleabbrev>
- <para><userinput>justification we proved t (id)</userinput></para>
+ <sect1 id="tac_case">
+ <title>case</title>
+ <titleabbrev>case</titleabbrev>
+ <para><userinput>case id (id1:t1) … (idn:tn)</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para>&justification; <emphasis role="bold">we proved</emphasis> &term;
- <emphasis role="bold">(</emphasis> &id;
- <emphasis role="bold">)</emphasis></para>
+ <para><emphasis role="bold">case</emphasis> &id; [<emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">)</emphasis>] … </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>To be used in a proof by induction or by cases to start
+ a new case</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Starts the new case <command>id</command> declaring
+ the local parameters <command>(id1:t1) … (idn:tn)</command></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None</para>
</listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_byinduction">
+ <title>by induction hypothesis we know</title>
+ <titleabbrev>by induction hypothesis we know</titleabbrev>
+ <para><userinput>by induction hypothesis we know t (id)</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem><para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>To be used in a proof by induction to state the inductive
+ hypothesis.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para> Introduces the inductive hypothesis. </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_thesisbecomes">
+ <title>the thesis becomes</title>
+ <titleabbrev>the thesis becomes</titleabbrev>
+ <para><userinput>the thesis becomes t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
+ </listitem>
</varlistentry>
<varlistentry>
<term>Pre-condition:</term>
<listitem>
- <para><command>t</command>must have type <command>Prop</command>.
- </para>
+ <para>The provided term <command>t</command> must be convertible with
+ current sequent.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>It derives <command>t</command>
- using the justification and labels the conclusion with
- <command>id</command>.
- </para>
+ <para>It changes the current goal to the one provided.</para>
</listitem>
</varlistentry>
<varlistentry>
</varlistentry>
</variablelist>
</para>
- </sect1>
+ </sect1>
+ <sect1 id="tac_obtain">
+ <title>conclude/obtain</title>
+ <titleabbrev>conclude/obtain</titleabbrev>
+ <para><userinput>conclude/obtain (H) t1 = t2 justification</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">using once</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para><command>conclude</command> can be used only if the current
+ sequent is stating an equality. The left hand side must be omitted
+ in an equality chain.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Starts or continues an equality chain. If the chain starts
+ with <command>obtain H</command> a new subproof named
+ <command>H</command> is started.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>If the chain starts
+ with <command>obtain H</command> a nre sequent for
+ <command>t2 = ?</command> is opened.
+ </para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+
+
+
+
+
+
</chapter>
--->
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
<keyword>inversion</keyword>
<keyword>lapply</keyword>
<keyword>destruct</keyword>
+ <keyword>assume</keyword>
+ <keyword>suppose</keyword>
+ <keyword>that</keyword>
+ <keyword>is</keyword>
+ <keyword>equivalent</keyword>
+ <keyword>to</keyword>
+ <keyword>we</keyword>
+ <keyword>need</keyword>
+ <keyword>prove</keyword>
+ <keyword>or</keyword>
+ <keyword>equivalently</keyword>
+ <keyword>by</keyword>
+ <keyword>done</keyword>
+ <keyword>proved</keyword>
+ <keyword>have</keyword>
+ <keyword>such</keyword>
+ <keyword>the</keyword>
+ <keyword>thesis</keyword>
+ <keyword>becomes</keyword>
+ <keyword>conclude</keyword>
+ <keyword>obtain</keyword>
+ <keyword>proceed</keyword>
+ <keyword>induction</keyword>
+ <keyword>case</keyword>
+ <keyword>hypothesis</keyword>
+ <keyword>know</keyword>
<!-- commands -->
<keyword>alias</keyword>
(* 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
* 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
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 =
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);
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 "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" 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
;;
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))
;;
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? *)
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)
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
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);
projects / helm.git / commitdiff