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

  ;; ============================================================
  ;; LANGUAGE GRAMMARS
  (define ms (grammar-union base
                            natural-embedding:simple-natural-embedding-extensions
                            exceptions-base))
  
  ;; ------------------------------------------------------------
  ;; DYNAMIC SEMANTICS
  
  (define exns2-ml-reductions
    (list
     
     (reduction ms
                (in-named-hole m
                               E_1
                               (handle m:e_handler (in-named-hole m m:nhc (raise m:ty string))))
                (term (in-hole E_1 m:e_handler)))
     
     (reduction ms
                (in-named-hole m m:nhc (raise m:ty string_1))
                (term string_1))

     (reduction ms
                (in-named-hole m
                               E
                               (MSG m:ty (in-named-hole s s:nhc (wrong string_1))))
                (term string_1))))
  
  (define exns2-scheme-reductions
    (list
     (reduction ms
                (in-named-hole s
                               E_1
                               (handle s:e_handler (in-named-hole s s:nhc (wrong string))))
                (term (in-hole E_1 s:e_handler)))
     
     (reduction ms
                (in-named-hole s
                               E
                               (GSM m:ty (in-named-hole m m:nhc (raise m:ty string_1))))
                (term string_1))))
  
  (define reductions (append (base-scheme-reductions/no-wrong ms)
                             (natural-embedding:natural-embedding-scheme-reductions ms)
                             (exceptions-base-scheme-reductions ms)
                             exns2-scheme-reductions
                             
                             (base-ml-reductions ms)
                             (natural-embedding:natural-embedding-ml-reductions ms)
                             (exceptions-base-ml-reductions ms)
                             exns2-ml-reductions))
  
  ;; ============================================================
  ;; TESTS 
  (define-values (gui E N1 N2) (get-evaluators ms m:typeof reductions error-message?))


  ;; exception-specific tests
  #;(define tests
   (test (handle (lambda (x : num) x) 
                 ((lambda (x : (num -> num)) x) (lambda (y : num) y))) (lambda (y : num) y))
   (test (handle (lambda (x : num) x) ((lambda (z : num) z) (raise num "error"))) "Type error")
   (test (handle 3 ((lambda (z : num) z) (raise num "error"))) 3)
   (test (MSG (num -> num)
             (handle (lambda (x) x) (handle (lambda (x) (x x)) (wrong "user error"))))
         (lambda (y : num) 
           (MSG num ((lambda (x) (x x)) (GSM num y)))))
   (test (+ 3 (raise num "ML error")) "ML error")
   (test (handle 3 (MSG num (wrong "user error"))) "user error")
   (test (MSG num (GSM num (raise num "ML error"))) "ML error")
   (test (handle 34 (MSG num (GSM num (MSG num (GSM num (raise num "ML error")))))) "ML error")
   (test (MSG num (handle 200 (GSM num (handle 20 (MSG num (wrong "user error")))))) "user error")
   (test (MSG num (handle 200 (GSM num (handle 20 (MSG num (GSM num (raise num "ML error"))))))) "ML error")
   (test (handle 1 ((handle (lambda (x : num) (raise num "ML")) 
                            (raise (num -> num) "ML 2"))
                    2))
         1)
   (test (MSG num (+ 1 (lambda (x) x))) "non-number")
   (test (MSG num (2 3)) "non-procedure")
   (test (MSG num (handle 42 (+ 3 (GSM num (MSG num (3 12)))))) "non-procedure")))