{-# LANGUAGE OverloadedStrings, Safe, DeriveDataTypeable #-}
module SMTLib2.AST where
import Data.Typeable
import Data.Data
import Data.String(IsString(..))
newtype Name = N String
deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq,Eq Name
Eq Name =>
(Name -> Name -> Ordering)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> Ord Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmax :: Name -> Name -> Name
>= :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c< :: Name -> Name -> Bool
compare :: Name -> Name -> Ordering
$ccompare :: Name -> Name -> Ordering
$cp1Ord :: Eq Name
Ord,Int -> Name -> ShowS
[Name] -> ShowS
Name -> String
(Int -> Name -> ShowS)
-> (Name -> String) -> ([Name] -> ShowS) -> Show Name
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name] -> ShowS
$cshowList :: [Name] -> ShowS
show :: Name -> String
$cshow :: Name -> String
showsPrec :: Int -> Name -> ShowS
$cshowsPrec :: Int -> Name -> ShowS
Show,Typeable Name
Constr
DataType
Typeable Name =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name)
-> (Name -> Constr)
-> (Name -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Name))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name))
-> ((forall b. Data b => b -> b) -> Name -> Name)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r)
-> (forall u. (forall d. Data d => d -> u) -> Name -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Name -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Name -> m Name)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name -> m Name)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name -> m Name)
-> Data Name
Name -> Constr
Name -> DataType
(forall b. Data b => b -> b) -> Name -> Name
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Name -> u
forall u. (forall d. Data d => d -> u) -> Name -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Name -> m Name
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name -> m Name
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Name)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
$cN :: Constr
$tName :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Name -> m Name
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name -> m Name
gmapMp :: (forall d. Data d => d -> m d) -> Name -> m Name
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name -> m Name
gmapM :: (forall d. Data d => d -> m d) -> Name -> m Name
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Name -> m Name
gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Name -> u
gmapQ :: (forall d. Data d => d -> u) -> Name -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Name -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
gmapT :: (forall b. Data b => b -> b) -> Name -> Name
$cgmapT :: (forall b. Data b => b -> b) -> Name -> Name
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Name)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Name)
dataTypeOf :: Name -> DataType
$cdataTypeOf :: Name -> DataType
toConstr :: Name -> Constr
$ctoConstr :: Name -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name
$cp1Data :: Typeable Name
Data,Typeable)
data Ident = I Name [Integer]
deriving (Ident -> Ident -> Bool
(Ident -> Ident -> Bool) -> (Ident -> Ident -> Bool) -> Eq Ident
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ident -> Ident -> Bool
$c/= :: Ident -> Ident -> Bool
== :: Ident -> Ident -> Bool
$c== :: Ident -> Ident -> Bool
Eq,Eq Ident
Eq Ident =>
(Ident -> Ident -> Ordering)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Ident)
-> (Ident -> Ident -> Ident)
-> Ord Ident
Ident -> Ident -> Bool
Ident -> Ident -> Ordering
Ident -> Ident -> Ident
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ident -> Ident -> Ident
$cmin :: Ident -> Ident -> Ident
max :: Ident -> Ident -> Ident
$cmax :: Ident -> Ident -> Ident
>= :: Ident -> Ident -> Bool
$c>= :: Ident -> Ident -> Bool
> :: Ident -> Ident -> Bool
$c> :: Ident -> Ident -> Bool
<= :: Ident -> Ident -> Bool
$c<= :: Ident -> Ident -> Bool
< :: Ident -> Ident -> Bool
$c< :: Ident -> Ident -> Bool
compare :: Ident -> Ident -> Ordering
$ccompare :: Ident -> Ident -> Ordering
$cp1Ord :: Eq Ident
Ord,Int -> Ident -> ShowS
[Ident] -> ShowS
Ident -> String
(Int -> Ident -> ShowS)
-> (Ident -> String) -> ([Ident] -> ShowS) -> Show Ident
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ident] -> ShowS
$cshowList :: [Ident] -> ShowS
show :: Ident -> String
$cshow :: Ident -> String
showsPrec :: Int -> Ident -> ShowS
$cshowsPrec :: Int -> Ident -> ShowS
Show,Typeable Ident
Constr
DataType
Typeable Ident =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ident -> c Ident)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ident)
-> (Ident -> Constr)
-> (Ident -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ident))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident))
-> ((forall b. Data b => b -> b) -> Ident -> Ident)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r)
-> (forall u. (forall d. Data d => d -> u) -> Ident -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Ident -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ident -> m Ident)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ident -> m Ident)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ident -> m Ident)
-> Data Ident
Ident -> Constr
Ident -> DataType
(forall b. Data b => b -> b) -> Ident -> Ident
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ident -> c Ident
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ident
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Ident -> u
forall u. (forall d. Data d => d -> u) -> Ident -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ident -> m Ident
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ident -> m Ident
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ident
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ident -> c Ident
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ident)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident)
$cI :: Constr
$tIdent :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Ident -> m Ident
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ident -> m Ident
gmapMp :: (forall d. Data d => d -> m d) -> Ident -> m Ident
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ident -> m Ident
gmapM :: (forall d. Data d => d -> m d) -> Ident -> m Ident
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ident -> m Ident
gmapQi :: Int -> (forall d. Data d => d -> u) -> Ident -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ident -> u
gmapQ :: (forall d. Data d => d -> u) -> Ident -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Ident -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
gmapT :: (forall b. Data b => b -> b) -> Ident -> Ident
$cgmapT :: (forall b. Data b => b -> b) -> Ident -> Ident
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Ident)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ident)
dataTypeOf :: Ident -> DataType
$cdataTypeOf :: Ident -> DataType
toConstr :: Ident -> Constr
$ctoConstr :: Ident -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ident
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ident
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ident -> c Ident
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ident -> c Ident
$cp1Data :: Typeable Ident
Data,Typeable)
data Quant = Exists | Forall
deriving (Quant -> Quant -> Bool
(Quant -> Quant -> Bool) -> (Quant -> Quant -> Bool) -> Eq Quant
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Quant -> Quant -> Bool
$c/= :: Quant -> Quant -> Bool
== :: Quant -> Quant -> Bool
$c== :: Quant -> Quant -> Bool
Eq,Eq Quant
Eq Quant =>
(Quant -> Quant -> Ordering)
-> (Quant -> Quant -> Bool)
-> (Quant -> Quant -> Bool)
-> (Quant -> Quant -> Bool)
-> (Quant -> Quant -> Bool)
-> (Quant -> Quant -> Quant)
-> (Quant -> Quant -> Quant)
-> Ord Quant
Quant -> Quant -> Bool
Quant -> Quant -> Ordering
Quant -> Quant -> Quant
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Quant -> Quant -> Quant
$cmin :: Quant -> Quant -> Quant
max :: Quant -> Quant -> Quant
$cmax :: Quant -> Quant -> Quant
>= :: Quant -> Quant -> Bool
$c>= :: Quant -> Quant -> Bool
> :: Quant -> Quant -> Bool
$c> :: Quant -> Quant -> Bool
<= :: Quant -> Quant -> Bool
$c<= :: Quant -> Quant -> Bool
< :: Quant -> Quant -> Bool
$c< :: Quant -> Quant -> Bool
compare :: Quant -> Quant -> Ordering
$ccompare :: Quant -> Quant -> Ordering
$cp1Ord :: Eq Quant
Ord,Int -> Quant -> ShowS
[Quant] -> ShowS
Quant -> String
(Int -> Quant -> ShowS)
-> (Quant -> String) -> ([Quant] -> ShowS) -> Show Quant
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Quant] -> ShowS
$cshowList :: [Quant] -> ShowS
show :: Quant -> String
$cshow :: Quant -> String
showsPrec :: Int -> Quant -> ShowS
$cshowsPrec :: Int -> Quant -> ShowS
Show,Typeable Quant
Constr
DataType
Typeable Quant =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quant -> c Quant)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quant)
-> (Quant -> Constr)
-> (Quant -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quant))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant))
-> ((forall b. Data b => b -> b) -> Quant -> Quant)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r)
-> (forall u. (forall d. Data d => d -> u) -> Quant -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant)
-> Data Quant
Quant -> Constr
Quant -> DataType
(forall b. Data b => b -> b) -> Quant -> Quant
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quant -> c Quant
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quant
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
forall u. (forall d. Data d => d -> u) -> Quant -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quant
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quant -> c Quant
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quant)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
$cForall :: Constr
$cExists :: Constr
$tQuant :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Quant -> m Quant
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
gmapMp :: (forall d. Data d => d -> m d) -> Quant -> m Quant
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
gmapM :: (forall d. Data d => d -> m d) -> Quant -> m Quant
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
gmapQi :: Int -> (forall d. Data d => d -> u) -> Quant -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
gmapQ :: (forall d. Data d => d -> u) -> Quant -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Quant -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant
$cgmapT :: (forall b. Data b => b -> b) -> Quant -> Quant
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Quant)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quant)
dataTypeOf :: Quant -> DataType
$cdataTypeOf :: Quant -> DataType
toConstr :: Quant -> Constr
$ctoConstr :: Quant -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quant
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quant
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quant -> c Quant
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quant -> c Quant
$cp1Data :: Typeable Quant
Data,Typeable)
data Binder = Bind { Binder -> Name
bindVar :: Name, Binder -> Type
bindType :: Type }
deriving (Binder -> Binder -> Bool
(Binder -> Binder -> Bool)
-> (Binder -> Binder -> Bool) -> Eq Binder
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Binder -> Binder -> Bool
$c/= :: Binder -> Binder -> Bool
== :: Binder -> Binder -> Bool
$c== :: Binder -> Binder -> Bool
Eq,Eq Binder
Eq Binder =>
(Binder -> Binder -> Ordering)
-> (Binder -> Binder -> Bool)
-> (Binder -> Binder -> Bool)
-> (Binder -> Binder -> Bool)
-> (Binder -> Binder -> Bool)
-> (Binder -> Binder -> Binder)
-> (Binder -> Binder -> Binder)
-> Ord Binder
Binder -> Binder -> Bool
Binder -> Binder -> Ordering
Binder -> Binder -> Binder
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Binder -> Binder -> Binder
$cmin :: Binder -> Binder -> Binder
max :: Binder -> Binder -> Binder
$cmax :: Binder -> Binder -> Binder
>= :: Binder -> Binder -> Bool
$c>= :: Binder -> Binder -> Bool
> :: Binder -> Binder -> Bool
$c> :: Binder -> Binder -> Bool
<= :: Binder -> Binder -> Bool
$c<= :: Binder -> Binder -> Bool
< :: Binder -> Binder -> Bool
$c< :: Binder -> Binder -> Bool
compare :: Binder -> Binder -> Ordering
$ccompare :: Binder -> Binder -> Ordering
$cp1Ord :: Eq Binder
Ord,Int -> Binder -> ShowS
[Binder] -> ShowS
Binder -> String
(Int -> Binder -> ShowS)
-> (Binder -> String) -> ([Binder] -> ShowS) -> Show Binder
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Binder] -> ShowS
$cshowList :: [Binder] -> ShowS
show :: Binder -> String
$cshow :: Binder -> String
showsPrec :: Int -> Binder -> ShowS
$cshowsPrec :: Int -> Binder -> ShowS
Show,Typeable Binder
Constr
DataType
Typeable Binder =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Binder -> c Binder)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Binder)
-> (Binder -> Constr)
-> (Binder -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Binder))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder))
-> ((forall b. Data b => b -> b) -> Binder -> Binder)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Binder -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Binder -> r)
-> (forall u. (forall d. Data d => d -> u) -> Binder -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Binder -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Binder -> m Binder)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Binder -> m Binder)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Binder -> m Binder)
-> Data Binder
Binder -> Constr
Binder -> DataType
(forall b. Data b => b -> b) -> Binder -> Binder
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Binder -> c Binder
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Binder
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Binder -> u
forall u. (forall d. Data d => d -> u) -> Binder -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Binder -> m Binder
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Binder -> m Binder
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Binder
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Binder -> c Binder
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Binder)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder)
$cBind :: Constr
$tBinder :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Binder -> m Binder
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Binder -> m Binder
gmapMp :: (forall d. Data d => d -> m d) -> Binder -> m Binder
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Binder -> m Binder
gmapM :: (forall d. Data d => d -> m d) -> Binder -> m Binder
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Binder -> m Binder
gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Binder -> u
gmapQ :: (forall d. Data d => d -> u) -> Binder -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Binder -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
gmapT :: (forall b. Data b => b -> b) -> Binder -> Binder
$cgmapT :: (forall b. Data b => b -> b) -> Binder -> Binder
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Binder)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Binder)
dataTypeOf :: Binder -> DataType
$cdataTypeOf :: Binder -> DataType
toConstr :: Binder -> Constr
$ctoConstr :: Binder -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Binder
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Binder
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Binder -> c Binder
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Binder -> c Binder
$cp1Data :: Typeable Binder
Data,Typeable)
data Defn = Defn { Defn -> Name
defVar :: Name, Defn -> Expr
defExpr :: Expr }
deriving (Defn -> Defn -> Bool
(Defn -> Defn -> Bool) -> (Defn -> Defn -> Bool) -> Eq Defn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Defn -> Defn -> Bool
$c/= :: Defn -> Defn -> Bool
== :: Defn -> Defn -> Bool
$c== :: Defn -> Defn -> Bool
Eq,Eq Defn
Eq Defn =>
(Defn -> Defn -> Ordering)
-> (Defn -> Defn -> Bool)
-> (Defn -> Defn -> Bool)
-> (Defn -> Defn -> Bool)
-> (Defn -> Defn -> Bool)
-> (Defn -> Defn -> Defn)
-> (Defn -> Defn -> Defn)
-> Ord Defn
Defn -> Defn -> Bool
Defn -> Defn -> Ordering
Defn -> Defn -> Defn
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Defn -> Defn -> Defn
$cmin :: Defn -> Defn -> Defn
max :: Defn -> Defn -> Defn
$cmax :: Defn -> Defn -> Defn
>= :: Defn -> Defn -> Bool
$c>= :: Defn -> Defn -> Bool
> :: Defn -> Defn -> Bool
$c> :: Defn -> Defn -> Bool
<= :: Defn -> Defn -> Bool
$c<= :: Defn -> Defn -> Bool
< :: Defn -> Defn -> Bool
$c< :: Defn -> Defn -> Bool
compare :: Defn -> Defn -> Ordering
$ccompare :: Defn -> Defn -> Ordering
$cp1Ord :: Eq Defn
Ord,Int -> Defn -> ShowS
[Defn] -> ShowS
Defn -> String
(Int -> Defn -> ShowS)
-> (Defn -> String) -> ([Defn] -> ShowS) -> Show Defn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Defn] -> ShowS
$cshowList :: [Defn] -> ShowS
show :: Defn -> String
$cshow :: Defn -> String
showsPrec :: Int -> Defn -> ShowS
$cshowsPrec :: Int -> Defn -> ShowS
Show,Typeable Defn
Constr
DataType
Typeable Defn =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn)
-> (Defn -> Constr)
-> (Defn -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Defn))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn))
-> ((forall b. Data b => b -> b) -> Defn -> Defn)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r)
-> (forall u. (forall d. Data d => d -> u) -> Defn -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn)
-> Data Defn
Defn -> Constr
Defn -> DataType
(forall b. Data b => b -> b) -> Defn -> Defn
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
forall u. (forall d. Data d => d -> u) -> Defn -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Defn)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
$cDefn :: Constr
$tDefn :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Defn -> m Defn
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
gmapMp :: (forall d. Data d => d -> m d) -> Defn -> m Defn
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
gmapM :: (forall d. Data d => d -> m d) -> Defn -> m Defn
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
gmapQi :: Int -> (forall d. Data d => d -> u) -> Defn -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
gmapQ :: (forall d. Data d => d -> u) -> Defn -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Defn -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn
$cgmapT :: (forall b. Data b => b -> b) -> Defn -> Defn
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Defn)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Defn)
dataTypeOf :: Defn -> DataType
$cdataTypeOf :: Defn -> DataType
toConstr :: Defn -> Constr
$ctoConstr :: Defn -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn
$cp1Data :: Typeable Defn
Data,Typeable)
data Literal = LitBV Integer Integer
| LitNum Integer
| LitFrac Rational
| LitStr String
deriving (Literal -> Literal -> Bool
(Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool) -> Eq Literal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Literal -> Literal -> Bool
$c/= :: Literal -> Literal -> Bool
== :: Literal -> Literal -> Bool
$c== :: Literal -> Literal -> Bool
Eq,Eq Literal
Eq Literal =>
(Literal -> Literal -> Ordering)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Literal)
-> (Literal -> Literal -> Literal)
-> Ord Literal
Literal -> Literal -> Bool
Literal -> Literal -> Ordering
Literal -> Literal -> Literal
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Literal -> Literal -> Literal
$cmin :: Literal -> Literal -> Literal
max :: Literal -> Literal -> Literal
$cmax :: Literal -> Literal -> Literal
>= :: Literal -> Literal -> Bool
$c>= :: Literal -> Literal -> Bool
> :: Literal -> Literal -> Bool
$c> :: Literal -> Literal -> Bool
<= :: Literal -> Literal -> Bool
$c<= :: Literal -> Literal -> Bool
< :: Literal -> Literal -> Bool
$c< :: Literal -> Literal -> Bool
compare :: Literal -> Literal -> Ordering
$ccompare :: Literal -> Literal -> Ordering
$cp1Ord :: Eq Literal
Ord,Int -> Literal -> ShowS
[Literal] -> ShowS
Literal -> String
(Int -> Literal -> ShowS)
-> (Literal -> String) -> ([Literal] -> ShowS) -> Show Literal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Literal] -> ShowS
$cshowList :: [Literal] -> ShowS
show :: Literal -> String
$cshow :: Literal -> String
showsPrec :: Int -> Literal -> ShowS
$cshowsPrec :: Int -> Literal -> ShowS
Show,Typeable Literal
Constr
DataType
Typeable Literal =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal)
-> (Literal -> Constr)
-> (Literal -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Literal))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal))
-> ((forall b. Data b => b -> b) -> Literal -> Literal)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r)
-> (forall u. (forall d. Data d => d -> u) -> Literal -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal)
-> Data Literal
Literal -> Constr
Literal -> DataType
(forall b. Data b => b -> b) -> Literal -> Literal
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
forall u. (forall d. Data d => d -> u) -> Literal -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Literal)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
$cLitStr :: Constr
$cLitFrac :: Constr
$cLitNum :: Constr
$cLitBV :: Constr
$tLiteral :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Literal -> m Literal
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
gmapMp :: (forall d. Data d => d -> m d) -> Literal -> m Literal
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
gmapM :: (forall d. Data d => d -> m d) -> Literal -> m Literal
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
gmapQi :: Int -> (forall d. Data d => d -> u) -> Literal -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
gmapQ :: (forall d. Data d => d -> u) -> Literal -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Literal -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal
$cgmapT :: (forall b. Data b => b -> b) -> Literal -> Literal
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Literal)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Literal)
dataTypeOf :: Literal -> DataType
$cdataTypeOf :: Literal -> DataType
toConstr :: Literal -> Constr
$ctoConstr :: Literal -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal
$cp1Data :: Typeable Literal
Data,Typeable)
data Type = TApp Ident [Type]
| TVar Name
deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq,Eq Type
Eq Type =>
(Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c< :: Type -> Type -> Bool
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
$cp1Ord :: Eq Type
Ord,Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show,Typeable Type
Constr
DataType
Typeable Type =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type)
-> (Type -> Constr)
-> (Type -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type))
-> ((forall b. Data b => b -> b) -> Type -> Type)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
-> (forall u. (forall d. Data d => d -> u) -> Type -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Type -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type)
-> Data Type
Type -> Constr
Type -> DataType
(forall b. Data b => b -> b) -> Type -> Type
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
forall u. (forall d. Data d => d -> u) -> Type -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cTVar :: Constr
$cTApp :: Constr
$tType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapMp :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapM :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
gmapQ :: (forall d. Data d => d -> u) -> Type -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapT :: (forall b. Data b => b -> b) -> Type -> Type
$cgmapT :: (forall b. Data b => b -> b) -> Type -> Type
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Type)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
dataTypeOf :: Type -> DataType
$cdataTypeOf :: Type -> DataType
toConstr :: Type -> Constr
$ctoConstr :: Type -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cp1Data :: Typeable Type
Data,Typeable)
data Expr = Lit Literal
| App Ident (Maybe Type) [Expr]
| Quant Quant [Binder] Expr
| Let [Defn] Expr
| Annot Expr [Attr]
deriving (Expr -> Expr -> Bool
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c== :: Expr -> Expr -> Bool
Eq,Eq Expr
Eq Expr =>
(Expr -> Expr -> Ordering)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Expr)
-> (Expr -> Expr -> Expr)
-> Ord Expr
Expr -> Expr -> Bool
Expr -> Expr -> Ordering
Expr -> Expr -> Expr
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Expr -> Expr -> Expr
$cmin :: Expr -> Expr -> Expr
max :: Expr -> Expr -> Expr
$cmax :: Expr -> Expr -> Expr
>= :: Expr -> Expr -> Bool
$c>= :: Expr -> Expr -> Bool
> :: Expr -> Expr -> Bool
$c> :: Expr -> Expr -> Bool
<= :: Expr -> Expr -> Bool
$c<= :: Expr -> Expr -> Bool
< :: Expr -> Expr -> Bool
$c< :: Expr -> Expr -> Bool
compare :: Expr -> Expr -> Ordering
$ccompare :: Expr -> Expr -> Ordering
$cp1Ord :: Eq Expr
Ord,Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> String
(Int -> Expr -> ShowS)
-> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show,Typeable Expr
Constr
DataType
Typeable Expr =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr -> c Expr)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Expr)
-> (Expr -> Constr)
-> (Expr -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Expr))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr))
-> ((forall b. Data b => b -> b) -> Expr -> Expr)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r)
-> (forall u. (forall d. Data d => d -> u) -> Expr -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr)
-> Data Expr
Expr -> Constr
Expr -> DataType
(forall b. Data b => b -> b) -> Expr -> Expr
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr -> c Expr
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Expr
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u
forall u. (forall d. Data d => d -> u) -> Expr -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Expr
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr -> c Expr
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Expr)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr)
$cAnnot :: Constr
$cLet :: Constr
$cQuant :: Constr
$cApp :: Constr
$cLit :: Constr
$tExpr :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Expr -> m Expr
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
gmapMp :: (forall d. Data d => d -> m d) -> Expr -> m Expr
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
gmapM :: (forall d. Data d => d -> m d) -> Expr -> m Expr
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u
gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Expr -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr
$cgmapT :: (forall b. Data b => b -> b) -> Expr -> Expr
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Expr)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Expr)
dataTypeOf :: Expr -> DataType
$cdataTypeOf :: Expr -> DataType
toConstr :: Expr -> Constr
$ctoConstr :: Expr -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Expr
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Expr
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr -> c Expr
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr -> c Expr
$cp1Data :: Typeable Expr
Data,Typeable)
data Attr = Attr { Attr -> Name
attrName :: Name , Attr -> Maybe Expr
attrVal :: Maybe AttrVal }
deriving (Attr -> Attr -> Bool
(Attr -> Attr -> Bool) -> (Attr -> Attr -> Bool) -> Eq Attr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Attr -> Attr -> Bool
$c/= :: Attr -> Attr -> Bool
== :: Attr -> Attr -> Bool
$c== :: Attr -> Attr -> Bool
Eq,Eq Attr
Eq Attr =>
(Attr -> Attr -> Ordering)
-> (Attr -> Attr -> Bool)
-> (Attr -> Attr -> Bool)
-> (Attr -> Attr -> Bool)
-> (Attr -> Attr -> Bool)
-> (Attr -> Attr -> Attr)
-> (Attr -> Attr -> Attr)
-> Ord Attr
Attr -> Attr -> Bool
Attr -> Attr -> Ordering
Attr -> Attr -> Attr
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Attr -> Attr -> Attr
$cmin :: Attr -> Attr -> Attr
max :: Attr -> Attr -> Attr
$cmax :: Attr -> Attr -> Attr
>= :: Attr -> Attr -> Bool
$c>= :: Attr -> Attr -> Bool
> :: Attr -> Attr -> Bool
$c> :: Attr -> Attr -> Bool
<= :: Attr -> Attr -> Bool
$c<= :: Attr -> Attr -> Bool
< :: Attr -> Attr -> Bool
$c< :: Attr -> Attr -> Bool
compare :: Attr -> Attr -> Ordering
$ccompare :: Attr -> Attr -> Ordering
$cp1Ord :: Eq Attr
Ord,Int -> Attr -> ShowS
[Attr] -> ShowS
Attr -> String
(Int -> Attr -> ShowS)
-> (Attr -> String) -> ([Attr] -> ShowS) -> Show Attr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Attr] -> ShowS
$cshowList :: [Attr] -> ShowS
show :: Attr -> String
$cshow :: Attr -> String
showsPrec :: Int -> Attr -> ShowS
$cshowsPrec :: Int -> Attr -> ShowS
Show,Typeable Attr
Constr
DataType
Typeable Attr =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Attr -> c Attr)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Attr)
-> (Attr -> Constr)
-> (Attr -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Attr))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr))
-> ((forall b. Data b => b -> b) -> Attr -> Attr)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r)
-> (forall u. (forall d. Data d => d -> u) -> Attr -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Attr -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Attr -> m Attr)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Attr -> m Attr)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Attr -> m Attr)
-> Data Attr
Attr -> Constr
Attr -> DataType
(forall b. Data b => b -> b) -> Attr -> Attr
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Attr -> c Attr
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Attr
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Attr -> u
forall u. (forall d. Data d => d -> u) -> Attr -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Attr -> m Attr
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Attr -> m Attr
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Attr
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Attr -> c Attr
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Attr)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr)
$cAttr :: Constr
$tAttr :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Attr -> m Attr
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Attr -> m Attr
gmapMp :: (forall d. Data d => d -> m d) -> Attr -> m Attr
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Attr -> m Attr
gmapM :: (forall d. Data d => d -> m d) -> Attr -> m Attr
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Attr -> m Attr
gmapQi :: Int -> (forall d. Data d => d -> u) -> Attr -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Attr -> u
gmapQ :: (forall d. Data d => d -> u) -> Attr -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Attr -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
gmapT :: (forall b. Data b => b -> b) -> Attr -> Attr
$cgmapT :: (forall b. Data b => b -> b) -> Attr -> Attr
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Attr)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Attr)
dataTypeOf :: Attr -> DataType
$cdataTypeOf :: Attr -> DataType
toConstr :: Attr -> Constr
$ctoConstr :: Attr -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Attr
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Attr
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Attr -> c Attr
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Attr -> c Attr
$cp1Data :: Typeable Attr
Data,Typeable)
type AttrVal = Expr
data Option
= OptPrintSuccess Bool
| OptExpandDefinitions Bool
| OptInteractiveMode Bool
| OptProduceProofs Bool
| OptProduceUnsatCores Bool
| OptProduceModels Bool
| OptProduceAssignments Bool
| OptRegularOutputChannel String
| OptDiagnosticOutputChannel String
| OptRandomSeed Integer
| OptVerbosity Integer
| OptAttr Attr
deriving (Typeable Option
Constr
DataType
Typeable Option =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Option -> c Option)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Option)
-> (Option -> Constr)
-> (Option -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Option))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Option))
-> ((forall b. Data b => b -> b) -> Option -> Option)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Option -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Option -> r)
-> (forall u. (forall d. Data d => d -> u) -> Option -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Option -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Option -> m Option)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Option -> m Option)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Option -> m Option)
-> Data Option
Option -> Constr
Option -> DataType
(forall b. Data b => b -> b) -> Option -> Option
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Option -> c Option
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Option
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Option -> u
forall u. (forall d. Data d => d -> u) -> Option -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Option -> m Option
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Option -> m Option
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Option
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Option -> c Option
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Option)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Option)
$cOptAttr :: Constr
$cOptVerbosity :: Constr
$cOptRandomSeed :: Constr
$cOptDiagnosticOutputChannel :: Constr
$cOptRegularOutputChannel :: Constr
$cOptProduceAssignments :: Constr
$cOptProduceModels :: Constr
$cOptProduceUnsatCores :: Constr
$cOptProduceProofs :: Constr
$cOptInteractiveMode :: Constr
$cOptExpandDefinitions :: Constr
$cOptPrintSuccess :: Constr
$tOption :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Option -> m Option
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Option -> m Option
gmapMp :: (forall d. Data d => d -> m d) -> Option -> m Option
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Option -> m Option
gmapM :: (forall d. Data d => d -> m d) -> Option -> m Option
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Option -> m Option
gmapQi :: Int -> (forall d. Data d => d -> u) -> Option -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Option -> u
gmapQ :: (forall d. Data d => d -> u) -> Option -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Option -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
gmapT :: (forall b. Data b => b -> b) -> Option -> Option
$cgmapT :: (forall b. Data b => b -> b) -> Option -> Option
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Option)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Option)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Option)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Option)
dataTypeOf :: Option -> DataType
$cdataTypeOf :: Option -> DataType
toConstr :: Option -> Constr
$ctoConstr :: Option -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Option
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Option
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Option -> c Option
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Option -> c Option
$cp1Data :: Typeable Option
Data,Typeable)
data InfoFlag
= InfoAllStatistics
| InfoErrorBehavior
| InfoName
| InfoAuthors
| InfoVersion
| InfoStatus
| InfoReasonUnknown
| InfoAttr Attr
deriving (Typeable InfoFlag
Constr
DataType
Typeable InfoFlag =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InfoFlag -> c InfoFlag)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c InfoFlag)
-> (InfoFlag -> Constr)
-> (InfoFlag -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c InfoFlag))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoFlag))
-> ((forall b. Data b => b -> b) -> InfoFlag -> InfoFlag)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InfoFlag -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InfoFlag -> r)
-> (forall u. (forall d. Data d => d -> u) -> InfoFlag -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> InfoFlag -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag)
-> Data InfoFlag
InfoFlag -> Constr
InfoFlag -> DataType
(forall b. Data b => b -> b) -> InfoFlag -> InfoFlag
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InfoFlag -> c InfoFlag
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c InfoFlag
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> InfoFlag -> u
forall u. (forall d. Data d => d -> u) -> InfoFlag -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c InfoFlag
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InfoFlag -> c InfoFlag
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c InfoFlag)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoFlag)
$cInfoAttr :: Constr
$cInfoReasonUnknown :: Constr
$cInfoStatus :: Constr
$cInfoVersion :: Constr
$cInfoAuthors :: Constr
$cInfoName :: Constr
$cInfoErrorBehavior :: Constr
$cInfoAllStatistics :: Constr
$tInfoFlag :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
gmapMp :: (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
gmapM :: (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
gmapQi :: Int -> (forall d. Data d => d -> u) -> InfoFlag -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> InfoFlag -> u
gmapQ :: (forall d. Data d => d -> u) -> InfoFlag -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> InfoFlag -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
gmapT :: (forall b. Data b => b -> b) -> InfoFlag -> InfoFlag
$cgmapT :: (forall b. Data b => b -> b) -> InfoFlag -> InfoFlag
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoFlag)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoFlag)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c InfoFlag)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c InfoFlag)
dataTypeOf :: InfoFlag -> DataType
$cdataTypeOf :: InfoFlag -> DataType
toConstr :: InfoFlag -> Constr
$ctoConstr :: InfoFlag -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c InfoFlag
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c InfoFlag
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InfoFlag -> c InfoFlag
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InfoFlag -> c InfoFlag
$cp1Data :: Typeable InfoFlag
Data,Typeable)
data Command
= CmdSetLogic Name
| CmdSetOption Option
| CmdSetInfo Attr
| CmdDeclareType Name Integer
| CmdDefineType Name [Name] Type
| CmdDeclareConst Name Type
| CmdDeclareFun Name [Type] Type
| CmdDefineFun Name [Binder] Type Expr
| CmdPush Integer
| CmdPop Integer
| CmdAssert Expr
| CmdCheckSat
| CmdGetAssertions
| CmdGetValue [Expr]
| CmdGetProof
| CmdGetUnsatCore
| CmdGetInfo InfoFlag
| CmdGetOption Name
| String
| CmdExit
deriving (,Typeable)
newtype Script = Script [Command]
instance IsString Name where fromString :: String -> Name
fromString = String -> Name
N
instance IsString Ident where fromString :: String -> Ident
fromString x :: String
x = Name -> [Integer] -> Ident
I (String -> Name
forall a. IsString a => String -> a
fromString String
x) []
instance IsString Type where fromString :: String -> Type
fromString x :: String
x = Ident -> [Type] -> Type
TApp (String -> Ident
forall a. IsString a => String -> a
fromString String
x) []
instance IsString Expr where fromString :: String -> Expr
fromString = Literal -> Expr
Lit (Literal -> Expr) -> (String -> Literal) -> String -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Literal
LitStr (String -> Literal) -> ShowS -> String -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. IsString a => String -> a
fromString
instance Num Expr where
fromInteger :: Integer -> Expr
fromInteger x :: Integer
x = Literal -> Expr
Lit (Integer -> Literal
LitNum Integer
x)
x :: Expr
x + :: Expr -> Expr -> Expr
+ y :: Expr
y = Ident -> [Expr] -> Expr
app "+" [Expr
x,Expr
y]
x :: Expr
x - :: Expr -> Expr -> Expr
- y :: Expr
y = Ident -> [Expr] -> Expr
app "-" [Expr
x,Expr
y]
x :: Expr
x * :: Expr -> Expr -> Expr
* y :: Expr
y = Ident -> [Expr] -> Expr
app "*" [Expr
x,Expr
y]
signum :: Expr -> Expr
signum x :: Expr
x = Ident -> [Expr] -> Expr
app "signum" [Expr
x]
abs :: Expr -> Expr
abs x :: Expr
x = Ident -> [Expr] -> Expr
app "abs" [Expr
x]
instance Fractional Expr where
fromRational :: Rational -> Expr
fromRational x :: Rational
x = Literal -> Expr
Lit (Rational -> Literal
LitFrac Rational
x)
x :: Expr
x / :: Expr -> Expr -> Expr
/ y :: Expr
y = Ident -> [Expr] -> Expr
app "/" [Expr
x,Expr
y]
app :: Ident -> [Expr] -> Expr
app :: Ident -> [Expr] -> Expr
app f :: Ident
f es :: [Expr]
es = Ident -> Maybe Type -> [Expr] -> Expr
App Ident
f Maybe Type
forall a. Maybe a
Nothing [Expr]
es