(module macro mzscheme (require "../reduction-semantics.ss" "../gui.ss") (define lang (language (e (lambda (variable) e) (app e e) number variable) (e-ctxt (lambda (variable) e-ctxt) (app e-ctxt any) (app e e-ctxt) hole))) (define macros '(or let if true false id)) (define-syntax (--> stx) (syntax-case stx () [(_ frm to) (syntax (reduction/context lang e-ctxt frm to))])) (define reductions (list (--> (id (name e any)) (term e)) (--> (side-condition ((name e1 any) (name e2 any)) (not (memq (term e1) macros))) (term (app e1 e2))) (--> (or (name e1 any) (name e2 any)) (let ([var (variable-not-in (list (term e1) (term e2)) 'x)]) (term (let (,var e1) (if ,var ,var e2))))) (--> (let ((name var variable) (name rhs any)) (name body any)) (term ((lambda (var) body) rhs))) (--> (if (name test any) (name thn any) (name els any)) (term ((test thn) els))) (--> (true) (term (lambda (x) (lambda (y) x)))) (--> (false) (term (lambda (x) (lambda (y) y)))))) (traces lang reductions '((id id) 5)) (traces lang reductions '(id 5)) (traces lang reductions '(or (false) (true))))