herman-tomb-flanagan.ss
```(module herman-tomb-flanagan 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 coercion-language
(extend-language language/htf
[nc (! D)
(? D)
(function nc nc)
(∘ (! function) (function nc nc))
(∘ (function nc nc) (? function))
succ
fail]
[C hole
(∘ C c)
(∘ nc C)
(function C c)
(function nc C)]))

(define coercion-normalization
(reduction-relation coercion-language
[--> (∘ succ c_0)
c_0
"IdentL"]
[--> (∘ c_0 succ)
c_0
(side-condition (not (eq? (term c_0) 'succ)))
"IdentR"]
[--> (∘ fail c_0)
fail
"ZeroL"]
[--> (∘ c_0 fail)
fail
"ZeroR"]
[--> (∘ (? D_0) (! D_0))
succ
"CheckY"]
[--> (∘ (? D_0) (! D_1))
fail
(side-condition (not (eq? (term D_0) (term D_1))))
"CheckN"]
[--> (∘ (function c_1 c_2) (function c_3 c_4))
(function (∘ c_3 c_1) (∘ c_2 c_4))
"Fun"]
[--> (∘ c_0 c_0)
c_0
"Idem"]
;; TODO: can we prove these never happen?
[--> (∘ (! D_0) (! D_1))
fail
(side-condition (not (eq? (term D_0) (term D_1))))
[--> (∘ (? D_0) (? D_1))
fail
(side-condition (not (eq? (term D_1) (term D_2))))
;; TODO: I'm really unsure of these next couple rules
[--> (∘ (∘ c_0 (? function)) (∘ (! function) c_1))
(∘ c_0 c_1)
"FunCheckY"]
[--> (∘ (∘ c_0 (? function)) (! D_0))
fail
(side-condition (not (eq? (term D_0) 'function)))
"FunCheckN"]
;; TODO: what about (∘ (! D_0) (? D_1))
;; TODO: are there other possible stuck states I haven't defined?
[--> (∘ (∘ c_0 (function c_1 c_2)) (function c_3 c_4))
(∘ c_0 (∘ (function c_1 c_2) (function c_3 c_4)))
"Assoc"]
))

(define normalized-coercion?
(let ([test (test-match coercion-language nc)])
(let ([normalized-coercion? (lambda (c)
(not (not (test c))))])
normalized-coercion?)))

(define normalize-coercion
(let ([r (context-closure coercion-normalization coercion-language C)])
(letrec ([normalize-coercion (lambda (c)
(if (normalized-coercion? c)
c
(match (apply-reduction-relation r c)
[() (error 'normalize-coercion (format "could not normalize: ~a" c))]
[(c) (normalize-coercion c)]
[(c ...) (error 'normalize-coercion (format "non-deterministic normalization: ~a" c))])))])
normalize-coercion)))

(define reductions/htf
(union-reduction-relations
(core-reductions language/htf)
(reduction-relation language/htf
[--> (in-hole E_0 ((cast ((t_0 -> t_1) <= (function c_0 c_1)) s_0) v_0))
(in-hole E_0 (cast (t_1 <= c_1) (s_0 (cast (t_0 <= c_0) v_0))))
"E-CApp"]
[--> (in-hole E_0 (cast (t_0 <= succ) s_0))
(in-hole E_0 s_0)
(side-condition (not (test-match language/htf (in-hole E_1 (cast (t_1 <= c_1) hole)) (term E_0))))
"E-Succ"]
[--> (in-hole E_0 (cast (t_0 <= fail) e_0))
"error: failed cast"
"E-Fail"]
[--> (in-hole E_0 (cast (t_0 <= c_0) (cast (t_1 <= c_1) e_0)))
,(term-let ([c_2 (normalize-coercion (term (∘ c_0 c_1)))])
(term (in-hole E_0 (cast (t_0 <= c_2) e_0))))
"E-CCast"]
)))

(define (coerce/htf src dst)
(define (coerce src dst)
(cond
[(equal? src dst) 'succ]
[(and (eq? src 'bool) (eq? dst 'dynamic)) '(! bool)]
[(and (eq? src 'int) (eq? dst 'dynamic)) '(! int)]
[(and (eq? src 'dynamic) (eq? dst 'bool)) '(? bool)]
[(and (eq? src 'dynamic) (eq? dst 'int)) '(? int)]
[(and (function-type? src) (function-type? dst))
`(function ,(coerce (function-type-domain dst) (function-type-domain src))
,(coerce (function-type-range src) (function-type-range dst)))]
[(and (eq? src 'dynamic) (function-type? dst))
(normalize-coercion
`(∘ ,(coerce '(dynamic -> dynamic) dst) (? function)))]
[(and (function-type? src) (eq? dst 'dynamic))
(normalize-coercion
`(∘ (! function) ,(coerce src '(dynamic -> dynamic))))]
[else
(error 'coerce (format "cannot coerce ~a to ~a" src dst))]))
`(,dst <= ,(coerce src dst)))

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

(provide (all-defined)))
```