Fix/datatype uninterpreted sort

.github/workflows/ci.yml

@@ -2,6 +2,22 @@ name: CI
 on: [push, pull_request]
 
 jobs:
+  # Fast lint pass: ruff format, ruff check, mypy.
+  lint:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Install uv
+        uses: astral-sh/setup-uv@v5
+      - run: uv python install 3.12
+      - run: uv sync --dev
+      - name: ruff format
+        run: uv run ruff format --check .
+      - name: ruff check
+        run: uv run ruff check .
+      - name: mypy
+        run: uv run mypy lean_py/
+
   # Run the full test suite on Linux + macOS.
   test:
     strategy:

LeanPy/Z3.lean

@@ -247,7 +247,20 @@ partial def compileSort (varMap : Std.HashMap String Lean.Expr) : Z3Sort → Met
   | .uninterp name =>
     match varMap.get? name with
     | some e => return e
-    | none   => throwError s!"compileSort: unknown uninterpreted sort '{name}'"
+    | none => do
+      let tName := Name.mkSimple name
+      let env ← getEnv
+      if env.contains tName then return mkConst tName
+      else do
+        -- Auto-declare as an opaque type (axiom of sort Type)
+        let decl := Declaration.axiomDecl {
+          name := tName
+          levelParams := []
+          type := mkSort (.succ .zero)
+          isUnsafe := false
+        }
+        addDecl decl
+        return mkConst tName
   | .arrow dom cod => do
     let domExpr ← compileSort varMap dom
     let codExpr ← compileSort varMap cod
@@ -1000,7 +1013,8 @@ def z3Compile (expr : Z3Expr) : IO Lean.Expr := do
     let ctx ← LeanPy.Kernel.freshCoreContext
     let cs : Core.State := { env }
     let act : MetaM Lean.Expr := compileExpr {} expr
