(module section-2-lump-embedding mzscheme
  
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2))
           (lib "plt-match.ss")
           "language-composer-tools.ss"
           "core-calculi.ss")
  
  (provide (all-defined))
  
  ;; ============================================================
  ;; THE Scheme<->ML embedding example calculus
  ;; (really embedding untyped cbv LC and simply-typed cbv LC)

  ;; ------------------------------------------------------------
  ;; GRAMMARS
  (define-pre-grammar lump-extensions
    (s:e (SM m:ty m:e))
    (s:v (side-condition (SM m:ty_1 m:v) (not (equal? (term m:ty_1) 'L))))
    (sc  (SM m:ty mc))
    
    (m:e (MS m:ty s:e))
    (m:v (MS L s:v))
    (m:ty  L)
    (mc (MS m:ty sc))
    (E mc))
  
  (define ms (grammar-union base lump-extensions))
  
  ;; ------------------------------------------------------------
  ;; DYNAMIC SEMANTICS
  (define scheme-lump-reductions
    (list
     (reduction ms
                (in-named-hole s
                               E_1
                               (SM L (MS L s:v_1)))
                (term (in-hole E_1 s:v_1)))))
  
  (define ml-lump-reductions
    (list
     (reduction ms
                (side-condition
                 (in-named-hole m
                                E_1
                                (MS m:ty_1 (SM m:ty_1 m:v_1)))
                 (not (equal? (term m:ty_1) 'L)))
                (term (in-hole E_1 m:v_1)))
     (reduction ms
                (side-condition
                 (in-named-hole m
                                E_1
                                (MS m:ty_1 s:v_1))
                 (and
                  (not (equal? (term m:ty_1) 'L))
                  (not 
                   (match (term s:v_1)
                     [`(SM ,ty2 ,_)
                       (equal? (term m:ty_1) ty2)]
                     [_ #f]))))
                (term "Bad value"))))
  
  (define reductions (append scheme-lump-reductions (base-scheme-reductions ms)
                             ml-lump-reductions (base-ml-reductions ms)))
  
  ;; ------------------------------------------------------------
  ;; TYPE SYSTEM
  
  (define-type-judgements lump-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)]))
    
  (define-values (m:typeof s:typeof) (type-system-union base-types lump-types))
  
  ;; ------------------------------------------------------------
  ;; TESTS
  (define-values (gui E N1 N2) (get-evaluators ms m:typeof reductions error-message?))
)