; The M0 Virtual Machine
; Copyright (C) 2004  J Strother Moore,
;               University of Texas at Austin

; This program is free software; you can redistribute it and/or 
; modify it under the terms of the GNU General Public License as
; published by the Free Software Foundation; either version 2 of
; the License, or (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free 
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
; USA.

; Written by: J Strother Moore
; email:      Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.

; Modified by: John Cowles
; email:       cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.
;==============================================================
; This file is a certified book that contains the definition of 
; m0.

; Instructions

; To certify this book, make sure it is on a directory on which 
; you have write permission, fire up ACL2 while connected to that
; directory, and then execute the following two events.

#|
(defpkg "M0"
  (set-difference-equal
   (union-eq '(ASSOC-EQUAL LEN NTH ZP SYNTAXP
                           QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<)
             (union-eq *acl2-exports*
                       *common-lisp-symbols-from-main-lisp-package*))
   '(PC PROGRAM PUSH POP REVERSE STEP ++)))

(certify-book "m0" 1)
|#

(in-package "M0")

; ----------------------------------------------------------------
; Utilities

(defun push (obj stack) (cons obj stack))
(defun top (stack) (car stack))
(defun pop (stack) (cdr stack))

(defun bound? (x alist) (assoc-equal x alist))

(defun bind (x y alist)
  (cond ((endp alist) (list (cons x y)))
        ((equal x (car (car alist)))
         (cons (cons x y) (cdr alist)))
        (t (cons (car alist) (bind x y (cdr alist))))))

(defun binding (x alist) (cdr (assoc-equal x alist)))

(defun op-code (inst) (car inst))
(defun arg1 (inst) (car (cdr inst)))
(defun arg2 (inst) (car (cdr (cdr inst))))
(defun arg3 (inst) (car (cdr (cdr (cdr inst)))))

; The Core of M0

(defun make-state (pc locals stack program)
  (list pc locals stack program))
(defun pc (s) (car s))
(defun locals (s) (cadr s))
(defun stack (s) (caddr s))
(defun program (s) (cadddr s))
(defun next-inst (s) (nth (pc s) (program s)))

(defun suppliedp (key args)
  (cond ((endp args) nil)
        ((equal key (car args)) t)
        (t (suppliedp key (cdr args)))))

(defun actual (key args)
  (cond ((endp args) nil)
        ((equal key (car args)) (cadr args))
        (t (actual key (cdr args)))))

(defmacro modify (s &rest args)
  (list 'make-state
        (if (suppliedp :pc args)
            (actual :pc args)
          (list 'pc s))
        (if (suppliedp :locals args)
            (actual :locals args)
          (list 'locals s))
        (if (suppliedp :stack args)
            (actual :stack args)
          (list 'stack s))
        (if (suppliedp :program args)
            (actual :program args)
          (list 'program s))))

; We now informally specify and then define each m0 instruction.

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (PUSH c)
; Push the constant c onto the operand stack.

(defun execute-PUSH (inst s)
  (modify s
          :pc (+ 1 (pc s))
          :stack (push (arg1 inst) (stack s))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
; Informal Spec: (POP)
; Pop the top item off the operand stack and discard it.

(defun execute-POP (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc s))
          :stack (pop (stack s))))

; Note: When you define an ACL2 function that ignores one of its
; arguments you must declare that you are doing it intentionally.
; That is the purpose of the DECLARE form above.  Why does 
; execute-POP ignore inst?  The reason is that, by convention 
; here, we know that inst is an instruction whose opcode is POP.
; Since the POP instruction contains no additional fields, there 
; is nothing else we need from it.

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (LOAD v)
; Push the contents stored in local variable v onto the operand 
; stack.

(defun execute-LOAD (inst s)
  (modify s
          :pc (+ 1 (pc s))
          :stack (push (binding (arg1 inst)
                                (locals s))
                       (stack s))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (STORE v)
; Pop the top item off the operand stack and store it into the
; local variable v.

(defun execute-STORE (inst s)
  (modify s
          :pc (+ 1 (pc s))
          :locals (bind (arg1 inst) (top (stack s)) (locals s))
          :stack (pop (stack s))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
; Informal Spec: (DUP)
; Duplicate the top item on the stack.

(defun execute-DUP (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc s))
          :stack (push (top (stack s)) (stack s))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (ADD)
; Pop the top two items off the stack and push their sum.

(defun execute-ADD (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc s))
          :stack (push (+ (top (pop (stack s)))
                          (top (stack s)))
                       (pop (pop (stack s))))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (SUB)
; Pop the top two items off the stack and push their difference.
; (The top item should be subtracted from the one below it.)

(defun execute-SUB (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc s))
          :stack (push (- (top (pop (stack s)))
                          (top (stack s)))
                       (pop (pop (stack s))))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (MUL)
; Pop the top two items off the stack and push their product.

(defun execute-MUL (inst s)
  (declare (ignore inst))
  (modify s
          :pc (+ 1 (pc s))
          :stack (push (* (top (pop (stack s)))
                          (top (stack s)))
                       (pop (pop (stack s))))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (GOTO delta)
; Jump to the instruction delta steps from the current 
; instruction.

(defun execute-GOTO (inst s)
  (modify s
          :pc (+ (arg1 inst) (pc s))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (IFEQ delta)
; Pop the top item off the stack and if it is 0, jump to the 
; instruction delta steps from the current instruction; otherwise,
; step to the next instruction.

(defun execute-IFEQ (inst s)
  (modify s
          :pc (if (equal (top (stack s)) 0)
                  (+ (arg1 inst) (pc s))
                (+ 1 (pc s)))
          :stack (pop (stack s))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (IFNE delta)
; Pop the top item off the stack and if it is not 0, jump to the
; instruction delta steps from the current instruction; otherwise,
; step to the next instruction.;

(defun execute-IFNE (inst s)
  (modify s
          :pc (if (equal (top (stack s)) 0)
                  (+ 1 (pc s))
                (+ (arg1 inst) (pc s)))
          :stack (pop (stack s))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
; Informal Spec: (IFGT delta)
; Pop the top item off the stack and if it is greater than 0, jump
; to the instruction delta steps from the current instruction;
; otherwise, step to the next instruction.;

(defun execute-IFGT (inst s)
  (modify s
          :pc (if (> (top (stack s)) 0)
                  (+ (arg1 inst) (pc s))
                (+ 1 (pc s)))
          :stack (pop (stack s))))

; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
; Informal Spec: (IFLE delta)
; Pop the top item off the stack and if it is less than or equal
; to 0, jump to the instruction delta steps from the current 
; instruction; otherwise, step to the next instruction.;

(defun execute-IFLE (inst s)
  (modify s
          :pc (if (> (top (stack s)) 0)
		  (+ 1 (pc s))
		(+ (arg1 inst) (pc s)))
          :stack (pop (stack s))))

; --------------------------------------------------------------

; Now we wrap it all up by defining the m0 step function and the
; top-level interpreter.

(defun do-inst (inst s)
  (case (op-code inst)
    (PUSH   (execute-PUSH  inst s))
    (POP    (execute-POP   inst s))
    (LOAD   (execute-LOAD  inst s))
    (STORE  (execute-STORE inst s))
    (DUP    (execute-DUP   inst s))
    (ADD    (execute-ADD   inst s))
    (SUB    (execute-SUB   inst s))
    (MUL    (execute-MUL   inst s))
    (GOTO   (execute-GOTO  inst s))
    (IFEQ   (execute-IFEQ  inst s))
    (IFNE   (execute-IFNE  inst s))
    (IFGT   (execute-IFGT  inst s))
    (IFLE   (execute-IFLE  inst s)) 
    (otherwise s)))

; Notice that there is no instruction with op-code HALT.  But what
; is (do-inst '(HALT) s)?  The answer: s!  That is, every 
; undefined op-code is a no-op, and a no-op is the same as a halt
; instruction in the sense that execution never gets past it.

(defun step (s)
  (do-inst (next-inst s) s))

; So here is the operational semantics for the m0 virtual machine.

(defun run (s n)
  (if (zp n)
      s
      (run (step s) (- n 1))))