-    let (r, _) ← (act.run' {} {}).toIO ctx cs
+    let (r, cs') ← (act.run' {} {}).toIO ctx cs
+    LeanPy.Kernel.envRef.set (some cs'.env)
     return r
 
 @[python "z3_goal_create_expr"]

examples/04_sympy_tactic/python/lean_to_sympy.py

@@ -16,7 +16,7 @@
 from typing import TYPE_CHECKING
 
 import sympy
-from sympy import Integer, Symbol, Eq, simplify
+from sympy import Eq, Integer, Symbol, simplify
 
 from lean_py.marshal import LeanInductiveValue
 
@@ -28,6 +28,7 @@
 #  Name helpers
 # ---------------------------------------------------------------------------
 
+
 def name_to_str(name: LeanInductiveValue) -> str:
     """Walk a ``Lean.Name`` ADT (anonymous / str / num) to a dot-separated string."""
     parts: list[str] = []
@@ -53,13 +54,14 @@ def name_to_str(name: LeanInductiveValue) -> str:
 #  Expr helpers
 # ---------------------------------------------------------------------------
 
+
 def uncurry_app(expr: LeanInductiveValue) -> tuple[LeanInductiveValue, list[LeanInductiveValue]]:
     """Flatten nested ``Expr.app(f, x)`` into ``(head, [arg0, arg1, ...])``."""
     args: list[LeanInductiveValue] = []
     cur = expr
     while cur.ctor == "app":
-        args.append(cur._1)   # arg
-        cur = cur._0          # fn
+        args.append(cur._1)  # arg
+        cur = cur._0  # fn
     args.reverse()
     return cur, args
 
@@ -72,19 +74,24 @@ def uncurry_app(expr: LeanInductiveValue) -> tuple[LeanInductiveValue, list[Lean
 # For elaborated Lean expressions, the first few args are type/instance params;
 # we only look at the *last N* arguments.
 
+
 def _binop(op):
     """Return a builder for a binary operation (last 2 args)."""
+
     def build(args):
         a = expr_to_sympy(args[-2])
         b = expr_to_sympy(args[-1])
         return op(a, b)
+
     return 2, build
 
 
 def _unop(op):
     """Return a builder for a unary operation (last 1 arg)."""
+
     def build(args):
         return op(expr_to_sympy(args[-1]))
+
     return 1, build
 
 
@@ -93,11 +100,11 @@ def build(args):
     "HSub.hSub": _binop(lambda a, b: a - b),
     "HMul.hMul": _binop(lambda a, b: a * b),
     "HDiv.hDiv": _binop(lambda a, b: a / b),
-    "HPow.hPow": _binop(lambda a, b: a ** b),
-    "Eq":        (2, lambda args: Eq(expr_to_sympy(args[-2]), expr_to_sympy(args[-1]))),
-    "Neg.neg":   _unop(lambda x: -x),
+    "HPow.hPow": _binop(lambda a, b: a**b),
+    "Eq": (2, lambda args: Eq(expr_to_sympy(args[-2]), expr_to_sympy(args[-1]))),
+    "Neg.neg": _unop(lambda x: -x),
     "HNeg.hNeg": _unop(lambda x: -x),
-    "Nat.succ":  (1, lambda args: expr_to_sympy(args[-1]) + 1),
+    "Nat.succ": (1, lambda args: expr_to_sympy(args[-1]) + 1),
     "Int.ofNat": (1, lambda args: expr_to_sympy(args[-1])),
     "Int.negSucc": (1, lambda args: -(expr_to_sympy(args[-1]) + 1)),
 }
@@ -175,6 +182,7 @@ def expr_to_sympy(expr: LeanInductiveValue) -> sympy.Basic:
 #  Proposition checkers
 # ---------------------------------------------------------------------------
 
+
 def sympy_prop_check(prop: sympy.Basic) -> bool:
     """Check if a SymPy proposition is identically true."""
     s = simplify(prop)
@@ -206,9 +214,7 @@ def decode_and_check_prop(lean_obj) -> bool:
     Called from the Lean tactic via ``Py.ofLeanObj`` + ``@[python]``.
     """
     if _marshaller is None:
-        raise RuntimeError(
-            "lean_to_sympy.setup(lib) must be called before decode_and_check_prop"
-        )
+        raise RuntimeError("lean_to_sympy.setup(lib) must be called before decode_and_check_prop")
     expr_tree = _marshaller.decode_lean_obj("Lean.Expr", lean_obj)
     prop = expr_to_sympy(expr_tree)
     return sympy_prop_check(prop)

examples/05_knuckledragger/python/lean_to_z3.py

@@ -28,6 +28,7 @@
 #  Name helpers
 # ---------------------------------------------------------------------------
 
+
 def name_to_str(name: LeanInductiveValue) -> str:
     """Walk a ``Lean.Name`` ADT (anonymous / str / num) to a dot-separated string."""
     parts: list[str] = []
@@ -53,13 +54,14 @@ def name_to_str(name: LeanInductiveValue) -> str:
 #  Expr helpers
 # ---------------------------------------------------------------------------
 
+
 def uncurry_app(expr: LeanInductiveValue) -> tuple[LeanInductiveValue, list[LeanInductiveValue]]:
     """Flatten nested ``Expr.app(f, x)`` into ``(head, [arg0, arg1, ...])``."""
     args: list[LeanInductiveValue] = []
     cur = expr
     while cur.ctor == "app":
-        args.append(cur._1)   # arg
-        cur = cur._0          # fn
+        args.append(cur._1)  # arg
+        cur = cur._0  # fn
     args.reverse()
     return cur, args
 
@@ -81,15 +83,18 @@ def _var(name: str) -> z3.ArithRef:
 #  Main converter
 # ---------------------------------------------------------------------------
 
+
 def _binop(op):
     def build(args):
         return op(expr_to_z3(args[-2]), expr_to_z3(args[-1]))
+
     return 2, build
 
 
 def _unop(op):
     def build(args):
         return op(expr_to_z3(args[-1]))
+
     return 1, build
 
 
@@ -98,11 +103,11 @@ def build(args):
     "HSub.hSub": _binop(lambda a, b: a - b),
     "HMul.hMul": _binop(lambda a, b: a * b),
     "HDiv.hDiv": _binop(lambda a, b: a / b),
-    "HPow.hPow": _binop(lambda a, b: a ** b),
-    "Eq":        (2, lambda args: expr_to_z3(args[-2]) == expr_to_z3(args[-1])),
-    "Neg.neg":   _unop(lambda x: -x),
+    "HPow.hPow": _binop(lambda a, b: a**b),
+    "Eq": (2, lambda args: expr_to_z3(args[-2]) == expr_to_z3(args[-1])),
+    "Neg.neg": _unop(lambda x: -x),
     "HNeg.hNeg": _unop(lambda x: -x),
-    "Nat.succ":  (1, lambda args: expr_to_z3(args[-1]) + 1),
+    "Nat.succ": (1, lambda args: expr_to_z3(args[-1]) + 1),
     "Int.ofNat": (1, lambda args: expr_to_z3(args[-1])),
     "Int.negSucc": (1, lambda args: -(expr_to_z3(args[-1]) + 1)),
 }
@@ -179,6 +184,7 @@ def expr_to_z3(expr: LeanInductiveValue):
 #  Proposition checkers
 # ---------------------------------------------------------------------------
 
+
 def check_prop(prop) -> bool:
     """Check a proposition via Knuckledragger (backed by Z3)."""
     try:
@@ -208,9 +214,7 @@ def decode_and_check_prop(lean_obj) -> bool:
     Called from the Lean tactic via ``Py.ofLeanObj`` + ``@[python]``.
     """
     if _marshaller is None:
-        raise RuntimeError(
-            "lean_to_z3.setup(lib) must be called before decode_and_check_prop"
-        )
+        raise RuntimeError("lean_to_z3.setup(lib) must be called before decode_and_check_prop")
     expr_tree = _marshaller.decode_lean_obj("Lean.Expr", lean_obj)
     prop = expr_to_z3(expr_tree)
     return check_prop(prop)

examples/05_knuckledragger/python/main.py

@@ -59,7 +59,6 @@ def mk_eq(lhs, rhs):
             rhs,
         )
 
-    import z3
 
     print("== expr_to_z3 ==")
 

examples/06_effectful_verifier/python/main.py

@@ -15,18 +15,19 @@
 from pathlib import Path
 from typing import Annotated
 
+from refine import Ge, Gt, assert_refined, verify_function
+
 from lean_py import LeanLibrary
 from lean_py.kernel import Kernel
 
-from refine import Gt, Ge, assert_refined, verify_function
-
 lake_dir = Path(__file__).resolve().parent.parent / "lean"
 lib = LeanLibrary.from_lake(lake_dir, "EffectfulVerifier", build=True)
 
 kernel = Kernel(lib)
 kernel.init_search("")
 kernel.load(["Init"])
 
+
 def verify(fn):
     all_ok = True
     for msg, ok in verify_function(fn, lib, kernel):
@@ -42,22 +43,29 @@ def verify(fn):
 #  Programs under verification
 # ---------------------------------------------------------------------------
 
+
 def positive_increment(x: Annotated[int, Gt(0)]):
     y = x + 3
-    assert_refined(y, Gt(3))      # x > 0 → x + 3 > 3   ✓
+    assert_refined(y, Gt(3))  # x > 0 → x + 3 > 3   ✓
     z = x + 10
-    assert_refined(z, Gt(10))     # x > 0 → x + 10 > 10  ✓
+    assert_refined(z, Gt(10))  # x > 0 → x + 10 > 10  ✓
+
+
 assert verify(positive_increment)
 
+
 def bounded_sum(x: Annotated[int, Gt(0)], y: Annotated[int, Gt(0)]):
     s = x + y
-    assert_refined(s, Gt(1))      # x > 0 ∧ y > 0 → x + y > 1   ✓
-    assert_refined(s, Ge(2))      # x > 0 ∧ y > 0 → x + y >= 2  ✓
+    assert_refined(s, Gt(1))  # x > 0 ∧ y > 0 → x + y > 1   ✓
+    assert_refined(s, Ge(2))  # x > 0 ∧ y > 0 → x + y >= 2  ✓
+
+
 assert verify(bounded_sum)
 
 
 def failing(x: Annotated[int, Gt(0)]):
     y = x + 1
-    assert_refined(y, Gt(10))     # x > 0 → x + 1 > 10  ✗
-assert not verify(failing)
+    assert_refined(y, Gt(10))  # x > 0 → x + 1 > 10  ✗
+
 
+assert not verify(failing)