(module section-3-natural-embedding-1 mzscheme
  
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2))           
           (lib "plt-match.ss")
           "language-composer-tools.ss"
           "core-calculi.ss")
  
  (provide (all-defined))
  
  ;; ============================================================
  ;; LANGUAGE GRAMMARS
  
  (define-pre-grammar simple-natural-embedding-extensions
    (s:e (GSM m:ty m:e))
    (m:e (MSG m:ty s:e)))
  
  (define-pre-grammar simple-natural-embedding-contexts
    (sc  (GSM m:ty mc))
    (mc  (MSG m:ty sc))
    (E mc))
  
  (define ms (grammar-union base simple-natural-embedding-extensions simple-natural-embedding-contexts))
  ;; ------------------------------------------------------------
  ;; DYNAMIC SEMANTICS
  
  (define (natural-embedding-scheme-reductions ms)
    (list
     (reduction ms
                (in-named-hole s
                               E_1
                               (GSM num number_1))
                (term (in-hole E_1 number_1)))
     (reduction ms
                (in-named-hole s
                               E_1
                               (GSM (m:ty_1 -> m:ty_2) m:v_1))
                (term (in-hole E_1 (lambda (y) (GSM m:ty_2 (m:v_1 (MSG m:ty_1 y)))))))))
  
  (define (natural-embedding-ml-reductions ms)
    (list
     (reduction ms
                (in-named-hole m
                               E_1
                               (MSG num number_1))
                (term (in-hole E_1 number_1)))
     (reduction ms
                (side-condition
                 (in-named-hole m
                                E_1
                                (MSG num s:v_1))
                 (not (number? (term s:v_1))))
                (term (in-hole E_1 (MSG num (wrong "Non-number")))))
     (reduction ms
                (in-named-hole m
                               E_1
                               (MSG (m:ty_1 -> m:ty_2) (lambda (x_1) s:e_1)))
                (term (in-hole E_1 (lambda (y : m:ty_1) (MSG m:ty_2 ((lambda (x_1) s:e_1) (GSM m:ty_1 y)))))))
     (reduction ms
                (side-condition
                 (in-named-hole m
                                E_1
                                (MSG (m:ty_1 -> m:ty_2) s:v_1))
                 (number? (term s:v_1)))
                (term (in-hole E_1 (MSG (m:ty_1 -> m:ty_2) (wrong "Non-procedure")))))))
  
  (define reductions (append (base-scheme-reductions ms) (natural-embedding-scheme-reductions ms)
                             (base-ml-reductions ms) (natural-embedding-ml-reductions ms)))

  ;; ------------------------------------------------------------
  ;; TYPE SYSTEM
  
  (define-type-judgements natural-embedding-types
    (m:typeof Γ
      [`(MSG ,ty ,se)
        (if (s:typeof se Γ) ty #f)])
    (s:typeof Γ
      [`(GSM ,mty ,m)
        (if (equal? mty (m:typeof m Γ)) 'TST #f)]))

  (define-values (m:typeof s:typeof) (type-system-union base-types natural-embedding-types))
  
  ;; ============================================================
  ;; TESTS
  (define-values (gui E N1 N2) (get-evaluators ms m:typeof reductions error-message?)))