{-# LANGUAGE OverloadedStrings, Safe, DeriveDataTypeable #-}
module SMTLib1.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
$c== :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
/= :: 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
$ccompare :: Name -> Name -> Ordering
compare :: Name -> Name -> Ordering
$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
>= :: Name -> Name -> Bool
$cmax :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
min :: Name -> Name -> Name
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
$cshowsPrec :: Int -> Name -> String -> String
showsPrec :: Int -> Name -> String -> String
$cshow :: Name -> String
show :: Name -> String
$cshowList :: [Name] -> String -> String
showList :: [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 -> Constr
Name -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name
$ctoConstr :: Name -> Constr
toConstr :: Name -> Constr
$cdataTypeOf :: Name -> DataType
dataTypeOf :: Name -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Name)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Name)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
$cgmapT :: (forall b. Data b => b -> b) -> Name -> Name
gmapT :: (forall b. Data b => b -> b) -> Name -> Name
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Name -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Name -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Name -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Name -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name -> m Name
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name -> m Name
Data,Typeable)
data Ident = I Name [Integer]
deriving (Sort -> Sort -> Bool
(Sort -> Sort -> Bool) -> (Sort -> Sort -> Bool) -> Eq Sort
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Sort -> Sort -> Bool
== :: Sort -> Sort -> Bool
$c/= :: Sort -> Sort -> Bool
/= :: Sort -> Sort -> Bool
Eq,Eq Sort
Eq Sort
-> (Sort -> Sort -> Ordering)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Sort)
-> (Sort -> Sort -> Sort)
-> Ord Sort
Sort -> Sort -> Bool
Sort -> Sort -> Ordering
Sort -> Sort -> Sort
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
$ccompare :: Sort -> Sort -> Ordering
compare :: Sort -> Sort -> Ordering
$c< :: Sort -> Sort -> Bool
< :: Sort -> Sort -> Bool
$c<= :: Sort -> Sort -> Bool
<= :: Sort -> Sort -> Bool
$c> :: Sort -> Sort -> Bool
> :: Sort -> Sort -> Bool
$c>= :: Sort -> Sort -> Bool
>= :: Sort -> Sort -> Bool
$cmax :: Sort -> Sort -> Sort
max :: Sort -> Sort -> Sort
$cmin :: Sort -> Sort -> Sort
min :: Sort -> Sort -> Sort
Ord,Int -> Sort -> String -> String
[Sort] -> String -> String
Sort -> String
(Int -> Sort -> String -> String)
-> (Sort -> String) -> ([Sort] -> String -> String) -> Show Sort
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Sort -> String -> String
showsPrec :: Int -> Sort -> String -> String
$cshow :: Sort -> String
show :: Sort -> String
$cshowList :: [Sort] -> String -> String
showList :: [Sort] -> String -> String
Show,Typeable Sort
Typeable Sort
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort -> c Sort)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sort)
-> (Sort -> Constr)
-> (Sort -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sort))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort))
-> ((forall b. Data b => b -> b) -> Sort -> Sort)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sort -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sort -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort)
-> Data Sort
Sort -> Constr
Sort -> DataType
(forall b. Data b => b -> b) -> Sort -> Sort
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) -> Sort -> u
forall u. (forall d. Data d => d -> u) -> Sort -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sort
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort -> c Sort
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sort)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort -> c Sort
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sort -> c Sort
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sort
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sort
$ctoConstr :: Sort -> Constr
toConstr :: Sort -> Constr
$cdataTypeOf :: Sort -> DataType
dataTypeOf :: Sort -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sort)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sort)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort)
$cgmapT :: (forall b. Data b => b -> b) -> Sort -> Sort
gmapT :: (forall b. Data b => b -> b) -> Sort -> Sort
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sort -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Sort -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sort -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sort -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sort -> m Sort
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
$c== :: Quant -> Quant -> Bool
== :: Quant -> Quant -> Bool
$c/= :: Quant -> Quant -> Bool
/= :: 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
$ccompare :: Quant -> Quant -> Ordering
compare :: Quant -> Quant -> Ordering
$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
>= :: Quant -> Quant -> Bool
$cmax :: Quant -> Quant -> Quant
max :: Quant -> Quant -> Quant
$cmin :: Quant -> Quant -> Quant
min :: Quant -> Quant -> Quant
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
$cshowsPrec :: Int -> Quant -> String -> String
showsPrec :: Int -> Quant -> String -> String
$cshow :: Quant -> String
show :: Quant -> String
$cshowList :: [Quant] -> String -> String
showList :: [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 -> Constr
Quant -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quant -> c Quant
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Quant -> c Quant
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quant
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Quant
$ctoConstr :: Quant -> Constr
toConstr :: Quant -> Constr
$cdataTypeOf :: Quant -> DataType
dataTypeOf :: Quant -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quant)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Quant)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
$cgmapT :: (forall b. Data b => b -> b) -> Quant -> Quant
gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Quant -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Quant -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Quant -> m Quant
Data,Typeable)
data Conn = Not | Implies | And | Or | Xor | Iff | IfThenElse
deriving (Conn -> Conn -> Bool
(Conn -> Conn -> Bool) -> (Conn -> Conn -> Bool) -> Eq Conn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Conn -> Conn -> Bool
== :: Conn -> Conn -> Bool
$c/= :: Conn -> Conn -> Bool
/= :: Conn -> Conn -> Bool
Eq,Eq Conn
Eq Conn
-> (Conn -> Conn -> Ordering)
-> (Conn -> Conn -> Bool)
-> (Conn -> Conn -> Bool)
-> (Conn -> Conn -> Bool)
-> (Conn -> Conn -> Bool)
-> (Conn -> Conn -> Conn)
-> (Conn -> Conn -> Conn)
-> Ord Conn
Conn -> Conn -> Bool
Conn -> Conn -> Ordering
Conn -> Conn -> Conn
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
$ccompare :: Conn -> Conn -> Ordering
compare :: Conn -> Conn -> Ordering
$c< :: Conn -> Conn -> Bool
< :: Conn -> Conn -> Bool
$c<= :: Conn -> Conn -> Bool
<= :: Conn -> Conn -> Bool
$c> :: Conn -> Conn -> Bool
> :: Conn -> Conn -> Bool
$c>= :: Conn -> Conn -> Bool
>= :: Conn -> Conn -> Bool
$cmax :: Conn -> Conn -> Conn
max :: Conn -> Conn -> Conn
$cmin :: Conn -> Conn -> Conn
min :: Conn -> Conn -> Conn
Ord,Int -> Conn -> String -> String
[Conn] -> String -> String
Conn -> String
(Int -> Conn -> String -> String)
-> (Conn -> String) -> ([Conn] -> String -> String) -> Show Conn
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Conn -> String -> String
showsPrec :: Int -> Conn -> String -> String
$cshow :: Conn -> String
show :: Conn -> String
$cshowList :: [Conn] -> String -> String
showList :: [Conn] -> String -> String
Show,Typeable Conn
Typeable Conn
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Conn -> c Conn)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Conn)
-> (Conn -> Constr)
-> (Conn -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Conn))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conn))
-> ((forall b. Data b => b -> b) -> Conn -> Conn)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r)
-> (forall u. (forall d. Data d => d -> u) -> Conn -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Conn -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn)
-> Data Conn
Conn -> Constr
Conn -> DataType
(forall b. Data b => b -> b) -> Conn -> Conn
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) -> Conn -> u
forall u. (forall d. Data d => d -> u) -> Conn -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Conn
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Conn -> c Conn
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Conn)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conn)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Conn -> c Conn
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Conn -> c Conn
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Conn
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Conn
$ctoConstr :: Conn -> Constr
toConstr :: Conn -> Constr
$cdataTypeOf :: Conn -> DataType
dataTypeOf :: Conn -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Conn)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Conn)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conn)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conn)
$cgmapT :: (forall b. Data b => b -> b) -> Conn -> Conn
gmapT :: (forall b. Data b => b -> b) -> Conn -> Conn
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Conn -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Conn -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Conn -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Conn -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Conn -> m Conn
Data,Typeable)
data Formula = FTrue
| FFalse
| FPred Ident [Term]
| FVar Name
| Conn Conn [Formula]
| Quant Quant [Binder] Formula
| Let Name Term Formula
| FLet Name Formula Formula
| FAnnot Formula [Annot]
deriving (Formula -> Formula -> Bool
(Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool) -> Eq Formula
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Formula -> Formula -> Bool
== :: Formula -> Formula -> Bool
$c/= :: Formula -> Formula -> Bool
/= :: Formula -> Formula -> Bool
Eq,Eq Formula
Eq Formula
-> (Formula -> Formula -> Ordering)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Formula)
-> (Formula -> Formula -> Formula)
-> Ord Formula
Formula -> Formula -> Bool
Formula -> Formula -> Ordering
Formula -> Formula -> Formula
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
$ccompare :: Formula -> Formula -> Ordering
compare :: Formula -> Formula -> Ordering
$c< :: Formula -> Formula -> Bool
< :: Formula -> Formula -> Bool
$c<= :: Formula -> Formula -> Bool
<= :: Formula -> Formula -> Bool
$c> :: Formula -> Formula -> Bool
> :: Formula -> Formula -> Bool
$c>= :: Formula -> Formula -> Bool
>= :: Formula -> Formula -> Bool
$cmax :: Formula -> Formula -> Formula
max :: Formula -> Formula -> Formula
$cmin :: Formula -> Formula -> Formula
min :: Formula -> Formula -> Formula
Ord,Int -> Formula -> String -> String
[Formula] -> String -> String
Formula -> String
(Int -> Formula -> String -> String)
-> (Formula -> String)
-> ([Formula] -> String -> String)
-> Show Formula
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Formula -> String -> String
showsPrec :: Int -> Formula -> String -> String
$cshow :: Formula -> String
show :: Formula -> String
$cshowList :: [Formula] -> String -> String
showList :: [Formula] -> String -> String
Show,Typeable Formula
Typeable Formula
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula)
-> (Formula -> Constr)
-> (Formula -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula))
-> ((forall b. Data b => b -> b) -> Formula -> Formula)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r)
-> (forall u. (forall d. Data d => d -> u) -> Formula -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula)
-> Data Formula
Formula -> Constr
Formula -> DataType
(forall b. Data b => b -> b) -> Formula -> Formula
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) -> Formula -> u
forall u. (forall d. Data d => d -> u) -> Formula -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
$ctoConstr :: Formula -> Constr
toConstr :: Formula -> Constr
$cdataTypeOf :: Formula -> DataType
dataTypeOf :: Formula -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
$cgmapT :: (forall b. Data b => b -> b) -> Formula -> Formula
gmapT :: (forall b. Data b => b -> b) -> Formula -> Formula
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Formula -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Formula -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
Data,Typeable)
type Sort = Ident
data Binder = Bind { Binder -> Name
bindVar :: Name, Binder -> Sort
bindSort :: Sort }
deriving (Binder -> Binder -> Bool
(Binder -> Binder -> Bool)
-> (Binder -> Binder -> Bool) -> Eq Binder
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Binder -> Binder -> Bool
== :: Binder -> Binder -> Bool
$c/= :: Binder -> Binder -> Bool
/= :: 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
$ccompare :: Binder -> Binder -> Ordering
compare :: Binder -> Binder -> Ordering
$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
>= :: Binder -> Binder -> Bool
$cmax :: Binder -> Binder -> Binder
max :: Binder -> Binder -> Binder
$cmin :: Binder -> Binder -> Binder
min :: Binder -> Binder -> Binder
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
$cshowsPrec :: Int -> Binder -> String -> String
showsPrec :: Int -> Binder -> String -> String
$cshow :: Binder -> String
show :: Binder -> String
$cshowList :: [Binder] -> String -> String
showList :: [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 -> Constr
Binder -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Binder -> c Binder
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Binder -> c Binder
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Binder
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Binder
$ctoConstr :: Binder -> Constr
toConstr :: Binder -> Constr
$cdataTypeOf :: Binder -> DataType
dataTypeOf :: Binder -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Binder)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Binder)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder)
$cgmapT :: (forall b. Data b => b -> b) -> Binder -> Binder
gmapT :: (forall b. Data b => b -> b) -> Binder -> Binder
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Binder -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Binder -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Binder -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Binder -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Binder -> m Binder
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Binder -> m Binder
Data,Typeable)
data Term = Var Name
| App Ident [Term]
| Lit Literal
| ITE Formula Term Term
| TAnnot Term [Annot]
deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
/= :: Term -> Term -> Bool
Eq,Eq Term
Eq Term
-> (Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
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
$ccompare :: Term -> Term -> Ordering
compare :: Term -> Term -> Ordering
$c< :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
>= :: Term -> Term -> Bool
$cmax :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
min :: Term -> Term -> Term
Ord,Int -> Term -> String -> String
[Term] -> String -> String
Term -> String
(Int -> Term -> String -> String)
-> (Term -> String) -> ([Term] -> String -> String) -> Show Term
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Term -> String -> String
showsPrec :: Int -> Term -> String -> String
$cshow :: Term -> String
show :: Term -> String
$cshowList :: [Term] -> String -> String
showList :: [Term] -> String -> String
Show,Typeable Term
Typeable Term
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term)
-> (Term -> Constr)
-> (Term -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term))
-> ((forall b. Data b => b -> b) -> Term -> Term)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r)
-> (forall u. (forall d. Data d => d -> u) -> Term -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Term -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term)
-> Data Term
Term -> Constr
Term -> DataType
(forall b. Data b => b -> b) -> Term -> Term
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) -> Term -> u
forall u. (forall d. Data d => d -> u) -> Term -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
$ctoConstr :: Term -> Constr
toConstr :: Term -> Constr
$cdataTypeOf :: Term -> DataType
dataTypeOf :: Term -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
$cgmapT :: (forall b. Data b => b -> b) -> Term -> Term
gmapT :: (forall b. Data b => b -> b) -> Term -> Term
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Term -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Term -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
Data,Typeable)
data Literal = 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
$c== :: Literal -> Literal -> Bool
== :: Literal -> Literal -> Bool
$c/= :: Literal -> Literal -> Bool
/= :: 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
$ccompare :: Literal -> Literal -> Ordering
compare :: Literal -> Literal -> Ordering
$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
>= :: Literal -> Literal -> Bool
$cmax :: Literal -> Literal -> Literal
max :: Literal -> Literal -> Literal
$cmin :: Literal -> Literal -> Literal
min :: Literal -> Literal -> Literal
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
$cshowsPrec :: Int -> Literal -> String -> String
showsPrec :: Int -> Literal -> String -> String
$cshow :: Literal -> String
show :: Literal -> String
$cshowList :: [Literal] -> String -> String
showList :: [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 -> Constr
Literal -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Literal -> c Literal
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Literal
$ctoConstr :: Literal -> Constr
toConstr :: Literal -> Constr
$cdataTypeOf :: Literal -> DataType
dataTypeOf :: Literal -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Literal)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Literal)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
$cgmapT :: (forall b. Data b => b -> b) -> Literal -> Literal
gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Literal -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Literal -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Literal -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Literal -> m Literal
Data,Typeable)
data Annot = Attr { Annot -> Name
attrName :: Name, Annot -> Maybe String
attrVal :: Maybe String }
deriving (Annot -> Annot -> Bool
(Annot -> Annot -> Bool) -> (Annot -> Annot -> Bool) -> Eq Annot
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Annot -> Annot -> Bool
== :: Annot -> Annot -> Bool
$c/= :: Annot -> Annot -> Bool
/= :: Annot -> Annot -> Bool
Eq,Eq Annot
Eq Annot
-> (Annot -> Annot -> Ordering)
-> (Annot -> Annot -> Bool)
-> (Annot -> Annot -> Bool)
-> (Annot -> Annot -> Bool)
-> (Annot -> Annot -> Bool)
-> (Annot -> Annot -> Annot)
-> (Annot -> Annot -> Annot)
-> Ord Annot
Annot -> Annot -> Bool
Annot -> Annot -> Ordering
Annot -> Annot -> Annot
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
$ccompare :: Annot -> Annot -> Ordering
compare :: Annot -> Annot -> Ordering
$c< :: Annot -> Annot -> Bool
< :: Annot -> Annot -> Bool
$c<= :: Annot -> Annot -> Bool
<= :: Annot -> Annot -> Bool
$c> :: Annot -> Annot -> Bool
> :: Annot -> Annot -> Bool
$c>= :: Annot -> Annot -> Bool
>= :: Annot -> Annot -> Bool
$cmax :: Annot -> Annot -> Annot
max :: Annot -> Annot -> Annot
$cmin :: Annot -> Annot -> Annot
min :: Annot -> Annot -> Annot
Ord,Int -> Annot -> String -> String
[Annot] -> String -> String
Annot -> String
(Int -> Annot -> String -> String)
-> (Annot -> String) -> ([Annot] -> String -> String) -> Show Annot
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Annot -> String -> String
showsPrec :: Int -> Annot -> String -> String
$cshow :: Annot -> String
show :: Annot -> String
$cshowList :: [Annot] -> String -> String
showList :: [Annot] -> String -> String
Show,Typeable Annot
Typeable Annot
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annot -> c Annot)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annot)
-> (Annot -> Constr)
-> (Annot -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annot))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annot))
-> ((forall b. Data b => b -> b) -> Annot -> Annot)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r)
-> (forall u. (forall d. Data d => d -> u) -> Annot -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Annot -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot)
-> Data Annot
Annot -> Constr
Annot -> DataType
(forall b. Data b => b -> b) -> Annot -> Annot
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) -> Annot -> u
forall u. (forall d. Data d => d -> u) -> Annot -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annot
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annot -> c Annot
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annot)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annot)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annot -> c Annot
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annot -> c Annot
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annot
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annot
$ctoConstr :: Annot -> Constr
toConstr :: Annot -> Constr
$cdataTypeOf :: Annot -> DataType
dataTypeOf :: Annot -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annot)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annot)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annot)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annot)
$cgmapT :: (forall b. Data b => b -> b) -> Annot -> Annot
gmapT :: (forall b. Data b => b -> b) -> Annot -> Annot
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Annot -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Annot -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Annot -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Annot -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annot -> m Annot
Data,Typeable)
data FunDecl = FunDecl { FunDecl -> Sort
funName :: Ident
, FunDecl -> [Sort]
funArgs :: [Sort]
, FunDecl -> Sort
funRes :: Sort
, FunDecl -> [Annot]
funAnnots :: [Annot]
}
deriving (Typeable FunDecl
Typeable FunDecl
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDecl -> c FunDecl)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDecl)
-> (FunDecl -> Constr)
-> (FunDecl -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunDecl))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl))
-> ((forall b. Data b => b -> b) -> FunDecl -> FunDecl)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r)
-> (forall u. (forall d. Data d => d -> u) -> FunDecl -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> FunDecl -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl)
-> Data FunDecl
FunDecl -> Constr
FunDecl -> DataType
(forall b. Data b => b -> b) -> FunDecl -> FunDecl
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) -> FunDecl -> u
forall u. (forall d. Data d => d -> u) -> FunDecl -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDecl
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDecl -> c FunDecl
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunDecl)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDecl -> c FunDecl
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDecl -> c FunDecl
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDecl
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDecl
$ctoConstr :: FunDecl -> Constr
toConstr :: FunDecl -> Constr
$cdataTypeOf :: FunDecl -> DataType
dataTypeOf :: FunDecl -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunDecl)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunDecl)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl)
$cgmapT :: (forall b. Data b => b -> b) -> FunDecl -> FunDecl
gmapT :: (forall b. Data b => b -> b) -> FunDecl -> FunDecl
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FunDecl -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> FunDecl -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FunDecl -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FunDecl -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
Data,Typeable)
data PredDecl = PredDecl { PredDecl -> Sort
predName :: Ident
, PredDecl -> [Sort]
predArgs :: [Sort]
, PredDecl -> [Annot]
predAnnots :: [Annot]
}
deriving (Typeable PredDecl
Typeable PredDecl
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredDecl -> c PredDecl)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredDecl)
-> (PredDecl -> Constr)
-> (PredDecl -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PredDecl))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl))
-> ((forall b. Data b => b -> b) -> PredDecl -> PredDecl)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r)
-> (forall u. (forall d. Data d => d -> u) -> PredDecl -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PredDecl -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl)
-> Data PredDecl
PredDecl -> Constr
PredDecl -> DataType
(forall b. Data b => b -> b) -> PredDecl -> PredDecl
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) -> PredDecl -> u
forall u. (forall d. Data d => d -> u) -> PredDecl -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredDecl
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredDecl -> c PredDecl
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PredDecl)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredDecl -> c PredDecl
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredDecl -> c PredDecl
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredDecl
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredDecl
$ctoConstr :: PredDecl -> Constr
toConstr :: PredDecl -> Constr
$cdataTypeOf :: PredDecl -> DataType
dataTypeOf :: PredDecl -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PredDecl)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PredDecl)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl)
$cgmapT :: (forall b. Data b => b -> b) -> PredDecl -> PredDecl
gmapT :: (forall b. Data b => b -> b) -> PredDecl -> PredDecl
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PredDecl -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> PredDecl -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PredDecl -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PredDecl -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
Data,Typeable)
data Status = Sat | Unsat | Unknown
deriving (Typeable Status
Typeable Status
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Status -> c Status)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Status)
-> (Status -> Constr)
-> (Status -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Status))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status))
-> ((forall b. Data b => b -> b) -> Status -> Status)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Status -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Status -> r)
-> (forall u. (forall d. Data d => d -> u) -> Status -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Status -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Status -> m Status)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status)
-> Data Status
Status -> Constr
Status -> DataType
(forall b. Data b => b -> b) -> Status -> Status
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) -> Status -> u
forall u. (forall d. Data d => d -> u) -> Status -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Status -> m Status
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Status
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Status -> c Status
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Status)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Status -> c Status
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Status -> c Status
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Status
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Status
$ctoConstr :: Status -> Constr
toConstr :: Status -> Constr
$cdataTypeOf :: Status -> DataType
dataTypeOf :: Status -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Status)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Status)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status)
$cgmapT :: (forall b. Data b => b -> b) -> Status -> Status
gmapT :: (forall b. Data b => b -> b) -> Status -> Status
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Status -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Status -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Status -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Status -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Status -> m Status
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Status -> m Status
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status
Data,Typeable)
data Command
= CmdLogic Ident
| CmdAssumption Formula
| CmdFormula Formula
| CmdStatus Status
| [ Sort ]
| [ FunDecl ]
| [ PredDecl ]
| CmdNotes String
| CmdAnnot Annot
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 -> Constr
Command -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Command -> c Command
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Command -> c Command
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Command
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Command
$ctoConstr :: Command -> Constr
toConstr :: Command -> Constr
$cdataTypeOf :: Command -> DataType
dataTypeOf :: Command -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Command)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Command)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command)
$cgmapT :: (forall b. Data b => b -> b) -> Command -> Command
gmapT :: (forall b. Data b => b -> b) -> Command -> Command
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Command -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Command -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Command -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Command -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
Data,Typeable)
data Script = Script { Script -> Sort
scrName :: Ident, Script -> [Command]
scrCommands :: [Command] }
instance IsString Name where fromString :: String -> Name
fromString String
x = String -> Name
N String
x
instance IsString Ident where fromString :: String -> Sort
fromString String
x = Name -> [Integer] -> Sort
I (String -> Name
forall a. IsString a => String -> a
fromString String
x) []
instance IsString Term where fromString :: String -> Term
fromString String
x = Literal -> Term
Lit (String -> Literal
LitStr String
x)
instance Num Term where
fromInteger :: Integer -> Term
fromInteger = Literal -> Term
Lit (Literal -> Term) -> (Integer -> Literal) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
LitNum
Term
x + :: Term -> Term -> Term
+ Term
y = Sort -> [Term] -> Term
App Sort
"+" [Term
x,Term
y]
Term
x - :: Term -> Term -> Term
- Term
y = Sort -> [Term] -> Term
App Sort
"-" [Term
x,Term
y]
Term
x * :: Term -> Term -> Term
* Term
y = Sort -> [Term] -> Term
App Sort
"*" [Term
x,Term
y]
signum :: Term -> Term
signum Term
x = Sort -> [Term] -> Term
App Sort
"signum" [Term
x]
abs :: Term -> Term
abs Term
x = Sort -> [Term] -> Term
App Sort
"abs" [Term
x]
instance Fractional Term where
fromRational :: Rational -> Term
fromRational = Literal -> Term
Lit (Literal -> Term) -> (Rational -> Literal) -> Rational -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Literal
LitFrac (Rational -> Literal)
-> (Rational -> Rational) -> Rational -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Fractional a => Rational -> a
fromRational
Term
x / :: Term -> Term -> Term
/ Term
y = Sort -> [Term] -> Term
App Sort
"/" [Term
x,Term
y]
(===) :: Term -> Term -> Formula
Term
x === :: Term -> Term -> Formula
=== Term
y = Sort -> [Term] -> Formula
FPred Sort
"=" [Term
x,Term
y]
(=/=) :: Term -> Term -> Formula
Term
x =/= :: Term -> Term -> Formula
=/= Term
y = Sort -> [Term] -> Formula
FPred Sort
"distinct" [Term
x,Term
y]
(.<.) :: Term -> Term -> Formula
Term
x .<. :: Term -> Term -> Formula
.<. Term
y = Sort -> [Term] -> Formula
FPred Sort
"<" [Term
x,Term
y]
(.>.) :: Term -> Term -> Formula
Term
x .>. :: Term -> Term -> Formula
.>. Term
y = Sort -> [Term] -> Formula
FPred Sort
">" [Term
x,Term
y]
tInt :: Sort
tInt :: Sort
tInt = Sort
"Int"
funDef :: Ident -> [Sort] -> Sort -> Command
funDef :: Sort -> [Sort] -> Sort -> Command
funDef Sort
x [Sort]
as Sort
b = [FunDecl] -> Command
CmdExtraFuns [ FunDecl { funName :: Sort
funName = Sort
x
, funArgs :: [Sort]
funArgs = [Sort]
as
, funRes :: Sort
funRes = Sort
b
, funAnnots :: [Annot]
funAnnots = []
} ]
constDef :: Ident -> Sort -> Command
constDef :: Sort -> Sort -> Command
constDef Sort
x Sort
t = Sort -> [Sort] -> Sort -> Command
funDef Sort
x [] Sort
t
logic :: Ident -> Command
logic :: Sort -> Command
logic = Sort -> Command
CmdLogic
assume :: Formula -> Command
assume :: Formula -> Command
assume = Formula -> Command
CmdAssumption
goal :: Formula -> Command
goal :: Formula -> Command
goal = Formula -> Command
CmdFormula