(module section-4-typed-lump-embedding mzscheme
  
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2))
           (planet "gui.ss" ("robby" "redex.plt" 2))
           (planet "subst.ss" ("robby" "redex.plt" 2))
           (lib "plt-match.ss"))
  
  ;; ============================================================
  ;; THE Scheme<->ML embedding example calculus
  ;; (really embedding untyped cbv LC and simply-typed cbv LC)

  ;; ------------------------------------------------------------
  ;; LANGUAGE GRAMMARS
  
  (define mm
    (language      
     (m:e (m:e m:e) 
          x 
          (lambda (x : m:ty) m:e)
          (op m:e m:e)
          number
          (ifzero m:e m:e m:e)
          (M1M2 m:ty m2:ty m2:e))
     (m:v (lambda (x : m:ty) m:e)
          number
          (side-condition
           (M1M2 L1 m2:ty m2:v_1)
           (not (match (term m2:v_1)
                  [`(M2M1 ,_ L1 ,v) #t]
                  [_ #f]))))
     (op + -)
     (m:ty num (m:ty -> m:ty) L1)
     
     (mc (hole m) 
         (mc m:e)
         (m:v mc)
         (op mc m:e)
         (op m:v mc)
         (ifzero mc m:e m:e)
         (M1M2 m:ty m2:ty m2c))
     
     
     ;; ml
     (m2:e (m2:e m2:e) 
          x 
          (lambda (x : m2:ty) m2:e)
          (op m2:e m2:e)
          number
          (ifzero m2:e m2:e m2:e)
          (M2M1 m2:ty m:ty m:e))
     (m2:v (lambda (x : m2:ty) m2:e)
           number
           (side-condition
            (M2M1 L2 m:ty m:v_1)
            (not (match (term m:v_1)
                   [`(M1M2 ,_ L2 ,v) #t]
                   [_ #f]))))
     (m2:ty num (m2:ty -> m2:ty) L2)
     
     (m2c (hole m2) 
          (m2c m2:e)
          (m2:v m2c)
          (op m2c m2:e)
          (op m2:v m2c)
          (ifzero m2c m2:e m2:e)
          (M2M1 m2:ty m:ty mc))

     (x (variable-except lambda M1M2 M2M1 -> num L1 L2 ifzero + -))))
  
  ;; ------------------------------------------------------------
  ;; DYNAMIC SEMANTICS
  
  (define m1-reductions
    (list
     
     ;; beta
     (reduction mm
                (in-named-hole m 
                               mc_1
                               ((lambda (x_a : m:ty) m:e_b) m:v_a))
                (term (in-hole mc_1 
                               ,(substitute (term x_a) (term m:v_a) (term m:e_b)))))
     
     ;; sum
     (reduction mm
                (in-named-hole m
                               mc_1
                               (+ number_1 number_2))
                (term
                 (in-hole 
                  mc_1 
                  ,(+ (term number_1) (term number_2)))))
     (reduction mm
                (in-named-hole m
                               mc_1
                               (- number_1 number_2))
                (term
                 (in-hole 
                  mc_1 
                  ,(max (- (term number_1) (term number_2)) 0))))
     
     ;; ifzero
     (reduction mm
                (in-named-hole m
                               mc_1
                               (ifzero number_1 m:e_1 m:e_2))
                (cond
                  [(eqv? (term number_1) 0)
                   (term (in-hole mc_1 m:e_1))]
                  [else
                   (term (in-hole mc_1 m:e_2))]))
     
     ;; mapping
     (reduction mm
                (side-condition
                 (in-named-hole m
                                mc_1
                                (M1M2 m:ty_1 L2 (M2M1 L2 m:ty_1 m:v_1)))
                 (not (equal? (term m:ty_1) 'L1)))
                (term (in-hole mc_1 m:v_1)))
     
     (reduction mm
                (side-condition
                 (in-named-hole m
                                mc_1
                                (M1M2 m:ty_1 L2 (M2M1 L2 m:ty_2 m:v_2)))
                 (and 
                  (not (equal? (term m:ty_1) 'L1))
                  (not (equal? (term m:ty_1) (term m:ty_2)))))
                (format 
                 "Bad conversion (M1M2): can't convert ~s to ~s"
                 (term (M2M1 L2 m:ty_2 m:v_2))
                 (term m:ty_1)))))
  
  
  (define m2-reductions
    (list
     
     ;; beta
     (reduction mm
                (in-named-hole m2
                               mc_1
                               ((lambda (x_a : m2:ty) m2:e_b) m2:v_a))
                (term (in-hole mc_1 
                               ,(substitute (term x_a) (term m2:v_a) (term m2:e_b)))))
     
     ;; sum
     (reduction mm
                (in-named-hole m2
                               mc_1
                               (+ number_1 number_2))
                (term
                 (in-hole 
                  mc_1 
                  ,(+ (term number_1) (term number_2)))))
     (reduction mm
                (in-named-hole m2
                               mc_1
                               (- number_1 number_2))
                (term
                 (in-hole 
                  mc_1 
                  ,(max (- (term number_1) (term number_2)) 0))))
     
     ;; ifzero
     (reduction mm
                (in-named-hole m2
                               mc_1
                               (ifzero number_1 m2:e_1 m2:e_2))
                (cond
                  [(eqv? (term number_1) 0)
                   (term (in-hole mc_1 m2:e_1))]
                  [else
                   (term (in-hole mc_1 m2:e_2))]))
     
     ;; mapping
     (reduction mm
                (side-condition
                 (in-named-hole m2
                                mc_1
                                (M2M1 m2:ty_1 L1 (M1M2 L1 m2:ty_1 m2:v_1)))
                 (not (equal? (term m2:ty_1) 'L2)))
                (term (in-hole mc_1 m2:v_1)))
     (reduction mm
                (side-condition
                 (in-named-hole m2
                                mc_1
                                (M2M1 m2:ty_1 L1 (M1M2 L1 m2:ty_2 m2:v_1)))
                 (and
                  (not (equal? (term m2:ty_1) 'L2))
                  (not (equal? (term m2:ty_1) (term m2:ty_2)))))
                (term "Bad conversion (M2M1)"))))
  
  (define reductions (append m1-reductions m2-reductions))
    
  ;; ------------------------------------------------------------
  ;; TYPE SYSTEM
  (define op? (language->predicate mm 'op))
  
  
  ;; m:typeof : m:e env -> m:ty | #f
  ;; determines the type of an ML program.
  (define (m:typeof p Γ)
    (match p
      [(? string?) 'error]
      [(? symbol?) (lookup p Γ)]
      [(? number?) 'num]
      [`(,e_1 ,e_2)
        (match (list (m:typeof e_1 Γ) (m:typeof e_2 Γ))
          [`((,ty_dom -> ,ty_rng) ,ty_arg)
            (if (equal? ty_dom ty_arg)
                ty_rng
                #f)]
          [_ #f])]
      [`(lambda (,x : ,dom_ty) ,e)
        (let ((rng_ty (m:typeof e (extend Γ x dom_ty))))
          (if rng_ty
              `(,dom_ty -> ,rng_ty)
              #f))]
      [`(,(? op?) ,e_1 ,e_2)
        (match (list (m:typeof e_1 Γ) (m:typeof e_2 Γ))
          [`(num num)
            'num]
          [_ #f])]
      [`(ifzero ,e1 ,e2 ,e3)
        (let ((t1 (m:typeof e1 Γ))
              (t2 (m:typeof e2 Γ))
              (t3 (m:typeof e2 Γ)))
          (if (and (equal? t1 'num)
                   (equal? t2 t3))
              t2
              #f))]
      [`(M1M2 ,mty ,m2ty ,m2e)
        (let ((subty (m2:typeof m2e Γ)))
          (if (and subty (equal? subty m2ty))
              mty
              #f))]))
  
  (define (m2:typeof p Γ)
    (match p
      [(? symbol?) (lookup p Γ)]
      [(? number?) 'num]
      [`(,e_1 ,e_2)
        (match (list (m2:typeof e_1 Γ) (m2:typeof e_2 Γ))
          [`((,ty_dom -> ,ty_rng) ,ty_arg)
            (if (equal? ty_dom ty_arg)
                ty_rng
                #f)]
          [_ #f])]
      [`(lambda (,x : ,dom_ty) ,e)
        (let ((rng_ty (m2:typeof e (extend Γ x dom_ty))))
          (if rng_ty
              `(,dom_ty -> ,rng_ty)
              #f))]
      [`(,(? op?) ,e_1 ,e_2)
        (match (list (m2:typeof e_1 Γ) (m2:typeof e_2 Γ))
          [`(num num)
            'num]
          [_ #f])]
      [`(ifzero ,e1 ,e2 ,e3)
        (let ((t1 (m2:typeof e1 Γ))
              (t2 (m2:typeof e2 Γ))
              (t3 (m2:typeof e2 Γ)))
          (if (and (equal? t1 'num)
                   (equal? t2 t3))
              t2
              #f))]
      [`(M2M1 ,m2ty ,mty ,me)
        (let ((subty (m:typeof me Γ)))
          (if (and subty (equal? mty subty))
              m2ty
              #f))]))
  
  ;; ------------------------------------------------------------
  ;; ENVIRONMENT MANAGEMENT
  
  (define empty-set '())
  (define (lookup x Γ)
    (let ((ans (assq x Γ)))
      (unless ans
        (error 'lookup "Variable not in environment: ~a" x))
      (cadr ans)))
  (define (extend Γ x v)
    (cons (list x v) Γ))  
    
  ;; ------------------------------------------------------------
  ;; MISC. HELPERS  
  (define (truish v) (if v #t #f))
  
  (define (newname x) (string->symbol (symbol->string (gensym x))))
  
  (define substitute
    (subst
     [(? symbol?) (variable)]
     [(? number?) (constant)]
     [`(lambda (,x : ,ty) ,b)
      (all-vars (list x))
      (build (lambda (vars body) `(lambda (,(car vars) : ,ty) ,body)))
      (subterm (list x) b)]
     [`(M1M2 ,ty1 ,ty2 ,e)
      (all-vars '())
      (build (lambda (vars eb) `(M1M2 ,ty1 ,ty2 ,eb)))
      (subterm '() e)]
     [`(M2M1 ,ty2 ,ty1 ,e)
      (all-vars '())
      (build (lambda (vars eb) `(M2M1 ,ty2 ,ty1 ,eb)))
      (subterm '() e)]
     [`(,(? op? o) ,e1 ,e2)
      (all-vars '())
      (build (lambda (vars e1 e2) `(,o ,e1 ,e2)))
      (subterm '() e1)
      (subterm '() e2)]
     [`(ifzero ,e1 ,e2 ,e3)
      (all-vars '())
      (build (lambda (vars e1 e2 e3) `(ifzero ,e1 ,e2 ,e3)))
      (subterm '() e1)
      (subterm '() e2)
      (subterm '() e3)]
     [`(,f ,x)
      (all-vars '())
      (build (lambda (vars f x) `(,f ,x)))
      (subterm '() f)
      (subterm '() x)]))

  ;; ------------------------------------------------------------
  ;; TEST CODE
  

  (define (run p)
    (let* ([thetype (m:typeof p empty-set)]
           [initial-term (if thetype p "Type error")])
      (traces/pred mm 
                   reductions
                   (list initial-term)
                   (λ (x) 
                     (let ((newtype (m:typeof x empty-set)))
                       (or (equal? newtype thetype)
                           (eq? newtype 'error)))))))
  
  (define (evaluate p)
    (if (m:typeof p empty-set)
        (normalize p)
        "Type error"))
  
  (define m:value? (language->predicate mm 'm:v))

  (define normalize (λ (p) (normalize* p void)))
  (define normalize/tell (λ (p) (normalize* p (λ (x) (write x) (newline)))))
  (define (normalize* p observer)
    (let loop ((p p))
      (observer p)
      (cond
        [(m:value? p) p]
        [else
         (let ((nexts (reduce reductions p)))
           (cond
             [(null? nexts) p]
             [(null? (cdr nexts))
              (loop (car nexts))]
             [else
              (error 'normalize "Term ~s reduces multiple ways" p)]))])))

  (require-for-syntax (lib "etc.ss"))
  (define-syntax (tests stx)
    (syntax-case stx (test)
      [(_ (test term expected)  ...)
       (with-syntax ([(num ...) (build-list (length (syntax-e #'(term ...))) add1)])
         #`(let ((numcases #,(length (syntax-e #'(term ...))))
                 (numfailed 0))
             (let ((fail (lambda (exp result)
                           (set! numfailed (add1 numfailed))
                           (printf "TEST ~a FAILED :\nTest:\t\t~s\nExpected:\t~s\nReceived:\t~s\n\n" num 'term exp result))))
               (with-handlers ([exn:fail? (lambda (exn) (fail 'expected (format "[exception: ~a]" (exn-message exn))))])
                 
                 (let ((ans (evaluate `term))
                       (e   `expected))
                   (unless (α-equivalent? ans e)
                     (fail e ans)))))
             ...
             (if (= numfailed 0)
                 (printf "Passed all ~a tests.\n" numcases)
                 (printf "Passed ~a out of ~a tests.\n" (- numcases numfailed) numcases))))]))
  
  (define (α-equivalent? p1 p2)
    
    (define free (gensym))
    (define (mt var) free)
    (define (extend env var depth)
      (lambda (v)
        (if (eq? v var) depth (env v))))
    
    (define (m:α-equivalent? p1 p2 depth m1 m2)
      (match (list p1 p2)
        [`(,(? symbol?) ,(? symbol?))
          (eq? (m1 p1) (m2 p2))]
        [`(,(? number?) ,(? number?))
         (= p1 p2)]
        [`(,(? string?) ,(? string?))
         (string=? p1 p2)]
        [`((lambda (,x1 : ,ty1) ,b1) (lambda (,x2 : ,ty2) ,b2))
          (m:α-equivalent? b1 b2 (add1 depth) (extend m1 x1 depth) (extend m2 x2 depth))]
        [`((,p1f ,p1a) (,p2f ,p2a))
          (and (m:α-equivalent? p1f p2f depth m1 m2)
               (m:α-equivalent? p1a p2a depth m1 m2))]
        [`((,(? op? o1)  ,p1f ,p1a) (,(? op? o2) ,p2f ,p2a))
          (and (eqv? o1 o2)
               (m:α-equivalent? p1f p2f depth m1 m2)
               (m:α-equivalent? p1a p2a depth m1 m2))]
        [`((ifzero ,e11 ,e12 ,e13) (ifzero ,e21 ,e22 ,e23))
          (and (m:α-equivalent? e11 e21 depth m1 m2)
               (m:α-equivalent? e12 e22 depth m1 m2)
               (m:α-equivalent? e13 e23 depth m1 m2))]
        [`((M1M2 ,ty11 ,ty12 ,st1) (M1M2 ,ty21 ,ty22  ,st2))
          (and (equal? ty11 ty21)
               (equal? ty12 ty22)
               (m2:α-equivalent? st1 st2 depth m1 m2))]
        [_ #f]))
    
    (define (m2:α-equivalent? p1 p2 depth m1 m2)
      (match (list p1 p2)
        [`(,(? symbol?) ,(? symbol?))
          (eq? (m1 p1) (m2 p2))]
        [`(,(? number?) ,(? number?))
         (= p1 p2)]
        [`(,(? string?) ,(? string?))
         (string=? p1 p2)]
        [`((lambda (,x1 : ,ty1) ,b1) (lambda (,x2 : ,ty2) ,b2))
          (m2:α-equivalent? b1 b2 (add1 depth) (extend m1 x1 depth) (extend m2 x2 depth))]
        [`((,p1f ,p1a) (,p2f ,p2a))
          (and (m2:α-equivalent? p1f p2f depth m1 m2)
               (m2:α-equivalent? p1a p2a depth m1 m2))]
        [`((,(? op? o1)  ,p1f ,p1a) (,(? op? o2) ,p2f ,p2a))
          (and (eqv? o1 o2)
               (m2:α-equivalent? p1f p2f depth m1 m2)
               (m2:α-equivalent? p1a p2a depth m1 m2))]
        [`((ifzero ,e11 ,e12 ,e13) (ifzero ,e21 ,e22 ,e23))
          (and (m2:α-equivalent? e11 e21 depth m1 m2)
               (m2:α-equivalent? e12 e22 depth m1 m2)
               (m2:α-equivalent? e13 e23 depth m1 m2))]
        [`((M2M1 ,ty12 ,ty11 ,m1t1) (M2M1 ,ty22 ,ty21 ,m1t2))
          (and (equal? ty11 ty21)
               (equal? ty12 ty22)
               (m:α-equivalent? m1t1 m1t2 depth m1 m2))]
        [_ #f]))
    
    (m:α-equivalent? p1 p2 0 mt mt))
  
  #;(tests
   (test ((lambda (x : num) x) 4) 4)
   (test ((lambda (x : (num -> num)) x) (lambda (y : num) y))
         (lambda (y : num) y))
  
   (test (+ 5 12) 17)
   (test (- 12 5) 7)
   (test (- 5 12) 0)
   (test (ifzero 0 2 3) 2)
   (test (ifzero 1 2 3) 3)
   (test (M1M2 L1 num (+ 5 12)) (M1M2 L1 num 17))
   (test (M1M2 L1 num (- 5 12)) (M1M2 L1 num 0))
   (test (M1M2 L1 num (ifzero 0 2 3)) (M1M2 L1 num 2))
   (test (M1M2 L1 num (ifzero 1 2 3)) (M1M2 L1 num 3))
   
   (test (M1M2 L1 (num -> num) ((lambda (x : (num -> num)) x) 4)) "Type error")
   (test ((lambda (x : (num -> num)) x) 4) "Type error")
   
   (test (M1M2 num L2 (M2M1 L2 num 3)) 3)
   (test (M1M2 L1 num (M2M1 num L1 (M1M2 L1 num 3))) (M1M2 L1 num 3))
   
   (test (M1M2 (num -> num) L2 (M2M1 L2 num 3)) "Bad conversion")
   (test (M1M2 L1 (num -> num) (M2M1 (num -> num) L1 (M1M2 L1 num 3))) "Bad conversion"))
  
  (define (nontermination-example)
    ;; P : (L1 -> L1) -> L1
    (define P `(lambda (x : (L1 -> L1)) (M1M2 L1 (num -> L2) (lambda (z : num) (M2M1 L2 (L1 -> L1) x)))))
    ;; U : L1 -> (L1 -> L1)
    (define U `(lambda (x : L1) (M1M2 (L1 -> L1) L2 ((M2M1 (num -> L2) L1 x) 0))))
    (run `((lambda (x : L1) ((,U x) x)) (,P (lambda (x : L1) ((,U x) x))))))
  
  ;; display a GUI with the example reduction sequence
  (nontermination-example))