		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucidstate

State for the lucid transform.

This is a product type introduced by defprod.

Fields

Main database mapping keys to their use/set occurrences.

paramsp — booleanp

Should we issue warnings for parameters? It generally will only make sense to do this before unparameterization has taken place, because unparameterization should generally get rid of any sensible parameters.

generatesp — booleanp

Should we include multidrive warnings in generates? It will generally only make sense to do this after unparameterization, because until then things like

if (condition) assign foo = 1;
                   else assign foo = 0;

may appear to be multiple assignments to foo, even though they never happen at the same time.

warnings — vl-warninglist

Subtopics

Vl-lucidstate-p: Recognizer for vl-lucidstate structures.
Vl-lucidstate-fix: Fixing function for vl-lucidstate structures.
Vl-lucidval: Use/set information about a single variable.
Vl-lucidocc: Record of an occurrence of an identifier.
Vl-lucidkey: A single key in the lucid database.
Vl-lucidstate-equiv: Basic equivalence relation for vl-lucidstate structures.
Make-vl-lucidstate: Basic constructor macro for vl-lucidstate structures.
Vl-lucidstate->warnings: Get the warnings field from a vl-lucidstate.
Vl-lucidstate->generatesp: Get the generatesp field from a vl-lucidstate.
Vl-luciddb-count
Vl-lucidstate->paramsp: Get the paramsp field from a vl-lucidstate.
Change-vl-lucidstate: Modifying constructor for vl-lucidstate structures.
Vl-lucidstate->db: Get the db field from a vl-lucidstate.
Vl-lucidocc->ctx
Vl-lucidocc->ss
Vl-luciddb: The main lucid database. Binds keys (scopestack/item pairs) to information about how they have been used.
Vl-lucidocclist: A list of vl-lucidocc-p objects.
Vl-lucidkeylist: A list of vl-lucidkey-p objects.