Schemalg-gen-x-z1...zm
Generate the list of variables (x z1 ... zm).
- Signature
(schemalg-gen-x-z1...zm x-a1...am x-x1...xn x y) → x-z1...zm
- Arguments
- x-a1...am — Guard (pseudo-term-listp x-a1...am).
- x-x1...xn — Guard (symbol-listp x-x1...xn).
- x — Guard (symbolp x).
- y — Guard (symbolp y).
- Returns
- x-z1...zm — A symbol-listp.
The zj variables replace the aj<x1,...,xn> terms
in some of the generated events.
If an aj<x1,...,xn> term is one of the xi variables,
and it is the only one that is that variable,
then zj is just xi.
In all other cases, zj is a freshly generated variable.
In particular, if m is n
and each aj<x1,...,xn> if xj,
we use x1, ..., xn as z1, ..., zm,
without generating new variable names.
Recall that the list x-a1..am
may contain x at any position (but just at one position),
not necessarily at the beginning.
We return a list x-a1...am
with x in the same position as x-a1...am,
and with each zj in the same position as aj<x1,...,xn>.
We go through the list of terms x-a1...am,
and handle each as follows.
If the term is a variable that differs from all the other terms
(we test this by checking membership in
the result of removing one occurrence from the list;
this is okay since the list is expected to be small),
then we leave it unchanged;
this applies to x in particular.
Otherwise, we generate a new variable,
having care that it is distinct
from the ones generated so far,
from all the ones in x-x1...xn,
and also from y
(because they are used in a theorem that includes y).
Definitions and Theorems
Function: schemalg-gen-x-z1...zm-aux
(defun schemalg-gen-x-z1...zm-aux
(terms-to-do vars-done x-a1...am x-x1...xn x y)
(declare (xargs :guard (and (pseudo-term-listp terms-to-do)
(symbol-listp vars-done)
(pseudo-term-listp x-a1...am)
(symbol-listp x-x1...xn)
(symbolp x)
(symbolp y))))
(let ((__function__ 'schemalg-gen-x-z1...zm-aux))
(declare (ignorable __function__))
(b*
(((when (endp terms-to-do)) nil)
(term (car terms-to-do))
(var
(if (and (symbolp term)
(not (member-eq term (remove1-eq term x-a1...am))))
term
(genvar x "VAR$" nil
(append vars-done x-x1...xn (list y))))))
(cons var
(schemalg-gen-x-z1...zm-aux (cdr terms-to-do)
(cons var vars-done)
x-a1...am x-x1...xn x y)))))
Function: schemalg-gen-x-z1...zm
(defun schemalg-gen-x-z1...zm (x-a1...am x-x1...xn x y)
(declare (xargs :guard (and (pseudo-term-listp x-a1...am)
(symbol-listp x-x1...xn)
(symbolp x)
(symbolp y))))
(let ((__function__ 'schemalg-gen-x-z1...zm))
(declare (ignorable __function__))
(schemalg-gen-x-z1...zm-aux
x-a1...am nil x-a1...am x-x1...xn x y)))
