Language.Fixpoint.Types.Constraints

This module contains the top-level query data types and elements, including (Horn) implication & well-formedness constraints and sets.

Top-level Queries

type FInfo a = GInfo SubC a

Top-level Queries

type SInfo a = GInfo SimpC a

data GInfo c a

Constructors

FI

Fields

cm :: HashMap Integer (c a)

ws :: HashMap KVar (WfC a)

bs :: !BindEnv

lits :: !(SEnv Sort)

kuts :: Kuts

quals :: ![Qualifier]

bindInfo :: HashMap BindId a

fileName :: FilePath

allowHO :: !Bool

Instances

Functor c => Functor (GInfo c)

PTable (SInfo a)

SymConsts (FInfo a)

Inputable (FInfo ())

(Eq a, Eq (c a)) => Eq (GInfo c a)

(Show a, Show (c a), Fixpoint a) => Show (GInfo c a)

Generic (GInfo c a)

Monoid (GInfo c a)

(Binary (c a), Binary a) => Binary (GInfo c a)

(NFData (c a), NFData a) => NFData (GInfo c a)

type Rep (GInfo c a)

convertFormat :: Fixpoint a => FInfo a -> SInfo a

Query Conversions: FInfo to SInfo

type Solver a = Config -> FInfo a -> IO (Result (Integer, a))

Top level Solvers ----------------------------------------------------

Serializing

toFixpoint :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> Doc

Rendering Queries

writeFInfo :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> FilePath -> IO ()

saveQuery :: Config -> FInfo a -> IO ()

Constructing Queries

fi :: [SubC a] -> [WfC a] -> BindEnv -> SEnv Sort -> Kuts -> [Qualifier] -> HashMap BindId a -> FilePath -> Bool -> GInfo SubC a

Constructing Queries

Constraints

data WfC a

Constructors

WfC

Fields

wenv :: !IBindEnv

wrft :: (Symbol, Sort, KVar)

winfo :: !a

Instances

Functor WfC

Eq a => Eq (WfC a)

Fixpoint a => Show (WfC a)

Generic (WfC a)

Binary a => Binary (WfC a)

NFData a => NFData (WfC a)

Fixpoint a => PPrint (WfC a)

Fixpoint a => Fixpoint (WfC a)

type Rep (WfC a)

data SubC a

Instances

Functor SubC

TaggedC SubC a

Eq a => Eq (SubC a)

Fixpoint a => Show (SubC a)

Generic (SubC a)

Binary a => Binary (SubC a)

NFData a => NFData (SubC a)

Fixpoint a => PPrint (SubC a)

(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a))

Fixpoint a => Fixpoint (SubC a)

SymConsts (FInfo a)

SymConsts (SubC a)

Inputable (FInfo ())

type Rep (SubC a)

mkSubC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a

subcId :: TaggedC c a => c a -> Integer

slhs :: SubC a -> SortedReft

srhs :: SubC a -> SortedReft

subC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a]

wfC :: Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]

"Smart Constructors" for Constraints ---------------------------------

data SimpC a

Constructors

SimpC

Fields

_cenv :: !IBindEnv

_crhs :: !Expr

_cid :: !(Maybe Integer)

_ctag :: !Tag

_cinfo :: !a

Instances

Functor SimpC

TaggedC SimpC a

Fixpoint a => Show (SimpC a)

Generic (SimpC a)

Binary a => Binary (SimpC a)

NFData a => NFData (SimpC a)

PTable (SInfo a)

Fixpoint a => PPrint (SimpC a)

Fixpoint a => Fixpoint (SimpC a)

type Rep (SimpC a)

type Tag = [Int]

Constraints ---------------------------------------------------------------

class TaggedC c a where

Methods

senv :: c a -> IBindEnv

sid :: c a -> Maybe Integer

stag :: c a -> Tag

sinfo :: c a -> a

clhs :: BindEnv -> c a -> [(Symbol, SortedReft)]

crhs :: c a -> Expr

Instances

TaggedC SimpC a

TaggedC SubC a

Accessing Constraints

addIds :: [SubC a] -> [(Integer, SubC a)]

shiftVV :: Reft -> Symbol -> Reft

Qualifiers

data Qualifier

Qualifiers ----------------------------------------------------------------

Constructors

Q

Fields

q_name :: Symbol

Name

q_params :: [(Symbol, Sort)]

Parameters

q_body :: Expr

Predicate

q_pos :: !SourcePos

Source Location

Instances

Eq Qualifier

Data Qualifier

Show Qualifier

Generic Qualifier

Binary Qualifier

NFData Qualifier

PPrint Qualifier

Fixpoint Qualifier

Loc Qualifier

type Rep Qualifier

qualifier :: SEnv Sort -> SourcePos -> SEnv Sort -> Symbol -> Sort -> Expr -> Qualifier

data EQual

Solutions (Instantiated Qualfiers )----------------------------------------

Constructors

EQL

Fields

eqQual :: !Qualifier

eqPred :: !Expr

eqArgs :: ![Expr]

Instances

Eq EQual

Data EQual

Show EQual

Generic EQual

NFData EQual

PPrint EQual

type Rep EQual

eQual :: Qualifier -> [Symbol] -> EQual

Results

type FixSolution = HashMap KVar Expr

Solutions and Results

data Result a

Constructors

Result

Fields

resStatus :: FixResult a

resSolution :: FixSolution

Instances

Show a => Show (Result a)

Generic (Result a)

Monoid (Result a)

NFData a => NFData (Result a)

type Rep (Result a)

Solutions

type Hyp = ListNE Cube

data Cube

Constructors

Cube

Fields

cuBinds :: IBindEnv

cuSubst :: Subst

type QBind = [EQual]

type Cand a = [(Expr, a)]

data Sol a

Constructors

Sol

Fields

sMap :: HashMap KVar a

sHyp :: HashMap KVar Hyp

Instances

Functor Sol

Monoid (Sol a)

PPrint a => PPrint (Sol a)

type Solution = Sol QBind

Types ---------------------------------------------------------------------

solFromList :: [(KVar, a)] -> [(KVar, Hyp)] -> Sol a

Create a Solution ---------------------------------------------------------

solInsert :: KVar -> a -> Sol a -> Sol a

solLookup :: Solution -> KVar -> QBind

Read / Write Solution at KVar ---------------------------------------------

solResult :: Solution -> HashMap KVar Expr

Cut KVars

newtype Kuts

Constraint Cut Sets -------------------------------------------------------

Constructors

KS

Fields

ksVars :: HashSet KVar

Instances

Eq Kuts

Show Kuts

Generic Kuts

Monoid Kuts

Binary Kuts

NFData Kuts

Fixpoint Kuts

type Rep Kuts

ksMember :: KVar -> Kuts -> Bool