		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-common

Atc-check-symbol-3part

Check if a symbol consists of three parts separated by dash.

Signature
(atc-check-symbol-3part sym) → (mv yes/no part1 part2 part3)
Arguments: sym — Guard (symbolp sym).
Returns: yes/no — Type (booleanp yes/no).; part1 — Type (symbolp part1).; part2 — Type (symbolp part2).; part3 — Type (symbolp part3).

If the symbol has the form <part1>-<part2>-<part3>, with <part1> and <part2> and <part3> non-empty and without dashes, we return an indication of success and the three parts. Otherwise, we return an indication of failure and nil as the parts. The three returned symbols, when the function is successful, are interned in the same package as the input symbol.

Definitions and Theorems

Function: atc-check-symbol-3part

(defun atc-check-symbol-3part (sym)
  (declare (xargs :guard (symbolp sym)))
  (let ((__function__ 'atc-check-symbol-3part))
    (declare (ignorable __function__))
    (b* ((parts (str::strtok! (symbol-name sym)
                              (list #\-)))
         ((unless (= (len parts) 3))
          (mv nil nil nil nil))
         (part1 (intern-in-package-of-symbol (first parts)
                                             sym))
         (part2 (intern-in-package-of-symbol (second parts)
                                             sym))
         (part3 (intern-in-package-of-symbol (third parts)
                                             sym)))
      (mv t part1 part2 part3))))

Theorem: booleanp-of-atc-check-symbol-3part.yes/no

(defthm booleanp-of-atc-check-symbol-3part.yes/no
  (b* (((mv ?yes/no ?part1 ?part2 ?part3)
        (atc-check-symbol-3part sym)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-symbol-3part.part1

(defthm symbolp-of-atc-check-symbol-3part.part1
  (b* (((mv ?yes/no ?part1 ?part2 ?part3)
        (atc-check-symbol-3part sym)))
    (symbolp part1))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-symbol-3part.part2

(defthm symbolp-of-atc-check-symbol-3part.part2
  (b* (((mv ?yes/no ?part1 ?part2 ?part3)
        (atc-check-symbol-3part sym)))
    (symbolp part2))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-symbol-3part.part3

(defthm symbolp-of-atc-check-symbol-3part.part3
  (b* (((mv ?yes/no ?part1 ?part2 ?part3)
        (atc-check-symbol-3part sym)))
    (symbolp part3))
  :rule-classes :rewrite)