SSL patch-5.lisp Sprache: Lisp

(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)

quality100%

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