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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Solutions

Contents

Description

This module contains the top-level SOLUTION data types, including various indices used for solving.

Synopsis

Solution tables

type Solution = Sol () QBind Source #

The Solution data type --------------------------------------------------

data Sol b a Source #

A Sol contains the various indices needed to compute a solution, in particular, to compute lhsPred for any given constraint.

Instances

Functor (Sol a) Source # 

Methods

fmap :: (a -> b) -> Sol a a -> Sol a b #

(<$) :: a -> Sol a b -> Sol a a #

Monoid (Sol a b) Source # 

Methods

mempty :: Sol a b #

mappend :: Sol a b -> Sol a b -> Sol a b #

mconcat :: [Sol a b] -> Sol a b #

(PPrint a, PPrint b) => PPrint (Sol a b) Source # 

Methods

pprintTidy :: Tidy -> Sol a b -> Doc Source #

pprintPrec :: Int -> Tidy -> Sol a b -> Doc Source #

updateGMap :: Sol b a -> HashMap KVar b -> Sol b a Source #

sScp :: Sol b a -> HashMap KVar IBindEnv Source #

set of allowed binders for kvar

Solution elements

type Hyp = ListNE Cube Source #

A Cube is a single constraint defining a KVar ---------------------------

data Cube Source #

Constructors

Cube 

Fields

Instances

data QBind Source #

Instances

Eq QBind Source # 

Methods

(==) :: QBind -> QBind -> Bool #

(/=) :: QBind -> QBind -> Bool #

Data QBind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QBind -> c QBind #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QBind #

toConstr :: QBind -> Constr #

dataTypeOf :: QBind -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c QBind) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind) #

gmapT :: (forall b. Data b => b -> b) -> QBind -> QBind #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r #

gmapQ :: (forall d. Data d => d -> u) -> QBind -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> QBind -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QBind -> m QBind #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QBind -> m QBind #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QBind -> m QBind #

Show QBind Source # 

Methods

showsPrec :: Int -> QBind -> ShowS #

show :: QBind -> String #

showList :: [QBind] -> ShowS #

Generic QBind Source # 

Associated Types

type Rep QBind :: * -> * #

Methods

from :: QBind -> Rep QBind x #

to :: Rep QBind x -> QBind #

NFData QBind Source # 

Methods

rnf :: QBind -> () #

PPrint QBind Source # 
type Rep QBind Source # 
type Rep QBind = D1 * (MetaData "QBind" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.7.0.7-DC7X7gzBmY2Ic8PTKxWTVg" True) (C1 * (MetaCons "QB" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [EQual])))

data GBind Source #

Instances

Data GBind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GBind -> c GBind #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GBind #

toConstr :: GBind -> Constr #

dataTypeOf :: GBind -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c GBind) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GBind) #

gmapT :: (forall b. Data b => b -> b) -> GBind -> GBind #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r #

gmapQ :: (forall d. Data d => d -> u) -> GBind -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> GBind -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GBind -> m GBind #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GBind -> m GBind #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GBind -> m GBind #

Show GBind Source # 

Methods

showsPrec :: Int -> GBind -> ShowS #

show :: GBind -> String #

showList :: [GBind] -> ShowS #

Generic GBind Source # 

Associated Types

type Rep GBind :: * -> * #

Methods

from :: GBind -> Rep GBind x #

to :: Rep GBind x -> GBind #

NFData GBind Source # 

Methods

rnf :: GBind -> () #

type Rep GBind Source # 
type Rep GBind = D1 * (MetaData "GBind" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.7.0.7-DC7X7gzBmY2Ic8PTKxWTVg" True) (C1 * (MetaCons "GB" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * [[EQual]])))

data EQual Source #

Instantiated Qualifiers ---------------------------------------------------

Constructors

EQL 

Fields

Instances

Eq EQual Source # 

Methods

(==) :: EQual -> EQual -> Bool #

(/=) :: EQual -> EQual -> Bool #

Data EQual Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EQual -> c EQual #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EQual #

toConstr :: EQual -> Constr #

dataTypeOf :: EQual -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c EQual) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EQual) #

gmapT :: (forall b. Data b => b -> b) -> EQual -> EQual #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r #

gmapQ :: (forall d. Data d => d -> u) -> EQual -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> EQual -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EQual -> m EQual #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EQual -> m EQual #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EQual -> m EQual #

