Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Solutions

Contents

Solution tables
Solution elements
Equal elements
Solution Candidates (move to SolverMonad?)
Update
Lookup
Manipulating QBind
Conversion for client
Fast Solver (DEPRECATED as unsound)

Description

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

Synopsis

type Solution = Sol QBind
data Sol a = Sol {
- sMap :: !(HashMap KVar a)
- sHyp :: !(HashMap KVar Hyp)
- sScp :: !(HashMap KVar IBindEnv)
}
type CMap a = HashMap SubcId a
type Hyp = ListNE Cube
data Cube = Cube {
- cuBinds :: IBindEnv
- cuSubst :: Subst
- cuId :: SubcId
- cuTag :: Tag
}
newtype QBind = QB [EQual]
data EQual = EQL {
- eqQual :: !Qualifier
- eqPred :: !Expr
- _eqArgs :: ![Expr]
}
eQual :: Qualifier -> [Symbol] -> EQual
trueEqual :: EQual
qbExprs :: QBind -> [Expr]
type Cand a = [(Expr, a)]
update :: Sol QBind -> [(KVar, QBind)] -> (Bool, Sol QBind)
lookupQBind :: Sol QBind -> KVar -> QBind
lookup :: Sol QBind -> KVar -> Either Hyp QBind
qb :: [EQual] -> QBind
qbPreds :: Subst -> QBind -> [(Pred, EQual)]
qbFilter :: (EQual -> Bool) -> QBind -> QBind
qbFilterM :: Monad m => (EQual -> m Bool) -> QBind -> m QBind
result :: Sol QBind -> HashMap KVar Expr
data Index = FastIdx {
- bindExpr :: !(BindId |-> BindPred)
- kvUse :: !(KIndex |-> KVSub)
- kvDef :: !(KVar |-> Hyp)
- envBinds :: !(CMap IBindEnv)
- envTx :: !(CMap [SubcId])
- envSorts :: !(SEnv Sort)
}
data KIndex = KIndex {
- kiBIndex :: !BindId
- kiPos :: !Int
- kiKVar :: !KVar
}
data BindPred = BP {
- bpConc :: !Pred
- bpKVar :: ![KIndex]
}
data BIndex
- = Root
- | Bind !BindId
- | Cstr !SubcId

Solution tables

type Solution = Sol QBind Source #

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

data Sol a Source #

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

Constructors

Sol
Fields sMap :: !(HashMap KVar a) Actual solution (for cut kvar) sHyp :: !(HashMap KVar Hyp) Defining cubes (for non-cut kvar) sScp :: !(HashMap KVar IBindEnv) Set of binders which are in scope for every occurrence of the kvar

Instances

Instances details

Functor Sol Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

Monoid (Sol a) Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

mempty :: Sol a #

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

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

Semigroup (Sol a) Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

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

