Filtering...

computed-hint

books/misc/computed-hint
other
(in-package "ACL2")
other
(program)
use-hint-alwaysmacro
(defmacro use-hint-always (&rest hint) `',HINT)
when-occurmacro
(defmacro when-occur
  (term &rest hint)
  `(and (occur-lst ',TERM clause) ',HINT))
when-occur-&macro
(defmacro when-occur-&
  (term hint)
  `(and (occur-lst ',TERM clause) ,HINT))
multiple-occur-checkfunction
(defun multiple-occur-check
  (terms clause)
  (if (endp terms)
    nil
    (if (endp (cdr terms))
      (occur-lst (car terms) clause)
      (and (occur-lst (car terms) clause)
        (multiple-occur-check (cdr terms) clause)))))
when-multiple-occurmacro
(defmacro when-multiple-occur
  (terms &rest hint)
  `(and (multiple-occur-check ',TERMS clause) ',HINT))
when-multiple-occur-&macro
(defmacro when-multiple-occur-&
  (terms hint)
  `(and (multiple-occur-check ',TERMS clause) ,HINT))
show-hintmacro
(defmacro show-hint
  (hint &optional marker)
  (cond ((and (consp hint) (stringp (car hint))) hint)
    (t `(let ((marker ,MARKER) (ans ,(IF (SYMBOLP HINT)
     `(,HINT ID CLAUSE WORLD)
     HINT)))
        (if ans
          (prog2$ (cw "~%***** Computed Hint~#0~[~/ (from hint ~x1)~]****~%~x2~%~%"
              (if (null marker)
                0
                1)
              marker
              (cons (string-for-tilde-@-clause-id-phrase id) ans))
            ans)
          nil)))))
fmeta-varpfunction
(defun fmeta-varp
  (x)
  (and (equal (car x) '@) (symbolp (cadr x))))
fmeta-var-namefunction
(defun fmeta-var-name (x) (cadr x))
mv2-ormacro
(defmacro mv2-or
  (first second)
  `(mv-let (flg val)
    ,FIRST
    (if flg
      (mv flg val)
      ,SECOND)))
pattern-matchmutual-recursion
(mutual-recursion (defun pattern-match
    (pattern term subst)
    (cond ((variablep pattern) (if (eq pattern term)
          (mv t subst)
          (mv nil nil)))
      ((fquotep pattern) (if (equal pattern term)
          (mv t subst)
          (mv nil nil)))
      ((fmeta-varp pattern) (let ((inst (assoc-eq (fmeta-var-name pattern) subst)))
          (if inst
            (if (equal term (cdr inst))
              (mv t subst)
              (mv nil nil))
            (mv t (cons (cons (fmeta-var-name pattern) term) subst)))))
      ((and (not (variablep term))
         (not (fquotep term))
         (eq (ffn-symb pattern) (ffn-symb term))) (pattern-match-lst (fargs pattern) (fargs term) subst))
      (t (mv nil nil))))
  (defun pattern-match-lst
    (patterns terms subst)
    (cond ((and (null patterns) (null terms)) (mv t subst))
      ((or (null patterns) (null terms)) (mv nil nil))
      (t (mv-let (flg new-subst)
          (pattern-match (car patterns) (car terms) subst)
          (if flg
            (pattern-match-lst (cdr patterns) (cdr terms) new-subst)
            (mv nil nil)))))))
pattern-occurmutual-recursion
(mutual-recursion (defun pattern-occur
    (pattern term subst)
    (if (or (variablep term) (fquotep term))
      (pattern-match pattern term subst)
      (mv2-or (pattern-match pattern term subst)
        (pattern-occur-lst pattern (fargs term) subst))))
  (defun pattern-occur-lst
    (patterns args subst)
    (cond ((null args) (mv nil nil))
      (t (mv2-or (pattern-occur patterns (car args) subst)
          (pattern-occur-lst patterns (cdr args) subst))))))
subst-metamutual-recursion
(mutual-recursion (defun subst-meta
    (pattern subst)
    (cond ((or (variablep pattern) (fquotep pattern)) pattern)
      ((fmeta-varp pattern) (let ((inst (assoc-eq (fmeta-var-name pattern) subst)))
          (if inst
            (cdr inst)
            pattern)))
      (t (subst-meta-lst pattern subst))))
  (defun subst-meta-lst
    (patterns subst)
    (if (null patterns)
      nil
      (cons (subst-meta (car patterns) subst)
        (subst-meta-lst (cdr patterns) subst)))))
when-patternmacro
(defmacro when-pattern
  (term &rest hint)
  `(mv-let (flg subst)
    (pattern-occur-lst ',TERM clause nil)
    (if flg
      (subst-meta ',HINT subst)
      nil)))
multiple-pattern-checkfunction
(defun multiple-pattern-check
  (terms)
  (if (endp terms)
    nil
    (if (endp (cdr terms))
      `(pattern-occur-lst ',(CAR TERMS) clause nil)
      `(mv-let (flg subst)
        ,(MULTIPLE-PATTERN-CHECK (CDR TERMS))
        (if flg
          (pattern-occur-lst ',(CAR TERMS) clause subst)
          (mv nil nil))))))
when-multi-patternsmacro
(defmacro when-multi-patterns
  (terms &rest hint)
  `(mv-let (flg subst)
    ,(MULTIPLE-PATTERN-CHECK (REVERSE TERMS))
    (if flg
      (subst-meta ',HINT subst)
      nil)))
when-gs-matchmacro
(defmacro when-gs-match
  (spec-pattern &rest hint)
  `(and (gs-pattern-match id ',SPEC-PATTERN) ',HINT))
when-gs-match-&macro
(defmacro when-gs-match-&
  (spec-pattern hint)
  `(and (gs-pattern-match id ',SPEC-PATTERN) ,HINT))
when-not-gs-matchmacro
(defmacro when-not-gs-match
  (spec-pattern &rest hint)
  `(and (not (gs-pattern-match id ',SPEC-PATTERN)) ',HINT))
when-not-gs-match-&macro
(defmacro when-not-gs-match-&
  (spec-pattern hint)
  `(and (not (gs-pattern-match id ',SPEC-PATTERN)) ,HINT))
gsnum-pattern-matchfunction
(defun gsnum-pattern-match
  (id pattern)
  (or (equal pattern '*) (equal id pattern)))
gslist-pattern-matchfunction
(defun gslist-pattern-match
  (id pattern)
  (if (atom pattern)
    (if (equal pattern '*)
      t
      (equal id pattern))
    (if (atom id)
      nil
      (and (gsnum-pattern-match (car id) (car pattern))
        (gslist-pattern-match (cdr id) (cdr pattern))))))
gs-pattern-matchfunction
(defun gs-pattern-match
  (id pattern)
  (and (gslist-pattern-match (car id) (car pattern))
    (gslist-pattern-match (cadr id) (cadr pattern))
    (gsnum-pattern-match (cddr id) (cddr pattern))))
show-clausemacro
(defmacro show-clause
  (hint)
  (cond ((and (consp hint) (stringp (car hint))) hint)
    (t `(let ((ans ,(IF (SYMBOLP HINT)
     `(,HINT ID CLAUSE WORLD)
     HINT)))
        (prog2$ (cw "~%***** Computed Hint~x0~%~x1~%~%"
            clause
            (cons (string-for-tilde-@-clause-id-phrase id) ans))
          (if ans
            ans
            nil))))))
when-occur-positivemacro
(defmacro when-occur-positive
  (literal &rest hint)
  `(and (member-equal ',LITERAL clause) ',HINT))
when-occur-negativemacro
(defmacro when-occur-negative
  (literal &rest hint)
  `(and (member-equal '(not ,LITERAL) clause) ',HINT))
when-occur-positive-&macro
(defmacro when-occur-positive-&
  (literal hint)
  `(and (member-equal ',LITERAL clause) ,HINT))
when-occur-negative-&macro
(defmacro when-occur-negative-&
  (literal hint)
  `(and (member-equal '(not ,LITERAL) clause) ,HINT))
pattern-positive-pfunction
(defun pattern-positive-p
  (lit clause subst)
  (if (endp clause)
    (mv nil nil)
    (mv2-or (pattern-match lit (car clause) subst)
      (pattern-positive-p lit (cdr clause) subst))))
pattern-negative-pfunction
(defun pattern-negative-p
  (lit clause subst)
  (if (endp clause)
    (mv nil nil)
    (mv2-or (pattern-match `(not ,LIT) (car clause) subst)
      (pattern-negative-p lit (cdr clause) subst))))
multi-patterns-positive-pfunction
(defun multi-patterns-positive-p
  (lts clause subst)
  (if (endp lts)
    (mv t subst)
    (mv-let (flag new-subst)
      (pattern-positive-p (car lts) clause subst)
      (if flag
        (multi-patterns-positive-p (cdr lts) clause new-subst)
        (mv nil nil)))))
multi-patterns-negative-pfunction
(defun multi-patterns-negative-p
  (lts clause subst)
  (if (endp lts)
    (mv t subst)
    (mv-let (flag new-subst)
      (pattern-negative-p (car lts) clause subst)
      (if flag
        (multi-patterns-negative-p (cdr lts) clause new-subst)
        (mv nil nil)))))
multi-patterns-asserted-pfunction
(defun multi-patterns-asserted-p
  (plit nlit clause subst)
  (mv-let (flg new-subst)
    (multi-patterns-positive-p plit clause subst)
    (if flg
      (multi-patterns-negative-p nlit clause new-subst)
      (mv nil nil))))
when-pos/neg-occurmacro
(defmacro when-pos/neg-occur
  (plit nlit &rest hint)
  `(mv-let (flg subst)
    (multi-patterns-asserted-p ',PLIT ',NLIT clause nil)
    (if flg
      (subst-meta ',HINT subst)
      nil)))