Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: patch-7.lisp Sprache: Lisp

Original von: PVS^©

(in-package :pvs)

(defmethod translate-to-prove ((expr name-expr))
  (let* ((pos (position expr *bindings* ;(NSH:4-5-91)
   :test #'same-declaration))
  (apos (position expr *bound-variables*
    :test #'same-declaration))
  (bpos (when apos (- (length *bound-variables*)
        apos))))
    (cond ((and (null pos)(null bpos))
    (unique-prover-name expr))
   (bpos (let ((id (intern
      (concatenate 'string
        "*" (string (id expr)) "_"
        (princ-to-string bpos) "*") :pvs)
     ;;(makesym "*~a_~a*" (id expr) bpos)
     ))
    (add-to-local-typealist id expr)
    id)) ;;NSH(4.2.95) id was (id expr) and unsound!
   ;;eg. proved (FORALL i, (j|j<i): (FORALL (j| j>i): j<i).
   (t (let* ((nvar (intern (concatenate 'string
            "*" (princ-to-string (1+ pos)) "*") :pvs)
     ;;(makesym "*~a*" (1+ pos))

     )
      (expr-type (type expr))
      (vars (intersection (freevars expr-type)
     *bindings*
     :test #'same-declaration))
      (tr-vars (translate-to-prove vars))

      (st-name (get-subtype-coercion expr-type))
      (st-expr (cons st-name (cons nvar tr-vars))))
        st-expr)))))

(defun unique-prover-name (expr)
  (cond ((constant? expr) ;;NSH(2.16.94): changed to deal with Ricky's
                   ;;soundness bug where actuals are ignored.
  (cond ((and (constructor? expr)
       (enum-adt? (find-supertype (type expr))))
  (position (id expr)
     (constructors (adt (find-supertype (type expr))))
     :test #'eq :key #'id))
        ((tc-eq expr *true*) '(true))
        ((tc-eq expr *false*) '(false))
        (t (let* ((norm-expr (normalize-name-expr-actuals expr))
    (id-hash (gethash norm-expr *translate-id-hash*))
    (newconst (or id-hash
           (list (intern
           (concatenate 'string
          (string (if (integerp (id expr))
               (format nil "~r"
                (id expr))
             (id expr)))
          "_"
          (princ-to-string
           (funcall
            *translate-id-counter*))) :pvs))))
    (expr-freevars (freevars expr))
    (expr-bindings (intersection expr-freevars *bindings*
            :test #'same-declaration))
    )
      (unless id-hash
        (setf (gethash norm-expr *translate-id-hash*)
       newconst)
        ;;(format t "~%adding ~a to typealist" (car newconst))
     ;(add-to-typealist (car newconst) expr)
        )
      (cond (expr-bindings
      (let* ((tr-vars (translate-to-prove expr-bindings))
      (prtype (prover-type (or (type expr) (car (ptypes expr)))))
      (apname (make-apply-symbol (length tr-vars) prtype)))
        (cons apname (cons newconst tr-vars))))
     (t (add-to-typealist (car newconst) expr)
        newconst))))))
(t (add-to-local-typealist (id expr) expr)
    (id expr))))

(defun get-subtype-coercion (expr-type)
  (let* ((name (cdr (assoc expr-type *subtype-names* :test #'tc-eq))))
    (or name
(let* ((name (intern (concatenate 'string
       "*" (string (gentemp "subtype")) "*") :pvs)
       ;;(makesym "*~a*" (gentemp "subtype"))
       )
        )
   (push  (cons expr-type name) *subtype-names*)
   name))))

(defmethod translate-to-prove ((expr cases-expr))
  (translate-to-prove (translate-cases-to-if expr)))

(defmethod translate-to-prove ((expr binding-expr))
  (let* ((*bindings* (append (bindings expr) *bindings*))
  (type (type expr))
  (prtype (prover-type type))
  (body (expression expr))
  (exprtype (prover-type (type body)))
  (connective? (connective-occurs? body))
  (tr-expr
   (if connective?
       ;;NSH(11.4.95): Fixes unsoundness caused
      ;;by translating (LAMBDA : IF B ...) to (LAMBDA 1: CC)
      ;;by generating (LAMBDA 1 : CC(*1*)) instead.
      ;;Note that two tc-eq such LAMBDAs will generate
      ;;different translations so that ASSERT might miss some
      ;;syntactic equalities when there are IFs in LAMBDAs.
       (cond
        (*bindings*
  (let* ((newid (gentemp))
         (body-freevars (freevars body))
         (body-bindings (intersection body-freevars *bindings*
          :test #'same-declaration))
         ;;bound variables can't be ignored; subtyp constraints needed
         ;;freevars of the expr are needed for connectives.
         (tr-vars (translate-to-prove body-bindings))
         (apname (make-apply-symbol (length tr-vars) exprtype))
         (apform (cons apname (cons newid tr-vars))))
    (unless (or (null exprtype)
         (assoc apname typealist))
      (push (cons apname exprtype) typealist)
      (pushnew apname applysymlist))
    apform))
        (t (let ((name (cdr (assoc body *named-exprs* :test #'tc-eq))))
      ;;if there are no *bindings* then use the cached translation in *named-exprs*
      (or name
   (let ((newid (gentemp)))
     (add-to-typealist newid nil (type expr))
     (push (list body newid) *named-exprs*)
     (list newid))))))
       (translate-to-prove (expression expr))))
  (tr-operator (unique-binding-operator expr))
  (tr-lambda-expr
   (cons 'lambda
  (cons (length (bindings expr))
        (list tr-expr)))))
    (if (lambda-expr? expr)
tr-lambda-expr
  (list (make-apply-symbol 1 prtype)
        tr-operator
        tr-lambda-expr))))

(defun make-apply-symbol (arity type)
  (let ((name (intern (concatenate 'string
       "APPLY-"
       (princ-to-string arity)
       "-" (string (or type '||))) :pvs)))
    (unless (or (not type)
  (assoc name typealist))
      (push (cons name type) typealist)
      (pushnew name applysymlist))
    name))

(defmethod make-apply-name ((te type-expr))
  (let* ((type (find-supertype te))
  (prtype (prover-type (range type)))
  (name (make-apply-symbol (length (domain-types type))
      prtype))
  )
    name))

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.