Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Horn.Types

Contents

Horn Constraints and their components
Raw Query
accessing constraint labels
invariants (refinements) on constraints
extract qualifiers

Description

This module formalizes the key datatypes needed to represent Horn NNF constraints as described in "Local Refinement Typing", ICFP 2017

Synopsis

data Query a = Query {
- qQuals :: ![Qualifier]
- qVars :: ![Var a]
- qCstr :: !(Cstr a)
- qCon :: HashMap Symbol Sort
- qDis :: HashMap Symbol Sort
- qEqns :: ![Equation]
- qMats :: ![Rewrite]
- qData :: ![DataDecl]
}
data Cstr a
- = Head !Pred !a
- | CAnd ![Cstr a]
- | All !(Bind a) !(Cstr a)
- | Any !(Bind a) !(Cstr a)
data Pred
- = Reft !Expr
- | Var !Symbol ![Symbol]
- | PAnd ![Pred]
data Bind a = Bind {
- bSym :: !Symbol
- bSort :: !Sort
- bPred :: !Pred
- bMeta :: !a
}
data Var a = HVar {
- hvName :: !Symbol
- hvArgs :: ![Sort]
- hvMeta :: a
}
data Tag
- = NoTag
- | Tag String
type TagVar = Var Tag
type TagQuery = Query Tag
cLabel :: Cstr a -> a
okCstr :: Cstr a -> Bool
quals :: Cstr a -> [Qualifier]

Horn Constraints and their components

data Query a Source #

Query is an NNF Horn Constraint.

Constructors

Query

Fields

