(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))))
           "BadTags"]
      [--> (∘ (? D_0) (? D_1))
           fail
           (side-condition (not (eq? (term D_1) (term D_2))))
           "BadChecks"]
      ;; 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)))