Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
patch-106.lisp
Sprache: Unknown
;;
;; pvsio.lisp
;; Release: PVSio-6.0.9 (3/14/14)
;;
;; Contact: Cesar Munoz ([email protected])
;; NASA Langley Research Center
;; http://shemesh.larc.nasa.gov/people/cam/PVSio
;;
;; Copyright (c) 2011-2012 United States Government as represented by
;; the National Aeronautics and Space Administration. No copyright
;; is claimed in the United States under Title 17, U.S.Code. All Other
;; Rights Reserved.
;;
;; PVSio interface to the ground evaluator
;;
(in-package :pvs)
(defparameter *pvsio-promptin* " ")
(defparameter *pvsio-promptout* "==>~%")
(defun help-pvsio ()
(format
t
"~%Enter a PVS ground expression followed by ';' at the prompt '~a'" *pvsio-promptin*)
(format t "~% OR ")
(format
t
"~%Enter a Lisp expression followed by '!' at the prompt '~a'~%" *pvsio-promptin*)
(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
list_pvs_attachments : List semantic attachments loaded in the current
context
pvsio_version : Show current version of PVSio
To display help for <attachment>:
help_pvs_attachment(\"\");
To display help for semantic attachments in <theory>:
help_pvs_theory_attachments(\"\");
To change input prompt '~a':
set_promptin(\"\");
To change output prompt '~a':
set_promptout(\"\");
" *pvsio-promptin* *pvsio-promptout*))
(defun evaluation-mode-pvsio (theoryname &optional input tccs? (banner? t))
(let ((theory (get-typechecked-theory theoryname)))
(when theory
(with-open-file
(*error-output*
(merge-pathnames (format nil "~a.log" theoryname))
:direction :output
:if-does-not-exist :create
:if-exists (if *pvs-emacs-interface* :supersede :append))
(unwind-protect
(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)
(*disable-gc-printout* t)
(input-stream (when input (make-string-input-stream input))))
(if banner?
(format t "
+----
| ~a
|
| Enter a PVS ground expression followed by ';' at the prompt '~a'.
| Enter a Lisp expression followed by '!' at the prompt '~a'.
|
| Enter 'help' for help and 'exit' to exit the evaluator. Follow
| these commands with either ';' or '!'.
|
| *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* *pvsio-promptin* *pvsio-promptin*)
(format t "Starting pvsio script~%"))
(evaluate-pvsio input-stream))
(when *pvs-emacs-interface*
(pvs-emacs-eval "(pvs-evaluator-ready)")))))))
(defun read-expr (input-stream)
(catch '*pvsio-command*
(do ((have-real-char nil)
(have-first-space nil)
(instr nil)
(fstr (make-string-output-stream))
(c (read-char input-stream nil nil)
(read-char input-stream nil nil)))
((and (eq c #\;)
(not instr))
(string-trim '(#\Space #\Tab #\Newline)
(get-output-stream-string fstr)))
(when (null c) (throw '*pvsio-quit* nil))
(when (and (not instr)
have-real-char
(not have-first-space)
(member c '(#\Space #\Newline #\Tab) :test #'char=))
(let ((pref (get-output-stream-string fstr)))
(cond ((member pref '("(lisp" "(pvs::lisp")
:test #+allegro #'string= #-allegro #'string-equal)
(let ((input (read input-stream nil nil)))
(format t "~%~s~2%~a" (eval input) *pvsio-promptin*))
(loop until (or (null c) (char= c #\)))
do (setq c (read-char-no-hang input-stream nil nil)))
(setq c #\Space)
(setq have-real-char nil
have-first-space nil))
(t (loop for ch across pref do (write-char ch fstr))
(setq havespace t)))))
(when (and (eq c #\!) (not instr))
(clear-input)
(throw '*pvsio-command*
(read-from-string
(get-output-stream-string fstr))))
(if have-real-char
(write-char c fstr)
(unless (member c '(#\Space #\Newline #\Tab) :test #'char=)
(write-char c fstr)
(setq have-real-char t)))
(when (eq c #\") (setq instr (not instr))))))
(defun evaluate-pvsio (input-stream)
(let ((result
(multiple-value-bind
(val err)
(ignore-errors ;; Change to progn for debugging
(catch '*pvsio-error*
(catch '*pvsio-quit*
(catch 'tcerror
(let* ((input (read-pvsio input-stream))
(pr-input (pc-parse input 'expr))
(*tccforms* nil)
(tc-input (pc-typecheck pr-input))
(isvoid (and tc-input
(type-name? (type tc-input))
(string= "void"
(format
nil "~a"
(print-type (type tc-input)))))))
(when *evaluator-debug*
(format t "~%Expression ~a typechecks to: ~%" pr-input)
(show tc-input))
(when *tccforms*
(format t "~%Typechecking ~a produced the following TCCs:~%" pr-input)
(evaluator-print-tccs *tccforms*)
(format
t
"~%~%Evaluating in the presence of unproven TCCs may be unsound~%")
(clear-input)
(unless (pvs-y-or-n-p "Do you wish to proceed with evaluation? ")
(throw '*pvsio-error* t)))
(let ((cl-input (pvs2cl tc-input)))
(when *evaluator-debug*
(format t "~%PVS expression ~a translates to Common Lisp expression:~%~a~%"
tc-input cl-input))
(multiple-value-bind
(cl-eval err)
(catch 'undefined
(ignore-errors
(if *pvs-eval-do-timing*
(time (eval cl-input))
(eval cl-input))))
(when *evaluator-debug*
(format t "~%Common Lisp expression ~a evaluates to:~%~a~%" cl-input cl-eval))
(cond ((and err (null cl-eval))
(format t "~%Error: ~a" err))
(err (format t "~%Error (~a): ~a" cl-eval err))
((eq cl-eval 'cant-translate)
(format t "~%Error: Expression doesn't appear to be ground"))
(*convert-back-to-pvs*
(unless isvoid
(let ((pvs-val
(catch 'cant-translate (cl2pvs cl-eval (type tc-input)))))
(if (expr? pvs-val)
(progn
(format t *pvsio-promptout*)
(force-output)
(unparse pvs-val))
(format t "~%Error: Result ~a is not ground" cl-eval)))))
(t (format t "~a" cl-eval)))))
t)))))
(if err (null input-stream) val))))
(when result
(format t "~%")
(evaluate-pvsio input-stream))))
(defun read-pvsio (input-stream)
(when (not input-stream)
(format t "~%~a" *pvsio-promptin*)
(force-output))
(let ((input (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 '*pvsio-quit* nil))
(read-pvsio input-stream))
((member input '(exit (exit) "exit") :test #'equal)
(throw '*pvsio-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-pvs-attachments list_pvs_attachments
"list_pvs_attachments")
:test #'equal)
(list-pvs-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 (multiple-value-bind
(val err)
(ignore-errors (eval input))
(if err (format t "ERROR (lisp): ~a" err)
(format t "~a" val))
(fresh-line)
(read-pvsio input-stream))))))
(defun run-pvsio ()
(let* ((file (environment-variable "PVSIOFILE"))
(time (read-from-string (environment-variable "PVSIOTIME")))
(theory (environment-variable "PVSIOTHEORY"))
(packlist (read-from-string (environment-variable "PVSIOPACK")))
(verb (read-from-string (environment-variable "PVSIOVERB")))
(tccs (read-from-string (environment-variable "PVSIOTCCS")))
(pvsio-main (environment-variable "PVSIOMAIN"))
(main (unless (string= pvsio-main "") (format nil "~a;" pvsio-main)))
(*pvsio-promptin* (environment-variable "PVSIOPROMPTIN"))
(*pvsio-promptout* (environment-variable "PVSIOPROMPTOUT"))
(*pvsio-version* (environment-variable "PVSIOVERSION")))
(when time (setq *pvs-eval-do-timing* t))
(multiple-value-bind
(val err)
(ignore-errors
(unless main
(format t "~%Generating ~a.log~%" theory))
(with-open-file
(*standard-output*
(merge-pathnames (directory-namestring file) (format nil "~a.log" theory))
:direction :output
:if-does-not-exist :create
:if-exists :supersede)
(change-context (directory-namestring file))
(dolist (pack packlist) (load-prelude-library pack))
(unwind-protect
(typecheck-file (file-namestring file) nil nil nil t)
(fresh-line)
(finish-output)))
(load-pvs-attachments)
(evaluation-mode-pvsio theory main tccs (null main))
t)
(when err (format t "~%~a (~a.pvs). See ~a~a.log~%"
err file (directory-namestring file) theory)))
(fresh-line)
(bye 0)))
[ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
]
|
|
