(module section-5-polymorphism 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 polymorphism-extensions
    (s:e (GSM m:ty m:e))
    (m:e (MSG m:ty s:e) (LAMBDA (x) m:e) (tyapp m:e m:ty))

    (m:v (MSG L s:v) (LAMBDA (x) m:e))
    
    (m:ty L (forall (x) m:ty) x))
  
  (define-pre-grammar polymorphism-contexts
    (sc  (GSM m:ty mc))
    (mc  (MSG m:ty sc) (tyapp mc m:ty))
    (E mc))
  
  (define ms (grammar-union base polymorphism-extensions polymorphism-contexts))
  ;; ------------------------------------------------------------
  ;; DYNAMIC SEMANTICS
  
  
  (define op? (language->predicate ms 'op))
  (define pr? (language->predicate ms 'pr))
  
  (define (substitute-type type var new-type)
    (define (do-sub type)
      (match type
        [(? (λ (t) (and (symbol? t) (not (eq? t var))))) type]
        [(? (λ (t) (and (symbol? t) (eq? t var)))) new-type]
        [`(,t1 -> ,t2)
          `(,(do-sub t1) -> ,(do-sub t2))]
        [`(forall (,x) ,t2)
          (if (eq? x var)
              `(forall (,x) ,t2)
              `(forall (,x) ,(do-sub t2)))]
        [_ (error 'do-sub "unknown type ~s" type)]))
    (do-sub type))
  
  (define (type-sub t var new-type)
    (define (do-sub type) (substitute-type type var new-type))
    (define (m:ts p)
      (match p
        [(? symbol?) p]
        [(? number?) p]
        [`(lambda (,x : ,mty) ,e)
          `(lambda (,x : ,(do-sub mty)) ,(m:ts e))]
        [`(MSG ,mty ,sterm)
          `(MSG ,(do-sub mty) ,(s:ts sterm))]
        [`(,(? op? o) ,e1 ,e2)
          `(,o ,(m:ts e1) ,(m:ts e2))]
        [`(ifzero ,e1 ,e2 ,e3)
          `(ifzero ,(m:ts e1) ,(m:ts e2) ,(m:ts e3))]
        [`(tyapp ,e ,mty)
          `(tyapp ,(m:ts e) ,(do-sub mty))]
        [`(LAMBDA (,x) ,e)
          (if (eq? x var)
              `(LAMBDA (,x) ,e)
              `(LAMBDA (,x) ,(m:ts e)))]
        [`(,e1 ,e2)
          `(,(m:ts e1) ,(m:ts e2))]))
  
    (define (s:ts p)
      (match p
        [(? symbol?) p]
        [(? number?) p]
        [`(lambda (,x) ,e)
          `(lambda (,x) ,(s:ts e))]
        [`(,(? op? o) ,e1 ,e2)
          `(,o ,(s:ts e1) ,(s:ts e2))]
        [`(,(? pr? p) ,e)
          `(,p ,(s:ts e))]
        [`(wrong ,(? string? s))
          `(wrong ,s)]
        [`(ifzero ,e1 ,e2 ,e3)
          `(ifzero ,(s:ts e1) ,(s:ts e2) ,(s:ts e3))]
        [`(GSM ,mty ,mterm)
          `(GSM ,(do-sub mty) ,(m:ts mterm))]
        [`(,e1 ,e2)
          `(,(s:ts e1) ,(s:ts e2))]))
    (m:ts t))
  
  (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)))))))
     (reduction ms
                (in-named-hole s
                               E_1
                               (GSM (forall (x_1) m:ty_1) m:v_1))
                (term (in-hole E_1 (GSM ,(substitute-type (term m:ty_1) (term x_1) (term L))
                                        (tyapp m:v_1 L)))))
     (reduction ms
                (in-named-hole s
                               E_1
                               (GSM L (MSG L s:v_1)))
                (term (in-hole E_1 s:v_1)))))
  
  (define (natural-embedding-ml-reductions ms)
    (list
     (reduction ms
                (in-named-hole m E_1 (tyapp (LAMBDA (x_1) m:e_1) m:ty_1))
                (term (in-hole E_1 ,(type-sub (term m:e_1) (term x_1) (term m:ty_1)))))
     (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")))))
     (reduction ms
                (in-named-hole m E_1 (MSG (forall (x_1) m:ty_1) s:v_1))
                (term (in-hole E_1 (LAMBDA (x_1) (MSG m:ty_1 s:v_1)))))))
  
  (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)]
      [`(MS ,ty ,se)
        (if (s:typeof se Γ) ty #f)]
      [`(LAMBDA (,x) ,e)
        (let ((body-ty (m:typeof e Γ))) ;; note :: we simply assume that type variables are not used free
          (if body-ty
              `(forall (,x) ,body-ty)
              #f))]
      [`(tyapp ,e ,t) ;; again, we just assume that t is a valid type
        (let ((fn-ty (m:typeof e Γ)))
          (match fn-ty
            [`(forall (,x) ,body-ty)
              (substitute-type body-ty x t)]
            [_ #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?)))