Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Solutions

Contents

Solution tables
Solution elements
Equal elements
Gradual Solution elements
Solution Candidates (move to SolverMonad?)
Constructor
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
type GSolution = Sol (((Symbol, Sort), Expr), GBind) QBind
data Sol b a
updateGMap :: Sol b a -> HashMap KVar b -> Sol b a
updateGMapWithKey :: [(KVar, QBind)] -> GSolution -> GSolution
sScp :: Sol b a -> HashMap KVar IBindEnv
type CMap a = HashMap SubcId a
type Hyp = ListNE Cube
data Cube = Cube {
- cuBinds :: IBindEnv
- cuSubst :: Subst
- cuId :: SubcId
- cuTag :: Tag
}
data QBind
data GBind
data EQual = EQL {
- eqQual :: !Qualifier
- eqPred :: !Expr
- _eqArgs :: ![Expr]
}
data EbindSol
- = EbDef [SimpC ()] Symbol
- | EbSol Expr
- | EbIncr
eQual :: Qualifier -> [Symbol] -> EQual
trueEqual :: EQual
qbToGb :: QBind -> GBind
gbToQbs :: GBind -> [QBind]
gbEquals :: GBind -> [[EQual]]
equalsGb :: [[EQual]] -> GBind
emptyGMap :: GSolution -> GSolution
qbExprs :: QBind -> [Expr]
type Cand a = [(Expr, a)]
fromList :: SymEnv -> [(KVar, a)] -> [(KVar, b)] -> [(KVar, Hyp)] -> HashMap KVar IBindEnv -> [(BindId, EbindSol)] -> SEnv (BindId, Sort) -> Sol a b
update :: Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind)
updateEbind :: Sol a b -> BindId -> Pred -> Sol a b
lookupQBind :: Sol a QBind -> KVar -> QBind
lookup :: Sol a QBind -> KVar -> Either Hyp QBind
glookup :: GSolution -> KVar -> Either Hyp (Either QBind (((Symbol, Sort), Expr), GBind))
qb :: [EQual] -> QBind
qbPreds :: String -> Sol a QBind -> Subst -> QBind -> [(Pred, EQual)]
qbFilter :: (EQual -> Bool) -> QBind -> QBind
gbFilterM :: Monad m => ([EQual] -> m Bool) -> GBind -> m GBind
result :: Sol a QBind -> HashMap KVar Expr
resultGradual :: GSolution -> HashMap KVar (Expr, [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 --------------------------------------------------

type GSolution = Sol (((Symbol, Sort), Expr), GBind) QBind Source #

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 #
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 type Rep (Sol b a) = D1 ('MetaData "Sol" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "Sol" 'PrefixI 'True) ((S1 ('MetaSel ('Just "sEnv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SymEnv) :: (S1 ('MetaSel ('Just "sMap") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar a)) :: S1 ('MetaSel ('Just "gMap") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar b)))) :: ((S1 ('MetaSel ('Just "sHyp") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar Hyp)) :: S1 ('MetaSel ('Just "sScp") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar IBindEnv))) :: (S1 ('MetaSel ('Just "sEbd") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap BindId EbindSol)) :: S1 ('MetaSel ('Just "sxEnv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SEnv (BindId, Sort)))))))

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

updateGMapWithKey :: [(KVar, QBind)] -> GSolution -> GSolution Source #

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

Set of allowed binders for kvar

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

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 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.8.10.2-inplace" '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

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

data EQual Source #

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

Constructors

EQL
Fields eqQual :: !Qualifier eqPred :: !Expr _eqArgs :: ![Expr]

Instances

Instances details

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 :: 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 #
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 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.8.10.2-inplace" '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

Show EbindSol Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods showsPrec :: Int -> EbindSol -> ShowS # show :: EbindSol -> String # showList :: [EbindSol] -> ShowS #
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 Methods pprintTidy :: Tidy -> EbindSol -> Doc Source # pprintPrec :: Int -> Tidy -> EbindSol -> Doc Source #
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.8.10.2-inplace" '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

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

trueEqual :: EQual Source #

Gradual Solution elements

qbToGb :: QBind -> GBind Source #

gbToQbs :: GBind -> [QBind] Source #

gbEquals :: GBind -> [[EQual]] Source #

equalsGb :: [[EQual]] -> GBind Source #

emptyGMap :: GSolution -> GSolution 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

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

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

glookup :: GSolution -> KVar -> Either Hyp (Either QBind (((Symbol, Sort), Expr), GBind)) Source #

Manipulating QBind

qb :: [EQual] -> QBind Source #

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

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

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

Conversion for client

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

resultGradual :: GSolution -> HashMap KVar (Expr, [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

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 #
Show KIndex Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods showsPrec :: Int -> KIndex -> ShowS # show :: KIndex -> String # showList :: [KIndex] -> ShowS #
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 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.8.10.2-inplace" '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 #

data BIndex Source #

A BIndex is created for each LHS Bind or RHS constraint

Constructors

Root
Bind !BindId
Cstr !SubcId

Instances

Instances details

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 Methods compare :: BIndex -> BIndex -> Ordering # (<) :: BIndex -> BIndex -> Bool # (<=) :: BIndex -> BIndex -> Bool # (>) :: BIndex -> BIndex -> Bool # (>=) :: BIndex -> BIndex -> Bool # max :: BIndex -> BIndex -> BIndex # min :: BIndex -> BIndex -> BIndex #
Show BIndex Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods showsPrec :: Int -> BIndex -> ShowS # show :: BIndex -> String # showList :: [BIndex] -> ShowS #
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 Methods pprintTidy :: Tidy -> BIndex -> Doc Source # pprintPrec :: Int -> Tidy -> BIndex -> Doc Source #
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-inplace" '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))))