(module siek-taha mzscheme
  (require (planet "" ("robby" "redex.plt" 3 9))
           (planet "" ("cobbe" "environment.plt" 3 0))
           (lib "")

  (define (strip-box term)
    (match term
      [`(cast ,t ,v) v]
      [_ term]))

  (define (coerce/st src dst) dst)

  ;; ===========================================================================
  ;; ===========================================================================

  (define reductions/st
     (core-reductions language/st)
     (reduction-relation language/st
       [==> (cast t_cast v_boxed)
            ,(strip-box (term v_boxed))
            (side-condition (and (ground-type? (term t_cast))
                                 (compatible? (type-of (strip-box (term v_boxed)) (make-empty-env))
                                              (term t_cast))))
       [==> (cast (t_dom -> t_rng) v_f)
            ,(let ([f (strip-box (term v_f))])
               (let ([type-of-f (type-of f (make-empty-env))])
                 (let ([dom (function-type-domain type-of-f)]
                       [rng (function-type-range type-of-f)])
                   (term-let ([t_f f]
                              [t_domcast (function-type-domain type-of-f)])
                     (term (lambda (z : t_dom)
                             (cast t_rng (t_f (cast t_domcast z)))))))))
            (side-condition (and (function-type? (type-of (strip-box (term v_f)) (make-empty-env)))
                                 (compatible? (type-of (strip-box (term v_f)) (make-empty-env))
                                              (term (t_dom -> t_rng)))))
            (fresh z)
       ;; The ECstU rule is intended to removed nested casts when they are wrapped
       ;; by a cast to dynamic. However, at least as stated, the rule only removes
       ;; nested casts to *dynamic*, because the definition of a value v is either
       ;; s or <?> s. Thus the rule amounts to removing nested casts to dynamic on
       ;; unboxed values.
       [==> (cast dynamic (cast dynamic s_boxed))
            ;; TODO: (cast dynamic s_boxed)
            ,`(cast dynamic ,(term s_boxed))
       [(==> a b) (--> (in-hole E_1 a) (in-hole E_1 b))])))

  (define st (make-semantics language/st reductions/st coerce/st (test-match language/st v)))

  (provide (all-defined)))