{-# 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
Ord,Int -> Name -> String -> String
[Name] -> String -> String
Name -> String
(Int -> Name -> String -> String)
-> (Name -> String) -> ([Name] -> String -> String) -> Show Name
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Name] -> String -> String
$cshowList :: [Name] -> String -> String
show :: Name -> String
$cshow :: Name -> String
showsPrec :: Int -> Name -> String -> String
$cshowsPrec :: Int -> Name -> String -> String
Show,Typeable Name
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 -> DataType
Name -> Constr
(forall b. Data b => b -> b) -> Name -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Name -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Name -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Name -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Name -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
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
Ord,Int -> Ident -> String -> String
[Ident] -> String -> String
Ident -> String
(Int -> Ident -> String -> String)
-> (Ident -> String) -> ([Ident] -> String -> String) -> Show Ident
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Ident] -> String -> String
$cshowList :: [Ident] -> String -> String
show :: Ident -> String
$cshow :: Ident -> String
showsPrec :: Int -> Ident -> String -> String
$cshowsPrec :: Int -> Ident -> String -> String
Show,Typeable Ident
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 -> DataType
Ident -> Constr
(forall b. Data b => b -> b) -> Ident -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Ident -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ident -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Ident -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Ident -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
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
Ord,Int -> Quant -> String -> String
[Quant] -> String -> String
Quant -> String
(Int -> Quant -> String -> String)
-> (Quant -> String) -> ([Quant] -> String -> String) -> Show Quant
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Quant] -> String -> String
$cshowList :: [Quant] -> String -> String
show :: Quant -> String
$cshow :: Quant -> String
showsPrec :: Int -> Quant -> String -> String
$cshowsPrec :: Int -> Quant -> String -> String
Show,Typeable Quant
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 -> DataType
Quant -> Constr
(forall b. Data b => b -> b) -> Quant -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Quant -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Quant -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
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
Ord,Int -> Binder -> String -> String
[Binder] -> String -> String
Binder -> String
(Int -> Binder -> String -> String)
-> (Binder -> String)
-> ([Binder] -> String -> String)
-> Show Binder
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Binder] -> String -> String
$cshowList :: [Binder] -> String -> String
show :: Binder -> String
$cshow :: Binder -> String
showsPrec :: Int -> Binder -> String -> String
$cshowsPrec :: Int -> Binder -> String -> String
Show,Typeable Binder
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 -> DataType
Binder -> Constr
(forall b. Data b => b -> b) -> Binder -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Binder -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Binder -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Binder -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Binder -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
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
Ord,Int -> Defn -> String -> String
[Defn] -> String -> String
Defn -> String
(Int -> Defn -> String -> String)
-> (Defn -> String) -> ([Defn] -> String -> String) -> Show Defn
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Defn] -> String -> String
$cshowList :: [Defn] -> String -> String
show :: Defn -> String
$cshow :: Defn -> String
showsPrec :: Int -> Defn -> String -> String
$cshowsPrec :: Int -> Defn -> String -> String
Show,Typeable Defn
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 -> DataType
Defn -> Constr
(forall b. Data b => b -> b) -> Defn -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Defn -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Defn -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
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
Ord,Int -> Literal -> String -> String
[Literal] -> String -> String
Literal -> String
(Int -> Literal -> String -> String)
-> (Literal -> String)
-> ([Literal] -> String -> String)
-> Show Literal
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Literal] -> String -> String
$cshowList :: [Literal] -> String -> String
show :: Literal -> String
$cshow :: Literal -> String
showsPrec :: Int -> Literal -> String -> String
$cshowsPrec :: Int -> Literal -> String -> String
Show,Typeable Literal
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 -> DataType
Literal -> Constr
(forall b. Data b => b -> b) -> Literal -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Literal -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Literal -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
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
Ord,Int -> Type -> String -> String
[Type] -> String -> String
Type -> String
(Int -> Type -> String -> String)
-> (Type -> String) -> ([Type] -> String -> String) -> Show Type
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Type] -> String -> String
$cshowList :: [Type] -> String -> String
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> String -> String
$cshowsPrec :: Int -> Type -> String -> String
Show,Typeable Type
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 -> DataType
Type -> Constr
(forall b. Data b => b -> b) -> Type -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
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
Ord,Int -> Expr -> String -> String
[Expr] -> String -> String
Expr -> String
(Int -> Expr -> String -> String)
-> (Expr -> String) -> ([Expr] -> String -> String) -> Show Expr
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Expr] -> String -> String
$cshowList :: [Expr] -> String -> String
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> String -> String
$cshowsPrec :: Int -> Expr -> String -> String
Show,Typeable Expr
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 -> DataType
Expr -> Constr
(forall b. Data b => b -> b) -> Expr -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Expr -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Expr -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
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
Ord,Int -> Attr -> String -> String
[Attr] -> String -> String
Attr -> String
(Int -> Attr -> String -> String)
-> (Attr -> String) -> ([Attr] -> String -> String) -> Show Attr
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Attr] -> String -> String
$cshowList :: [Attr] -> String -> String
show :: Attr -> String
$cshow :: Attr -> String
showsPrec :: Int -> Attr -> String -> String
$cshowsPrec :: Int -> Attr -> String -> String
Show,Typeable Attr
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 -> DataType
Attr -> Constr
(forall b. Data b => b -> b) -> Attr -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Attr -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Attr -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Attr -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Attr -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
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
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 -> DataType
Option -> Constr
(forall b. Data b => b -> b) -> Option -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Option -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Option -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Option -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Option -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data,Typeable)
data InfoFlag
= InfoAllStatistics
| InfoErrorBehavior
| InfoName
| InfoAuthors
| InfoVersion
| InfoStatus
| InfoReasonUnknown
| InfoAttr Attr
deriving (Typeable InfoFlag
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 -> DataType
InfoFlag -> Constr
(forall b. Data b => b -> b) -> InfoFlag -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> InfoFlag -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> InfoFlag -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> InfoFlag -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> InfoFlag -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
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 Command
Typeable Command
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Command -> c Command)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Command)
-> (Command -> Constr)
-> (Command -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Command))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command))
-> ((forall b. Data b => b -> b) -> Command -> Command)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r)
-> (forall u. (forall d. Data d => d -> u) -> Command -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Command -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Command -> m Command)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command)
-> Data Command
Command -> DataType
Command -> Constr
(forall b. Data b => b -> b) -> Command -> Command
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) -> Command -> u
forall u. (forall d. Data d => d -> u) -> Command -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Command -> m Command
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Command
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Command -> c Command
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Command)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Command -> m Command
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Command -> m Command
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Command -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Command -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Command -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Command -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
gmapT :: (forall b. Data b => b -> b) -> Command -> Command
$cgmapT :: (forall b. Data b => b -> b) -> Command -> Command
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Command)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Command)
dataTypeOf :: Command -> DataType
$cdataTypeOf :: Command -> DataType
toConstr :: Command -> Constr
$ctoConstr :: Command -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Command
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Command
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Command -> c Command
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Command -> c Command
Data,Typeable)
newtype Script = Script [Command]
instance IsString Name where fromString :: String -> Name
fromString = String -> Name
N
instance IsString Ident where fromString :: String -> Ident
fromString 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 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) -> (String -> String) -> String -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. IsString a => String -> a
fromString
instance Num Expr where
fromInteger :: Integer -> Expr
fromInteger Integer
x = Literal -> Expr
Lit (Integer -> Literal
LitNum Integer
x)
Expr
x + :: Expr -> Expr -> Expr
+ Expr
y = Ident -> [Expr] -> Expr
app Ident
"+" [Expr
x,Expr
y]
Expr
x - :: Expr -> Expr -> Expr
- Expr
y = Ident -> [Expr] -> Expr
app Ident
"-" [Expr
x,Expr
y]
Expr
x * :: Expr -> Expr -> Expr
* Expr
y = Ident -> [Expr] -> Expr
app Ident
"*" [Expr
x,Expr
y]
signum :: Expr -> Expr
signum Expr
x = Ident -> [Expr] -> Expr
app Ident
"signum" [Expr
x]
abs :: Expr -> Expr
abs Expr
x = Ident -> [Expr] -> Expr
app Ident
"abs" [Expr
x]
instance Fractional Expr where
fromRational :: Rational -> Expr
fromRational Rational
x = Literal -> Expr
Lit (Rational -> Literal
LitFrac Rational
x)
Expr
x / :: Expr -> Expr -> Expr
/ Expr
y = Ident -> [Expr] -> Expr
app Ident
"/" [Expr
x,Expr
y]
app :: Ident -> [Expr] -> Expr
app :: Ident -> [Expr] -> Expr
app Ident
f [Expr]
es = Ident -> Maybe Type -> [Expr] -> Expr
App Ident
f Maybe Type
forall a. Maybe a
Nothing [Expr]
es