| 12 | |
| 13 | |
| 14 | def main() -> None: |
| 15 | lake_dir = Path(__file__).resolve().parent.parent / "lean" |
| 16 | lib = LeanLibrary.from_lake(lake_dir, "KnuckleTactic", build=True) |
| 17 | |
| 18 | import lean_to_z3 |
| 19 | from lean_to_z3 import expr_to_z3 |
| 20 | |
| 21 | # Wire up the marshaller for Path B (tactic decode). |
| 22 | lean_to_z3.setup(lib) |
| 23 | |
| 24 | Name = lib.Name |
| 25 | Expr = lib.Expr |
| 26 | Literal = lib.Literal |
| 27 | |
| 28 | def mk_name(s: str): |
| 29 | parts = s.split(".") |
| 30 | n = Name.anonymous |
| 31 | for p in parts: |
| 32 | n = Name.str(n, p) |
| 33 | return n |
| 34 | |
| 35 | def mk_const(s: str): |
| 36 | return Expr.const(mk_name(s), []) |
| 37 | |
| 38 | def mk_nat(n: int): |
| 39 | return Expr.app( |
| 40 | Expr.app( |
| 41 | Expr.app(mk_const("OfNat.ofNat"), mk_const("Nat")), |
| 42 | Expr.lit(Literal.natVal(n)), |
| 43 | ), |
| 44 | mk_const("inst"), |
| 45 | ) |
| 46 | |
| 47 | def mk_binop(op_name: str, a, b): |
| 48 | op = mk_const(op_name) |
| 49 | for _ in range(4): |
| 50 | op = Expr.app(op, mk_const("inst")) |
| 51 | return Expr.app(Expr.app(op, a), b) |
| 52 | |
| 53 | def mk_eq(lhs, rhs): |
| 54 | return Expr.app( |
| 55 | Expr.app( |
| 56 | Expr.app(mk_const("Eq"), mk_const("Nat")), |
| 57 | lhs, |
| 58 | ), |
| 59 | rhs, |
| 60 | ) |
| 61 | |
| 62 | |
| 63 | print("== expr_to_z3 ==") |
| 64 | |
| 65 | one = mk_nat(1) |
| 66 | two = mk_nat(2) |
| 67 | expr_add = mk_binop("HAdd.hAdd", one, one) |
| 68 | z3_add = expr_to_z3(expr_add) |
| 69 | print(f" 1 + 1 -> {z3_add}") |
| 70 | |
| 71 | z3_eq = expr_to_z3(mk_eq(expr_add, two)) |