;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;           __    __        __    __                                        ;;
;;          /  \  /  \      (__)  |  |    ____   ___      __    ____         ;;
;;         /    \/    \      __   |  |   / _  |  \  \ __ /  /  / _  |        ;;
;;        /  /\    /\  \    |  |  |  |  / / | |   \  '  '  /  / / | |        ;;
;;       /  /  \__/  \  \   |  |  |  |  \ \_| |    \  /\  /   \ \_| |        ;;
;;      /__/          \__\  |__|  |__|   \____|     \/  \/     \____|        ;;
;; ~ ~~ \  ~ ~  ~_~~ ~/~ /~ | ~|~ | ~| ~ /~_ ~|~ ~  ~\  ~\~ ~  ~ ~  |~~    ~ ;;
;;  ~ ~  \~ \~ / ~\~ / ~/ ~ |~ | ~|  ~ ~/~/ | |~ ~~/ ~\/ ~~ ~ / / | |~   ~   ;;
;; ~ ~  ~ \ ~\/ ~  \~ ~/ ~~ ~__|  |~ ~  ~ \_~  ~  ~  .__~ ~\ ~\ ~_| ~  ~ ~~  ;;
;;  ~~ ~  ~\  ~ /~ ~  ~ ~  ~ __~  |  ~ ~ \~__~| ~/__~   ~\__~ ~~___~| ~ ~    ;;
;; ~  ~~ ~  \~_/  ~_~/ ~ ~ ~(__~ ~|~_| ~  ~  ~~  ~  ~ ~~    ~  ~   ~~  ~  ~  ;;
;;                                                                           ;;
;;            A   R e f l e c t i v e   P r o o f   C h e c k e r            ;;
;;                                                                           ;;
;;       Copyright (C) 2005-2009 by Jared Davis <jared@cs.utexas.edu>        ;;
;;                                                                           ;;
;; 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 MERCHANTABIL-  ;;
;; ITY 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 (see the file COPYING); if not, write to the Free       ;;
;; Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA    ;;
;; 02110-1301, USA.                                                          ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; cl-prelude.lisp
;   - only needed on Common Lisp systems (not on Jitawa)
;   - sets up the MILAWA:: package and its

(in-package "CL-USER")
(declaim (optimize (speed 3)))

#+clozure
(progn
  (setq ccl::*default-control-stack-size* (expt 2 27))
  (setq ccl::*default-value-stack-size* (expt 2 27))
  (setq ccl::*default-temp-stack-size* (expt 2 27))
  (setq ccl::*initial-listener-default-value-stack-size* (expt 2 27))
  (setq ccl::*initial-listener-default-control-stack-size* (expt 2 27))
  (setq ccl::*initial-listener-default-temp-stack-size* (expt 2 27))
  (CCL::egc nil)
  (CCL::set-lisp-heap-gc-threshold (expt 2 34))
  (CCL::gc-verbose t t))

#+cmucl
(progn
  (setq extensions:*bytes-consed-between-gcs* (expt 2 29)))

#+sbcl
(progn
  ;; SBCL on linux-32 complains about 2^29 being just slightly too big.
  ;; In the original Milawa, I set this to:
  ;;    (setf (sb-ext:bytes-consed-between-gcs) (- (expt 2 29) 10)))
  ;; For my 64-bit tests against Jitawa, this is as high as I can set it:
  (setf (sb-ext:bytes-consed-between-gcs) (1- (expt 2 32))))

(defmacro defun-comp (&rest args)
  `(compile (defun ,@args)))

(defpackage "MILAWA" (:use))

(import '(COMMON-LISP::nil
          COMMON-LISP::t
          COMMON-LISP::quote
          COMMON-LISP::if
          COMMON-LISP::equal
          COMMON-LISP::consp
          COMMON-LISP::cons
          COMMON-LISP::symbolp
          COMMON-LISP::let
          COMMON-LISP::let*
          COMMON-LISP::list
          COMMON-LISP::and
          COMMON-LISP::or
          COMMON-LISP::cond
          COMMON-LISP::lambda)
        "MILAWA")

(declaim (inline MILAWA::natp
                 MILAWA::symbol-<
                 MILAWA::<
                 MILAWA::+
                 MILAWA::-
                 MILAWA::car
                 MILAWA::cdr))

(defun-comp MILAWA::natp (x)
  (integerp x))

(defun-comp MILAWA::symbol-< (x y)
  (let ((x-fix (if (symbolp x) x nil))
        (y-fix (if (symbolp y) y nil)))
    (if (string< (symbol-name x-fix) (symbol-name y-fix))
        t
      nil)))

(defun-comp MILAWA::< (x y)
  (let ((x-fix (if (integerp x) x 0))
        (y-fix (if (integerp y) y 0)))
    (< (the integer x-fix)
       (the integer y-fix))))

(defun-comp MILAWA::+ (x y)
  (let* ((x-fix (if (integerp x) x 0))
         (y-fix (if (integerp y) y 0))
         (ret   (+ (the integer x-fix)
                   (the integer y-fix))))
    ret))

(defun-comp MILAWA::- (x y)
  (let* ((x-fix (if (integerp x) x 0))
         (y-fix (if (integerp y) y 0))
         (ans   (- (the integer x-fix)
                   (the integer y-fix))))
    (if (< (the integer ans) 0)
        0
      ans)))

(defun-comp MILAWA::car (x)
  (if (consp x) (car x) nil))

(defun-comp MILAWA::cdr (x)
  (if (consp x) (cdr x) nil))

(defmacro MILAWA::first  (x) `(MILAWA::car ,x))
(defmacro MILAWA::second (x) `(MILAWA::first  (MILAWA::cdr ,x)))
(defmacro MILAWA::third  (x) `(MILAWA::second (MILAWA::cdr ,x)))
(defmacro MILAWA::fourth (x) `(MILAWA::third  (MILAWA::cdr ,x)))
(defmacro MILAWA::fifth  (x) `(MILAWA::fourth (MILAWA::cdr ,x)))


; SAFE DEFINITION MECHANISM

(defun-comp MILAWA::define (name formals body)
  ;; Define a function in Raw Lisp.
  (eval `(compile (defun ,name ,formals
                    (declare (ignorable ,@formals)
                             (optimize (speed 3)))
                    ,body))))

(defun-comp MILAWA::error (description)
  ;; Abort execution with a run-time error
  (error "Milawa::error called: ~a" description)
  (quit))

(defun-comp MILAWA::print (obj)
  (format t "~a~%" obj)
  (finish-output)
  nil)

(defmacro MILAWA::funcall (&rest args)
  `(CL-USER::funcall . ,args))

(in-package "MILAWA")