		Search-engine friendly clone of the ACL2 documentation.

Plexeme

Plexeme-kind

Get the kind (tag) of a plexeme structure.

Signature
(plexeme-kind x) → kind
Arguments: x — Guard (plexemep x).

Definitions and Theorems

Function: plexeme-kind$inline

(defun plexeme-kind$inline (x)
  (declare (xargs :guard (plexemep x)))
  (mbe :logic (cond ((or (atom x) (eq (car x) :header))
                     :header)
                    ((eq (car x) :ident) :ident)
                    ((eq (car x) :number) :number)
                    ((eq (car x) :char) :char)
                    ((eq (car x) :string) :string)
                    ((eq (car x) :punctuator) :punctuator)
                    ((eq (car x) :other) :other)
                    ((eq (car x) :block-comment)
                     :block-comment)
                    ((eq (car x) :line-comment)
                     :line-comment)
                    ((eq (car x) :newline) :newline)
                    ((eq (car x) :spaces) :spaces)
                    ((eq (car x) :horizontal-tab)
                     :horizontal-tab)
                    ((eq (car x) :vertical-tab)
                     :vertical-tab)
                    (t :form-feed))
       :exec (car x)))

Theorem: plexeme-kind-possibilities

(defthm plexeme-kind-possibilities
  (or (equal (plexeme-kind x) :header)
      (equal (plexeme-kind x) :ident)
      (equal (plexeme-kind x) :number)
      (equal (plexeme-kind x) :char)
      (equal (plexeme-kind x) :string)
      (equal (plexeme-kind x) :punctuator)
      (equal (plexeme-kind x) :other)
      (equal (plexeme-kind x) :block-comment)
      (equal (plexeme-kind x) :line-comment)
      (equal (plexeme-kind x) :newline)
      (equal (plexeme-kind x) :spaces)
      (equal (plexeme-kind x) :horizontal-tab)
      (equal (plexeme-kind x) :vertical-tab)
      (equal (plexeme-kind x) :form-feed))
  :rule-classes
  ((:forward-chaining :trigger-terms ((plexeme-kind x)))))