#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)