more micro lean operators

Author: philzook58

src/kdrag/contrib/fast/__init__.py

@@ -36,15 +36,15 @@
 sys.path.insert(1, tmpdir)
 os.chdir(dir0)
 
-from _fast.lib import *  # noqa: E402, F403
+from _fast.lib import *  # noqa: E402, F403  # type: ignore
 
 
 def ctxptr(ctx: z3.Context):
-    return ffibuilder.cast("void *", ctx.ctx.value)
+    return ffibuilder.cast("void *", ctx.ctx.value)  # type: ignore
 
 
 def astptr(ast: z3.AstRef):
-    return ffibuilder.cast("void *", ast.as_ast().value)
+    return ffibuilder.cast("void *", ast.as_ast().value)  # type: ignore
 
 
 def intify(ptr):

src/kdrag/contrib/fast/fast.c

@@ -35,6 +35,7 @@ Z3_ast_vector KDRAG_get_consts(Z3_context ctx, Z3_ast t) {
   Z3_ast_vector_inc_ref(ctx, res);
   Z3_ast_vector todo = Z3_mk_ast_vector(ctx);
   Z3_ast_vector_inc_ref(ctx, todo);
+  // todo: seen set
   // Z3_ast_map seen = Z3_mk_ast_map(ctx);
   // Z3_ast_map_inc_ref(ctx, seen);
 

src/kdrag/contrib/pcode/__init__.py

@@ -145,7 +145,7 @@ def set_register(self, offset: int, value: smt.BitVecRef):
         return dataclasses.replace(
             self,
             mem=self.mem._replace(  # type: ignore
-                register=bv.StoreConcat(
+                register=bv.StoreConcat(  # type: ignore
                     self.mem.register,  # type: ignore
                     smt.BitVecVal(offset, self.bits),
                     value,

src/kdrag/parsers/microlean.py

@@ -1,41 +1,54 @@
+"""
+A parser for a simple logical expression language using Lark. The syntax is inspired by Lean's
+
+Unicode symbols are not required, but if you like them, adding the Unicode LaTeX extension for VSCode
+https://marketplace.visualstudio.com/items?itemName=oijaz.unicode-latex
+Goto the `File > Preferences > Settings` of the plugin and add `python` to the enabled extensions.
+Reloading your window will enable access via backslash autocomplete commands.
+For example \\alpha will tab autocomplete to α.
+"""
+
 import lark
 import kdrag.smt as smt
 from lark import Tree
 
 grammar = r"""
 start: expr
 
-?expr: quantifier
+?expr: ite
+?ite: quantifier | "if" expr "then" expr "else" expr -> if
 ?quantifier: implication  | ("forall" | "∀") binders "," expr  -> forall_ | \
-    ("exists" | "∃") binders "," expr -> exists_ | ("fun" | "λ") binders "=>" expr -> fun_
+    ("exists" | "∃") binders "," expr -> exists_ | ("fun" | "λ") binders ("=>" | "↦") expr -> fun_ | set
 ?implication: disjunction | disjunction ("->" | "→") implication  -> implies
-?disjunction: conjunction | disjunction ("\\/" | "∨" | "||") conjunction  -> or_
-?conjunction: comparison  | conjunction ("/\\" | "∧" | "&&") comparison  -> and_
+?disjunction: conjunction | disjunction ("\\/" | "∨" | "||" | "∪" ) conjunction  -> or_
+?conjunction: comparison  | conjunction ("/\\" | "∧" | "&&" | "∩") comparison  -> and_
 ?comparison: additive
     | comparison ("=" | "==") additive   -> eq  
     | comparison "!=" additive  -> neq
-    | comparison "<" additive   -> lt  
-    | comparison ">" additive   -> gt
-    | comparison "<=" additive  -> le  
-    | comparison ">=" additive  -> ge
+    | comparison ("<" | "⊂") additive   -> lt  
+    | comparison (">" | "⊃") additive   -> gt
+    | comparison ("<=" | "≤" | "⊆") additive  -> le  
+    | comparison (">=" | "≥" | "⊇") additive  -> ge
 ?additive: multiplicative
     | additive "+" multiplicative  -> add | additive "-" multiplicative  -> sub
 ?multiplicative: application
     | multiplicative "*" application  -> mul | multiplicative "/" application  -> div
 ?application: atom atom* -> app
 ?atom: const | num | bool_ | "(" expr ")" | seq
 
-binders: binder+
+binders: binder+ | NAME ":" sort -> sing_binder
 ?binder: "(" NAME+ ":" sort ")" -> annot_binder | NAME -> infer_binder
 ?sort: arrow
 ?arrow: sortatom | sortatom "->" arrow -> array
 ?sortatom : NAME -> sortlit | "BitVec" NUMBER -> bitvecsort | "(" sort ")" | "'" NAME -> typevar
 
-const: NAME
+const: NAME ("." NAME)*
 num: NUMBER
 bool_: "true" -> true | "false" -> false
 seq  : "[" expr ("," expr)* "]"
 
+set : "{" binders "|" expr "}"
+
 NAME: /[a-zA-Z_][a-zA-Z0-9_']*/
 NUMBER: /-?\d+/
 %import common.WS
@@ -79,6 +92,13 @@ def parse(s: str, globals=None) -> smt.ExprRef:
     True
     >>> parse("[true, false]")
     Concat(Unit(True), Unit(False))
+    >>> q = smt.Const("x", smt.TupleSort("pair", [smt.IntSort(), smt.BoolSort()])[0])
+    >>> parse("q.project1", {"q": q})
+    project1(x)
+    >>> parse("{x : Int | x > 0}")
+    Lambda(x, x > 0)
+    >>> parse("if true && false then 1 + 1 else 0")
+    If(And(True, False), 2, 0)
     """
     env = {}
 
@@ -139,10 +159,14 @@ def binders(tree) -> list[smt.ExprRef]:
         match tree:
             case Tree("binders", bs):
                 return [v for b in bs for v in binder(b)]
+            case Tree("sing_binder", [name, sort_tree]):
+                s = sort(sort_tree)
+                return [smt.Const(str(name), s)]
             case _:
                 raise ValueError("Unknown binders tree", tree)
 
     def quant(vs, body_tree, q) -> smt.QuantifierRef:
+        # TODO: doofy. Should make a env stack
         nonlocal env
         old_env = env.copy()
         vs = binders(vs)
@@ -157,8 +181,10 @@ def expr(tree) -> smt.ExprRef:
             # TODO: obviously this is not well typed.
             case Tree("num", [n]):
                 return int(n)  # type: ignore
-            case Tree("const", [name]):
+            case Tree("const", [name, *attrs]):
                 res = lookup(name)  # type: ignore
+                for attr in attrs:
+                    res = getattr(res, str(attr))  # type: ignore
                 return res  # type: ignore
             case Tree("true", []):
                 return smt.BoolVal(True)
@@ -213,6 +239,13 @@ def expr(tree) -> smt.ExprRef:
                 return quant(vs, body, smt.Exists)
             case Tree("fun_", [vs, body]):
                 return quant(vs, body, smt.Lambda)
+            case Tree("set", [vs, body]):
+                t = quant(vs, body, smt.Lambda)
+                if t.sort().range() != smt.BoolSort():
+                    raise ValueError("Set comprehension must return Bool", t)
+                return t
+            case Tree("if", [cond, then_, else_]):
+                return smt.If(expr(cond), expr(then_), expr(else_))
             case Tree("implies", [left, right]):
                 return smt.Implies(expr(left), expr(right))
             case _:

src/kdrag/theories/logic/zf.py

@@ -24,7 +24,7 @@
 Class = ZFSet >> smt.BoolSort()
 P, Q = smt.Consts("P Q", Class)
 
-elem = smt.Function("elem", ZFSet, ZFSet, smt.BoolSort())
+elem = smt.Function("∈", ZFSet, ZFSet, smt.BoolSort())
 elts = kd.define("elts", [A], smt.Lambda([x], elem(x, A)))
 
 zf_db = []
@@ -57,7 +57,7 @@ def slemma(thm, by=[], **kwargs):
 
 le = kd.notation.le.define([A, B], kd.QForAll([x], elem(x, A), elem(x, B)))
 
-emp = smt.Const("emp", ZFSet)
+emp = smt.Const("∅", ZFSet)
 elem_emp = kd.axiom(smt.ForAll([x], elem(x, emp) == smt.BoolVal(False)))
 
 
@@ -237,7 +237,7 @@ def sep_upair(l):
 
 # bigunion
 
-bigunion = smt.Function("bigunion", ZFSet, ZFSet)
+bigunion = smt.Function("bigunion", ZFSet, ZFSet)  # ⋃
 bigunion_ax = kd.axiom(
     kd.QForAll(
         [A, x], smt.Eq(elem(x, bigunion(A)), kd.QExists([B], elem(B, A), elem(x, B)))