(module iswim mzscheme
  (require "../reduction-semantics.ss"
	   (lib "contract.ss"))
  ;; Expression grammar:
  (define iswim-grammar
    (language (M (M M)
		 (o1 M)
		 (o2 M M)
		 ("letcc" X M)
		 ("cc" M M))
	      (V X
		 ("lam" variable M)
		 ("[" 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)

	      ;; 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
     [(? 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
     (--> (("lam" X_1 M_1) V_1)
          ,(iswim-subst (term M_1) (term X_1) (term V_1)))))
  (define delta
     (--> ("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)
  ;; :->v
  (define :->v (context-closure (union-reduction-relations beta_v delta)

  ;; :->v+letcc
  (define :->v+letcc 
      ;; 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)
	  (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)))))
  (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?)))