|
|
|---|
|
|
|
|---|
recognizer for the quotation of a term
Example: (termp '(CAR (CONS X Y)) (w state)) General Form: (termp x w)
where
Each metafunction (see meta) is supposed to take (the quotation of)
a translated term as input and yield (the quotation of) a translated term as
output. When a metafunction is run by the simplifier its input is guaranteed
to be well-formed by invariants maintained by ACL2. But its output is checked
by an explicit call of
Termp is mutually recursive with term-listp.
Function:
(defun termp (x w) (declare (xargs :guard (plist-worldp-with-formals w))) (cond ((atom x) (legal-variablep x)) ((eq (car x) 'quote) (and (consp (cdr x)) (null (cddr x)))) ((symbolp (car x)) (let ((arity (arity (car x) w))) (and arity (term-listp (cdr x) w) (eql (length (cdr x)) arity)))) ((and (consp (car x)) (true-listp (car x)) (eq (car (car x)) 'lambda) (eql 3 (length (car x))) (arglistp (cadr (car x))) (termp (caddr (car x)) w) (null (set-difference-eq (all-vars (caddr (car x))) (cadr (car x)))) (term-listp (cdr x) w) (eql (length (cadr (car x))) (length (cdr x)))) t) (t nil)))
Function:
(defun term-listp (x w) (declare (xargs :guard (plist-worldp-with-formals w))) (cond ((atom x) (equal x nil)) ((termp (car x) w) (term-listp (cdr x) w)) (t nil)))