liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Types.Solutions

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

Instances details
Functor (Sol a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

Monoid (Sol a b) Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

mempty :: Sol a b #

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

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

Semigroup (Sol a b) Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

sconcat :: NonEmpty (Sol a b) -> Sol a b #

stimes :: Integral b0 => b0 -> Sol a b -> Sol a b #

Generic (Sol b a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep (Sol b a) :: Type -> Type #

Methods

from :: Sol b a -> Rep (Sol b a) x #

to :: Rep (Sol b a) x -> Sol b a #

(NFData b, NFData a) => NFData (Sol b a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: Sol b a -> () #

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

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

type Rep (Sol b a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

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

sHyp :: Sol b a -> HashMap KVar Hyp Source #

Defining cubes (for non-cut kvar)

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

Instances details
Generic Cube Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep Cube :: Type -> Type #

Methods

from :: Cube -> Rep Cube x #

to :: Rep Cube x -> Cube #

Show Cube Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> Cube -> ShowS #

show :: Cube -> String #

showList :: [Cube] -> ShowS #

NFData Cube Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: Cube -> () #

PPrint Cube Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep Cube Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep Cube = D1 ('MetaData "Cube" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "Cube" 'PrefixI 'True) ((S1 ('MetaSel ('Just "cuBinds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IBindEnv) :*: S1 ('MetaSel ('Just "cuSubst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Subst)) :*: (S1 ('MetaSel ('Just "cuId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SubcId) :*: S1 ('MetaSel ('Just "cuTag") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Tag))))

data QBind Source #

Instances

Instances details
Data QBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

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 :: forall r r'. (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 #

Generic QBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep QBind :: Type -> Type #

Methods

from :: QBind -> Rep QBind x #

to :: Rep QBind x -> QBind #

Show QBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> QBind -> ShowS #

show :: QBind -> String #

showList :: [QBind] -> ShowS #

NFData QBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: QBind -> () #

Eq QBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

PPrint QBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep QBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep QBind = D1 ('MetaData "QBind" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "QB" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [EQual])))

data GBind Source #

Instances

Instances details
Data GBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

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 :: forall r r'. (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 #

Generic GBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep GBind :: Type -> Type #

Methods

from :: GBind -> Rep GBind x #

to :: Rep GBind x -> GBind #

Show GBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> GBind -> ShowS #

show :: GBind -> String #

showList :: [GBind] -> ShowS #

NFData GBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: GBind -> () #

type Rep GBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep GBind = D1 ('MetaData "GBind" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "GB" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[EQual]])))

data EQual Source #

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

Constructors

EQL 

Fields

Instances

Instances details
Data EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

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 :: forall r r'. (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 #

Generic EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep EQual :: Type -> Type #

Methods

from :: EQual -> Rep EQual x #

to :: Rep EQual x -> EQual #

Show EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> EQual -> ShowS #

show :: EQual -> String #

showList :: [EQual] -> ShowS #

NFData EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: EQual -> () #

Eq EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

PPrint EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Loc EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep EQual = D1 ('MetaData "EQual" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "EQL" 'PrefixI 'True) (S1 ('MetaSel ('Just "eqQual") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Qualifier) :*: (S1 ('MetaSel ('Just "eqPred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Just "_eqArgs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Expr]))))

data EbindSol Source #

An EbindSol contains the relevant information for an existential-binder; (See testsposebind-*.fq for examples.) This is either 1. the constraint whose HEAD is a singleton that defines the binder, OR 2. the solved out TERM that we should use in place of the ebind at USES.

Constructors

EbDef [SimpC ()] Symbol

The constraint whose HEAD "defines" the Ebind and the Symbol for that EBind

EbSol Expr

The solved out term that should be used at USES.

EbIncr

EBinds not to be solved for (because they're currently being solved for)

Instances

Instances details
Generic EbindSol Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep EbindSol :: Type -> Type #

Methods

from :: EbindSol -> Rep EbindSol x #

to :: Rep EbindSol x -> EbindSol #

Show EbindSol Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

NFData EbindSol Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: EbindSol -> () #

PPrint EbindSol Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep EbindSol Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep EbindSol = D1 ('MetaData "EbindSol" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "EbDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SimpC ()]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)) :+: (C1 ('MetaCons "EbSol" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "EbIncr" 'PrefixI 'False) (U1 :: Type -> Type)))

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 -> [(BindId, EbindSol)] -> SEnv (BindId, Sort) -> Sol a b Source #

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

Update

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

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

updateEbind :: Sol a b -> BindId -> Pred -> Sol a b Source #

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

Instances details
Generic KIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep KIndex :: Type -> Type #

Methods

from :: KIndex -> Rep KIndex x #

to :: Rep KIndex x -> KIndex #

Show KIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Eq KIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

Ord KIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Hashable KIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

hashWithSalt :: Int -> KIndex -> Int #

hash :: KIndex -> Int #

PPrint KIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep KIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep KIndex = D1 ('MetaData "KIndex" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "KIndex" 'PrefixI 'True) (S1 ('MetaSel ('Just "kiBIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BindId) :*: (S1 ('MetaSel ('Just "kiPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "kiKVar") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KVar))))

data BindPred Source #

Each Bind corresponds to a conjunction of a bpConc and bpKVars

Constructors

BP 

Fields

Instances

Instances details
Show BindPred Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

PPrint BindPred Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

data BIndex Source #

A BIndex is created for each LHS Bind or RHS constraint

Constructors

Root 
Bind !BindId 
Cstr !SubcId 

Instances

Instances details
Generic BIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep BIndex :: Type -> Type #

Methods

from :: BIndex -> Rep BIndex x #

to :: Rep BIndex x -> BIndex #

Show BIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Eq BIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

Ord BIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Hashable BIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

hashWithSalt :: Int -> BIndex -> Int #

hash :: BIndex -> Int #

PPrint BIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep BIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep BIndex = D1 ('MetaData "BIndex" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "Root" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Bind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BindId)) :+: C1 ('MetaCons "Cstr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SubcId))))