Language.Fixpoint.Solver.Sanitize

Validate and Transform Constraints to Ensure various Invariants ------------------------- 1. Each binder must be associated with a UNIQUE sort

Transform FInfo to enforce invariants

sanitize :: Config -> SInfo a -> SanitizeM (SInfo a)

Sorts for each Symbol (move elsewhere)

symbolEnv :: Config -> SInfo a -> SymEnv

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

dropDeadSubsts removes dead `K[x := e]` where x NOT in the domain of K.