		Search-engine friendly clone of the ACL2 documentation.

Vl-context

Ctxexprs

Functions for gathering expressions and the context in which they occur.

Like the allexprs family of functions, these functions gather up what we regard as the "top level" expressions used throughout some module. But whereas the allexprs functions just return flat lists of expressions, we return a vl-ctxexprlist that associates each expression with a vl-context-p describing its origin.

Subtopics

Vl-exprlist-ctxexprs: Bind some expressions to their context.
Vl-paramdecllist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-paramdecllist-ps.
Vl-vardecllist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-vardecllist-ps.
Vl-typedeflist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-typedeflist-ps.
Vl-taskdecllist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-taskdecllist-ps.
Vl-portdecllist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-portdecllist-ps.
Vl-modinstlist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-modinstlist-ps.
Vl-initiallist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-initiallist-ps.
Vl-gateinstlist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-gateinstlist-ps.
Vl-fundecllist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-fundecllist-ps.
Vl-assignlist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-assignlist-ps.
Vl-alwayslist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-alwayslist-ps.
Vl-portlist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-portlist-ps.
Vl-aliaslist-ctxexprs: Collect up a vl-ctxexprlist-p from a list of vl-aliaslist-ps.
Vl-portdecl-ctxexprs
Vl-paramdecl-ctxexprs
Vl-gateinst-ctxexprs
Vl-vardecl-ctxexprs
Vl-typedef-ctxexprs
Vl-modinst-ctxexprs
Vl-port-ctxexprs
Vl-assign-ctxexprs
Vl-alias-ctxexprs