| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Solver.Sanitize
Contents
Description
Validate and Transform Constraints to Ensure various Invariants ------------------------- 1. Each binder must be associated with a UNIQUE sort
Transform FInfo to enforce invariants
Sorts for each Symbol (move elsewhere)
symbolEnv :: Config -> SInfo a -> SymEnv Source #
symbol |-> sort for EVERY variable in the SInfo; symbolEnv can ONLY be
called with **sanitized** environments (post the uniqification etc.) or
else you get duplicate sorts and other such errors.
We do this peculiar dance with env0 to extract the apply-sorts from the
function definitions inside the AxiomEnv which cannot be elaborated as
it makes it hard to actually find the fundefs within (breaking PLE.)
Remove substitutions K[x := e] where x is not in dom(K)
dropDeadSubsts :: SInfo a -> SInfo a Source #
dropDeadSubsts removes dead `K[x := e]` where x NOT in the domain of K.