(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)
(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"]
[==> (cast dynamic (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)))