;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;           __    __        __    __                                        ;;
;;          /  \  /  \      (__)  |  |    ____   ___      __    ____         ;;
;;         /    \/    \      __   |  |   / _  |  \  \ __ /  /  / _  |        ;;
;;        /  /\    /\  \    |  |  |  |  / / | |   \  '  '  /  / / | |        ;;
;;       /  /  \__/  \  \   |  |  |  |  \ \_| |    \  /\  /   \ \_| |        ;;
;;      /__/          \__\  |__|  |__|   \____|     \/  \/     \____|        ;;
;; ~ ~~ \  ~ ~  ~_~~ ~/~ /~ | ~|~ | ~| ~ /~_ ~|~ ~  ~\  ~\~ ~  ~ ~  |~~    ~ ;;
;;  ~ ~  \~ \~ / ~\~ / ~/ ~ |~ | ~|  ~ ~/~/ | |~ ~~/ ~\/ ~~ ~ / / | |~   ~   ;;
;; ~ ~  ~ \ ~\/ ~  \~ ~/ ~~ ~__|  |~ ~  ~ \_~  ~  ~  .__~ ~\ ~\ ~_| ~  ~ ~~  ;;
;;  ~~ ~  ~\  ~ /~ ~  ~ ~  ~ __~  |  ~ ~ \~__~| ~/__~   ~\__~ ~~___~| ~ ~    ;;
;; ~  ~~ ~  \~_/  ~_~/ ~ ~ ~(__~ ~|~_| ~  ~  ~~  ~  ~ ~~    ~  ~   ~~  ~  ~  ;;
;;                                                                           ;;
;;            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-run.lisp (only needed on Common Lisp systems, not on Jitawa)
;   - loads the prelude (which defines milawa primitives)
;   - loads the core
;   - defines file reading stuff and acceptable-object checking

(in-package "CL-USER")
(load "cl-prelude.lisp")

(in-package "MILAWA")

(CL-USER::load "core.lisp")

(CL-USER::in-package "CL-USER")

(defun maybe-gc ()
  #+clozure (ccl::gc)
  #+sbcl (sb-ext:gc :full t)
  nil)

; READING THE PROOF FILE

(defun-comp aux-acceptable-objectp (x cache)
  (or (and (integerp x)
           (<= 0 x))
      (and (symbolp x)
           (eq x (intern (symbol-name x) "MILAWA")))
      (and (consp x)
           (let ((status (gethash x cache)))
             (cond ((eq status t)
                    t)
                   ((eq status nil)
                    (progn (setf (gethash x cache) 'exploring)
                           (and (aux-acceptable-objectp (car x) cache)
                                (aux-acceptable-objectp (cdr x) cache)
                                (setf (gethash x cache) t))))
                   (t
                    nil))))))

(defconstant rough-number-of-unique-conses-in-proofs 525000000)

(defun-comp acceptable-objectp (x)
  (format t "Checking acceptable-objectp.~%")
  (finish-output)
  (let* ((size  (ceiling (* 1.10 rough-number-of-unique-conses-in-proofs)))
         (cache (make-hash-table :size size :test 'eq)))
    (aux-acceptable-objectp x cache)))

(defvar *milawa-readtable* (copy-readtable *readtable*))
(declaim (readtable *milawa-readtable*))

(defvar *milawa-abbreviations-hash-table*)
(declaim (type hash-table *milawa-abbreviations-hash-table*))

(defun-comp milawa-sharp-equal-reader (stream subchar arg)
  (declare (ignore subchar))
  (multiple-value-bind
   (value presentp)
   (gethash arg *milawa-abbreviations-hash-table*)
   (declare (ignore value))
   (when presentp
     (error "#~A= is already defined." arg))
   (let ((object (read stream)))
     (setf (gethash arg *milawa-abbreviations-hash-table*) object))))

(defun-comp milawa-sharp-sharp-reader (stream subchar arg)
  (declare (ignore stream subchar))
  (or (gethash arg *milawa-abbreviations-hash-table*)
      (error "#~A# used but not defined." arg)))

(let ((*readtable* *milawa-readtable*))
  (set-dispatch-macro-character #\# #\# #'milawa-sharp-sharp-reader)
  (set-dispatch-macro-character #\# #\= #'milawa-sharp-equal-reader))

(defconstant unique-cons-for-eof (cons 'unique-cons 'for-eof))

(defun-comp milawa-read-file-loop (stream)
   (let ((obj (read stream nil unique-cons-for-eof)))
     (cond ((eq obj unique-cons-for-eof)
            nil)
           (t
            (cons obj (milawa-read-file-loop stream))))))

(defun-comp milawa-read-file-aux (filename)
  (let* ((size (ceiling (* 1.10 rough-number-of-unique-conses-in-proofs)))
         (*milawa-abbreviations-hash-table*
          (make-hash-table :size size :test 'eql))
         (*readtable* *milawa-readtable*)
         (*package* (find-package "MILAWA"))
         (stream (open filename
                       :direction :input
                       :if-does-not-exist :error))
         (contents (time (milawa-read-file-loop stream))))
    (close stream)
    contents))

(defun-comp milawa-read-file (filename)
  (format t ";; Reading from ~A~%" filename)
  (finish-output)
  (let ((contents (milawa-read-file-aux filename)))
    (maybe-gc)
    (format t ";; Checking acceptable-objectp.~%")
    (finish-output)
    (unless (time (acceptable-objectp contents))
      (error "unacceptable object encountered"))
    (maybe-gc)
    contents))