;; Use in  DrScheme, version 207, Language: Pretty Big,  Case sensitive.
;; coding F-F's small numerical ISWIM example on p 39
;; <http://www.ccs.neu.edu/course/com3357/mono.ps>. 

;; Use HtDP structs to code the BNF definition of Exp:
;; M :: = x | n | (lambda (x) M) | (M M) | (op1 M) | (op2 M M)
;; op1 ::= iszero? | - | add1 | sub1
;; op2 ::= + | - | * | quotient | expt

(define 1aryPrimOp
  (list 'iszero? '- 'add1 'sub1 'display))

;; display is only added for LC_v debugging purposes, following a suggestion
;; of Joe Marshall.  As indicated in the BNF above, display is *not* part of 
;; the ISWIM language.   For that matter, the procedures E and E_1 have
;; a number of print statements for errors, but these error messages are
;; only for us LC_v programmers, and are not part of the ISWIM semantics.

(define 2aryPrimOp
  (list '+ '- '* 'quotient 'expt '=? '<? '>? '<=? '>=?))

(define-struct variable (var))
(define-struct pre-abstraction (var body))   ;; bound variables in  Exp
(define-struct abstraction (body))   ;; the deBruijn tree version in LC_vExp below
(define-struct comb (proc arg))
(define-struct 1ary-prim-comb (op arg))
(define-struct 2ary-prim-comb (op arg1 arg2))
(define-struct 3ary-prim-comb (op arg1 arg2 arg3))

;; the BNF/struct definition of the syntactic domain Exp:

(define (Exp? exp)
  ;; any ---> boolean
  ;; to determine if some value is in Exp.  That is, if exp is a 
  ;; satisfying the BNF specification of Exp above
  (cond 
    [(variable? exp)
     (symbol? (variable-var exp))]
    [(integer? exp) 
     true]
    [(pre-abstraction? exp)
     (and (symbol? (pre-abstraction-var exp))
          (Exp? (pre-abstraction-body exp)))]
    
    [(comb? exp)
     (and (Exp? (comb-proc exp))
          (Exp? (comb-arg exp)))]
    
    [(1ary-prim-comb? exp)
     (and (member (1ary-prim-comb-op exp) 1aryPrimOp)
          (Exp? (1ary-prim-comb-arg exp)))]
    
    [(2ary-prim-comb? exp)
     (and (member (2ary-prim-comb-op exp) 2aryPrimOp)
          (Exp? (2ary-prim-comb-arg1 exp))
          (Exp? (2ary-prim-comb-arg2 exp)))]
    [else false]))

;; Define the hybrid set (not syntactic or semantic domain) LC_vExp.
;; 
;; Mod out by alpha-equivalence by turning Exp expressions into
;; deBruijn trees.  Free variables go to themselves; that's perhaps a
;; mild novelty.  A bound variable x is replaced by a number, which is
;; the distance up the tree to the binding occurence of x, i.e. the
;; (lambda (x) ....) creating the lexical scope in which x belongs.
;; So (lambda (x) x) is replaced by (lambda <0>), and 
;; (lambda (x) (+ x y))  is replaced by (lambda (+ <1> y)), etc.
;;
;; Such deBruijn trees will now be called elements of the hybrid set 
;; LC_vExp.  A BNF/struct definition is given in the predicate LC_vExp?

(define (LC_vExp? exp)
  ;; any ---> boolean
  ;; to determine if some value is in LC_vExp.  
  ;; M in LC_vExp
  ;; M :: = var | n | (abstraction M) | (M M) | (op1 M) | (op2 M M)
  ;; var ::= x | <n>
  ;; op1 ::= iszero? | - | add1 | sub1
  ;; op2 ::= + | - | * | quotient | expt
  (cond [(variable? exp)
         (let ([v (variable-var exp)])
           (or (symbol? v) (integer? v)))]
        [(integer? exp) 
         true]
        [(abstraction? exp)
         (LC_vExp? (abstraction-body exp))]
        [(comb? exp)
         (and (LC_vExp? (comb-proc exp))
              (LC_vExp? (comb-arg exp)))]
        [(1ary-prim-comb? exp)
         (and (member (1ary-prim-comb-op exp) 1aryPrimOp)
              (LC_vExp? (1ary-prim-comb-arg exp)))]
        [(2ary-prim-comb? exp)
         (and (member (2ary-prim-comb-op exp) 2aryPrimOp)
              (LC_vExp? (2ary-prim-comb-arg1 exp))
              (LC_vExp? (2ary-prim-comb-arg2 exp)))]
        [else false]))

;; Define the semantic domain Value_bottom.  
;; Since we can't code up the noncomputable total map 
;; E: LC_vExp ---> Value_bottom,
;; we replace it by the OpS partial map
;; E: LC_vExp ---> Value

(define (LC_vValue? exp)
  ;; LC_vExp ---> boolean
  ;; to test if an LC_vExp is a Value
  (and (LC_vExp? exp) 
       (or (variable? exp) (integer? exp) (abstraction? exp))))

;; Now the domains are all defined: syntactic, semantic, and hybrid.
;; We'll define (the computable) version of our semantic function
;; E_1: Exp ---> Value_bottom,
;; which is the composite 
;; Exp ---> LC_vExp -E--> Value_bottom
;; where the first map is the function Exp->LC_v below, which converts
;; to a deBruijn tree.  

(define (E_1 exp)
  ;; Exp ---> Value
  (E (Exp->LC_v exp)))

;; First task is the parser, turning quoted lists of symbols & integers into 
;; Exp elements. 

(define (Exp-parser exp)
  ;; quoted text ISWIM expression ---> Exp
  (let ([X (Exp-preParser exp)])
    (if (Exp? X)
        X
        (printf "expression ~v not an parsable to Exp ~n" exp))))

(define (Exp-preParser exp)
  ;; quoted text ISWIM expression ---> Exp struct
  ;; turns the if0 expression (if0 X Y Z) into the F-F's expression 
  ;;                          ((((iszero? X) 
  ;;                             (lambda (DoNotUse) Y)) 
  ;;                            (lambda (DoNotUse) Z)) 0)
  ;; Kludge: we require the variable DoNotUse not be free in either Y or Z.
  ;; Fixing thekludge would replicate deBruijn tree processing below.  
  ;; It's OK to kludge this, as it's a macro of F-F's, and not part of our BNF spec.
  (local ((define (parse-comb? exp)
            (and  (cons? exp) (= (length exp) 2)))
          
          (define (parse-pre-abstraction? exp)
            (and (cons? exp) (= (length exp) 3)
                 (symbol? (first exp)) 
                 (symbol=? (first exp) 'lambda)
                 (cons? (second exp)) (= (length (second exp)) 1) 
                 (symbol? (first (second exp)))))
          
          (define (parse-1ary-prim-comb? exp)
            (and (cons? exp) (= (length exp) 2)
                 (member (first exp) 1aryPrimOp)))
          
          (define (parse-2ary-prim-comb? exp)
            (and (cons? exp) (= (length exp) 3)
                 (member (first exp) 2aryPrimOp)))
          
          (define (parse-if0exp? exp)
            ;; look for expression (if0 X Y Z), where 
            ;; X should be return a number
            (and  (cons? exp) (= (length exp) 4) 
                  (symbol? (first exp)) (symbol=? (first exp) 'if0)))
          
          (define (parse-ifBexp? exp)
            ;; look for expression (ifB X Y Z), where 
            ;; X should be an LC Boolean procedure that returns either 
            ;; LC-true or LC-false
            (and  (cons? exp) (= (length exp) 4)
                  (symbol? (first exp)) (symbol=? (first exp) 'ifB)))
          
          (define (parse-triple-comb? exp)
            (and (cons? exp) (= (length exp) 3)))
          
          (define (parse-let? exp)
            (and  (cons? exp) (= (length exp) 3) 
                  (let ([f (first exp)]
                        [l (second exp)])
                    (and (symbol? f) (symbol=? f 'let)
                         (cons? l) (= (length l) 1)  
                         (let ([var-bind (first l)])
                           (and (cons? var-bind) (= (length var-bind) 2) 
                                (let ([var (first var-bind)]
                                      [bind (second var-bind)])
                                  (symbol? var)))))))))
    
    (cond 
      [(symbol? exp)
       (make-variable exp)]
      [(integer? exp)
       exp]
      [(parse-pre-abstraction? exp)
       (make-pre-abstraction (first (second exp)) (Exp-preParser (third exp)))]
      [(parse-1ary-prim-comb? exp)
       (make-1ary-prim-comb (first exp) (Exp-preParser (second exp)))]
      [(parse-2ary-prim-comb? exp)
       (make-2ary-prim-comb (first exp) 
                            (Exp-preParser (second exp)) 
                            (Exp-preParser (third exp)))]
      [(parse-comb? exp)
       (make-comb (Exp-parser (first exp)) (Exp-preParser (second exp)))]
      [(parse-if0exp? exp)
       ;; pass a list back to Exp-preParser.  Send (if0 X Y Z) to essentially
       ;;                          ((((iszero? X) 
       ;;                             (lambda (DoNotUse) Y)) 
       ;;                            (lambda (DoNotUse) Z)) 0)
       (Exp-preParser
        `((((iszero? ,(second exp)) 
            (lambda (DoNotUse) ,(third exp))) 
           (lambda (DoNotUse) ,(fourth exp))) 0))]
      
      [(parse-ifBexp? exp)
       ;; pass a list back to Exp-preParser.  Send (ifB X Y Z) to essentially
       ;;                          (((X
       ;;                             (lambda (DoNotUse) Y)) 
       ;;                            (lambda (DoNotUse) Z)) 0)
       ;; Like if0, but we assume that X is an LC Boolean procedure, i.e. 
       ;; X returns either LCtrue or LCfalse
       (Exp-preParser
        `(((,(second exp)
             (lambda (DoNotUse) ,(third exp)))
           (lambda (DoNotUse) ,(fourth exp))) 0))]
      
      [(parse-let? exp)
       (Exp-preParser
        ;; given (let ([x bind]) body), pass to Exp-preParser
        ;; ((lambda (x) body) bind)
        (let* ([f (first exp)]
               [var-bind (first (second exp))] 
               [var (first var-bind)]
               [bind (second var-bind)]
               [body (third exp)])
          `((lambda (,var) ,body) ,bind)))]
      
      [(parse-triple-comb? exp)
       ;; pass a list back to Exp-preParser.  Send (X Y Z) to 
       ;;   essentially ((X Y)) Z))
       ;; the purpose is to make the LC_v expressions easier to read: to write
       ;; (cons A B) instead of ((cons A) B), even though in LC_v, procedures
       ;; can only take one op.  But this usage is standard in LC_v anyway:
       ;; it's the associativity convention, where (X Y Z) means ((X Y) Z)
       ;; This option goes last of course because if0, let, and ifB all match.
       (Exp-preParser
        `((,(first exp) ,(second exp)) ,(third exp)))]
      
      
      [else 
       (printf "~v is not in Exp ~n" exp)])))


(define (Exp-print exp)
  ;; Exp ----> list, for printing
  (cond [(variable? exp)
         (variable-var exp)]
        [(integer? exp) 
         exp]
        [(pre-abstraction? exp)
         (list 'lambda (list (pre-abstraction-var exp))
               (Exp-print (pre-abstraction-body exp)))]
        [(comb? exp)
         (list (Exp-print (comb-proc exp))
               (Exp-print (comb-arg exp)))]
        [(1ary-prim-comb? exp)
         (list (1ary-prim-comb-op exp) (Exp-print (1ary-prim-comb-arg exp)))]
        [(2ary-prim-comb? exp)
         (list (2ary-prim-comb-op exp) (Exp-print (2ary-prim-comb-arg1 exp))
               (Exp-print (2ary-prim-comb-arg2 exp)))]
        [else (printf "expression ~v is not in Exp ~n" exp)]))


(define (Exp->LC_v exp)
  ;; Exp ---> LC_vExp
  ;; exp goes to the deBruijn tree, as follows.
  ;; We change all the bound variables simultaneously, by descending
  ;; through a tree maintaining a list of pairs (x, n) of bound
  ;; variables and tree depths.  When we descend, we increment n unless
  ;; the expression is (lambda (x) ...), and there we reset n to -1.  A
  ;; (lambda (x) ...) is replaced by (abstraction ...), since the number
  ;; -1 would convey no information.
  (deBruinize exp empty))

(define (deBruinize exp alovar-num)
  ;; Exp x (listof (var num)) ----> LC_vExp 
  ;; an element of LC_vExp is a deBruin tree, made out of structs, so 
  ;; a variable-var will now return an integer n >= 0.
  ;; alovar-num is a list of pairs (x n) of bound variables together with the 
  ;; tree-depth up to the binding occurence
  (local ((define (find-var-in-alovar-num y alovar-num)
            ;; given a list of pairs (x n), and a variable y, 
            ;; test if y is a first of an element in the list 
            ;; if so, return the pair (y, n).  Otherwise return false
            (let ([y-tail (memf 
                           (lambda (var-num) 
                             (symbol=? y (first var-num)))
                           alovar-num)])
              (if y-tail
                  (first y-tail)
                  false)))
          
          (define (1+alovar-num alox-n)
            ;; list of (x n) goes to list (x n+1) 
            (map (lambda (x-n)
                   (list (first x-n) (add1 (second x-n))))
                 alox-n)))
    
    (cond [(variable? exp)
           (let ([var-num (find-var-in-alovar-num (variable-var exp) 
                                                  alovar-num)])
             (if var-num
                 (make-variable (second var-num))
                 exp))]
          [(integer? exp) 
           exp]
          
          [(pre-abstraction? exp)
           (let* ([y (pre-abstraction-var exp)]
                  [y-n (find-var-in-alovar-num  y alovar-num)])
             (make-abstraction 
              (deBruinize (pre-abstraction-body exp) 
                          (1+alovar-num 
                           (cons (list y  -1)
                                 ;; if y occurs in list of (x n), then remove it first
                                 (if y-n
                                     (remove y-n alovar-num)
                                     alovar-num))))))]
          [else 
           (let ([1+list (1+alovar-num alovar-num)])
             
             (cond [(comb? exp)
                    (make-comb (deBruinize (comb-proc exp) 1+list)
                               (deBruinize (comb-arg exp) 1+list))]
                   
                   [(1ary-prim-comb? exp)
                    (make-1ary-prim-comb (1ary-prim-comb-op exp)
                                         (deBruinize (1ary-prim-comb-arg exp) 1+list))]
                   
                   [(2ary-prim-comb? exp)
                    (make-2ary-prim-comb (2ary-prim-comb-op exp)
                                         (deBruinize (2ary-prim-comb-arg1 exp) 1+list)
                                         (deBruinize (2ary-prim-comb-arg2 exp) 1+list))]
                   [else (print "not an ISWIM expression")]))])))

(define (LC_vExp-print exp)
  (cond [(variable? exp)
         (let ([v (variable-var exp)])
           (if (symbol? v)
               v
               (list v)))]
        [(integer? exp) 
         exp]
        [(abstraction? exp)
         (list 'lambda 
               (LC_vExp-print (abstraction-body exp)))]
        [(comb? exp)
         (list (LC_vExp-print (comb-proc exp))
               (LC_vExp-print (comb-arg exp)))]
        [(1ary-prim-comb? exp)
         (list (1ary-prim-comb-op exp) (LC_vExp-print (1ary-prim-comb-arg exp)))]
        [(2ary-prim-comb? exp)
         (list (2ary-prim-comb-op exp) (LC_vExp-print (2ary-prim-comb-arg1 exp))
               (LC_vExp-print (2ary-prim-comb-arg2 exp)))]
        [else (print "not an ISWIM expression")]))


(define (substitute exp V n)
  ;; Substitute V into the deBruijn tree of exp.  That is, 
  ;; descend through the tree of body of proc, and substitute in arg at depth n
  ;; if the variable is n. 
  (cond [(variable? exp)
         (let ([p (variable-var exp)])
           (if (and (integer? p) (= p n))
               V
               exp))]
        [(integer? exp) 
         exp]
        [(abstraction? exp)
         (make-abstraction 
          (substitute (abstraction-body exp) V (add1 n)))]
        
        [(comb? exp)
         (make-comb (substitute (comb-proc exp) V (add1 n))
                    (substitute (comb-arg exp) V (add1 n)))]
        
        [(1ary-prim-comb? exp)
         (make-1ary-prim-comb (1ary-prim-comb-op exp)
                              (substitute  (1ary-prim-comb-arg exp) V (add1 n)))]
        
        [(2ary-prim-comb? exp)
         (make-2ary-prim-comb (2ary-prim-comb-op exp)
                              (substitute  (2ary-prim-comb-arg1 exp) V (add1 n))
                              (substitute  (2ary-prim-comb-arg2 exp) V (add1 n)))]))


(define (LC_v-redex? exp)
  ;; LC_vExp ---> boolean
  ;; true if exp is either (abstraction value) | (op1 value) | (op2 value value)
  (if (not (LC_vExp? exp))
      (printf "expression not in LC_vExp ~n")
      (if (LC_vValue? exp)
          false
          (cond 
            [(comb? exp)
             (and (abstraction? (comb-proc exp)) 
                  (LC_vValue? (comb-arg exp)))]
            
            [(1ary-prim-comb? exp)
             (let ([arg (1ary-prim-comb-arg exp)])
               (if (not (integer? arg))
                   (printf "1ary-prim-call violation: ~n argument ~v is not an integer ~n" 
                           (LC_vExp-print arg)))
               (LC_vValue? arg))]
            
            [(2ary-prim-comb? exp)
             (let ([arg1 (2ary-prim-comb-arg1 exp)]
                   [arg2 (2ary-prim-comb-arg2 exp)])
               (if (not (integer? arg1))
                   (printf "2ary-prim-call violation: ~n 1st arguments ~v  not an integer ~n" 
                           (LC_vExp-print arg1))
                   (if (not (integer? arg2))
                       (printf "2ary-prim-call violation: ~n 2nd arguments ~v  not an integer ~n" 
                               (LC_vExp-print arg2))))
               (and (LC_vValue? arg1) (LC_vValue? arg2)))]))))


(define (beta_v-reduce exp)
  ;; LC_v-redex ---> LC_vExp
  ;; beta_v reduce the LC_v-redex exp
  (if (not (LC_v-redex? exp))
      (printf "expression not a redex ~n")
      (cond 
        [(comb? exp)
         (substitute (abstraction-body (comb-proc exp)) (comb-arg exp) 0)]
        
        [(1ary-prim-comb? exp)
         ((1ary-prim-function (1ary-prim-comb-op exp))
          (1ary-prim-comb-arg exp))]
        
        [(2ary-prim-comb? exp)
         ((2ary-prim-function (2ary-prim-comb-op exp))
          (2ary-prim-comb-arg1 exp)
          (2ary-prim-comb-arg2 exp))])))

(define LC-true 
  '(lambda (x) (lambda (y) x)))

(define LC-false 
  '(lambda (x) (lambda (y) y)))

(define LC_v-true (Exp->LC_v (Exp-parser LC-true)))
(define LC_v-false (Exp->LC_v (Exp-parser LC-false)))


(define (1ary-prim-function op)
  ;; 1aryPrimOp  ---> (Integer -> LC_vValue)
  (cond
    [(symbol=? 'iszero? op) 
     (lambda (n)
       (if (zero? n)
           LC_v-true
           LC_v-false))]
    [(symbol=? '- op) -]
    [(symbol=? 'add1 op) add1]
    [(symbol=? 'sub1 op) sub1]
    [(symbol=? 'display op)
     (lambda (arg)
       (begin
         (display arg)
         (printf " ")
         arg))]))

(define (2ary-prim-function op)
  ;; 2aryPrimOp  ---> (Integer Integer -> LC_vValue)
  (cond
    [(symbol=? '+ op) +]
    [(symbol=? '- op) -]
    [(symbol=? '* op) *]
    [(symbol=? 'quotient op) quotient]
    [(symbol=? 'expt op) expt]
    [(symbol=? '<? op)
     (lambda (n x)
       (if (< n x)
           LC_v-true
           LC_v-false))]
    [(symbol=? '>? op)
     (lambda (n x)
       (if (> n x)
           LC_v-true
           LC_v-false))]
    [(symbol=? '>=? op)
     (lambda (n x)
       (if (>= n x)
           LC_v-true
           LC_v-false))]
    [(symbol=? '<=? op)
     (lambda (n x)
       (if (<= n x)
           LC_v-true
           LC_v-false))]
    [(symbol=? '=? op)
     (lambda (n x)
       (if (= n x)
           LC_v-true
           LC_v-false))]))


;; Function below not actually used, as we don't quite follow F-F's approach
;; of finding the evaluation context & the potential redex, trying  to beta_v
;; reduce potential redex, and plugging it back into the eval context.
;; Instead, we reduce the leftmost redex

(define (find-LC_v-redex exp)
  ;; LC_vExp [non-Value] ---> LC_v-redex + false
  ;; search through exp (assumed not to be a value) 
  ;; to find the leftmost redex
  (if (not (LC_vExp? exp))
      (printf "expression not in LC_vExp ~n")
      (cond 
        [(LC_vValue? exp)
         (print "no redex: expression is a value")]
        [(comb? exp)
         (let ([proc (comb-proc exp)]
               [arg (comb-arg exp)])
           (if (LC_vValue? proc)
               (if (abstraction? proc)
                   (if (LC_vValue? arg)
                       exp
                       (find-LC_v-redex arg))
                   ;false)
                   (printf "it's not an abstraction: ~n" 
                           (LC_vExp-print proc)))
               (find-LC_v-redex proc)))]
        
        [(1ary-prim-comb? exp)
         (let ([arg (1ary-prim-comb-arg exp)])
           (if (LC_vValue? arg)
               exp
               (find-LC_v-redex arg)))]
        
        [(2ary-prim-comb? exp)
         (let ([arg1 (2ary-prim-comb-arg1 exp)]
               [arg2 (2ary-prim-comb-arg2 exp)])
           (if (LC_vValue? arg1)
               (if (LC_vValue? arg2)
                   exp
                   (find-LC_v-redex arg2))
               (find-LC_v-redex arg1)))])))

(define (\|--->_v exp)
  ;; LC_vExp [non-Value] --->  LC_vExp + false
  ;; F-F's one-step standard reduction arrow
  ;; search through exp (assumed not to be a value) 
  ;; to find the leftmost redex, and beta_v-reduce it.
  (if (not (LC_vExp? exp))
      (printf "expression not in LC_vExp ~n")
      (cond 
        [(LC_vValue? exp)
         (print "no redex: expression is a value")]
        [(comb? exp)
         (let ([proc (comb-proc exp)]
               [arg (comb-arg exp)])
           (if (LC_vValue? proc)
               (if (abstraction? proc)
                   (if (LC_vValue? arg)
                       (beta_v-reduce exp)
                       (make-comb proc (\|--->_v arg)))
                   (begin 
                     (printf "proc ~v is not an abstraction ~n"
                             (LC_vExp-print proc))
                     false))
               (make-comb (\|--->_v  proc) arg)))]
        
        [(1ary-prim-comb? exp)
         (let ([op (1ary-prim-comb-op exp)]
               [arg (1ary-prim-comb-arg exp)])
           (if (LC_vValue? arg)
               (beta_v-reduce exp)
               (make-1ary-prim-comb op (\|--->_v arg))))]
        
        [(2ary-prim-comb? exp)
         (let ([op (2ary-prim-comb-op exp)]
               [arg1 (2ary-prim-comb-arg1 exp)]
               [arg2 (2ary-prim-comb-arg2 exp)])
           (if (LC_vValue? arg1)
               (if (LC_vValue? arg2)
                   (beta_v-reduce exp)
                   (make-2ary-prim-comb op arg1 (\|--->_v arg2)))
               (make-2ary-prim-comb op (\|--->_v arg1) arg2)))])))

(define (E exp)
  ;; LC_vExp [non-Value] --->  LC_vValue + false
  ;; F-F's transitive closure of the one-step standard reduction arrow
  (if (not (LC_vExp? exp))
      (printf "expression ~v not in LC_vExp ~n" 
              (LC_vExp-print exp))
      (if (LC_vValue? exp)
          exp
          (E (\|--->_v exp)))))

(define exp '(((lambda (f)
                 ((lambda (x) (x x))
                  (lambda (x) 
                    (f (lambda (p) ((x x) p))))))
               (lambda (f)
                 (lambda (n)
                   (if0 n
                        1
                        (* (display n) (f (sub1 n))))))) 5))
exp
(define exp1 (Exp-parser exp))
(Exp-print exp1)
(define exp2 (Exp->LC_v exp1))
(LC_vExp-print exp2)
(E exp2)

(printf "big quicksort example ~n")

;; LC_v implementation of HtDP's 25.2 quick-sort procedure: their 2nd example
;; of generative recursion

;; Lists are implemented as simple procedures.  
;; The empty list is (lambda (x) 0), and (empty? f) = (f 0)
;; cons is only used to create nonempty lists.   So 
;; (cons x f) is the procedure sending 0 ->1, 1 -> x, and 2 -> f.  
;; Then of course (first f) = (f 1), (rest f) = (f 2)

(define exp 
  '(let ([Y_v 
          (lambda (f)
            ((lambda (d) (d d)) 
             (lambda (x) (f (lambda (p) ((x x) p))))))])
     (let ([empty 
            (lambda (x) 0)])
       (let ([empty? 
              (lambda (alist)
                (iszero? (alist 0)))])
         (let ([cons
                (lambda (x)
                  (lambda (alist)
                    (lambda (i)
                      (if0 i
                           1
                           ( ifB (=? i 1)
                                 x
                                 alist)))))])
           (let ([first 
                  (lambda( alist)
                    (alist 1))])
             (let ([rest 
                    (lambda (alist)
                      (alist 2))])
               (let 
                   ([append 
                     (Y_v 
                      (lambda (append)
                        (lambda (A)
                          (lambda (B)
                            (ifB (empty? A)
                                 B
                                 ((cons (first A)) 
                                  ((append (rest A)) 
                                   B)))))))])
                 (let ([larger-items 
                        (Y_v (lambda (larger-items)
                               (lambda (alon) 
                                 (lambda (threshold)
                                   (ifB (empty? alon) 
                                        empty
                                        (ifB (>? (first alon) threshold)
                                             (cons (first alon) 
                                                   (larger-items (rest alon) threshold))
                                             (larger-items (rest alon) threshold)))))))])
                   (let ([smaller-items 
                          (Y_v (lambda (smaller-items)
                                 (lambda (alon) 
                                   (lambda (threshold)
                                     (ifB (empty? alon) 
                                          empty
                                          (ifB (<? (first alon) threshold)
                                               (cons (first alon) 
                                                     (smaller-items (rest alon) threshold))
                                               (smaller-items (rest alon) threshold)))))))])
                     (let ([quick-sort
                            (Y_v (lambda (quick-sort)
                                   (lambda (alon)
                                     (ifB (empty? alon) 
                                          empty
                                          (append
                                           (quick-sort (smaller-items (rest alon) (first alon)))
                                           (cons (first alon)
                                                 (quick-sort (larger-items (rest alon) (first alon)))))))))])
                       (let ([x 
                              (cons 5 
                                    (cons 1
                                          (cons 2 
                                                (cons 3
                                                      (cons 5 
                                                            (cons 4
                                                                  (cons 1
                                                                        (cons 2
                                                                              (cons 3
                                                                                    (cons 4 empty))))))))))])
                         (quick-sort x)
                         ))))))))))))
exp
(define exp1 (Exp-parser exp))
(E_1 exp1)
(define exp2 (E_1 exp1))

(define (LC_vList->list exp)
  ;; LC_vValue [abstraction] ---> (listof number)
  ;; assume exp is an abstraction which actually is one of our 
  ;; lists, so a function f s.t. (f 0) = 1 iff the list is nonempty
  (let ([LC_vList-empty? 
         (lambda (exp)
           (zero? (E (make-comb exp 0))))]
        [LC_vList-first 
         (lambda (exp)
           (E (make-comb exp 1)))]
        [LC_vList-rest
         (lambda (exp)
           (E (make-comb exp 2)))])
    (if (LC_vList-empty? exp)
        empty
        (cons (LC_vList-first exp)
              (LC_vList->list (LC_vList-rest exp))))))


(LC_vList->list exp2)


(printf "print out the 29 one-step reductions for 2!, for 
2! = (* 2 1!) = (* 2 (* 1 0!)) = (* 2 (* 1 1)) = (* 2 1) = 2 ~n")

(define (E exp)
  ;; LC_vExp [non-Value] --->  LC_vValue + false
  ;; F-F's transitive closure of the one-step standard reduction arrow
  (if (not (LC_vExp? exp))
      (printf "expression ~v not in LC_vExp" 
              (LC_vExp-print exp))
      (begin 
        (printf "~v ~n" 
                (LC_vExp-print exp))
        (if (LC_vValue? exp)
            exp
            (begin 
              (printf "\\|--->_v~n")
              (E (\|--->_v exp)))))))

(define exp '(((lambda (f)
                 ((lambda (x) (x x))
                  (lambda (x) 
                    (f (lambda (p) ((x x) p))))))
               (lambda (f)
                 (lambda (n)
                   (ifB (iszero? n)
                        1
                        (* n (f (sub1 n))))))) 2))
exp
(define exp1 (Exp-parser exp))
(Exp-print exp1)
(E_1 exp1)