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

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.8.10.2-inplace" '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))))))

data Cstr a Source #

Constructors

Head !Pred a

p

CAnd ![Cstr a]

c1 ... cn

All !Bind !(Cstr a)

all x:t. p => c

Any !Bind !(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 #

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 #

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

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 #

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 #

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
Eq Pred Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

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 #

Show Pred Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Pred -> ShowS #

show :: Pred -> String #

showList :: [Pred] -> ShowS #

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 #

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 #

Monoid Pred Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

mempty :: Pred #

mappend :: Pred -> Pred -> Pred #

mconcat :: [Pred] -> Pred #

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

Cst is an NNF Horn Constraint.

Constructors

Bind 

Fields

Instances

Instances details
Eq Bind Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

Data Bind 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 -> c Bind #

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

toConstr :: Bind -> Constr #

dataTypeOf :: Bind -> DataType #

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

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

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

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

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

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

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

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

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

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

Show Bind Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Bind -> ShowS #

show :: Bind -> String #

showList :: [Bind] -> ShowS #

Generic Bind Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Associated Types

type Rep Bind :: Type -> Type #

Methods

from :: Bind -> Rep Bind x #

to :: Rep Bind x -> Bind #

PPrint Bind Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Subable Bind Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

type Rep Bind Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

type Rep Bind = D1 ('MetaData "Bind" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.8.10.2-inplace" '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))))

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 #

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 #

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

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 #

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 #

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 #

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.8.10.2-inplace" '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))))

accessing constraint labels

cLabel :: Cstr a -> a Source #

invariants (refinements) on constraints

extract qualifiers