#lang plait #:untyped

;; Original
(local [(define len
          (lambda (l)
            (type-case (Listof 'x) l
              [empty 0]
              [(cons fst rst) (+ 1 (len rst))])))]
  (len (list 1 2 3)))

;; Convert `type-case` to `if`
(local [(define len
          (lambda (l)
            (if (empty? l)
                0
                (+ 1 (len (rest l))))))]
  (len (list 1 2 3)))

;; Get rid of `list`
(local [(define len
          (lambda (l)
            (if (empty? l)
                0
                (+ 1 (len (rest l))))))]
  (len (cons 1 (cons 2 (cons 3 empty)))))

;; Convert `local` to `letrec`
(letrec ([len
          (lambda (l)
            (if (empty? l)
                0
                (+ 1 (len (rest l)))))])
  (len (cons 1 (cons 2 (cons 3 empty)))))

;; This was the key trick: self-application instead of letrec
(let ([len
       (lambda (lenX l)
         (if (empty? l)
             0
             (+ 1 (lenX lenX (rest l)))))])
  (len len (cons 1 (cons 2 (cons 3 empty)))))

;; Avoid 2-argument functions
(let ([lenX
       (lambda (lenX)
         (lambda (l)
           (if (empty? l)
               0
               (+ 1 ((lenX lenX) (rest l))))))])
  ((lenX lenX) (cons 1 (cons 2 (cons 3 empty)))))

;; Wrap up as a 1-argument `len`
(let ([len (lambda (l)
             (let ([lenX
                    (lambda (lenX)
                      (lambda (l)
                        (if (empty? l)
                            0
                            (+ 1 ((lenX lenX) (rest l))))))])
               ((lenX lenX) l)))])
  (len (cons 1 (cons 2 (cons 3 empty)))))

;; Simplify `len`
(let ([len (let ([lenX
                  (lambda (lenX)
                    (lambda (l)
                      (if (empty? l)
                          0
                          (+ 1 ((lenX lenX) (rest l))))))])
             (lenX lenX))])
  (len (cons 1 (cons 2 (cons 3 empty)))))

;; Try to lift out `(lenX lenX)`, but it runs out of memory
#;
(let ([len (let ([lenX
                  (lambda (lenX)
                    (let ([len (lenX lenX)])
                      (lambda (l)
                        (if (empty? l)
                            0
                            (+ 1 (len (rest l)))))))])
             (lenX lenX))])
  (len (cons 1 (cons 2 (cons 3 empty)))))

;; Delay `(lenX lenX)` to avoid an infinite loop
(let ([len (let ([lenX
                  (lambda (lenX)
                    (let ([len (lambda (l) ((lenX lenX) l))])
                      (lambda (l)
                        (if (empty? l)
                            0
                            (+ 1 (len (rest l)))))))])
             (lenX lenX))])
  (len (cons 1 (cons 2 (cons 3 empty)))))

(let ([sum
       (let ([lenX
              (lambda (lenX)
                (let ([sum (lambda (l) ((lenX lenX) l))])
                  (lambda (l)
                    (if (empty? l)
                        0
                        (+ (first l) (sum (rest l)))))))])
         (lenX lenX))])
  (sum (cons 3 (cons 7 (cons 5 empty)))))