(module iswim mzscheme
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 4))
           (planet "subst.ss" ("robby" "redex.plt" 4))
           (lib "contract.ss"))
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;; Expression grammar:
  
  (define-language iswim-grammar
    (M (M M)
       (o1 M)
       (o2 M M)
       V
       ("letcc" X M)
       ("cc" M M))
    (V X
       ("lam" variable M)
       b
       ("[" M "]"))
    (X variable)
    (b number)
    (o1 "add1" "sub1" "iszero")
    (o2 "+" "-" "*" "^")
    (on o1 o2)
    
    ;; Evaluation contexts:
    (E hole
       (E M)
       (V E)
       (o1 E)
       (o2 E M)
       (o2 V E)
       ("cc" E M)
       ("cc" V E))
    
    ;; Continuations (CK machine):
    (k "mt"
       ("fun" V k)
       ("arg" M k)
       ("narg" (V ... on) (M ...) k))
    
    ;; Environments and closures (CEK):
    (env ((X = vcl) ...))
    (cl (M : env))
    (vcl (V- : env))
    
    ;; Values that are not variables:
    (V- ("lam" variable M)
        b)
    
    ;; Continuations with closures (CEK):
    (k- "mt"
        ("fun" vcl k-)
        ("arg" cl k-)
        ("narg" (vcl ... on) (cl ...) k-)))

  (define M? (test-match iswim-grammar M))
  (define V? (test-match iswim-grammar V))
  (define o1? (test-match iswim-grammar o1))
  (define o2? (test-match iswim-grammar o2))
  (define on? (test-match iswim-grammar on))
  (define k? (test-match iswim-grammar k))

  (define env? (test-match iswim-grammar env))
  (define cl? (test-match iswim-grammar cl))
  (define vcl? (test-match iswim-grammar vcl))
  (define k-? (test-match iswim-grammar k-))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;; Substitution:
  
  ;; The subst form makes implemention of capture-avoiding
  ;; easier. We just have to describe how variables bind
  ;; in our language's forms.
  
  (define iswim-subst/backwards
    (subst
     [(? symbol?) (variable)]
     [(? number?) (constant)]
     [`("lam" ,X ,M)
      (all-vars (list X))
      (build (lambda (X-list M) `("lam" ,(car X-list) ,M)))
      (subterm (list X) M)]
     [`(,(and o (or "add1" "sub1" "iszero")) ,M1)
      (all-vars '())
      (build (lambda (vars M1) `(,o ,M1)))
      (subterm '() M1)]
     [`(,(and o (or "+" "-" "*" "^")) ,M1 ,M2)
      (all-vars '())
      (build (lambda (vars M1 M2) `(,o ,M1 ,M2)))
      (subterm '() M1)
      (subterm '() M2)]
     [`(,M1 ,M2)
      (all-vars '())
      (build (lambda (empty-list M1 M2) `(,M1 ,M2)))
      (subterm '() M1)
      (subterm '() M2)]
     [`("letcc" ,X ,M)
      (all-vars (list X))
      (build (lambda (X-list M) `("letcc" ,(car X-list) ,M)))
      (subterm (list X) M)]
     [`("cc" ,M1 ,M2)
      (all-vars '())
      (build (lambda (vars M1 M2) `("cc" ,M1 ,M2)))
      (subterm '() M1)
      (subterm '() M2)]
     [`("[" ,E "]")
      (all-vars '())
      (build (lambda (vars) `("[" ,E "]")))]))
     

  ;; the argument order for the subst-generated function
  ;; doesn't match the order in the notes:
  (define (iswim-subst M Xr Mr)
    (iswim-subst/backwards Xr Mr M))

  (define empty-env '())

  ;; Environment lookup
  (define (env-lookup env X)
    (let ([m (assq X env)])
      (and m (caddr m))))

  ;; Environment extension
  (define (env-extend env X vcl)
    (cons (list X '= vcl) env))
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;; Reductions:
  
  ;; beta_v reduction
  (define beta_v
    (reduction-relation
     iswim-grammar
     (--> (("lam" X_1 M_1) V_1)
          ,(iswim-subst (term M_1) (term X_1) (term V_1)))))
  
  (define delta
    (reduction-relation
     iswim-grammar
     (--> ("add1" b_1) ,(add1 (term b_1)))
     (--> ("sub1" b_1) ,(sub1 (term b_1)))
     (--> ("iszero" b_1)
          ,(if (zero? (term b_1)) 
               (term ("lam" x ("lam" y x)))
               (term ("lam" x ("lam" y y)))))
     (--> ("+" b_1 b_2) ,(+ (term b_1) (term b_2)))
     (--> ("-" b_1 b_2) ,(- (term b_1) (term b_2)))
     (--> ("*" b_1 b_2) ,(* (term b_1) (term b_2)))
     (--> ("^" b_1 b_2) ,(expt (term b_1) (term b_2)))))
  
  ;; ->v
  (define ->v (compatible-closure (union-reduction-relations beta_v delta)
                                  iswim-grammar 
                                  M))
  
  ;; :->v
  (define :->v (context-closure (union-reduction-relations beta_v delta)
                                iswim-grammar
                                E))

  ;; :->v+letcc
  (define :->v+letcc 
    (union-reduction-relations
     :->v
     (reduction-relation
      iswim-grammar
      
      ;; letcc rule:
      (--> (in-hole E_1 ("letcc" X_1 M_1))
           (in-hole E_1 ,(iswim-subst (term M_1)
                                      (term X_1)
                                      `("[" (in-hole E_1 ||) "]"))))
      
      ;; cc rule:
      (--> (in-hole E ("cc" ("[" (in-hole E_2 ||) "]") V_1))
           (in-hole E_2 V_1)))))
			
  
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;; Helpers:
  
  (define (delta*n on Vs)
    (let ([l (apply-reduction-relation delta `(,on ,@Vs))])
      (if (null? l)
	  #f
	  (car l))))

  (define (delta*1 o1 V)
    (delta*n o1 (list V)))

  (define (delta*2 o2 V1 V2)
    (delta*n o2 (list V1 V2)))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;; Abbreviations:
  
  (define (if0 test then else)
    (let ([X (variable-not-in `(,then ,else) 'X)])
      `(((("iszero" ,test) ("lam" ,X ,then)) ("lam" ,X ,else)) 77)))
  
  (define true '("lam" x ("lam" y x)))
  (define false '("lam" x ("lam" y y)))
  (define boolean-not `("lam" x ((x ,false) ,true)))
  
  (define mkpair '("lam" x ("lam" y ("lam" s ((s x) y)))))
  (define fst '("lam" p (p ("lam" x ("lam" y x)))))
  (define snd '("lam" p (p ("lam" x ("lam" y y)))))
  
  (define Y_v '("lam" f ("lam" x
			 ((("lam" g (f ("lam" x ((g g) x))))
			   ("lam" g (f ("lam" x ((g g) x)))))
			  x))))
  
  (define mksum `("lam" s
		  ("lam" x 
		   ,(if0 'x 0 '("+" x (s ("sub1" x)))))))
  (define sum `(,Y_v ,mksum))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;; Exports:
  
  (provide/contract (iswim-grammar compiled-lang?)
		    (M? (any/c . -> . boolean?))
		    (V? (any/c . -> . boolean?))
		    (o1? (any/c . -> . boolean?))
		    (o2? (any/c . -> . boolean?))
		    (on? (any/c . -> . boolean?))
		    (k? (any/c . -> . boolean?))
		    (env? (any/c . -> . boolean?))
		    (cl? (any/c . -> . boolean?))
		    (vcl? (any/c . -> . boolean?))
		    (iswim-subst (M? symbol? M? . -> . M?))
		    (env-lookup (env? symbol? . -> . (union false/c vcl?)))
		    (env-extend (env? symbol? vcl? . -> . env?))
		    (empty-env env?)
		    (beta_v reduction-relation?)
		    (delta reduction-relation?)
		    (delta*1 (o1? V?  . -> . (union false/c V?)))
		    (delta*2 (o2? V? V? . -> .  (union false/c V?)))
		    (delta*n (on? (listof V?) . -> .  (union false/c V?)))
		    (->v reduction-relation?)
		    (:->v reduction-relation?)
		    (:->v+letcc reduction-relation?)
		    (if0 (M? M? M? . -> . M?))
		    (true M?)
		    (false M?)
		    (boolean-not M?)
		    (mkpair M?)
		    (fst M?)
		    (snd M?)
		    (Y_v M?)
		    (sum M?)))