;; ;; pvsio.lisp ;; Release: PVSio-6.0.9 (3/14/14) ;; ;; Contact: Cesar Munoz (cesar.a.munoz@nasa.gov) ;; 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 ;;
(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 nilnil)
(read-char input-stream nilnil)))
((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 nilnil)))
(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 nilnil)))
(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))))
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
