		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-case-insensitive-string

A case-insensitive-string parse tree is abstracted to its character string and to a boolean flag saying whether the %i prefix is present or not.

Signature
(abstract-case-insensitive-string tree) → (mv charstring iprefix)
Arguments: tree — Guard (treep tree).
Returns: charstring — Type (common-lisp::stringp charstring).; iprefix — Type (booleanp iprefix).

Definitions and Theorems

Function: abstract-case-insensitive-string

(defun abstract-case-insensitive-string (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail) (mv "" nil)))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (and (consp treess)
                     (consp (cdr treess))))
        (fail))
       (trees (cadr treess))
       ((unless (consp trees)) (fail))
       (subtree (car trees))
       (charstring (abstract-quoted-string subtree))
       (trees (car treess))
       ((unless (consp trees)) (fail))
       (subtree (car trees))
       ((unless (tree-case subtree :nonleaf))
        (fail))
       (iprefix (consp (tree-nonleaf->branches subtree))))
    (mv charstring iprefix)))

Theorem: stringp-of-abstract-case-insensitive-string.charstring

(defthm stringp-of-abstract-case-insensitive-string.charstring
  (b* (((mv ?charstring ?iprefix)
        (abstract-case-insensitive-string tree)))
    (common-lisp::stringp charstring))
  :rule-classes :rewrite)

Theorem: booleanp-of-abstract-case-insensitive-string.iprefix

(defthm booleanp-of-abstract-case-insensitive-string.iprefix
  (b* (((mv ?charstring ?iprefix)
        (abstract-case-insensitive-string tree)))
    (booleanp iprefix))
  :rule-classes :rewrite)