added doctest

Author: philzook58

kdrag/contrib/prolog/__init__.py

@@ -1 +1,79 @@
+import kdrag.smt as smt
 import lark
+
+grammar = r"""
+    start: _statement*
+
+    _statement: fact
+             | rule
+             | query
+
+    fact: predicate "."
+    rule: predicate ":-" predicate_list "."
+    query: "?-" predicate_list "."
+
+    predicate_list: predicate ("," predicate)* // inlined
+
+    predicate: IDENTIFIER "(" term_list? ")"
+    term_list: term ("," term)* // inlined
+
+    term: IDENTIFIER    -> const          // constants or functors
+        | VARIABLE      -> var          // variables
+        | IDENTIFIER "(" term_list ")" -> fun_app  // recursive terms (e.g., s(X))
+
+    VARIABLE: /[A-Z][A-Za-z0-9_]*/  // Variables start with uppercase
+    IDENTIFIER: /[a-z][A-Za-z0-9_]*/  // Constants and function names start with lowercase
+
+    %import common.WS
+    %ignore WS
+"""
+
+Term = smt.DeclareSort("Term")
+
+
+def interp_term(t):
+    token = t.data
+    if token == "const":
+        return smt.Const(t.children[0], Term)
+    elif token == "var":
+        return smt.Const(t.children[0], Term)
+    elif token == "fun_app":
+        args = t.children[1].children
+        sortlist = [Term] * (len(args) + 1)
+        f = smt.Function(t.children[0], *sortlist)
+        return f(*[interp_term(a) for a in args])
+    else:
+        raise ValueError(f"Unexpected term {t}")
+
+
+def interp_pred(t):
+    assert t.data == "predicate"
+    name = t.children[0]
+    args = [interp_term(a) for a in t.children[1].children]
+    return smt.Function(name, *([Term] * len(args)), smt.BoolSort())(*args)
+
+
+def interp(t):
+    assert t.data == "start"
+    clauses = []
+    for stmt in t.children:
+        if stmt.data == "fact":
+            clauses.append(interp_pred(stmt.children[0]))
+        elif stmt.data == "rule":
+            head = interp_pred(stmt.children[0])
+            predlist = stmt.children[1]
+
+            assert predlist.data == "predicate_list"
+            body = [
+                interp_pred(p) for p in [stmt.children[0]] + stmt.children[1].children
+            ]
+            clauses.append(smt.Implies(smt.And(*body), head))
+        elif stmt.data == "query":
+            q = [interp_pred(p) for p in stmt.children[0].children]
+            print("query", q)
+        else:
+            raise ValueError(f"Unexpected statement {stmt}")
+    return clauses
+
+
+parser = lark.Lark(grammar, start="start", parser="lalr")

kdrag/kernel.py

@@ -59,10 +59,10 @@ def lemma(
     Returns:
         Proof: A proof object of thm
 
-    >>> lemma(BoolVal(True))
-
-    >>> lemma(RealVal(1) >= RealVal(0))
-
+    >>> lemma(smt.BoolVal(True))
+    |- True
+    >>> lemma(smt.RealVal(1) >= smt.RealVal(0))
+    |- 1 >= 0
     """
     if admit:
         logger.warning("Admitting lemma {}".format(thm))

kdrag/parsers/prolog.py

@@ -132,9 +132,11 @@ def lemma(
     Returns:
         Proof: A proof object of thm
 
-    >>> lemma(BoolVal(True))
+    >>> lemma(smt.BoolVal(True))
+    |- True
 
-    >>> lemma(RealVal(1) >= RealVal(0))
+    >>> lemma(smt.RealVal(1) >= smt.RealVal(0))
+    |- 1 >= 0
 
     """
     if kd.kernel.is_proof(by):
@@ -394,6 +396,9 @@ def exists(self, *ts):
         """
         Give terms `ts` to satisfy an exists goal
         `?|- exists x, p(x)` becomes `?|- p(ts)`
+        >>> x,y = smt.Ints("x y")
+        >>> Lemma(smt.Exists([x], x == y)).exists(y)
+        [] ?|- y == y
         """
         ctx, goal = self.goals[-1]
         lemma = kd.kernel.forget2(ts, goal)

kdrag/tactics.py

@@ -0,0 +1,5 @@
+[pytest]
+# Exclude specific directories
+norecursedirs = kdrag/solvers/eprover kdrag/solvers/gappa* kdrag/solvers/Prover9
+
+addopts = --doctest-modules

pytest.ini

@@ -1,5 +1,5 @@
 import kdrag.parsers as parsers
-import kdrag.parsers.prolog as prolog
+import kdrag.contrib.prolog as prolog
 import kdrag.parsers.tptp as tptp
 import kdrag.parsers.smtlib as smtlib
 import lark