Re: CC Machine in Scheme

dvanhorn wrote:
>    The CC Machine -- an ISWIM interpreter

That last version had bug in substitute.  Here's a fixed version.  Relicensed.
 Written as a module.  Simplified state transitions.  Latest version at:

   http://www.cs.uvm.edu/~dvanhorn/scheme/cc.ss

-d


#|                                                              -*- Scheme -*-
    Copyright (c) 2003 David Van Horn
    Licensed under the Academic Free License version 2.0

    The CC Machine -- an ISWIM interpreter
    [email protected]

    The specification of this eval-cc function comes from Felleisen & Flatt --
    Programming Languages and Lambda Calculi.

    See http://www.cs.uvm.edu/~dvanhorn/ocaml/cc.ml for an OCaml version of
    this machine.
|#

(module cc mzscheme
  (provide eval-cc)
  (require (lib "match.ss"))

  ;; span : ('a -> bool) * 'a list -> ('a list 'a list)

  ;; Span splits the list into the longest initial prefix whose elements all
  ;; satisfy the predicate f, and the remaining tail. Cf. SRFI-1.

  (define (span f ls)
    (letrec ((recur (match-lambda
                     [() '(() ())]
                     [(x . rest)
                      (if (f x)
                          (match-let ([(prefix suffix) (recur rest)])
                                     (list (cons x prefix) suffix))
                          (list '() (cons x rest)))])))
      (recur ls)))

  ;; delta : primop * term list -> term

  (define (delta op args)
    (match args
      [(('value ('base ('int x))) . rest)
       (let* ((y
               (match rest
                 [(('value ('base ('int y)))) y]
                 [() 1]))
              (result
               (match op
                 [(or 'add1  'plus) (+ x y)]
                 [(or 'sub1 'minus)
                  (let ((sum (- x y)))
                    (if (<= sum 0) 0 sum))])))
         `(value (base (int ,result))))]))

  (define value?
    (match-lambda
     [('value v) #t]
     [_  #f]))

  (define base?
    (match-lambda
     [('value ('base b)) #t]
     [_ #f]))

  ;; gen-var : unit -> string

  ;; Returns a fresh variable name of the form "zn" where n is an integer (so
  ;; don't use variables of this form!).

  (define gen-var
    (let ((i 0))
      (lambda ()
        (set! i (add1 i))
        (string-append "z" (number->string i)))))

  ;; substitute : term * var * value -> term

  ;; Substitutes v for x in m.

  (define (substitute m x v)
    (match m
      [('value ('base b)) `(value (base ,b))]
      [('value ('var y))
       (if (equal? x y)
           `(value ,v)
           `(value (var ,y)))]
      [('value ('lambda (y n)))
       (if (equal? x y)
           `(value (lambda (,y ,n)))
           (let* ((z (gen-var))
                  (m (substitute (substitute n y `(var ,z)) x v)))
             `(value (lambda (,z ,m)))))]
      [('app n p)
       `(app ,(substitute n x v) ,(substitute p x v))]
      [('app-prim o . tlist)
       `(app-prim ,o ,@(map (lambda (t) (substitute t x v)) tlist))]))

  ;; cc : (term context) -> (term context)

  ;;   The machine state transition function.

  (define cc
    (match-lambda
     [(('app m n) e)
      (=> fail)
      (when (value? m) (fail))
      `(,m (c-in-hole ,e (c-app-e c-empty-hole ,n)))]
     [(('app ('value v) m) e)
      (=> fail)
      (when (value? m) (fail))
      `(,m (c-in-hole ,e (c-app-v ,v c-empty-hole)))]
     [(('app-prim o . args) e)
      (=> fail)
      (unless (andmap base? args) (fail))
      `(,(delta o args) ,e)]
     [(('app-prim o . args) e)
      (match-let (((vlist (m . tlist)) (span value? args)))
        (let ((vlist (map (match-lambda [('value v) v]) vlist)))
          `(,m (c-in-hole ,e (c-app-prim ,o ,vlist c-empty-hole ,tlist)))))]
     [(('app ('value ('lambda x m)) ('value v)) e)
      `(,(substitute m x v) ,e)]
     [(('value v) ('c-in-hole e ('c-app-v u 'c-empty-hole)))
      `((app (value ,u) (value ,v)) ,e)]
     [(('value v) ('c-in-hole e ('c-app-e 'c-empty-hole n)))
      `((app (value ,v) ,n) ,e)]
     [(('value v) ('c-in-hole e ('c-app-prim o vlist 'c-empty-hole tlist)))
      (let ((vlist (map (lambda (x) `(value ,x)) vlist)))
        `((app-prim ,o ,@vlist (value ,v) ,@tlist) ,e))]))

  ;; Simplified version of state transitions.

  (define cc
    (match-lambda
     [(('app m n) e)
      `(,m (c-in-hole ,e (c-app-e c-empty-hole ,n)))]
     [(('app-prim o m . tlist) e)
      `(,m (c-in-hole ,e (c-app-prim ,o () c-empty-hole ,tlist)))]
     [(('value v) ('c-in-hole e ('c-app-v ('lambda x m) 'c-empty-hole)))
      `(,(substitute m x v) ,e)]
     [(('value v) ('c-in-hole e ('c-app-e 'c-empty-hole n)))
      `(,n (c-in-hole ,e (c-app-v ,v c-empty-hole)))]
     [(('value v) ('c-in-hole e ('c-app-prim o blist 'c-empty-hole ())))
      (=> fail)
      (unless (base? `(value ,v)) (fail))
      `(,(delta o `(,@blist (value ,v))) ,e)]
     [(('value v)
       ('c-in-hole e ('c-app-prim o blist 'c-empty-hole (n . tlist))))
      `(,n (c-in-hole ,e (c-app-prim ,o (,@blist ,v) c-empty-hole ,tlist)))]))

  ;;   eval-cc : term -> result

  (define (eval-cc term)
    (letrec ((loop (match-lambda
                    [(('value ('base b)) 'c-empty-hole)
                     `(result ,b)]
                    [(('value ('lambda x m)) 'c-empty-hole) 'function]
                    [(term context) (loop (cc `(,term ,context)))])))
      (loop `(,term c-empty-hole))))

  (define (test-eval-cc)

    ;; Useful to see how evaluation proceeds.
    ;;(require (lib "trace.ss"))
    ;;(trace cc)

    (define-syntax assert
      (syntax-rules ()
        [(_ term expected-result)
         (let ((calculated-result (eval-cc 'term)))
           (unless (equal? calculated-result 'expected-result)
             (error
              (format "~a --exp--> ~a~n~a --got--> ~a"
                      'term 'expected-result
                      'term calculated-result))))]))

    (assert
     (app-prim add1 (value (base (int 1))))
     (result (int 2)))

    (assert
     (app (value (lambda "x" (value (var "x"))))
          (app (value (lambda "x" (value (var "x"))))
               (value (base (int 5)))))
     (result (int 5)))

    (assert
     (app (value (lambda "x" (app-prim add1 (value (var "x")))))
          (app (value (lambda "x" (value (var "x"))))
               (value (base (int 5)))))
     (result (int 6)))

    (assert
     (app (value (lambda "x" (app-prim add1 (value (var "x")))))
          (value (base (int 1))))
     (result (int 2)))

    (assert
     (app (value (lambda "x" (value (base (int 9)))))
          (value (base (int 3))))
     (result (int 9)))

    #t) ;; passed test-eval-cc

  ) ;; end module cc