Generic (Sol a) Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep (Sol a)

Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep (Sol a) = D1 ('MetaData "Sol" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "Sol" 'PrefixI 'True) (S1 ('MetaSel ('Just "sMap") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar a)) :*: (S1 ('MetaSel ('Just "sHyp") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar Hyp)) :*: S1 ('MetaSel ('Just "sScp") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar IBindEnv)))))

Methods

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

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

NFData a => NFData (Sol a) Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: Sol a -> () #

PPrint a => PPrint (Sol a) Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

type Rep (Sol a) Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep (Sol a) = D1 ('MetaData "Sol" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "Sol" 'PrefixI 'True) (S1 ('MetaSel ('Just "sMap") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar a)) :*: (S1 ('MetaSel ('Just "sHyp") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar Hyp)) :*: S1 ('MetaSel ('Just "sScp") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar IBindEnv)))))

type CMap a = HashMap SubcId a Source #

Solution elements

type Hyp = ListNE Cube Source #

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

data Cube Source #

Constructors

Cube
Fields cuBinds :: IBindEnv Binders from defining Env cuSubst :: Subst Substitutions from cstrs Rhs cuId :: SubcId Id of defining Cstr cuTag :: Tag Tag of defining Cstr (DEBUG)

Instances

Instances details

Generic Cube Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep Cube

Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep Cube = D1 ('MetaData "Cube" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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))))

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

Methods

pprintTidy :: Tidy -> Cube -> Doc Source #

pprintPrec :: Int -> Tidy -> Cube -> Doc Source #

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.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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))))

newtype QBind Source #

Constructors

QB [EQual]

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
Instance details Defined in Language.Fixpoint.Types.Solutions type Rep QBind = D1 ('MetaData "QBind" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "QB" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [EQual])))

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

Methods

pprintTidy :: Tidy -> QBind -> Doc Source #

pprintPrec :: Int -> Tidy -> QBind -> Doc Source #

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

data EQual Source #

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

Constructors

EQL
Fields eqQual :: !Qualifier eqPred :: !Expr predicate obtained by instantiating the qualifier _eqArgs :: ![Expr] actual arguments used to instantiate the qualifier

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

Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep EQual = D1 ('MetaData "EQual" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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]))))

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

Methods

pprintTidy :: Tidy -> EQual -> Doc Source #

pprintPrec :: Int -> Tidy -> EQual -> Doc Source #

Loc EQual Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

srcSpan :: EQual -> SrcSpan Source #

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.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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]))))

Equal elements

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

eQual q xs instantiates q with the arguments in xs

trueEqual :: EQual Source #

qbExprs :: QBind -> [Expr] Source #

Solution Candidates (move to SolverMonad?)

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

A Cand is an association list indexed by predicates

Update

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

Update Solution

update s kqs sets in s each KVar in kqs to the corresponding QBind.

Yields a pair (b, s') where b is true if the mapping of any KVar was changed.

Precondition: kqs contains no duplicate KVars.

Lookup

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

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

lookup :: Sol QBind -> KVar -> Either Hyp QBind Source #

Manipulating QBind

qb :: [EQual] -> QBind Source #

qbPreds :: Subst -> QBind -> [(Pred, EQual)] Source #

qbFilter :: (EQual -> Bool) -> QBind -> QBind Source #

qbFilterM :: Monad m => (EQual -> m Bool) -> QBind -> m QBind Source #

Conversion for client

result :: Sol QBind -> HashMap KVar Expr Source #

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

bindExpr :: !(BindId |-> BindPred)
BindPred for each BindId
kvUse :: !(KIndex |-> KVSub)
Definition of each KIndex
kvDef :: !(KVar |-> Hyp)
Constraints defining each KVar
envBinds :: !(CMap IBindEnv)
Binders of each Subc
envTx :: !(CMap [SubcId])
Transitive closure oof all dependent binders
envSorts :: !(SEnv Sort)
Sorts for all symbols , bindPrev :: !(BIndex |-> BIndex) -- ^ "parent" (immediately dominating) binder , kvDeps :: !(CMap [KIndex]) -- ^ List of (Cut) KVars on which a SubC depends

data KIndex Source #

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

Constructors

KIndex
Fields kiBIndex :: !BindId kiPos :: !Int kiKVar :: !KVar

Instances

Instances details

Generic KIndex Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

Associated Types

type Rep KIndex

Instance details

Defined in Language.Fixpoint.Types.Solutions

type Rep KIndex = D1 ('MetaData "KIndex" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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))))

Methods

from :: KIndex -> Rep KIndex x #

to :: Rep KIndex x -> KIndex #

Show KIndex Source #

Instance details

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> KIndex -> ShowS #

show :: KIndex -> String #

showList :: [KIndex] -> ShowS #

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

Methods

compare :: KIndex -> KIndex -> Ordering #

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

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

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

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

max :: KIndex -> KIndex -> KIndex #

min :: KIndex -> KIndex -> 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

Methods

pprintTidy :: Tidy -> KIndex -> Doc Source #

pprintPrec :: Int -> Tidy -> KIndex -> Doc Source #

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.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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 bpConc :: !Pred Concrete predicate (PTrue o) bpKVar :: ![KIndex] KVar-Subst pairs

Instances

Instances details

Show BindPred Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods showsPrec :: Int -> BindPred -> ShowS # show :: BindPred -> String # showList :: [BindPred] -> ShowS #
PPrint BindPred Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> BindPred -> Doc Source # pprintPrec :: Int -> Tidy -> BindPred -> Doc Source #