liquid-fixpoint-0.9.6.3.4: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Triggers

Documentation

data Triggered a Source #

Constructors

Instances

Instances details

Functor Triggered Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

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

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

Generic (Triggered a) Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Associated Types

type Rep (Triggered a)

Instance details

Defined in Language.Fixpoint.Types.Triggers

type Rep (Triggered a) = D1 ('MetaData "Triggered" "Language.Fixpoint.Types.Triggers" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "TR" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Trigger) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

Methods

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

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

Show a => Show (Triggered a) Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

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

show :: Triggered a -> String #

showList :: [Triggered a] -> ShowS #

NFData a => NFData (Triggered a) Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

rnf :: Triggered a -> () #

Eq a => Eq (Triggered a) Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

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

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

Defunc a => Defunc (Triggered a) Source #

Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

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

SMTLIB2 (Triggered Expr) Source #

Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: Triggered Expr -> SymM Builder Source #

Elaborate e => Elaborate (Triggered e) Source #

Instance details

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: ElabParam -> Triggered e -> Triggered e Source #

PPrint a => PPrint (Triggered a) Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

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

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

Store a => Store (Triggered a) Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

size :: Size (Triggered a) #

poke :: Triggered a -> Poke () #

peek :: Peek (Triggered a) #

type Rep (Triggered a) Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

type Rep (Triggered a) = D1 ('MetaData "Triggered" "Language.Fixpoint.Types.Triggers" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "TR" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Trigger) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

data Trigger Source #

Constructors

NoTrigger
LeftHandSide

Instances

Instances details

Generic Trigger Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Associated Types

type Rep Trigger
Instance details Defined in Language.Fixpoint.Types.Triggers type Rep Trigger = D1 ('MetaData "Trigger" "Language.Fixpoint.Types.Triggers" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "NoTrigger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LeftHandSide" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: Trigger -> Rep Trigger x #

to :: Rep Trigger x -> Trigger #

Show Trigger Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

showsPrec :: Int -> Trigger -> ShowS #

show :: Trigger -> String #

showList :: [Trigger] -> ShowS #

NFData Trigger Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

rnf :: Trigger -> () #

Eq Trigger Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

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

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

PPrint Trigger Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

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

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

Store Trigger Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

Methods

size :: Size Trigger #

poke :: Trigger -> Poke () #

peek :: Peek Trigger #

type Rep Trigger Source #

Instance details

Defined in Language.Fixpoint.Types.Triggers

type Rep Trigger = D1 ('MetaData "Trigger" "Language.Fixpoint.Types.Triggers" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "NoTrigger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LeftHandSide" 'PrefixI 'False) (U1 :: Type -> Type))

noTrigger :: e -> Triggered e Source #

defaultTrigger :: e -> Triggered e Source #

makeTriggers :: Triggered Expr -> [Expr] Source #