#lang racket (require redex) (define-language Roo (p (begin d ... e)) (d (define z e)) (c (class object% (init-field i) m ... (super-make-object))) (m (define/public (x y ...) e)) (e c (make-object x e) (send e x e ...) x this number (if0 e e e) (+ e ...)) (a (begin d ... v)) (v (make-object x v) number) (P (begin d ... E)) (E (make-object x E) (send E x e ...) (send v x v ... E e ...) (if0 E e e) (+ v ... E e ...) hole) ((i x y z) variable-not-otherwise-mentioned)) (define send-rule (reduction-relation Roo (--> (begin d_1 ... (define z (class object% (init-field i) m_1 ... (define/public (x y ...) e) m_2 ... (super-make-object))) d_2 ... (in-hole E (send (make-object z v_i) x v_y ...))) (begin d_1 ... (define z (class object% (init-field i) m_1 ... (define/public (x y ...) e) m_2 ... (super-make-object))) d_2 ... (in-hole E (substs-e e (y v_y) ... (i v_i) (this (make-object z v_i))))) "send"))) (define num-rules (reduction-relation Roo (--> (in-hole P (+ number ...)) (in-hole P (Σ number ...)) "+") (--> (in-hole P (if0 0 e_1 e_2)) (in-hole P e_1) "if0t") (--> (in-hole P (if0 number e_1 e_2)) (in-hole P e_2) (side-condition (term (nonzero number))) "if0f"))) (define red (union-reduction-relations send-rule num-rules)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; substitution ;; (define-metafunction Roo subst-e : e variable any -> any [(subst-e (class e (init-field i_1) d ... (super-new [i_2 i_3] ...)) x any) (class (subst-e e variable any) (init-field i_1) (subst-e d variable any) ... (super-new [i_2 i_3] ...))] [(subst-e object% variable any) object%] [(subst-e (new e_1 [i e_2] ...) variable any) (new (subst-e e_1 variable any) [i (subst-e e_2 variable any)] ...)] [(subst-e (send e_1 x e_2 ...) variable any) (send (subst-e e_1 variable any) x (subst-e e_2 variable any) ...)] [(subst-e x variable any) ,(if (equal? (term x) (term variable)) (term any) (term x))] [(subst-e number variable any) number] [(subst-e (+ e ...) variable any) (+ (subst-e e variable any) ...)] [(subst-e (if0 e_1 e_2 e_3) variable any) (if0 (subst-e e_1 variable any) (subst-e e_2 variable any) (subst-e e_3 variable any))] [(subst-e this this any) any] [(subst-e this variable any) this]) (define-metafunction Roo substs-e : e (variable any) ... -> any [(substs-e e) e] [(substs-e e (variable_1 any_1) (variable_2 any_2) ...) (substs-e (subst-e e variable_1 any_1) (variable_2 any_2) ...)]) (define-metafunction Roo nonzero : number -> any [(nonzero 0) #f] [(nonzero number) #t]) (define-metafunction Roo Σ : number ... -> number [(Σ number ...) ,(apply + (term (number ...)))]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; a few unit tests ;; (test-->> red (term (begin (+ 1 2 3))) (term (begin 6))) (test-->> red (term (begin (if0 (if0 0 1 2) 3 (if0 4 5 6)))) (term (begin 6))) (test-->> red (term (begin (define x (class object% (init-field i) (define/public (m) 1) (super-make-object))) (send (make-object x 0) m))) (term (begin (define x (class object% (init-field i) (define/public (m) 1) (super-make-object))) 1))) (test-->> red (term (begin (define x (class object% (init-field i) (define/public (m x) x) (super-make-object))) (send (make-object x 0) m 1))) (term (begin (define x (class object% (init-field i) (define/public (m x) x) (super-make-object))) 1))) (test-->> red (term (begin (define x (class object% (init-field y) (define/public (m x) (+ x y)) (super-make-object))) (send (make-object x 2) m 1))) (term (begin (define x (class object% (init-field y) (define/public (m x) (+ x y)) (super-make-object))) 3))) (test-->> red (term (begin (define x (class object% (init-field y) (define/public (m x) (if0 x y (send this m (+ x -1)))) (super-make-object))) (send (make-object x 11) m 10))) (term (begin (define x (class object% (init-field y) (define/public (m x) (if0 x y (send this m (+ x -1)))) (super-make-object))) 11))) (test-results) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; eval-expr ;; (require racket/list racket/class) (define ns (make-base-empty-namespace)) (namespace-attach-module (current-namespace) 'racket/class ns) (parameterize ([current-namespace ns]) (eval (quote-syntax (module minimal-stuff racket/base (require racket/class (for-syntax racket/base) (only-in lang/htdp-intermediate local)) (define-syntax-rule (if0 a b c) (if (zero? a) b c)) (define-syntax-rule (begin d ... body) (local [d ...] body)) (provide begin if0 make-object object% define class define/public super-make-object init-field send this + #%app #%datum)))) (namespace-require ''minimal-stuff)) (define (eval-expr e) (with-handlers ((not-syntax-error? (λ (x) 'error))) (let ([result (eval e ns)]) (cond [(number? result) result] [(class? result) 'class] [(object? result) 'object])))) (define (not-syntax-error? x) (and (exn:fail? x) (not (exn:fail:syntax? x)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; reduce-expr ;; (define a? (redex-match Roo a)) (define (reduce-expr expr) (define results (apply-reduction-relation* red expr)) (unless (= 1 (length results)) (error 'reduce-expr "got multiple results for ~s" expr)) (define result (last (car results))) (cond [(not (a? (car results))) 'error] [(number? result) result] [(eq? result 'object%) 'class] [(eq? (car result) 'class) 'class] [(eq? (car result) 'make-object) 'object])) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; redex-check call ;; (redex-check Roo p (with-handlers ((exn:fail:syntax? (λ (x) #t))) (equal? (eval-expr (term p)) (reduce-expr (term p)))) #:attempts 1000)