<reponame>BenWiederhake/general_purpose_fixedpoint<filename>general_purpose_proof.py
#!/usr/bin/env python3

## The "format" is explained in `run`.
#def old_safe_eval(code, sim_input):
#    if not isinstance(code, str):
#        raise TypeError('Lolwut?  Attempted to run non-str code (was {})')
#    given = dict()
#    given['input'] = sim_input
#    # Pass `safe_eval` for now.
#    # FIXME: Is this really not cheating?
#    given['safe_eval'] = old_safe_eval
#    the_locals = dict()
#    try:
#        exec(code, given, the_locals)
#    except BaseException as e:
#        raise e
#    return the_locals.get('output') or ''


def make_fixedpoint(transformation_code):
    quine_raw_fmt = '''\
def e(c, i):
    l = dict()
    exec(c, dict(input=i), l)
    return l.get('output') or ''
magic = %
own_code = magic.replace(chr(37), repr(magic))
output = e(e({0}, own_code), input)'''
    # The core magic is that:
    # - `make_fixedpoint` must be total, i.e., always halt
    # - `transformation_code` must be total, i.e. always halt
    # - The code generated by `make_fixedpoint` is allowed to diverge.
    # Therefore, we (`make_fixedpoint`) can generate a quine, i.e. get
    # a handle on our own source code.  Then, we call the transformation on it.
    # This means that the transformation cannot possibly distinguish whether it
    # is currently run during the quine, or being run by the judge.
    # Therefore, It must spit out the same code in both situations.
    # The rest is easy: just run the result of the transformation, and we're done.
    quine_raw = quine_raw_fmt.format(repr(transformation_code))
    return quine_raw.replace('%', repr(quine_raw))


def run():
    def e(c, i):
        l = dict()
        exec(c, dict(input=i), l)
        return l.get('output') or ''

    print('Write your transformation on a single line, then press ENTER.')
    print('The input will be given as the *variable* `input`.')
    print('Write the output into the variable `output`, do not print it!')
    print('Note that it has to be a *transformation*, so both input and output are programs.')
    # FIXME: Currently reads only 1 line
    transformation_code = input('>>> ')
    fixedpoint_code = make_fixedpoint(transformation_code)
    f_fixedpoint_code = e(transformation_code, fixedpoint_code)
    print()
    print('# The fixed-point code `e` is:')
    print(fixedpoint_code)
    print()
    print('# In order to show the theorem, this should have the same effect as the code `F(e)`,')
    print('# i.e., the code after running it *once* through your transformation:')
    print(f_fixedpoint_code)
    print()
    print()
    print('# If you want to run it, enter anything (not necessarily code)')
    print('# and press ENTER. If you want to exit, just press ENTER:')
    try:
        noncode_input = input('>>> ')
    except EOFError:
        print('# Have a nice day! :)')
        exit(0)
    except KeyboardInterrupt:
        print('# Alrighty, bye! :)')
        exit(0)
    if not noncode_input:
        print('# Exit it is; have fun! :)')
        exit(0)

    print()
    print()
    print('# First, run it with the (second) transformed code:')
    transformed_output = e(f_fixedpoint_code, noncode_input)
    print(transformed_output)
    print()
    print('# Finally, run it with the (first) "fixed-point" code:')
    fp_output = e(fixedpoint_code, noncode_input)
    print(fp_output)
    print()
    if fp_output == transformed_output:
        print('# They are equal!  Told ya so! :D')
    else:
        print('# Ahh shit.  They differ.  Please open an issue!')
        print('# https://github.com/BenWiederhake/general_purpose_fixedpoint/issues/new')


if __name__ == '__main__':
    run()

#!/usr/bin/env python3

## The "format" is explained in `run`.
#def old_safe_eval(code, sim_input):
#    if not isinstance(code, str):
#        raise TypeError('Lolwut?  Attempted to run non-str code (was {})')
#    given = dict()
#    given['input'] = sim_input
#    # Pass `safe_eval` for now.
#    # FIXME: Is this really not cheating?
#    given['safe_eval'] = old_safe_eval
#    the_locals = dict()
#    try:
#        exec(code, given, the_locals)
#    except BaseException as e:
#        raise e
#    return the_locals.get('output') or ''


