Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: trk_bands_2D.prf Sprache: Lisp

Original von: PVS^©

(defmethod add-usings-to-context* ((adt recursive-type) inst)
  (let ((acts (actuals inst)))
    (add-usings-to-context
     (mapcar #'(lambda (gen)
   (when gen
     (let ((frms (formals-sans-usings gen)))
       (cond ((length= acts frms)
       (mk-modname (id gen) (actuals inst)
     (library inst)))
      (t (mk-modname (id gen) nil
       (library inst)))))))
      (delete-if #'null
   (list (adt-theory adt)
         (adt-map-theory adt)
         (adt-reduce-theory adt)))))))

(defun bindings-to-modinsts (bindings modinsts theories)
  (if (null bindings)
      (values modinsts theories)
      (let* ((theory (module (caar bindings)))
      (rem (if (eq theory (current-theory))
        bindings
        (nthcdr (length (formals-sans-usings theory)) bindings)))
      (decl (when (and rem (decl-formal-type? (caar rem)))
       (associated-decl (caar rem))))
      (drem (if decl (nthcdr (length (decl-formals decl)) rem) rem)))
(bindings-to-modinsts
  drem
  (cons (make-instance 'modname
   :id (id theory)
   :actuals (mapcar #'(lambda (a)
          ;; mk-res-actual lifts equality
          (mk-res-actual (cdr a) theory))
       (ldiff bindings rem))
   :dactuals (mapcar #'(lambda (a) (mk-actual (cdr a)))
        (ldiff rem drem)))
        modinsts)
  (acons theory decl theories)))))

