    -- This file is based on:
    --
    -- "The SMT-LIB Standard, Version 1.2"
    -- by Silvio Ranise and Cesare Tinelli
    -- Release: 5 August 2006
    -- Appendix A
    --
    -- URL:
    -- http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.05.pdf

    {-# 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
      | CmdExtraSorts [ Sort ]
      | CmdExtraFuns  [ FunDecl ]
      | CmdExtraPreds [ 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)

    -- aka "benchmark"
    data Script = Script { Script -> Sort
    scrName :: Ident, Script -> [Command]
    scrCommands :: [Command] }

    --------------------------------------------------------------------------------
    -- To make it a bit simpler to write terms in the above AST
    -- we provide some instances.  They are intended to be used only
    -- for writing simple literals, and not any of the computational
    -- operations associated with the classes.

    -- Strings
    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)

    -- Integral operations
    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]

    -- Fractional numbers
    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]

    --------------------------------------------------------------------------------
    -- XXX: move to a separate module?

    (===) :: 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]

    -- | For 'Int'
    (.<.) :: Term -> Term -> Formula
    Term
    x .<. :: Term -> Term -> Formula
    .<. Term
    y   = Sort -> [Term] -> Formula
    FPred Sort
    "<" [Term
    x,Term
    y]

    -- | For 'Int'
    (.>.) :: 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