def make_fixedpoint(transformation_code):
    quine_raw_fmt = '''\
def e(c, i):
    l = dict()
    exec(c, dict(input=i), l)
    return l.get('output') or ''
magic = %
own_code = magic.replace(chr(37), repr(magic))
output = e(e({0}, own_code), input)'''
    # The core magic is that:
    # - `make_fixedpoint` must be total, i.e., always halt
    # - `transformation_code` must be total, i.e. always halt
    # - The code generated by `make_fixedpoint` is allowed to diverge.
    # Therefore, we (`make_fixedpoint`) can generate a quine, i.e. get
    # a handle on our own source code.  Then, we call the transformation on it.
    # This means that the transformation cannot possibly distinguish whether it
    # is currently run during the quine, or being run by the judge.
    # Therefore, It must spit out the same code in both situations.
    # The rest is easy: just run the result of the transformation, and we're done.
    quine_raw = quine_raw_fmt.format(repr(transformation_code))
    return quine_raw.replace('%', repr(quine_raw))


def run():
    def e(c, i):
        l = dict()
        exec(c, dict(input=i), l)
        return l.get('output') or ''

    print('Write your transformation on a single line, then press ENTER.')
    print('The input will be given as the *variable* `input`.')
    print('Write the output into the variable `output`, do not print it!')
    print('Note that it has to be a *transformation*, so both input and output are programs.')
    # FIXME: Currently reads only 1 line
    transformation_code = input('>>> ')
    fixedpoint_code = make_fixedpoint(transformation_code)
    f_fixedpoint_code = e(transformation_code, fixedpoint_code)
    print()
    print('# The fixed-point code `e` is:')
    print(fixedpoint_code)
    print()
    print('# In order to show the theorem, this should have the same effect as the code `F(e)`,')
    print('# i.e., the code after running it *once* through your transformation:')
    print(f_fixedpoint_code)
    print()
    print()
    print('# If you want to run it, enter anything (not necessarily code)')
    print('# and press ENTER. If you want to exit, just press ENTER:')
    try:
        noncode_input = input('>>> ')
    except EOFError:
        print('# Have a nice day! :)')
        exit(0)
    except KeyboardInterrupt:
        print('# Alrighty, bye! :)')
        exit(0)
    if not noncode_input:
        print('# Exit it is; have fun! :)')
        exit(0)

    print()
    print()
    print('# First, run it with the (second) transformed code:')
    transformed_output = e(f_fixedpoint_code, noncode_input)
    print(transformed_output)
    print()
    print('# Finally, run it with the (first) "fixed-point" code:')
    fp_output = e(fixedpoint_code, noncode_input)
    print(fp_output)
    print()
    if fp_output == transformed_output:
        print('# They are equal!  Told ya so! :D')
    else:
        print('# Ahh shit.  They differ.  Please open an issue!')
        print('# https://github.com/BenWiederhake/general_purpose_fixedpoint/issues/new')


if __name__ == '__main__':
    run()
#!/usr/bin/env python3 ## The "format" is explained in `run`. #def old_safe_eval(code, sim_input): #    if not isinstance(code, str): #        raise TypeError('Lolwut?  Attempted to run non-str code (was {})') #    given = dict() #    given['input'] = sim_input #    # Pass `safe_eval` for now. #    # FIXME: Is this really not cheating? #    given['safe_eval'] = old_safe_eval #    the_locals = dict() #    try: #        exec(code, given, the_locals) #    except BaseException as e: #        raise e #    return the_locals.get('output') or '' \ def e(c, i):     l = dict()     exec(c, dict(input=i), l)     return l.get('output') or '' magic = % own_code = magic.replace(chr(37), repr(magic)) output = e(e({0}, own_code), input) # The core magic is that: # - `make_fixedpoint` must be total, i.e., always halt # - `transformation_code` must be total, i.e. always halt # - The code generated by `make_fixedpoint` is allowed to diverge. # Therefore, we (`make_fixedpoint`) can generate a quine, i.e. get # a handle on our own source code.  Then, we call the transformation on it. # This means that the transformation cannot possibly distinguish whether it # is currently run during the quine, or being run by the judge. # Therefore, It must spit out the same code in both situations. # The rest is easy: just run the result of the transformation, and we're done. # FIXME: Currently reads only 1 line