- content.cmo : content.cmi
- content.cmx : content.cmi
++content.cmo : \
++ content.cmi
++content.cmx : \
++ content.cmi
content.cmi :
- notationEnv.cmo : notationUtil.cmi notationPt.cmo notationEnv.cmi
- notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationUtil.cmi : notationPt.cmo
--notationEnv.cmi : notationPt.cmo
- notationPp.cmo : notationPt.cmo notationEnv.cmi notationPp.cmi
- notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi
--notationPp.cmi : notationPt.cmo notationEnv.cmi
++notationEnv.cmo : \
++ notationUtil.cmi \
++ notationPt.cmo \
++ notationEnv.cmi
++notationEnv.cmx : \
++ notationUtil.cmx \
++ notationPt.cmx \
++ notationEnv.cmi
++notationEnv.cmi : \
++ notationPt.cmo
++notationPp.cmo : \
++ notationPt.cmo \
++ notationEnv.cmi \
++ notationPp.cmi
++notationPp.cmx : \
++ notationPt.cmx \
++ notationEnv.cmx \
++ notationPp.cmi
++notationPp.cmi : \
++ notationPt.cmo \
++ notationEnv.cmi
notationPt.cmo :
notationPt.cmx :
-content.cmo : content.cmi
-content.cmx : content.cmi
--notationUtil.cmo : notationPt.cmo notationUtil.cmi
--notationUtil.cmx : notationPt.cmx notationUtil.cmi
- notationUtil.cmi : notationPt.cmo
-notationEnv.cmo : notationUtil.cmi notationPt.cmo notationEnv.cmi
-notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationPp.cmo : notationPt.cmo notationEnv.cmi notationPp.cmi
-notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi
++notationUtil.cmo : \
++ notationPt.cmo \
++ notationUtil.cmi
++notationUtil.cmx : \
++ notationPt.cmx \
++ notationUtil.cmi
++notationUtil.cmi : \
++ notationPt.cmo
- content.cmx : content.cmi
++content.cmx : \
++ content.cmi
content.cmi :
- notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationUtil.cmi : notationPt.cmx
--notationEnv.cmi : notationPt.cmx
- notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi
--notationPp.cmi : notationPt.cmx notationEnv.cmi
-notationPt.cmo :
++notationEnv.cmx : \
++ notationUtil.cmx \
++ notationPt.cmx \
++ notationEnv.cmi
++notationEnv.cmi : \
++ notationPt.cmx
++notationPp.cmx : \
++ notationPt.cmx \
++ notationEnv.cmx \
++ notationPp.cmi
++notationPp.cmi : \
++ notationPt.cmx \
++ notationEnv.cmi
notationPt.cmx :
-content.cmo : content.cmi
-content.cmx : content.cmi
-notationUtil.cmo : notationPt.cmx notationUtil.cmi
--notationUtil.cmx : notationPt.cmx notationUtil.cmi
- notationUtil.cmi : notationPt.cmx
-notationEnv.cmo : notationUtil.cmi notationPt.cmx notationEnv.cmi
-notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationPp.cmo : notationPt.cmx notationEnv.cmi notationPp.cmi
-notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi
++notationUtil.cmx : \
++ notationPt.cmx \
++ notationUtil.cmi
++notationUtil.cmi : \
++ notationPt.cmx
- box.cmo : renderingAttrs.cmi box.cmi
- box.cmx : renderingAttrs.cmx box.cmi
-renderingAttrs.cmi :
-cicNotationLexer.cmi :
-cicNotationParser.cmi :
-mpresentation.cmi :
++box.cmo : \
++ renderingAttrs.cmi \
++ box.cmi
++box.cmx : \
++ renderingAttrs.cmx \
++ box.cmi
box.cmi :
-content2presMatcher.cmi :
-termContentPres.cmi : cicNotationParser.cmi
-boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi
-cicNotationPres.cmi : mpresentation.cmi box.cmi
-content2pres.cmi : termContentPres.cmi cicNotationPres.cmi
-renderingAttrs.cmo : renderingAttrs.cmi
-renderingAttrs.cmx : renderingAttrs.cmi
-cicNotationLexer.cmo : cicNotationLexer.cmi
-cicNotationLexer.cmx : cicNotationLexer.cmi
-cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi
-cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi
-mpresentation.cmo : mpresentation.cmi
-mpresentation.cmx : mpresentation.cmi
-box.cmo : renderingAttrs.cmi box.cmi
-box.cmx : renderingAttrs.cmx box.cmi
-content2presMatcher.cmo : content2presMatcher.cmi
-content2presMatcher.cmx : content2presMatcher.cmi
-termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \
- cicNotationParser.cmi termContentPres.cmi
-termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \
- cicNotationParser.cmx termContentPres.cmi
--boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
++boxPp.cmo : \
++ renderingAttrs.cmi \
++ mpresentation.cmi \
++ cicNotationPres.cmi \
++ box.cmi \
boxPp.cmi
--boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
++boxPp.cmx : \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ cicNotationPres.cmx \
++ box.cmx \
boxPp.cmi
- boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi
- cicNotationLexer.cmo : cicNotationLexer.cmi
- cicNotationLexer.cmx : cicNotationLexer.cmi
-cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \
++boxPp.cmi : \
++ mpresentation.cmi \
++ cicNotationPres.cmi \
++ box.cmi
++cicNotationLexer.cmo : \
++ cicNotationLexer.cmi
++cicNotationLexer.cmx : \
++ cicNotationLexer.cmi
+cicNotationLexer.cmi :
- cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi
- cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi
++cicNotationParser.cmo : \
++ cicNotationLexer.cmi \
++ cicNotationParser.cmi
++cicNotationParser.cmx : \
++ cicNotationLexer.cmx \
++ cicNotationParser.cmi
+cicNotationParser.cmi :
- cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \
++cicNotationPres.cmo : \
++ renderingAttrs.cmi \
++ mpresentation.cmi \
++ box.cmi \
+ cicNotationPres.cmi
- cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \
++cicNotationPres.cmx : \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ box.cmx \
cicNotationPres.cmi
- cicNotationPres.cmi : mpresentation.cmi box.cmi
- content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
- cicNotationPres.cmi box.cmi content2pres.cmi
- content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
- cicNotationPres.cmx box.cmx content2pres.cmi
- content2pres.cmi : termContentPres.cmi cicNotationPres.cmi
- content2presMatcher.cmo : content2presMatcher.cmi
- content2presMatcher.cmx : content2presMatcher.cmi
-cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \
++cicNotationPres.cmi : \
++ mpresentation.cmi \
++ box.cmi
++content2pres.cmo : \
++ termContentPres.cmi \
++ renderingAttrs.cmi \
++ mpresentation.cmi \
++ cicNotationPres.cmi \
++ box.cmi \
++ content2pres.cmi
++content2pres.cmx : \
++ termContentPres.cmx \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ cicNotationPres.cmx \
++ box.cmx \
++ content2pres.cmi
++content2pres.cmi : \
++ termContentPres.cmi \
+ cicNotationPres.cmi
-content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
- cicNotationPres.cmi box.cmi content2pres.cmi
-content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
- cicNotationPres.cmx box.cmx content2pres.cmi
++content2presMatcher.cmo : \
++ content2presMatcher.cmi
++content2presMatcher.cmx : \
++ content2presMatcher.cmi
+content2presMatcher.cmi :
- mpresentation.cmo : mpresentation.cmi
- mpresentation.cmx : mpresentation.cmi
++mpresentation.cmo : \
++ mpresentation.cmi
++mpresentation.cmx : \
++ mpresentation.cmi
+mpresentation.cmi :
- renderingAttrs.cmo : renderingAttrs.cmi
- renderingAttrs.cmx : renderingAttrs.cmi
++renderingAttrs.cmo : \
++ renderingAttrs.cmi
++renderingAttrs.cmx : \
++ renderingAttrs.cmi
+renderingAttrs.cmi :
- termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \
- cicNotationParser.cmi termContentPres.cmi
- termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \
- cicNotationParser.cmx termContentPres.cmi
- termContentPres.cmi : cicNotationParser.cmi
++termContentPres.cmo : \
++ renderingAttrs.cmi \
++ content2presMatcher.cmi \
++ cicNotationParser.cmi \
++ termContentPres.cmi
++termContentPres.cmx : \
++ renderingAttrs.cmx \
++ content2presMatcher.cmx \
++ cicNotationParser.cmx \
++ termContentPres.cmi
++termContentPres.cmi : \
++ cicNotationParser.cmi
- box.cmx : renderingAttrs.cmx box.cmi
-renderingAttrs.cmi :
-cicNotationLexer.cmi :
-cicNotationParser.cmi :
-mpresentation.cmi :
++box.cmx : \
++ renderingAttrs.cmx \
++ box.cmi
box.cmi :
-content2presMatcher.cmi :
-termContentPres.cmi : cicNotationParser.cmi
-boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi
-cicNotationPres.cmi : mpresentation.cmi box.cmi
-content2pres.cmi : termContentPres.cmi cicNotationPres.cmi
-renderingAttrs.cmo : renderingAttrs.cmi
-renderingAttrs.cmx : renderingAttrs.cmi
-cicNotationLexer.cmo : cicNotationLexer.cmi
-cicNotationLexer.cmx : cicNotationLexer.cmi
-cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi
-cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi
-mpresentation.cmo : mpresentation.cmi
-mpresentation.cmx : mpresentation.cmi
-box.cmo : renderingAttrs.cmi box.cmi
-box.cmx : renderingAttrs.cmx box.cmi
-content2presMatcher.cmo : content2presMatcher.cmi
-content2presMatcher.cmx : content2presMatcher.cmi
-termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \
- cicNotationParser.cmi termContentPres.cmi
-termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \
- cicNotationParser.cmx termContentPres.cmi
-boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
- boxPp.cmi
--boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
++boxPp.cmx : \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ cicNotationPres.cmx \
++ box.cmx \
boxPp.cmi
- boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi
- cicNotationLexer.cmx : cicNotationLexer.cmi
-cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \
++boxPp.cmi : \
++ mpresentation.cmi \
++ cicNotationPres.cmi \
++ box.cmi
++cicNotationLexer.cmx : \
++ cicNotationLexer.cmi
+cicNotationLexer.cmi :
- cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi
++cicNotationParser.cmx : \
++ cicNotationLexer.cmx \
++ cicNotationParser.cmi
+cicNotationParser.cmi :
- cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \
++cicNotationPres.cmx : \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ box.cmx \
cicNotationPres.cmi
- cicNotationPres.cmi : mpresentation.cmi box.cmi
- content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
- cicNotationPres.cmx box.cmx content2pres.cmi
- content2pres.cmi : termContentPres.cmi cicNotationPres.cmi
- content2presMatcher.cmx : content2presMatcher.cmi
-cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \
++cicNotationPres.cmi : \
++ mpresentation.cmi \
++ box.cmi
++content2pres.cmx : \
++ termContentPres.cmx \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ cicNotationPres.cmx \
++ box.cmx \
++ content2pres.cmi
++content2pres.cmi : \
++ termContentPres.cmi \
+ cicNotationPres.cmi
-content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
- cicNotationPres.cmi box.cmi content2pres.cmi
-content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
- cicNotationPres.cmx box.cmx content2pres.cmi
++content2presMatcher.cmx : \
++ content2presMatcher.cmi
+content2presMatcher.cmi :
- mpresentation.cmx : mpresentation.cmi
++mpresentation.cmx : \
++ mpresentation.cmi
+mpresentation.cmi :
- renderingAttrs.cmx : renderingAttrs.cmi
++renderingAttrs.cmx : \
++ renderingAttrs.cmi
+renderingAttrs.cmi :
- termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \
- cicNotationParser.cmx termContentPres.cmi
- termContentPres.cmi : cicNotationParser.cmi
++termContentPres.cmx : \
++ renderingAttrs.cmx \
++ content2presMatcher.cmx \
++ cicNotationParser.cmx \
++ termContentPres.cmi
++termContentPres.cmi : \
++ cicNotationParser.cmi
- disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi
- disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi
- disambiguate.cmi : disambiguateTypes.cmi
- disambiguateTypes.cmo : disambiguateTypes.cmi
- disambiguateTypes.cmx : disambiguateTypes.cmi
++disambiguate.cmo : \
++ disambiguateTypes.cmi \
++ disambiguate.cmi
++disambiguate.cmx : \
++ disambiguateTypes.cmx \
++ disambiguate.cmi
++disambiguate.cmi : \
++ disambiguateTypes.cmi
++disambiguateTypes.cmo : \
++ disambiguateTypes.cmi
++disambiguateTypes.cmx : \
++ disambiguateTypes.cmi
disambiguateTypes.cmi :
-disambiguate.cmi : disambiguateTypes.cmi
-multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi
-disambiguateTypes.cmo : disambiguateTypes.cmi
-disambiguateTypes.cmx : disambiguateTypes.cmi
-disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi
-disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi
--multiPassDisambiguator.cmo : disambiguateTypes.cmi disambiguate.cmi \
++multiPassDisambiguator.cmo : \
++ disambiguateTypes.cmi \
++ disambiguate.cmi \
multiPassDisambiguator.cmi
--multiPassDisambiguator.cmx : disambiguateTypes.cmx disambiguate.cmx \
++multiPassDisambiguator.cmx : \
++ disambiguateTypes.cmx \
++ disambiguate.cmx \
multiPassDisambiguator.cmi
- multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi
++multiPassDisambiguator.cmi : \
++ disambiguateTypes.cmi \
++ disambiguate.cmi
- disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi
- disambiguate.cmi : disambiguateTypes.cmi
- disambiguateTypes.cmx : disambiguateTypes.cmi
++disambiguate.cmx : \
++ disambiguateTypes.cmx \
++ disambiguate.cmi
++disambiguate.cmi : \
++ disambiguateTypes.cmi
++disambiguateTypes.cmx : \
++ disambiguateTypes.cmi
disambiguateTypes.cmi :
-disambiguate.cmi : disambiguateTypes.cmi
-multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi
-disambiguateTypes.cmo : disambiguateTypes.cmi
-disambiguateTypes.cmx : disambiguateTypes.cmi
-disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi
-disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi
-multiPassDisambiguator.cmo : disambiguateTypes.cmi disambiguate.cmi \
- multiPassDisambiguator.cmi
--multiPassDisambiguator.cmx : disambiguateTypes.cmx disambiguate.cmx \
++multiPassDisambiguator.cmx : \
++ disambiguateTypes.cmx \
++ disambiguate.cmx \
multiPassDisambiguator.cmi
- multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi
++multiPassDisambiguator.cmi : \
++ disambiguateTypes.cmi \
++ disambiguate.cmi
- componentsConf.cmo : componentsConf.cmi
- componentsConf.cmx : componentsConf.cmi
++componentsConf.cmo : \
++ componentsConf.cmi
++componentsConf.cmx : \
++ componentsConf.cmi
componentsConf.cmi :
- discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi
- discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi
++discrimination_tree.cmo : \
++ trie.cmi \
++ hExtlib.cmi \
++ discrimination_tree.cmi
++discrimination_tree.cmx : \
++ trie.cmx \
++ hExtlib.cmx \
++ discrimination_tree.cmi
+discrimination_tree.cmi :
- graphvizPp.cmo : graphvizPp.cmi
- graphvizPp.cmx : graphvizPp.cmi
++graphvizPp.cmo : \
++ graphvizPp.cmi
++graphvizPp.cmx : \
++ graphvizPp.cmi
+graphvizPp.cmi :
- hExtlib.cmo : hExtlib.cmi
- hExtlib.cmx : hExtlib.cmi
++hExtlib.cmo : \
++ hExtlib.cmi
++hExtlib.cmx : \
++ hExtlib.cmi
hExtlib.cmi :
- hLog.cmo : hLog.cmi
- hLog.cmx : hLog.cmi
++hLog.cmo : \
++ hLog.cmi
++hLog.cmx : \
++ hLog.cmi
+hLog.cmi :
- hMarshal.cmo : hExtlib.cmi hMarshal.cmi
- hMarshal.cmx : hExtlib.cmx hMarshal.cmi
++hMarshal.cmo : \
++ hExtlib.cmi \
++ hMarshal.cmi
++hMarshal.cmx : \
++ hExtlib.cmx \
++ hMarshal.cmi
hMarshal.cmi :
- hTopoSort.cmo : hTopoSort.cmi
- hTopoSort.cmx : hTopoSort.cmi
++hTopoSort.cmo : \
++ hTopoSort.cmi
++hTopoSort.cmx : \
++ hTopoSort.cmi
+hTopoSort.cmi :
- patternMatcher.cmo : patternMatcher.cmi
- patternMatcher.cmx : patternMatcher.cmi
++patternMatcher.cmo : \
++ patternMatcher.cmi
++patternMatcher.cmx : \
++ patternMatcher.cmi
patternMatcher.cmi :
- trie.cmo : trie.cmi
- trie.cmx : trie.cmi
-hLog.cmi :
++trie.cmo : \
++ trie.cmi
++trie.cmx : \
++ trie.cmi
trie.cmi :
-discrimination_tree.cmi :
-hTopoSort.cmi :
-graphvizPp.cmi :
-componentsConf.cmo : componentsConf.cmi
-componentsConf.cmx : componentsConf.cmi
-hExtlib.cmo : hExtlib.cmi
-hExtlib.cmx : hExtlib.cmi
-hMarshal.cmo : hExtlib.cmi hMarshal.cmi
-hMarshal.cmx : hExtlib.cmx hMarshal.cmi
-patternMatcher.cmo : patternMatcher.cmi
-patternMatcher.cmx : patternMatcher.cmi
-hLog.cmo : hLog.cmi
-hLog.cmx : hLog.cmi
-trie.cmo : trie.cmi
-trie.cmx : trie.cmi
-discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi
-discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi
-hTopoSort.cmo : hTopoSort.cmi
-hTopoSort.cmx : hTopoSort.cmi
-graphvizPp.cmo : graphvizPp.cmi
-graphvizPp.cmx : graphvizPp.cmi
- componentsConf.cmx : componentsConf.cmi
++componentsConf.cmx : \
++ componentsConf.cmi
componentsConf.cmi :
- discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi
++discrimination_tree.cmx : \
++ trie.cmx \
++ hExtlib.cmx \
++ discrimination_tree.cmi
+discrimination_tree.cmi :
- graphvizPp.cmx : graphvizPp.cmi
++graphvizPp.cmx : \
++ graphvizPp.cmi
+graphvizPp.cmi :
- hExtlib.cmx : hExtlib.cmi
++hExtlib.cmx : \
++ hExtlib.cmi
hExtlib.cmi :
- hLog.cmx : hLog.cmi
++hLog.cmx : \
++ hLog.cmi
+hLog.cmi :
- hMarshal.cmx : hExtlib.cmx hMarshal.cmi
++hMarshal.cmx : \
++ hExtlib.cmx \
++ hMarshal.cmi
hMarshal.cmi :
- hTopoSort.cmx : hTopoSort.cmi
++hTopoSort.cmx : \
++ hTopoSort.cmi
+hTopoSort.cmi :
- patternMatcher.cmx : patternMatcher.cmi
++patternMatcher.cmx : \
++ patternMatcher.cmi
patternMatcher.cmi :
- trie.cmx : trie.cmi
-hLog.cmi :
++trie.cmx : \
++ trie.cmi
trie.cmi :
-discrimination_tree.cmi :
-hTopoSort.cmi :
-graphvizPp.cmi :
-componentsConf.cmo : componentsConf.cmi
-componentsConf.cmx : componentsConf.cmi
-hExtlib.cmo : hExtlib.cmi
-hExtlib.cmx : hExtlib.cmi
-hMarshal.cmo : hExtlib.cmi hMarshal.cmi
-hMarshal.cmx : hExtlib.cmx hMarshal.cmi
-patternMatcher.cmo : patternMatcher.cmi
-patternMatcher.cmx : patternMatcher.cmi
-hLog.cmo : hLog.cmi
-hLog.cmx : hLog.cmi
-trie.cmo : trie.cmi
-trie.cmx : trie.cmi
-discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi
-discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi
-hTopoSort.cmo : hTopoSort.cmi
-hTopoSort.cmx : hTopoSort.cmi
-graphvizPp.cmo : graphvizPp.cmi
-graphvizPp.cmx : graphvizPp.cmi
- http_getter.cmo : http_getter_wget.cmi http_getter_types.cmo \
- http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \
- http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \
-http_getter_wget.cmi :
++http_getter.cmo : \
++ http_getter_wget.cmi \
++ http_getter_types.cmo \
++ http_getter_storage.cmi \
++ http_getter_misc.cmi \
++ http_getter_logger.cmi \
++ http_getter_env.cmi \
++ http_getter_const.cmi \
++ http_getter_common.cmi \
+ http_getter.cmi
- http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \
- http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \
- http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \
++http_getter.cmx : \
++ http_getter_wget.cmx \
++ http_getter_types.cmx \
++ http_getter_storage.cmx \
++ http_getter_misc.cmx \
++ http_getter_logger.cmx \
++ http_getter_env.cmx \
++ http_getter_const.cmx \
++ http_getter_common.cmx \
+ http_getter.cmi
- http_getter.cmi : http_getter_types.cmo
- http_getter_common.cmo : http_getter_types.cmo http_getter_misc.cmi \
- http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi
- http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi
- http_getter_common.cmi : http_getter_types.cmo
- http_getter_const.cmo : http_getter_const.cmi
- http_getter_const.cmx : http_getter_const.cmi
++http_getter.cmi : \
++ http_getter_types.cmo
++http_getter_common.cmo : \
++ http_getter_types.cmo \
++ http_getter_misc.cmi \
++ http_getter_logger.cmi \
++ http_getter_env.cmi \
++ http_getter_common.cmi
++http_getter_common.cmx : \
++ http_getter_types.cmx \
++ http_getter_misc.cmx \
++ http_getter_logger.cmx \
++ http_getter_env.cmx \
++ http_getter_common.cmi
++http_getter_common.cmi : \
++ http_getter_types.cmo
++http_getter_const.cmo : \
++ http_getter_const.cmi
++http_getter_const.cmx : \
++ http_getter_const.cmi
+http_getter_const.cmi :
- http_getter_env.cmo : http_getter_types.cmo http_getter_misc.cmi \
- http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi
- http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi
- http_getter_env.cmi : http_getter_types.cmo
- http_getter_logger.cmo : http_getter_logger.cmi
- http_getter_logger.cmx : http_getter_logger.cmi
++http_getter_env.cmo : \
++ http_getter_types.cmo \
++ http_getter_misc.cmi \
++ http_getter_logger.cmi \
++ http_getter_const.cmi \
++ http_getter_env.cmi
++http_getter_env.cmx : \
++ http_getter_types.cmx \
++ http_getter_misc.cmx \
++ http_getter_logger.cmx \
++ http_getter_const.cmx \
++ http_getter_env.cmi
++http_getter_env.cmi : \
++ http_getter_types.cmo
++http_getter_logger.cmo : \
++ http_getter_logger.cmi
++http_getter_logger.cmx : \
++ http_getter_logger.cmi
http_getter_logger.cmi :
- http_getter_misc.cmo : http_getter_logger.cmi http_getter_misc.cmi
- http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi
++http_getter_misc.cmo : \
++ http_getter_logger.cmi \
++ http_getter_misc.cmi
++http_getter_misc.cmx : \
++ http_getter_logger.cmx \
++ http_getter_misc.cmi
http_getter_misc.cmi :
- http_getter_storage.cmo : http_getter_wget.cmi http_getter_types.cmo \
- http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi
- http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \
- http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi
-http_getter_const.cmi :
-http_getter_env.cmi : http_getter_types.cmo
++http_getter_storage.cmo : \
++ http_getter_wget.cmi \
++ http_getter_types.cmo \
++ http_getter_misc.cmi \
++ http_getter_env.cmi \
++ http_getter_storage.cmi
++http_getter_storage.cmx : \
++ http_getter_wget.cmx \
++ http_getter_types.cmx \
++ http_getter_misc.cmx \
++ http_getter_env.cmx \
++ http_getter_storage.cmi
http_getter_storage.cmi :
-http_getter_common.cmi : http_getter_types.cmo
-http_getter.cmi : http_getter_types.cmo
http_getter_types.cmo :
http_getter_types.cmx :
--http_getter_wget.cmo : http_getter_types.cmo http_getter_wget.cmi
--http_getter_wget.cmx : http_getter_types.cmx http_getter_wget.cmi
-http_getter_logger.cmo : http_getter_logger.cmi
-http_getter_logger.cmx : http_getter_logger.cmi
-http_getter_misc.cmo : http_getter_logger.cmi http_getter_misc.cmi
-http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi
-http_getter_const.cmo : http_getter_const.cmi
-http_getter_const.cmx : http_getter_const.cmi
-http_getter_env.cmo : http_getter_types.cmo http_getter_misc.cmi \
- http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi
-http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi
-http_getter_storage.cmo : http_getter_wget.cmi http_getter_types.cmo \
- http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi
-http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \
- http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi
-http_getter_common.cmo : http_getter_types.cmo http_getter_misc.cmi \
- http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi
-http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi
-http_getter.cmo : http_getter_wget.cmi http_getter_types.cmo \
- http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \
- http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \
- http_getter.cmi
-http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \
- http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \
- http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \
- http_getter.cmi
++http_getter_wget.cmo : \
++ http_getter_types.cmo \
++ http_getter_wget.cmi
++http_getter_wget.cmx : \
++ http_getter_types.cmx \
++ http_getter_wget.cmi
+http_getter_wget.cmi :
- http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \
- http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \
- http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \
-http_getter_wget.cmi :
++http_getter.cmx : \
++ http_getter_wget.cmx \
++ http_getter_types.cmx \
++ http_getter_storage.cmx \
++ http_getter_misc.cmx \
++ http_getter_logger.cmx \
++ http_getter_env.cmx \
++ http_getter_const.cmx \
++ http_getter_common.cmx \
+ http_getter.cmi
- http_getter.cmi : http_getter_types.cmx
- http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi
- http_getter_common.cmi : http_getter_types.cmx
- http_getter_const.cmx : http_getter_const.cmi
++http_getter.cmi : \
++ http_getter_types.cmx
++http_getter_common.cmx : \
++ http_getter_types.cmx \
++ http_getter_misc.cmx \
++ http_getter_logger.cmx \
++ http_getter_env.cmx \
++ http_getter_common.cmi
++http_getter_common.cmi : \
++ http_getter_types.cmx
++http_getter_const.cmx : \
++ http_getter_const.cmi
+http_getter_const.cmi :
- http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi
- http_getter_env.cmi : http_getter_types.cmx
- http_getter_logger.cmx : http_getter_logger.cmi
++http_getter_env.cmx : \
++ http_getter_types.cmx \
++ http_getter_misc.cmx \
++ http_getter_logger.cmx \
++ http_getter_const.cmx \
++ http_getter_env.cmi
++http_getter_env.cmi : \
++ http_getter_types.cmx
++http_getter_logger.cmx : \
++ http_getter_logger.cmi
http_getter_logger.cmi :
- http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi
++http_getter_misc.cmx : \
++ http_getter_logger.cmx \
++ http_getter_misc.cmi
http_getter_misc.cmi :
- http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \
- http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi
-http_getter_const.cmi :
-http_getter_env.cmi : http_getter_types.cmx
++http_getter_storage.cmx : \
++ http_getter_wget.cmx \
++ http_getter_types.cmx \
++ http_getter_misc.cmx \
++ http_getter_env.cmx \
++ http_getter_storage.cmi
http_getter_storage.cmi :
-http_getter_common.cmi : http_getter_types.cmx
-http_getter.cmi : http_getter_types.cmx
-http_getter_types.cmo :
http_getter_types.cmx :
-http_getter_wget.cmo : http_getter_types.cmx http_getter_wget.cmi
--http_getter_wget.cmx : http_getter_types.cmx http_getter_wget.cmi
-http_getter_logger.cmo : http_getter_logger.cmi
-http_getter_logger.cmx : http_getter_logger.cmi
-http_getter_misc.cmo : http_getter_logger.cmi http_getter_misc.cmi
-http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi
-http_getter_const.cmo : http_getter_const.cmi
-http_getter_const.cmx : http_getter_const.cmi
-http_getter_env.cmo : http_getter_types.cmx http_getter_misc.cmi \
- http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi
-http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi
-http_getter_storage.cmo : http_getter_wget.cmi http_getter_types.cmx \
- http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi
-http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \
- http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi
-http_getter_common.cmo : http_getter_types.cmx http_getter_misc.cmi \
- http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi
-http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi
-http_getter.cmo : http_getter_wget.cmi http_getter_types.cmx \
- http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \
- http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \
- http_getter.cmi
-http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \
- http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \
- http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \
- http_getter.cmi
++http_getter_wget.cmx : \
++ http_getter_types.cmx \
++ http_getter_wget.cmi
+http_getter_wget.cmi :
-grafiteAstPp.cmi : grafiteAst.cmo
grafiteAst.cmo :
grafiteAst.cmx :
--grafiteAstPp.cmo : grafiteAst.cmo grafiteAstPp.cmi
--grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi
- grafiteAstPp.cmi : grafiteAst.cmo
++grafiteAstPp.cmo : \
++ grafiteAst.cmo \
++ grafiteAstPp.cmi
++grafiteAstPp.cmx : \
++ grafiteAst.cmx \
++ grafiteAstPp.cmi
++grafiteAstPp.cmi : \
++ grafiteAst.cmo
-grafiteAstPp.cmi : grafiteAst.cmx
-grafiteAst.cmo :
grafiteAst.cmx :
-grafiteAstPp.cmo : grafiteAst.cmx grafiteAstPp.cmi
--grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi
- grafiteAstPp.cmi : grafiteAst.cmx
++grafiteAstPp.cmx : \
++ grafiteAst.cmx \
++ grafiteAstPp.cmi
++grafiteAstPp.cmi : \
++ grafiteAst.cmx
(* 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
| NApply (_,t) -> "@" ^ NotationPp.pp_term status t
- | NSmartApply (_,t) -> "fixme"
+ | NSmartApply (_,_t) -> "fixme"
| NAuto (_,(None,flgs)) ->
"nautobatch" ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
"nautobatch" ^ " by " ^
(String.concat "," (List.map (NotationPp.pp_term status) l)) ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
- | NCases (_,what,where) -> "ncases " ^ NotationPp.pp_term status what ^
+ | NCases (_,what,_where) -> "ncases " ^ NotationPp.pp_term status what ^
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NConstructor (_,None,l) -> "@ " ^
String.concat " " (List.map (NotationPp.pp_term status) l)
| NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
String.concat " " (List.map (NotationPp.pp_term status) l)
| NCase1 (_,n) -> "*" ^ n ^ ":"
- | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^
- | NChange (_,what,wwhat) -> "nchange " ^ "...to be implemented..." ^
++ | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^
" with " ^ NotationPp.pp_term status wwhat
| NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t
(*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t
| NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *)
| NClear (_,l) -> "nclear " ^ String.concat " " l
- | NDestruct (_,_dom,_skip) -> "ndestruct ..."
- | NDestruct (_,dom,skip) -> "ndestruct ..."
- | NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term status what ^
++ | NDestruct (_,_dom,_skip) -> "ndestruct ..."
+ | NElim (_,what,_where) -> "nelim " ^ NotationPp.pp_term status what ^
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
| NIntros (_,l) -> "#" ^ String.concat " " l
- | NInversion (_,what,where) -> "ninversion " ^ NotationPp.pp_term status what ^
+ | NInversion (_,what,_where) -> "ninversion " ^ NotationPp.pp_term status what ^
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NLApply (_,t) -> "lapply " ^ NotationPp.pp_term status t
| NRewrite (_,dir,n,where) -> "nrewrite " ^
| NPosbyname (_, s) -> s ^ ":"
| NWildcard _ -> "*:"
| NMerge _ -> "]"
- | NFocus (_,l) ->
- Printf.sprintf "focus %s"
+ | NFocus (_,l) ->
+ Printf.sprintf "focus %s"
(String.concat " " (List.map string_of_int l))
| NUnfocus _ -> "unfocus"
| NSkip _ -> "skip"
| NTry (_,tac) -> "ntry " ^ pp_ntactic status ~map_unicode_to_tex tac
| NAssumption _ -> "nassumption"
- | NBlock (_,l) ->
+ | NBlock (_,l) ->
"(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")"
| NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t
+ | Assume (_, ident, term) -> "assume " ^ ident ^ ":(" ^ (NotationPp.pp_term status term) ^ ")"
+ | Suppose (_,term,ident) -> "suppose (" ^ (NotationPp.pp_term status term) ^ ") (" ^ ident ^ ") "
+ | By_just_we_proved (_, just, term1, ident) -> pp_just status just ^ " we proved (" ^
+ (NotationPp.pp_term status term1) ^ ")" ^ (match ident with
+ None -> "" | Some ident -> "(" ^ident^ ")")
+ | We_need_to_prove (_,term,ident) -> "we need to prove (" ^ (NotationPp.pp_term status term) ^ ") " ^
+ (match ident with None -> "" | Some id -> "(" ^ id ^ ")")
+ | BetaRewritingStep (_,t) -> "that is equivalent to (" ^ (NotationPp.pp_term status t) ^ ")"
+ | Bydone (_, just) -> pp_just status just ^ "done"
+ | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ": ("
+ ^ (NotationPp.pp_term status term) ^ ") such that (" ^ (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ")"
+ | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ " we have (" ^
+ (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ") " ^ "and (" ^ (NotationPp.pp_term status
+ term2)
+ ^ ") (" ^ ident2 ^ ")"
+ | Thesisbecomes (_, t) -> "the thesis becomes (" ^ (NotationPp.pp_term status t) ^ ")"
+ | RewritingStep (_, rhs, just, cont) ->
+ "= (" ^
+ (NotationPp.pp_term status rhs) ^ ")" ^
+ (match just with
+ | `Auto params -> let s = pp_auto_params params status in
+ if s <> "" then " by " ^ s
+ else ""
+ | `Term t -> " exact (" ^ (NotationPp.pp_term status t) ^ ")"
+ | `Proof -> " proof"
+ | `SolveWith t -> " using (" ^ (NotationPp.pp_term status t) ^ ")"
+ )
+ ^ (if cont then " done" else "")
+ | Obtain (_,id,t1) -> "obtain (" ^ id ^ ")" ^ " (" ^ (NotationPp.pp_term status t1) ^ ")"
+ | Conclude (_,t1) -> "conclude (" ^ (NotationPp.pp_term status t1) ^ ")"
+ | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on (" ^ NotationPp.pp_term
+ status term ^ ") to prove (" ^ NotationPp.pp_term status term1 ^ ")"
+ | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on (" ^
+ NotationPp.pp_term status term ^ ") to prove (" ^ NotationPp.pp_term status term1 ^ ")"
+ | Byinduction (_, term, ident) -> "by induction hypothesis we know (" ^ NotationPp.pp_term status
+ term ^ ") (" ^ ident ^ ")"
+ | Case (_, id, args) ->
+ "case " ^ id ^
+ String.concat " "
+ (List.map (function (id,term) -> "(" ^ id ^ ": (" ^ NotationPp.pp_term status term ^ "))")
+ args)
++ | PrintStack _ -> "print_stack"
;;
let pp_nmacro status = function
| NCheck (_, term) -> Printf.sprintf "ncheck %s" (NotationPp.pp_term status term)
| Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
+ | NAutoInteractive _
+ | NIntroGuess _ -> assert false (* TODO *)
;;
let pp_l1_pattern = NotationPp.pp_term
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"
let pp_argument_pattern = function
| NotationPt.IdentArg (eta_depth, name) ->
let eta_buf = Buffer.create 5 in
- for i = 1 to eta_depth do
+ for _i = 1 to eta_depth do
Buffer.add_string eta_buf "\\eta."
done;
sprintf "%s%s" (Buffer.contents eta_buf) name
- let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
+ let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
sprintf "interpretation \"%s\" '%s %s = %s."
dsc symbol
(String.concat " " (List.map pp_argument_pattern arg_patterns))
(NotationPp.pp_cic_appl_pattern cic_appl_pattern)
-
+
let pp_dir_opt = function
| None -> ""
| Some `LeftToRight -> "> "
| Some `RightToLeft -> "< "
- let pp_notation status dir_opt l1_pattern assoc prec l2_pattern =
+ let pp_notation status dir_opt l1_pattern assoc prec l2_pattern =
sprintf "notation %s\"%s\" %s %s for %s."
(pp_dir_opt dir_opt)
(pp_l1_pattern status l1_pattern)
(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
-grafiteTypes.cmi :
-nCicCoercDeclaration.cmi : grafiteTypes.cmi
-grafiteEngine.cmi : grafiteTypes.cmi
-grafiteTypes.cmo : grafiteTypes.cmi
-grafiteTypes.cmx : grafiteTypes.cmi
-nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi
-nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi
--grafiteEngine.cmo : nCicCoercDeclaration.cmi grafiteTypes.cmi \
++grafiteEngine.cmo : \
++ nCicCoercDeclaration.cmi \
++ grafiteTypes.cmi \
grafiteEngine.cmi
--grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \
++grafiteEngine.cmx : \
++ nCicCoercDeclaration.cmx \
++ grafiteTypes.cmx \
grafiteEngine.cmi
- grafiteEngine.cmi : grafiteTypes.cmi
- grafiteTypes.cmo : grafiteTypes.cmi
- grafiteTypes.cmx : grafiteTypes.cmi
++grafiteEngine.cmi : \
++ grafiteTypes.cmi
++grafiteTypes.cmo : \
++ grafiteTypes.cmi
++grafiteTypes.cmx : \
++ grafiteTypes.cmi
+grafiteTypes.cmi :
- nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi
- nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi
- nCicCoercDeclaration.cmi : grafiteTypes.cmi
++nCicCoercDeclaration.cmo : \
++ grafiteTypes.cmi \
++ nCicCoercDeclaration.cmi
++nCicCoercDeclaration.cmx : \
++ grafiteTypes.cmx \
++ nCicCoercDeclaration.cmi
++nCicCoercDeclaration.cmi : \
++ grafiteTypes.cmi
-grafiteTypes.cmi :
-nCicCoercDeclaration.cmi : grafiteTypes.cmi
-grafiteEngine.cmi : grafiteTypes.cmi
-grafiteTypes.cmo : grafiteTypes.cmi
-grafiteTypes.cmx : grafiteTypes.cmi
-nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi
-nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi
-grafiteEngine.cmo : nCicCoercDeclaration.cmi grafiteTypes.cmi \
- grafiteEngine.cmi
--grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \
++grafiteEngine.cmx : \
++ nCicCoercDeclaration.cmx \
++ grafiteTypes.cmx \
grafiteEngine.cmi
- grafiteEngine.cmi : grafiteTypes.cmi
- grafiteTypes.cmx : grafiteTypes.cmi
++grafiteEngine.cmi : \
++ grafiteTypes.cmi
++grafiteTypes.cmx : \
++ grafiteTypes.cmi
+grafiteTypes.cmi :
- nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi
- nCicCoercDeclaration.cmi : grafiteTypes.cmi
++nCicCoercDeclaration.cmx : \
++ grafiteTypes.cmx \
++ nCicCoercDeclaration.cmi
++nCicCoercDeclaration.cmi : \
++ grafiteTypes.cmi
let inject_unification_hint =
let basic_eval_unification_hint (t,n)
- ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~refresh_uri_in_universe:_ ~refresh_uri_in_term ~refresh_uri_in_reference:_
~alias_only status
=
if not alias_only then
let inject_interpretation =
let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
- ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_
~alias_only
=
let rec refresh =
;;
let inject_alias =
- let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term
- ~refresh_uri_in_reference ~alias_only =
+ let basic_eval_alias (mode,diff) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_
+ ~refresh_uri_in_reference:_ ~alias_only:_ =
basic_eval_alias (mode,diff)
in
GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
let inject_input_notation =
let basic_eval_input_notation (l1,l2)
- ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~refresh_uri_in_universe:_ ~refresh_uri_in_term ~refresh_uri_in_reference
~alias_only status
=
if not alias_only then
let inject_output_notation =
let basic_eval_output_notation (l1,l2)
- ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~refresh_uri_in_universe:_ ~refresh_uri_in_term ~refresh_uri_in_reference
~alias_only status
=
if not alias_only then
;;
let record_index_obj =
- let aux l ~refresh_uri_in_universe
- ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status
+ let aux l ~refresh_uri_in_universe:_
+ ~refresh_uri_in_term ~refresh_uri_in_reference:_ ~alias_only status
=
let refresh_uri_in_term = refresh_uri_in_term (status:>NCic.status) in
if not alias_only then
let inject_extract_obj =
let basic_extract_obj info
- ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
- ~alias_only status
+ ~refresh_uri_in_universe:__ ~refresh_uri_in_term:_ ~refresh_uri_in_reference
+ ~alias_only:_ status
=
let info= NCicExtraction.refresh_uri_in_info ~refresh_uri_in_reference info in
status#set_extraction_db
let inject_extract_ocaml_obj =
let basic_extract_ocaml_obj info
- ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
- ~alias_only status
+ ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference
+ ~alias_only:_ status
=
let info= OcamlExtractionTable.refresh_uri_in_info ~refresh_uri_in_reference ~refresh_uri:NCicLibrary.refresh_uri info in
status#set_ocaml_extraction_db
let record_index_eq =
let basic_index_eq uri
- ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_
~alias_only status
= if not alias_only then index_eq false (NCicLibrary.refresh_uri uri) status
else
let inject_constraint =
let basic_eval_add_constraint (acyclic,u1,u2)
- ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~refresh_uri_in_universe ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_
~alias_only status
=
if not alias_only then
;;
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))
- `Term t -> just_to_tacstatus_just just text prefix_len
- | `Auto params -> just_to_tacstatus_just just text prefix_len
+ |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 *)
;;
let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
match cmd with
- | GrafiteAst.Include (loc, mode, fname) ->
+ | GrafiteAst.Include (_loc, mode, fname) ->
let _root, baseuri, fullpath, _rrelpath =
Librarian.baseuri_of_script ~include_paths fname in
let baseuri = NUri.uri_of_string baseuri in
~alias_only ~baseuri ~fname:fullpath status in
OcamlExtraction.print_open status
(NCicLibrary.get_transitively_included status)
- | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
+ | GrafiteAst.UnificationHint (_loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NCoercion (loc, name, compose, None) ->
let status, t, ty, source, target =
let o_t = NotationPt.Ident (name,None) in
GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target))
in
eval_ncommand ~include_paths opts status (text,prefix_len,cmd)
- | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) ->
+ | GrafiteAst.NCoercion (_loc, name, compose, Some (t, ty, source, target)) ->
let status, composites =
NCicCoercDeclaration.eval_ncoercion status name compose t ty source
target in
let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
eval_alias status (mode,aliases)
- | GrafiteAst.NQed (loc,index) ->
+ | GrafiteAst.NQed (_loc,index) ->
if status#ng_mode <> `ProofMode then
raise (GrafiteTypes.Command_error "Not in proof mode")
else
- let uri,height,menv,subst,obj_kind = status#obj in
+ let uri,_height,menv,subst,obj_kind = status#obj in
if menv <> [] then
raise
(GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
let status = match nobj with
NCic.Inductive (is_ind,leftno,itl,_) ->
List.fold_left (fun status it ->
- (let _,ind_name,ty,cl = it in
+ (let _,ind_name,_ty,_cl = it in
List.fold_left
(fun status outsort ->
let status = status#set_ng_mode `ProofMode in
| _ -> status
in
let status = match nobj with
- NCic.Inductive (is_ind,leftno,itl,_) ->
+ NCic.Inductive (_is_ind,leftno,itl,_) ->
(* first leibniz *)
let status' = List.fold_left
(fun status it ->
- let _,ind_name,ty,cl = it in
+ let _,ind_name,_ty,_cl = it in
let status = status#set_ng_mode `ProofMode in
try
(let status,invobj =
(* then JMeq *)
List.fold_left
(fun status it ->
- let _,ind_name,ty,cl = it in
+ let _,ind_name,_ty,_cl = it in
let status = status#set_ng_mode `ProofMode in
try
(let status,invobj =
exn ->
NCicLibrary.time_travel old_status;
raise exn)
- | GrafiteAst.NCopy (log,tgt,src_uri, map) ->
+ | GrafiteAst.NCopy (_loc,tgt,src_uri, map) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
else
let status = subst_metasenv_and_fix_names status in
let status = status#set_ng_mode `ProofMode in
eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
- | GrafiteAst.NObj (loc,obj,index) ->
+ | GrafiteAst.NObj (_loc,obj,index) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
else
let status,obj =
GrafiteDisambiguate.disambiguate_nobj status
~baseuri:status#baseuri (text,prefix_len,obj) in
- let uri,height,nmenv,nsubst,nobj = obj in
+ let _uri,_height,nmenv,_nsubst,_nobj = obj in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let status = status#set_obj obj in
let status = status#set_stack ninitial_stack in
eval_ncommand ~include_paths opts status
("",0,GrafiteAst.NQed(Stdpp.dummy_loc,index))
| _ -> status)
- | GrafiteAst.NDiscriminator (loc, indty) ->
+ | GrafiteAst.NDiscriminator (_loc, indty) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
else
let status = status#set_ng_mode `ProofMode in
- let metasenv,subst,status,indty =
+ let _metasenv,_subst,status,indty =
GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] [] (text,prefix_len,indty) in
let indtyno, (_,_,tys,_,_),leftno = match indty with
NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
[] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
| _ -> prerr_endline ("Discriminator: non empty metasenv");
status)
- | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
+ | GrafiteAst.NInverter (_loc, name, indty, selection, sort) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
else
"ninverter: found target %s, which is not a sort"
(status#ppterm ~metasenv ~subst ~context:[] sort))) in
let status = status#set_ng_mode `ProofMode in
- let metasenv,subst,status,indty =
+ let _metasenv,_subst,status,indty =
GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] subst
(text,prefix_len,indty) in
let indtyno,(_,leftno,tys,_,_) =
eval_ncommand ~include_paths opts status
("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
| _ -> assert false)
- | GrafiteAst.NUnivConstraint (loc,acyclic,u1,u2) ->
+ | GrafiteAst.NUnivConstraint (_loc,acyclic,u1,u2) ->
eval_add_constraint status acyclic [`Type,u1] [`Type,u2]
(* ex lexicon commands *)
- | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
+ | GrafiteAst.Interpretation (_loc, dsc, (symbol, args), cic_appl_pattern) ->
let cic_appl_pattern =
GrafiteDisambiguate.disambiguate_cic_appl_pattern status args
cic_appl_pattern
in
eval_interpretation status (dsc,(symbol, args),cic_appl_pattern)
- | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) ->
+ | GrafiteAst.Notation (_loc, dir, l1, associativity, precedence, l2) ->
let l1 =
CicNotationParser.check_l1_pattern
l1 (dir = Some `RightToLeft) precedence associativity
in
if dir <> Some `LeftToRight then eval_output_notation status (l1,l2)
else status
- | GrafiteAst.Alias (loc, spec) ->
+ | GrafiteAst.Alias (_loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
code in DisambiguatePp *)
match spec with
- | GrafiteAst.Ident_alias (id,uri) ->
+ | GrafiteAst.Ident_alias (id,_uri) ->
[DisambiguateTypes.Id id,spec]
- | GrafiteAst.Symbol_alias (symb, instance, desc) ->
+ | GrafiteAst.Symbol_alias (symb, instance, _desc) ->
[DisambiguateTypes.Symbol (symb,instance),spec]
- | GrafiteAst.Number_alias (instance,desc) ->
+ | GrafiteAst.Number_alias (instance,_desc) ->
[DisambiguateTypes.Num instance,spec]
in
let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
eval_alias status (mode,diff)
;;
-let eval_comment opts status (text,prefix_len,c) = status
+let eval_comment _opts status (_text,_prefix_len,_c) = status
let rec eval_executable ~include_paths opts status (text,prefix_len,ex) =
match ex with
- grafiteParser.cmo : grafiteParser.cmi
- grafiteParser.cmx : grafiteParser.cmi
++grafiteParser.cmo : \
++ grafiteParser.cmi
++grafiteParser.cmx : \
++ grafiteParser.cmi
grafiteParser.cmi :
-print_grammar.cmi : grafiteParser.cmi
-grafiteParser.cmo : grafiteParser.cmi
-grafiteParser.cmx : grafiteParser.cmi
--print_grammar.cmo : print_grammar.cmi
--print_grammar.cmx : print_grammar.cmi
- print_grammar.cmi : grafiteParser.cmi
++print_grammar.cmo : \
++ print_grammar.cmi
++print_grammar.cmx : \
++ print_grammar.cmi
++print_grammar.cmi : \
++ grafiteParser.cmi
- grafiteParser.cmx : grafiteParser.cmi
++grafiteParser.cmx : \
++ grafiteParser.cmi
grafiteParser.cmi :
- print_grammar.cmx : print_grammar.cmi
--print_grammar.cmi : grafiteParser.cmi
-grafiteParser.cmo : grafiteParser.cmi
-grafiteParser.cmx : grafiteParser.cmi
-print_grammar.cmo : print_grammar.cmi
-print_grammar.cmx : print_grammar.cmi
++print_grammar.cmx : \
++ print_grammar.cmi
++print_grammar.cmi : \
++ grafiteParser.cmi
- librarian.cmo : librarian.cmi
- librarian.cmx : librarian.cmi
++librarian.cmo : \
++ librarian.cmi
++librarian.cmx : \
++ librarian.cmi
librarian.cmi :
- libraryClean.cmo : libraryClean.cmi
- libraryClean.cmx : libraryClean.cmi
-libraryMisc.cmi :
++libraryClean.cmo : \
++ libraryClean.cmi
++libraryClean.cmx : \
++ libraryClean.cmi
libraryClean.cmi :
-librarian.cmo : librarian.cmi
-librarian.cmx : librarian.cmi
--libraryMisc.cmo : libraryMisc.cmi
--libraryMisc.cmx : libraryMisc.cmi
-libraryClean.cmo : libraryClean.cmi
-libraryClean.cmx : libraryClean.cmi
++libraryMisc.cmo : \
++ libraryMisc.cmi
++libraryMisc.cmx : \
++ libraryMisc.cmi
+libraryMisc.cmi :
- librarian.cmx : librarian.cmi
++librarian.cmx : \
++ librarian.cmi
librarian.cmi :
- libraryClean.cmx : libraryClean.cmi
-libraryMisc.cmi :
++libraryClean.cmx : \
++ libraryClean.cmi
libraryClean.cmi :
-librarian.cmo : librarian.cmi
-librarian.cmx : librarian.cmi
-libraryMisc.cmo : libraryMisc.cmi
--libraryMisc.cmx : libraryMisc.cmi
-libraryClean.cmo : libraryClean.cmi
-libraryClean.cmx : libraryClean.cmi
++libraryMisc.cmx : \
++ libraryMisc.cmi
+libraryMisc.cmi :
- helmLogger.cmo : helmLogger.cmi
- helmLogger.cmx : helmLogger.cmi
++helmLogger.cmo : \
++ helmLogger.cmi
++helmLogger.cmx : \
++ helmLogger.cmi
helmLogger.cmi :
-helmLogger.cmo : helmLogger.cmi
-helmLogger.cmx : helmLogger.cmi
- helmLogger.cmx : helmLogger.cmi
++helmLogger.cmx : \
++ helmLogger.cmi
helmLogger.cmi :
-helmLogger.cmo : helmLogger.cmi
-helmLogger.cmx : helmLogger.cmi
- interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi
- interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
-ncic2astMatcher.cmi :
++interpretations.cmo : \
++ ncic2astMatcher.cmi \
++ interpretations.cmi
++interpretations.cmx : \
++ ncic2astMatcher.cmx \
++ interpretations.cmi
interpretations.cmi :
--ncic2astMatcher.cmo : ncic2astMatcher.cmi
--ncic2astMatcher.cmx : ncic2astMatcher.cmi
-interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi
-interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
++ncic2astMatcher.cmo : \
++ ncic2astMatcher.cmi
++ncic2astMatcher.cmx : \
++ ncic2astMatcher.cmi
+ncic2astMatcher.cmi :
- interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
-ncic2astMatcher.cmi :
++interpretations.cmx : \
++ ncic2astMatcher.cmx \
++ interpretations.cmi
interpretations.cmi :
-ncic2astMatcher.cmo : ncic2astMatcher.cmi
--ncic2astMatcher.cmx : ncic2astMatcher.cmi
-interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi
-interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
++ncic2astMatcher.cmx : \
++ ncic2astMatcher.cmi
+ncic2astMatcher.cmi :
- disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi
- disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi
-nnumber_notation.cmi :
++disambiguateChoices.cmo : \
++ nnumber_notation.cmi \
++ disambiguateChoices.cmi
++disambiguateChoices.cmx : \
++ nnumber_notation.cmx \
++ disambiguateChoices.cmi
disambiguateChoices.cmi :
-nCicDisambiguate.cmi :
-grafiteDisambiguate.cmi :
-nnumber_notation.cmo : nnumber_notation.cmi
-nnumber_notation.cmx : nnumber_notation.cmi
-disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi
-disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi
-nCicDisambiguate.cmo : nCicDisambiguate.cmi
-nCicDisambiguate.cmx : nCicDisambiguate.cmi
--grafiteDisambiguate.cmo : nCicDisambiguate.cmi disambiguateChoices.cmi \
++grafiteDisambiguate.cmo : \
++ nCicDisambiguate.cmi \
++ disambiguateChoices.cmi \
grafiteDisambiguate.cmi
--grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \
++grafiteDisambiguate.cmx : \
++ nCicDisambiguate.cmx \
++ disambiguateChoices.cmx \
grafiteDisambiguate.cmi
- nCicDisambiguate.cmo : nCicDisambiguate.cmi
- nCicDisambiguate.cmx : nCicDisambiguate.cmi
+grafiteDisambiguate.cmi :
- nnumber_notation.cmo : nnumber_notation.cmi
- nnumber_notation.cmx : nnumber_notation.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.cmi :
- disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi
-nnumber_notation.cmi :
++disambiguateChoices.cmx : \
++ nnumber_notation.cmx \
++ disambiguateChoices.cmi
disambiguateChoices.cmi :
-nCicDisambiguate.cmi :
-grafiteDisambiguate.cmi :
-nnumber_notation.cmo : nnumber_notation.cmi
-nnumber_notation.cmx : nnumber_notation.cmi
-disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi
-disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi
-nCicDisambiguate.cmo : nCicDisambiguate.cmi
-nCicDisambiguate.cmx : nCicDisambiguate.cmi
-grafiteDisambiguate.cmo : nCicDisambiguate.cmi disambiguateChoices.cmi \
- grafiteDisambiguate.cmi
--grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \
++grafiteDisambiguate.cmx : \
++ nCicDisambiguate.cmx \
++ disambiguateChoices.cmx \
grafiteDisambiguate.cmi
- nCicDisambiguate.cmx : nCicDisambiguate.cmi
+grafiteDisambiguate.cmi :
- nnumber_notation.cmx : nnumber_notation.cmi
++nCicDisambiguate.cmx : \
++ nCicDisambiguate.cmi
+nCicDisambiguate.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
-nCicExtraction.cmi :
-coq.cmi :
-ocamlExtractionTable.cmi : miniml.cmo coq.cmi
-mlutil.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
-common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi
-extraction.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
-ocaml.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
-ocamlExtraction.cmi : ocamlExtractionTable.cmi
-miniml.cmo : coq.cmi
-miniml.cmx : coq.cmx
-nCicExtraction.cmo : nCicExtraction.cmi
-nCicExtraction.cmx : nCicExtraction.cmi
--coq.cmo : coq.cmi
--coq.cmx : coq.cmi
-ocamlExtractionTable.cmo : miniml.cmo coq.cmi ocamlExtractionTable.cmi
-ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi
-mlutil.cmo : ocamlExtractionTable.cmi miniml.cmo coq.cmi mlutil.cmi
-mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi
-common.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
++common.cmo : \
++ ocamlExtractionTable.cmi \
++ mlutil.cmi \
++ coq.cmi \
+ common.cmi
-common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
++common.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ coq.cmx \
+ common.cmi
-extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
- common.cmi extraction.cmi
-extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx extraction.cmi
-ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
- common.cmi ocaml.cmi
-ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx ocaml.cmi
-ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \
- coq.cmi ocamlExtraction.cmi
-ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \
- coq.cmx ocamlExtraction.cmi
++common.cmi : \
++ ocamlExtractionTable.cmi \
++ coq.cmi
++coq.cmo : \
++ coq.cmi
++coq.cmx : \
++ coq.cmi
+coq.cmi :
- extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
- common.cmi extraction.cmi
- extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx extraction.cmi
- extraction.cmi : ocamlExtractionTable.cmi miniml.cmo
- miniml.cmo : coq.cmi
- miniml.cmx : coq.cmx
- mlutil.cmo : ocamlExtractionTable.cmi miniml.cmo coq.cmi mlutil.cmi
- mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi
- mlutil.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
- nCicExtraction.cmo : nCicExtraction.cmi
- nCicExtraction.cmx : nCicExtraction.cmi
++extraction.cmo : \
++ ocamlExtractionTable.cmi \
++ mlutil.cmi \
++ miniml.cmo \
++ coq.cmi \
++ common.cmi \
++ extraction.cmi
++extraction.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ miniml.cmx \
++ coq.cmx \
++ common.cmx \
++ extraction.cmi
++extraction.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmo
++miniml.cmo : \
++ coq.cmi
++miniml.cmx : \
++ coq.cmx
++mlutil.cmo : \
++ ocamlExtractionTable.cmi \
++ miniml.cmo \
++ coq.cmi \
++ mlutil.cmi
++mlutil.cmx : \
++ ocamlExtractionTable.cmx \
++ miniml.cmx \
++ coq.cmx \
++ mlutil.cmi
++mlutil.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmo \
++ coq.cmi
++nCicExtraction.cmo : \
++ nCicExtraction.cmi
++nCicExtraction.cmx : \
++ nCicExtraction.cmi
+nCicExtraction.cmi :
- ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
- common.cmi ocaml.cmi
- ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx ocaml.cmi
- ocaml.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
- ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \
- coq.cmi ocamlExtraction.cmi
- ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \
- coq.cmx ocamlExtraction.cmi
- ocamlExtraction.cmi : ocamlExtractionTable.cmi
- ocamlExtractionTable.cmo : miniml.cmo coq.cmi ocamlExtractionTable.cmi
- ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi
- ocamlExtractionTable.cmi : miniml.cmo coq.cmi
++ocaml.cmo : \
++ ocamlExtractionTable.cmi \
++ mlutil.cmi \
++ miniml.cmo \
++ coq.cmi \
++ common.cmi \
++ ocaml.cmi
++ocaml.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ miniml.cmx \
++ coq.cmx \
++ common.cmx \
++ ocaml.cmi
++ocaml.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmo \
++ coq.cmi
++ocamlExtraction.cmo : \
++ ocamlExtractionTable.cmi \
++ ocaml.cmi \
++ extraction.cmi \
++ coq.cmi \
++ ocamlExtraction.cmi
++ocamlExtraction.cmx : \
++ ocamlExtractionTable.cmx \
++ ocaml.cmx \
++ extraction.cmx \
++ coq.cmx \
++ ocamlExtraction.cmi
++ocamlExtraction.cmi : \
++ ocamlExtractionTable.cmi
++ocamlExtractionTable.cmo : \
++ miniml.cmo \
++ coq.cmi \
++ ocamlExtractionTable.cmi
++ocamlExtractionTable.cmx : \
++ miniml.cmx \
++ coq.cmx \
++ ocamlExtractionTable.cmi
++ocamlExtractionTable.cmi : \
++ miniml.cmo \
++ coq.cmi
- common.cmx : ocamlExtractionTable.cmx mlutil.cmx coq.cmx common.cmi
- common.cmi : ocamlExtractionTable.cmi coq.cmi
-nCicExtraction.cmi :
-coq.cmi :
-ocamlExtractionTable.cmi : miniml.cmx coq.cmi
-mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
-common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi
-extraction.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
-ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
-ocamlExtraction.cmi : ocamlExtractionTable.cmi
-miniml.cmo : coq.cmi
-miniml.cmx : coq.cmx
-nCicExtraction.cmo : nCicExtraction.cmi
-nCicExtraction.cmx : nCicExtraction.cmi
-coq.cmo : coq.cmi
--coq.cmx : coq.cmi
-ocamlExtractionTable.cmo : miniml.cmx coq.cmi ocamlExtractionTable.cmi
-ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi
-mlutil.cmo : ocamlExtractionTable.cmi miniml.cmx coq.cmi mlutil.cmi
-mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi
-common.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \
- common.cmi
-common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
++common.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ coq.cmx \
+ common.cmi
-extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \
- common.cmi extraction.cmi
-extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx extraction.cmi
-ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \
- common.cmi ocaml.cmi
-ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx ocaml.cmi
-ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \
- coq.cmi ocamlExtraction.cmi
-ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \
- coq.cmx ocamlExtraction.cmi
++common.cmi : \
++ ocamlExtractionTable.cmi \
++ coq.cmi
++coq.cmx : \
++ coq.cmi
+coq.cmi :
- extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx extraction.cmi
- extraction.cmi : ocamlExtractionTable.cmi miniml.cmx
- miniml.cmx : coq.cmx
- mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi
- mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
- nCicExtraction.cmx : nCicExtraction.cmi
++extraction.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ miniml.cmx \
++ coq.cmx \
++ common.cmx \
++ extraction.cmi
++extraction.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmx
++miniml.cmx : \
++ coq.cmx
++mlutil.cmx : \
++ ocamlExtractionTable.cmx \
++ miniml.cmx \
++ coq.cmx \
++ mlutil.cmi
++mlutil.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmx \
++ coq.cmi
++nCicExtraction.cmx : \
++ nCicExtraction.cmi
+nCicExtraction.cmi :
- ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx ocaml.cmi
- ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
- ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \
- coq.cmx ocamlExtraction.cmi
- ocamlExtraction.cmi : ocamlExtractionTable.cmi
- ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi
- ocamlExtractionTable.cmi : miniml.cmx coq.cmi
++ocaml.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ miniml.cmx \
++ coq.cmx \
++ common.cmx \
++ ocaml.cmi
++ocaml.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmx \
++ coq.cmi
++ocamlExtraction.cmx : \
++ ocamlExtractionTable.cmx \
++ ocaml.cmx \
++ extraction.cmx \
++ coq.cmx \
++ ocamlExtraction.cmi
++ocamlExtraction.cmi : \
++ ocamlExtractionTable.cmi
++ocamlExtractionTable.cmx : \
++ miniml.cmx \
++ coq.cmx \
++ ocamlExtractionTable.cmi
++ocamlExtractionTable.cmi : \
++ miniml.cmx \
++ coq.cmi
let clean_free mle =
let rem = ref Metaset.empty
and add = ref Metaset.empty in
- let clean m = match m.contents with
+ let clean m = match m.Miniml.contents with
| None -> ()
| Some u -> rem := Metaset.add m !rem; add := find_free !add u
in
(*s What are the type variables occurring in [t]. *)
-let intset_union_map_list f l =
- List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l
+(*let intset_union_map_list f l =
+ List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l*)
-let intset_union_map_array f a =
- Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a
+(*let intset_union_map_array f a =
+ Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a*)
-let rec type_listvar = function
+(*let rec type_listvar = function
| Tmeta {contents = Some t} -> type_listvar t
| Tvar i | Tvar' i -> Intset.singleton i
| Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b)
| Tglob (_,l) -> intset_union_map_list type_listvar l
- | _ -> Intset.empty
+ | _ -> Intset.empty*)
(*s From [a -> b -> c] to [[a;b],c]. *)
(*s Number of occurences of [Rel k] (resp. [Rel 1]) in [t]. *)
-let nb_occur_k k t =
+(*let nb_occur_k k t =
let cpt = ref 0 in
ast_iter_rel (fun i -> if i = k then incr cpt) t;
- !cpt
+ !cpt*)
-let nb_occur t = nb_occur_k 1 t
+(*let nb_occur t = nb_occur_k 1 t*)
(* Number of occurences of [Rel 1] in [t], with special treatment of match:
occurences in different branches aren't added, but we rather use max. *)
| 0 -> a
| n -> many_lams id (MLlam (id,a)) (pred n)
-let anonym_lams a n = many_lams anonymous a n
+(*let anonym_lams a n = many_lams anonymous a n*)
let anonym_tmp_lams a n = many_lams (Tmp anonymous_name) a n
let dummy_lams a n = many_lams Dummy a n
(*s Computes an eta-reduction. *)
-let eta_red e =
+(*let eta_red e =
let ids,t = collect_lams e in
let n = List.length ids in
if n = 0 then e
if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body)
then named_lams ids (ast_lift (-p) body)
else e
- | _ -> e
+ | _ -> e*)
(*s Computes all head linear beta-reductions possible in [(t a)].
Non-linear head beta-redex become let-in. *)
-let rec linear_beta_red a t = match a,t with
+(*let rec linear_beta_red a t = match a,t with
| [], _ -> t
| a0::a, MLlam (id,t) ->
(match nb_occur_match t with
| _ ->
let a = List.map (ast_lift 1) a in
MLletin (id, a0, linear_beta_red a t))
- | _ -> MLapp (t, a)
+ | _ -> MLapp (t, a)*)
-let rec tmp_head_lams = function
+(*let rec tmp_head_lams = function
| MLlam (id, t) -> MLlam (tmp_id id, tmp_head_lams t)
- | e -> e
+ | e -> e*)
(*s Applies a substitution [s] of constants by their body, plus
linear beta reductions at modified positions.
reduction (this helps the inlining of recursors).
*)
-let rec ast_glob_subst _s _t = assert false (*CSC: reimplement match t with
+let ast_glob_subst _s _t = assert false (*CSC: reimplement match t with
| MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in
(try linear_beta_red a (Refmap'.find refe s)
let is_exn = function MLexn _ -> true | _ -> false
-let rec permut_case_fun br _acc =
+let permut_case_fun br _acc =
let nb = ref max_int in
Array.iter (fun (_,_,t) ->
let ids, c = collect_lams t in
(* Utility functions used in the decision of inlining. *)
-let rec ml_size = function
+(*let rec ml_size = function
| MLapp(t,l) -> List.length l + ml_size t + ml_size_list l
| MLlam(_,t) -> 1 + ml_size t
| MLcons(_,_,l) -> ml_size_list l
and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
-and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l
+and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l*)
-let is_fix = function MLfix _ -> true | _ -> false
+(*let is_fix = function MLfix _ -> true | _ -> false*)
-let rec is_constr = function
+(*let rec is_constr = function
| MLcons _ -> true
| MLlam(_,t) -> is_constr t
- | _ -> false
+ | _ -> false*)
(*s Strictness *)
it begins by at least one non-strict lambda, since the corresponding
argument to [t] might be unevaluated in the expanded code. *)
-exception Toplevel
+(*exception Toplevel*)
-let lift n l = List.map ((+) n) l
+(*let lift n l = List.map ((+) n) l*)
-let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l
+(*let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l*)
(* This function returns a list of de Bruijn indices of non-strict variables,
or raises [Toplevel] if it has an internal non-strict variable.
variable to the candidates? We use this flag to check only the external
lambdas, those that will correspond to arguments. *)
-let rec non_stricts add cand = function
+(*let rec non_stricts add cand = function
| MLlam (_id,t) ->
let cand = lift 1 cand in
let cand = if add then 1::cand else cand in
let n = List.length i in
let cand = lift n cand in
let cand = pop n (non_stricts add cand t) in
- List.merge (compare) cand c) [] v
- List.merge (fun c1 c2 -> c1 - c2) cand c) [] v
++ List.merge (-) cand c) [] v
(* [merge] may duplicates some indices, but I don't mind. *)
| MLmagic t ->
non_stricts add cand t
| _ ->
- cand
+ cand*)
(* The real test: we are looking for internal non-strict variables, so we start
with no candidates, and the only positive answer is via the [Toplevel]
exception. *)
-let is_not_strict t =
+(*let is_not_strict t =
try let _ = non_stricts true [] t in false
- with Toplevel -> true
+ with Toplevel -> true*)
(*s Inlining decision *)
restriction for the moment.
*)
-let inline_test _r _t =
+(*let inline_test _r _t =
(*CSC:if not (auto_inline ()) then*) false
(*
else
let t1 = eta_red t in
let t2 = snd (collect_lams t1) in
not (is_fix t2) && ml_size t < 12 && is_not_strict t
-*)
+*)*)
(*CSC: (not) reimplemented
let con_of_string s =
]
Cset_env.empty*)
-let manual_inline = function (*CSC:
+(*let manual_inline = function (*CSC:
| ConstRef c -> Cset_env.mem c manual_inline_set
- |*) _ -> false
+ |*) _ -> false*)
(* If the user doesn't say he wants to keep [t], we inline in two cases:
\begin{itemize}
- nCic.cmo : nUri.cmi nReference.cmi
- nCic.cmx : nUri.cmx nReference.cmx
- nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi
- nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
-nUri.cmi :
-nReference.cmi : nUri.cmi
-nCicUtils.cmi : nCic.cmo
-nCicSubstitution.cmi : nCic.cmo
--nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmo
- nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
- nCicEnvironment.cmi nCic.cmo nCicPp.cmi
- nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
- nCicEnvironment.cmx nCic.cmx nCicPp.cmi
- nCicPp.cmi : nReference.cmi nCic.cmo
- nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicEnvironment.cmi nCic.cmo nCicReduction.cmi
- nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
--nCicReduction.cmi : nCic.cmo
- nCicSubstitution.cmo : nCicUtils.cmi nCic.cmo nCicSubstitution.cmi
- nCicSubstitution.cmx : nCicUtils.cmx nCic.cmx nCicSubstitution.cmi
- nCicSubstitution.cmi : nCic.cmo
- nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \
- nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmo \
-nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmo
-nCicUntrusted.cmi : nCic.cmo
-nCicPp.cmi : nReference.cmi nCic.cmo
-nCic.cmo : nUri.cmi nReference.cmi
-nCic.cmx : nUri.cmx nReference.cmx
-nUri.cmo : nUri.cmi
-nUri.cmx : nUri.cmi
-nReference.cmo : nUri.cmi nReference.cmi
-nReference.cmx : nUri.cmx nReference.cmi
-nCicUtils.cmo : nReference.cmi nCic.cmo nCicUtils.cmi
-nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi
-nCicSubstitution.cmo : nReference.cmi nCicUtils.cmi nCic.cmo \
++nCic.cmo : \
++ nUri.cmi \
++ nReference.cmi
++nCic.cmx : \
++ nUri.cmx \
++ nReference.cmx
++nCicEnvironment.cmo : \
++ nUri.cmi \
++ nReference.cmi \
++ nCic.cmo \
++ nCicEnvironment.cmi
++nCicEnvironment.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCic.cmx \
++ nCicEnvironment.cmi
++nCicEnvironment.cmi : \
++ nUri.cmi \
++ nReference.cmi \
++ nCic.cmo
++nCicPp.cmo : \
++ nUri.cmi \
++ nReference.cmi \
++ nCicSubstitution.cmi \
++ nCicReduction.cmi \
++ nCicEnvironment.cmi \
++ nCic.cmo \
++ nCicPp.cmi
++nCicPp.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicPp.cmi
++nCicPp.cmi : \
++ nReference.cmi \
++ nCic.cmo
++nCicReduction.cmo : \
++ nReference.cmi \
++ nCicUtils.cmi \
++ nCicSubstitution.cmi \
++ nCicEnvironment.cmi \
++ nCic.cmo \
++ nCicReduction.cmi
++nCicReduction.cmx : \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicReduction.cmi
++nCicReduction.cmi : \
++ nCic.cmo
++nCicSubstitution.cmo : \
++ nCicUtils.cmi \
++ nCic.cmo \
+ nCicSubstitution.cmi
-nCicSubstitution.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \
++nCicSubstitution.cmx : \
++ nCicUtils.cmx \
++ nCic.cmx \
+ nCicSubstitution.cmi
-nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi
-nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
-nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicEnvironment.cmi nCic.cmo nCicReduction.cmi
-nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
-nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \
- nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmo \
++nCicSubstitution.cmi : \
++ nCic.cmo
++nCicTypeChecker.cmo : \
++ nUri.cmi \
++ nReference.cmi \
++ nCicUtils.cmi \
++ nCicSubstitution.cmi \
++ nCicReduction.cmi \
++ nCicEnvironment.cmi \
++ nCic.cmo \
nCicTypeChecker.cmi
--nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \
-- nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \
++nCicTypeChecker.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
nCicTypeChecker.cmi
- nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmo
--nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
-- nCicReduction.cmi nCicEnvironment.cmi nCic.cmo nCicUntrusted.cmi
--nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
-- nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi
- nCicUntrusted.cmi : nCic.cmo
- nCicUtils.cmo : nCic.cmo nCicUtils.cmi
- nCicUtils.cmx : nCic.cmx nCicUtils.cmi
- nCicUtils.cmi : nCic.cmo
- nReference.cmo : nUri.cmi nReference.cmi
- nReference.cmx : nUri.cmx nReference.cmi
- nReference.cmi : nUri.cmi
- nUri.cmo : nUri.cmi
- nUri.cmx : nUri.cmi
-nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
- nCicEnvironment.cmi nCic.cmo nCicPp.cmi
-nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
- nCicEnvironment.cmx nCic.cmx nCicPp.cmi
++nCicTypeChecker.cmi : \
++ nUri.cmi \
++ nReference.cmi \
++ nCic.cmo
++nCicUntrusted.cmo : \
++ nReference.cmi \
++ nCicUtils.cmi \
++ nCicSubstitution.cmi \
++ nCicReduction.cmi \
++ nCicEnvironment.cmi \
++ nCic.cmo \
++ nCicUntrusted.cmi
++nCicUntrusted.cmx : \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicUntrusted.cmi
++nCicUntrusted.cmi : \
++ nCic.cmo
++nCicUtils.cmo : \
++ nCic.cmo \
++ nCicUtils.cmi
++nCicUtils.cmx : \
++ nCic.cmx \
++ nCicUtils.cmi
++nCicUtils.cmi : \
++ nCic.cmo
++nReference.cmo : \
++ nUri.cmi \
++ nReference.cmi
++nReference.cmx : \
++ nUri.cmx \
++ nReference.cmi
++nReference.cmi : \
++ nUri.cmi
++nUri.cmo : \
++ nUri.cmi
++nUri.cmx : \
++ nUri.cmi
+nUri.cmi :
- nCic.cmx : nUri.cmx nReference.cmx
- nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
-nUri.cmi :
-nReference.cmi : nUri.cmi
-nCicUtils.cmi : nCic.cmx
-nCicSubstitution.cmi : nCic.cmx
--nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmx
- nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
- nCicEnvironment.cmx nCic.cmx nCicPp.cmi
- nCicPp.cmi : nReference.cmi nCic.cmx
- nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
--nCicReduction.cmi : nCic.cmx
- nCicSubstitution.cmx : nCicUtils.cmx nCic.cmx nCicSubstitution.cmi
- nCicSubstitution.cmi : nCic.cmx
- nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \
- nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \
-nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx
-nCicUntrusted.cmi : nCic.cmx
-nCicPp.cmi : nReference.cmi nCic.cmx
-nCic.cmo : nUri.cmi nReference.cmi
-nCic.cmx : nUri.cmx nReference.cmx
-nUri.cmo : nUri.cmi
-nUri.cmx : nUri.cmi
-nReference.cmo : nUri.cmi nReference.cmi
-nReference.cmx : nUri.cmx nReference.cmi
-nCicUtils.cmo : nReference.cmi nCic.cmx nCicUtils.cmi
-nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi
-nCicSubstitution.cmo : nReference.cmi nCicUtils.cmi nCic.cmx \
- nCicSubstitution.cmi
-nCicSubstitution.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \
++nCic.cmx : \
++ nUri.cmx \
++ nReference.cmx
++nCicEnvironment.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCic.cmx \
++ nCicEnvironment.cmi
++nCicEnvironment.cmi : \
++ nUri.cmi \
++ nReference.cmi \
++ nCic.cmx
++nCicPp.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicPp.cmi
++nCicPp.cmi : \
++ nReference.cmi \
++ nCic.cmx
++nCicReduction.cmx : \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicReduction.cmi
++nCicReduction.cmi : \
++ nCic.cmx
++nCicSubstitution.cmx : \
++ nCicUtils.cmx \
++ nCic.cmx \
+ nCicSubstitution.cmi
-nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi
-nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
-nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicEnvironment.cmi nCic.cmx nCicReduction.cmi
-nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
-nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \
- nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \
++nCicSubstitution.cmi : \
++ nCic.cmx
++nCicTypeChecker.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
nCicTypeChecker.cmi
- nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx
-nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \
- nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \
- nCicTypeChecker.cmi
-nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi
--nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
-- nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi
- nCicUntrusted.cmi : nCic.cmx
- nCicUtils.cmx : nCic.cmx nCicUtils.cmi
- nCicUtils.cmi : nCic.cmx
- nReference.cmx : nUri.cmx nReference.cmi
- nReference.cmi : nUri.cmi
- nUri.cmx : nUri.cmi
-nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
- nCicEnvironment.cmi nCic.cmx nCicPp.cmi
-nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
- nCicEnvironment.cmx nCic.cmx nCicPp.cmi
++nCicTypeChecker.cmi : \
++ nUri.cmi \
++ nReference.cmi \
++ nCic.cmx
++nCicUntrusted.cmx : \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicUntrusted.cmi
++nCicUntrusted.cmi : \
++ nCic.cmx
++nCicUtils.cmx : \
++ nCic.cmx \
++ nCicUtils.cmi
++nCicUtils.cmi : \
++ nCic.cmx
++nReference.cmx : \
++ nUri.cmx \
++ nReference.cmi
++nReference.cmi : \
++ nUri.cmi
++nUri.cmx : \
++ nUri.cmi
+nUri.cmi :
- nCicLibrary.cmo : nCicLibrary.cmi
- nCicLibrary.cmx : nCicLibrary.cmi
++nCicLibrary.cmo : \
++ nCicLibrary.cmi
++nCicLibrary.cmx : \
++ nCicLibrary.cmi
nCicLibrary.cmi :
-nCicLibrary.cmo : nCicLibrary.cmi
-nCicLibrary.cmx : nCicLibrary.cmi
- nCicLibrary.cmx : nCicLibrary.cmi
++nCicLibrary.cmx : \
++ nCicLibrary.cmi
nCicLibrary.cmi :
-nCicLibrary.cmo : nCicLibrary.cmi
-nCicLibrary.cmx : 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 :
-pp.cmi : terms.cmi
-foSubst.cmi : terms.cmi
-orderings.cmi : terms.cmi
-foUtils.cmi : terms.cmi orderings.cmi
-foUnif.cmi : terms.cmi orderings.cmi
-index.cmi : terms.cmi orderings.cmi
-superposition.cmi : terms.cmi orderings.cmi index.cmi
-stats.cmi : terms.cmi orderings.cmi
-paramod.cmi : terms.cmi orderings.cmi
-nCicBlob.cmi : terms.cmi
-nCicProof.cmi : terms.cmi
-nCicParamod.cmi : terms.cmi
-terms.cmo : terms.cmi
-terms.cmx : terms.cmi
-pp.cmo : terms.cmi pp.cmi
-pp.cmx : terms.cmx pp.cmi
-foSubst.cmo : terms.cmi foSubst.cmi
-foSubst.cmx : terms.cmx foSubst.cmi
-orderings.cmo : terms.cmi pp.cmi foSubst.cmi orderings.cmi
-orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi
-foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
-foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
-foUnif.cmo : terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi
-foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
-index.cmo : terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi
-index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi
-superposition.cmo : terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
- foUnif.cmi foSubst.cmi superposition.cmi
-superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
- foUnif.cmx foSubst.cmx superposition.cmi
-stats.cmo : terms.cmi stats.cmi
-stats.cmx : terms.cmx stats.cmi
-paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \
- foUtils.cmi foUnif.cmi paramod.cmi
-paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
- foUtils.cmx foUnif.cmx paramod.cmi
-nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi
-nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi
-nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi
-nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
-nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \
- nCicBlob.cmi nCicParamod.cmi
-nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
- nCicBlob.cmx nCicParamod.cmi
- foSubst.cmx : terms.cmx foSubst.cmi
- foSubst.cmi : terms.cmi
- foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
- foUnif.cmi : terms.cmi orderings.cmi
- foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
- foUtils.cmi : terms.cmi orderings.cmi
- index.cmx : terms.cmx orderings.cmx foUtils.cmx index.cmi
- index.cmi : terms.cmi orderings.cmi
- nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi
- nCicBlob.cmi : terms.cmi
- nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
- nCicBlob.cmx nCicParamod.cmi
- nCicParamod.cmi : terms.cmi
- nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
- nCicProof.cmi : terms.cmi
- orderings.cmx : terms.cmx foSubst.cmx orderings.cmi
- orderings.cmi : terms.cmi
- paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
- foUtils.cmx paramod.cmi
- paramod.cmi : terms.cmi orderings.cmi
- pp.cmx : terms.cmx pp.cmi
- pp.cmi : terms.cmi
- stats.cmx : terms.cmx stats.cmi
- stats.cmi : terms.cmi orderings.cmi
- superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
- foUnif.cmx foSubst.cmx superposition.cmi
- superposition.cmi : terms.cmi orderings.cmi index.cmi
- terms.cmx : terms.cmi
++foSubst.cmx : \
++ terms.cmx \
++ foSubst.cmi
++foSubst.cmi : \
++ terms.cmi
++foUnif.cmx : \
++ terms.cmx \
++ orderings.cmx \
++ foUtils.cmx \
++ foSubst.cmx \
++ foUnif.cmi
++foUnif.cmi : \
++ terms.cmi \
++ orderings.cmi
++foUtils.cmx : \
++ terms.cmx \
++ orderings.cmx \
++ foSubst.cmx \
++ foUtils.cmi
++foUtils.cmi : \
++ terms.cmi \
++ orderings.cmi
++index.cmx : \
++ terms.cmx \
++ orderings.cmx \
++ foUtils.cmx \
++ index.cmi
++index.cmi : \
++ terms.cmi \
++ orderings.cmi
++nCicBlob.cmx : \
++ terms.cmx \
++ foUtils.cmx \
++ nCicBlob.cmi
++nCicBlob.cmi : \
++ terms.cmi
++nCicParamod.cmx : \
++ terms.cmx \
++ pp.cmx \
++ paramod.cmx \
++ orderings.cmx \
++ nCicProof.cmx \
++ nCicBlob.cmx \
++ nCicParamod.cmi
++nCicParamod.cmi : \
++ terms.cmi
++nCicProof.cmx : \
++ terms.cmx \
++ pp.cmx \
++ nCicBlob.cmx \
++ foSubst.cmx \
++ nCicProof.cmi
++nCicProof.cmi : \
++ terms.cmi
++orderings.cmx : \
++ terms.cmx \
++ foSubst.cmx \
++ orderings.cmi
++orderings.cmi : \
++ terms.cmi
++paramod.cmx : \
++ terms.cmx \
++ superposition.cmx \
++ pp.cmx \
++ orderings.cmx \
++ index.cmx \
++ foUtils.cmx \
++ paramod.cmi
++paramod.cmi : \
++ terms.cmi \
++ orderings.cmi
++pp.cmx : \
++ terms.cmx \
++ pp.cmi
++pp.cmi : \
++ terms.cmi
++stats.cmx : \
++ terms.cmx \
++ stats.cmi
++stats.cmi : \
++ terms.cmi \
++ orderings.cmi
++superposition.cmx : \
++ terms.cmx \
++ pp.cmx \
++ orderings.cmx \
++ index.cmx \
++ foUtils.cmx \
++ foUnif.cmx \
++ foSubst.cmx \
++ superposition.cmi
++superposition.cmi : \
++ terms.cmi \
++ orderings.cmi \
++ index.cmi
++terms.cmx : \
++ terms.cmi
terms.cmi :
-pp.cmi : terms.cmi
-foSubst.cmi : terms.cmi
-orderings.cmi : terms.cmi
-foUtils.cmi : terms.cmi orderings.cmi
-foUnif.cmi : terms.cmi orderings.cmi
-index.cmi : terms.cmi orderings.cmi
-superposition.cmi : terms.cmi orderings.cmi index.cmi
-stats.cmi : terms.cmi orderings.cmi
-paramod.cmi : terms.cmi orderings.cmi
-nCicBlob.cmi : terms.cmi
-nCicProof.cmi : terms.cmi
-nCicParamod.cmi : terms.cmi
-terms.cmo : terms.cmi
-terms.cmx : terms.cmi
-pp.cmo : terms.cmi pp.cmi
-pp.cmx : terms.cmx pp.cmi
-foSubst.cmo : terms.cmi foSubst.cmi
-foSubst.cmx : terms.cmx foSubst.cmi
-orderings.cmo : terms.cmi pp.cmi foSubst.cmi orderings.cmi
-orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi
-foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
-foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
-foUnif.cmo : terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi
-foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
-index.cmo : terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi
-index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi
-superposition.cmo : terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
- foUnif.cmi foSubst.cmi superposition.cmi
-superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
- foUnif.cmx foSubst.cmx superposition.cmi
-stats.cmo : terms.cmi stats.cmi
-stats.cmx : terms.cmx stats.cmi
-paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \
- foUtils.cmi foUnif.cmi paramod.cmi
-paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
- foUtils.cmx foUnif.cmx paramod.cmi
-nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi
-nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi
-nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi
-nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
-nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \
- nCicBlob.cmi nCicParamod.cmi
-nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
- nCicBlob.cmx nCicParamod.cmi
- nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \
- nCicMetaSubst.cmi nCicCoercion.cmi
- nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \
- nCicMetaSubst.cmx nCicCoercion.cmi
- nCicCoercion.cmi : nCicUnifHint.cmi
- nCicMetaSubst.cmo : nCicMetaSubst.cmi
- nCicMetaSubst.cmx : nCicMetaSubst.cmi
-nDiscriminationTree.cmi :
++nCicCoercion.cmo : \
++ nDiscriminationTree.cmi \
++ nCicUnifHint.cmi \
++ nCicMetaSubst.cmi \
++ nCicCoercion.cmi
++nCicCoercion.cmx : \
++ nDiscriminationTree.cmx \
++ nCicUnifHint.cmx \
++ nCicMetaSubst.cmx \
++ nCicCoercion.cmi
++nCicCoercion.cmi : \
++ nCicUnifHint.cmi
++nCicMetaSubst.cmo : \
++ nCicMetaSubst.cmi
++nCicMetaSubst.cmx : \
++ nCicMetaSubst.cmi
nCicMetaSubst.cmi :
- nCicRefineUtil.cmo : nCicMetaSubst.cmi nCicRefineUtil.cmi
- nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi
-nCicUnifHint.cmi :
-nCicCoercion.cmi : nCicUnifHint.cmi
++nCicRefineUtil.cmo : \
++ nCicMetaSubst.cmi \
++ nCicRefineUtil.cmi
++nCicRefineUtil.cmx : \
++ nCicMetaSubst.cmx \
++ nCicRefineUtil.cmi
nCicRefineUtil.cmi :
- nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
- nCicCoercion.cmi nCicRefiner.cmi
- nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmx nCicRefiner.cmi
-nCicUnification.cmi : nCicCoercion.cmi
--nCicRefiner.cmi : nCicCoercion.cmi
-nDiscriminationTree.cmo : nDiscriminationTree.cmi
-nDiscriminationTree.cmx : nDiscriminationTree.cmi
-nCicMetaSubst.cmo : nCicMetaSubst.cmi
-nCicMetaSubst.cmx : nCicMetaSubst.cmi
--nCicUnifHint.cmo : nDiscriminationTree.cmi nCicMetaSubst.cmi \
++nCicRefiner.cmo : \
++ nCicUnification.cmi \
++ nCicRefineUtil.cmi \
++ nCicMetaSubst.cmi \
++ nCicCoercion.cmi \
++ nCicRefiner.cmi
++nCicRefiner.cmx : \
++ nCicUnification.cmx \
++ nCicRefineUtil.cmx \
++ nCicMetaSubst.cmx \
++ nCicCoercion.cmx \
++ nCicRefiner.cmi
++nCicRefiner.cmi : \
++ nCicCoercion.cmi
++nCicUnifHint.cmo : \
++ nDiscriminationTree.cmi \
++ nCicMetaSubst.cmi \
nCicUnifHint.cmi
--nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \
++nCicUnifHint.cmx : \
++ nDiscriminationTree.cmx \
++ nCicMetaSubst.cmx \
nCicUnifHint.cmi
-nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \
- nCicMetaSubst.cmi nCicCoercion.cmi
-nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \
- nCicMetaSubst.cmx nCicCoercion.cmi
-nCicRefineUtil.cmo : nCicMetaSubst.cmi nCicRefineUtil.cmi
-nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi
-nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
-nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
-nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
- nCicCoercion.cmi nCicRefiner.cmi
-nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmx nCicRefiner.cmi
+nCicUnifHint.cmi :
- nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
- nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
- nCicUnification.cmi : nCicCoercion.cmi
- nDiscriminationTree.cmo : nDiscriminationTree.cmi
- nDiscriminationTree.cmx : nDiscriminationTree.cmi
++nCicUnification.cmo : \
++ nCicUnifHint.cmi \
++ nCicMetaSubst.cmi \
++ nCicUnification.cmi
++nCicUnification.cmx : \
++ nCicUnifHint.cmx \
++ nCicMetaSubst.cmx \
++ nCicUnification.cmi
++nCicUnification.cmi : \
++ nCicCoercion.cmi
++nDiscriminationTree.cmo : \
++ nDiscriminationTree.cmi
++nDiscriminationTree.cmx : \
++ nDiscriminationTree.cmi
+nDiscriminationTree.cmi :
- nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \
- nCicMetaSubst.cmx nCicCoercion.cmi
- nCicCoercion.cmi : nCicUnifHint.cmi
- nCicMetaSubst.cmx : nCicMetaSubst.cmi
-nDiscriminationTree.cmi :
++nCicCoercion.cmx : \
++ nDiscriminationTree.cmx \
++ nCicUnifHint.cmx \
++ nCicMetaSubst.cmx \
++ nCicCoercion.cmi
++nCicCoercion.cmi : \
++ nCicUnifHint.cmi
++nCicMetaSubst.cmx : \
++ nCicMetaSubst.cmi
nCicMetaSubst.cmi :
- nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi
-nCicUnifHint.cmi :
-nCicCoercion.cmi : nCicUnifHint.cmi
++nCicRefineUtil.cmx : \
++ nCicMetaSubst.cmx \
++ nCicRefineUtil.cmi
nCicRefineUtil.cmi :
- nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmx nCicRefiner.cmi
-nCicUnification.cmi : nCicCoercion.cmi
--nCicRefiner.cmi : nCicCoercion.cmi
- nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \
-nDiscriminationTree.cmo : nDiscriminationTree.cmi
-nDiscriminationTree.cmx : nDiscriminationTree.cmi
-nCicMetaSubst.cmo : nCicMetaSubst.cmi
-nCicMetaSubst.cmx : nCicMetaSubst.cmi
-nCicUnifHint.cmo : nDiscriminationTree.cmi nCicMetaSubst.cmi \
++nCicRefiner.cmx : \
++ nCicUnification.cmx \
++ nCicRefineUtil.cmx \
++ nCicMetaSubst.cmx \
++ nCicCoercion.cmx \
++ nCicRefiner.cmi
++nCicRefiner.cmi : \
++ nCicCoercion.cmi
++nCicUnifHint.cmx : \
++ nDiscriminationTree.cmx \
++ nCicMetaSubst.cmx \
nCicUnifHint.cmi
-nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \
- nCicUnifHint.cmi
-nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \
- nCicMetaSubst.cmi nCicCoercion.cmi
-nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \
- nCicMetaSubst.cmx nCicCoercion.cmi
-nCicRefineUtil.cmo : nCicMetaSubst.cmi nCicRefineUtil.cmi
-nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi
-nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
-nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
-nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
- nCicCoercion.cmi nCicRefiner.cmi
-nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmx nCicRefiner.cmi
+nCicUnifHint.cmi :
- nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
- nCicUnification.cmi : nCicCoercion.cmi
- nDiscriminationTree.cmx : nDiscriminationTree.cmi
++nCicUnification.cmx : \
++ nCicUnifHint.cmx \
++ nCicMetaSubst.cmx \
++ nCicUnification.cmi
++nCicUnification.cmi : \
++ nCicCoercion.cmi
++nDiscriminationTree.cmx : \
++ nDiscriminationTree.cmi
+nDiscriminationTree.cmi :
--continuationals.cmo : continuationals.cmi
--continuationals.cmx : continuationals.cmi
++continuationals.cmo : \
++ continuationals.cmi
++continuationals.cmx : \
++ continuationals.cmi
continuationals.cmi :
-declarative.cmo : nnAuto.cmi nTactics.cmi nTacStatus.cmi nCicElim.cmi \
- continuationals.cmi declarative.cmi
-declarative.cmx : nnAuto.cmx nTactics.cmx nTacStatus.cmx nCicElim.cmx \
- continuationals.cmx declarative.cmi
-declarative.cmi : nnAuto.cmi nTacStatus.cmi
--nCicElim.cmo : nCicElim.cmi
--nCicElim.cmx : nCicElim.cmi
++declarative.cmo : \
++ nnAuto.cmi \
++ nTactics.cmi \
++ nTacStatus.cmi \
++ nCicElim.cmi \
++ continuationals.cmi \
++ declarative.cmi
++declarative.cmx : \
++ nnAuto.cmx \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ declarative.cmi
++declarative.cmi : \
++ nnAuto.cmi \
++ nTacStatus.cmi
++nCicElim.cmo : \
++ nCicElim.cmi
++nCicElim.cmx : \
++ nCicElim.cmi
nCicElim.cmi :
--nCicTacReduction.cmo : nCicTacReduction.cmi
--nCicTacReduction.cmx : nCicTacReduction.cmi
++nCicTacReduction.cmo : \
++ nCicTacReduction.cmi
++nCicTacReduction.cmx : \
++ nCicTacReduction.cmi
nCicTacReduction.cmi :
--nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \
++nDestructTac.cmo : \
++ nTactics.cmi \
++ nTacStatus.cmi \
++ continuationals.cmi \
nDestructTac.cmi
--nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \
++nDestructTac.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ continuationals.cmx \
nDestructTac.cmi
--nDestructTac.cmi : nTacStatus.cmi
--nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \
-- continuationals.cmi nInversion.cmi
--nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \
-- continuationals.cmx nInversion.cmi
--nInversion.cmi : nTacStatus.cmi
--nTacStatus.cmo : nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi
--nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
--nTacStatus.cmi : continuationals.cmi
--nTactics.cmo : nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi
--nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
--nTactics.cmi : nTacStatus.cmi
--nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \
-- continuationals.cmi nnAuto.cmi
--nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
-- continuationals.cmx nnAuto.cmi
--nnAuto.cmi : nTacStatus.cmi
++nDestructTac.cmi : \
++ nTacStatus.cmi
++nInversion.cmo : \
++ nTactics.cmi \
++ nTacStatus.cmi \
++ nCicElim.cmi \
++ continuationals.cmi \
++ nInversion.cmi
++nInversion.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ nInversion.cmi
++nInversion.cmi : \
++ nTacStatus.cmi
++nTacStatus.cmo : \
++ nCicTacReduction.cmi \
++ continuationals.cmi \
++ nTacStatus.cmi
++nTacStatus.cmx : \
++ nCicTacReduction.cmx \
++ continuationals.cmx \
++ nTacStatus.cmi
++nTacStatus.cmi : \
++ continuationals.cmi
++nTactics.cmo : \
++ nTacStatus.cmi \
++ nCicElim.cmi \
++ continuationals.cmi \
++ nTactics.cmi
++nTactics.cmx : \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ nTactics.cmi
++nTactics.cmi : \
++ nTacStatus.cmi
++nnAuto.cmo : \
++ nTactics.cmi \
++ nTacStatus.cmi \
++ nCicTacReduction.cmi \
++ continuationals.cmi \
++ nnAuto.cmi
++nnAuto.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicTacReduction.cmx \
++ continuationals.cmx \
++ nnAuto.cmi
++nnAuto.cmi : \
++ nTacStatus.cmi
- continuationals.cmx : continuationals.cmi
++continuationals.cmx : \
++ continuationals.cmi
continuationals.cmi :
- nCicElim.cmx : nCicElim.cmi
-nCicTacReduction.cmi :
-nTacStatus.cmi : continuationals.cmi
++declarative.cmx : \
++ nnAuto.cmx \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ declarative.cmi
++declarative.cmi : \
++ nnAuto.cmi \
++ nTacStatus.cmi
++nCicElim.cmx : \
++ nCicElim.cmi
nCicElim.cmi :
-nTactics.cmi : nTacStatus.cmi
-declarative.cmi : nTacStatus.cmi
-nnAuto.cmi : nTacStatus.cmi
-nDestructTac.cmi : nTacStatus.cmi
-nInversion.cmi : nTacStatus.cmi
-continuationals.cmo : continuationals.cmi
-continuationals.cmx : continuationals.cmi
-nCicTacReduction.cmo : nCicTacReduction.cmi
--nCicTacReduction.cmx : nCicTacReduction.cmi
-nTacStatus.cmo : nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi
-nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
-nCicElim.cmo : nCicElim.cmi
-nCicElim.cmx : nCicElim.cmi
-nTactics.cmo : nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi
-nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
-declarative.cmo : nTactics.cmi declarative.cmi
-declarative.cmx : nTactics.cmx declarative.cmi
-nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \
- continuationals.cmi nnAuto.cmi
-nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
- continuationals.cmx nnAuto.cmi
-nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \
- nDestructTac.cmi
-nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \
++nCicTacReduction.cmx : \
++ nCicTacReduction.cmi
+nCicTacReduction.cmi :
- nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \
++nDestructTac.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ continuationals.cmx \
nDestructTac.cmi
- nDestructTac.cmi : nTacStatus.cmi
-nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \
- continuationals.cmi nInversion.cmi
--nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \
-- continuationals.cmx nInversion.cmi
- nInversion.cmi : nTacStatus.cmi
- nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
- nTacStatus.cmi : continuationals.cmi
- nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
- nTactics.cmi : nTacStatus.cmi
- nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
- continuationals.cmx nnAuto.cmi
- nnAuto.cmi : nTacStatus.cmi
++nDestructTac.cmi : \
++ nTacStatus.cmi
++nInversion.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ nInversion.cmi
++nInversion.cmi : \
++ nTacStatus.cmi
++nTacStatus.cmx : \
++ nCicTacReduction.cmx \
++ continuationals.cmx \
++ nTacStatus.cmi
++nTacStatus.cmi : \
++ continuationals.cmi
++nTactics.cmx : \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ nTactics.cmi
++nTactics.cmi : \
++ nTacStatus.cmi
++nnAuto.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicTacReduction.cmx \
++ continuationals.cmx \
++ nnAuto.cmi
++nnAuto.cmi : \
++ nTacStatus.cmi
type goal = int
+ type parameters = (string * string) list
+
module Stack =
struct
type switch = Open of goal | Closed of goal
type locator = int * switch
type tag = [ `BranchTag | `FocusTag | `NoTag ]
- type entry = locator list * locator list * locator list * tag
+ type entry = locator list * locator list * locator list * tag * parameters
type t = entry list
- let empty = [ [], [], [], `NoTag ]
+ let empty = [ [], [], [], `NoTag , []]
let fold ~env ~cont ~todo init stack =
let rec aux acc depth =
function
| [] -> acc
- | (locs, todos, conts, tag) :: tl ->
- | (locs, todos, conts, tag, p) :: tl ->
++ | (locs, todos, conts, tag, _p) :: tl ->
let acc = List.fold_left (fun acc -> env acc depth tag) acc locs in
let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in
let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in
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)));
--- /dev/null
- | (g1, _, k, tag1, _) :: tl ->
+ (* 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")
- | loc::tl ->
++ | (g1, _, _k, _tag1, _) :: _tl ->
+ let goals = filter_open g1 in
+ match goals with
+ [] -> fail (lazy "No goals under focus")
- let status,gty = term_of_cic_term status gty ctx in
- gty
++ | 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
- | (k,v as hd')::tl' ->
++ 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
+ [] -> []
- | NCic.Prod (_,t,_) ->
++ | (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
- let t = extract_conclusion_type status goal in
++ | 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,res = are_convertible t1 t2 status goal in
++ let status,t = extract_conclusion_type status goal in
+ if alpha_eq_tacterm_kerterm t1 t status goal then
+ match t2 with
+ | None -> continuation
+ | Some t2 ->
- | (g,t,k,tag,p)::_ -> try List.assoc key p with _ -> ""
++ 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
+ [] -> ""
- let wrappedjust = just in
++ | (_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
- | (k',v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl)
+ 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
+ [] -> []
- let (mattrs,ctx,t as conj) = try List.assoc goal metasenv with _ -> assert false in
++ | (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 =
- | (g,_,_,_,_) :: tl ->
++ 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")
- | ([],_,_,_,_) :: tl -> false
++ | (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:
+ * *)
let mk_cic_term c t = c,t ;;
let ppterm (status:#pstatus) t =
- let uri,height,metasenv,subst,obj = status#obj in
+ let _uri,_height,metasenv,subst,_obj = status#obj in
let context,t = t in
status#ppterm ~metasenv ~subst ~context t
;;
let ppcontext (status: #pstatus) c =
- let uri,height,metasenv,subst,obj = status#obj in
+ let _uri,_height,metasenv,subst,_obj = status#obj in
status#ppcontext ~metasenv ~subst c
;;
let ppterm_and_context (status: #pstatus) t =
- let uri,height,metasenv,subst,obj = status#obj in
+ let _uri,_height,metasenv,subst,_obj = status#obj in
let context,t = t in
status#ppcontext ~metasenv ~subst context ^ "\n ⊢ "^
status#ppterm ~metasenv ~subst ~context t
;;
-let relocate status destination (source,t as orig) =
+let relocate status destination (source,_t as orig) =
pp(lazy("relocate:\n" ^ ppterm_and_context status orig));
pp(lazy("relocate in:\n" ^ ppcontext status destination));
let rc =
compute_ops (e::ctx) (cl1,cl2)
else
[ `Delift ctx; `Lift (List.rev ex) ]
- | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
+ | (n1, NCic.Def (_b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
if n1 = n2 &&
NCicReduction.are_convertible status ctx ~subst ~metasenv t1 t2 then
compute_ops (e::ctx) (cl1,cl2)
else
[ `Delift ctx; `Lift (List.rev ex) ]
- | (n1, NCic.Decl _)::cl1 as ex, (n2, NCic.Def _)::cl2 ->
+ | (_n1, NCic.Decl _)::_cl1 as ex, (_n2, NCic.Def _)::_cl2 ->
[ `Delift ctx; `Lift (List.rev ex) ]
| _::_ as ex, [] -> [ `Lift (List.rev ex) ]
| [], _::_ -> [ `Delift ctx ]
status, (ctx, t)
;;
- let n,h,metasenv,subst,o = status#obj in
+ 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
else
let _,_,_,subst,_ = status#obj in
match t with
- | NCic.Meta (i,lc) when List.mem_assoc i subst ->
+ | NCic.Meta (i,_lc) when List.mem_assoc i subst ->
let _,_,t,_ = NCicUtils.lookup_subst i subst in
aux ctx (status,already_found) t
| NCic.Meta _ -> (status,already_found),t
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 =
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
;;
let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
- | (hd,_) :: tl when hd = name -> acc
+ | (hd,_) :: _ when hd = name -> acc
| _ :: tl -> aux (acc + 1) tl
in
aux 1 context
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 _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 ->
++ | (g,_,_,_,_) :: _s ->
assert (List.length g = List.length seqs);
(match seqs with
[] -> id_tac
let print ?(depth=0) s =
prerr_endline (String.make (2*depth) ' '^Lazy.force s)
-let noprint ?(depth=0) _ = ()
+let noprint ?depth:(_=0) _ = ()
let debug_print = noprint
open Continuationals.Stack
let toref f tbl t =
match t with
| Ast.NRef n ->
- f tbl n
+ f tbl n
| Ast.NCic _ (* local candidate *)
| _ -> ()
else true
with Not_found -> true
-let print_stat status tbl =
+let print_stat _status tbl =
let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
let relevance v = float !(v.uses) /. float !(v.nominations) in
let vcompare (_,v1) (_,v2) =
"; 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 =
++let index_local_equations2 eq_cache status open_goal lemmas ?flag:(_=false) nohyps =
noprint (lazy "indexing equations");
let eq_cache,lemmas =
match lemmas with
eq_cache lemmas
;;
-let fast_eq_check_tac ~params s =
+let fast_eq_check_tac ~params:_ s =
let unit_eq = index_local_equations s#eq_cache s in
dist_fast_eq_check unit_eq s
;;
| s::_ -> s
;;
-let paramod_tac ~params s =
+let paramod_tac ~params:_ s =
let unit_eq = index_local_equations s#eq_cache s in
NTactics.distribute_tac (paramod unit_eq) s
;;
(fun ty ctx_entry ->
match ctx_entry with
| name, NCic.Decl t -> NCic.Prod(name,t,ty)
- | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
+ | _name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
;;
let args_for_context ?(k=1) ctx =
List.fold_left
(fun (n,l) ctx_entry ->
match ctx_entry with
- | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
- | name, NCic.Def(bo, _) -> n+1,l)
+ | _name, NCic.Decl _t -> n+1,NCic.Rel(n)::l
+ | _name, NCic.Def(_bo, _) -> n+1,l)
(k,[]) ctx in
args
List.fold_left
(fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
let ikind = NCicUntrusted.kind_of_meta iattr in
- let metasenv,j,instance,ty =
+ let metasenv,_j,instance,ty =
NCicMetaSubst.mk_meta ~attrs:iattr
metasenv ctx ~with_type:ty ikind in
let s_entry = i,(iattr, ctx, instance, ty) in
*)
let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in
List.fold_left
- (fun (subst,objs) (i,(iattr,ctx,ty)) ->
+ (fun (subst,objs) (i,(_iattr,ctx,ty)) ->
let ty = NCicUntrusted.apply_subst status subst ctx ty in
let ctx =
NCicUntrusted.apply_subst_context status ~fix_projections:true
subst ctx in
- let (uri,_,_,_,obj) as okind =
+ let (uri,_,_,_,_obj) as okind =
constant_for_meta status ctx ty i in
try
NCicEnvironment.check_and_add_obj status okind;
| _ -> let args =
List.map (NCicSubstitution.subst_meta status lc) args in
NCic.Appl(NCic.Rel k::args))
- | NCic.Meta (j,lc) as m ->
+ | NCic.Meta (_j,lc) as m ->
(match lc with
_,NCic.Irl _ -> m
| n,NCic.Ctx l ->
let close_wrt_metasenv status subst =
List.fold_left
- (fun ty (i,(iattr,ctx,mty)) ->
+ (fun ty (i,(_iattr,ctx,mty)) ->
let mty = NCicUntrusted.apply_subst status subst ctx mty in
let ctx =
NCicUntrusted.apply_subst_context status ~fix_projections:true
NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in
match ty with
| NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
- when nre<>nref ->
- let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
- aux metasenv bo (args@moreargs)
+ when nre<>nref ->
+ let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
+ aux metasenv bo (args@moreargs)
| NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
- when nre<>nref ->
- let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
- aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
+ when nre<>nref ->
+ let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
+ aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
| _ -> ty,metasenv,(args@moreargs)
in
aux metasenv ty []
let smart_apply t unit_eq status g =
- let n,h,metasenv,subst,o = status#obj in
- let gname, ctx, gty = List.assoc g metasenv in
+ let n,h,metasenv,_subst,o = status#obj in
+ let _gname, ctx, gty = List.assoc g metasenv in
(* let ggty = mk_cic_term context gty in *)
let status, t = disambiguate status ctx t `XTNone in
let status,t = term_of_cic_term status t ctx in
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
debug_print(lazy("ritorno da fast_eq_check"));
res
with
- | NCicEnvironment.ObjectNotFound s as e ->
+ | NCicEnvironment.ObjectNotFound _s as e ->
raise (Error (lazy "eq_coerc non yet defined",Some e))
| Error _ as e -> debug_print (lazy "error"); raise e
(* FG: for now we catch TypeCheckerFailure; to be understood *)
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 *)
unit_eq = unit_eq;
trace = trace}
-let only signature _context candidate = true
+let only _signature _context _candidate = true
(*
(* TASSI: nel trie ci mettiamo solo il body, non il ty *)
let candidate_ty =
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
;;
-let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
+let try_candidate ?(smart=0) _flags depth status eq_cache _ctx t =
try
- let old_og_no = List.length (open_goals (depth+1) status) in
+ (*let old_og_no = List.length (open_goals (depth+1) status) in*)
debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : "
^ (NotationPp.pp_term status) t));
let status =
(* some flexibility *)
if og_no - old_og_no > res then
(debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
- ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
+ ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
debug_print ~depth (lazy "strange application"); None)
else
*) (incr candidate_no; Some ((!candidate_no,t),status))
- with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
+ with Error _ -> debug_print ~depth (lazy "failed"); None
;;
let sort_of status subst metasenv ctx t =
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 get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty =
+ 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 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 *)
flags status tcache signature gty
in
let sm = if is_eq || is_prod then 0 else 2 in
- let sm1 = if flags.last then 2 else 0 in
+ (*let sm1 = if flags.last then 2 else 0 in *)
let maxd = (depth + 1 = flags.maxdepth) in
let try_candidates only_one sm acc candidates =
List.fold_left
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 =
let intro ~depth status facts name =
let status = NTactics.intro_tac name status in
- let _, ctx, ngty = current_goal status in
+ let _, ctx, _ngty = current_goal status in
let t = mk_cic_term ctx (NCic.Rel 1) in
let status, keys = keys_of_term status t in
let facts = List.fold_left (add_to_th t) facts keys in
| _ -> 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 =
++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 status ?(use_given_only=false): unit=
++auto_main flags signature cache depth ?(use_given_only=false) status: unit=
debug_print ~depth (lazy "entering auto main");
debug_print ~depth (pptrace status cache.trace);
debug_print ~depth (lazy ("stack length = " ^
- (string_of_int (List.length status#stack))));
+ (string_of_int (List.length status#stack))));
(* ignore(Unix.select [] [] [] 0.01); *)
let status = sort_tac (clean_up_tac status) in
let goals = head_goals status#stack in
match goals with
| [] when depth = 0 -> raise (Proved (status,cache.trace))
| [] ->
- let status = NTactics.merge_tac status in
- let cache =
- let l,tree = cache.under_inspection in
- match l with
- | [] -> cache (* possible because of intros that cleans the cache *)
- | a::tl -> let tree = rm_from_th a tree a in
- {cache with under_inspection = tl,tree}
- in
- auto_clusters flags signature cache (depth-1) status ~use_given_only
- | orig::_ ->
- if depth > 0 && move_to_side depth status
- then
- let status = NTactics.merge_tac status in
- let cache =
- let l,tree = cache.under_inspection in
- match l with
- | [] -> cache (* possible because of intros that cleans the cache*)
- | a::tl -> let tree = rm_from_th a tree a in
- {cache with under_inspection = tl,tree}
- in
- auto_clusters flags signature cache (depth-1) status ~use_given_only
- else
+ let status = NTactics.merge_tac status in
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> cache (* possible because of intros that cleans the cache *)
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
- auto_clusters flags signature cache (depth-1) status
++ auto_clusters flags signature cache (depth-1) status ~use_given_only
+ | _orig::_ ->
+ if depth > 0 && move_to_side depth status
+ then
+ let status = NTactics.merge_tac status in
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> cache (* possible because of intros that cleans the cache*)
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
- auto_clusters flags signature cache (depth-1) status
++ auto_clusters flags signature cache (depth-1) status ~use_given_only
+ else
let ng = List.length goals in
(* moved inside auto_clusters *)
if ng > flags.maxwidth then begin
debug_print ~depth (lazy "FAIL LOCAL WIDTH");
- HLog.warn (sprintf "local width (%u) exceeded: %u"
- flags.maxwidth ng);
- raise (Gaveup cache.failures)
+ HLog.warn (sprintf "local width (%u) exceeded: %u"
+ flags.maxwidth ng);
+ raise (Gaveup cache.failures)
end else if depth = flags.maxdepth then
- raise (Gaveup cache.failures)
+ raise (Gaveup cache.failures)
else
let status = NTactics.branch_tac ~force:true status in
let g,gctx, gty = current_goal status in
(* 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 auto_lowtac ~params:(univ,flags as params) status goal =
+ 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
- helm_registry.cmo : helm_registry.cmi
- helm_registry.cmx : helm_registry.cmi
++helm_registry.cmo : \
++ helm_registry.cmi
++helm_registry.cmx : \
++ helm_registry.cmi
helm_registry.cmi :
-helm_registry.cmo : helm_registry.cmi
-helm_registry.cmx : helm_registry.cmi
- helm_registry.cmx : helm_registry.cmi
++helm_registry.cmx : \
++ helm_registry.cmi
helm_registry.cmi :
-helm_registry.cmo : helm_registry.cmi
-helm_registry.cmx : helm_registry.cmi
- utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi
++utf8Macro.cmx : \
++ utf8MacroTable.cmx \
++ utf8Macro.cmi
utf8Macro.cmi :
-utf8MacroTable.cmo :
utf8MacroTable.cmx :
-utf8Macro.cmo : utf8MacroTable.cmx utf8Macro.cmi
-utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi
- extThread.cmo : extThread.cmi
- extThread.cmx : extThread.cmi
-threadSafe.cmi :
++extThread.cmo : \
++ extThread.cmi
++extThread.cmx : \
++ extThread.cmi
extThread.cmi :
--threadSafe.cmo : threadSafe.cmi
--threadSafe.cmx : threadSafe.cmi
-extThread.cmo : extThread.cmi
-extThread.cmx : extThread.cmi
++threadSafe.cmo : \
++ threadSafe.cmi
++threadSafe.cmx : \
++ threadSafe.cmi
+threadSafe.cmi :
- extThread.cmx : extThread.cmi
-threadSafe.cmi :
++extThread.cmx : \
++ extThread.cmi
extThread.cmi :
-threadSafe.cmo : threadSafe.cmi
--threadSafe.cmx : threadSafe.cmi
-extThread.cmo : extThread.cmi
-extThread.cmx : extThread.cmi
++threadSafe.cmx : \
++ threadSafe.cmi
+threadSafe.cmi :
- xml.cmo : xml.cmi
- xml.cmx : xml.cmi
++xml.cmo : \
++ xml.cmi
++xml.cmx : \
++ xml.cmi
xml.cmi :
- xmlPushParser.cmo : xmlPushParser.cmi
- xmlPushParser.cmx : xmlPushParser.cmi
++xmlPushParser.cmo : \
++ xmlPushParser.cmi
++xmlPushParser.cmx : \
++ xmlPushParser.cmi
xmlPushParser.cmi :
-xml.cmo : xml.cmi
-xml.cmx : xml.cmi
-xmlPushParser.cmo : xmlPushParser.cmi
-xmlPushParser.cmx : xmlPushParser.cmi
- xml.cmx : xml.cmi
++xml.cmx : \
++ xml.cmi
xml.cmi :
- xmlPushParser.cmx : xmlPushParser.cmi
++xmlPushParser.cmx : \
++ xmlPushParser.cmi
xmlPushParser.cmi :
-xml.cmo : xml.cmi
-xml.cmx : xml.cmi
-xmlPushParser.cmo : xmlPushParser.cmi
-xmlPushParser.cmx : xmlPushParser.cmi
Content2pres.ncontext2pres
((new NCicPp.status)#ppcontext ~metasenv ~subst)
-let ntxt_of_cic_subst ~map_unicode_to_tex size status ~metasenv ?use_subst subst =
+let ntxt_of_cic_subst ~map_unicode_to_tex:_ _size _status ~metasenv ?use_subst subst =
[],
"<<<high level printer for subst not implemented; low-level printing:>>>\n" ^
(new NCicPp.status)#ppsubst ~metasenv ?use_subst subst
object(self)
inherit Interpretations.status
inherit TermContentPres.status
- method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =
+ method ppterm ~context ~subst ~metasenv ?margin:(_) ?inside_fix:(_) t =
snd (ntxt_of_cic_term ~map_unicode_to_tex:false 80 self ~metasenv ~subst
~context t)
- method ppcontext ?sep ~subst ~metasenv context =
+ method ppcontext ?sep:(_) ~subst ~metasenv context =
snd (ntxt_of_cic_context ~map_unicode_to_tex:false 80 self ~metasenv ~subst
context)
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))
(* 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$ *)
-open GrafiteTypes
+ 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
++ | (_g,_t,_k,_tag,p)::_tl -> try
+ let s = List.assoc "context" p in
+ s = "cases" || s = "induction"
+ with
+ Not_found -> false
+ ;;
+
+ let has_focused_goal stack =
+ match stack with
+ [] -> false
- | (g,t,k,tag,p)::tl -> (List.length g) > 0
++ | (g,_t,_k,_tag,_p)::_tl -> (List.length g) > 0
+ ;;
+
-let get_indentation status statement =
++let get_indentation status _statement =
+ let base_ind =
+ match status#stack with
+ [] -> 0
+ | s -> List.length(s) * 2
in
- let stm = Pcre.replace ~rex:slash_n_RE stm in
- let stm =
+ if cases_or_induction_context status#stack then
+ (
+ if has_focused_goal status#stack then
+ base_ind + 2
+ else
+ base_ind
+ )
+ else
+ base_ind
+ ;;
+
+ let pp_ind s n =
+ let rec aux s n =
+ match n with
+ 0 -> s
+ | n -> " " ^ (aux s (n-1))
+ in
+ aux s n
+
+ let write_ast_to_file status fname statement =
+ let indentation = get_indentation status statement in
+ let str = match statement with
+ G.Comment _ -> GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | G.Executable (_,code) ->
+ (
+ match code with
+ G.NTactic _ -> GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | G.NCommand (_,cmd) ->
+ (
+ match cmd with
+ | G.NObj (_,obj,_) ->
+ (
+ match obj with
- Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
++ NotationPt.Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | _ -> ""
+ )
+ | G.NQed _ -> GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | _ -> ""
+ )
+ | _ -> ""
+ )
+ in
+ if str <> "" then
+ (
+ let s = pp_ind str indentation in
+ let flaglist = if !first_line = false then [Open_wronly; Open_append; Open_creat]
+ else (first_line := false; [Open_wronly; Open_trunc; Open_creat])
+ in
+ let out_channel =
+ Stdlib.open_out_gen flaglist 0o0644 fname in
+ let _ = Stdlib.output_string out_channel ((if str.[0] <> '\n' then s else str) ^ "\n") in
+ let _ = Stdlib.close_out out_channel in
+ str
+ )
+ else
+ str
+ ;;
+
+ let pp_ast_statement status stm ~fname =
+ let stm = write_ast_to_file status (fname ^ ".parsed.ma") stm in
+ if stm <> "" then
+ (
+ let stm = Pcre.replace ~rex:slash_n_RE stm in
+ let stm =
if String.length stm > 50 then String.sub stm 0 50 ^ " ..."
else stm
- in
+ in
HLog.debug ("Executing: ``" ^ stm ^ "''")
+ )
+ else
+ HLog.debug ("Executing: `` Unprintable statement ''")
;;
let clean_exit baseuri exn =
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))
;;
(* given a path to a ma file inside the include_paths, returns the
new include_paths associated to that file *)
-let read_include_paths ~include_paths file =
- try
- let root, _buri, _fname, _tgt =
- Librarian.baseuri_of_script ~include_paths:[] file in
- let includes =
- try
- Str.split (Str.regexp " ")
- (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
- with Not_found -> []
- in
- let rc = root :: includes in
+let read_include_paths ~include_paths:_ file =
+ try
+ let root, _buri, _fname, _tgt =
+ Librarian.baseuri_of_script ~include_paths:[] file in
+ let includes =
+ try
+ Str.split (Str.regexp " ")
+ (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+ with Not_found -> []
+ in
+ let rc = root :: includes in
List.iter (HLog.debug) rc; rc
- with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
- []
+ with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+ []
;;
- let rec get_ast status ~compiling ~asserted ~include_paths strm =
+ let rec get_ast status ~compiling ~asserted ~include_paths strm =
match GrafiteParser.parse_statement status strm with
- (GrafiteAst.Executable
+ (GrafiteAst.Executable
(_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
- ->
- let already_included = NCicLibrary.get_transitively_included status in
- let asserted,_ =
- assert_ng ~already_included ~compiling ~asserted ~include_paths
- mafilename
- in
- asserted,cmd
- | cmd -> asserted,cmd
+ ->
+ let already_included = NCicLibrary.get_transitively_included status in
+ let asserted,_ =
+ assert_ng ~already_included ~compiling ~asserted ~include_paths
+ mafilename
+ in
+ asserted,cmd
+ | cmd -> asserted,cmd
and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
- let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop asserted status str =
- let asserted,stop,status,str =
- try
- let cont =
- try Some (get_ast status ~compiling ~asserted ~include_paths str)
- with End_of_file -> None in
- match cont with
- | None -> asserted, true, status, str
- | Some (asserted,ast) ->
- cb status ast;
- let new_statuses =
- eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
- let status =
- match new_statuses with
- [s,None] -> s
- | _::(_,Some (_,value))::_ ->
- raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
- | _ -> assert false in
- (* CSC: complex patch to re-build the lexer since the tokens may
- have changed. Note: this way we loose look-ahead tokens.
- Hence the "include" command must be terminated (no look-ahead) *)
- let str =
- match ast with
- (GrafiteAst.Executable
- (_,GrafiteAst.NCommand
- (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
+ let rec loop asserted status str =
+ let asserted,stop,status,str =
+ try
+ let cont =
+ try Some (get_ast status ~compiling ~asserted ~include_paths str)
+ with End_of_file -> None in
+ match cont with
+ | None -> asserted, true, status, str
+ | Some (asserted,ast) ->
+ cb status ast;
+ let new_statuses =
+ eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
+ let status =
+ match new_statuses with
+ [s,None] -> s
+ | _::(_,Some (_,value))::_ ->
+ raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
+ | _ -> assert false in
+ (* CSC: complex patch to re-build the lexer since the tokens may
+ have changed. Note: this way we loose look-ahead tokens.
+ Hence the "include" command must be terminated (no look-ahead) *)
+ let str =
+ match ast with
+ (GrafiteAst.Executable
+ (_,GrafiteAst.NCommand
+ (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
GrafiteParser.parsable_statement status
- (GrafiteParser.strm_of_parsable str)
- | _ -> str
- in
- asserted, false, status, str
- with exn when not matita_debug ->
- raise (EnrichedWithStatus (exn, status))
+ (GrafiteParser.strm_of_parsable str)
+ | _ -> str
+ in
+ asserted, false, status, str
+ with exn when not matita_debug ->
+ raise (EnrichedWithStatus (exn, status))
+ in
+ if stop then asserted,status else loop asserted status str
in
- if stop then asserted,status else loop asserted status str
- in
loop asserted status str
and compile ~compiling ~asserted ~include_paths fname =
if List.mem fname compiling then raise (CircularDependency fname);
let compiling = fname::compiling in
let matita_debug = Helm_registry.get_bool "matita.debug" in
- let root,baseuri,fname,_tgt =
+ let root,baseuri,fname,_tgt =
Librarian.baseuri_of_script ~include_paths fname in
if Http_getter_storage.is_read_only baseuri then assert false;
(* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
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)
open MatitaGtkMisc
open MatitaMisc
-exception Found of int
-
let all_disambiguation_passes = ref false
(* this is a shit and should be changed :-{ *)
?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
?copy_cb ()
- ~id uris
+ ~id:_ uris
=
if (selection_mode <> `SINGLE) &&
(Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
| uris -> return (Some (List.map NReference.reference_of_string uris)));
connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
dialog#uriChoiceDialog#show ();
+ (* CSC: old Gtk2 code. Use #run instead. Look for similar code handling
+ other dialogs *)
GtkThread.main ();
(match !choices with
| None -> raise MatitaTypes.Cancel
(let loc_row = tree_store#append () in
begin
match lll with
- [passes,envs_and_diffs,_,_] ->
+ [passes,_envs_and_diffs,_,_] ->
tree_store#set ~row:loc_row ~column:id_col
("Error location " ^ string_of_int (!idx1+1) ^
", error message " ^ string_of_int (!idx1+1) ^ ".1" ^
exception UseLibrary;;
let interactive_error_interp ~all_passes
- (source_buffer:GSourceView2.source_buffer) notify_exn offset errorll filename
+ (source_buffer:GSourceView3.source_buffer) notify_exn offset errorll filename
=
(* hook to save a script for each disambiguation error *)
if false then
(MultiPassDisambiguator.DisambiguationError
(offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
| _::_ ->
+ GtkThread.sync (fun _ ->
let dialog = new disambiguationErrors () in
- if all_passes then
- dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
+ dialog#toplevel#add_button "Fix this interpretation" `OK;
+ dialog#toplevel#add_button "Close" `DELETE_EVENT;
+ if not all_passes then
+ dialog#toplevel#add_button "More errors" `HELP; (* HELP means MORE *)
let model = new interpErrorModel dialog#treeview choices in
dialog#disambiguationErrors#set_title "Disambiguation error";
dialog#disambiguationErrorsLabel#set_label
(MultiPassDisambiguator.DisambiguationError
(offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
));
- let return _ =
- dialog#disambiguationErrors#destroy ();
- GMain.Main.quit ()
+ (match GtkThread.sync dialog#toplevel#run () with
+ | `OK ->
+ let tree_path =
+ match fst (dialog#treeview#get_cursor ()) with
+ None -> assert false
+ | Some tp -> tp in
+ let idx1,idx2,idx3 = model#get_interp_no tree_path in
+ let diff =
+ match idx2,idx3 with
+ Some idx2, Some idx3 ->
+ let _,lll = List.nth choices idx1 in
+ let _,envs_and_diffs,_,_ = List.nth lll idx2 in
+ let _,_,diff = List.nth envs_and_diffs idx3 in
+ diff
+ | _,_ -> assert false
in
- let fail _ = return () in
- ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true));
- connect_button dialog#disambiguationErrorsOkButton
- (fun _ ->
- let tree_path =
- match fst (dialog#treeview#get_cursor ()) with
- None -> assert false
- | Some tp -> tp in
- let idx1,idx2,idx3 = model#get_interp_no tree_path in
- let diff =
- match idx2,idx3 with
- Some idx2, Some idx3 ->
- let _,lll = List.nth choices idx1 in
- let _,envs_and_diffs,_,_ = List.nth lll idx2 in
- let _,_,diff = List.nth envs_and_diffs idx3 in
- diff
- | _,_ -> assert false
- in
- let newtxt =
- String.concat "\n"
- ("" ::
- List.map
- (fun k,desc ->
- let alias =
- match k with
- | DisambiguateTypes.Id id ->
- GrafiteAst.Ident_alias (id, desc)
- | DisambiguateTypes.Symbol (symb, i)->
- GrafiteAst.Symbol_alias (symb, i, desc)
- | DisambiguateTypes.Num i ->
- GrafiteAst.Number_alias (i, desc)
- in
- GrafiteAstPp.pp_alias alias)
- diff) ^ "\n"
- in
- source_buffer#insert
- ~iter:
- (source_buffer#get_iter_at_mark
- (`NAME "beginning_of_statement")) newtxt ;
- return ()
- );
- connect_button dialog#disambiguationErrorsMoreErrors
- (fun _ -> return () ; raise UseLibrary);
- connect_button dialog#disambiguationErrorsCancelButton fail;
- dialog#disambiguationErrors#show ();
- GtkThread.main ()
-
+ let newtxt =
+ String.concat "\n"
+ ("" ::
+ List.map
+ (fun k,desc ->
+ let alias =
+ match k with
+ | DisambiguateTypes.Id id ->
+ GrafiteAst.Ident_alias (id, desc)
+ | DisambiguateTypes.Symbol (symb, i)->
+ GrafiteAst.Symbol_alias (symb, i, desc)
+ | DisambiguateTypes.Num i ->
+ GrafiteAst.Number_alias (i, desc)
+ in
+ GrafiteAstPp.pp_alias alias)
+ diff) ^ "\n"
+ in
+ source_buffer#insert
+ ~iter:
+ (source_buffer#get_iter_at_mark
+ (`NAME "beginning_of_statement")) newtxt
+ | `HELP (* HELP MEANS MORE *) ->
+ dialog#toplevel#destroy () ;
+ raise UseLibrary
+ | `DELETE_EVENT -> ()
+ | _ -> assert false) ;
+ dialog#toplevel#destroy ()
+ ) ()
class gui () =
(* creation order _is_ relevant for windows placement *)
let main = new mainWin () in
let sequents_viewer =
MatitaMathView.sequentsViewer_instance main#sequentsNotebook in
- let fileSel = new fileSelectionWin () in
let findRepl = new findReplWin () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ main#mainWinEventBox ]
~website:"http://matita.cs.unibo.it"
()
in
+ ignore(about_dialog#event#connect#delete (fun _ -> true));
ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ()));
connect_menu_item main#contentsMenuItem (fun () ->
if 0 = Sys.command "which gnome-help" then
~callback:(fun _ -> hide_find_Repl ();true));
connect_menu_item main#undoMenuItem
(fun () -> (MatitaScript.current ())#safe_undo);
-(*CSC: XXX
- ignore(source_view#source_buffer#connect#can_undo
- ~callback:main#undoMenuItem#misc#set_sensitive);
-*) main#undoMenuItem#misc#set_sensitive true;
+ main#undoMenuItem#misc#set_sensitive false;
connect_menu_item main#redoMenuItem
(fun () -> (MatitaScript.current ())#safe_redo);
-(*CSC: XXX
- ignore(source_view#source_buffer#connect#can_redo
- ~callback:main#redoMenuItem#misc#set_sensitive);
-*) main#redoMenuItem#misc#set_sensitive true;
+ main#redoMenuItem#misc#set_sensitive false;
connect_menu_item main#editMenu (fun () ->
main#copyMenuItem#misc#set_sensitive
(MatitaScript.current ())#canCopy;
GtkThread.sync (fun () -> ()) ()
in
let worker_thread = ref None in
- let notify_exn (source_view : GSourceView2.source_view) exn =
+ let notify_exn (source_view : GSourceView3.source_view) exn =
let floc, msg = MatitaExcPp.to_string exn in
begin
match floc with
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);
with
exc -> script#source_view#misc#grab_focus (); raise exc in
- (* file selection win *)
- ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
- ignore (fileSel#fileSelectionWin#connect#response (fun event ->
- let return r =
- chosen_file <- r;
- fileSel#fileSelectionWin#misc#hide ();
- GMain.Main.quit ()
- in
- match event with
- | `OK ->
- let fname = fileSel#fileSelectionWin#filename in
- if Sys.file_exists fname then
- begin
- if HExtlib.is_regular fname && not (_only_directory) then
- return (Some fname)
- else if _only_directory && HExtlib.is_dir fname then
- return (Some fname)
- end
- else
- begin
- if _ok_not_exists then
- return (Some fname)
- end
- | `CANCEL -> return None
- | `HELP -> ()
- | `DELETE_EVENT -> return None));
(* menus *)
List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
(* console *)
current_page <- page;
let script = MatitaScript.at_page page in
script#activate;
+ main#undoMenuItem#misc#set_sensitive
+ script#source_view#source_buffer#can_undo ;
+ main#redoMenuItem#misc#set_sensitive
+ script#source_view#source_buffer#can_redo ;
main#saveMenuItem#misc#set_sensitive script#has_name))
method private externalEditor () =
save_moo script#status;
true
| `NO -> true
- | `CANCEL -> false
+ | `DELETE_EVENT -> false
else
(save_moo script#status; true)
console#message ("'"^file^"' loaded.");
self#_enableSaveTo file
- method private _enableSaveTo file =
+ method private _enableSaveTo _file =
self#main#saveMenuItem#misc#set_sensitive true
method private console = console
- method private fileSel = fileSel
method private findRepl = findRepl
method main = main
(fun _ -> callback ();true));
self#addKeyBinding GdkKeysyms._q callback
+ method private chooseFileOrDir ok_not_exists only_directory =
+ let fileSel = GWindow.file_chooser_dialog
+ ~action:`OPEN
+ ~title:"Select file"
+ ~modal:true
+ ~type_hint:`DIALOG
+ ~position:`CENTER
+ () in
+ fileSel#add_select_button_stock `OPEN `OK;
+ fileSel#add_button_stock `CANCEL `CANCEL;
+ ignore (fileSel#set_current_folder(Sys.getcwd ())) ;
+ let res =
+ let rec aux () =
+ match fileSel#run () with
+ | `OK ->
+ (match fileSel#filename with
+ None -> aux ()
+ | Some fname ->
+ if Sys.file_exists fname then
+ begin
+ if HExtlib.is_regular fname && not (only_directory) then
+ Some fname
+ else if only_directory && HExtlib.is_dir fname then
+ Some fname
+ else
+ aux ()
+ end
+ else if ok_not_exists then Some fname else aux ())
+ | `CANCEL -> None
+ | `DELETE_EVENT -> None in
+ aux () in
+ fileSel#destroy () ;
+ res
+
method private chooseFile ?(ok_not_exists = false) () =
- _ok_not_exists <- ok_not_exists;
- _only_directory <- false;
- fileSel#fileSelectionWin#show ();
- GtkThread.main ();
- chosen_file
+ self#chooseFileOrDir ok_not_exists false
method private chooseDir ?(ok_not_exists = false) () =
- _ok_not_exists <- ok_not_exists;
- _only_directory <- true;
- fileSel#fileSelectionWin#show ();
- GtkThread.main ();
(* we should check that this is a directory *)
- chosen_file
+ self#chooseFileOrDir ok_not_exists true
end
let interactive_string_choice
- text prefix_len ?(title = "") ?(msg = "") () ~id locs uris
+ text prefix_len ?(title = "") ?msg:(_ = "") () ~id:_ locs uris
=
+ GtkThread.sync (fun _ ->
let dialog = new uriChoiceDialog () in
dialog#uriEntryHBox#misc#hide ();
dialog#uriChoiceSelectedButton#misc#hide ();
dialog#uriChoiceTreeView#selection#set_mode
(`SINGLE :> Gtk.Tags.selection_mode);
let model = new stringListModel dialog#uriChoiceTreeView in
- let choices = ref None in
+ let choices = ref [] in
dialog#uriChoiceDialog#set_title title;
let hack_len = MatitaGtkMisc.utf8_string_length text in
let rec colorize acc_len = function
in
dialog#uriChoiceLabel#set_label txt;
List.iter model#easy_append uris;
- let return v =
- choices := v;
- dialog#uriChoiceDialog#destroy ();
- GMain.Main.quit ()
- in
- ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
connect_button dialog#uriChoiceForwardButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some uris));
- connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+ | uris -> choices := uris; dialog#toplevel#response `OK);
+ connect_button dialog#uriChoiceAbortButton (fun _ -> dialog#toplevel#response `DELETE_EVENT);
dialog#uriChoiceDialog#show ();
- GtkThread.main ();
- (match !choices with
- | None -> raise MatitaTypes.Cancel
- | Some uris -> uris)
+ let res =
+ match dialog#toplevel#run () with
+ | `DELETE_EVENT -> dialog#toplevel#destroy() ; raise MatitaTypes.Cancel
+ | `OK -> !choices
+ | _ -> assert false in
+ dialog#toplevel#destroy () ;
+ res) ()
let interactive_interp_choice () text prefix_len choices =
(*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)
let _ =
(* disambiguator callbacks *)
Disambiguate.set_choose_uris_callback
- (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg ->
+ (fun ~selection_mode ?ok ?enable_button_for_non_vars:(_=false) ~title ~msg ->
interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ());
Disambiguate.set_choose_interp_callback (interactive_interp_choice ());
(* gtk initialization *)
- GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
- ignore (GMain.Main.init ())
-
+ GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file (* loads gtk rc *)
projects / helm.git / commitdiff