lark cache is fishy

Author: philzook58

examples/soft_found/lf/indprop.py

@@ -47,7 +47,7 @@
     "| Collatz_holds_for.chf_odd sub => (even n = false) /\\ collatz_holds_for_wf sub ((3 * n) + 1)"
 )
 
-print(collatz_holds_for_wf.defn)
+# print(collatz_holds_for_wf.defn)
 
 
 @kd.Theorem("exists (ev : Collatz_holds_for), collatz_holds_for_wf ev 1")
@@ -57,6 +57,7 @@ def collatz_1(pf):
     pf.auto(by=[collatz_holds_for_wf.defn])
 
 
+"""
 try:
     # We cannot yet finish this without better evaluation of recursive defines.
     @kd.Theorem("exists (ev : Collatz_holds_for), collatz_holds_for_wf ev 12")
@@ -69,7 +70,7 @@ def collatz_12(pf):
         pf.auto(by=[collatz_holds_for_wf.defn, div2.defn])
 except Exception as err:
     print("Expected failure (needs better Collatz evaluation):", err)
-
+"""
 
 # --------------------------------------------------------------------
 # A binary relation for <= on Nat.

src/kdrag/parsers/tptp.py

@@ -115,14 +115,14 @@
 """
 
 
-term_parser = lark.Lark(fof_grammar, start="term", parser="lalr", cache=True)
+term_parser = lark.Lark(fof_grammar, start="term", parser="lalr", cache=False)
 fof_parser = lark.Lark(fof_grammar, start="start", parser="lalr", cache=True)
 
 
 def test():
     """
     >>> term_parser.parse("f(Xy1,g(y23))")
-    Tree('fun_app', [Token('NAME', 'f'), Tree('arguments', [Tree('var', [Token('UPPER_WORD', 'Xy1')]), Tree('fun_app', [Token('NAME', 'g'), Tree('arguments', [Tree('const', [Token('NAME', 'y23')])])])])])
+    Tree('fun_app', [Token('NAME', 'f'), Tree(Token('RULE', 'arguments'), [Tree('var', [Token('UPPER_WORD', 'Xy1')]), Tree('fun_app', [Token('NAME', 'g'), Tree(Token('RULE', 'arguments'), [Tree('const', [Token('NAME', 'y23')])])])])])
     """