Show EQual Source # 

Methods

showsPrec :: Int -> EQual -> ShowS #

show :: EQual -> String #

showList :: [EQual] -> ShowS #

Generic EQual Source # 

Associated Types

type Rep EQual :: * -> * #

Methods

from :: EQual -> Rep EQual x #

to :: Rep EQual x -> EQual #

NFData EQual Source # 

Methods

rnf :: EQual -> () #

PPrint EQual Source # 
type Rep EQual Source # 
type Rep EQual = D1 * (MetaData "EQual" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.7.0.7-DC7X7gzBmY2Ic8PTKxWTVg" False) (C1 * (MetaCons "EQL" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "_eqQual") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Qualifier)) ((:*:) * (S1 * (MetaSel (Just Symbol "eqPred") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Expr)) (S1 * (MetaSel (Just Symbol "_eqArgs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * [Expr])))))

Equal elements

Gradual Solution elements

Solution Candidates (move to SolverMonad?)

type Cand a = [(Expr, a)] Source #

A Cand is an association list indexed by predicates

Constructor

fromList :: SymEnv -> [(KVar, a)] -> [(KVar, b)] -> [(KVar, Hyp)] -> HashMap KVar IBindEnv -> Sol a b Source #

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

Update

update :: Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind) Source #

Update Solution -----------------------------------------------------------

Lookup

lookupQBind :: Sol a QBind -> KVar -> QBind Source #

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

Manipulating QBind

gbFilterM :: Monad m => ([EQual] -> m Bool) -> GBind -> m GBind Source #

Conversion for client

Fast Solver (DEPRECATED as unsound)

data Index Source #

A Index is a suitably indexed version of the cosntraints that lets us 1. CREATE a monolithic "background formula" representing all constraints, 2. ASSERT each lhs via bits for the subc-id and formulas for dependent cut KVars

Constructors

FastIdx 

Fields

data KIndex Source #

A KIndex uniquely identifies each *use* of a KVar in an (LHS) binder

Constructors

KIndex 

Fields

Instances

Eq KIndex Source # 

Methods

(==) :: KIndex -> KIndex -> Bool #

(/=) :: KIndex -> KIndex -> Bool #

Ord KIndex Source # 
Show KIndex Source # 
Generic KIndex Source # 

Associated Types

type Rep KIndex :: * -> * #

Methods

from :: KIndex -> Rep KIndex x #

to :: Rep KIndex x -> KIndex #

Hashable KIndex Source # 

Methods

hashWithSalt :: Int -> KIndex -> Int #

hash :: KIndex -> Int #

PPrint KIndex Source # 
type Rep KIndex Source # 
type Rep KIndex = D1 * (MetaData "KIndex" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.7.0.7-DC7X7gzBmY2Ic8PTKxWTVg" False) (C1 * (MetaCons "KIndex" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "kiBIndex") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * BindId)) ((:*:) * (S1 * (MetaSel (Just Symbol "kiPos") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Int)) (S1 * (MetaSel (Just Symbol "kiKVar") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * KVar)))))

data BindPred Source #

Each Bind corresponds to a conjunction of a bpConc and bpKVars

Constructors

BP 

Fields

data BIndex Source #

A BIndex is created for each LHS Bind or RHS constraint

Constructors

Root 
Bind !BindId 
Cstr !SubcId 

Instances

Eq BIndex Source # 

Methods

(==) :: BIndex -> BIndex -> Bool #

(/=) :: BIndex -> BIndex -> Bool #

Ord BIndex Source # 
Show BIndex Source # 
Generic BIndex Source # 

Associated Types

type Rep BIndex :: * -> * #

Methods

from :: BIndex -> Rep BIndex x #

to :: Rep BIndex x -> BIndex #

Hashable BIndex Source # 

Methods

hashWithSalt :: Int -> BIndex -> Int #

hash :: BIndex -> Int #

PPrint BIndex Source # 
type Rep BIndex Source # 
type Rep BIndex = D1 * (MetaData "BIndex" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.7.0.7-DC7X7gzBmY2Ic8PTKxWTVg" False) ((:+:) * (C1 * (MetaCons "Root" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "Bind" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * BindId))) (C1 * (MetaCons "Cstr" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * SubcId)))))