Env
A C environment mapping identifiers to values.
This is implemented as a stack of maps. Blocks within the stack
correspond to nested scopes within C. Entries within higher blocks
shadow those in the lower blocks.
Subtopics
- Envp
- (envp x) recognizes lists where every element satisfies env-blockp.
- Env-fix
- (env-fix x) is a usual ACL2::fty list fixing function.
- Union-env
- Take the conservative union of two environments.
- Env-equiv
- Basic equivalence relation for env structures.
- Write-env
- Overwrite the value of a variable.
- Declare-var-env
- Declare a new variables within the environment.
- Read-env
- Retrieve the value of a variable.
- Push-scope-env
- Push a new scope block to the top of the environment.
- In-scope-env
- Check whether a variable is in scope.
- Pop-scope-env
- Pop a scope block from the top of the environment.
- Merge-block-env
- Update the top block of the environment with the specified scope block.
- Env-block
- A scope block within an environment.
