Safe Haskell | None |
---|---|
Language | Haskell98 |
Language.Fixpoint.Horn.Types
Contents
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 :: (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-Ld6PWXA9XrKe3HZnOCc57" 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 :: (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-Ld6PWXA9XrKe3HZnOCc57" 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 :: (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-Ld6PWXA9XrKe3HZnOCc57" 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 :: (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-Ld6PWXA9XrKe3HZnOCc57" 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)))) |