CORE DENOTATIONAL SEMANTICS CODED IN LISP
                             -----------------------------------------


          Script started on Thu Sep 29 11:12:24 1994

          vestavia% cat coreds.lsp
          (defun Msem (S file1) (prog (newstore)
              (setq newstore '(lambda (V) (cond (t 'bottom))))
              (return (caddr (Ssem S (list newstore file1 nil))))))

          (defun Ssem (S conf)
              (cond
                  ((eq (car S) ':) (prog (S1 S2)
                      (setq S1 (cadr S))
                      (setq S2 (caddr S))
                      (return (Ssem S2 (Ssem S1 conf)))))
                  ((eq (car S) ':=) (prog (V E store file1 file2)
                      (setq V (cadr S))
                      (setq E (caddr S))
                      (setq store (car conf))
                      (setq file1 (cadr conf))
                      (setq file2 (caddr conf))
                      (return (list (update store V (Esem E store)) file1 file2))))
                  ((eq (car S) 'while-loop) (prog (C S1)
                      (setq C (cadr S))
                      (setq S1 (caddr S))
                      (cond
                          ((Csem C (car conf)) (return (Ssem S (Ssem S1 conf))))
                          (t (return conf)))))
                  ((eq (car S) 'if-then) (prog (C S1)
                      (setq C (cadr S))
                      (setq S1 (caddr S))
                      (cond
                          ((Csem C (car conf)) (return (Ssem S1 conf)))
                          (t (return conf)))))
                  ((eq (car S) 'if-then-else) (prog (C S1 S2)
                      (setq C (cadr S))
                      (setq S1 (caddr S))
                      (setq S2 (cadddr S))
                      (cond
                          ((Csem C (car conf)) (return (Ssem S1 conf)))
                          (t (return (Ssem S2 conf))))))
                  ((eq (car S) 'input) (prog (V store file1 file2)
                      (setq V (cadr S))
                      (setq store (car conf))
                      (setq file1 (cadr conf))
                      (setq file2 (caddr conf))
                      (cond
                          ((eq file1 'nil) (return 'top))
                          (t (return 
                              (list (update store V (hd file1)) (tl file1) file2))))))
                  ((eq (car S) 'output) (prog (V store file1 file2 n)
                      (setq V (cadr S))
                      (setq store (car conf))
                      (setq file1 (cadr conf))
                      (setq file2 (caddr conf))
                      (setq n (access store V))
                      (cond
                          ((eq n 'bottom) (return 'top))
                          (t (return (list store file1 (append file2 (list n))))))))))







          (defun Csem (C store) (prog (R E1 E2)
              (setq R (car C))
              (setq E1 (cadr C))
              (setq E2 (caddr C))
              (cond
                  ((eq R '<) (return (< (Esem E1 store) (Esem E2 store))))
                  ((eq R '<=) (return (not (> (Esem E1 store) (Esem E2 store)))))
                  ((eq R '=) (return (= (Esem E1 store) (Esem E2 store))))
                  ((eq R '<>) (return (not (= (Esem E1 store) (Esem E2 store)))))
                  ((eq R '>=) (return (not (< (Esem E1 store) (Esem E2 store)))))
                  ((eq R '>) (return (> (Esem E1 store) (Esem E2 store)))))))

          (defun Esem (E store)
              (cond
                  ((listp E) (prog (O E1 E2)
                      (setq O (car E))
                      (setq E1 (cadr E))
                      (setq E2 (caddr E))
                      (cond
                          ((eq O '+) (return (+ (Esem E1 store) (Esem E2 store))))
                          ((eq O '-) (return (- (Esem E1 store) (Esem E2 store))))
                          ((eq O '*) (return (* (Esem E1 store) (Esem E2 store)))))))
                  ((numberp E) E)
                  (t (prog (V n)
                      (setq V E)
                      (setq n (access store V))
                      (cond
                          ((eq n 'bottom) (return 'top))
                          (t (return n)))))))

          (defun access (store V) (apply store (list V)))

          (defun update (store V n) (prog (currentenv newbinding newstore)
              (setq currentenv (cdar (cddr store)))
              (setq newbinding (cons (list 'eq 'V (list 'quote V)) (list N)))
              (setq newstore
                  (list 'lambda (list 'V) (cons 'cond (cons newbinding currentenv))))
              (return newstore))))

          (defun hd (list) (car list))

          (defun tl (list) (cdr list))

          vestavia% cat quotrem.core
          input x; input y;
          q := 0; r := x;
          while (r >= y) loop
              q := q + 1;
              r := r - y
          end;
          output q; output r;














          vestavia% kcl
          AKCL (Austin Kyoto Common Lisp)  Version(1.615) Fri Jan  8 13:26:25 CST 1993
          Contains Enhancements by W. Schelter
          Loading init.lsp
          Finished loading init.lsp

          >(load "coreds")
          Loading coreds.lsp
          Finished loading coreds.lsp
          T

          >(Msem 
              '(: 
                 (: 
                   (: 
                     (: 
                       (: 
                         (: 
                           (input x) 
                           (input y)) 
                         (:= q 0)) 
                       (:= r x)) 
                     (while-loop 
                       (>= r y) 
                       (: 
                         (:= q (+ q 1)) 
                         (:= r (- r y))))) 
                   (output q)) 
                 (output r)) 
              '(32 5))
          (6 2)

          >Bye.

          vestavia% ^D
          script done on Thu Sep 29 11:14:50 1994