Quelle patch-107.lisp Sprache: Lisp

;;
;; defattach.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.
;;
;; Functions and macros for defining PVSio semantic attachments
;;

(in-package :pvs)

(defparameter *pvsio-attachments* (make-hash-table :test #'equal))

(defun pvsio-version ()
  (pvs-message *pvsio-version*))

;; Primitive attachments are TRUSTED
(defstruct attachment theory name args primitive symbol)

(defun find-attachments (name)
  (loop for attachments being the hash-value of *pvsio-attachments*
append (loop for attachment in attachments
       when (string= name (attachment-name attachment))
       collect attachment)))

(defun same-attachment (a1 a2)
  (and (string= (attachment-name a1)
  (attachment-name a2))
       (string= (attachment-theory a1)
  (attachment-theory a2))
       (equal (attachment-args a1)
       (attachment-args a2))))

(defun find-attachment (attachmnt)
  (find attachmnt (gethash (attachment-theory attachmnt)
      *pvsio-attachments*)
:test #'same-attachment))

(defun pvsio-symbol (expr nargs)
  (let* ((nm (string (id expr)))
  (th (string (id (module-instance expr))))
  (a  (find-attachment (make-attachment
          :theory th
          :name nm
          :args nargs))))
      (when a (attachment-symbol a))))

(defun attachment-list ()
  (loop for attachments being the hash-value of *pvsio-attachments*
append attachments))

(defun attachment-names ()
  (sort (remove-duplicates
  (mapcar #'attachment-name (attachment-list))
  :test #'string=)
#'string<))

(defun attachment-theories ()
  (sort (loop for theory being the hash-key of *pvsio-attachments*
       collect theory)
#'string<))

(defun attachment-name-prim (attachmnt)
  (format nil "~a [~a~:[~;, primitive~]]"
   (attachment-name attachmnt)
   (attachment-args attachmnt)
   (attachment-primitive attachmnt)))

(defun list-pvs-attachments-str ()
  (let ((l (loop for theory being the hash-key using (hash-value attachments) of
   *pvsio-attachments*
   collect (cons (format nil "~a" theory)
          (format nil "Theory ~a: ~{~a~^, ~}.~2%" theory
           (mapcar #'attachment-name-prim
            (sort attachments #'(lambda (x y)
             (string-lessp
              (attachment-name x)
              (attachment-name y))))))))))
    (if l (format nil "Semantic attachments loaded in current context:~2%~{~a~}"
    (mapcar #'cdr (sort l #'(lambda(x y) (string-lessp (car x) (car y))))))
      (format nil "No semantics attachments loaded in current context.~2%"))))

(defun list-pvs-attachments ()
  (format t "~a" (list-pvs-attachments-str)))

(defun help-attachment-doc (attachmnt)
  (let ((fun (makesym "pvsio_~a_~a_~a"
        (attachment-theory attachmnt)
        (attachment-name attachmnt)
        (attachment-args attachmnt))))
    (documentation fun 'function)))

(defun help-theory-attachments-str (theory)
  (let ((l (loop for attachmnt in (gethash theory *pvsio-attachments*)
   collect (help-attachment-doc attachmnt))))
    (if l (format nil "Semantic attachments in theory ~a:~2%~{~a~}" theory l)
  (format nil "No semantic attachments in theory ~a.~2%" theory))))

(defun help-pvs-theory-attachments (theory)
  (format t "~a" (help-theory-attachments-str theory)))

(defun help_pvs_theory_attachments (theory)
  (help-pvs-theory-attachments theory))

(defun help-attachment-str (name)
  (let ((l (loop for attachmnt in (find-attachments name)
   collect (help-attachment-doc attachmnt))))
    (if l
(format nil "Semantic attachments named ~a:~2%~{~a~}" name l)
      (format nil "No semantic attachments named ~a.~2%" name))))

(defun help-pvs-attachment (name)
  (format t "~a" (help-attachment-str name)))

(defun help_pvs_attachment (name)
  (help-pvs-attachment name))

(defun check-defattach (name body)
  (cond ((not (symbolp name))
  (pvs-message
   "Error: ~a is not a valid name for a semantic attachment"
   name)
  nil)
((null body)
  (pvs-message "Error: Body of semantic attachment ~a is missing"
        name))
(t t)))

(defmacro defattach (thnm args &rest body)
  (when (check-defattach thnm body)
    (let* ((thnms  (symbol-name thnm))
    (pos    (position #\. thnms)))
      (cond ((not pos)
      (pvs-message
       "Error: ~a is not a valid name for a semantic attachment"
       thnms))
     (t
      (let ((theory (subseq thnms 0 pos))
     (name   (subseq thnms (+ pos 1))))
        (pvs-message "Loading semantic attachment: ~a.~a [~a]"
       theory name (length args))
        (defattach-aux theory name args body)))))))

;; semantic primitives are TRUSTED
(defmacro defprimitive (thnm args &rest body)
  (when (check-defattach thnm body)
    (let* ((thnms  (symbol-name thnm))
    (pos    (position #\. thnms)))
      (cond ((not pos)
      (pvs-message
       "Error: ~a is not a valid name for a semantic attachment [primitive]"
       thnms))
     (t
      (let ((theory (subseq thnms 0 pos))
     (name   (subseq thnms (+ pos 1))))
        (pvs-message "Loading semantic attachment: ~a.~a [~a, primitive]"
       theory name (length args))
        (defattach-aux theory name args body t)))))))

;; Primitive attachments are TRUSTED
(defun defattach-aux (theory name args body &optional primitive)
  (let* ((nargs     (length args))
  (newargs   (append args (list '&optional '*the-pvs-type*)))
  (fnm       (makesym "pvsio_~a_~a_~a" theory name nargs))
  (attachmnt (make-attachment :theory theory :name name :args nargs
         :primitive primitive :symbol fnm))
  (nm        (makesym "~a" name))
  (th        (makesym "~a" theory))
  (argstr    (if args (format nil "(~{~a~^, ~})" args) ""))
  (dobo      (if (and body (cdr body) (stringp (car body)))
   body
        (cons "" body)))
  (doc       (format nil "
Attachment: ~a.~a~%
Usage: ~a~a~%
Documentation: ~a~%
Lisp name : ~a~%
Lisp definition: ~%
~s~%~%"
      theory (attachment-name-prim attachmnt)
                           name argstr
      (car dobo)
      fnm
      (cons 'progn (cdr dobo))))
  (mssg
   (format
    nil
    "Function ~a.~a is defined as a semantic attachment.
It cannot be evaluated in a formal proof."
    theory name)))
    (when (find-attachment attachmnt)
      (pvs-message "Redefining ~a.~a" theory (attachment-name-prim attachmnt)))
    (setf (gethash theory *pvsio-attachments*)
   (cons attachmnt (remove-if #'(lambda (x) (same-attachment attachmnt x))
         (gethash theory *pvsio-attachments*))))
    (let ((body (if primitive
      (cons 'progn (cdr dobo))
    `(if *in-evaluator*
         ,(cons 'progn (cdr dobo))
       (throw '*pvsio-inprover* ,mssg)))))
      `(defun ,fnm ,newargs ,doc ,body))))

(defmacro defattach-th-nm (theory nm args &rest body)
  (when (check-defattach nm body)
    (defattach-aux theory (symbol-name nm) args body)))

(defmacro defprimitive-th-nm (theory nm args &rest body)
  (when (check-defattach nm body)
    (defattach-aux theory (symbol-name nm) args body t)))

(defun reattach (theory macros)
  (mapcar #'(lambda (x)
       (cond ((and (consp x) (eq (car x) 'defattach))
       (cons 'defattach-th-nm (cons theory (cdr x))))
      ((and (consp x) (eq (car x) 'defprimitive))
       (cons 'defprimitive-th-nm (cons theory (cdr x))))
      (t x)))
   macros))

(defmacro attachments (th &rest macros)
  (cond ((not (symbolp th))
  (pvs-message "Error: ~a is not a valid theory name" th))
(t
  (let ((theory (symbol-name th)))
    (pvs-message "Loading semantic attachments in theory ~a" theory)
    (cons 'progn (reattach theory macros))))))

quality97%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.