(module section-5-exceptions-base mzscheme
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2))
           (prefix natural-embedding: "section-3-natural-embedding-1.ss")
           "core-calculi.ss"
           "language-composer-tools.ss")
  (provide (all-defined))

  (define-pre-grammar exceptions-base
    (s:e (handle s:e s:e))
    (m:e  (handle m:e m:e)
          (raise m:ty string))
    
    (exn-sc s:nfc (in-named-hole s s:nfc (GSM m:ty exn-mc)))
    (s:nfc s:nhc (in-named-hole s s:nhc (handle s:e s:nfc)))
    (s:nhc sc)
    
    (exn-mc m:nfc (in-named-hole m m:nfc (MSG m:ty exn-sc)))
    (m:nfc m:nhc (in-named-hole m m:nhc (handle m:e m:nfc)))
    (m:nhc mc)
    
    ((replace E) exn-mc))
  
  ;; dynamic
  
  (define (exceptions-base-scheme-reductions ms)
    (list
     (reduction ms
                (in-named-hole s
                               E_1
                               (handle s:e s:v_1))
                (term (in-hole E_1 s:v_1)))))
  
  (define (exceptions-base-ml-reductions ms)
    (list
     (reduction ms
                (in-named-hole m
                               E_1
                               (handle m:e m:v_1))
                (term (in-hole E_1 m:v_1)))))
  
  
  ;; ============================================================
  ;; TYPE SYSTEM
  
  (define-type-judgements exns-types
    (m:typeof Γ
      [`(handle ,e1 ,e2)
        (let ((t1 (m:typeof e1 Γ))
              (t2 (m:typeof e2 Γ)))
          (if (and t1 t2 (equal? t1 t2))
              t1
              #f))]
      [`(raise ,tau ,s)
        tau])
    (s:typeof Γ
      [`(handle ,e1 ,e2)
        (if (and (s:typeof e1 Γ) (s:typeof e2 Γ))
            'TST
            #f)]))
  
  (define-values (m:typeof s:typeof) (type-system-union base-types natural-embedding:natural-embedding-types exns-types)))