Changes

9 changed files (+121/-70)

• images/canvas.webp (new)
• images/garden.webp > images/bg garden.webp
• lambcalc.py
  • @@ -4,6 +4,7 @@ # So no pattern matching sadly
    # Format with ruff format lambcalc.py # Must specify file or it'll mess with the vendored deps too + import sys from random import randrange from typing import Any, NamedTuple
  • @@ -23,8 +24,10 @@
    # Recursively substitute var with rep in term def sub(term, var, rep): if type(term) is L: - # Shadowing should never happen - assert term.var != var + # assert term.var != var + if term.var == var: + # Shadowing + return term return L(term.var, sub(term.body, var, rep)) if type(term) is A: return A(sub(term.fn, var, rep), sub(term.arg, var, rep))
  • @@ -57,6 +60,18 @@ return A(fn, red(term.arg))
    return term + # Simplify term using beta reduction without var renaming + def red_dumb(term): + if type(term) is L: + return L(term.var, red_dumb(term.body)) + if type(term) is A: + fn = red_dumb(term.fn) + if type(fn) is L: + return red_dumb(sub(fn.body, fn.var, term.arg)) + return A(fn, red_dumb(term.arg)) + return term + + # Rename vars using first available int # Input term must be reduced first def canonicalize(term, bound, free):
  • @@ -64,7 +79,7 @@ if type(term) is L:
    # Shadowing should never happen assert not term.var in bound if len(bound) == 0 and len(free) == 0: - var2 = 0 + var2 = 1 else: var2 = max((bound | free).values()) + 1 return L(var2, canonicalize(term.body, bound | {term.var: var2}, free))
  • @@ -75,7 +90,7 @@ )
    if term in bound: return bound[term] if len(bound) == 0 and len(free) == 0: - free[term] = 0 + free[term] = 1 elif not term in free: free[term] = max((bound | free).values()) + 1 return free[term]
  • @@ -95,7 +110,7 @@ def eq(term1, term2):
    return canonicalize(term1, {}, {}) == canonicalize(term2, {}, {}) - animals = "🦊🐱🐸🐷🐼🐶🐭🐻🐨🐯🐺🦁🐮🐹🐰🐵🦝🤔😱" + animals = "!🦊🐱🐸🐷🐼🐶🐭🐻🐨🐯🐺🦁🐮🐹🐰🐵🦝🤔😱" # Get friendly uncurried repr of canon term
  • @@ -139,9 +154,9 @@ lnil = L(1, ltrue)
    lnull = L(1, A(1, L(2, L(3, lfalse)))) ltree = L(1, L(2, L(3, A(A(1, 2), 3)))) ldatum = L(1, A(1, lfirst)) - left = L(1, A(A(1, lsecond), lfirst)) - right = L(1, A(1, lsecond)) - lincr = L(1, L(2, L(3, A(2, A(1, 3))))) + lleft = L(1, A(A(1, lsecond), lfirst)) + lright = L(1, A(1, lsecond)) + lincr = L(1, L(2, L(3, A(2, A(A(1, 2), 3))))) lplus = L(1, L(2, A(1, lincr))) ltimes = L(1, L(2, A(1, A(lplus, 2)))) liszero = L(1, A(A(1, L(2, lfalse)), ltrue))
  • @@ -155,7 +170,7 @@ lfive = L(1, L(2, A(1, A(1, A(1, A(1, A(1, 2)))))))
    lsix = L(1, L(2, A(1, A(1, A(1, A(1, A(1, A(1, 2)))))))) lseven = L(1, L(2, A(1, A(1, A(1, A(1, A(1, A(1, A(1, 2))))))))) leight = L(1, L(2, A(1, A(1, A(1, A(1, A(1, A(1, A(1, A(1, 2)))))))))) - lnine = L(1, L(2, A(1, A(1, A(1, A(1, A(1, A(1, A(1, A(1, A(1, 2)))))))))) + lnine = L(1, L(2, A(1, A(1, A(1, A(1, A(1, A(1, A(1, A(1, A(1, 2))))))))))) # Tests
  • @@ -190,7 +205,7 @@ for i in range(len(terms)):
    for j in range(len(terms)): newterms = terms.copy() try: - newterms[j] = red(A(terms[i], terms[j])) + newterms[j] = red_dumb(A(terms[i], terms[j])) # if size(newterms[j]) > 50: # Heuristic: stop if term is blowing up # continue
  • @@ -199,20 +214,19 @@ continue
    solve(newterms, moves + [i, j], depth - 1) - # Tech - # L(1, 2): make this and you instawin - # L(1, 1): identity - # K = L(1, L(2, 1)), L(1, L(2, L(3, 2))) autored toggle - if __name__ == "__main__": - import sys - sys.setrecursionlimit(50) - # solve([L(1, A(2, L(2, 1))), L(1, 1)], [], 6) - # solve([L(1, L(2, L(3, 1))), A(1, A(2, L(3, 4)))], [], 10) - # solve([L(1, L(2, 1)), L(1, A(A(A(A(1, 2), 3), 4), L(5, 6))), L(1, A(1, 1))], [], 8) + solve([L(1, A(1, 1)), L(2, L(1, 2)), A(A(A(A(1, 2), 3), 4), L(5, 6))], [], 9) + # [ + # A(1, A(2, A(3, 4))), + # L(1, L(2, 1)), + # L(2, L(3, 2)), + # L(3, L(4, 3)), + # L(1, 1), + # ], + # [], + # 10, + # ) - # solve([L(1, L(2, 1)), L(1, L(2, 1)), A(A(1, 2), L(1, 1))], [], 9) - - # solve([]) + # solve([L(1, L(2, 1)), L(1, A(A(A(A(1, 2), 3), 4), L(5, 6))), L(1, A(1, 1))], [], 8)
• level.rpy
  • @@ -10,13 +10,25 @@ narrator "Level [id]"
    while not all(type(term) is int for term in terms): # https://www.renpy.org/doc/html/statement_equivalents.html narrator "[i].1 Select eater" (interact=False) - $ fn = renpy.display_menu(list(zip(map(animal_repr, terms), range(N)))) + $ fn = renpy.display_menu(list(zip(map(animal_repr_canon, terms), range(N)))) narrator "[i].2 Select food" (interact=False) - $ arg = renpy.display_menu(list(zip(map(animal_repr, terms), range(N)))) + $ arg = renpy.display_menu(list(zip(map(animal_repr_canon, terms), range(N)))) + # $ terms[arg] = red(A(terms[fn], terms[arg])) # Replace arg because if we did the other way around # Then it would be impossible to get rid of A terms because they aren't funcs - $ terms[arg] = red(A(terms[fn], terms[arg])) + # How to destroy A terms??? + # It's impossible + # Because if we run it through a func + # Then if it ends up as an A.fn it's not reducible + # If it ends up as an A.arg we're just back where we started + # And if it's in a L.body the L can't capture free vars so it'll stay whole + # So we can't destroy A terms + # Unless we have L.body doesn't contain L.var + # So proposal: Disable alphaconv + # Then L *can* capture free vars and no vars ever get renamed + # So maybe then the puzzles will be more interesting? + $ terms[arg] = red_dumb(A(terms[fn], terms[arg])) $ i += 1 narrator "Level cleared! Select any option to continue." (interact=False) - $ renpy.display_menu(list(zip(map(animal_repr, terms), range(N)))) + $ renpy.display_menu(list(zip(map(animal_repr_canon, terms), range(N)))) return
• level.rpyc
• poetry.rpy
  • @@ -89,6 +89,10 @@ transform farleft:
    xalign -0.1 yalign 1.1 + transform canvas: + xalign 0.95 + yalign 0.1 + # OK this is gonna be super gross screen poetry(poem, rubypoem):
  • @@ -145,6 +149,7 @@
    label run_poetry_game(do_tutorial): scene bg garden + show canvas at canvas show shl at farleft show screen poetry(poem, rubypoem) with fade
  • @@ -258,3 +263,8 @@
    label poetry3: s "One last poem!" call run_poetry_game(False) + + s "Hope you had fun! Bye!" + stop music fadeout 2 + scene black with fade + $ renpy.quit()
• poetry.rpyc
• script.rpy
  • @@ -17,10 +17,10 @@ linear 0.1 matrixcolor TintMatrix("#FF0000") # Red again
    repeat parallel: - ease 0.05 xoffset -2 yoffset -3 rotate -2 - ease 0.05 xoffset 3 yoffset 2 rotate 2 - ease 0.05 xoffset -3 yoffset 2 rotate -3 - ease 0.05 xoffset 2 yoffset -3 rotate 3 + ease 0.05 xoffset -2 yoffset -1 rotate -1 + ease 0.05 xoffset 1 yoffset 2 rotate 2 + ease 0.05 xoffset -1 yoffset 2 rotate -2 + ease 0.05 xoffset 2 yoffset -1 rotate 1 repeat # Variant of say from screens.rpy
  • @@ -43,7 +43,6 @@ # Skip the main menu and immediately start the game
    label start: scene bg codebase show kublai - play music "push_ahead.ogg" k "Huh?" k "What are you doing here?"
  • @@ -59,14 +58,15 @@ label kublai_intro:
    k "Well I'm not really sure what happened to the usual homepage, but I guess just, uh, close the tab maybe?" k "You see, um, I'm not really being paid for this, so... not really sure what to say..." k "Oh! I remember now! You should totally download Kublai: Star Rail right this instant! I definitely wasn't paid to say that, I swear!" - scene white - show bg ksr at top with vpunch + play music "push_ahead.ogg" + scene white with vpunch + show bg ksr at top with zoomin k "Yes yes yes! Kublai: Star Rail! It's a critically acclaimed award-winning free-to-play turn-based mobile role-playing game, sequel to the one-and-only Genghis Impact!" - hide bg ksr with dissolve - show bg gi at top with dissolve + hide bg ksr + show bg gi at top k "You've heard of Genghis Impact at least, right? I mean like, Genghis did have a pretty big impact." hide bg gi - show bg ksr at top with vpunch + show bg ksr at top k "Well, trust me, Kublai: Star Rail is just the best thing ever, like who wouldn't want to build galactic railroads for the glory of the equally critically acclaimed and award-winning Mongol Empire?" show gopher at left with vpunch
  • @@ -267,7 +267,7 @@ show fenwick at right
    f "Don't panic! Stay calm and let's look around for possible exits." g "HEEEYYYY! I found something!" (screen="shake_say") - # We're mathematicians, we start level indexing from 1 + # We're math folks we start level indexing from 1 # Sadly Python is bad so the solution is 0-indexed # [0, 0] call level(1, [L(1, 2)])
  • @@ -287,60 +287,75 @@
    # [0, 1, 0, 0] call level(3, [L(1, 2), L(1, L(2, 3))]) - # [1, 0, 1, 1] - call level(4, [A(1, 2), L(1, 2)]) + # [1, 2, 1, 0, 1, 1] + call level(4, [L(1, 1), L(1, 2), A(1, A(2, 3))]) play music "strange_inspiration.ogg" fadeout 1.0 k "We did... something!" k "But I'm still pretty confused!" - # [1, 2, 1, 0, 1, 1] - call level(5, [L(1, 1), L(1, 2), A(1, A(2, 3))]) + # [0, 1, 1, 0, 0, 2, 0, 1, 0, 0] + call level(5, [L(1, L(2, 1)), A(2, 1), A(1, A(2, 3))]) - # [0, 0, 0, 2, 0, 2, 2, 0, 2, 1, 2, 2] + # [0, 0, 0, 0, 0, 2, 2, 0, 2, 1, 2, 2] call level(6, [L(1, L(2, A(1, A(2, L(3, 4))))), L(1, L(2, 2)), L(1, L(2, 1))]) - # Possible solutions - # [0, 0, 0, 2, 2, 0, 1, 0, 2, 0, 0, 1, 0, 2, 0, 0] - # [0, 2, 0, 2, 0, 2, 1, 2, 0, 2, 2, 0, 2, 1, 2, 2] - call level(7, [L(1, L(2, 1)), L(1, A(A(A(A(1, 2), 3), 4), L(5, 6))), L(1, A(1, 1))]) + # [0, 0, 0, 2, 1, 0, 2, 0, 0, 1, 0, 2, 0, 0] + call level(7, [L(1, L(2, 1)), L(1, A(A(A(1, 2), 3), L(4, 5))), L(1, A(1, 1))]) - # TODO - call level(8, [A(1, A(2, A(3, A(4, 5)))), L(1, L(2, 1)), L(1, 1), L(1, 1), L(1, 1), L(1, 1)]) + # [0, 1, 1, 0, 0, 1, 0, 2, 2, 1, 0, 1, 1, 0, 1, 2, 1, 1] + call level(8, [L(1, A(1, 1)), L(2, L(1, 2)), A(A(A(A(1, 2), 3), 4), L(5, 6))]) play music "nomogus41.ogg" fadeout 1.0 + k "Yay!! We're making progress!" - call level(9, []) + [0, 0, 1, 0, 0, 2, 3, 2, 2, 1, 1, 0, 1, 2, 1, 3, 1, 1] + call level(9, [A(1, A(2, A(3, L(4, 5)))), L(2, L(1, 2)), L(3, L(2, 3)), L(4, L(3, 4))]) - call level(10, []) + call level(10, [L(1, L(2, L(3, L(4, L(5, L(6, A(7, 8))))))), ]) + + play music "nightmarechipheavy3.144.ogg" fadeout 1.0 call level(11, []) call level(12, []) - play music "nightmarechipheavy3.144.ogg" fadeout 1.0 + play music "boundless2.ogg" fadeout 1.0 + scene bg bathroom + show shl at left + show kublai at right + with pixellate - call level(13, []) + s "Wow! We made it! We're back!" + s "Thanks for helping us with those puzzles!" + g "Awwwww no more puzzles..." - call level(14, []) - - call level(15, []) - - call level(16, []) - - play music "boundless2.ogg" fadeout 1.0 - # credits - # Dafny - # Isaac - # Music: https://opengameart.org/content/strange-inspiration + nvl_narrator "{size=69}Credits{/size}" + nvl_narrator "Made using Ren'Py, Krita, Rembg, ImageMagick, and a super buggy lambda calculus library that I wrote." + nvl_narrator "Special thanks to Rustan Leino for creating Dafny and investigating my proof of false!" + nvl_narrator "Music by https://opengameart.org/users/centurionofwar." + nvl_narrator "Inspired by my favorite webcomic, Proof of False, which you can find at proof-of-false.the-user.org on the Wayback Machine." + nvl_narrator "Happy (very belated) birthday Isaac!" + centered "{size=150}And thanks to you for playing!{/size}" (screen="shake_say") play music "push_ahead.ogg" fadeout 1.0 - #then they return back to the normal site and Kublai asks if they wanna hear the proof again and everyone screams, roll the credits, then show link to the proof of false webcomic and the usual homepage at /home.html - - # TODO: and you unlock a tang poetry minigame + k "Hey SHL, wanna hear my proof of false again?" + s "Oh no..." + k "What about you over there? Do you wanna hear it?" + menu: + "Nah": + k "Ah man. You're really missing out!" + k "Well have a nice day then. Seeya next time!" + stop music fadeout 2 + scene black with fade + $ renpy.quit() + "Sure!": + k "Cool, let's do it!" + s "DON'T YOU DARE..." + hide kublai with moveoutright + k "I'm kidding, I'm kidding, I swear!!" + label secret_ending: play music "happy_timepass.ogg" fadeout 1.0 + s "Hey, do you like poetry?" jump minigame - - # That's the end - # $ renpy.quit()
• script.rpyc