Fancy-ev
Term evaluator used by FGL for syntaxp, bind-free, and syntax-bind interpretation.
- Signature
(fancy-ev x alist reclimit interp-st state hard-errp aokp)
→
(mv errmsg val new-interp-st new-state)
- Arguments
- x — Guard (pseudo-termp x).
- alist — Guard (symbol-alistp alist).
- reclimit — Guard (natp reclimit).
- interp-st — Guard (interp-st-bfrs-ok interp-st).
Fancy-ev is a term evaluator capable of running terms that include functions
that access the FGL interpreter state and the ACL2 state, and even may modify
the FGL interpreter state in limited ways. It is used for evaluating syntaxp,
bind-free, and syntax-bind forms in the FGL rewriter.
Fancy-ev uses magic-ev-fncall to allow it to run most functions that
do not access stobjs. When magic-ev-fncall fails, it can also expand function
definitions and interpret their bodies. But additionally, it calls an
attachable function fancy-ev-primitive to allow it to directly execute
functions that access and/or modify the ACL2 state and FGL interp-st.
To allow a function my-fn that accesses/updates interp-st or
state to be executable by fancy-ev, there are two steps:
- (fancy-ev-add-primitive my-fn guard-form) checks that the function
is valid as a fancy-ev primitive and that guard-form suffices to check that the
function's guard is satisfied when provided an interp-st satisfying
interp-st-bfrs-ok. If so, the function/guard pair is recorded in the
table fancy-ev-primitives for later use by
def-fancy-ev-primitives.
- (def-fancy-ev-primitives my-fancy-ev-primitives-impl) defines a
function named my-fancy-ev-primitives-impl and attaches it to
fancy-ev-primitive. The function is defined as a case statement on the
input function symbol where for each function/guard pair in the
fancy-ev-primitives table, if the input function symbol matches that
function, it checks the given guard form and then executes the function on the
input arguments, returning its return value list and modified interp-st (if
any). This allows all functions that were added using
fancy-ev-add-primitive to be executed by fancy-ev.
Note that fancy-ev primitives cannot invoke fancy-ev. However, a term
evaluated in fancy-ev can invoke fancy-ev (though the recursive call limit and
hard-errp/aokp flags from the term are ignored).
See also fancy-translate.
Subtopics
- Fancy-translate
- Pseudo-translate an ACL2 form into a term using fancy-ev to evaluate macros.
