liquid-fixpoint-0.8.0.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Solver.Sanitize

Contents

Description

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

Synopsis

Transform FInfo to enforce invariants

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

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.