Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Horn.Types

Contents

Horn Constraints and their components
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
}
data Cstr a
- = Head !Pred a
- | CAnd ![Cstr a]
- | All !Bind !(Cstr a)
- | Any !Bind !(Cstr a)
data Pred
- = Reft !Expr
- | Var !Symbol ![Symbol]
- | PAnd ![Pred]
data Bind = Bind {
- bSym :: !Symbol
- bSort :: !Sort
- bPred :: !Pred
}
data Var a = HVar {
- hvName :: !Symbol
- hvArgs :: ![Sort]
- hvMeta :: a
}
cLabel :: Cstr a -> a
okCstr :: Cstr a -> Bool
dummyBind :: Bind
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

Instances

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 :: (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.0.2-EGSzGwrlcJrCaUaEYLNzOY" 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

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 :: (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 type Rep (Cstr a) = D1 (MetaData "Cstr" "Language.Fixpoint.Horn.Types" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" 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 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

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 :: (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 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.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" 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 Source #

Cst is an NNF Horn Constraint.

Constructors

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

Instances

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 :: (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 Methods pprintTidy :: Tidy -> Bind -> Doc Source # pprintPrec :: Int -> Tidy -> Bind -> Doc Source #
Subable Bind Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods syms :: Bind -> [Symbol] Source # substa :: (Symbol -> Symbol) -> Bind -> Bind Source # substf :: (Symbol -> Expr) -> Bind -> Bind Source # subst :: Subst -> Bind -> Bind Source # subst1 :: Bind -> (Symbol, Expr) -> Bind Source #
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.0.2-EGSzGwrlcJrCaUaEYLNzOY" 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

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 :: (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.0.2-EGSzGwrlcJrCaUaEYLNzOY" 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

okCstr :: Cstr a -> Bool Source #

dummyBind :: Bind Source #

extract qualifiers

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