qQuals :: ![Qualifier]
qualifiers over which to solve cstrs
qVars :: ![Var a]
kvars, with parameter-sorts
qCstr :: !(Cstr a)
list of constraints
qCon :: HashMap Symbol Sort
list of constants (uninterpreted functions
qDis :: HashMap Symbol Sort
list of constants (uninterpreted functions
qEqns :: ![Equation]
list of equations
qMats :: ![Rewrite]
list of match-es
qData :: ![DataDecl]
list of data-declarations

Instances

Instances details

Functor Query Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods fmap :: (a -> b) -> Query a -> Query b # (<$) :: a -> Query b -> Query a #
Data a => Data (Query a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Query a -> c (Query a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Query a) # toConstr :: Query a -> Constr # dataTypeOf :: Query a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Query a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Query a)) # gmapT :: (forall b. Data b => b -> b) -> Query a -> Query a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Query a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Query a -> r # gmapQ :: (forall d. Data d => d -> u) -> Query a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Query a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Query a -> m (Query a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Query a -> m (Query a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Query a -> m (Query a) #
Generic (Query a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Associated Types type Rep (Query a) :: Type -> Type # Methods from :: Query a -> Rep (Query a) x # to :: Rep (Query a) x -> Query a #
PPrint (Query a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Query a -> Doc Source # pprintPrec :: Int -> Tidy -> Query a -> Doc Source #
type Rep (Query a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types type Rep (Query a) = D1 ('MetaData "Query" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "Query" 'PrefixI 'True) (((S1 ('MetaSel ('Just "qQuals") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Qualifier]) :: S1 ('MetaSel ('Just "qVars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Var a])) :: (S1 ('MetaSel ('Just "qCstr") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Cstr a)) :: S1 ('MetaSel ('Just "qCon") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap Symbol Sort)))) :: ((S1 ('MetaSel ('Just "qDis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap Symbol Sort)) :: S1 ('MetaSel ('Just "qEqns") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Equation])) :: (S1 ('MetaSel ('Just "qMats") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Rewrite]) :*: S1 ('MetaSel ('Just "qData") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl])))))

data Cstr a Source #

Constructors

Head !Pred !a	p
CAnd ![Cstr a]	c1 ... cn
All !(Bind a) !(Cstr a)	all x:t. p => c
Any !(Bind a) !(Cstr a)	exi x:t. p / c or is it exi x:t. p => c?

Instances

Instances details

Functor Cstr Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods fmap :: (a -> b) -> Cstr a -> Cstr b # (<$) :: a -> Cstr b -> Cstr a #
Data a => Data (Cstr a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Cstr a -> c (Cstr a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Cstr a) # toConstr :: Cstr a -> Constr # dataTypeOf :: Cstr a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Cstr a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Cstr a)) # gmapT :: (forall b. Data b => b -> b) -> Cstr a -> Cstr a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Cstr a -> r # gmapQ :: (forall d. Data d => d -> u) -> Cstr a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Cstr a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Cstr a -> m (Cstr a) #
Generic (Cstr a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Associated Types type Rep (Cstr a) :: Type -> Type # Methods from :: Cstr a -> Rep (Cstr a) x # to :: Rep (Cstr a) x -> Cstr a #
Show (Cstr a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods showsPrec :: Int -> Cstr a -> ShowS # show :: Cstr a -> String # showList :: [Cstr a] -> ShowS #
Eq a => Eq (Cstr a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods (==) :: Cstr a -> Cstr a -> Bool # (/=) :: Cstr a -> Cstr a -> Bool #
PPrint (Cstr a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Cstr a -> Doc Source # pprintPrec :: Int -> Tidy -> Cstr a -> Doc Source #
Visitable (Cstr a) Source #
Instance details Defined in Language.Fixpoint.Horn.Transformations Methods visit :: Monoid a0 => Visitor a0 c -> c -> Cstr a -> VisitM a0 (Cstr a) Source #
type Rep (Cstr a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types type Rep (Cstr a) = D1 ('MetaData "Cstr" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) ((C1 ('MetaCons "Head" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Pred) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)) :+: C1 ('MetaCons "CAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Cstr a]))) :+: (C1 ('MetaCons "All" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Bind a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Cstr a))) :+: C1 ('MetaCons "Any" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Bind a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Cstr a)))))

data Pred Source #

HPred is a Horn predicate that appears as LHS (body) or RHS (head) of constraints

Constructors

Reft !Expr	r
Var !Symbol ![Symbol]	$k(y1..yn)
PAnd ![Pred]	p1 ... pn

Instances

Instances details

Data Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pred -> c Pred # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pred # toConstr :: Pred -> Constr # dataTypeOf :: Pred -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pred) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred) # gmapT :: (forall b. Data b => b -> b) -> Pred -> Pred # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r # gmapQ :: (forall d. Data d => d -> u) -> Pred -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pred -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pred -> m Pred # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pred -> m Pred # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pred -> m Pred #
Monoid Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods mempty :: Pred # mappend :: Pred -> Pred -> Pred # mconcat :: [Pred] -> Pred #
Semigroup Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods (<>) :: Pred -> Pred -> Pred # sconcat :: NonEmpty Pred -> Pred # stimes :: Integral b => b -> Pred -> Pred #
Generic Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Associated Types type Rep Pred :: Type -> Type # Methods from :: Pred -> Rep Pred x # to :: Rep Pred x -> Pred #
Show Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods showsPrec :: Int -> Pred -> ShowS # show :: Pred -> String # showList :: [Pred] -> ShowS #
Eq Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods (==) :: Pred -> Pred -> Bool # (/=) :: Pred -> Pred -> Bool #
PPrint Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Pred -> Doc Source # pprintPrec :: Int -> Tidy -> Pred -> Doc Source #
Subable Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods syms :: Pred -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Pred -> Pred Source # substf :: (Symbol -> Expr) -> Pred -> Pred Source # subst :: Subst -> Pred -> Pred Source # subst1 :: Pred -> (Symbol, Expr) -> Pred Source #
Visitable Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Transformations Methods visit :: Monoid a => Visitor a c -> c -> Pred -> VisitM a Pred Source #
type Rep Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types type Rep Pred = D1 ('MetaData "Pred" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "Reft" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr)) :+: (C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Symbol])) :+: C1 ('MetaCons "PAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Pred]))))

data Bind a Source #

Cst is an NNF Horn Constraint.

Constructors

Bind
Fields bSym :: !Symbol bSort :: !Sort bPred :: !Pred bMeta :: !a

Instances

Instances details

Functor Bind Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods fmap :: (a -> b) -> Bind a -> Bind b # (<$) :: a -> Bind b -> Bind a #
Data a => Data (Bind a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Bind a -> c (Bind a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Bind a) # toConstr :: Bind a -> Constr # dataTypeOf :: Bind a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Bind a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Bind a)) # gmapT :: (forall b. Data b => b -> b) -> Bind a -> Bind a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bind a -> r # gmapQ :: (forall d. Data d => d -> u) -> Bind a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Bind a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Bind a -> m (Bind a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Bind a -> m (Bind a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Bind a -> m (Bind a) #
Generic (Bind a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Associated Types type Rep (Bind a) :: Type -> Type # Methods from :: Bind a -> Rep (Bind a) x # to :: Rep (Bind a) x -> Bind a #
Show (Bind a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods showsPrec :: Int -> Bind a -> ShowS # show :: Bind a -> String # showList :: [Bind a] -> ShowS #
Eq a => Eq (Bind a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods (==) :: Bind a -> Bind a -> Bool # (/=) :: Bind a -> Bind a -> Bool #
PPrint (Bind a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Bind a -> Doc Source # pprintPrec :: Int -> Tidy -> Bind a -> Doc Source #
Subable (Bind a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods syms :: Bind a -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Bind a -> Bind a Source # substf :: (Symbol -> Expr) -> Bind a -> Bind a Source # subst :: Subst -> Bind a -> Bind a Source # subst1 :: Bind a -> (Symbol, Expr) -> Bind a Source #
type Rep (Bind a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types type Rep (Bind a) = D1 ('MetaData "Bind" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "Bind" 'PrefixI 'True) ((S1 ('MetaSel ('Just "bSym") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :: S1 ('MetaSel ('Just "bSort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)) :: (S1 ('MetaSel ('Just "bPred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Pred) :*: S1 ('MetaSel ('Just "bMeta") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a))))

data Var a Source #

HVar is a Horn variable

Constructors

HVar
Fields hvName :: !Symbol name of the variable $k1, $k2 etc. hvArgs :: ![Sort] sorts of its parameters i.e. of the relation defined by the `HVar` hvMeta :: a meta-data

Instances

Instances details

Functor Var Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods fmap :: (a -> b) -> Var a -> Var b # (<$) :: a -> Var b -> Var a #
Data a => Data (Var a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Var a -> c (Var a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Var a) # toConstr :: Var a -> Constr # dataTypeOf :: Var a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Var a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a)) # gmapT :: (forall b. Data b => b -> b) -> Var a -> Var a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r # gmapQ :: (forall d. Data d => d -> u) -> Var a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Var a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Var a -> m (Var a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Var a -> m (Var a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Var a -> m (Var a) #
Generic (Var a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Associated Types type Rep (Var a) :: Type -> Type # Methods from :: Var a -> Rep (Var a) x # to :: Rep (Var a) x -> Var a #
Show (Var a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods showsPrec :: Int -> Var a -> ShowS # show :: Var a -> String # showList :: [Var a] -> ShowS #
Eq a => Eq (Var a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods (==) :: Var a -> Var a -> Bool # (/=) :: Var a -> Var a -> Bool #
Ord a => Ord (Var a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods compare :: Var a -> Var a -> Ordering # (<) :: Var a -> Var a -> Bool # (<=) :: Var a -> Var a -> Bool # (>) :: Var a -> Var a -> Bool # (>=) :: Var a -> Var a -> Bool # max :: Var a -> Var a -> Var a # min :: Var a -> Var a -> Var a #
PPrint (Var a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Var a -> Doc Source # pprintPrec :: Int -> Tidy -> Var a -> Doc Source #
type Rep (Var a) Source #
Instance details Defined in Language.Fixpoint.Horn.Types type Rep (Var a) = D1 ('MetaData "Var" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "HVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "hvName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :: (S1 ('MetaSel ('Just "hvArgs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Sort]) :: S1 ('MetaSel ('Just "hvMeta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

Raw Query

data Tag Source #

Constructors

NoTag
Tag String

Instances

Instances details

ToJSON Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toJSON :: Tag -> Value # toEncoding :: Tag -> Encoding # toJSONList :: [Tag] -> Value # toEncodingList :: [Tag] -> Encoding #
Data Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Tag -> c Tag # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Tag # toConstr :: Tag -> Constr # dataTypeOf :: Tag -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Tag) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Tag) # gmapT :: (forall b. Data b => b -> b) -> Tag -> Tag # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tag -> r # gmapQ :: (forall d. Data d => d -> u) -> Tag -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Tag -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Tag -> m Tag # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Tag -> m Tag # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Tag -> m Tag #
Generic Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types Associated Types type Rep Tag :: Type -> Type # Methods from :: Tag -> Rep Tag x # to :: Rep Tag x -> Tag #
Show Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods showsPrec :: Int -> Tag -> ShowS # show :: Tag -> String # showList :: [Tag] -> ShowS #
NFData Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods rnf :: Tag -> () #
Fixpoint Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods toFix :: Tag -> Doc Source # simplify :: Tag -> Tag Source #
PPrint Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Tag -> Doc Source # pprintPrec :: Int -> Tidy -> Tag -> Doc Source #
Loc Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods srcSpan :: Tag -> SrcSpan Source #
type Rep Tag Source #
Instance details Defined in Language.Fixpoint.Horn.Types type Rep Tag = D1 ('MetaData "Tag" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "NoTag" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Tag" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

type TagVar = Var Tag Source #

Tag each query with a possible string denoting "provenance"

type TagQuery = Query Tag Source #

accessing constraint labels

cLabel :: Cstr a -> a Source #

invariants (refinements) on constraints

okCstr :: Cstr a -> Bool Source #

extract qualifiers

quals :: Cstr a -> [Qualifier] Source #