liquid-fixpoint-0.7.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 :: 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.

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.