liquid-fixpoint-0.8.10.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Constraints

Description

This module contains the top-level QUERY data types and elements, including (Horn) implication & well-formedness constraints and sets.

Synopsis

Top-level Queries

type FInfo a = GInfo SubC a Source #

type SInfo a = GInfo SimpC a Source #

data GInfo c a Source #

Constructors

FI 

Fields

Instances

Instances details
Functor c => Functor (GInfo c) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

fmap :: (a -> b) -> GInfo c a -> GInfo c b #

(<$) :: a -> GInfo c b -> GInfo c a #

PTable (SInfo a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

ptable :: SInfo a -> DocTable Source #

Loc a => Elaborate (SInfo a) Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> SInfo a -> SInfo a Source #

Inputable (FInfo ()) Source # 
Instance details

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> FInfo () Source #

rr' :: String -> String -> FInfo () Source #

Gradual (SInfo a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> SInfo a -> SInfo a Source #

(Eq a, Eq (c a)) => Eq (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

(==) :: GInfo c a -> GInfo c a -> Bool #

(/=) :: GInfo c a -> GInfo c a -> Bool #

(Fixpoint a, Show a, Show (c a)) => Show (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

showsPrec :: Int -> GInfo c a -> ShowS #

show :: GInfo c a -> String #

showList :: [GInfo c a] -> ShowS #

Generic (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep (GInfo c a) :: Type -> Type #

Methods

from :: GInfo c a -> Rep (GInfo c a) x #

to :: Rep (GInfo c a) x -> GInfo c a #

Semigroup (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

(<>) :: GInfo c a -> GInfo c a -> GInfo c a #

sconcat :: NonEmpty (GInfo c a) -> GInfo c a #

stimes :: Integral b => b -> GInfo c a -> GInfo c a #

Monoid (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

mempty :: GInfo c a #

mappend :: GInfo c a -> GInfo c a -> GInfo c a #

mconcat :: [GInfo c a] -> GInfo c a #

(Binary (c a), Binary a) => Binary (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: GInfo c a -> Put #

get :: Get (GInfo c a) #

putList :: [GInfo c a] -> Put #

(NFData (c a), NFData a) => NFData (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: GInfo c a -> () #

HasGradual (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

isGradual :: GInfo c a -> Bool Source #

gVars :: GInfo c a -> [KVar] Source #

ungrad :: GInfo c a -> GInfo c a Source #

SymConsts (c a) => SymConsts (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: GInfo c a -> [SymConst] Source #

Visitable (c a) => Visitable (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a0 => Visitor a0 c0 -> c0 -> GInfo c a -> VisitM a0 (GInfo c a) Source #

(Defunc (c a), TaggedC c a) => Defunc (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: GInfo c a -> DF (GInfo c a) Source #

type Rep (GInfo c a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep (GInfo c a) = D1 ('MetaData "GInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "FI" 'PrefixI 'True) (((S1 ('MetaSel ('Just "cm") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap SubcId (c a))) :*: (S1 ('MetaSel ('Just "ws") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap KVar (WfC a))) :*: S1 ('MetaSel ('Just "bs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BindEnv))) :*: (S1 ('MetaSel ('Just "ebinds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [BindId]) :*: (S1 ('MetaSel ('Just "gLits") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SEnv Sort)) :*: S1 ('MetaSel ('Just "dLits") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SEnv Sort))))) :*: ((S1 ('MetaSel ('Just "kuts") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Kuts) :*: (S1 ('MetaSel ('Just "quals") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Qualifier]) :*: S1 ('MetaSel ('Just "bindInfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap BindId a)))) :*: ((S1 ('MetaSel ('Just "ddecls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl]) :*: S1 ('MetaSel ('Just "hoInfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 HOInfo)) :*: (S1 ('MetaSel ('Just "asserts") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Triggered Expr]) :*: S1 ('MetaSel ('Just "ae") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AxiomEnv))))))

data FInfoWithOpts a Source #

Top-level Queries

Constructors

FIO 

Fields

Instances

Instances details
Inputable (FInfoWithOpts ()) Source # 
Instance details

Defined in Language.Fixpoint.Parse

convertFormat :: Fixpoint a => FInfo a -> SInfo a Source #

Query Conversions: FInfo to SInfo

type Solver a = Config -> FInfo a -> IO (Result (Integer, a)) Source #

Top level Solvers ----------------------------------------------------

Serializing

toFixpoint :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> Doc Source #

Rendering Queries

writeFInfo :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> FilePath -> IO () Source #

Constructing Queries

fi :: [SubC a] -> [WfC a] -> BindEnv -> SEnv Sort -> SEnv Sort -> Kuts -> [Qualifier] -> HashMap BindId a -> Bool -> Bool -> [Triggered Expr] -> AxiomEnv -> [DataDecl] -> [BindId] -> GInfo SubC a Source #

Constructing Queries

Constraints

data WfC a Source #

Constructors

WfC 

Fields

GWfC 

Fields

Instances

Instances details
Functor WfC Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

Eq a => Eq (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

(==) :: WfC a -> WfC a -> Bool #

(/=) :: WfC a -> WfC a -> Bool #

Fixpoint a => Show (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

showsPrec :: Int -> WfC a -> ShowS #

show :: WfC a -> String #

showList :: [WfC a] -> ShowS #

Generic (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep (WfC a) :: Type -> Type #

Methods

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

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

Binary a => Binary (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: WfC a -> Put #

get :: Get (WfC a) #

putList :: [WfC a] -> Put #

NFData a => NFData (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: WfC a -> () #

Fixpoint a => PPrint (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

Fixpoint a => Fixpoint (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

toFix :: WfC a -> Doc Source #

simplify :: WfC a -> WfC a Source #

HasGradual (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

isGradual :: WfC a -> Bool Source #

gVars :: WfC a -> [KVar] Source #

ungrad :: WfC a -> WfC a Source #

Defunc (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: WfC a -> DF (WfC a) Source #

type Rep (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

updateWfCExpr :: (Expr -> Expr) -> WfC a -> WfC a Source #

data SubC a Source #

Instances

Instances details
Functor SubC Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

TaggedC SubC a Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Eq a => Eq (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

(==) :: SubC a -> SubC a -> Bool #

(/=) :: SubC a -> SubC a -> Bool #

Fixpoint a => Show (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

showsPrec :: Int -> SubC a -> ShowS #

show :: SubC a -> String #

showList :: [SubC a] -> ShowS #

Generic (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep (SubC a) :: Type -> Type #

Methods

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

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

Binary a => Binary (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: SubC a -> Put #

get :: Get (SubC a) #

putList :: [SubC a] -> Put #

NFData a => NFData (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: SubC a -> () #

Fixpoint a => PPrint (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint a => Fixpoint (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

toFix :: SubC a -> Doc Source #

simplify :: SubC a -> SubC a Source #

SymConsts (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: SubC a -> [SymConst] Source #

Visitable (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a0 => Visitor a0 c -> c -> SubC a -> VisitM a0 (SubC a) Source #

Inputable (FInfo ()) Source # 
Instance details

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> FInfo () Source #

rr' :: String -> String -> FInfo () Source #

type Rep (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

subcId :: TaggedC c a => c a -> SubcId Source #

sid :: TaggedC c a => c a -> Maybe Integer Source #

senv :: TaggedC c a => c a -> IBindEnv Source #

stag :: TaggedC c a => c a -> Tag Source #

wfC :: Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a] Source #

"Smart Constructors" for Constraints ---------------------------------

data SimpC a Source #

Constructors

SimpC 

Fields

Instances

Instances details
Functor SimpC Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

TaggedC SimpC a Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint a => Show (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

showsPrec :: Int -> SimpC a -> ShowS #

show :: SimpC a -> String #

showList :: [SimpC a] -> ShowS #

Generic (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep (SimpC a) :: Type -> Type #

Methods

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

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

Binary a => Binary (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: SimpC a -> Put #

get :: Get (SimpC a) #

putList :: [SimpC a] -> Put #

NFData a => NFData (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: SimpC a -> () #

PTable (SInfo a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

ptable :: SInfo a -> DocTable Source #

Fixpoint a => PPrint (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

Fixpoint a => Fixpoint (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

toFix :: SimpC a -> Doc Source #

simplify :: SimpC a -> SimpC a Source #

Loc a => Loc (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

srcSpan :: SimpC a -> SrcSpan Source #

SymConsts (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

symConsts :: SimpC a -> [SymConst] Source #

Visitable (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a0 => Visitor a0 c -> c -> SimpC a -> VisitM a0 (SimpC a) Source #

Loc a => Elaborate (SInfo a) Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> SInfo a -> SInfo a Source #

Loc a => Elaborate (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> SimpC a -> SimpC a Source #

Gradual (SInfo a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> SInfo a -> SInfo a Source #

Gradual (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Graduals

Methods

gsubst :: GSol -> SimpC a -> SimpC a Source #

Defunc (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: SimpC a -> DF (SimpC a) Source #

type Rep (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Tag = [Int] Source #

Constraints ---------------------------------------------------------------

class TaggedC c a Source #

Minimal complete definition

senv, sid, stag, sinfo, clhs, crhs

Instances

Instances details
TaggedC SimpC a Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

TaggedC SubC a Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

clhs :: TaggedC c a => BindEnv -> c a -> [(Symbol, SortedReft)] Source #

crhs :: TaggedC c a => c a -> Expr Source #

Accessing Constraints

addIds :: [SubC a] -> [(Integer, SubC a)] Source #

sinfo :: TaggedC c a => c a -> a Source #

data GWInfo Source #

Constructors

GWInfo 

Fields

Instances

Instances details
Eq GWInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

Generic GWInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep GWInfo :: Type -> Type #

Methods

from :: GWInfo -> Rep GWInfo x #

to :: Rep GWInfo x -> GWInfo #

Binary GWInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: GWInfo -> Put #

get :: Get GWInfo #

putList :: [GWInfo] -> Put #

NFData GWInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: GWInfo -> () #

type Rep GWInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep GWInfo = D1 ('MetaData "GWInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "GWInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "gsym") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "gsort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :*: (S1 ('MetaSel ('Just "gexpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Just "ginfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GradInfo))))

Qualifiers

data Qualifier Source #

Qualifiers ----------------------------------------------------------------

Constructors

Q 

Fields

Instances

Instances details
Eq Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Data Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Qualifier -> c Qualifier #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Qualifier #

toConstr :: Qualifier -> Constr #

dataTypeOf :: Qualifier -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Qualifier) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Qualifier) #

gmapT :: (forall b. Data b => b -> b) -> Qualifier -> Qualifier #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Qualifier -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Qualifier -> r #

gmapQ :: (forall d. Data d => d -> u) -> Qualifier -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Qualifier -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Qualifier -> m Qualifier #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Qualifier -> m Qualifier #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Qualifier -> m Qualifier #

Show Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Generic Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep Qualifier :: Type -> Type #

Binary Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

NFData Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: Qualifier -> () #

Hashable Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Loc Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Subable Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep Qualifier = D1 ('MetaData "Qualifier" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "Q" 'PrefixI 'True) ((S1 ('MetaSel ('Just "qName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "qParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QualParam])) :*: (S1 ('MetaSel ('Just "qBody") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Just "qPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos))))

data QualParam Source #

Constructors

QP 

Fields

Instances

Instances details
Eq QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Data QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QualParam -> c QualParam #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QualParam #

toConstr :: QualParam -> Constr #

dataTypeOf :: QualParam -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QualParam) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualParam) #

gmapT :: (forall b. Data b => b -> b) -> QualParam -> QualParam #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QualParam -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QualParam -> r #

gmapQ :: (forall d. Data d => d -> u) -> QualParam -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> QualParam -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QualParam -> m QualParam #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QualParam -> m QualParam #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QualParam -> m QualParam #

Show QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Generic QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep QualParam :: Type -> Type #

Binary QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

NFData QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: QualParam -> () #

Hashable QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep QualParam = D1 ('MetaData "QualParam" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "QP" 'PrefixI 'True) (S1 ('MetaSel ('Just "qpSym") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: (S1 ('MetaSel ('Just "qpPat") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QualPattern) :*: S1 ('MetaSel ('Just "qpSort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort))))

data QualPattern Source #

Constructors

PatNone

match everything

PatPrefix !Symbol !Int

str . $i i.e. match prefix str with suffix bound to $i

PatSuffix !Int !Symbol

$i . str i.e. match suffix str with prefix bound to $i

PatExact !Symbol

str i.e. exactly match str

Instances

Instances details
Eq QualPattern Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Data QualPattern Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QualPattern -> c QualPattern #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QualPattern #

toConstr :: QualPattern -> Constr #

dataTypeOf :: QualPattern -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QualPattern) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualPattern) #

gmapT :: (forall b. Data b => b -> b) -> QualPattern -> QualPattern #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QualPattern -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QualPattern -> r #

gmapQ :: (forall d. Data d => d -> u) -> QualPattern -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> QualPattern -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QualPattern -> m QualPattern #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QualPattern -> m QualPattern #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QualPattern -> m QualPattern #

Show QualPattern Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Generic QualPattern Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep QualPattern :: Type -> Type #

Binary QualPattern Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

NFData QualPattern Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: QualPattern -> () #

Hashable QualPattern Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint QualPattern Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep QualPattern Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier Source #

constructing qualifiers

Results

type FixSolution = HashMap KVar Expr Source #

type GFixSolution = GFixSol Expr Source #

Solutions and Results

toGFixSol :: HashMap KVar (e, [e]) -> GFixSol e Source #

data Result a Source #

Instances

Instances details
Functor Result Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

Show a => Show (Result a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

showsPrec :: Int -> Result a -> ShowS #

show :: Result a -> String #

showList :: [Result a] -> ShowS #

Generic (Result a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep (Result a) :: Type -> Type #

Methods

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

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

Semigroup (Result a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

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

Monoid (Result a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

mempty :: Result a #

mappend :: Result a -> Result a -> Result a #

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

NFData a => NFData (Result a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: Result a -> () #

type Rep (Result a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep (Result a) = D1 ('MetaData "Result" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "Result" 'PrefixI 'True) (S1 ('MetaSel ('Just "resStatus") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (FixResult a)) :*: (S1 ('MetaSel ('Just "resSolution") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FixSolution) :*: S1 ('MetaSel ('Just "gresSolution") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 GFixSolution))))

Cut KVars

newtype Kuts Source #

Constraint Cut Sets -------------------------------------------------------

Constructors

KS 

Fields

Instances

Instances details
Eq Kuts Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

Show Kuts Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

showsPrec :: Int -> Kuts -> ShowS #

show :: Kuts -> String #

showList :: [Kuts] -> ShowS #

Generic Kuts Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep Kuts :: Type -> Type #

Methods

from :: Kuts -> Rep Kuts x #

to :: Rep Kuts x -> Kuts #

Semigroup Kuts Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

(<>) :: Kuts -> Kuts -> Kuts #

sconcat :: NonEmpty Kuts -> Kuts #

stimes :: Integral b => b -> Kuts -> Kuts #

Monoid Kuts Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

mempty :: Kuts #

mappend :: Kuts -> Kuts -> Kuts #

mconcat :: [Kuts] -> Kuts #

Binary Kuts Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: Kuts -> Put #

get :: Get Kuts #

putList :: [Kuts] -> Put #

NFData Kuts Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: Kuts -> () #

Fixpoint Kuts Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep Kuts Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep Kuts = D1 ('MetaData "Kuts" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'True) (C1 ('MetaCons "KS" 'PrefixI 'True) (S1 ('MetaSel ('Just "ksVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet KVar))))

Higher Order Logic

data HOInfo Source #

Constructors

HOI 

Fields

Instances

Instances details
Eq HOInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

Show HOInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Generic HOInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep HOInfo :: Type -> Type #

Methods

from :: HOInfo -> Rep HOInfo x #

to :: Rep HOInfo x -> HOInfo #

Semigroup HOInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Monoid HOInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Binary HOInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: HOInfo -> Put #

get :: Get HOInfo #

putList :: [HOInfo] -> Put #

NFData HOInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: HOInfo -> () #

type Rep HOInfo Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep HOInfo = D1 ('MetaData "HOInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "HOI" 'PrefixI 'True) (S1 ('MetaSel ('Just "hoBinds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "hoQuals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

Axioms

data AxiomEnv Source #

Axiom Instantiation Information --------------------------------------

Constructors

AEnv 

Fields

Instances

Instances details
Eq AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Show AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Generic AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep AxiomEnv :: Type -> Type #

Methods

from :: AxiomEnv -> Rep AxiomEnv x #

to :: Rep AxiomEnv x -> AxiomEnv #

Semigroup AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Monoid AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Binary AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: AxiomEnv -> Put #

get :: Get AxiomEnv #

putList :: [AxiomEnv] -> Put #

NFData AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: AxiomEnv -> () #

PPrint AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Visitable AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> AxiomEnv -> VisitM a AxiomEnv Source #

Elaborate AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

type Rep AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep AxiomEnv = D1 ('MetaData "AxiomEnv" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "AEnv" 'PrefixI 'True) ((S1 ('MetaSel ('Just "aenvEqs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Equation]) :*: S1 ('MetaSel ('Just "aenvSimpl") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Rewrite])) :*: (S1 ('MetaSel ('Just "aenvExpand") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SubcId Bool)) :*: S1 ('MetaSel ('Just "aenvAutoRW") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SubcId [AutoRewrite])))))

data Equation Source #

Constructors

Equ 

Fields

Instances

Instances details
Eq Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Show Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Generic Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep Equation :: Type -> Type #

Methods

from :: Equation -> Rep Equation x #

to :: Rep Equation x -> Equation #

Binary Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: Equation -> Put #

get :: Get Equation #

putList :: [Equation] -> Put #

NFData Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: Equation -> () #

Hashable Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Subable Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Visitable Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> Equation -> VisitM a Equation Source #

Elaborate Equation Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

type Rep Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep Equation = D1 ('MetaData "Equation" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "Equ" 'PrefixI 'True) ((S1 ('MetaSel ('Just "eqName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "eqArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Symbol, Sort)])) :*: (S1 ('MetaSel ('Just "eqBody") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: (S1 ('MetaSel ('Just "eqSort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Just "eqRec") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)))))

data Rewrite Source #

Constructors

SMeasure 

Fields

Instances

Instances details
Eq Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

Show Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Generic Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep Rewrite :: Type -> Type #

Methods

from :: Rewrite -> Rep Rewrite x #

to :: Rep Rewrite x -> Rewrite #

Binary Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

put :: Rewrite -> Put #

get :: Get Rewrite #

putList :: [Rewrite] -> Put #

NFData Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: Rewrite -> () #

PPrint Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Visitable Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Visitor

Methods

visit :: Monoid a => Visitor a c -> c -> Rewrite -> VisitM a Rewrite Source #

Elaborate Rewrite Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

type Rep Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep Rewrite = D1 ('MetaData "Rewrite" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "SMeasure" 'PrefixI 'True) ((S1 ('MetaSel ('Just "smName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "smDC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)) :*: (S1 ('MetaSel ('Just "smArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "smBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))

data AutoRewrite Source #

Constructors

AutoRewrite 

Fields

Instances

Instances details
Eq AutoRewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Show AutoRewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Generic AutoRewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Associated Types

type Rep AutoRewrite :: Type -> Type #

Binary AutoRewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

NFData AutoRewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

rnf :: AutoRewrite -> () #

Hashable AutoRewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint (HashMap SubcId [AutoRewrite]) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

toFix :: HashMap SubcId [AutoRewrite] -> Doc Source #

simplify :: HashMap SubcId [AutoRewrite] -> HashMap SubcId [AutoRewrite] Source #

type Rep AutoRewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

type Rep AutoRewrite = D1 ('MetaData "AutoRewrite" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.8.10.2-inplace" 'False) (C1 ('MetaCons "AutoRewrite" 'PrefixI 'True) (S1 ('MetaSel ('Just "arArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortedReft]) :*: (S1 ('MetaSel ('Just "arLHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Just "arRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))

Misc [should be elsewhere but here due to dependencies]

gSorts :: [Sort] -> [Sort] Source #

Orphan instances

Binary Eliminate Source # 
Instance details

Binary SMTSolver Source # 
Instance details

NFData Eliminate Source # 
Instance details

Methods

rnf :: Eliminate -> () #

NFData SMTSolver Source # 
Instance details

Methods

rnf :: SMTSolver -> () #

Hashable SortedReft Source # 
Instance details

Fixpoint Doc Source # 
Instance details

Methods

toFix :: Doc -> Doc Source #

simplify :: Doc -> Doc Source #