Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: patch-5.lisp Sprache: Lisp

Original von: PVS^©

(defmethod set-type* :around ((ex application) expected)
   (declare (ignore expected))
   (let* ((op (operator* ex))
   (added? (and (name-expr? op)
         (not (memq op *applied-operators*))))
   (*applied-operators* (if added?
       (cons op *applied-operators*)
       *applied-operators*)))
     (call-next-method)
     ;; Note that the call-next-method could have modified ex
     (setf op (operator* ex))
     (typecase ex
       (field-application
(when (from-macro (argument ex))
     ;;(cdr (assq (argument ex) (macro-expressions (current-theory))))
   (let ((orig (copy ex))
  (nex (beta-reduce ex)))
     (unless (eq ex nex)
       (change-class ex (class-of nex))
       (copy-slots ex nex)
       (setf (from-macro ex) orig)
       ;;(push (cons orig ex) (macro-expressions (current-theory)))
       ))))
       (application
(cond ((and added?
      (name-expr? op)
      (macro-decl? (declaration op))
      (not (eq (declaration op) (current-declaration))))
        (let* ((def (subst-mod-params
       (args2 (car (last (def-axiom (declaration op)))))
       (module-instance op)
       (module (declaration op))))
        (dappl (make!-applications def (argument* ex)))
        (appl (beta-reduce dappl nil))
        (orig (copy ex)))
   (when (and (lambda-expr? def)
       (eq *generate-tccs* 'none))
     (mapc #'(lambda (arg dom)
        (let* ((jtypes (judgement-types+ arg))
        (incs (compatible-predicates jtypes dom arg)))
          (when incs
     (generate-subtype-tcc arg dom incs))))
    (argument* ex) (get-lambda-expr-full-domain def)))
   (change-class ex (class-of appl))
   (copy-slots ex appl)
   (setf (from-macro ex) orig)
   ;;(push (cons orig ex) (macro-expressions (current-theory)))
   ))
       ((and (accessor-name-expr? (operator ex))
      (from-macro (argument ex))
      ;;(cdr (assq (argument ex)
      ;;        (macro-expressions (current-theory))))
      )
        (let ((orig (copy ex))
       (nex (beta-reduce ex)))
   (unless (eq ex nex)
     (change-class ex (class-of nex))
     (copy-slots ex nex)
     (setf (from-macro ex) orig)
     ;;(push (cons orig ex) (macro-expressions (current-theory)))
     ))))))))

(defmethod get-lambda-expr-full-domain ((ex lambda-expr))
  (cons (get-lambda-expr-domain ex)
(get-lambda-expr-full-domain (expression ex))))

(defmethod get-lambda-expr-full-domain (ex)
  nil)

¤ Dauer der Verarbeitung: 0.1 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.