Safe Haskell | None |
---|---|
Language | Haskell98 |
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.
Instances
Functor Query Source # | |
Data a => Data (Query a) Source # | |
Defined in Language.Fixpoint.Horn.Types 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)))))) |
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 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 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
Instances
Functor Var Source # | |
Eq a => Eq (Var a) Source # | |
Data a => Data (Var a) Source # | |
Defined in Language.Fixpoint.Horn.Types 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)))) |