;; NbE on untyped deBruin Lambda-Terms
;; ===================================

;;
;; Syntactical Objects
;; -------------------
(define (abstr syntax) (list 'abs syntax))
(define (app syntaxA syntaxB)(list 'app syntaxA syntaxB))
(define (var n)(list 'var n))
(define (abs? syntax)(eq? (car syntax) 'abs))
(define (app? syntax)(eq? (car syntax) 'app))
(define (var? syntax)(eq? (car syntax) 'var))
(define var-nr cadr)(define app-l cadr) (define app-r caddr)
(define abs-body cadr)

;; Output
;; ------

(define (syntax-to-string syntax)
  (cond ((var? syntax)(format "~a" (var-nr syntax)))
        ((abs? syntax)(format "[~a]" (syntax-to-string (abs-body syntax))))
        ((app? syntax)(format "~a ~a @" 
                              (syntax-to-string (app-l syntax))
                              (syntax-to-string (app-r syntax))))))


;; Terms
;; -----
;; Terms are mappings from the level to the syntactical 
;; representation  of a term at this level:

(define (fv k) (lambda (n) (var (+ n k))))
(define (bv k) (lambda (n) (var (- n k 1))))
(define (term-app termA termB) 
  (lambda (n) 
    (app (termA n)(termB n))))
(define (term-abstr term)
  (lambda (n) 
    (abstr (term (+ n 1)))))

;; valuations
;; ----------
;; mappings from variables to objects

(define empty (lambda (n) (error "empty valuation" "undefined!")))

(define (dot object valuation) ;; concatenation of valuations
  (lambda (n)
    (if (= n 0) 
        object
        (valuation (- n 1)))))


;;; Input/Output (Parsing)
;;; ------------

(define (explode string)
  ;; returns the lists of symbols of the string
  (letrec 
      ((f (lambda (string n l)
            (cond ((>= n l) '())
                  (else (cons (string-ref string n)
                              (f string (+ n 1) l)))))))
    (f string 0 (string-length string))))

(define (lexer char-list)
  ;; returns a pair of a token and the rest of the list
  ;; a token is either 'app or 'lam or a number
  (if (null? char-list)
      '()
      (letrec ((lex-number (lambda (sofar char-list)
                             (cond ((null? char-list) (cons sofar char-list))
                                   ((char-numeric? (car char-list))
                                    (lex-number 
                                     (+ (* 10 sofar)
                                        (char->integer (car char-list))
                                        (- (char->integer #\0)))
                                     (cdr char-list)))
                                   (else (cons sofar char-list)))))
               (c (car char-list))
               (r (cdr char-list)))
        (cond ((char=? c #\]) (cons 'lam r))
              ((char=? c #\@) (cons 'app r))
              ((char-numeric? c) (lex-number 0 char-list))
              (else (lexer r))))))

(define (parse-syntax char-list)
  (letrec ((p (lambda (token stack rest)
                (cond 
                 ((eq? token 'lam)
                  (if (null? stack)
                      (error "parse-syntax" "too few arguments for lambda")
                      (q (cons (abstr (car stack)) (cdr stack)) 
                         rest)))
                 ((eq? token 'app)
                  (if (< (length stack) 2)
                      (error "parse-syntax" "too few arguments for app")
                      (q (cons (app (cadr stack)(car stack))
                               (cddr stack))
                         rest)))
                 (else (q (cons (var token) stack) rest)))))
           (q (lambda (stack rest)
                (if (null? rest) 
                    (if (= (length stack) 1)
                        (car stack)
                        (error "parse-syntax" "stack not empty"))
                    (let ((l (lexer rest)))
                      (p (car l) stack (cdr l)))))))
    (q '() char-list)))

(define (pt string)(parse-syntax (explode string)))

;; Semantics 
;; =========
;; Each semantical object is a function of no argument,
;; that evaluates to one of the following:
;; - a pair ('fun . function)
;;   where function is from the semantics into the semantics
;; - a pair ('syn . term)
;;   where term is a term of the abstract syntax

;; down takes an object and returns a representation in the 
;; abstract syntax

(define (make-bv n)
  ;; the correct representation of a variable bound at level n
  (lambda () 
    (cons 'syn (bv n))))

(define (down obj)
  (let ((val (obj)))         ;; inspect the object 
    (if (eq? (car val) 'syn) ;; if it is in the syntax...
        (cdr val)            ;; ...we're done 
        (lambda (n)
          ;; otherwise construct something of the abstract syntax
          ((term-abstr 
            ;; by a syntactical abstraction
            ;; and application to a ``new'' variable
            (down ((cdr val) (make-bv n)))) n)))))

;; sem-app takes two objects and applies them to each other

(define (sem-app obja objb)
  (lambda () ;; we delay
    (let ((obj (obja)))          ;; first inspect ``function argument''
      (if (eq? (car obj) 'fun)   ;; if it is a function...
          (((cdr obj) objb))     ;; ...just call
          ;; otherwise we have some syntax, so transform the argument
          ;; into syntax as well and apply them there
          (let ((term (down objb))) 
            (cons 'syn (term-app (cdr obj) term)))))))

;; evaluation
;; ==========

(define (evaluate syntax valuation)
  (cond ((var? syntax)(lambda () ((valuation (var-nr syntax)))))
        ((abs? syntax)(lambda () (cons 'fun 
                                       (lambda (obj)
                                         (evaluate (abs-body syntax) 
                                                   (dot obj valuation))))))
        ((app? syntax)(lambda ()
                        ((sem-app
                          (evaluate (app-l syntax) valuation)
                          (evaluate (app-r syntax) valuation)))))))
;; NBE
;; ===

(define (identical-valuation n)
  (lambda ()
    (cons 'syn (fv n))))
(define (nbe string)
  (display (syntax-to-string
            ((down(evaluate (pt string) identical-valuation)) 0)
            ))
  (newline))


;; Syntax
;; ======

(define-syntax lam
  ;; abstraction: remember: functions are delayed ones!
  (syntax-rules ()
    ((_ (arg) . body)
     (lambda () (cons 'fun (lambda (arg)  . body))))
    ((_ (arg . args) . body)
     ;; also support implicit currying
     (lam (arg) (lam args . body)))))

(define-syntax !
  ;; application: 
  ;; remember: delayed as well, but don't forget to 
  ;;           undelay the result
  (syntax-rules ()
    ((_ fun  arg)
     (lambda () ((sem-app fun arg))))
    ((_ fun arg . args)
     ;; also support implicit uncurrying
        (! (! fun arg) . args))))


(define (? value)
  (newline)
  (display (syntax-to-string ((down value) 0)))
  (newline))


;; Examples:
;; =========


;; Without variables it's just half the fun!
(define (make-var number)
  (lambda () (cons 'syn (fv number))))

;; Church-style natural numbers
;; ----------------------------
(define ZERO (lam (step base) base))
(define SUC (lam (n step base)
                 (! step (! n step base))))
(define make-nat (lambda (n)
                   (if (= 0 n) ZERO
                       (! SUC (make-nat (- n 1))))))

;; (? (! (make-nat 2) (make-nat 3))) 
;;     --> [[1 1 1 1 1 1 1 1 1 0 @ @ @ @ @ @ @ @ @]]
;; (? (! (make-nat 2) (make-var 42))) --> [43 43 0 @ @]
;; (? (! (make-var 42)(make-nat 2))) --> 42 [[1 1 0 @ @]] @


;; Or, more general stuff:
;; -----------------------
(define S (lam (x y z) (! x z (! y z))))
(define K (lam (x y) x))
(define I (! S K K))         ;; (? I)             --> [0]
(define w (lam (x) (! x x))) ;; (? w)             --> [0 0 @]
(define Omega (! w w)) ;; You can define it, but better don't 
                       ;; look at it via (? ...)
                       ;; However: 
                             ;; (? (! K I Omega)) --> [0]