Safe Haskell | None |
---|---|
Language | Haskell98 |
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
Horn Constraints and their components
Query
is an NNF Horn Constraint.
Constructors
Query | |
Instances
Functor Query Source # | |
Data a => Data (Query a) Source # | |
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 # | |
type Rep (Query a) Source # | |
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)))))) |
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
HPred
is a Horn predicate that appears as LHS (body) or RHS (head) of constraints
Instances
Eq Pred Source # | |
Data Pred Source # | |
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 # 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 # | |
Generic Pred Source # | |
Semigroup Pred Source # | |
Monoid Pred Source # | |
PPrint Pred Source # | |
Defined in Language.Fixpoint.Horn.Types | |
Subable Pred Source # | |
Visitable Pred Source # | |
type Rep Pred Source # | |
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])))) |
Cst
is an NNF Horn Constraint.
Instances
Eq Bind Source # | |
Data Bind Source # | |
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 # 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 # | |
Generic Bind Source # | |
PPrint Bind Source # | |
Defined in Language.Fixpoint.Horn.Types | |
Subable Bind Source # | |
type Rep Bind Source # | |
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)))) |
HVar
is a Horn variable
Constructors
HVar | |
Instances
Functor Var Source # | |
Eq a => Eq (Var a) Source # | |
Data a => Data (Var a) Source # | |
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) # 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 # | |
Show (Var a) Source # | |
Generic (Var a) Source # | |
PPrint (Var a) Source # | |
Defined in Language.Fixpoint.Horn.Types | |
type Rep (Var a) Source # | |
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)))) |