Skip to content

Instantly share code, notes, and snippets.

@johnynek
Last active August 16, 2020 02:57
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save johnynek/5b75c21a055a8883c624f3ef3128afb2 to your computer and use it in GitHub Desktop.
Save johnynek/5b75c21a055a8883c624f3ef3128afb2 to your computer and use it in GitHub Desktop.
first example of (terrible) python code generation from bosatsu.
def times2(___bn2):
if ___bn2 == 0:
return 0
else:
___a0 = ___bn2 - 1
___bprev2 = ___a0
return times2(___bprev2) + 2
def add(___bn12):
if ___bn12 == 0:
return lambda ___bn24: ___bn24
else:
___a2 = ___bn12 - 1
___bprev__n12 = ___a2
def ___t4(___bn25):
if ___bn25 == 0:
return ___bn12
else:
___a1 = ___bn25 - 1
___bprev__n22 = ___a1
return add(___bprev__n12)(___bprev__n22) + 2
return ___t4
def mult(___bn17):
if ___bn17 == 0:
return lambda ___bn212: 0
else:
___a4 = ___bn17 - 1
___bn18 = ___a4
def ___t8(___bn213):
if ___bn213 == 0:
return 0
else:
___a3 = ___bn213 - 1
___bn214 = ___a3
return add(mult(___bn18)(___bn214))(add(___bn18)(___bn214)) + 1
return ___t8
def ___bloop0(___bacc1):
def ___t18(___bn5):
___t16 = True
___t14 = ___bacc1
___t15 = ___bn5
___t17 = ()
while ___t16:
___t16 = False
if ___t15 == 0:
___t17 = ___t14
else:
___a5 = ___t15 - 1
___bn6 = ___a5
___t16 = True
___t14 = ___t14 + 1
___t15 = ___bn6
___t17 = ()
return ___t17
return ___t18
to_Int = ___bloop0(0)
def to_Nat(___bi2):
___t25 = 0 < ___bi2
___t26 = 0
___t27 = ___bi2
___t28 = 0
while ___t25:
___t26 = (lambda ___bi3: lambda ___bnat1: (___bi3 - 1, (___bnat1 + 1,
())))(___t27)(___t28)
___t29 = ___t26[0]
___t28 = ___t26[1][0]
___t25 = (0 < ___t29) and (___t29 < ___t27)
___t27 = ___t29
return ___t28
n1 = 1
n2 = n1 + 1
n3 = n2 + 1
n4 = n3 + 1
n5 = n4 + 1
n6 = n5 + 1
def ___noperator_W__z__z_(___bi01):
def ___t36(___bi11):
if ___bi01 < ___bi11:
___a6 = 0
elif ___bi01 == ___bi11:
___a6 = 1
else:
___a6 = 2
___a7 = ___a6
___t35 = ___a6 == 1
if ___t35:
return 1
else:
return 0
return ___t36
def addLaw(___bn110):
return lambda ___bn216: lambda ___t38: (0,
___noperator_W__z__z_(to_Int(add(___bn110)(___bn216)))(to_Int(___bn110) + to_Int(___bn216)),
___t38)
def multLaw(___bn112):
return lambda ___bn218: lambda ___t40: (0,
___noperator_W__z__z_(to_Int(mult(___bn112)(___bn218)))(to_Int(___bn112) * to_Int(___bn218)),
___t40)
def from_to_law(___bi5):
return lambda ___t42: (0,
___noperator_W__z__z_(to_Int(to_Nat(___bi5)))(___bi5), ___t42)
from_to_suite = (1, "to_Nat/to_Int tests", (1, (0,
___noperator_W__z__z_(to_Int(to_Nat(-1)))(0), "-1 -> 0"), (1, (0,
___noperator_W__z__z_(to_Int(to_Nat(-42)))(0), "-42 -> 0"), (1,
from_to_law(0)("0"), (1, from_to_law(1)("1"), (1, from_to_law(10)("10"), (1,
from_to_law(42)("42"), 0)))))))
tests = (1, "Nat tests", (1, addLaw(0)(0)("0 + 0"), (1, addLaw(0)(n1)("0 + 1"),
(1, addLaw(n1)(0)("1 + 0"), (1, addLaw(n1)(n2)("1 + 2"), (1,
addLaw(n2)(n1)("2 + 1"), (1, multLaw(0)(0)("0 * 0"), (1,
multLaw(0)(n1)("0 * 1"), (1, multLaw(n1)(0)("1 * 0"), (1,
multLaw(n1)(n2)("1 * 2"), (1, multLaw(n2)(n1)("2 * 1"), (1, from_to_suite,
0))))))))))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment