;; ;; pvs-lib.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. ;; ;; This code implements the functionality to load PVSio semantic ;; attachments from the files pvs-attachments and ~/.pvs-attachments ;;
(defun libload-attachments (dir file &optional force (verbose t))
(if (probe-file (merge-pathnames dir file))
(load-update-attachments dir file force verbose)
(some #'(lambda (path)
(let ((lib (format nil"~a~a" path dir)))
(load-update-attachments lib file force verbose)))
*pvs-library-path*)))
(defun load-imported-attachments (libs &optional force (verbose t))
(loop for dir being the hash-key of libs
when (or (and (not (member dir *pvsio-imported* :test #'string=))
(push dir *pvsio-imported*))
force)
do (libload-attachments dir "pvs-attachments" force verbose)))
(defun load-pvs-attachments (&optional force (verbose t))
(format t "Loading semantic attachments~%")
(when force (initialize-prelude-attachments))
(load-imported-attachments *prelude-libraries* force verbose)
(load-imported-attachments *imported-libraries* force verbose)
(load-update-attachments "~/"".pvs-attachments" force verbose)
(load-update-attachments *pvs-context-path* "pvs-attachments" force verbose))
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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.
