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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Solver.Validate

Contents

Description

Validate and Transform Constraints to Ensure various Invariants ------------------------- 1. Each binder must be unique

Synopsis

Validate and Transform FInfo to enforce invariants

validate :: Config -> FInfo a -> Either Error (FInfo a) Source

Sorts for each Symbol

symbolSorts :: FInfo a -> Either Error [(Symbol, Sort)] Source

symbol |-> sort for EVERY variable in the FInfo