(defmethod type-expr-from-print-type ((te type-name))
  (let* ((decl (declaration (resolution te)))
  (tval (type-value decl))
  (thinst (module-instance (resolution te))))
    (assert (eq (id (module decl)) (id thinst))
     () "Strange type-name resolution")
    (restore-object* (actuals thinst))
    (assert (not (store-print-type? tval)))
    (let* ((type-expr (if (actuals thinst)
     (let ((*pseudo-normalizing* t)) ;; disallow pseudo-normalize
       (subst-mod-params tval thinst (module decl) decl))
     (copy tval 'print-type te))))
      #+pvsdebug (assert (or (print-type type-expr) (tc-eq te type-expr)))
      #+pvsdebug (assert (true-type-expr? type-expr))
      type-expr)))

(defmethod type-expr-from-print-type ((te type-application))
  (let* ((res (resolution (type te)))
  (decl (declaration res))
  (thinst (module-instance res)))
    (with-current-decl decl
      (restore-object* (actuals thinst))
      (let* ((mtype-expr (if (actuals thinst)
        (let ((*pseudo-normalizing* t)) ;; disallow pseudo-normalize
          (subst-mod-params (type-value decl) thinst
     (module decl) decl))
        (type-value decl)))
      (type-expr (if (every #'(lambda (x y)
           (and (name-expr? y)
         (eq (declaration y) x)))
       (car (formals decl)) (parameters te))
       mtype-expr
       (substit mtype-expr
         (pairlis (car (formals decl)) (parameters te))))))
#+pvsdebug (assert (true-type-expr? type-expr))
(with-slots (print-type) type-expr
   (setf print-type te))
type-expr))))

(defun set-tc-match-binding (binding arg bindings &optional (last-attempt? t))
  (let ((dtype (compatible-type (cdr binding) arg)))
    (if dtype
(let ((type (dep-binding-type dtype)))
   (unless (or (and (dependent-type? type)
      (not (has-type-vars? (cdr binding))))
        (and (member (cdr binding) *tc-strict-matches*
       :test #'tc-eq)
      (or (fully-instantiated? (cdr binding))
          (not (fully-instantiated? arg)))))
     (cond (*tc-match-strictly*
     (push arg *tc-strict-matches*)
     (setf (cdr binding) arg))
    (t (setf (cdr binding) type))))
    bindings)
(when last-attempt?
   (tc-match-last-attempt (cdr binding) arg binding bindings)))))

(defmethod set-type* ((ex if-expr) expected)
  #+pvsdebug (assert (fully-typed? (operator ex)))
  (let* ((op (operator ex))
  (optype (determine-operator-type op (argument ex) expected ex)))
    (set-type* op optype)
    (let ((reses (remove-if-not
       #'(lambda (r)
    (let ((stype (find-supertype (type r))))
      (and stype
    (typep stype 'funtype)
    (compatible? (range stype) expected))))
     (resolutions op))))
      (unless (singleton? reses)
(if reses
     (type-ambiguity ex)
     (type-incompatible ex (ptypes ex) expected)))
      (if (eq (id (module-instance (car reses))) '|if_def|)
   (let ((econd (condition ex))
  (ethen (then-part ex))
  (eelse (else-part ex)))
     (set-type* econd *boolean*)
     (let ((*tcc-conditions* (push-tcc-condition econd
             *tcc-conditions*)))
       (set-type* ethen expected))
     (let* ((*generate-tccs* (if *ignore-else-part-tccs*
     'none
     *generate-tccs*))
     (*tcc-conditions*
      (if (typep ex '(or first-cond-expr single-cond-expr
           cond-expr last-cond-expr))
   *tcc-conditions*
   (push-tcc-condition (make!-negation econd)
        *tcc-conditions*))))
       (set-type* eelse expected))
     (let* ((iftype (dep-binding-type
       (compatible-type (type ethen) (type eelse)))))
       (assert iftype)
       ;;(set-type* op (mk-funtype (list *boolean* iftype iftype)
       ;; iftype))
       (let ((res (resolve (copy (operator ex)
        :resolutions nil
        :type nil)
      'expr (arguments ex))))
  (cond ((and (singleton? res)
       (not (tc-eq (car res)
     (resolution (operator ex)))))
         (setf (type op) (type (car res)))
         (setf (resolutions op) (list (car res))))
        (t (setf (type op)
          (mk-funtype (list *boolean* iftype iftype)
        iftype))
    (setf (resolutions op) reses))))
       (unless (eq (id (current-theory)) '|if_def|)
  (setf (actuals (module-instance op))
        (list (mk-actual iftype))))
       #+pvsdebug (assert (fully-instantiated? op))
       (setf (type (argument ex))
      (mk-tupletype (list *boolean* iftype iftype)))
       (setf (type ex) iftype))
     (unless (typep ex 'branch)
       (if (typep ex 'chained-if-expr)
    (change-class ex 'chained-branch)
    (change-class ex 'mixfix-branch))))
   (call-next-method)))))

(defun create-formulas* (res decl)
  (cond ((formula-decl? decl)
  (unless (closed-definition decl)
    (let* ((*in-checker* nil)
    (*current-context* (context decl)))
      (setf (closed-definition decl)
     (with-current-decl decl
       (universal-closure (definition decl))))))
  (let ((*no-expected* t))
    (list
     (subst-mod-params (closed-definition decl)
         (module-instance res)
         (module decl)
         decl))))
((typep decl '(or const-decl def-decl))
  (let ((subst-list (subst-mod-params (def-axiom decl)
          (module-instance res)
        (module decl)
        decl)))
    (assert (subsetp (freevars subst-list)
       (freevars (module-instance res))
       :test #'same-declaration))
    (copy-list subst-list)))
(t nil)))

(defmethod set-type* ((te type-name) expected)
  (declare (ignore expected))
  (assert (resolution te))
  (when (and (or (actuals te) (dactuals te))
      (not (or (actuals (module-instance te))
        (dactuals (module-instance te)))))
    (if (same-id (module-instance te) (current-theory))
(type-error te
   "May not provide actuals for entities defined locally")
(type-error te
   "May not specify actuals for this type name")))
;  (unless (or (same-id (module-instance te) (current-theory))
;       (from-prelude? (get-theory (module-instance te))))
;    (pushnew (module-instance te)
;      (instances-used (current-theory))
;      :test #'tc-eq))
  (when (or (actuals (module-instance te))
     (dactuals (module-instance te)))
    (setf (module-instance (resolution te))
   (set-type-actuals-and-maps te (module (declaration (resolution te))))))
  #+pvsdebug (fully-typed? te)
  (when (and (typep (type (resolution te)) 'type-name)
      (adt (type (resolution te))))
    (unless (and (boundp '*adt-type-name-pending*)
   (memq te (assq (id te) *adt-type-name-pending*)))
      (let ((adt (adt (type (resolution te)))))
(change-class te 'adt-type-name
   :adt adt
   :single-constructor? (singleton? (constructors adt))))))
  (unless (or *dont-worry-about-full-instantiations*
       (fully-instantiated? te))
    (maybe-instantiate-from-decl-formals te)
    (unless (fully-instantiated? te)
      (type-error te
"Could not determine the full theory instance for ~a~
       ~%  Theory instance: ~a"
te (full-name (module-instance te))))))

(defmethod constructors ((tn type-name))
  (when (adt? tn)
    (when (symbolp (adt tn))
      ;; May happen after restoring from bin files
      (restore-adt-slot tn))
    (mapcar #'(lambda (cd)
  (mk-name-expr (id cd) nil nil
         (make-resolution cd (module-instance tn))))
     (mapcar #'con-decl (constructors (adt tn))))))

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.