siek-taha.ss
(module siek-taha mzscheme
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 3 9))
           (planet "environment.ss" ("cobbe" "environment.plt" 3 0))
           (lib "match.ss")
           "static-semantics.ss"
           "core-language.ss"
           "front-end.ss")

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

  (define (coerce/st src dst) dst)

  ;; ===========================================================================
  ;; REDUCTIONS
  ;; ===========================================================================

  (define reductions/st
    (union-reduction-relations
     (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))))
            "ECstG"]
       [==> (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)
            "ECstF"]
       ;; 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))
            "ECstU"]
       where
       [(==> 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)))