(module section-3-natural-embedding-3 mzscheme
  
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2))
           (lib "plt-match.ss")
           "core-calculi.ss"
           "language-composer-tools.ss")
  
  (provide (all-defined))
  
  ;; ============================================================
  ;; LANGUAGE GRAMMARS
  
  (define-pre-grammar contracts-natural-embedding
    (s:e (SM m:ty m:e) (g+ m:ty s:e) (g- m:ty s:e))
    (m:e (MS m:ty s:e)))
  
  (define-pre-grammar contracts-natural-embedding-contexts
    (sc  (SM m:ty mc) (g+ m:ty sc) (g- m:ty sc))
    (mc  (MS m:ty sc))
    (E mc))
  
  (define ms (grammar-union base contracts-natural-embedding contracts-natural-embedding-contexts))
  
  ;; ------------------------------------------------------------
  ;; DYNAMIC SEMANTICS
  
  (define contracts-scheme-reductions
    (list
     ;; mapping
     (reduction ms
                (in-named-hole s
                               E_1
                               (SM num number_1))
                (term (in-hole E_1 number_1)))
     (reduction ms
                (in-named-hole s
                               E_1
                               (SM (m:ty_1 -> m:ty_2) m:v_1))
                (term (in-hole E_1 (lambda (y) (SM m:ty_2 (m:v_1 (MS m:ty_1 y)))))))
     
     ;; guards
     (reduction ms
                (in-named-hole s
                               E_1
                               (g+ (m:ty_1 -> m:ty_2) (lambda (x_a) s:e_b)))
                (term (in-hole E_1 (lambda (y) (g+ m:ty_2 ((lambda (x_a) s:e_b) (g- m:ty_1 y)))))))
     (reduction ms
                (in-named-hole s
                               E_1
                               (g+ (m:ty_1 -> m:ty_2) number))
                (term (in-hole E_1 (wrong "Non-procedure"))))
     (reduction ms
                (in-named-hole s
                               E_1
                               (g+ num s:v_1))
                (if (number? (term s:v_1))
                    (term (in-hole E_1 s:v_1))
                    (term (in-hole E_1 (wrong "Non-number")))))
     (reduction ms
                (in-named-hole s
                               E_1
                               (g- (m:ty_1 -> m:ty_2) (lambda (x_a) s:e_b)))
                (term (in-hole E_1 (lambda (y) (g- m:ty_2 ((lambda (x_a) s:e_b) (g+ m:ty_1 y)))))))
     (reduction ms
                (in-named-hole s
                               E_1
                               (g- num s:v_1))
                (term (in-hole E_1 s:v_1)))))
  
  (define contracts-ml-reductions
    (list
     (reduction ms
                (in-named-hole m
                               E_1
                               (MS num number_1))
                (term (in-hole E_1 number_1)))
     (reduction ms
                (in-named-hole m
                               E_1
                               (MS (m:ty_1 -> m:ty_2) s:v_1))
                (term (in-hole E_1 (lambda (y : m:ty_1) (MS m:ty_2 (s:v_1 (SM m:ty_1 y)))))))))
  
  (define reductions (append (base-scheme-reductions ms) contracts-scheme-reductions
                             (base-ml-reductions ms) contracts-ml-reductions))

  ;; ------------------------------------------------------------
  ;; TYPE SYSTEM
  
  (define-type-judgements contracts-types
    (m:typeof Γ
      [`(MS ,ty ,se)
        (if (s:typeof se Γ) ty #f)])
    (s:typeof Γ
      [`(SM ,mty ,m)
        (if (equal? mty (m:typeof m Γ)) 'TST #f)]
      [`(g+ ,mty ,e) (s:typeof e Γ)]
      [`(g- ,mty ,e) (s:typeof e Γ)]))
  
  (define-values (m:typeof s:typeof) (type-system-union base-types contracts-types))
  
  ;; ============================================================
  ;; ELABORATION
  (define op? (language->predicate ms 'op))
  (define pr? (language->predicate ms 'pr))
  
  (define (m:elaborate p)
    (match p
      [(? symbol?) p]
      [(? number?) p]
      [`(lambda (,x : ,mty) ,e)
       `(lambda (,x : ,mty) ,(m:elaborate e))]
      [`(MS ,mty ,mterm)
       `(MS ,mty (g+ ,mty ,(s:elaborate mterm)))]
      [`(,(? op? o) ,e1 ,e2)
        `(,o ,(m:elaborate e1) ,(m:elaborate e2))]
      [`(ifzero ,e1 ,e2 ,e3)
        `(ifzero ,(m:elaborate e1) ,(m:elaborate e2) ,(m:elaborate e3))]
      [`(,e1 ,e2)
        `(,(m:elaborate e1) ,(m:elaborate e2))]))
  
  (define (s:elaborate p)
    (match p
      [(? symbol?) p]
      [(? number?) p]
      [`(lambda (,x) ,e)
       `(lambda (,x) ,(s:elaborate e))]
      [`(,(? op? o) ,e1 ,e2)
        `(,o ,(s:elaborate e1) ,(s:elaborate e2))]
      [`(g+ ,mty ,e)
        `(g+ ,mty ,(s:elaborate e))]
      [`(g- ,mty ,e)
        `(g- ,mty ,(s:elaborate e))]
      [`(,(? pr? p) ,e)
        `(,p ,(s:elaborate e))]
      [`(wrong ,(? string? s))
        `(wrong ,s)]
      [`(ifzero ,e1 ,e2 ,e3)
        `(ifzero ,(s:elaborate e1) ,(s:elaborate e2) ,(s:elaborate e3))]
      [`(SM ,mty ,mterm)
       `(g- ,mty (SM ,mty ,(m:elaborate mterm)))]
      [`(,e1 ,e2)
        `(,(s:elaborate e1) ,(s:elaborate e2))]))

  ;; ============================================================
  ;; TESTS
  (define-values (gui E N1 N2) (get-evaluators ms m:typeof reductions error-message?)))