Filtering...

defapply

books/centaur/gl/defapply
other
(in-package "GL")
other
(include-book "clause-processors/generalize" :dir :system)
other
(include-book "tools/defevaluator-fast" :dir :system)
other
(include-book "tools/mv-nth" :dir :system)
other
(include-book "tools/rulesets" :dir :system)
other
(include-book "gl-util")
other
(include-book "misc/hons-help2" :dir :system)
defeval-fns-to-callsfunction
(defun defeval-fns-to-calls
  (fns world)
  (declare (xargs :guard (and (symbol-listp fns)
        (plist-worldp world))))
  (b* (((when (atom fns)) nil) (formals (getprop (car fns)
          'formals
          :missing 'current-acl2-world
          world))
      ((when (eq formals :missing)) (er hard?
          'defeval-fns-to-calls
          "Missing formals for function: ~x0~%"
          (car fns))
        (defeval-fns-to-calls (cdr fns) world)))
    (cons (cons (car fns) formals)
      (defeval-fns-to-calls (cdr fns) world))))
defeval-wrapmacro
(defmacro defeval-wrap
  (ev evlst fns)
  `(make-event `(defevaluator-fast ,',GL::EV
      ,',GL::EVLST
      ,(GL::DEFEVAL-FNS-TO-CALLS ',GL::FNS (GL::W GL::STATE))
      :namedp t)))
other
(defthmd len-open-for-defapply
  (equal (len (cons a b)) (+ 1 (len b))))
other
(defthmd nth-open-for-defapply
  (implies (syntaxp (quotep n))
    (equal (nth n (cons a b))
      (if (zp n)
        a
        (nth (1- n) b)))))
other
(defstub apply-stub (f args) t)
other
(program)
make-list-of-nthsfunction
(defun make-list-of-nths
  (sym start n)
  (declare (xargs :guard (and (natp start) (natp n))))
  (if (zp n)
    nil
    (cons `(nth ,GL::START ,GL::SYM)
      (make-list-of-nths sym (1+ start) (1- n)))))
eccmacro
(defmacro ecc
  (call)
  (declare (xargs :guard (consp call)))
  (if (member-eq (car call) *ec-call-bad-ops*)
    call
    `(ec-call ,GL::CALL)))
make-mv-callfunction
(defun make-mv-call
  (f args world)
  (let* ((stobjs-out (getprop f
         'stobjs-out
         nil
         'current-acl2-world
         world)))
    (if (and stobjs-out (< 1 (length stobjs-out)))
      `(mv-list ,(LENGTH GL::STOBJS-OUT)
        (ecc (,GL::F . ,GL::ARGS)))
      `(ecc (,GL::F . ,GL::ARGS)))))
make-apply-entryfunction
(defun make-apply-entry
  (f world)
  (let* ((formals (getprop f
         'formals
         nil
         'current-acl2-world
         world)))
    `((and (eq f ',GL::F)
       (true-listp args)
       (eql (len args) ,(LENGTH GL::FORMALS))) ,(GL::MAKE-MV-CALL GL::F
  (GL::MAKE-LIST-OF-NTHS 'GL::ARGS 0 (LENGTH GL::FORMALS)) GL::WORLD))))
make-apply-clique-entriesfunction
(defun make-apply-clique-entries
  (clique world)
  (if (atom clique)
    nil
    (cons (make-apply-entry (car clique) world)
      (make-apply-clique-entries (cdr clique) world))))
make-apply-entriesfunction
(defun make-apply-entries
  (fns world acc)
  (if (atom fns)
    (prog2$ (flush-hons-get-hash-table-link acc)
      nil)
    (if (hons-get (car fns) acc)
      (make-apply-entries (cdr fns) world acc)
      (let* ((clique (or (wgetprop (car fns) 'recursivep)
             (list (car fns)))) (acc (hons-put-list clique t acc)))
        (append (make-apply-clique-entries clique world)
          (make-apply-entries (cdr fns) world acc))))))
other
(def-ruleset! defapply-guards
  '((:executable-counterpart eqlablep) (:executable-counterpart equal)))
mk-arity-tablefunction
(defun mk-arity-table
  (lst w)
  (if (atom lst)
    nil
    (cons (cons (car lst)
        (len (getprop (car lst)
            'formals
            nil
            'current-acl2-world
            w)))
      (mk-arity-table (cdr lst) w))))
other
(local (defun myapp-arities
    nil
    (declare (xargs :guard t))
    '((mvfn . 2) (if . 3)
      (equal . 2)
      (not . 1)
      (len . 1)
      (cons . 2))))
other
(local (defeval-wrap myapp-ev
    myapp-ev-lst
    (mvfn if equal not len cons)))
other
(include-book "clause-processors/unify-subst" :dir :system)
other
(include-book "clause-processors/meta-extract-user" :dir :system)
other
(include-book "clause-processors/find-subterms" :dir :system)
other
(include-book "tools/match-tree" :dir :system)
make-applyfunction
(defun make-apply
  (name fns world)
  (declare (xargs :mode :program))
  (b* ((ev (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-EV")
         name)) (ev-lst (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-EV-LST")
          name)))
    `(progn (defun ,(GL::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME GL::NAME) "-ARITIES") GL::NAME)
        nil
        (declare (xargs :guard t))
        ',(GL::MK-ARITY-TABLE GL::FNS GL::WORLD))
      (encapsulate nil
        (local (in-theory (e/d** ((:ruleset defapply-guards) eq
                eql
                car-cons
                cdr-cons
                cadr-kwote-lst-meta-correct
                (nfix)
                (:rules-of-class :type-prescription :here)))))
        (defeval-wrap ,GL::EV ,GL::EV-LST ,GL::FNS)
        (defund ,GL::NAME
          (f args)
          (declare (xargs :guard t :normalize nil))
          (mbe :logic (,GL::EV (cons f (kwote-lst args)) nil)
            :exec (cond ,@(GL::MAKE-APPLY-ENTRIES GL::FNS GL::WORLD NIL)
              (t (,GL::EV (cons f (ec-call (kwote-lst args)))
                  nil)))))
        (table g-apply-table ',GL::NAME ',GL::FNS)))))
