liquid-fixpoint-0.8.10.2: 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 # 
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 #

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 #

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 #

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 #

(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 #

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
Show Cube Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> Cube -> ShowS #

show :: Cube -> String #

showList :: [Cube] -> ShowS #

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 #

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

data QBind Source #

Instances
Eq QBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

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 :: (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 # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> QBind -> ShowS #

show :: QBind -> String #

showList :: [QBind] -> ShowS #

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 #

NFData QBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: QBind -> () #

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.8.10.2-Ld6PWXA9XrKe3HZnOCc57" True) (C1 (MetaCons "QB" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [EQual])))

data GBind Source #

Instances
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 :: (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 # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> GBind -> ShowS #

show :: GBind -> String #

showList :: [GBind] -> ShowS #

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 #

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.8.10.2-Ld6PWXA9XrKe3HZnOCc57" 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
Eq EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

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 :: (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 # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> EQual -> ShowS #

show :: EQual -> String #

showList :: [EQual] -> ShowS #

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 #

NFData EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: EQual -> () #

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.8.10.2-Ld6PWXA9XrKe3HZnOCc57" 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
Show EbindSol Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

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 #

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

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
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

Show KIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

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 #

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.8.10.2-Ld6PWXA9XrKe3HZnOCc57" 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

data BIndex Source #

A BIndex is created for each LHS Bind or RHS constraint

Constructors

Root 
Bind !BindId 
Cstr !SubcId 
Instances
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

Show BIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

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 #

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.8.10.2-Ld6PWXA9XrKe3HZnOCc57" 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))))