liquid-fixpoint-0.8.10.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellNone
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 #

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 #

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

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

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

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

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

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

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

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

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

result :: Sol a 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

data KIndex Source #

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

Constructors

KIndex 

Fields

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

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

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