liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Horn.Types

Description

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

Synopsis

Horn Constraints and their components

data Query a Source #

Query is an NNF Horn Constraint.

Constructors

Query 

Fields

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

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

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

Subable Pred Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

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

data Bind a Source #

Cst is an NNF Horn Constraint.

Constructors

Bind 

Fields

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

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"

accessing constraint labels

cLabel :: Cstr a -> a Source #

invariants (refinements) on constraints

extract qualifiers