		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-group-coordinate

Abstract a group-coordinate to a group literal coordinate.

Signature
(abs-group-coordinate tree) → coor
Arguments: tree — Guard (abnf::treep tree).
Returns: coor — Type (coordinate-resultp coor).

Definitions and Theorems

Function: abs-group-coordinate

(defun abs-group-coordinate (tree)
 (declare (xargs :guard (abnf::treep tree)))
 (let ((__function__ 'abs-group-coordinate))
  (declare (ignorable __function__))
  (b* (((okf tree)
        (abnf::check-tree-nonleaf-1-1 tree "group-coordinate")))
   (if (abnf::tree-case tree :nonleaf)
       (b* (((okf (abnf::tree-list-tuple2 sub))
             (abnf::check-tree-nonleaf-2 tree nil))
            ((okf num-tree)
             (abnf::check-tree-list-1 sub.2nd))
            ((okf nat) (abs-numeral num-tree))
            ((okf opt-dash-tree)
             (abnf::check-tree-list-1 sub.1st))
            ((okf opt-dash-sub)
             (abnf::check-tree-nonleaf opt-dash-tree nil))
            ((when (endp opt-dash-sub))
             (coordinate-explicit nat))
            ((okf dash-trees)
             (abnf::check-tree-list-list-1 opt-dash-sub))
            ((okf dash-tree)
             (abnf::check-tree-list-1 dash-trees))
            ((okf &)
             (abnf::check-tree-ichars dash-tree "-")))
         (coordinate-explicit (- nat)))
    (b* (((okf nats)
          (abnf::check-tree-leafterm tree)))
     (cond
      ((abnf::nats-match-insensitive-chars-p nats (list #\+))
       (coordinate-sign-high))
      ((abnf::nats-match-insensitive-chars-p nats (list #\-))
       (coordinate-sign-low))
      ((abnf::nats-match-insensitive-chars-p nats (list #\_))
       (coordinate-inferred))
      (t
       (reserrf
        (list
            :found-subtree (abnf::tree-info-for-error tree))))))))))

Theorem: coordinate-resultp-of-abs-group-coordinate

(defthm coordinate-resultp-of-abs-group-coordinate
  (b* ((coor (abs-group-coordinate tree)))
    (coordinate-resultp coor))
  :rule-classes :rewrite)

Theorem: abs-group-coordinate-of-tree-fix-tree

(defthm abs-group-coordinate-of-tree-fix-tree
  (equal (abs-group-coordinate (abnf::tree-fix tree))
         (abs-group-coordinate tree)))

Theorem: abs-group-coordinate-tree-equiv-congruence-on-tree

(defthm abs-group-coordinate-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (abs-group-coordinate tree)
                  (abs-group-coordinate tree-equiv)))
  :rule-classes :congruence)