Language.Fixpoint.Solver.Validate

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

Transform FInfo to enforce invariants

sanitize :: SInfo a -> ValidateM (SInfo a)

Sorts for each Symbol

symbolSorts :: GInfo c a -> ValidateM [(Symbol, Sort)]

Conservative check that KVars appear at "top-level" in pred isOkRhs :: F.Pred -> Bool isOkRhs p = all isKvar ps || all isConc ps where ps = F.conjuncts p

symbol |-> sort for EVERY variable in the FInfo