diff --git a/collects/redex/examples/arithmetic.ss b/collects/redex/examples/arithmetic.ss index f91a5baeb5..b4911c4735 100644 --- a/collects/redex/examples/arithmetic.ss +++ b/collects/redex/examples/arithmetic.ss @@ -1,6 +1,5 @@ -(module arithmetic mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/gui)) +#lang scheme +(require redex) (define-language lang (e (binop e e) @@ -39,4 +38,4 @@ [(--> (in-hole e-ctxt_1 a) (in-hole e-ctxt_1 b)) (c--> a b)])) - (traces reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2))))) + (traces reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2)))) \ No newline at end of file diff --git a/collects/redex/examples/beginner.ss b/collects/redex/examples/beginner.ss index 5819a08edf..a9e9d6cfb8 100644 --- a/collects/redex/examples/beginner.ss +++ b/collects/redex/examples/beginner.ss @@ -9,15 +9,13 @@ reflects the (broken) spec). |# -(module beginner mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/subst) - (lib "match.ss")) +#lang scheme +(require redex) - (provide run-tests - run-big-test) - - #| +(provide run-tests + run-big-test) + +#| `lang' below is actually more generous than beginner, but the reductions assume that the programs are all syntactically @@ -33,899 +31,893 @@ reflects the (broken) spec). (should that be syntacically disallowed?) |# + +(define-language lang + (p (d/e ...)) + (d/e (define (x x x ...) e) + (define x (lambda (x x ...) e)) + (define x e) + (define-struct x (x ...)) + e) + (e (x e e ...) + (prim-op e ...) + (cond (e e) (e e) ...) + (cond (e e) ... (else e)) + (if e e e) + (and e e e ...) + (or e e e ...) + empty + x + 'x + number + boolean + string) - (define-language lang - (p (d/e ...)) - (d/e (define (x x x ...) e) - (define x (lambda (x x ...) e)) - (define x e) + (prim-op + / cons first rest empty? struct? symbol=?) + + (p-ctxt (d/e-v ... d/e-ctxt d/e ...)) + (d/e-ctxt (define x e-ctxt) + e-ctxt) + (e-ctxt hole + (x v ... e-ctxt e ...) + (prim-op v ... e-ctxt e ...) + (cond [false e] ... [e-ctxt e] [e e] ...) + (cond [false e] ... [e-ctxt e] [e e] ... [else e]) + (and true ... e-ctxt e ...) + (or false ... e-ctxt e ...)) + + (d/e-v (define x (lambda (x x ...) e)) + (define x v) + (define (x x x ...) e) (define-struct x (x ...)) - e) - (e (x e e ...) - (prim-op e ...) - (cond (e e) (e e) ...) - (cond (e e) ... (else e)) - (if e e e) - (and e e e ...) - (or e e e ...) - empty + v) + + (v (maker v ...) + non-struct-value) + (non-struct-value number + list-value + boolean + string + 'x) + (list-value empty + (cons v list-value)) + (boolean true + false) + + (maker (side-condition variable_1 (maker? (term variable_1)))) + + (x (side-condition + (name x - 'x - number - boolean - string) - - (prim-op + / cons first rest empty? struct? symbol=?) - - (p-ctxt (d/e-v ... d/e-ctxt d/e ...)) - (d/e-ctxt (define x e-ctxt) - e-ctxt) - (e-ctxt hole - (x v ... e-ctxt e ...) - (prim-op v ... e-ctxt e ...) - (cond [false e] ... [e-ctxt e] [e e] ...) - (cond [false e] ... [e-ctxt e] [e e] ... [else e]) - (and true ... e-ctxt e ...) - (or false ... e-ctxt e ...)) - - (d/e-v (define x (lambda (x x ...) e)) - (define x v) - (define (x x x ...) e) - (define-struct x (x ...)) - v) - - (v (maker v ...) - non-struct-value) - (non-struct-value number - list-value - boolean - string - 'x) - (list-value empty - (cons v list-value)) - (boolean true - false) - - (maker (side-condition variable_1 (maker? (term variable_1)))) - - (x (side-condition - (name - x - (variable-except define - define-struct - lambda - cond - else - if - and - or - empty - true - false - quote)) - (not (prim-op? (term x)))))) - - (define beg-e-subst - (subst - [(? number?) - (constant)] - [(? symbol?) - (variable)] - ;; slight cheat here -- but since cond, if, and, or, etc - ;; aren't allowed to be variables (syntactically), we're okay. - [`(,@(e ...)) - (all-vars '()) - (build (lambda (vars . e) e)) - (subterms '() e)])) - - (define (maker? v) - (and (symbol? v) - (regexp-match #rx"^make-" (symbol->string v)))) - - (define p? (redex-match lang p)) - (define prim-op? (redex-match lang prim-op)) + (variable-except define + define-struct + lambda + cond + else + if + and + or + empty + true + false + quote)) + (not (prim-op? (term x)))))) - (define reductions - (reduction-relation - lang - ((and true ... false e ...) . ==> . false) - ((and true ...) . ==> . true) - ((side-condition (and true ... v_1 e ...) - (and (not (eq? (term v_1) 'true)) - (not (eq? (term v_1) 'false)))) - . e==> . - "and: question result is not true or false") - ((or false ... true e ...) . ==> . true) - ((or false ...) . ==> . false) - ((side-condition (or false ... v_1 e ...) - (and (not (eq? (term v_1) 'true)) - (not (eq? (term v_1) 'false)))) - . e==> . - "or: question result is not true or false") - - ((if true e_1 e_2) . ==> . e_1) - ((if false e_1 e_2) . ==> . e_2) - (e==> (if v_1 e_1 e_2) - "if: question result is not true or false" - (side-condition (and (not (eq? (term v_1) 'false)) - (not (eq? (term v_1) 'true))))) - - - ((cond (false e) ... (true e_1) (e_2 e_3) ...) . ==> . e_1) - ((cond (false e) ... (true e_1) (e_2 e_3) ... (else e_4)) . ==> . e_1) - ((cond (false e) ... (else e_1)) . ==> . e_1) - ((cond (false e) ...) . e==> . "cond: all question results were false") - - ((side-condition - (cond (false e_1) ... (v_1 e_2) (e_3 e_4) ...) - (and (not (eq? (term v_1) 'false)) - (not (eq? (term v_1) 'true)) - (not (eq? (term v_1) 'else)))) - . e==> . - "cond: question result is not true or false") - - ((side-condition - (cond (false e_1) ... (v_1 e_2) (e_3 e_4) ... (else e_5)) - (and (not (eq? (term v_1) 'false)) - (not (eq? (term v_1) 'true)) - (not (eq? (term v_1) 'else)))) - . e==> . - "cond: question result is not true or false") - - - ((empty? empty) . ==> . true) - ((side-condition (empty? v_1) - (not (eq? (term v_1) 'empty))) - . ==> . - false) - ((empty?) . e==> . "empty?: expects one argument") - ((empty? v_1 v_2 v_3 ...) . e==> . "empty?: expects one argument") - - ((side-condition (cons v v_1) - (and (not (eq? (term v_1) 'empty)) - (not (and (pair? (term v_1)) - (eq? (car (term v_1)) 'cons))))) - . e==> . - "cons: second argument must be of type ") - - ((first (cons v_1 list-value)) . ==> . v_1) - ((first) . e==> . "first: expects one argument") - ((first v_1 v_2 v_3 ...) . e==> . "first: expects one argument") - ((side-condition (first v_1) - (not (and (pair? (term v_1)) - (eq? (car (term v_1)) 'cons)))) - . e==> . - "first: expects argument of type ") - - ((rest (cons v list-value_1)) . ==> . list-value_1) - ((rest v_1 v_2 v_3 ...) . e==> . "rest: expects one argument") - ((rest) . e==> . "rest: expects one argument") - - ((side-condition (rest v_1) - (not (and (pair? (term v_1)) - (eq? (car (term v_1)) 'cons)))) - . e==> . - "rest: expects argument of type ") - - ((symbol=? 'x_1 'x_2) . ==> . ,(if (eq? (term x_1) (term x_2)) (term true) (term false))) - ((side-condition (symbol=? v_1 v_2) - (or (not (and (pair? (term v_1)) - (eq? (car (term v_1)) 'quote))) - (not (and (pair? (term v_2)) - (eq? (car (term v_2)) 'quote))))) - . e==> . - "symbol=?: expects argument of type ") - ((symbol=?) - . e==> . - "procedure symbol=?: expects 2 arguments") - ((symbol=? v_1 v_2 v_3 v_4 ...) - . e==> . - "procedure symbol=?: expects 2 arguments") - - ((+ number_1 ...) . ==> . ,(apply + (term (number_1 ...)))) - ((side-condition (+ v_arg ...) - (ormap (lambda (v_arg) (not (number? v_arg))) (term (v_arg ...)))) - . e==> . - "+: expects type ") - - ((side-condition (/ number_1 number_2 ...) - (andmap (lambda (number_2) (not (zero? number_2))) (term (number_2 ...)))) - . ==> . - ,(apply / (term (number_1 number_2 ...)))) - ((side-condition (/ number_1 number_2 ...) - (ormap (lambda (number_2) (zero? number_2)) (term (number_2 ...)))) - . e==> . - "/: division by zero") - ((side-condition (/ v_arg ...) - (ormap (lambda (v_arg) (not (number? v_arg))) (term (v_arg ...)))) - . e==> . - "/: expects type ") - - ;; unbound id application - (--> (side-condition - (d/e-v_before ... - (in-hole d/e-ctxt (x_f v ...)) - d/e ...) - (and (not (prim-op? (term x_f))) - (not (defined? (term x_f) (term (d/e-v_before ...)))))) - ,(format "reference to undefined identifier: ~a" (term x_f))) - - ;; procedure application as lambda - (--> (d/e-v_before ... - (define x_f (lambda (x_var ...) e_body)) - d/e-v_middle ... - (in-hole d/e-ctxt_1 (x_f v_arg ...)) - d/e_after ...) - (d/e-v_before ... - (define x_f (lambda (x_var ...) e_body)) - d/e-v_middle ... - (in-hole d/e-ctxt_1 - ,(multi-subst (term (x_var ...)) - (term (v_arg ...)) - (term e_body))) - d/e_after ...)) - - ;; define-style procedure application - (--> (d/e-v_before ... - (define (x_f x_var ...) e_body) - d/e-v_middle ... - (in-hole d/e-ctxt (x_f v_arg ...)) - (name after d/e) ...) - (d/e-v_before ... - (define (x_f x_var ...) e_body) - d/e-v_middle ... - (in-hole d/e-ctxt - ,(multi-subst (term (x_var ...)) - (term (v_arg ...)) - (term e_body))) - after ...)) - - ;; reference to non-procedure define: - (--> (d/e-v_before ... - (name defn (define (name a x) (name val v))) - d/e-v_middle ... - (in-hole (name ctxt d/e-ctxt) (name a x)) - d/e_after ...) - (d/e-v_before ... - defn - d/e-v_middle ... - (in-hole ctxt val) - d/e_after ...)) - - ;; unbound reference to top-level id in hole: - (--> - (side-condition - (d/e-v_before ... - (in-hole d/e-ctxt (name a x)) - d/e ...) - (and (not (prim-op? (term a))) - (not (defined? (term a) (term (d/e-v_before ...)))))) - ,(format "reference to undefined identifier: ~a" (term a))) - - ;; reference to procedure-bound var in hole: - (--> (d/e-v ... - (define (x_f x_var ...) (name body e)) - d/e-v ... - (in-hole d/e-ctxt x_f) - d/e ...) - ,(format "~a is a procedure, so it must be applied to arguments" (term x_f))) - - ;; reference to non-procedure-bound-var in application - (--> (d/e-v ... - (define x_a v_val) - d/e-v ... - (in-hole d/e-ctxt (x_a v ...)) - d/e ...) - ,(format "procedure application: expected procedure, given: ~a" (term v_val))) - - ((struct? ((name maker maker) v ...)) . ==> . true) - ((struct? non-struct-value) . ==> . false) - - ;; struct predicate passes - (--> (side-condition - (d/e-v_before ... - (define-struct x_struct (x_field ...)) - d/e-v_middle ... - (in-hole d/e-ctxt (x_predicate (x_maker v_arg ...))) - d/e_after ...) - (and (maker-name-match? (term x_struct) (term x_maker)) - (predicate-name-match? (term x_struct) (term x_predicate)))) - (d/e-v_before ... - (define-struct x_struct (x_field ...)) - d/e-v_middle ... - (in-hole d/e-ctxt true) - d/e_after ...)) - - ;; struct predicate fail to another struct - (--> (side-condition - (d/e-v_before ... - (define-struct x_struct (x_field ...)) - d/e-v_middle ... - (in-hole d/e-ctxt (x_predicate (x_maker v ...))) - (name after d/e) ...) - (and (not (maker-name-match? (term x_struct) (term x_maker))) - (predicate-name-match? (term x_struct) (term x_predicate)))) - (d/e-v_before ... - (define-struct x_struct (x_field ...)) - d/e-v_middle ... - (in-hole d/e-ctxt false) - after ...)) - - ;; struct predicate fail to another value - (--> (side-condition - (d/e-v_before ... - (define-struct x_struct (x_field ...)) - d/e-v_middle ... - (in-hole (name ctxt d/e-ctxt) (x_predicate non-struct-value)) - d/e_after ...) - (predicate-name-match? (term x_struct) (term x_predicate))) - (d/e-v_before ... - (define-struct x_struct (x_field ...)) - d/e-v_middle ... - (in-hole ctxt false) - d/e_after ...)) - - ;; misapplied selector 1 - (--> (side-condition - (d/e-v_before ... - (define-struct x_struct (x_field ...)) - d/e-v_middle ... - (in-hole d/e-ctxt (x_selector (x_maker v_arg ...))) - d/e_after ...) - (and (not (maker-name-match? (term x_struct) (term x_maker))) - (selector-name-match? (term x_struct) (term (x_field ...)) (term x_selector)))) - ,(format "~a: expects argument of matching struct" (term x_selector))) - - ;; misapplied selector 2 - (--> (side-condition - (d/e-v_before ... - (define-struct x_struct (x_field ...)) - d/e-v_middle ... - (in-hole d/e-ctxt (x_selector non-struct-value)) - d/e_after ...) - (selector-name-match? (term x_struct) (term (x_field ...)) (term x_selector))) - ,(format "~a: expects argument of matching struct" (term x_selector))) - - ;; well-applied selector - (--> (side-condition - (d/e-v_before ... - (define-struct x_struct (x_field ...)) - d/e-v_middle ... - (in-hole (name ctxt d/e-ctxt) (x_selector (x_maker v_arg ...))) - d/e_after ...) - (and (maker-name-match? (term x_struct) (term x_maker)) - (selector-name-match? (term x_struct) (term (x_field ...)) (term x_selector)))) - (d/e-v_before ... - (define-struct x_struct (x_field ...)) - d/e-v_middle ... - (in-hole ctxt - ,(list-ref (term (v_arg ...)) - (struct-index (term x_struct) - (term (x_field ...)) - (term x_selector)))) - d/e_after ...)) - - where - [(==> a b) (--> (in-hole p-ctxt_1 a) (in-hole p-ctxt_1 b))] - [(e==> a b) (--> (in-hole p-ctxt a) b)])) +(define-metafunction beg-e-subst lang + [(x v x) v] + [(x v (any_1 ...)) ((beg-e-subst (x v any_1)) ...)] + [(x v any) any]) - (define (defined? f befores) - (ormap - (lambda (before) - (match before - [`(define (,a-name ,@(x ...)) ,b) - (eq? f a-name)] - [`(define ,a-name (lambda ,@(x ...))) - (eq? f a-name)] - [`(define-struct ,struct-name (,@(fields ...))) - (or (ormap (lambda (field) - (eq? f (string->symbol (format "~a-~a" struct-name field)))) - fields) - (eq? f (string->symbol (format "make-~a" struct-name))) - (eq? f (string->symbol (format "~a?" struct-name))))] - [else #t])) - befores)) - - (define (multi-subst orig-vars orig-args body) - (let loop ([args orig-args] - [vars orig-vars] - [body body]) - (cond - [(and (null? args) (null? vars)) - body] - [(or (null? args) (null? vars)) - (error 'multi-subst - "malformed program, formals ~s and actuals ~s do not have the same size" - orig-vars - orig-args)] - [else (loop (cdr args) - (cdr vars) - (beg-e-subst (car vars) (car args) body))]))) +(define (maker? v) + (and (symbol? v) + (regexp-match #rx"^make-" (symbol->string v)))) - (define (selector-name-match? struct fields selector) - (ormap (lambda (field) (string=? (format "~a-~a" struct field) - (symbol->string selector))) - fields)) - - (define (struct-index struct init-fields selector) - (let loop ([i 0] - [fields init-fields]) - (cond - [(null? fields) (error 'struct-index "~s ~s ~s" struct init-fields selector)] - [else (let ([field (car fields)]) - (if (string=? (format "~a-~a" struct field) - (symbol->string selector)) - i - (loop (+ i 1) - (cdr fields))))]))) - - (define (maker-name-match? name maker) - (let* ([names (symbol->string name)] - [makers (symbol->string maker)] - [namel (string-length names)] - [makerl (string-length makers)]) - (and (makerl . > . namel) - (string=? (substring makers (- makerl namel) makerl) - names)))) - - (define (predicate-name-match? name predicate) - (eq? (string->symbol (format "~a?" name)) predicate)) +(define p? (redex-match lang p)) +(define prim-op? (redex-match lang prim-op)) - (define failed-tests 0) - (define total-tests 0) - - (define (test in out) - (set! total-tests (+ total-tests 1)) - (let/ec k - (let* ([failed - (lambda (msg) - (set! failed-tests (+ failed-tests 1)) - (fprintf (current-error-port) "FAILED: ~a\n" msg) - (k (void)))] - [got (normalize in failed)]) - (unless (equal? got out) - (fprintf (current-error-port) "FAILED: ~s\ngot: ~s\nexpected: ~s\n" in got out) - (set! failed-tests (+ failed-tests 1)))))) - - (define (test-all step . steps) - (set! total-tests (+ total-tests 1)) - (let loop ([this step] - [rest steps]) - (let ([nexts (apply-reduction-relation reductions this)]) - (cond - [(null? rest) - (unless (null? nexts) - (set! failed-tests (+ failed-tests 1)) - (fprintf (current-error-port) "FAILED: ~s\n last step: ~s\n reduced to: ~s\n" - step - this - nexts))] - [else - (cond - [(and (pair? nexts) - (null? (cdr nexts))) - (let ([next (car nexts)]) - (if (equal? next (car rest)) - (loop (car rest) - (cdr rest)) - (begin - (set! failed-tests (+ failed-tests 1)) - (fprintf (current-error-port) - "FAILED: ~s\n step: ~s\n expected: ~s\n got: ~s\n" - step - this - (car rest) - next))))] - [else - (set! failed-tests (+ failed-tests 1)) - (fprintf (current-error-port) - "FAILED: ~s\n step: ~s\n not single step: ~s\n" - step - this - nexts)])])))) - - (define show-dots (make-parameter #f)) - (define (normalize orig-term failed) - (let loop ([term orig-term] - [n 1000]) - (unless (p? term) - (failed (format "not a p: ~s orig: ~s" term orig-term))) - (let ([nexts (apply-reduction-relation reductions term)]) - (when (show-dots) - (display #\.) - (flush-output)) - (cond - [(= n 0) - (when (show-dots) - (newline)) - (error 'normalize "found too many reductions")] - [(null? nexts) - (when (show-dots) - (newline)) - term] - [(string? (car nexts)) - (when (show-dots) - (newline)) - (car nexts)] - [(null? (cdr nexts)) (loop (car nexts) (- n 1))] - [else - (when (show-dots) - (newline)) - (failed (format "found more than one reduction\n ~s\n ->\n~s" term nexts))])))) +(define reductions + (reduction-relation + lang + ((and true ... false e ...) . ==> . false) + ((and true ...) . ==> . true) + ((side-condition (and true ... v_1 e ...) + (and (not (eq? (term v_1) 'true)) + (not (eq? (term v_1) 'false)))) + . e==> . + "and: question result is not true or false") + ((or false ... true e ...) . ==> . true) + ((or false ...) . ==> . false) + ((side-condition (or false ... v_1 e ...) + (and (not (eq? (term v_1) 'true)) + (not (eq? (term v_1) 'false)))) + . e==> . + "or: question result is not true or false") + + ((if true e_1 e_2) . ==> . e_1) + ((if false e_1 e_2) . ==> . e_2) + (e==> (if v_1 e_1 e_2) + "if: question result is not true or false" + (side-condition (and (not (eq? (term v_1) 'false)) + (not (eq? (term v_1) 'true))))) + + + ((cond (false e) ... (true e_1) (e_2 e_3) ...) . ==> . e_1) + ((cond (false e) ... (true e_1) (e_2 e_3) ... (else e_4)) . ==> . e_1) + ((cond (false e) ... (else e_1)) . ==> . e_1) + ((cond (false e) ...) . e==> . "cond: all question results were false") + + ((side-condition + (cond (false e_1) ... (v_1 e_2) (e_3 e_4) ...) + (and (not (eq? (term v_1) 'false)) + (not (eq? (term v_1) 'true)) + (not (eq? (term v_1) 'else)))) + . e==> . + "cond: question result is not true or false") + + ((side-condition + (cond (false e_1) ... (v_1 e_2) (e_3 e_4) ... (else e_5)) + (and (not (eq? (term v_1) 'false)) + (not (eq? (term v_1) 'true)) + (not (eq? (term v_1) 'else)))) + . e==> . + "cond: question result is not true or false") + + + ((empty? empty) . ==> . true) + ((side-condition (empty? v_1) + (not (eq? (term v_1) 'empty))) + . ==> . + false) + ((empty?) . e==> . "empty?: expects one argument") + ((empty? v_1 v_2 v_3 ...) . e==> . "empty?: expects one argument") + + ((side-condition (cons v v_1) + (and (not (eq? (term v_1) 'empty)) + (not (and (pair? (term v_1)) + (eq? (car (term v_1)) 'cons))))) + . e==> . + "cons: second argument must be of type ") + + ((first (cons v_1 list-value)) . ==> . v_1) + ((first) . e==> . "first: expects one argument") + ((first v_1 v_2 v_3 ...) . e==> . "first: expects one argument") + ((side-condition (first v_1) + (not (and (pair? (term v_1)) + (eq? (car (term v_1)) 'cons)))) + . e==> . + "first: expects argument of type ") + + ((rest (cons v list-value_1)) . ==> . list-value_1) + ((rest v_1 v_2 v_3 ...) . e==> . "rest: expects one argument") + ((rest) . e==> . "rest: expects one argument") + + ((side-condition (rest v_1) + (not (and (pair? (term v_1)) + (eq? (car (term v_1)) 'cons)))) + . e==> . + "rest: expects argument of type ") + + ((symbol=? 'x_1 'x_2) . ==> . ,(if (eq? (term x_1) (term x_2)) (term true) (term false))) + ((side-condition (symbol=? v_1 v_2) + (or (not (and (pair? (term v_1)) + (eq? (car (term v_1)) 'quote))) + (not (and (pair? (term v_2)) + (eq? (car (term v_2)) 'quote))))) + . e==> . + "symbol=?: expects argument of type ") + ((symbol=?) + . e==> . + "procedure symbol=?: expects 2 arguments") + ((symbol=? v_1 v_2 v_3 v_4 ...) + . e==> . + "procedure symbol=?: expects 2 arguments") + + ((+ number_1 ...) . ==> . ,(apply + (term (number_1 ...)))) + ((side-condition (+ v_arg ...) + (ormap (lambda (v_arg) (not (number? v_arg))) (term (v_arg ...)))) + . e==> . + "+: expects type ") + + ((side-condition (/ number_1 number_2 ...) + (andmap (lambda (number_2) (not (zero? number_2))) (term (number_2 ...)))) + . ==> . + ,(apply / (term (number_1 number_2 ...)))) + ((side-condition (/ number_1 number_2 ...) + (ormap (lambda (number_2) (zero? number_2)) (term (number_2 ...)))) + . e==> . + "/: division by zero") + ((side-condition (/ v_arg ...) + (ormap (lambda (v_arg) (not (number? v_arg))) (term (v_arg ...)))) + . e==> . + "/: expects type ") + + ;; unbound id application + (--> (side-condition + (d/e-v_before ... + (in-hole d/e-ctxt (x_f v ...)) + d/e ...) + (and (not (prim-op? (term x_f))) + (not (defined? (term x_f) (term (d/e-v_before ...)))))) + ,(format "reference to undefined identifier: ~a" (term x_f))) + + ;; procedure application as lambda + (--> (d/e-v_before ... + (define x_f (lambda (x_var ...) e_body)) + d/e-v_middle ... + (in-hole d/e-ctxt_1 (x_f v_arg ...)) + d/e_after ...) + (d/e-v_before ... + (define x_f (lambda (x_var ...) e_body)) + d/e-v_middle ... + (in-hole d/e-ctxt_1 + ,(multi-subst (term (x_var ...)) + (term (v_arg ...)) + (term e_body))) + d/e_after ...)) + + ;; define-style procedure application + (--> (d/e-v_before ... + (define (x_f x_var ...) e_body) + d/e-v_middle ... + (in-hole d/e-ctxt (x_f v_arg ...)) + (name after d/e) ...) + (d/e-v_before ... + (define (x_f x_var ...) e_body) + d/e-v_middle ... + (in-hole d/e-ctxt + ,(multi-subst (term (x_var ...)) + (term (v_arg ...)) + (term e_body))) + after ...)) + + ;; reference to non-procedure define: + (--> (d/e-v_before ... + (name defn (define (name a x) (name val v))) + d/e-v_middle ... + (in-hole (name ctxt d/e-ctxt) (name a x)) + d/e_after ...) + (d/e-v_before ... + defn + d/e-v_middle ... + (in-hole ctxt val) + d/e_after ...)) + + ;; unbound reference to top-level id in hole: + (--> + (side-condition + (d/e-v_before ... + (in-hole d/e-ctxt (name a x)) + d/e ...) + (and (not (prim-op? (term a))) + (not (defined? (term a) (term (d/e-v_before ...)))))) + ,(format "reference to undefined identifier: ~a" (term a))) + + ;; reference to procedure-bound var in hole: + (--> (d/e-v ... + (define (x_f x_var ...) (name body e)) + d/e-v ... + (in-hole d/e-ctxt x_f) + d/e ...) + ,(format "~a is a procedure, so it must be applied to arguments" (term x_f))) + + ;; reference to non-procedure-bound-var in application + (--> (d/e-v ... + (define x_a v_val) + d/e-v ... + (in-hole d/e-ctxt (x_a v ...)) + d/e ...) + ,(format "procedure application: expected procedure, given: ~a" (term v_val))) + + ((struct? ((name maker maker) v ...)) . ==> . true) + ((struct? non-struct-value) . ==> . false) + + ;; struct predicate passes + (--> (side-condition + (d/e-v_before ... + (define-struct x_struct (x_field ...)) + d/e-v_middle ... + (in-hole d/e-ctxt (x_predicate (x_maker v_arg ...))) + d/e_after ...) + (and (maker-name-match? (term x_struct) (term x_maker)) + (predicate-name-match? (term x_struct) (term x_predicate)))) + (d/e-v_before ... + (define-struct x_struct (x_field ...)) + d/e-v_middle ... + (in-hole d/e-ctxt true) + d/e_after ...)) + + ;; struct predicate fail to another struct + (--> (side-condition + (d/e-v_before ... + (define-struct x_struct (x_field ...)) + d/e-v_middle ... + (in-hole d/e-ctxt (x_predicate (x_maker v ...))) + (name after d/e) ...) + (and (not (maker-name-match? (term x_struct) (term x_maker))) + (predicate-name-match? (term x_struct) (term x_predicate)))) + (d/e-v_before ... + (define-struct x_struct (x_field ...)) + d/e-v_middle ... + (in-hole d/e-ctxt false) + after ...)) + + ;; struct predicate fail to another value + (--> (side-condition + (d/e-v_before ... + (define-struct x_struct (x_field ...)) + d/e-v_middle ... + (in-hole (name ctxt d/e-ctxt) (x_predicate non-struct-value)) + d/e_after ...) + (predicate-name-match? (term x_struct) (term x_predicate))) + (d/e-v_before ... + (define-struct x_struct (x_field ...)) + d/e-v_middle ... + (in-hole ctxt false) + d/e_after ...)) + + ;; misapplied selector 1 + (--> (side-condition + (d/e-v_before ... + (define-struct x_struct (x_field ...)) + d/e-v_middle ... + (in-hole d/e-ctxt (x_selector (x_maker v_arg ...))) + d/e_after ...) + (and (not (maker-name-match? (term x_struct) (term x_maker))) + (selector-name-match? (term x_struct) (term (x_field ...)) (term x_selector)))) + ,(format "~a: expects argument of matching struct" (term x_selector))) + + ;; misapplied selector 2 + (--> (side-condition + (d/e-v_before ... + (define-struct x_struct (x_field ...)) + d/e-v_middle ... + (in-hole d/e-ctxt (x_selector non-struct-value)) + d/e_after ...) + (selector-name-match? (term x_struct) (term (x_field ...)) (term x_selector))) + ,(format "~a: expects argument of matching struct" (term x_selector))) + + ;; well-applied selector + (--> (side-condition + (d/e-v_before ... + (define-struct x_struct (x_field ...)) + d/e-v_middle ... + (in-hole (name ctxt d/e-ctxt) (x_selector (x_maker v_arg ...))) + d/e_after ...) + (and (maker-name-match? (term x_struct) (term x_maker)) + (selector-name-match? (term x_struct) (term (x_field ...)) (term x_selector)))) + (d/e-v_before ... + (define-struct x_struct (x_field ...)) + d/e-v_middle ... + (in-hole ctxt + ,(list-ref (term (v_arg ...)) + (struct-index (term x_struct) + (term (x_field ...)) + (term x_selector)))) + d/e_after ...)) + + with + [(--> (in-hole p-ctxt_1 a) (in-hole p-ctxt_1 b)) (==> a b)] + [(--> (in-hole p-ctxt a) b) (e==> a b)])) - (define (show-test-results) +(define (defined? f befores) + (ormap + (lambda (before) + (match before + [`(define (,a-name ,x ...) ,b) + (eq? f a-name)] + [`(define ,a-name (lambda ,x ...)) + (eq? f a-name)] + [`(define-struct ,struct-name (,fields ...)) + (or (ormap (lambda (field) + (eq? f (string->symbol (format "~a-~a" struct-name field)))) + fields) + (eq? f (string->symbol (format "make-~a" struct-name))) + (eq? f (string->symbol (format "~a?" struct-name))))] + [else #t])) + befores)) + +(define (multi-subst orig-vars orig-args body) + (let loop ([args orig-args] + [vars orig-vars] + [body body]) (cond - [(= failed-tests 0) - (fprintf (current-error-port) "passed all ~a tests\n" total-tests)] - [else - (fprintf (current-error-port) "failed ~a out of ~a tests\n" failed-tests total-tests)])) - - (define-syntax (tests stx) - (syntax-case stx () - [(_ args ...) - (syntax - (begin - (set! failed-tests 0) - (set! total-tests 0) - args ... - (show-test-results)))])) - - (define (run-tests) + [(and (null? args) (null? vars)) + body] + [(or (null? args) (null? vars)) + (error 'multi-subst + "malformed program, formals ~s and actuals ~s do not have the same size" + orig-vars + orig-args)] + [else (loop (cdr args) + (cdr vars) + (term-let ((x (car vars)) + (v (car args)) + (body body)) + (term (beg-e-subst (x v body)))))]))) + +(define (selector-name-match? struct fields selector) + (ormap (lambda (field) (string=? (format "~a-~a" struct field) + (symbol->string selector))) + fields)) + +(define (struct-index struct init-fields selector) + (let loop ([i 0] + [fields init-fields]) + (cond + [(null? fields) (error 'struct-index "~s ~s ~s" struct init-fields selector)] + [else (let ([field (car fields)]) + (if (string=? (format "~a-~a" struct field) + (symbol->string selector)) + i + (loop (+ i 1) + (cdr fields))))]))) + +(define (maker-name-match? name maker) + (let* ([names (symbol->string name)] + [makers (symbol->string maker)] + [namel (string-length names)] + [makerl (string-length makers)]) + (and (makerl . > . namel) + (string=? (substring makers (- makerl namel) makerl) + names)))) + +(define (predicate-name-match? name predicate) + (eq? (string->symbol (format "~a?" name)) predicate)) + +(define failed-tests 0) +(define total-tests 0) + +(define (test in out) + (set! total-tests (+ total-tests 1)) + (let/ec k + (let* ([failed + (lambda (msg) + (set! failed-tests (+ failed-tests 1)) + (fprintf (current-error-port) "FAILED: ~a\n" msg) + (k (void)))] + [got (normalize in failed)]) + (unless (equal? got out) + (fprintf (current-error-port) "FAILED: ~s\ngot: ~s\nexpected: ~s\n" in got out) + (set! failed-tests (+ failed-tests 1)))))) + +(define (test-all step . steps) + (set! total-tests (+ total-tests 1)) + (let loop ([this step] + [rest steps]) + (let ([nexts (apply-reduction-relation reductions this)]) + (cond + [(null? rest) + (unless (null? nexts) + (set! failed-tests (+ failed-tests 1)) + (fprintf (current-error-port) "FAILED: ~s\n last step: ~s\n reduced to: ~s\n" + step + this + nexts))] + [else + (cond + [(and (pair? nexts) + (null? (cdr nexts))) + (let ([next (car nexts)]) + (if (equal? next (car rest)) + (loop (car rest) + (cdr rest)) + (begin + (set! failed-tests (+ failed-tests 1)) + (fprintf (current-error-port) + "FAILED: ~s\n step: ~s\n expected: ~s\n got: ~s\n" + step + this + (car rest) + next))))] + [else + (set! failed-tests (+ failed-tests 1)) + (fprintf (current-error-port) + "FAILED: ~s\n step: ~s\n not single step: ~s\n" + step + this + nexts)])])))) + +(define show-dots (make-parameter #f)) +(define (normalize orig-term failed) + (let loop ([term orig-term] + [n 1000]) + (unless (p? term) + (failed (format "not a p: ~s orig: ~s" term orig-term))) + (let ([nexts (apply-reduction-relation reductions term)]) + (when (show-dots) + (display #\.) + (flush-output)) + (cond + [(= n 0) + (when (show-dots) + (newline)) + (error 'normalize "found too many reductions")] + [(null? nexts) + (when (show-dots) + (newline)) + term] + [(string? (car nexts)) + (when (show-dots) + (newline)) + (car nexts)] + [(null? (cdr nexts)) (loop (car nexts) (- n 1))] + [else + (when (show-dots) + (newline)) + (failed (format "found more than one reduction\n ~s\n ->\n~s" term nexts))])))) + +(define (show-test-results) + (cond + [(= failed-tests 0) + (fprintf (current-error-port) "passed all ~a tests\n" total-tests)] + [else + (fprintf (current-error-port) "failed ~a out of ~a tests\n" failed-tests total-tests)])) + +(define-syntax (tests stx) + (syntax-case stx () + [(_ args ...) + (syntax + (begin + (set! failed-tests 0) + (set! total-tests 0) + args ... + (show-test-results)))])) + +(define (run-tests) + (tests + (test + '((define-struct s ()) + (s? (make-s))) + '((define-struct s ()) + true)) + + (test + '((define-struct s (a b)) + (s-a (make-s 1 3))) + '((define-struct s (a b)) + 1)) + + (test + '((define-struct s (a b)) + (s-b (make-s 1 3))) + '((define-struct s (a b)) + 3)) + + (test + '((define-struct s (a b)) + (define-struct t (x y)) + (t-x (make-s 1 2))) + "t-x: expects argument of matching struct") + + (test + '((define-struct t (x y)) + (t-x 12)) + "t-x: expects argument of matching struct") + + (test + '((define-struct s (a b)) + (define-struct t (x y)) + (s? (make-s 1 2))) + '((define-struct s (a b)) + (define-struct t (x y)) + true)) + + (test + '((define-struct s (a b)) + (define-struct t (x y)) + (t? (make-s 1 2))) + '((define-struct s (a b)) + (define-struct t (x y)) + false)) + + (test + '((define-struct s (a b)) + (struct? (make-s 1 2)) + (struct? 1)) + '((define-struct s (a b)) + true + false)) + + (test + '((define (f x) x) + (f 1)) + '((define (f x) x) + 1)) + + (test + '((define (double l) (+ l l)) + (double 2)) + '((define (double l) (+ l l)) + 4)) + + (test + '((define f (lambda (x) x)) + (f 1)) + '((define f (lambda (x) x)) + 1)) + + (test + '((define double (lambda (l) (+ l l))) + (double 2)) + '((define double (lambda (l) (+ l l))) + 4)) + + (test + '((f 1)) + "reference to undefined identifier: f") + + (test + '((f 1) + (define (f x) x)) + "reference to undefined identifier: f") + + (test + '((make-s 1) + (define-struct s (a b))) + "reference to undefined identifier: make-s") + + (test + '((+ 1 2 3)) + '(6)) + + (test + '((+ 1 "2" 3)) + "+: expects type ") + + (test + '((/ 1 2 3)) + '(1/6)) + + (test + '((/ 1 2 0 3)) + "/: division by zero") + + (test + '((/ 1 "2" 3)) + "/: expects type ") + + (test '((+ 1 (/ (+ 3 5) (+ 2 2)))) '(3)) + + (test '((symbol=? 'x 'x)) '(true)) + (test '((symbol=? 'x 'y)) '(false)) + (test '((symbol=? 1 'x)) + "symbol=?: expects argument of type ") + (test '((symbol=? 'x 1)) + "symbol=?: expects argument of type ") + + (test '((cons 1 empty)) '((cons 1 empty))) + (test '((cons 1 2)) + "cons: second argument must be of type ") + (test '((+ (first (cons 1 2)) 2)) + "cons: second argument must be of type ") + (test '((+ (first (cons 1 empty)) 2)) + '(3)) + + (test + '((first (cons 1 empty))) + '(1)) + + (test + '((first 1)) + "first: expects argument of type ") + + (test + '((first 1 2)) + "first: expects one argument") + + (test + '((first)) + "first: expects one argument") + + (test + '((rest (cons 1 empty))) + '(empty)) + + (test + '((rest 1)) + "rest: expects argument of type ") + + (test + '((rest 1 2)) + "rest: expects one argument") + + (test + '((rest)) + "rest: expects one argument") + + (test + '((empty? empty)) + '(true)) + + (test + '((empty? 1)) + '(false)) + + (test + '((empty?)) + "empty?: expects one argument") + + (test + '((empty? 1 2)) + "empty?: expects one argument") + + (test + '((cond [true 1])) + '(1)) + + (test + '((cond [else 1])) + '(1)) + + (test-all + '((cond [false 1] [else 2])) + '(2)) + + (test-all + '((cond [false 1] [false 2])) + "cond: all question results were false") + + (test + '((cond [1 1])) + "cond: question result is not true or false") + + (test + '((cond [(empty? empty) 'infinite] [else 3])) + '('infinite)) + + (test-all + '((cond [(if false false false) 'x] [(if true true true) 'y] [(if false false false) 'z])) + '((cond [false 'x] [(if true true true) 'y] [(if false false false) 'z])) + '((cond [false 'x] [true 'y] [(if false false false) 'z])) + '('y)) + + (test-all + '((cond [(if false false false) 'x] [(if true true true) 'y] [else 'z])) + '((cond [false 'x] [(if true true true) 'y] [else 'z])) + '((cond [false 'x] [true 'y] [else 'z])) + '('y)) + + (test-all + '((cond [(if false false false) 'x] [(if false false false) 'y] [else 'z])) + '((cond [false 'x] [(if false false false) 'y] [else 'z])) + '((cond [false 'x] [false 'y] [else 'z])) + '('z)) + + (test-all + '((and true true 3)) + "and: question result is not true or false") + + (test-all + '((and 1 true true)) + "and: question result is not true or false") + + (test-all + '((and true true true false)) + '(false)) + + (test-all + '((and false true)) + '(false)) + + (test-all + '((or false false 3)) + "or: question result is not true or false") + + (test-all + '((or 1 false false)) + "or: question result is not true or false") + + (test-all + '((or false false false true)) + '(true)) + + (test-all + '((or true false)) + '(true)) + + (test-all + '((or (if false false false) (if false false false) (if true true true) (if false false false))) + '((or false (if false false false) (if true true true) (if false false false))) + '((or false false (if true true true) (if false false false))) + '((or false false true (if false false false))) + '(true)) + + (test-all + '((and (if true true true) (if true true true) (if false false false) (if true true true))) + '((and true (if true true true) (if false false false) (if true true true))) + '((and true true (if false false false) (if true true true))) + '((and true true false (if true true true))) + '(false)) + + (test + '((if 1 2 3)) + "if: question result is not true or false") + + (test + '((if true 'x 'y)) + '('x)) + + (test + '((if false 'x 'y)) + '('y)) + + ; test non-procedure-defs in context: + (test + `((+ 3 4) (define a 3) (+ 5 6)) + `(7 (define a 3) 11)) + + ; test reduction of non-procedure-defs: + (test + `((define a 13) (define b (+ a 9)) (+ 3 4)) + `((define a 13) (define b 22) 7)) + + ; test reduction of unbound ids in hole: + (test + `(x) + "reference to undefined identifier: x") + + ; test reduction of function-bound id in hole: + (test + `((define (a x) (+ x 1)) a) + "a is a procedure, so it must be applied to arguments") + + ; test reduction of non-procedure-def in application: + (test + `((define a 3) (a 9)) + "procedure application: expected procedure, given: 3"))) + +(define (run-big-test) + (parameterize ([show-dots #t]) (tests (test - '((define-struct s ()) - (s? (make-s))) - '((define-struct s ()) - true)) - + '((define-struct pr (hd tl)) + (define (avg l) + (cond + [(empty? l) 'infinite] + [else (/ (sum l) (howmany/acc l 0))])) + (define (sum l) + (cond + [(empty? (pr-tl l)) (pr-hd l)] + [else (+ (pr-hd l) (sum (pr-tl l)))])) + (define (howmany/acc l acc) + (cond + [(empty? l) acc] + [else (howmany/acc (pr-tl l) (+ acc 1))])) + (avg empty) + (avg (make-pr 3 (make-pr 4 (make-pr 5 (make-pr 6 (make-pr 7 (make-pr 8 (make-pr 9 empty))))))))) + + '((define-struct pr (hd tl)) + (define (avg l) + (cond + [(empty? l) 'infinite] + [else (/ (sum l) (howmany/acc l 0))])) + (define (sum l) + (cond + [(empty? (pr-tl l)) (pr-hd l)] + [else (+ (pr-hd l) (sum (pr-tl l)))])) + (define (howmany/acc l acc) + (cond + [(empty? l) acc] + [else (howmany/acc (pr-tl l) (+ acc 1))])) + 'infinite + 6)) (test - '((define-struct s (a b)) - (s-a (make-s 1 3))) - '((define-struct s (a b)) - 1)) - - (test - '((define-struct s (a b)) - (s-b (make-s 1 3))) - '((define-struct s (a b)) - 3)) - - (test - '((define-struct s (a b)) - (define-struct t (x y)) - (t-x (make-s 1 2))) - "t-x: expects argument of matching struct") - - (test - '((define-struct t (x y)) - (t-x 12)) - "t-x: expects argument of matching struct") - - (test - '((define-struct s (a b)) - (define-struct t (x y)) - (s? (make-s 1 2))) - '((define-struct s (a b)) - (define-struct t (x y)) - true)) - - (test - '((define-struct s (a b)) - (define-struct t (x y)) - (t? (make-s 1 2))) - '((define-struct s (a b)) - (define-struct t (x y)) - false)) - - (test - '((define-struct s (a b)) - (struct? (make-s 1 2)) - (struct? 1)) - '((define-struct s (a b)) + '((define (contains-sym? s l) + (cond + [(empty? l) false] + [true (or (symbol=? s (first l)) + (contains-sym? s (rest l)))])) + (contains-sym? 'x (cons 'z (cons 'y (cons 'x empty)))) + (contains-sym? 'a (cons 'p (cons 'q (cons 'p (cons 'q (cons 'p (cons 'q empty)))))))) + '((define (contains-sym? s l) + (cond + [(empty? l) false] + [true (or (symbol=? s (first l)) + (contains-sym? s (rest l)))])) true - false)) - - (test - '((define (f x) x) - (f 1)) - '((define (f x) x) - 1)) - - (test - '((define (double l) (+ l l)) - (double 2)) - '((define (double l) (+ l l)) - 4)) - - (test - '((define f (lambda (x) x)) - (f 1)) - '((define f (lambda (x) x)) - 1)) - - (test - '((define double (lambda (l) (+ l l))) - (double 2)) - '((define double (lambda (l) (+ l l))) - 4)) - - (test - '((f 1)) - "reference to undefined identifier: f") - - (test - '((f 1) - (define (f x) x)) - "reference to undefined identifier: f") - - (test - '((make-s 1) - (define-struct s (a b))) - "reference to undefined identifier: make-s") - - (test - '((+ 1 2 3)) - '(6)) - - (test - '((+ 1 "2" 3)) - "+: expects type ") - - (test - '((/ 1 2 3)) - '(1/6)) - - (test - '((/ 1 2 0 3)) - "/: division by zero") - - (test - '((/ 1 "2" 3)) - "/: expects type ") - - (test '((+ 1 (/ (+ 3 5) (+ 2 2)))) '(3)) - - (test '((symbol=? 'x 'x)) '(true)) - (test '((symbol=? 'x 'y)) '(false)) - (test '((symbol=? 1 'x)) - "symbol=?: expects argument of type ") - (test '((symbol=? 'x 1)) - "symbol=?: expects argument of type ") - - (test '((cons 1 empty)) '((cons 1 empty))) - (test '((cons 1 2)) - "cons: second argument must be of type ") - (test '((+ (first (cons 1 2)) 2)) - "cons: second argument must be of type ") - (test '((+ (first (cons 1 empty)) 2)) - '(3)) - - (test - '((first (cons 1 empty))) - '(1)) - - (test - '((first 1)) - "first: expects argument of type ") - - (test - '((first 1 2)) - "first: expects one argument") - - (test - '((first)) - "first: expects one argument") - - (test - '((rest (cons 1 empty))) - '(empty)) - - (test - '((rest 1)) - "rest: expects argument of type ") - - (test - '((rest 1 2)) - "rest: expects one argument") - - (test - '((rest)) - "rest: expects one argument") - - (test - '((empty? empty)) - '(true)) - - (test - '((empty? 1)) - '(false)) - - (test - '((empty?)) - "empty?: expects one argument") - - (test - '((empty? 1 2)) - "empty?: expects one argument") - - (test - '((cond [true 1])) - '(1)) - - (test - '((cond [else 1])) - '(1)) - - (test-all - '((cond [false 1] [else 2])) - '(2)) - - (test-all - '((cond [false 1] [false 2])) - "cond: all question results were false") - - (test - '((cond [1 1])) - "cond: question result is not true or false") - - (test - '((cond [(empty? empty) 'infinite] [else 3])) - '('infinite)) - - (test-all - '((cond [(if false false false) 'x] [(if true true true) 'y] [(if false false false) 'z])) - '((cond [false 'x] [(if true true true) 'y] [(if false false false) 'z])) - '((cond [false 'x] [true 'y] [(if false false false) 'z])) - '('y)) - - (test-all - '((cond [(if false false false) 'x] [(if true true true) 'y] [else 'z])) - '((cond [false 'x] [(if true true true) 'y] [else 'z])) - '((cond [false 'x] [true 'y] [else 'z])) - '('y)) - - (test-all - '((cond [(if false false false) 'x] [(if false false false) 'y] [else 'z])) - '((cond [false 'x] [(if false false false) 'y] [else 'z])) - '((cond [false 'x] [false 'y] [else 'z])) - '('z)) - - (test-all - '((and true true 3)) - "and: question result is not true or false") - - (test-all - '((and 1 true true)) - "and: question result is not true or false") - - (test-all - '((and true true true false)) - '(false)) - - (test-all - '((and false true)) - '(false)) - - (test-all - '((or false false 3)) - "or: question result is not true or false") - - (test-all - '((or 1 false false)) - "or: question result is not true or false") - - (test-all - '((or false false false true)) - '(true)) - - (test-all - '((or true false)) - '(true)) - - (test-all - '((or (if false false false) (if false false false) (if true true true) (if false false false))) - '((or false (if false false false) (if true true true) (if false false false))) - '((or false false (if true true true) (if false false false))) - '((or false false true (if false false false))) - '(true)) - - (test-all - '((and (if true true true) (if true true true) (if false false false) (if true true true))) - '((and true (if true true true) (if false false false) (if true true true))) - '((and true true (if false false false) (if true true true))) - '((and true true false (if true true true))) - '(false)) - - (test - '((if 1 2 3)) - "if: question result is not true or false") - - (test - '((if true 'x 'y)) - '('x)) - - (test - '((if false 'x 'y)) - '('y)) - - ; test non-procedure-defs in context: - (test - `((+ 3 4) (define a 3) (+ 5 6)) - `(7 (define a 3) 11)) - - ; test reduction of non-procedure-defs: - (test - `((define a 13) (define b (+ a 9)) (+ 3 4)) - `((define a 13) (define b 22) 7)) - - ; test reduction of unbound ids in hole: - (test - `(x) - "reference to undefined identifier: x") - - ; test reduction of function-bound id in hole: - (test - `((define (a x) (+ x 1)) a) - "a is a procedure, so it must be applied to arguments") - - ; test reduction of non-procedure-def in application: - (test - `((define a 3) (a 9)) - "procedure application: expected procedure, given: 3"))) - - (define (run-big-test) - (parameterize ([show-dots #t]) - (tests - (test - '((define-struct pr (hd tl)) - (define (avg l) - (cond - [(empty? l) 'infinite] - [else (/ (sum l) (howmany/acc l 0))])) - (define (sum l) - (cond - [(empty? (pr-tl l)) (pr-hd l)] - [else (+ (pr-hd l) (sum (pr-tl l)))])) - (define (howmany/acc l acc) - (cond - [(empty? l) acc] - [else (howmany/acc (pr-tl l) (+ acc 1))])) - (avg empty) - (avg (make-pr 3 (make-pr 4 (make-pr 5 (make-pr 6 (make-pr 7 (make-pr 8 (make-pr 9 empty))))))))) - - '((define-struct pr (hd tl)) - (define (avg l) - (cond - [(empty? l) 'infinite] - [else (/ (sum l) (howmany/acc l 0))])) - (define (sum l) - (cond - [(empty? (pr-tl l)) (pr-hd l)] - [else (+ (pr-hd l) (sum (pr-tl l)))])) - (define (howmany/acc l acc) - (cond - [(empty? l) acc] - [else (howmany/acc (pr-tl l) (+ acc 1))])) - 'infinite - 6)) - (test - '((define (contains-sym? s l) - (cond - [(empty? l) false] - [true (or (symbol=? s (first l)) - (contains-sym? s (rest l)))])) - (contains-sym? 'x (cons 'z (cons 'y (cons 'x empty)))) - (contains-sym? 'a (cons 'p (cons 'q (cons 'p (cons 'q (cons 'p (cons 'q empty)))))))) - '((define (contains-sym? s l) - (cond - [(empty? l) false] - [true (or (symbol=? s (first l)) - (contains-sym? s (rest l)))])) - true - false))))) - - ;; timing test - ;#; - (time (run-tests) - (run-big-test))) + false))))) +;; timing test +;#; +(time (run-tests) + (run-big-test)) \ No newline at end of file diff --git a/collects/redex/examples/church.ss b/collects/redex/examples/church.ss index 06af4f7fa7..8bda565a1a 100644 --- a/collects/redex/examples/church.ss +++ b/collects/redex/examples/church.ss @@ -1,57 +1,56 @@ -(module church mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/gui)) - - (reduction-steps-cutoff 100) - - (define-language lang - (e (lambda (x) e) - (let (x e) e) - (app e e) - (+ e e) - number - x) - (e-ctxt (lambda (x) e-ctxt) - a-ctxt) - (a-ctxt (let (x a-ctxt) e) - (app a-ctxt e) - (app x a-ctxt) - hole) - (v (lambda (x) e) - x) - (x variable)) - - (define reductions - (reduction-relation - lang - (--> (in-hole e-ctxt_1 (app (lambda (x_1) e_body) e_arg)) - (in-hole e-ctxt_1 (subst (x_1 e_arg e_body)))) - (--> (in-hole e-ctxt_1 (let (x_1 v_1) e_1)) - (in-hole e-ctxt_1 (subst (x_1 v_1 e_1)))))) - - (define-metafunction subst - lang - [(x_1 e_1 (lambda (x_1) e_2)) (lambda (x_1) e_2)] - [(x_1 e_1 (lambda (x_2) e_2)) - ,(term-let ((x_new (variable-not-in (term e_1) (term x_2)))) - (term (lambda (x_new) (subst (x_1 e_1 (subst (x_2 x_new e_2)))))))] - [(x_1 e_1 (let (x_1 e_2) e_3)) (let (x_1 (subst (x_1 e_1 e_2))) e_3)] - [(x_1 e_1 (let (x_2 e_2) e_3)) - ,(term-let ((x_new (variable-not-in (term e_1) (term x_2)))) - (term (let (x_2 (subst (x_1 e_1 e_2))) (subst (x_1 e_1 (subst (x_2 x_new e_3)))))))] - [(x_1 e_1 x_1) e_1] - [(x_1 e_1 x_2) x_2] - [(x_1 e_1 (app e_2 e_3)) (app (subst (x_1 e_1 e_2)) - (subst (x_1 e_1 e_3)))] - [(x_1 e_1 (+ e_2 e_3)) (+ (subst (x_1 e_1 e_2)) - (subst (x_1 e_1 e_3)))] - [(x_1 e_1 number_1) number_1]) - - (traces lang reductions - '(let (plus (lambda (m) - (lambda (n) - (lambda (s) - (lambda (z) - (app (app m s) (app (app n s) z))))))) - (let (two (lambda (s) (lambda (z) (app s (app s z))))) - (app (app plus two) two))))) \ No newline at end of file +#lang scheme +(require redex) + +(reduction-steps-cutoff 100) + +(define-language lang + (e (lambda (x) e) + (let (x e) e) + (app e e) + (+ e e) + number + x) + (e-ctxt (lambda (x) e-ctxt) + a-ctxt) + (a-ctxt (let (x a-ctxt) e) + (app a-ctxt e) + (app x a-ctxt) + hole) + (v (lambda (x) e) + x) + (x variable)) + +(define reductions + (reduction-relation + lang + (--> (in-hole e-ctxt_1 (app (lambda (x_1) e_body) e_arg)) + (in-hole e-ctxt_1 (subst (x_1 e_arg e_body)))) + (--> (in-hole e-ctxt_1 (let (x_1 v_1) e_1)) + (in-hole e-ctxt_1 (subst (x_1 v_1 e_1)))))) + +(define-metafunction subst + lang + [(x_1 e_1 (lambda (x_1) e_2)) (lambda (x_1) e_2)] + [(x_1 e_1 (lambda (x_2) e_2)) + ,(term-let ((x_new (variable-not-in (term e_1) (term x_2)))) + (term (lambda (x_new) (subst (x_1 e_1 (subst (x_2 x_new e_2)))))))] + [(x_1 e_1 (let (x_1 e_2) e_3)) (let (x_1 (subst (x_1 e_1 e_2))) e_3)] + [(x_1 e_1 (let (x_2 e_2) e_3)) + ,(term-let ((x_new (variable-not-in (term e_1) (term x_2)))) + (term (let (x_2 (subst (x_1 e_1 e_2))) (subst (x_1 e_1 (subst (x_2 x_new e_3)))))))] + [(x_1 e_1 x_1) e_1] + [(x_1 e_1 x_2) x_2] + [(x_1 e_1 (app e_2 e_3)) (app (subst (x_1 e_1 e_2)) + (subst (x_1 e_1 e_3)))] + [(x_1 e_1 (+ e_2 e_3)) (+ (subst (x_1 e_1 e_2)) + (subst (x_1 e_1 e_3)))] + [(x_1 e_1 number_1) number_1]) + +(traces lang reductions + '(let (plus (lambda (m) + (lambda (n) + (lambda (s) + (lambda (z) + (app (app m s) (app (app n s) z))))))) + (let (two (lambda (s) (lambda (z) (app s (app s z))))) + (app (app plus two) two)))) \ No newline at end of file diff --git a/collects/redex/examples/combinators.ss b/collects/redex/examples/combinators.ss index b4d25faac1..9d1f4ef1d9 100644 --- a/collects/redex/examples/combinators.ss +++ b/collects/redex/examples/combinators.ss @@ -1,90 +1,91 @@ +#lang scheme + ;"one point basis" ;"formal aspects of computing" -(module combinators mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/gui)) - - (initial-font-size 12) - (reduction-steps-cutoff 100) - (initial-char-width 80) - - (define-language lang - (e (e e) - comb - abs1 - abs2 - abs3) - (e-ctxt (e e-ctxt) - (e-ctxt e) - hole) - (comb i - j - b - c - c* - w)) - - (define ij-relation - (reduction-relation - lang - (--> (in-hole e-ctxt_1 (i e_1)) - (in-hole e-ctxt_1 e_1)) - (--> (in-hole e-ctxt_1 ((((j e_a) e_b) e_c) e_d)) - (in-hole e-ctxt_1 ((e_a e_b) ((e_a e_d) e_c)))))) - - (define relation - (union-reduction-relations - ij-relation - (reduction-relation - lang - (--> (in-hole e-ctxt_1 (((b e_m) e_n) e_l)) - (in-hole e-ctxt_1 (e_m (e_n e_l)))) - (--> (in-hole e-ctxt_1 (((c e_m) e_n) e_l)) - (in-hole e-ctxt_1 ((e_m e_l) e_n))) - (--> (in-hole e-ctxt_1 ((c* e_a) e_b)) - (in-hole e-ctxt_1 (e_b e_a))) - (--> (in-hole e-ctxt_1 ((w e_a) e_b)) - (in-hole e-ctxt_1 ((e_a e_b) e_b)))))) +(require redex) - - (define c* `((j i) i)) - (define (make-c c*) `(((j ,c*) (j ,c*)) (j ,c*))) - (define (make-b c) `((,c ((j i) ,c)) (j i))) - (define (make-w b c c*) `(,c ((,c ((,b ,c) ((,c ((,b j) ,c*)) ,c*))) ,c*))) - (define (make-s b c w) `((,b ((,b (,b ,w)) ,c)) (,b ,b))) +(initial-font-size 12) +(reduction-steps-cutoff 100) +(initial-char-width 80) - (traces/multiple lang - relation - (list - `((,c* abs1) abs2) - `(((,(make-c 'c*) abs1) abs2) abs3) - `(((,(make-b 'c) abs1) abs2) abs3) - `((,(make-w 'b 'c 'c*) abs1) abs2) - `(((,(make-s 'b 'c 'w) abs1) abs2) abs3))) - - (require (lib "pretty.ss")) - #; - (let loop ([t (make-s (make-b (make-c c*)) +(define-language lang + (e (e e) + comb + abs1 + abs2 + abs3) + (e-ctxt (e e-ctxt) + (e-ctxt e) + hole) + (comb i + j + b + c + c* + w)) + +(define ij-relation + (reduction-relation + lang + (--> (in-hole e-ctxt_1 (i e_1)) + (in-hole e-ctxt_1 e_1)) + (--> (in-hole e-ctxt_1 ((((j e_a) e_b) e_c) e_d)) + (in-hole e-ctxt_1 ((e_a e_b) ((e_a e_d) e_c)))))) + +(define relation + (union-reduction-relations + ij-relation + (reduction-relation + lang + (--> (in-hole e-ctxt_1 (((b e_m) e_n) e_l)) + (in-hole e-ctxt_1 (e_m (e_n e_l)))) + (--> (in-hole e-ctxt_1 (((c e_m) e_n) e_l)) + (in-hole e-ctxt_1 ((e_m e_l) e_n))) + (--> (in-hole e-ctxt_1 ((c* e_a) e_b)) + (in-hole e-ctxt_1 (e_b e_a))) + (--> (in-hole e-ctxt_1 ((w e_a) e_b)) + (in-hole e-ctxt_1 ((e_a e_b) e_b)))))) + + +(define c* `((j i) i)) +(define (make-c c*) `(((j ,c*) (j ,c*)) (j ,c*))) +(define (make-b c) `((,c ((j i) ,c)) (j i))) +(define (make-w b c c*) `(,c ((,c ((,b ,c) ((,c ((,b j) ,c*)) ,c*))) ,c*))) +(define (make-s b c w) `((,b ((,b (,b ,w)) ,c)) (,b ,b))) + +(traces lang + relation + (list + `((,c* abs1) abs2) + `(((,(make-c 'c*) abs1) abs2) abs3) + `(((,(make-b 'c) abs1) abs2) abs3) + `((,(make-w 'b 'c 'c*) abs1) abs2) + `(((,(make-s 'b 'c 'w) abs1) abs2) abs3)) + #:multiple #t) + +(require (lib "pretty.ss")) +#; +(let loop ([t (make-s (make-b (make-c c*)) + (make-c c*) + (make-w (make-b (make-c c*)) + (make-c c*) + c*))] + [i 0]) + (when (zero? (modulo i 100)) + (display i) + (display " ") + (flush-output)) + (let ([next (apply-reduction-relation ij-relation t)]) + (if (null? next) + (begin (newline) + (pretty-print t)) + (loop (car next) (+ i 1))))) + +#; +(traces lang ij-relation + (make-s (make-b (make-c c*)) + (make-c c*) + (make-w (make-b (make-c c*)) (make-c c*) - (make-w (make-b (make-c c*)) - (make-c c*) - c*))] - [i 0]) - (when (zero? (modulo i 100)) - (display i) - (display " ") - (flush-output)) - (let ([next (apply-reduction-relation ij-relation t)]) - (if (null? next) - (begin (newline) - (pretty-print t)) - (loop (car next) (+ i 1))))) - - #; - (traces lang ij-relation - (make-s (make-b (make-c c*)) - (make-c c*) - (make-w (make-b (make-c c*)) - (make-c c*) - c*)))) + c*))) \ No newline at end of file diff --git a/collects/redex/examples/compatible-closure.ss b/collects/redex/examples/compatible-closure.ss index 1c949b082b..9187794059 100644 --- a/collects/redex/examples/compatible-closure.ss +++ b/collects/redex/examples/compatible-closure.ss @@ -1,18 +1,17 @@ -(module compatible-closure mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/gui)) - - (define-language grammar - (B t - f - (B * B))) +#lang scheme +(require redex) - (define r - (reduction-relation - grammar - (--> (f * B_1) B_1 false) ; [a] - (--> (t * B_1) t true))) ; [b] +(define-language grammar + (B t + f + (B * B))) - (define ->r (compatible-closure r grammar B)) - - (traces grammar ->r '((f * f) * (t * f)))) +(define r + (reduction-relation + grammar + (--> (f * B_1) B_1 false) ; [a] + (--> (t * B_1) t true))) ; [b] + +(define ->r (compatible-closure r grammar B)) + +(traces grammar ->r '((f * f) * (t * f))) diff --git a/collects/redex/examples/eta.ss b/collects/redex/examples/eta.ss deleted file mode 100644 index 416f05fb26..0000000000 --- a/collects/redex/examples/eta.ss +++ /dev/null @@ -1,67 +0,0 @@ -(module eta mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/gui) - (planet robby/redex:5/subst)) - - (reduction-steps-cutoff 100) - - (define-language lang - (e (e e) - x - (+ e e) - v) - (c (v c) - (c e) - (+ v c) - (+ c e) - hole) - (v (lambda (x) e) - number) - (x (variable-except lambda +))) - - (define reductions - (reduction-relation - lang - (c=> ((lambda (variable_x) e_body) v_arg) - ,(lc-subst (term variable_x) (term v_arg) (term e_body))) - (c=> (+ number_1 number_2) - ,(+ (term number_1) (term number_2))) - (c=> (side-condition (lambda (variable_x) (e_fun variable_x)) - (equal? (term e_fun) (lc-subst (term variable_x) 1234 (term e_fun)))) - e_fun) - - (--> (in-hole c (number_n v_arg)) - ,(format "procedure application: expected procedure, given: ~a; arguments were: ~a" - (term number_n) - (term v_arg))) - (--> (in-hole c (+ (name non-num (lambda (variable) e)) (name arg2 v))) - ,(format "+: expects type as 1st argument, given: ~s; other arguments were: ~s" - (term non-num) (term arg2))) - (--> (in-hole c (+ (name arg1 v) (name non-num (lambda (variable) e)))) - ,(format "+: expects type as 2nd argument, given: ~s; other arguments were: ~s" - (term arg1) (term non-num))) - - where - - [(c=> x y) (--> (in-hole c_1 x) (in-hole c_1 y))])) - - (define lc-subst - (subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list x) b)] - [`(+ ,n2 ,n1) - (all-vars '()) - (build (lambda (vars n1 n2) `(+ ,n1 ,n1))) - (subterm '() n1) - (subterm '() n2)] - [`(,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(,f ,x))) - (subterm '() f) - (subterm '() x)])) - - (traces lang reductions '(+ (lambda (x) ((+ 1 2) x)) 1))) \ No newline at end of file diff --git a/collects/redex/examples/iswim.ss b/collects/redex/examples/iswim.ss deleted file mode 100644 index 10498a284a..0000000000 --- a/collects/redex/examples/iswim.ss +++ /dev/null @@ -1,254 +0,0 @@ -(module iswim mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/subst) - (lib "contract.ss")) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Expression grammar: - - (define-language iswim-grammar - (M (M M) - (o1 M) - (o2 M M) - V - ("letcc" X M) - ("cc" M M)) - (V X - ("lam" variable M) - b - ("[" M "]")) - (X variable) - (b number) - (o1 "add1" "sub1" "iszero") - (o2 "+" "-" "*" "^") - (on o1 o2) - - ;; Evaluation contexts: - (E hole - (E M) - (V E) - (o1 E) - (o2 E M) - (o2 V E) - ("cc" E M) - ("cc" V E)) - - ;; Continuations (CK machine): - (k "mt" - ("fun" V k) - ("arg" M k) - ("narg" (V ... on) (M ...) k)) - - ;; Environments and closures (CEK): - (env ((X = vcl) ...)) - (cl (M : env)) - (vcl (V- : env)) - - ;; Values that are not variables: - (V- ("lam" variable M) - b) - - ;; Continuations with closures (CEK): - (k- "mt" - ("fun" vcl k-) - ("arg" cl k-) - ("narg" (vcl ... on) (cl ...) k-))) - - (define M? (redex-match iswim-grammar M)) - (define V? (redex-match iswim-grammar V)) - (define o1? (redex-match iswim-grammar o1)) - (define o2? (redex-match iswim-grammar o2)) - (define on? (redex-match iswim-grammar on)) - (define k? (redex-match iswim-grammar k)) - - (define env? (redex-match iswim-grammar env)) - (define cl? (redex-match iswim-grammar cl)) - (define vcl? (redex-match iswim-grammar vcl)) - (define k-? (redex-match iswim-grammar k-)) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Substitution: - - ;; The subst form makes implemention of capture-avoiding - ;; easier. We just have to describe how variables bind - ;; in our language's forms. - - (define iswim-subst/backwards - (subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`("lam" ,X ,M) - (all-vars (list X)) - (build (lambda (X-list M) `("lam" ,(car X-list) ,M))) - (subterm (list X) M)] - [`(,(and o (or "add1" "sub1" "iszero")) ,M1) - (all-vars '()) - (build (lambda (vars M1) `(,o ,M1))) - (subterm '() M1)] - [`(,(and o (or "+" "-" "*" "^")) ,M1 ,M2) - (all-vars '()) - (build (lambda (vars M1 M2) `(,o ,M1 ,M2))) - (subterm '() M1) - (subterm '() M2)] - [`(,M1 ,M2) - (all-vars '()) - (build (lambda (empty-list M1 M2) `(,M1 ,M2))) - (subterm '() M1) - (subterm '() M2)] - [`("letcc" ,X ,M) - (all-vars (list X)) - (build (lambda (X-list M) `("letcc" ,(car X-list) ,M))) - (subterm (list X) M)] - [`("cc" ,M1 ,M2) - (all-vars '()) - (build (lambda (vars M1 M2) `("cc" ,M1 ,M2))) - (subterm '() M1) - (subterm '() M2)] - [`("[" ,E "]") - (all-vars '()) - (build (lambda (vars) `("[" ,E "]")))])) - - - ;; the argument order for the subst-generated function - ;; doesn't match the order in the notes: - (define (iswim-subst M Xr Mr) - (iswim-subst/backwards Xr Mr M)) - - (define empty-env '()) - - ;; Environment lookup - (define (env-lookup env X) - (let ([m (assq X env)]) - (and m (caddr m)))) - - ;; Environment extension - (define (env-extend env X vcl) - (cons (list X '= vcl) env)) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Reductions: - - ;; beta_v reduction - (define beta_v - (reduction-relation - iswim-grammar - (--> (("lam" X_1 M_1) V_1) - ,(iswim-subst (term M_1) (term X_1) (term V_1))))) - - (define delta - (reduction-relation - iswim-grammar - (--> ("add1" b_1) ,(add1 (term b_1))) - (--> ("sub1" b_1) ,(sub1 (term b_1))) - (--> ("iszero" b_1) - ,(if (zero? (term b_1)) - (term ("lam" x ("lam" y x))) - (term ("lam" x ("lam" y y))))) - (--> ("+" b_1 b_2) ,(+ (term b_1) (term b_2))) - (--> ("-" b_1 b_2) ,(- (term b_1) (term b_2))) - (--> ("*" b_1 b_2) ,(* (term b_1) (term b_2))) - (--> ("^" b_1 b_2) ,(expt (term b_1) (term b_2))))) - - ;; ->v - (define ->v (compatible-closure (union-reduction-relations beta_v delta) - iswim-grammar - M)) - - ;; :->v - (define :->v (context-closure (union-reduction-relations beta_v delta) - iswim-grammar - E)) - - ;; :->v+letcc - (define :->v+letcc - (union-reduction-relations - :->v - (reduction-relation - iswim-grammar - - ;; letcc rule: - (--> (in-hole E_1 ("letcc" X_1 M_1)) - (in-hole E_1 ,(iswim-subst (term M_1) - (term X_1) - `("[" (in-hole E_1 ||) "]")))) - - ;; cc rule: - (--> (in-hole E ("cc" ("[" (in-hole E_2 ||) "]") V_1)) - (in-hole E_2 V_1))))) - - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Helpers: - - (define (delta*n on Vs) - (let ([l (apply-reduction-relation delta `(,on ,@Vs))]) - (if (null? l) - #f - (car l)))) - - (define (delta*1 o1 V) - (delta*n o1 (list V))) - - (define (delta*2 o2 V1 V2) - (delta*n o2 (list V1 V2))) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Abbreviations: - - (define (if0 test then else) - (let ([X (variable-not-in `(,then ,else) 'X)]) - `(((("iszero" ,test) ("lam" ,X ,then)) ("lam" ,X ,else)) 77))) - - (define true '("lam" x ("lam" y x))) - (define false '("lam" x ("lam" y y))) - (define boolean-not `("lam" x ((x ,false) ,true))) - - (define mkpair '("lam" x ("lam" y ("lam" s ((s x) y))))) - (define fst '("lam" p (p ("lam" x ("lam" y x))))) - (define snd '("lam" p (p ("lam" x ("lam" y y))))) - - (define Y_v '("lam" f ("lam" x - ((("lam" g (f ("lam" x ((g g) x)))) - ("lam" g (f ("lam" x ((g g) x))))) - x)))) - - (define mksum `("lam" s - ("lam" x - ,(if0 'x 0 '("+" x (s ("sub1" x))))))) - (define sum `(,Y_v ,mksum)) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Exports: - - (provide iswim-grammar) - - (provide/contract (M? (any/c . -> . any/c)) - (V? (any/c . -> . any/c)) - (o1? (any/c . -> . any/c)) - (o2? (any/c . -> . any/c)) - (on? (any/c . -> . any/c)) - (k? (any/c . -> . any/c)) - (env? (any/c . -> . any/c)) - (cl? (any/c . -> . any/c)) - (vcl? (any/c . -> . any/c)) - (iswim-subst (M? symbol? M? . -> . M?)) - (env-lookup (env? symbol? . -> . (union false/c vcl?))) - (env-extend (env? symbol? vcl? . -> . env?)) - (empty-env env?) - (beta_v reduction-relation?) - (delta reduction-relation?) - (delta*1 (o1? V? . -> . (union false/c V?))) - (delta*2 (o2? V? V? . -> . (union false/c V?))) - (delta*n (on? (listof V?) . -> . (union false/c V?))) - (->v reduction-relation?) - (:->v reduction-relation?) - (:->v+letcc reduction-relation?) - (if0 (M? M? M? . -> . M?)) - (true M?) - (false M?) - (boolean-not M?) - (mkpair M?) - (fst M?) - (snd M?) - (Y_v M?) - (sum M?))) diff --git a/collects/redex/examples/letrec.ss b/collects/redex/examples/letrec.ss index 0e728d3d61..cd638db491 100644 --- a/collects/redex/examples/letrec.ss +++ b/collects/redex/examples/letrec.ss @@ -1,155 +1,130 @@ -(module letrec mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/gui) - (planet robby/redex:5/subst) - (lib "list.ss")) +#lang scheme + +#| + +BUG: letrec & let are not handled properly by substitution + +|# + +(require redex "subst.ss") + +(reduction-steps-cutoff 20) + +(define-language lang + (p ((store (x v) ...) e)) + (e (set! x e) + (let ((x e)) e) + (letrec ((x e)) e) + (begin e e ...) + (e e) + x + v) + (v (lambda (x) e) + number) + (x variable) + (pc ((store (x v) ...) ec)) + (ec (ec e) + (v ec) + (set! variable ec) + (let ((x ec)) e) + (begin ec e e ...) + hole)) + +;; collect : term -> term +;; performs a garbage collection on the term `p' +(define (collect p) + (define (substitute var exp body) + (term-let ((var var) + (exp exp) + (body body)) + (term (subst (var exp body))))) - (reduction-steps-cutoff 20) + (define (find-unused vars p) + (filter (λ (var) (unused? var p)) + vars)) - (define-language lang - (p ((store (x v) ...) e)) - (e (set! x e) - (let ((x e)) e) - (letrec ((x e)) e) - (begin e e ...) - (e e) - x - v) - (v (lambda (x) e) - number) - (x variable) - (pc ((store (x v) ...) ec)) - (ec (ec e) - (v ec) - (set! variable ec) - (let ((x ec)) e) - (begin ec e e ...) - hole)) + (define (unused? var p) + (let ([rhss (map cadr (cdar p))] + [body (cadr p)]) + (and (not (free-in? var body)) + (andmap (λ (rhs) (not (free-in? var rhs))) + rhss)))) - (define substitute - (subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list x) b)] - [`(set! ,x ,e) - (all-vars '()) - (build (lambda (vars name body) `(set! ,name ,body))) - (subterm '() x) - (subterm '() e)] - [`(let ((,x ,e1)) ,e2) - (all-vars (list x)) - (build (lambda (vars letval body) `(let ((,(car vars) ,letval)) ,body))) - (subterm '() e1) - (subterm (list x) e2)] - [`(letrec ((,x ,e1)) ,e2) - (all-vars (list x)) - (build (lambda (vars letval body) `(letrec ((,(car vars) ,letval)) ,body))) - (subterm (list x) e1) - (subterm (list x) e2)] - [`(begin ,@(es ...)) - (all-vars (list)) - (build (lambda (vars . rest) `(begin ,@rest))) - (subterms '() es)] - [`(,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(,f ,x))) - (subterm '() f) - (subterm '() x)])) + (define (free-in? var body) + (not (equal? (substitute var (gensym) body) + body))) - ;; collect : term -> term - ;; performs a garbage collection on the term `p' - (define (collect p) - (define (find-unused vars p) - (filter (λ (var) (unused? var p)) - vars)) - - (define (unused? var p) - (let ([rhss (map cadr (cdar p))] - [body (cadr p)]) - (and (not (free-in? var body)) - (andmap (λ (rhs) (not (free-in? var rhs))) - rhss)))) - - (define (free-in? var body) - (not (equal? (substitute var (gensym) body) - body))) - - (define (remove-unused vars p) - `((store ,@(filter (λ (binding) (not (memq (car binding) vars))) - (cdar p))) - ,(cadr p))) - - (let* ([vars (map car (cdar p))] - [unused (find-unused vars p)]) - (cond - [(null? unused) p] - [else - (collect (remove-unused unused p))]))) + (define (remove-unused vars p) + `((store ,@(filter (λ (binding) (not (memq (car binding) vars))) + (cdar p))) + ,(cadr p))) - (define reductions - (reduction-relation - lang - (==> (in-hole pc_1 (begin v e_1 e_2 ...)) - (in-hole pc_1 (begin e_1 e_2 ...)) - begin\ many) - - (==> (in-hole pc_1 (begin e_1)) - (in-hole pc_1 e_1) - begin\ one) - - (==> ((store (x_before v_before) ... - (x_i v_i) - (x_after v_after) ...) - (in-hole ec_1 x_i)) - ((store - (x_before v_before) ... - (x_i v_i) - (x_after v_after) ...) - (in-hole ec_1 v_i)) - deref) - - (==> ((store (x_before v_before) ... - (x_i v) - (x_after v_after) ...) - (in-hole ec_1 (set! x_i v_new))) - ((store (x_before v_before) ... - (x_i v_new) - (x_after v_after) ...) - (in-hole ec_1 v_new)) - set!) - - (==> (in-hole pc_1 ((lambda (x_1) e_1) v_1)) - (in-hole pc_1 - ,(substitute (term x_1) (term v_1) (term e_1))) - βv) - - (==> ((store (name the-store any) ...) - (in-hole ec_1 (let ((x_1 v_1)) e_1))) - ,(let ((new-x (variable-not-in (term (the-store ...)) (term x_1)))) - (term - ((store the-store ... (,new-x v_1)) - (in-hole ec_1 - ,(substitute (term x_1) new-x (term e_1)))))) - let) - - (==> (in-hole pc_1 (letrec ((x_1 e_1)) e_2)) - (in-hole pc_1 (let ((x_1 0)) (begin (set! x_1 e_1) e_2))) - letrec) - - where - [(==> a b) (--> a ,(collect (term b)))])) - - (define (run e) (traces lang reductions `((store) ,e))) - - (run '(letrec ((f (lambda (x) - (letrec ((y (f 1))) - 2)))) - (f 3))) - - (run '(letrec ((f (lambda (x) - (letrec ((y 1)) - (f 1))))) - (f 3)))) + (let* ([vars (map car (cdar p))] + [unused (find-unused vars p)]) + (cond + [(null? unused) p] + [else + (collect (remove-unused unused p))]))) + +(define reductions + (reduction-relation + lang + (==> (in-hole pc_1 (begin v e_1 e_2 ...)) + (in-hole pc_1 (begin e_1 e_2 ...)) + begin\ many) + + (==> (in-hole pc_1 (begin e_1)) + (in-hole pc_1 e_1) + begin\ one) + + (==> ((store (x_before v_before) ... + (x_i v_i) + (x_after v_after) ...) + (in-hole ec_1 x_i)) + ((store + (x_before v_before) ... + (x_i v_i) + (x_after v_after) ...) + (in-hole ec_1 v_i)) + deref) + + (==> ((store (x_before v_before) ... + (x_i v) + (x_after v_after) ...) + (in-hole ec_1 (set! x_i v_new))) + ((store (x_before v_before) ... + (x_i v_new) + (x_after v_after) ...) + (in-hole ec_1 v_new)) + set!) + + (==> (in-hole pc_1 ((lambda (x_1) e_1) v_1)) + (in-hole pc_1 (subst (x_1 v_1 e_1))) + βv) + + (==> ((store (name the-store any) ...) + (in-hole ec_1 (let ((x_1 v_1)) e_1))) + ,(let ((new-x (variable-not-in (term (the-store ...)) (term x_1)))) + (term + ((store the-store ... (,new-x v_1)) + (in-hole ec_1 (subst (x_1 ,new-x e_1)))))) + let) + + (==> (in-hole pc_1 (letrec ((x_1 e_1)) e_2)) + (in-hole pc_1 (let ((x_1 0)) (begin (set! x_1 e_1) e_2))) + letrec) + + with + [(--> a ,(collect (term b))) (==> a b)])) + +(define (run e) (traces lang reductions `((store) ,e))) + +(run '(letrec ((f (lambda (x) + (letrec ((y (f 1))) + 2)))) + (f 3))) + +(run '(letrec ((f (lambda (x) + (letrec ((y 1)) + (f 1))))) + (f 3))) diff --git a/collects/redex/examples/omega.ss b/collects/redex/examples/omega.ss index ddda032efa..927997aed6 100644 --- a/collects/redex/examples/omega.ss +++ b/collects/redex/examples/omega.ss @@ -1,60 +1,36 @@ -(module omega mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/subst) - (planet robby/redex:5/gui)) +#lang scheme +(require redex "subst.ss") + +(reduction-steps-cutoff 10) + +(define-language lang + (e (e e) + (abort e) + x + v) + (c (v c) + (c e) + hole) + (v call/cc + number + (lambda (x) e)) - (reduction-steps-cutoff 10) - - (define-language lang - (e (e e) - (abort e) - x - v) - (c (v c) - (c e) - hole) - (v call/cc - number - (lambda (x) e)) - - (x (variable-except lambda call/cc abort))) - - (define reductions - (reduction-relation - lang - (--> (in-hole c_1 (call/cc v_arg)) - ,(term-let ([v (variable-not-in (term c_1) 'x)]) - (term (in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v))))))) - call/cc) - (--> (in-hole c (abort e_1)) - e_1 - abort) - (--> (in-hole c_1 ((lambda (variable_x) e_body) v_arg)) - (in-hole c_1 ,(lc-subst (term variable_x) (term v_arg) (term e_body))) - βv))) - - (define lc-subst - (plt-subst - ['abort (constant)] - ['call/cc (constant)] - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list x) b)] - [`(call/cc ,v) - (all-vars '()) - (build (lambda (vars arg) `(call/cc ,arg))) - (subterm '() v)] - [`(,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(,f ,x))) - (subterm '() f) - (subterm '() x)])) - - - (traces lang reductions '((lambda (x) (x x)) (lambda (x) (x x)))) - (traces lang reductions '((call/cc call/cc) (call/cc call/cc))) - (traces lang reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc))) - ) + (x (variable-except lambda call/cc abort))) + +(define reductions + (reduction-relation + lang + (--> (in-hole c_1 (call/cc v_arg)) + ,(term-let ([v (variable-not-in (term c_1) 'x)]) + (term (in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v))))))) + call/cc) + (--> (in-hole c (abort e_1)) + e_1 + abort) + (--> (in-hole c_1 ((lambda (variable_x) e_body) v_arg)) + (in-hole c_1 (subst (variable_x v_arg e_body))) + βv))) + +(traces lang reductions '((lambda (x) (x x)) (lambda (x) (x x)))) +(traces lang reductions '((call/cc call/cc) (call/cc call/cc))) +(traces lang reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc))) diff --git a/collects/redex/examples/semaphores.ss b/collects/redex/examples/semaphores.ss index 501c2397cb..5ba1f7718d 100644 --- a/collects/redex/examples/semaphores.ss +++ b/collects/redex/examples/semaphores.ss @@ -1,169 +1,168 @@ +#lang scheme +(require redex) + #| semaphores make things much more predictable... |# -(module semaphores mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/gui)) - - (reduction-steps-cutoff 100) - - (define-language lang - (p ((store (variable v) ...) - (semas (variable sema-count) ...) - (threads e ...))) - (sema-count number - none) - (e (set! variable e) - (begin e ...) - (semaphore variable) - (semaphore-wait e) - (semaphore-post e) - (lambda (variable) e) - (e e) - variable - (list e ...) - (cons e e) - number - (void)) - (p-ctxt ((store (variable v) ...) - (semas (variable sema-count) ...) - (threads e ... e-ctxt e ...))) - (e-ctxt (e-ctxt e) - (v e-ctxt) - (cons e-ctxt e) - (cons v e-ctxt) - (list v ... e-ctxt e ...) - (set! variable e-ctxt) - (begin e-ctxt e ...) - (semaphore-wait e-ctxt) - (semaphore-post e-ctxt) - hole) - (v (semaphore variable) - (lambda (variable) e) - (list v ...) - number - (void))) - - (define reductions - (reduction-relation - lang - (--> (in-hole (name c p-ctxt) (begin v e_1 e_2 e_rest ...)) - (in-hole c (begin e_1 e_2 e_rest ...))) - (--> (in-hole (name c p-ctxt) (cons v_1 (list v_2s ...))) - (in-hole c (list v_1 v_2s ...))) - (--> (in-hole (name c p-ctxt) (begin v e_1)) - (in-hole c e_1)) - (--> (in-hole (name c p-ctxt) (begin v_1)) - (in-hole c v_1)) - (--> ((store - (variable_before v_before) ... - ((name x variable) (name v v)) - (variable_after v_after) ...) - (name semas any) - (threads - e_before ... - (in-hole (name c e-ctxt) (name x variable)) - e_after ...)) - ((store - (variable_before v_before) ... - (x v) - (variable_after v_after) ...) - semas - (threads - e_before ... - (in-hole c v) - e_after ...))) - (--> ((store (variable_before v_before) ... - (variable_i v) +(reduction-steps-cutoff 100) + +(define-language lang + (p ((store (variable v) ...) + (semas (variable sema-count) ...) + (threads e ...))) + (sema-count number + none) + (e (set! variable e) + (begin e ...) + (semaphore variable) + (semaphore-wait e) + (semaphore-post e) + (lambda (variable) e) + (e e) + variable + (list e ...) + (cons e e) + number + (void)) + (p-ctxt ((store (variable v) ...) + (semas (variable sema-count) ...) + (threads e ... e-ctxt e ...))) + (e-ctxt (e-ctxt e) + (v e-ctxt) + (cons e-ctxt e) + (cons v e-ctxt) + (list v ... e-ctxt e ...) + (set! variable e-ctxt) + (begin e-ctxt e ...) + (semaphore-wait e-ctxt) + (semaphore-post e-ctxt) + hole) + (v (semaphore variable) + (lambda (variable) e) + (list v ...) + number + (void))) + +(define reductions + (reduction-relation + lang + (--> (in-hole (name c p-ctxt) (begin v e_1 e_2 e_rest ...)) + (in-hole c (begin e_1 e_2 e_rest ...))) + (--> (in-hole (name c p-ctxt) (cons v_1 (list v_2s ...))) + (in-hole c (list v_1 v_2s ...))) + (--> (in-hole (name c p-ctxt) (begin v e_1)) + (in-hole c e_1)) + (--> (in-hole (name c p-ctxt) (begin v_1)) + (in-hole c v_1)) + (--> ((store + (variable_before v_before) ... + ((name x variable) (name v v)) + (variable_after v_after) ...) + (name semas any) + (threads + e_before ... + (in-hole (name c e-ctxt) (name x variable)) + e_after ...)) + ((store + (variable_before v_before) ... + (x v) + (variable_after v_after) ...) + semas + (threads + e_before ... + (in-hole c v) + e_after ...))) + (--> ((store (variable_before v_before) ... + (variable_i v) + (variable_after v_after) ...) + (name semas any) + (threads + e_before ... + (in-hole (name c e-ctxt) (set! variable_i v_new)) + e_after ...)) + ((store (variable_before v_before) ... + (variable_i v_new) + (variable_after v_after) ...) + semas + (threads + e_before ... + (in-hole c (void)) + e_after ...))) + (--> ((name store any) + (semas + (variable_before v_before) ... + (variable_sema number_n) + (variable_after v_after) ...) + (threads + e_before ... + (in-hole (name c e-ctxt) (semaphore-wait (semaphore variable_sema))) + e_after ...)) + (store + (semas + (variable_before v_before) ... + (variable_sema ,(if (= (term number_n) 1) + (term none) + (- (term number_n) 1))) (variable_after v_after) ...) - (name semas any) - (threads - e_before ... - (in-hole (name c e-ctxt) (set! variable_i v_new)) - e_after ...)) - ((store (variable_before v_before) ... - (variable_i v_new) + (threads + e_before ... + (in-hole c (void)) + e_after ...))) + (--> ((name store any) + (semas + (variable_before v_before) ... + (variable_sema number_n) + (variable_after v_after) ...) + (threads + e_before ... + (in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema))) + e_after ...)) + (store + (semas + (variable_before v_before) ... + (variable_sema ,(+ (term number_n) 1)) (variable_after v_after) ...) - semas - (threads - e_before ... - (in-hole c (void)) - e_after ...))) - (--> ((name store any) - (semas - (variable_before v_before) ... - (variable_sema number_n) - (variable_after v_after) ...) - (threads - e_before ... - (in-hole (name c e-ctxt) (semaphore-wait (semaphore variable_sema))) - e_after ...)) - (store - (semas - (variable_before v_before) ... - (variable_sema ,(if (= (term number_n) 1) - (term none) - (- (term number_n) 1))) - (variable_after v_after) ...) - (threads - e_before ... - (in-hole c (void)) - e_after ...))) - (--> ((name store any) - (semas - (variable_before v_before) ... - (variable_sema number_n) - (variable_after v_after) ...) - (threads - e_before ... - (in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema))) - e_after ...)) - (store - (semas - (variable_before v_before) ... - (variable_sema ,(+ (term number_n) 1)) - (variable_after v_after) ...) - (threads - e_before ... - (in-hole c (void)) - e_after ...))) - - (--> ((name store any) - (semas - (variable_before v_before) ... - (variable_sema none) - (variable_after v_after) ...) - (threads - e_before ... - (in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema))) - e_after ...)) - (store - (semas - (variable_before v_before) ... - (variable_sema 1) - (variable_after v_after) ...) - (threads - e_before ... - (in-hole c (void)) - e_after ...))))) - - (stepper lang - reductions - `((store (y (list))) - (semas) - (threads (set! y (cons 1 y)) - (set! y (cons 2 y))))) - - (stepper lang - reductions - `((store (y (list))) - (semas (x 1)) - (threads (begin (semaphore-wait (semaphore x)) - (set! y (cons 1 y)) - (semaphore-post (semaphore x))) - (begin (semaphore-wait (semaphore x)) - (set! y (cons 2 y)) - (semaphore-post (semaphore x))))))) + (threads + e_before ... + (in-hole c (void)) + e_after ...))) + + (--> ((name store any) + (semas + (variable_before v_before) ... + (variable_sema none) + (variable_after v_after) ...) + (threads + e_before ... + (in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema))) + e_after ...)) + (store + (semas + (variable_before v_before) ... + (variable_sema 1) + (variable_after v_after) ...) + (threads + e_before ... + (in-hole c (void)) + e_after ...))))) + +(stepper lang + reductions + `((store (y (list))) + (semas) + (threads (set! y (cons 1 y)) + (set! y (cons 2 y))))) + +(stepper lang + reductions + `((store (y (list))) + (semas (x 1)) + (threads (begin (semaphore-wait (semaphore x)) + (set! y (cons 1 y)) + (semaphore-post (semaphore x))) + (begin (semaphore-wait (semaphore x)) + (set! y (cons 2 y)) + (semaphore-post (semaphore x)))))) \ No newline at end of file diff --git a/collects/redex/examples/subject-reduction.ss b/collects/redex/examples/subject-reduction.ss index feaddcec6c..8d608237cf 100644 --- a/collects/redex/examples/subject-reduction.ss +++ b/collects/redex/examples/subject-reduction.ss @@ -1,92 +1,71 @@ -(module subject-reduction mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/gui) - (planet robby/redex:5/subst) - (lib "plt-match.ss")) - - (reduction-steps-cutoff 10) - - (define-language lang - (e (e e) - (abort e) - x - v) - (x (variable-except lambda call/cc abort)) - (c (v c) - (c e) - hole) - (v call/cc - number - (lambda (x t) e)) - (t num - (t -> t))) - - (define reductions - (reduction-relation - lang - (--> (in-hole c_1 (call/cc v_arg)) - ,(term-let ([v (variable-not-in (term c_1) 'x)]) - (term - (in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v))))))) - call/cc) - (--> (in-hole c (abort e_1)) - e_1 - abort) - - ;; this rules calls subst with the wrong arguments, which is caught by the example below. - (--> (in-hole c_1 ((lambda (x_format t_1) e_body) v_actual)) - (in-hole c_1 ,(lc-subst (term x_format) (term e_body) (term v_actual))) - βv))) - - (define lc-subst - (plt-subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x ,t) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars) ,t) ,body))) - (subterm (list x) b)] - [`(call/cc ,v) - (all-vars '()) - (build (lambda (vars arg) `(call/cc ,arg))) - (subterm '() v)] - [`(,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(,f ,x))) - (subterm '() f) - (subterm '() x)])) - - (define (type-check term) - (let/ec k - (let loop ([term term] - [env '()]) - (match term - [(? symbol?) - (let ([l (assoc term env)]) - (if l - (cdr l) - (k #f)))] - [(? number?) 'num] - [`(lambda (,x ,t) ,b) - (let ([body (loop b (cons (cons x t) env))]) - `(,t -> ,body))] - [`(,e1 ,e2) - (let ([t1 (loop e1 env)] - [t2 (loop e2 env)]) - (match t1 - [`(,td -> ,tr) - (if (equal? td t2) - tr - (k #f))] - [else (k #f)]))])))) - - (define (pred term1) - (let ([t1 (type-check term1)]) - (lambda (term2) - (and t1 - (equal? (type-check term2) t1))))) - - (define (show term) - (traces/pred lang reductions (list term) (pred term))) - - (show '((lambda (x (num -> num)) 1) ((lambda (x (num -> num)) x) (lambda (x num) x))))) +#lang scheme +(require redex) + +(reduction-steps-cutoff 10) + +(define-language lang + (e (e e) + (abort e) + x + v) + (x (variable-except lambda call/cc abort)) + (c (v c) + (c e) + hole) + (v call/cc + number + (lambda (x t) e)) + (t num + (t -> t))) + +(define reductions + (reduction-relation + lang + (--> (in-hole c_1 (call/cc v_arg)) + ,(term-let ([v (variable-not-in (term c_1) 'x)]) + (term + (in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v))))))) + call/cc) + (--> (in-hole c (abort e_1)) + e_1 + abort) + + ;; this rules calls subst with the wrong arguments, which is caught by the example below. + (--> (in-hole c_1 ((lambda (x_format t_1) e_body) v_actual)) + (in-hole c_1 (subst x_format v_actual e_body)) + βv))) + +(define (type-check term) + (let/ec k + (let loop ([term term] + [env '()]) + (match term + [(? symbol?) + (let ([l (assoc term env)]) + (if l + (cdr l) + (k #f)))] + [(? number?) 'num] + [`(lambda (,x ,t) ,b) + (let ([body (loop b (cons (cons x t) env))]) + `(,t -> ,body))] + [`(,e1 ,e2) + (let ([t1 (loop e1 env)] + [t2 (loop e2 env)]) + (match t1 + [`(,td -> ,tr) + (if (equal? td t2) + tr + (k #f))] + [else (k #f)]))])))) + +(define (pred term1) + (let ([t1 (type-check term1)]) + (lambda (term2) + (and t1 + (equal? (type-check term2) t1))))) + +(define (show term) + (traces reductions term #:pred (pred term))) + +(show '((lambda (x (num -> num)) 1) ((lambda (x (num -> num)) x) (lambda (x num) x)))) \ No newline at end of file diff --git a/collects/redex/examples/subst.ss b/collects/redex/examples/subst.ss new file mode 100644 index 0000000000..24a336982a --- /dev/null +++ b/collects/redex/examples/subst.ss @@ -0,0 +1,74 @@ +#lang scheme +(require redex) +(provide subst subst-n) + +(define-language subst-lang + (x variable)) + +(define-metafunction subst-n + subst-lang + [((x_1 any_1) (x_2 any_2) ... any_3) + (subst (x_1 any_1 (subst-n ((x_2 any_2) ... any_3))))] + [(any_3) any_3]) + +(define-metafunction subst + subst-lang + ;; 1. x_1 bound, so don't continue in λ body + [(x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2)) + (λ (x_2 ... x_1 x_3 ...) any_2) + (side-condition (not (member (term x_1) (term (x_2 ...)))))] + ;; 2. general purpose capture avoiding case + [(x_1 any_1 (λ (x_2 ...) any_2)) + ,(term-let ([(x_new ...) + (variables-not-in (term (x_1 any_1 any_2)) + (term (x_2 ...)))]) + (term + (λ (x_new ...) + (subst (x_1 any_1 (subst-vars ((x_2 x_new) ... any_2)))))))] + ;; 3. replace x_1 with e_1 + [(x_1 any_1 x_1) any_1] + ;; 4. x_1 and x_2 are different, so don't replace + [(x_1 any_1 x_2) x_2] + ;; the last two cases cover all other expression forms + [(x_1 any_1 (any_2 ...)) + ((subst (x_1 any_1 any_2)) ...)] + [(x_1 any_1 any_2) any_2]) + +(define-metafunction subst-vars + subst-lang + [((x_1 any_1) x_1) any_1] + [((x_1 any_1) (any_2 ...)) ((subst-vars ((x_1 any_1) any_2)) ...)] + [((x_1 any_1) any_2) any_2] + [((x_1 any_1) (x_2 any_2) ... any_3) + (subst-vars ((x_1 any_1) (subst-vars ((x_2 any_2) ... any_3))))] + [(any) any]) + +(begin + (test-equal (term (subst (x y x))) (term y)) + (test-equal (term (subst (x y z))) (term z)) + (test-equal (term (subst (x y (x (y z))))) (term (y (y z)))) + (test-equal (term (subst (x y ((λ (x) x) ((λ (y1) y1) (λ (x) z)))))) + (term ((λ (x) x) ((λ (y2) y2) (λ (x) z))))) + (test-equal (term (subst (x y (if0 (+ 1 x) x x)))) + (term (if0 (+ 1 y) y y))) + (test-equal (term (subst (x (λ (z) y) (λ (y) x)))) + (term (λ (y1) (λ (z) y)))) + (test-equal (term (subst (x 1 (λ (y) x)))) + (term (λ (y) 1))) + (test-equal (term (subst (x y (λ (y) x)))) + (term (λ (y1) y))) + (test-equal (term (subst (x (λ (y) y) (λ (z) (z2 z))))) + (term (λ (z1) (z2 z1)))) + (test-equal (term (subst (x (λ (z) z) (λ (z) (z1 z))))) + (term (λ (z2) (z1 z2)))) + (test-equal (term (subst (x z (λ (z) (z1 z))))) + (term (λ (z2) (z1 z2)))) + (test-equal (term (subst (x3 5 (λ (x2) x2)))) + (term (λ (x1) x1))) + (test-equal (term (subst (z * (λ (z x) 1)))) + (term (λ (z x) 1))) + (test-equal (term (subst (q (λ (x) z) (λ (z x) q)))) + (term (λ (z1 x1) (λ (x) z)))) + (test-equal (term (subst (x 1 (λ (x x) x)))) + (term (λ (x x) x))) + (test-results)) \ No newline at end of file diff --git a/collects/redex/examples/threads.ss b/collects/redex/examples/threads.ss index cd95315255..57b318298d 100644 --- a/collects/redex/examples/threads.ss +++ b/collects/redex/examples/threads.ss @@ -1,117 +1,86 @@ -(module threads mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/subst) - (planet robby/redex:5/gui) - (lib "plt-match.ss")) - - (reduction-steps-cutoff 100) - - (define-language threads - (p ((store (x v) ...) (threads e ...))) - (e (set! x e) - (let ((x e)) e) - (e e) - x - v - (+ e e)) - (v (lambda (x) e) - number) - (x variable) - (pc ((store (x v) ...) tc)) - (tc (threads e ... ec e ...)) - (ec (ec e) (v ec) (set! variable ec) (let ((x ec)) e) (+ ec e) (+ v ec) hole)) - - (define reductions - (reduction-relation - threads - (--> (in-hole pc_1 (+ number_1 number_2)) - (in-hole pc_1 ,(+ (term number_1) (term number_2))) - sum) - - (--> ((store - (name befores (x v)) ... - (x_i v_i) - (name afters (x v)) ...) - (in-hole tc_1 x_i)) - ((store - befores ... - (x_i v_i) - afters ...) - (in-hole tc_1 v_i)) - deref) - - (--> ((store (x_1 v_1) ... (x_i v) (x_2 v_2) ...) - (in-hole tc_1 (set! x_i v_new))) - ((store (x_1 v_1) ... (x_i v_new) (x_2 v_2) ...) - (in-hole tc_1 v_new)) - set!) - - (--> (in-hole pc_1 ((lambda (x_1) e_1) v_1)) - (in-hole pc_1 ,(substitute (term x_1) (term v_1) (term e_1))) - app) - - (--> ((store (name the-store any) ...) - (in-hole tc_1 (let ((x_1 v_1)) e_1))) - (term-let ((new-x (variable-not-in (term (the-store ...)) (term x_1)))) - (term - ((store the-store ... (new-x v_1)) - (in-hole tc_1 ,(substitute (term x_1) (term new-x) (term e_1)))))) - let))) - - (define substitute - (plt-subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list x) b)] - [`(set! ,x ,e) - (all-vars '()) - (build (lambda (vars name body) `(set! ,name ,body))) - (subterm '() x) - (subterm '() e)] - [`(let ((,x ,e1)) ,e2) - (all-vars (list x)) - (build (lambda (vars letval body) `(let ((,(car vars) ,letval)) ,body))) - (subterm '() e1) - (subterm (list x) e2)] - [`(+ ,e1 ,e2) - (all-vars '()) - (build (lambda (vars e1 e2) `(+ ,e1 ,e2))) - (subterm '() e1) - (subterm '() e2)] - [`(,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(,f ,x))) - (subterm '() f) - (subterm '() x)])) - - (define (run es) (traces threads reductions `((store) (threads ,@es)))) - (provide run) - - (define (count x) - (match x - [`(set! ,x ,e) (+ 1 (count e))] - [(? symbol?) 1] - [(? number?) 0] - [`(+ ,e1 ,e2) (+ 1 (count e1) (count e2))])) - - ;; use a pretty-printer that just summaizes the terms, showing the depth of each thread. - (traces threads reductions - '((store (x 1)) - (threads - (set! x (+ x -1)) - (set! x (+ x 1)))) - - (lambda (exp) - (match exp - [`((store (x ,x)) (threads ,t1 ,t2)) - (format "~a ~a ~a" x (count t1) (count t2))]))) +#lang scheme +(require redex) - (parameterize ([initial-char-width 16]) - (stepper threads reductions '((store) (threads - (+ 1 1) - (+ 1 1) - (+ 1 1))))) - ) +(reduction-steps-cutoff 100) + +(define-language threads + (p ((store (x v) ...) (threads e ...))) + (e (set! x e) + (let ((x e)) e) + (e e) + x + v + (+ e e)) + (v (lambda (x) e) + number) + (x variable) + (pc ((store (x v) ...) tc)) + (tc (threads e ... ec e ...)) + (ec (ec e) (v ec) (set! variable ec) (let ((x ec)) e) (+ ec e) (+ v ec) hole)) + +(define reductions + (reduction-relation + threads + (--> (in-hole pc_1 (+ number_1 number_2)) + (in-hole pc_1 ,(+ (term number_1) (term number_2))) + sum) + + (--> ((store + (name befores (x v)) ... + (x_i v_i) + (name afters (x v)) ...) + (in-hole tc_1 x_i)) + ((store + befores ... + (x_i v_i) + afters ...) + (in-hole tc_1 v_i)) + deref) + + (--> ((store (x_1 v_1) ... (x_i v) (x_2 v_2) ...) + (in-hole tc_1 (set! x_i v_new))) + ((store (x_1 v_1) ... (x_i v_new) (x_2 v_2) ...) + (in-hole tc_1 v_new)) + set!) + + (--> (in-hole pc_1 ((lambda (x_1) e_1) v_1)) + (in-hole pc_1 ,(substitute (term x_1) (term v_1) (term e_1))) + app) + + (--> ((store (name the-store any) ...) + (in-hole tc_1 (let ((x_1 v_1)) e_1))) + (term-let ((new-x (variable-not-in (term (the-store ...)) (term x_1)))) + (term + ((store the-store ... (new-x v_1)) + (in-hole tc_1 ,(substitute (term x_1) (term new-x) (term e_1)))))) + let))) + +(define (substitute . x) (error 'substitute "~s" x)) + +(define (run es) (traces threads reductions `((store) (threads ,@es)))) +(provide run) + +(define (count x) + (match x + [`(set! ,x ,e) (+ 1 (count e))] + [(? symbol?) 1] + [(? number?) 0] + [`(+ ,e1 ,e2) (+ 1 (count e1) (count e2))])) + +;; use a pretty-printer that just summaizes the terms, showing the depth of each thread. +(traces reductions + '((store (x 1)) + (threads + (set! x (+ x -1)) + (set! x (+ x 1)))) + + (lambda (exp) + (match exp + [`((store (x ,x)) (threads ,t1 ,t2)) + (format "~a ~a ~a" x (count t1) (count t2))]))) + +(parameterize ([initial-char-width 16]) + (stepper threads reductions '((store) (threads + (+ 1 1) + (+ 1 1) + (+ 1 1))))) diff --git a/collects/redex/examples/types.ss b/collects/redex/examples/types.ss index 3f3e8a7753..7bd1d87392 100644 --- a/collects/redex/examples/types.ss +++ b/collects/redex/examples/types.ss @@ -1,87 +1,69 @@ -(module types mzscheme - (require (planet robby/redex:5/reduction-semantics) - (planet robby/redex:5/subst) - (planet robby/redex:5/gui)) - - (reduction-steps-cutoff 10) - - (define-language lang - (e (e e) - x - number - (lambda (x t) e) - (if e e e) - (= e e) - (-> e e) - num - bool) - (c (t c) - (c e) - (-> t c) - (-> c e) - (= t c) - (= c e) - (if c e e) - (if t c e) - (if t t c) - hole) - (x (variable-except lambda -> if =)) - (t num bool (-> t t))) - - (define reductions - (reduction-relation - lang - (r--> number num) - - (r--> (lambda (x_1 t_1) e_body) - (-> t_1 ,(lc-subst (term x_1) - (term t_1) - (term e_body)))) - - (r--> ((-> t_1 t_2) t_1) t_2) - - (e--> (side-condition ((-> t_1 t) t_2) - (not (equal? (term t_1) (term t_2)))) - ,(format "app: domain error ~s and ~s" (term t_1) (term t_2))) - - (e--> (num t_1) - ,(format "app: non function error ~s" (term t_1))) - - (r--> (if bool t_1 t_1) t_1) - (e--> (side-condition (if bool t_1 t_2) - (not (equal? (term t_1) (term t_2)))) - ,(format "if: then and else clause mismatch ~s and ~s" (term t_1) (term t_2))) - (e--> (side-condition (if t_1 t t) - (not (equal? (term t_1) 'bool))) - ,(format "if: test not boolean ~s" (term t_1))) - - (r--> (= num num) bool) - (e--> (side-condition (= t_1 t_2) - (or (not (equal? (term t_1) 'num)) - (not (equal? (term t_2) 'num)))) - ,(format "=: not comparing numbers ~s and ~s" (term t_1) (term t_2))) - - where - - [(r--> a b) (--> (in-hole c_1 a) (in-hole c_1 b))] - [(e--> a b) (--> (in-hole c a) b)])) - - (define lc-subst - (subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x ,t) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars) ,t) ,body))) - (subterm (list x) b)] - [`(,f ,@(xs ...)) - (all-vars '()) - (build (lambda (vars f . xs) `(,f ,@xs))) - (subterm '() f) - (subterms '() xs)])) - - (traces lang reductions - '((lambda (x num) (lambda (y num) (if (= x y) 0 x))) 1)) - (traces lang reductions - '((lambda (x num) (lambda (y num) (if (= x y) 0 (lambda (x num) x)))) 1)) - ) +#lang scheme +(require redex + "subst.ss") + +(reduction-steps-cutoff 10) + +(define-language lang + (e (e e) + x + number + (lambda (x t) e) + (if e e e) + (= e e) + (-> e e) + num + bool) + (c (t c) + (c e) + (-> t c) + (-> c e) + (= t c) + (= c e) + (if c e e) + (if t c e) + (if t t c) + hole) + (x (variable-except lambda -> if =)) + (t num bool (-> t t))) + +(define reductions + (reduction-relation + lang + (r--> number num) + + (r--> (lambda (x_1 t_1) e_body) + (-> t_1 (subst (x_1 t_1 e_body)))) + + (r--> ((-> t_1 t_2) t_1) t_2) + + (e--> (side-condition ((-> t_1 t) t_2) + (not (equal? (term t_1) (term t_2)))) + ,(format "app: domain error ~s and ~s" (term t_1) (term t_2))) + + (e--> (num t_1) + ,(format "app: non function error ~s" (term t_1))) + + (r--> (if bool t_1 t_1) t_1) + (e--> (side-condition (if bool t_1 t_2) + (not (equal? (term t_1) (term t_2)))) + ,(format "if: then and else clause mismatch ~s and ~s" (term t_1) (term t_2))) + (e--> (side-condition (if t_1 t t) + (not (equal? (term t_1) 'bool))) + ,(format "if: test not boolean ~s" (term t_1))) + + (r--> (= num num) bool) + (e--> (side-condition (= t_1 t_2) + (or (not (equal? (term t_1) 'num)) + (not (equal? (term t_2) 'num)))) + ,(format "=: not comparing numbers ~s and ~s" (term t_1) (term t_2))) + + with + + [(--> (in-hole c_1 a) (in-hole c_1 b)) (r--> a b)] + [(--> (in-hole c a) b) (e--> a b)])) + +(traces reductions + '((lambda (x num) (lambda (y num) (if (= x y) 0 x))) 1)) +(traces reductions + '((lambda (x num) (lambda (y num) (if (= x y) 0 (lambda (x num) x)))) 1)) diff --git a/collects/redex/private/color-test.ss b/collects/redex/private/color-test.ss index 3d5e26a365..181471a5fc 100644 --- a/collects/redex/private/color-test.ss +++ b/collects/redex/private/color-test.ss @@ -8,64 +8,62 @@ In the other window, you expect to see the currently unreducted terms in green a |# -(module color-test mzscheme - (require "../reduction-semantics.ss" - "../gui.ss" - (lib "mred.ss" "mred") - (lib "class.ss")) +#lang scheme/gui + +(require "../reduction-semantics.ss" + "../gui.ss") + +(reduction-steps-cutoff 1) + +(let () - (reduction-steps-cutoff 1) + (define (get-range term-node) + (let loop ([node term-node]) + (let ([parents (term-node-parents node)]) + (cond + [(null? parents) (list node)] + [else (cons node (loop (car parents)))])))) - (let () - - (define (get-range term-node) - (let loop ([node term-node]) - (let ([parents (term-node-parents node)]) - (cond - [(null? parents) (list node)] - [else (cons node (loop (car parents)))])))) - - (define (color-range-pred sexp term-node) - (let* ([parents (get-range term-node)] - [max-val (car (term-node-expr (car parents)))]) - (for-each - (λ (node) - (let ([val (car (term-node-expr node))]) - (term-node-set-color! node - (make-object color% - (floor (- 255 (* val (/ 255 max-val)))) - 0 - (floor (* val (/ 255 max-val))))))) - parents))) - - (define-language empty-language) - - (traces/pred empty-language - (reduction-relation - empty-language - (--> (number_1 word) - (,(+ (term number_1) 1) word) - inc)) - (list '(1 word)) - color-range-pred)) + (define (color-range-pred sexp term-node) + (let* ([parents (get-range term-node)] + [max-val (car (term-node-expr (car parents)))]) + (for-each + (λ (node) + (let ([val (car (term-node-expr node))]) + (term-node-set-color! node + (make-object color% + (floor (- 255 (* val (/ 255 max-val)))) + 0 + (floor (* val (/ 255 max-val))))))) + parents))) - (let () - (define-language empty-language) - - (define (last-color-pred sexp term-node) - (term-node-set-color! term-node - (if (null? (term-node-children term-node)) - "green" - "white"))) - - (traces/pred empty-language - (reduction-relation - empty-language - (--> (number_1 word) - (,(+ (term number_1) 1) word) - inc) - (--> (number_1 word) - (,(* (term number_1) 2) word) - dup)) - (list '(1 word)) - last-color-pred))) + (define-language empty-language) + + (traces + (reduction-relation + empty-language + (--> (number_1 word) + (,(+ (term number_1) 1) word) + inc)) + '(1 word) + #:pred color-range-pred)) + +(let () + (define-language empty-language) + + (define (last-color-pred sexp term-node) + (term-node-set-color! term-node + (if (null? (term-node-children term-node)) + "green" + "white"))) + + (traces (reduction-relation + empty-language + (--> (number_1 word) + (,(+ (term number_1) 1) word) + inc) + (--> (number_1 word) + (,(* (term number_1) 2) word) + dup)) + '(1 word) + #:pred last-color-pred)) \ No newline at end of file diff --git a/collects/redex/private/schemeunit-test.ss b/collects/redex/private/schemeunit-test.ss deleted file mode 100644 index b8769c8333..0000000000 --- a/collects/redex/private/schemeunit-test.ss +++ /dev/null @@ -1,60 +0,0 @@ -(module schemeunit-test mzscheme - (require "../schemeunit.ss" - (all-except "../reduction-semantics.ss" check) - (planet "text-ui.ss" ("schematics" "schemeunit.plt" 2)) - (planet "test.ss" ("schematics" "schemeunit.plt" 2))) - - (define-language lang - (e number (+ e e) (choose e e)) - (ec hole (+ e ec) (+ ec e)) - (v number true false)) - - (define reductions - (reduction-relation - lang - (--> (in-hole ec_1 (+ number_1 number_2)) - (in-hole ec_1 ,(+ (term number_1) (term number_2)))) - (--> (in-hole ec_1 (choose e_1 e_2)) - (in-hole ec_1 e_1)) - (--> (in-hole ec_1 (choose e_1 e_2)) - (in-hole ec_1 e_2)))) - - (define tests-passed 0) - - (define (try-it check in out key/vals) - (let ([sp (open-output-string)]) - (parameterize ([current-output-port sp]) - (test/text-ui (test-case "X" (check reductions in out)))) - (let ([s (get-output-string sp)]) - (for-each - (λ (key/val) - (let* ([key (car key/val)] - [val (cadr key/val)] - [m (regexp-match (format "\n~a: ([^\n]*)\n" key) s)]) - (unless m - (error 'try-it "didn't find key ~s in ~s" key s)) - (unless (if (regexp? val) - (regexp-match val (cadr m)) - (equal? val (cadr m))) - (error 'try-in "didn't match key ~s, expected ~s got ~s" key val (cadr m))))) - key/vals))) - (set! tests-passed (+ tests-passed 1))) - - (try-it check-reduces - '(choose 1 2) - 1 - '((multiple-results "(2 1)"))) - - (try-it check-reduces - '(+ 1 2) - 1 - '((expected "1") - (actual "3"))) - - (try-it check-reduces/multiple - '(+ (choose 3 4) 1) - '(4 6) - '((expecteds "(4 6)") - (actuals #rx"[(][45] [54][)]"))) - - (printf "schemeunit-tests: all ~a tests passed.\n" tests-passed)) diff --git a/collects/redex/private/subst-test.ss b/collects/redex/private/subst-test.ss deleted file mode 100644 index ff80736b3f..0000000000 --- a/collects/redex/private/subst-test.ss +++ /dev/null @@ -1,125 +0,0 @@ -(module subst-test mzscheme - (require "../subst.ss" - (lib "match.ss")) - - (define (lc-subst1 var val exp) (subst/proc var val exp lc-separate)) - (define (lc-free-vars exp) (free-vars/memoize (make-hash-table) exp lc-separate)) - (define (lc-rename old-name new-name exp) (alpha-rename old-name new-name exp lc-separate)) - - (define lc-subst2 - (subst - [`(lambda ,vars ,body) - (all-vars vars) - (build (lambda (vars body) `(lambda ,vars ,body))) - (subterm vars body)] - [`(let (,l-var ,exp) ,body) - (all-vars (list l-var)) - (build (lambda (l-vars exp body) `(let (,@l-vars ,exp) ,body))) - (subterm '() exp) - (subterm (list l-var) body)] - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(,fun ,@(args ...)) - (all-vars '()) - (build (lambda (vars fun . args) `(,fun ,@args))) - (subterm '() fun) - (subterms '() args)])) - - (define (lc-separate exp constant variable combine sub-piece) - (match exp - [`(lambda ,vars ,body) - (combine (lambda (vars body) `(lambda ,vars ,body)) - vars - (sub-piece vars body))] - [`(let (,l-var ,exp) ,body) - (combine (lambda (l-vars exp body) `(let (,(car l-vars) ,exp) ,body)) - (list l-var) - (sub-piece '() exp) - (sub-piece (list l-var) body))] - [(? symbol?) (variable (lambda (x) x) exp)] - [(? number?) (constant exp)] - [`(,fun ,@(args ...)) - (apply - combine - (lambda (variables fun . args) `(,fun ,@args)) - '() - (append - (list (sub-piece '() fun)) - (map (lambda (x) (sub-piece '() x)) args)))])) - - (define test-cases 0) - (define failed-tests? #f) - - (define-syntax (test stx) - (syntax-case stx () - [(_ test-exp expected) - (syntax (test test-exp expected equal?))] - [(_ test-exp expected same?) - (syntax - (let ([actual test-exp] - [expected-v expected]) - ;(printf "testing: ~s\n" (syntax-object->datum #'test-exp)) - (set! test-cases (+ test-cases 1)) - (unless (same? actual expected-v) - (set! failed-tests? #t) - (printf " test: ~s\n expected: ~s\n got: ~s\n" - (syntax-object->datum #'test-exp) - expected-v - actual))))])) - - (define (set-equal? xs ys) - (and (andmap (lambda (x) (memq x ys)) xs) - (andmap (lambda (y) (memq y xs)) ys))) - - (define (lc-tests) - (tests lc-free-vars lc-subst1 lc-rename) - (tests #f lc-subst2 #f)) - - (define (tests free-vars subst rename) - (when free-vars - (test (free-vars 'x) '(x) set-equal?) - (test (free-vars '(lambda (x) x)) '() set-equal?) - (test (free-vars '(lambda (x) y)) '(y) set-equal?) - (test (free-vars '(let (x 1) x)) '() set-equal?) - (test (free-vars '(let (x 1) y)) '(y) set-equal?) - (test (free-vars '(let (x x) y)) '(y x) set-equal?) - (test (free-vars '(let (x 1) (y y))) '(y) set-equal?) - (test (free-vars '(lambda (y) (y y))) '() set-equal?)) - - (when rename - (test (rename 'x 'y 'x) 'x) - (test (rename 'x 'y '(lambda (x) x)) '(lambda (y) y))) - - (test (subst 'x 1 'x) 1) - (test (subst 'x 1 'y) 'y) - (test (subst 'x 1 '(lambda (x) x)) '(lambda (x) x)) - (test (subst 'x 1 '(lambda (y) x)) '(lambda (y) 1)) - (test (subst 'x 'y '(lambda (y) x)) '(lambda (y@) y)) - (test (subst 'x 'y '(lambda (y) (x y))) '(lambda (y@) (y y@))) - (test (subst 'x 'y '(let (x 1) 1)) '(let (x 1) 1)) - (test (subst 'x 'y '(let (x 1) x)) '(let (x 1) x)) - (test (subst 'x 'y '(let (x 1) y)) '(let (x 1) y)) - (test (subst 'x 'y '(let (y 1) (x y))) '(let (y@ 1) (y y@))) - (test (subst 'q '(lambda (x) y) '(lambda (y) y)) '(lambda (y) y)) - (test (subst 'q '(lambda (x) y) '(let ([y q]) y)) '(let ([y (lambda (x) y)]) y)) - (test (subst 'p '1 '(let (t 2) ((p t) t))) - '(let (t 2) ((1 t) t))) - (test (subst 'p '(lambda (s) s) - '(let (t (lambda (s) s)) ((p t) t))) - '(let (t (lambda (s) s)) (((lambda (s) s) t) t))) - (test (subst 'p - '(lambda (s) (s s)) - '(let (t (lambda (s) s)) - p)) - '(let (t (lambda (s) s)) - (lambda (s) (s s)))) - - (test (subst 's - '(lambda (z) (s z)) - '(lambda (s) (lambda (z) (s z)))) - '(lambda (s) (lambda (z) (s z)))) - - (test (subst 's - '(lambda (s) (lambda (z) (s z))) - '(lambda (z) (s z))) - '(lambda (z) ((lambda (s) (lambda (z) (s z))) z)))))