		Search-engine friendly clone of the ACL2 documentation.

Mlib

Expr-tools

Basic functions for working with expressions.

Subtopics

Vl-expr-typedecide: Determine the arithmetic class (signed or unsigned integer, shortreal or real, or something else) of an top-level or self-determined expression.
Vl-exprlist-resolved->vals: (vl-exprlist-resolved->vals x) maps vl-resolved->val across a list.
Vl-make-idexpr-list: (vl-make-idexpr-list x) maps vl-idexpr across a list.
Vl-idexprlist->names: (vl-idexprlist->names x) maps vl-idexpr->name across a list.
Vl-expr-selfsize: Computation of self-determined expression sizes.
Vl-expr-update-subexprs
Vl-exprlist-to-plainarglist: Convert expressions into vl-plainarg-ps.
Vl-call-namedargs-update-subexprs
Vl-valuerangelist-update-subexprs
Vl-streamexprlist-update-subexprs
Vl-op-p
Vl-maybe-exprlist-update-subexprs
Vl-evatomlist-update-subexprs
Vl-expr-values: Gather all of the values throughout an expression.
Vl-keyvallist-update-subexprs
Vl-assignpat-update-subexprs
Vl-valuerange-update-subexprs
Vl-scopeexpr-update-subexprs
Vl-partselect-update-subexprs
Vl-hidexpr-update-subexprs
Vl-expr-add-atts
Vl-arrayrange-update-subexprs
Vl-streamexpr-update-subexprs
Vl-slicesize-update-subexprs
Vl-plusminus-update-subexprs
Vl-patternkey-update-subexprs
Vl-expr-ops: Gather all of the operators used throughout an expression.
Vl-make-integer: Safely create a well-typed constant integer atom whose value is n.
Vl-range-update-subexprs
Vl-idexpr: Construct an vl-idexpr-p.
Vl-make-index: Safely create a constant integer atom whose value is n.
Vl-expr->subexprs
Vl-bitlist-from-nat: Turn a natural number into a vl-bitlist-p of the given width.
Vl-pps-expr: Pretty-print an expression into a string.
Vl-maybe-exprlist->subexprs
Vl-hidexpr->subexprs
Vl-evatomlist->subexprs
Vl-call-namedargs->subexprs
Vl-valuerangelist->subexprs
Vl-streamexprlist->subexprs
Vl-keyvallist->subexprs
Vl-exprlist-has-ops
Vl-expr-resolved-p: Recognizes plain constant integer expressions.
Vl-valuerange->subexprs
Vl-streamexpr->subexprs
Vl-slicesize->subexprs
Vl-scopeexpr->subexprs
Vl-patternkey->subexprs
Vl-partselect->subexprs
Vl-assignpat->subexprs
Vl-arrayrange->subexprs
Vl-pps-origexpr: Pretty-print the "original," un-transformed version of an expression into a string.
Vl-plusminus->subexprs
Vl-idscope
Vl-idexpr->name: Get the name from a vl-idexpr-p.
Vl-expr-has-ops
Vl-resolved->val: Get the value from a resolved expression.
Vl-range->subexprs
Vl-idexpr-p: Recognize plain identifier expressions.
Vl-idexprlist-p: (vl-idexprlist-p x) recognizes lists where every element satisfies vl-idexpr-p.
Vl-exprlist-resolved-p: (vl-exprlist-resolved-p x) recognizes lists where every element satisfies vl-expr-resolved-p.
Vl-idscope->name
Vl-idscope-p: Recognize a scopeexpr that is just a plain identifier.
Vl-zbitlist-p
Vl-zatom-p
Vl-op-fix
Vl-oplist: A list of vl-op-p objects.
Vl-expr-varnames: Extract all the variable names from a VL expression.
Vl-one-bit-constants: Already-sized, one-bit constants.