(in-package :pvs)

(pvs-message "Loading .pvsio.lisp")

;--- Patch:  src/PVSio/pvs-lib.lisp
(defparameter *pvsio-version* "PVSio-4.a (11/07/07)")
;--- End Path: src/PVSio/pvs-lib.lisp

;--- Patch:  src/PVSio/pvsio.lisp
(defun help-pvsio ()
  (format 
   t 
   "~%Enter a PVS ground expression followed by ';' at the <PVSio> prompt")
  (format t "~%  OR ")
  (format 
   t 
   "~%Enter a Lisp expression followed by a '!' at the <PVSio> prompt~%")
  (format t "~%The following special commands can be followed by either ';' or '!':
  help                 : Print this message
  quit                 : Exit the evaluator with confirmation
  exit                 : Exit the evaluator without confirmation
  timing               : Turn on timing information per evaluation
  notiming             : Turn off timing information
  tccs                 : Turn on TCCs generation per evaluation 
  notccs               : Turn off TCCs generation
  load_pvs_attachments : Force a reload .pvs-attachments and pvs-attachments
  pvsio_version        : Show current version of PVSio
  list_attachments     : List semantic attachments loaded in the current 
                         context

Display help for <attachment>:
  (help_pvs_attachment <attachment>)!
  help_pvs_attachment(<attachment>);

Display help for semantic attachments in <theory>:
  (help_pvs_theory_attachments <theory>)!
  help_pvs_theory_attachments(<theory>);

ACKNOWLEDGMENT
PVS is a software developed, maintained, and licensed by SRI International.
PVSio is a freely available extension to the PVS Ground Evaluator developed 
by Cesar Munoz at the National Institute of Aerospace.

"))

(defun evaluation-mode-pvsio (theoryname 
			      &optional input tccs?  
			      append? (banner? t))
  (load-pvsio-library-if-needed)
  (let ((theory (get-typechecked-theory theoryname)))
    (format t "~%Generating ~a.log~%" theoryname)
    (with-open-file 
	(*error-output*
	 (merge-pathnames (format nil "~a.log" theoryname))
	 :direction :output 
	 :if-does-not-exist :create
	 :if-exists (if append? :append :supersede))
      (unwind-protect
	  (if theory
	      (let ((*current-theory* theory)
		    (*generate-tccs* (if tccs? 'all 'none))
		    (*current-context* (or (saved-context theory)
					   (context nil)))
		    (*suppress-msg* t)
		    (*in-evaluator* t)
		    (*destructive?* t)
		    (*eval-verbose* nil)
		    (*compile-verbose* nil)
		    (*convert-back-to-pvs* t)
		    (input-stream (when input 
				    (make-string-input-stream input))))
		(when banner?
		  (format t "
+---- 
| ~a
|
| Enter a PVS ground expression followed by a symbol ';' at the <PVSio> prompt.
| Enter a Lisp expression followed by a symbol '!' at the <PVSio> prompt.
|
| Enter help! for a list of commands and quit! to exit the evaluator.
|
| *CAVEAT*: evaluation of expressions which depend on unproven TCCs may be 
| unsound, and result in the evaluator crashing into lisp, running out of 
| stack, or worse. If you crash into lisp, type (restore) to resume.
|
+----~%" *pvsio-version*))
		(evaluate-pvsio input-stream))
	      (pvs-message "Theory ~a is not typechecked" theoryname))
	(pvs-emacs-eval "(pvs-evaluator-ready)")))))

(defun read-pvsio (input-stream)
  (when (not input-stream)
    (format t "~%<PVSio> ")
    (force-output))
  (let ((input ;;(ignore-errors (read-expr input-stream))
	       (read-expr input-stream)))
    (cond ((member input '(quit (quit) "quit") :test #'equal)
	   (clear-input)
	   (when (pvs-y-or-n-p "Do you really want to quit?  ")
	     (throw 'quit nil))
	   (read-pvsio input-stream))
	  ((member input '(exit (exit) "exit") :test #'equal)
	   (throw 'quit nil))
	  ((member input '(help "help") :test #'equal)
	   (help-pvsio)
	   (read-pvsio input-stream))
	  ((member input '(timing "timing") :test #'equal)
	   (setq *pvs-eval-do-timing* t)
	   (format t "Enabled printing of timing information~%")
	   (read-pvsio input-stream))
	  ((member input '(notiming "notiming") :test #'equal)
	   (setq *pvs-eval-do-timing* nil)
	   (format t "Disabled printing of timing information~%")
	   (read-pvsio input-stream))
	  ((member input '(tccs "tccs") :test #'equal)
	   (setq *generate-tccs* 'all)
	   (format t "Enabled TCCs generation~%")
	   (read-pvsio input-stream))
	  ((member input '(notccs "notccs") :test #'equal)
	   (setq *generate-tccs* 'none)
	   (format t "Disabled TCCs generation~%")
	   (read-pvsio input-stream))
          ((member input '(pvsio-version pvsio_version "pvsio_version") 
		   :test #'equal)
	   (format t "~a~%" *pvsio-version*)
	   (read-pvsio input-stream))
	  ((member input '(list-attachments list_attachments 
					    "list_attachments") 
		   :test #'equal)
	   (list-attachments)
	   (read-pvsio input-stream))
	  ((member input '(load-pvs-attachments load_pvs_attachments 
						"load_pvs_attachments") 
		   :test #'equal)
	   (load-pvs-attachments t)
	   (read-pvsio input-stream))
	  ((stringp input) input)
	  (t (format t "~a" (eval input))
	     (fresh-line)
	     (read-pvsio input-stream)))))
;--- End Patch:  src/PVSio/pvsio.lisp

;--- Patch:  src/groundeval/pvseval-update.lisp 			   
(defun subrange-index (type)
  (let ((below (simple-below? type)))
    (if below
	(list 0 (if (number-expr? below)
		    (1- (number below))
		    '*))
	(let ((upto (simple-upto? type)))
	  (or (and upto (if (number-expr? upto)
			    (list 0 (number upto))
			    (list 0 '*)))
	      (let ((x (simple-subrange? type)))
		(when x
		  (let ((lo (if (number-expr? (car x))
				(number (car x))
			      '*))
			(hi (if (number-expr? (cdr x))
				(number (cdr x))
			      '*)))
		    (list lo hi)))))))))

(defun simple-upto? (type)
  (when (and (subtype? type)
	     (tc-eq (type (predicate type))
		    (type (predicate (upto-subtype)))))
    (let* ((bindings (make-empty-bindings (free-params (upto-subtype))))
	   (subst (tc-match type (upto-subtype) bindings)))
      (cdr (assoc '|m| subst :test #'same-id)))))

;--- End Patch:  src/groundeval/pvseval-update.lisp