Language.Fixpoint.Horn.Types

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

Horn Constraints and their components

data Query a

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

Instances

Functor Query

Defined in Language.Fixpoint.Horn.Types

Methods

fmap :: (a -> b) -> Query a -> Query b

(<$) :: a -> Query b -> Query a

Data a => Data (Query a)

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)

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)

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

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

Functor Cstr

Defined in Language.Fixpoint.Horn.Types

Methods

fmap :: (a -> b) -> Cstr a -> Cstr b

(<$) :: a -> Cstr b -> Cstr a

Eq a => Eq (Cstr a)

Defined in Language.Fixpoint.Horn.Types

Methods

(==) :: Cstr a -> Cstr a -> Bool

(/=) :: Cstr a -> Cstr a -> Bool

Data a => Data (Cstr a)

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)

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Cstr a -> ShowS

show :: Cstr a -> String

showList :: [Cstr a] -> ShowS

Generic (Cstr a)

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)

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Cstr a -> Doc

pprintPrec :: Int -> Tidy -> Cstr a -> Doc

Visitable (Cstr a)

Defined in Language.Fixpoint.Horn.Transformations

Methods

visit :: Monoid a0 => Visitor a0 c -> c -> Cstr a -> VisitM a0 (Cstr a)

type Rep (Cstr a)

Defined in Language.Fixpoint.Horn.Types

type Rep (Cstr a) = D1 ('MetaData "Cstr" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.8.10.2-inplace" 'False) ((C1 ('MetaCons "Head" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Pred) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (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) :*: 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) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Cstr a)))))

data Pred

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

Eq Pred

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

Data Pred

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

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Pred -> ShowS

show :: Pred -> String

showList :: [Pred] -> ShowS

Generic Pred

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

Defined in Language.Fixpoint.Horn.Types

Methods

(<>) :: Pred -> Pred -> Pred

sconcat :: NonEmpty Pred -> Pred

stimes :: Integral b => b -> Pred -> Pred

Monoid Pred

Defined in Language.Fixpoint.Horn.Types

Methods

mempty :: Pred

mappend :: Pred -> Pred -> Pred

mconcat :: [Pred] -> Pred

PPrint Pred

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Pred -> Doc

pprintPrec :: Int -> Tidy -> Pred -> Doc

Subable Pred

Defined in Language.Fixpoint.Horn.Types

Methods

syms :: Pred -> [Symbol]

substa :: (Symbol -> Symbol) -> Pred -> Pred

substf :: (Symbol -> Expr) -> Pred -> Pred

subst :: Subst -> Pred -> Pred

subst1 :: Pred -> (Symbol, Expr) -> Pred

Visitable Pred

Defined in Language.Fixpoint.Horn.Transformations

Methods

visit :: Monoid a => Visitor a c -> c -> Pred -> VisitM a Pred

type Rep Pred

Defined in Language.Fixpoint.Horn.Types

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

Cst is an NNF Horn Constraint.

Constructors

Bind

Fields

• bSym :: !Symbol
• bSort :: !Sort
• bPred :: !Pred

Instances

Eq Bind

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

Data Bind

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

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Bind -> ShowS

show :: Bind -> String

showList :: [Bind] -> ShowS

Generic Bind

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

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Bind -> Doc

pprintPrec :: Int -> Tidy -> Bind -> Doc

Subable Bind

Defined in Language.Fixpoint.Horn.Types

Methods

syms :: Bind -> [Symbol]

substa :: (Symbol -> Symbol) -> Bind -> Bind

substf :: (Symbol -> Expr) -> Bind -> Bind

subst :: Subst -> Bind -> Bind

subst1 :: Bind -> (Symbol, Expr) -> Bind

type Rep Bind

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

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

Functor Var

Defined in Language.Fixpoint.Horn.Types

Methods

fmap :: (a -> b) -> Var a -> Var b

(<$) :: a -> Var b -> Var a

Eq a => Eq (Var a)

Defined in Language.Fixpoint.Horn.Types

Methods

(==) :: Var a -> Var a -> Bool

(/=) :: Var a -> Var a -> Bool

Data a => Data (Var a)

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)

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)

Defined in Language.Fixpoint.Horn.Types

Methods

showsPrec :: Int -> Var a -> ShowS

show :: Var a -> String

showList :: [Var a] -> ShowS

Generic (Var a)

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)

Defined in Language.Fixpoint.Horn.Types

Methods

pprintTidy :: Tidy -> Var a -> Doc

pprintPrec :: Int -> Tidy -> Var a -> Doc

type Rep (Var a)

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

invariants (refinements) on constraints

okCstr :: Cstr a -> Bool

dummyBind :: Bind

extract qualifiers

quals :: Cstr a -> [Qualifier]