Pseudo-term-fty
Overview of FTY support for pseudo-terms.
The book "clause-processors/pseudo-term-fty" defines a fixing
function and convenient accessors and constructors for fty-discipline support for pseudo-terms. It also provides macros that
generate appropriate theorems about evaluators allowing them to understand the
new accessors and constructors.
Usage
We treat the pseudo-term type as a sum of five kinds of products:
- :null, encompassing the unique pseudo-term NIL as well as
(ill-formed) non-symbol atoms and calls with non-symbol atom function names;
has no field
- :var, encompassing non-nil symbols; field: name
- :quote, conses whose car is quote; field: val
- fncall, conses whose car is a non-quote symbol; fields: fn and args
- lambda, conses whose car is a cons; fields: formals, body, and args.
Each of these product kinds has a constructor that uses the typical naming
convention; e.g., to make a lambda, use (pseudo-term-lambda formals body
args). The accessors also use the usual naming convention (e.g.,
pseudo-term-var->name). There is also a b* binder for each such
constructor that allows access to the fields using dotted notation; e.g.:
(b* (((pseudo-lambda x))) (list x.formals x.body x.args))
An alternative constructor (pseudo-term-call fn args) can create either
:fncall or :lambda kinds; its fn argument is of type pseudo-fn which can be either a function symbol (pseudo-fnsym) or
lambda (pseudo-lambda). The function of a :fncall or
:lambda object can also be accessed with pseudo-term-call->fn.
The :null and :quote kinds both simply have constant values. A
function pseudo-term-const->val is provided that accesses that value; that
is, it returns the value of a :quote object or NIL for a :null
object. We don't provide a constructor pseudo-term-const since
pseudo-term-quote will do just as well.
The macro pseudo-term-case can be used to conveniently branch on the kind
of term and access the fields; see its documentation for examples.
Evaluator support
The macro def-ev-pseudo-term-fty-support admits several theorems about an evaluator, enabling reasoning about evaluation over the provided constructors and accessors. See its documentation for details.
Another macro, def-ev-pseudo-term-congruence, admits only a subset of the theorems produced by def-ev-pseudo-term-fty-support, proving a pseudo-term-equiv congruence for the evaluator but no rules pertaining to the FTY-style accessors and updaters.
Subtopics
- Pseudo-term-lambda
- Constructor for a lambda call (:lambda) pseudo-term.
- Pseudo-term-call
- Constructor that produces either a function call or lambda call pseudo-term,
depending whether the given function is a function symbol or lambda.
- Pseudo-term-fncall
- Constructor for function call (:fncall) pseudo-terms.
- Pseudo-lambda
- Type of, and constructor for, a lambda function, used in the FTY support for pseudo-terms.
- Pseudo-term-var
- Constructor for variable (:var) pseudo-terms.
- Pseudo-term-quote
- Constructor for :quote pseudo-terms.
- Pseudo-term-kind
- Return the kind of a pseudo-term input (a keyword symbol).
- Pseudo-term-null
- Constructor for null pseudo-terms. Just returns NIL.
- Pseudo-fnsym
- Type of a function symbol used in the FTY support for pseudo-terms.
- Pseudo-term-case
- Case macro for pseudo-term objects.
- Pseudo-term-count
- Measure for recursion over pseudo-terms
- Def-ev-pseudo-term-fty-support
- Admit theorems about an evaluator that allow reasoning about FTY-style
accessors and constructors for pseudo-terms.
- Def-ev-pseudo-term-congruence
- Prove that pseudo-term-fix is transparent to an evaluator and
that the evaluator thus has a pseudo-term-equiv congruence on its
first argument.
- Pseudo-term-fix
- Fixing function for pseudo-terms that supports FTY-style discipline
and is transparent to evaluators.
- Pseudo-var
- Type of a variable symbol used in the FTY support for pseudo-terms.
- Pseudo-term-list-fix
- Fixing function for pseudo-term lists that supports FTY-style discipline
and is transparent to evaluators.
- Pseudo-fn
- Type of a function (either symbol or lambda), used in pseudo-term FTY support.
