kdrag.reflect.reflect

kdrag.reflect.reflect(f, globals=None, by=[]) → FuncDeclRef

Reflect a function definition by injecting the parameters and recursive self call into the local environment. Uses type annotations to do so.

Only handles a purely functional subset of python. Simple assignment is handled as a let who’s scope extends to the end of it’s subbranch. Every branch must end with a return.

You can still call original function under attribute __wrapped__.

>>> def foo(x : int) -> int:
...     return x + 3
>>> foo = reflect(foo)
>>> foo.__wrapped__(3)
6
>>> foo.defn
|= ForAll(x, foo(x) == x + 3)

>>> @reflect
... def bar(x : int, y : str) -> int:
...     if x > 4:
...         return x + 3
...     elif y == "fred":
...        return 14
...     else:
...        return bar(x - 1, y)
>>> bar.defn
|= ForAll([x, y],
       bar(x, y) ==
       If(x > 4, x + 3, If(y == "fred", 14, bar(x - 1, y))))
>>> @reflect
... def buzzy(n: int) -> int:
...     if n == 0:
...         assert n == 0
...         x = 1
...         y = x
...     else:
...         y = 2
...     return y
>>> @reflect
... def coverage(x : int) -> int:
...     if x + 1 > x:
...         return x
>>> z = smt.Int("z")
>>> @reflect
... def inc_78(n: int, m : "smt.Lambda([z], smt.And(z > 0, z > n))") -> "smt.Lambda([z], z > n)":
...    return n + m
>>> #test_match54.defn
>>> @reflect
... def test_add32(x : kd.Nat, y : kd.Nat) -> kd.Nat:
...     match x:
...         case S(n):
...             return kd.Nat.S(test_add32(n, y))
...         case Z():
...             return y
>>> test_add32.defn
|= ForAll([x, y],
    test_add32(x, y) ==
    If(is(S, x), S(test_add32(pred(x), y)), y))
>>> @reflect
... def test_match54(x: "int", y: int) -> int:
...     match x:
...         case 0:
...             return y
...         case _ if y > 0:
...             return y + 1
...         case _:
...             return y - 1
>>> test_match54.defn
|= ForAll([x, y],
    test_match54(x, y) ==
    If(x == 0, y, If(y > 0, y + 1, y - 1)))
>>> @reflect
... def test_false_pre(x: smt.Lambda([z], z != z)) -> int:
...     assert False
...     return 42
>>> @reflect
... def test_false_match(x: int)-> int:
...     match x:
...         case 4:
...             return x
...         case 4:
...             assert False
...             return x
...         case _:
...             return x
>>> @reflect
... def test_false_if(x: int, p : "smt.ExprRef # x > 0") -> "x > -1":
...     return ()
>>> @reflect
... def test_set_notation(x : "{x for x in int if x > 0}") -> "{y for y in int if y > x and y > 0}":
...     return x + 1
>>> test_set_notation.contract
|= ForAll(x,
    Implies(And(x > 0),
            Implies(And,
                    And(And(And(test_set_notation(x) > x,
                            test_set_notation(x) > 0))))))
>>> myconst = kd.define("myconst12345", [], smt.IntVal(42))
>>> @reflect
... def test_proof_call() -> "{y for y in int if y == myconst}":
...     if myconst != 42:
...         () = myconst.defn
...         assert False
...         return 0
...     else:
...         return 42
>>> test_proof_call.contract
|= Implies(And, And(And(test_proof_call == myconst12345)))
>>> @reflect
... def test_tuple(x : tuple[int, tuple[bool, int]]) -> bool:
...     (_, (b, y)) = x
...     return b
>>> @reflect
... def test_forloop(x : int) -> "{y for y in int if y == x + 6}":
...     for i in range(4):
...         x = x + i
...     return x

Return type:

FuncDeclRef