		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Path-to-var

Extract a variable from a path.

Signature
(path-to-var path) → var
Arguments: path — Guard (pathp path).
Returns: var — Type (identifier-resultp var).

As in the static semantics, also in the dynamic semantics we require a path to consist of a single identifier. This ACL2 function makes that check, returning the identifier. This is the variable denoted by the path.

Definitions and Theorems

Function: path-to-var

(defun path-to-var (path)
  (declare (xargs :guard (pathp path)))
  (let ((__function__ 'path-to-var))
    (declare (ignorable __function__))
    (b* ((idens (path->get path))
         ((unless (consp idens))
          (reserrf (list :empty-path (path-fix path))))
         ((unless (endp (cdr idens)))
          (reserrf (list :non-singleton-path (path-fix path))))
         (var (car idens)))
      var)))

Theorem: identifier-resultp-of-path-to-var

(defthm identifier-resultp-of-path-to-var
  (b* ((var (path-to-var path)))
    (identifier-resultp var))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-path-to-var

(defthm error-info-wfp-of-path-to-var
  (b* ((?var (path-to-var path)))
    (implies (reserrp var)
             (error-info-wfp var))))

Theorem: path-to-var-of-path-fix-path

(defthm path-to-var-of-path-fix-path
  (equal (path-to-var (path-fix path))
         (path-to-var path)))

Theorem: path-to-var-path-equiv-congruence-on-path

(defthm path-to-var-path-equiv-congruence-on-path
  (implies (path-equiv path path-equiv)
           (equal (path-to-var path)
                  (path-to-var path-equiv)))
  :rule-classes :congruence)