Language.Fixpoint.Types.Solutions

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

Solution tables

type Solution = Sol () QBind

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

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

data Sol b a

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

Instances

Functor (Sol a)

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)

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)

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)

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)

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: Sol b a -> ()

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

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

type Rep (Sol b a)

Defined in Language.Fixpoint.Types.Solutions

type Rep (Sol b a) = D1 ('MetaData "Sol" "Language.Fixpoint.Types.Solutions" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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

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

sHyp :: Sol b a -> HashMap KVar Hyp

Defining cubes (for non-cut kvar)

sScp :: Sol b a -> HashMap KVar IBindEnv

Set of allowed binders for kvar

type CMap a = HashMap SubcId a

Solution elements

type Hyp = ListNE Cube

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

data Cube

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

Generic Cube

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

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> Cube -> ShowS

show :: Cube -> String

showList :: [Cube] -> ShowS

NFData Cube

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: Cube -> ()

PPrint Cube

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> Cube -> Doc

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

type Rep Cube

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

Instances

Data QBind

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

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

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> QBind -> ShowS

show :: QBind -> String

showList :: [QBind] -> ShowS

NFData QBind

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: QBind -> ()

Eq QBind

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

PPrint QBind

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> QBind -> Doc

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

type Rep QBind

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

Instances

Data GBind

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

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

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> GBind -> ShowS

show :: GBind -> String

showList :: [GBind] -> ShowS

NFData GBind

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: GBind -> ()

type Rep GBind

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

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

Constructors

EQL

Fields

• eqQual :: !Qualifier
• eqPred :: !Expr
• _eqArgs :: ![Expr]

Instances

Data EQual

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

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

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> EQual -> ShowS

show :: EQual -> String

showList :: [EQual] -> ShowS

NFData EQual

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: EQual -> ()

Eq EQual

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

PPrint EQual

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> EQual -> Doc

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

Loc EQual

Defined in Language.Fixpoint.Types.Solutions

Methods

srcSpan :: EQual -> SrcSpan

type Rep EQual

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

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

Generic EbindSol

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

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> EbindSol -> ShowS

show :: EbindSol -> String

showList :: [EbindSol] -> ShowS

NFData EbindSol

Defined in Language.Fixpoint.Types.Solutions

Methods

rnf :: EbindSol -> ()

PPrint EbindSol

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> EbindSol -> Doc

pprintPrec :: Int -> Tidy -> EbindSol -> Doc

type Rep EbindSol

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

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

trueEqual :: EQual

Gradual Solution elements

qbToGb :: QBind -> GBind

gbToQbs :: GBind -> [QBind]

gbEquals :: GBind -> [[EQual]]

equalsGb :: [[EQual]] -> GBind

emptyGMap :: GSolution -> GSolution

qbExprs :: QBind -> [Expr]

Solution Candidates (move to SolverMonad?)

type Cand a = [(Expr, a)]

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

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

Update

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

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

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

Lookup

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

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

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

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

Manipulating QBind

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

Conversion for client

result :: Sol a QBind -> HashMap KVar Expr

resultGradual :: GSolution -> HashMap KVar (Expr, [Expr])

Fast Solver (DEPRECATED as unsound)

data Index

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

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

Constructors

KIndex

Fields

• kiBIndex :: !BindId
• kiPos :: !Int
• kiKVar :: !KVar

Instances

Generic KIndex

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

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> KIndex -> ShowS

show :: KIndex -> String

showList :: [KIndex] -> ShowS

Eq KIndex

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

Ord KIndex

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

Defined in Language.Fixpoint.Types.Solutions

Methods

hashWithSalt :: Int -> KIndex -> Int

hash :: KIndex -> Int

PPrint KIndex

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> KIndex -> Doc

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

type Rep KIndex

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

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

Show BindPred

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> BindPred -> ShowS

show :: BindPred -> String

showList :: [BindPred] -> ShowS

PPrint BindPred

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> BindPred -> Doc

pprintPrec :: Int -> Tidy -> BindPred -> Doc

data BIndex

A BIndex is created for each LHS Bind or RHS constraint

Constructors

Root

Bind !BindId

Cstr !SubcId

Instances

Generic BIndex

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

Defined in Language.Fixpoint.Types.Solutions

Methods

showsPrec :: Int -> BIndex -> ShowS

show :: BIndex -> String

showList :: [BIndex] -> ShowS

Eq BIndex

Defined in Language.Fixpoint.Types.Solutions

Methods

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

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

Ord BIndex

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

Hashable BIndex

Defined in Language.Fixpoint.Types.Solutions

Methods

hashWithSalt :: Int -> BIndex -> Int

hash :: BIndex -> Int

PPrint BIndex

Defined in Language.Fixpoint.Types.Solutions

Methods

pprintTidy :: Tidy -> BIndex -> Doc

pprintPrec :: Int -> Tidy -> BIndex -> Doc

type Rep BIndex

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