defapplymacro
(defmacro defapply
  (name fns)
  `(make-event (make-apply ',GL::NAME ',GL::FNS (w state))))
other
(logic)
other
(defthmd make-apply-open-nth
  (equal (nth n args)
    (if (zp n)
      (car args)
      (nth (1- n) (cdr args)))))
other
(defund mvfn (x y) (mv x y))
other
(defevaluator cadkw-ev
  cadkw-ev-lst
  ((car x) (cdr x)
    (len x)
    (kwote-lst x)
    (< x y)
    (nth n x)
    (cons x y)
    (nfix x)))
cadr-kwote-lst-count-cdrsfunction
(defun cadr-kwote-lst-count-cdrs
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (b* (((when (or (atom x) (not (eq (car x) 'cdr)))) (mv 0 x)) ((mv count final) (cadr-kwote-lst-count-cdrs (cadr x))))
    (mv (+ 1 count) final)))
other
(defthm natp-cadr-kwote-lst-count-cdrs
  (natp (mv-nth 0 (cadr-kwote-lst-count-cdrs x)))
  :rule-classes :type-prescription)
other
(local (include-book "arithmetic/top-with-meta" :dir :system))
other
(defthm cadr-kwote-lst-count-cdrs-correct
  (mv-let (n y)
    (cadr-kwote-lst-count-cdrs x)
    (equal (nthcdr n (cadkw-ev y a))
      (cadkw-ev x a)))
  :hints (("goal" :induct (cadr-kwote-lst-count-cdrs x))))
other
(defthm car-of-nthcdr
  (equal (car (nthcdr n x)) (nth n x)))
other
(defthm cadr-kwote-lst-count-cdrs-correct-nth
  (mv-let (n y)
    (cadr-kwote-lst-count-cdrs x)
    (equal (nth n (cadkw-ev y a))
      (car (cadkw-ev x a))))
  :hints (("goal" :use ((:instance car-of-nthcdr
        (n (mv-nth 0 (cadr-kwote-lst-count-cdrs x)))
        (x (cadkw-ev (mv-nth 1 (cadr-kwote-lst-count-cdrs x))
            a))))
     :in-theory (disable car-of-nthcdr))))
cadr-kwote-lst-meta-resfunction
(defun cadr-kwote-lst-meta-res
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (if (and (consp x) (eq (car x) 'car))
    (b* (((mv n kwote-lst-term) (cadr-kwote-lst-count-cdrs (cadr x))) ((unless (and (consp kwote-lst-term)
             (eq (car kwote-lst-term) 'kwote-lst))) x))
      `(cons 'quote
        (cons (nth ',GL::N ,(CADR GL::KWOTE-LST-TERM)) 'nil)))
    x))
cadr-kwote-lst-meta-hypfunction
(defun cadr-kwote-lst-meta-hyp
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (if (and (consp x) (eq (car x) 'car))
    (b* (((mv n kwote-lst-term) (cadr-kwote-lst-count-cdrs (cadr x))) ((unless (and (consp kwote-lst-term)
             (eq (car kwote-lst-term) 'kwote-lst))) 't))
      `(< (nfix ',GL::N) (len ,(CADR GL::KWOTE-LST-TERM))))
    't))
other
(in-theory (disable cadr-kwote-lst-count-cdrs
    car-of-nthcdr))
other
(defthm nth-of-kwote-lst-when-len
  (implies (< (nfix n) (len x))
    (equal (nth n (kwote-lst x))
      (list 'quote (nth n x)))))
other
(defthmd cadr-kwote-lst-meta-correct
  (implies (cadkw-ev (cadr-kwote-lst-meta-hyp x) a)
    (equal (cadkw-ev x a)
      (cadkw-ev (cadr-kwote-lst-meta-res x) a)))
  :hints (("goal" :use ((:instance cadr-kwote-lst-count-cdrs-correct-nth
        (x (cadr x))))
     :in-theory (disable cadr-kwote-lst-count-cdrs-correct-nth)))
  :rule-classes ((:meta :trigger-fns (car))))