    -- This file is based on:
    --
    -- "The SMT-LIB Standard, Version 2.0"
    -- by Clark Barrett Aaron Stump Cesare Tinelli
    -- Release: December 21, 2010
    -- Appendix C
    --
    -- URL:
    -- http://goedel.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10.12.21.pdf

    {-# LANGUAGE OverloadedStrings, Safe, DeriveDataTypeable #-}
    module SMTLib2.AST where

    import Data.Typeable
    import Data.Data
    import Data.String(IsString(..))

    newtype Name  = N String
                    deriving (Name -> Name -> Bool
    (Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Name -> Name -> Bool
    $c/= :: Name -> Name -> Bool
    == :: Name -> Name -> Bool
    $c== :: Name -> Name -> Bool
    Eq,Eq Name
    Eq Name =>
    (Name -> Name -> Ordering)
    -> (Name -> Name -> Bool)
    -> (Name -> Name -> Bool)
    -> (Name -> Name -> Bool)
    -> (Name -> Name -> Bool)
    -> (Name -> Name -> Name)
    -> (Name -> Name -> Name)
    -> Ord Name
    Name -> Name -> Bool
    Name -> Name -> Ordering
    Name -> Name -> Name
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Name -> Name -> Name
    $cmin :: Name -> Name -> Name
    max :: Name -> Name -> Name
    $cmax :: Name -> Name -> Name
    >= :: Name -> Name -> Bool
    $c>= :: Name -> Name -> Bool
    > :: Name -> Name -> Bool
    $c> :: Name -> Name -> Bool
    <= :: Name -> Name -> Bool
    $c<= :: Name -> Name -> Bool
    < :: Name -> Name -> Bool
    $c< :: Name -> Name -> Bool
    compare :: Name -> Name -> Ordering
    $ccompare :: Name -> Name -> Ordering
    $cp1Ord :: Eq Name
    Ord,Int -> Name -> ShowS
    [Name] -> ShowS
    Name -> String
    (Int -> Name -> ShowS)
    -> (Name -> String) -> ([Name] -> ShowS) -> Show Name
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Name] -> ShowS
    $cshowList :: [Name] -> ShowS
    show :: Name -> String
    $cshow :: Name -> String
    showsPrec :: Int -> Name -> ShowS
    $cshowsPrec :: Int -> Name -> ShowS
    Show,Typeable Name
    Constr
    DataType
    Typeable Name =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Name -> c Name)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Name)
    -> (Name -> Constr)
    -> (Name -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Name))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name))
    -> ((forall b. Data b => b -> b) -> Name -> Name)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Name -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Name -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Name -> m Name)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Name -> m Name)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Name -> m Name)
    -> Data Name
    Name -> Constr
    Name -> DataType
    (forall b. Data b => b -> b) -> Name -> Name
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Name -> c Name
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Name
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Name -> u
    forall u. (forall d. Data d => d -> u) -> Name -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Name -> m Name
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Name -> m Name
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Name
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Name -> c Name
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Name)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
    $cN :: Constr
    $tName :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Name -> m Name
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Name -> m Name
    gmapMp :: (forall d. Data d => d -> m d) -> Name -> m Name
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Name -> m Name
    gmapM :: (forall d. Data d => d -> m d) -> Name -> m Name
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Name -> m Name
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Name -> u
    gmapQ :: (forall d. Data d => d -> u) -> Name -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Name -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
    gmapT :: (forall b. Data b => b -> b) -> Name -> Name
    $cgmapT :: (forall b. Data b => b -> b) -> Name -> Name
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Name)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Name)
    dataTypeOf :: Name -> DataType
    $cdataTypeOf :: Name -> DataType
    toConstr :: Name -> Constr
    $ctoConstr :: Name -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Name
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Name
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Name -> c Name
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Name -> c Name
    $cp1Data :: Typeable Name
    Data,Typeable)

    data Ident    = I Name [Integer]
                    deriving (Ident -> Ident -> Bool
    (Ident -> Ident -> Bool) -> (Ident -> Ident -> Bool) -> Eq Ident
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Ident -> Ident -> Bool
    $c/= :: Ident -> Ident -> Bool
    == :: Ident -> Ident -> Bool
    $c== :: Ident -> Ident -> Bool
    Eq,Eq Ident
    Eq Ident =>
    (Ident -> Ident -> Ordering)
    -> (Ident -> Ident -> Bool)
    -> (Ident -> Ident -> Bool)
    -> (Ident -> Ident -> Bool)
    -> (Ident -> Ident -> Bool)
    -> (Ident -> Ident -> Ident)
    -> (Ident -> Ident -> Ident)
    -> Ord Ident
    Ident -> Ident -> Bool
    Ident -> Ident -> Ordering
    Ident -> Ident -> Ident
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Ident -> Ident -> Ident
    $cmin :: Ident -> Ident -> Ident
    max :: Ident -> Ident -> Ident
    $cmax :: Ident -> Ident -> Ident
    >= :: Ident -> Ident -> Bool
    $c>= :: Ident -> Ident -> Bool
    > :: Ident -> Ident -> Bool
    $c> :: Ident -> Ident -> Bool
    <= :: Ident -> Ident -> Bool
    $c<= :: Ident -> Ident -> Bool
    < :: Ident -> Ident -> Bool
    $c< :: Ident -> Ident -> Bool
    compare :: Ident -> Ident -> Ordering
    $ccompare :: Ident -> Ident -> Ordering
    $cp1Ord :: Eq Ident
    Ord,Int -> Ident -> ShowS
    [Ident] -> ShowS
    Ident -> String
    (Int -> Ident -> ShowS)
    -> (Ident -> String) -> ([Ident] -> ShowS) -> Show Ident
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Ident] -> ShowS
    $cshowList :: [Ident] -> ShowS
    show :: Ident -> String
    $cshow :: Ident -> String
    showsPrec :: Int -> Ident -> ShowS
    $cshowsPrec :: Int -> Ident -> ShowS
    Show,Typeable Ident
    Constr
    DataType
    Typeable Ident =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Ident -> c Ident)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Ident)
    -> (Ident -> Constr)
    -> (Ident -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Ident))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident))
    -> ((forall b. Data b => b -> b) -> Ident -> Ident)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Ident -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Ident -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Ident -> m Ident)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Ident -> m Ident)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Ident -> m Ident)
    -> Data Ident
    Ident -> Constr
    Ident -> DataType
    (forall b. Data b => b -> b) -> Ident -> Ident
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Ident -> c Ident
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Ident
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Ident -> u
    forall u. (forall d. Data d => d -> u) -> Ident -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Ident -> m Ident
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ident -> m Ident
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Ident
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Ident -> c Ident
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Ident)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident)
    $cI :: Constr
    $tIdent :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Ident -> m Ident
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ident -> m Ident
    gmapMp :: (forall d. Data d => d -> m d) -> Ident -> m Ident
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ident -> m Ident
    gmapM :: (forall d. Data d => d -> m d) -> Ident -> m Ident
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Ident -> m Ident
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Ident -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ident -> u
    gmapQ :: (forall d. Data d => d -> u) -> Ident -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Ident -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r
    gmapT :: (forall b. Data b => b -> b) -> Ident -> Ident
    $cgmapT :: (forall b. Data b => b -> b) -> Ident -> Ident
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Ident)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Ident)
    dataTypeOf :: Ident -> DataType
    $cdataTypeOf :: Ident -> DataType
    toConstr :: Ident -> Constr
    $ctoConstr :: Ident -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Ident
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Ident
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Ident -> c Ident
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Ident -> c Ident
    $cp1Data :: Typeable Ident
    Data,Typeable)

    data Quant    = Exists | Forall
                    deriving (Quant -> Quant -> Bool
    (Quant -> Quant -> Bool) -> (Quant -> Quant -> Bool) -> Eq Quant
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Quant -> Quant -> Bool
    $c/= :: Quant -> Quant -> Bool
    == :: Quant -> Quant -> Bool
    $c== :: Quant -> Quant -> Bool
    Eq,Eq Quant
    Eq Quant =>
    (Quant -> Quant -> Ordering)
    -> (Quant -> Quant -> Bool)
    -> (Quant -> Quant -> Bool)
    -> (Quant -> Quant -> Bool)
    -> (Quant -> Quant -> Bool)
    -> (Quant -> Quant -> Quant)
    -> (Quant -> Quant -> Quant)
    -> Ord Quant
    Quant -> Quant -> Bool
    Quant -> Quant -> Ordering
    Quant -> Quant -> Quant
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Quant -> Quant -> Quant
    $cmin :: Quant -> Quant -> Quant
    max :: Quant -> Quant -> Quant
    $cmax :: Quant -> Quant -> Quant
    >= :: Quant -> Quant -> Bool
    $c>= :: Quant -> Quant -> Bool
    > :: Quant -> Quant -> Bool
    $c> :: Quant -> Quant -> Bool
    <= :: Quant -> Quant -> Bool
    $c<= :: Quant -> Quant -> Bool
    < :: Quant -> Quant -> Bool
    $c< :: Quant -> Quant -> Bool
    compare :: Quant -> Quant -> Ordering
    $ccompare :: Quant -> Quant -> Ordering
    $cp1Ord :: Eq Quant
    Ord,Int -> Quant -> ShowS
    [Quant] -> ShowS
    Quant -> String
    (Int -> Quant -> ShowS)
    -> (Quant -> String) -> ([Quant] -> ShowS) -> Show Quant
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Quant] -> ShowS
    $cshowList :: [Quant] -> ShowS
    show :: Quant -> String
    $cshow :: Quant -> String
    showsPrec :: Int -> Quant -> ShowS
    $cshowsPrec :: Int -> Quant -> ShowS
    Show,Typeable Quant
    Constr
    DataType
    Typeable Quant =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Quant -> c Quant)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Quant)
    -> (Quant -> Constr)
    -> (Quant -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Quant))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant))
    -> ((forall b. Data b => b -> b) -> Quant -> Quant)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Quant -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Quant -> m Quant)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Quant -> m Quant)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Quant -> m Quant)
    -> Data Quant
    Quant -> Constr
    Quant -> DataType
    (forall b. Data b => b -> b) -> Quant -> Quant
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Quant -> c Quant
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Quant
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
    forall u. (forall d. Data d => d -> u) -> Quant -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Quant -> m Quant
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Quant -> m Quant
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Quant
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Quant -> c Quant
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Quant)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
    $cForall :: Constr
    $cExists :: Constr
    $tQuant :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Quant -> m Quant
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Quant -> m Quant
    gmapMp :: (forall d. Data d => d -> m d) -> Quant -> m Quant
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Quant -> m Quant
    gmapM :: (forall d. Data d => d -> m d) -> Quant -> m Quant
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Quant -> m Quant
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Quant -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Quant -> u
    gmapQ :: (forall d. Data d => d -> u) -> Quant -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Quant -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r
    gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant
    $cgmapT :: (forall b. Data b => b -> b) -> Quant -> Quant
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Quant)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Quant)
    dataTypeOf :: Quant -> DataType
    $cdataTypeOf :: Quant -> DataType
    toConstr :: Quant -> Constr
    $ctoConstr :: Quant -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Quant
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Quant
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Quant -> c Quant
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Quant -> c Quant
    $cp1Data :: Typeable Quant
    Data,Typeable)

    data Binder   = Bind { Binder -> Name
    bindVar :: Name, Binder -> Type
    bindType :: Type }
                    deriving (Binder -> Binder -> Bool
    (Binder -> Binder -> Bool)
    -> (Binder -> Binder -> Bool) -> Eq Binder
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Binder -> Binder -> Bool
    $c/= :: Binder -> Binder -> Bool
    == :: Binder -> Binder -> Bool
    $c== :: Binder -> Binder -> Bool
    Eq,Eq Binder
    Eq Binder =>
    (Binder -> Binder -> Ordering)
    -> (Binder -> Binder -> Bool)
    -> (Binder -> Binder -> Bool)
    -> (Binder -> Binder -> Bool)
    -> (Binder -> Binder -> Bool)
    -> (Binder -> Binder -> Binder)
    -> (Binder -> Binder -> Binder)
    -> Ord Binder
    Binder -> Binder -> Bool
    Binder -> Binder -> Ordering
    Binder -> Binder -> Binder
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Binder -> Binder -> Binder
    $cmin :: Binder -> Binder -> Binder
    max :: Binder -> Binder -> Binder
    $cmax :: Binder -> Binder -> Binder
    >= :: Binder -> Binder -> Bool
    $c>= :: Binder -> Binder -> Bool
    > :: Binder -> Binder -> Bool
    $c> :: Binder -> Binder -> Bool
    <= :: Binder -> Binder -> Bool
    $c<= :: Binder -> Binder -> Bool
    < :: Binder -> Binder -> Bool
    $c< :: Binder -> Binder -> Bool
    compare :: Binder -> Binder -> Ordering
    $ccompare :: Binder -> Binder -> Ordering
    $cp1Ord :: Eq Binder
    Ord,Int -> Binder -> ShowS
    [Binder] -> ShowS
    Binder -> String
    (Int -> Binder -> ShowS)
    -> (Binder -> String) -> ([Binder] -> ShowS) -> Show Binder
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Binder] -> ShowS
    $cshowList :: [Binder] -> ShowS
    show :: Binder -> String
    $cshow :: Binder -> String
    showsPrec :: Int -> Binder -> ShowS
    $cshowsPrec :: Int -> Binder -> ShowS
    Show,Typeable Binder
    Constr
    DataType
    Typeable Binder =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Binder -> c Binder)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Binder)
    -> (Binder -> Constr)
    -> (Binder -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Binder))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder))
    -> ((forall b. Data b => b -> b) -> Binder -> Binder)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Binder -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Binder -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Binder -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Binder -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Binder -> m Binder)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Binder -> m Binder)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Binder -> m Binder)
    -> Data Binder
    Binder -> Constr
    Binder -> DataType
    (forall b. Data b => b -> b) -> Binder -> Binder
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Binder -> c Binder
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Binder
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Binder -> u
    forall u. (forall d. Data d => d -> u) -> Binder -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Binder -> m Binder
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Binder -> m Binder
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Binder
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Binder -> c Binder
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Binder)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder)
    $cBind :: Constr
    $tBinder :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Binder -> m Binder
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Binder -> m Binder
    gmapMp :: (forall d. Data d => d -> m d) -> Binder -> m Binder
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Binder -> m Binder
    gmapM :: (forall d. Data d => d -> m d) -> Binder -> m Binder
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Binder -> m Binder
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Binder -> u
    gmapQ :: (forall d. Data d => d -> u) -> Binder -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Binder -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r
    gmapT :: (forall b. Data b => b -> b) -> Binder -> Binder
    $cgmapT :: (forall b. Data b => b -> b) -> Binder -> Binder
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Binder)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Binder)
    dataTypeOf :: Binder -> DataType
    $cdataTypeOf :: Binder -> DataType
    toConstr :: Binder -> Constr
    $ctoConstr :: Binder -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Binder
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Binder
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Binder -> c Binder
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Binder -> c Binder
    $cp1Data :: Typeable Binder
    Data,Typeable)

    data Defn     = Defn { Defn -> Name
    defVar :: Name, Defn -> Expr
    defExpr :: Expr }
                    deriving (Defn -> Defn -> Bool
    (Defn -> Defn -> Bool) -> (Defn -> Defn -> Bool) -> Eq Defn
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Defn -> Defn -> Bool
    $c/= :: Defn -> Defn -> Bool
    == :: Defn -> Defn -> Bool
    $c== :: Defn -> Defn -> Bool
    Eq,Eq Defn
    Eq Defn =>
    (Defn -> Defn -> Ordering)
    -> (Defn -> Defn -> Bool)
    -> (Defn -> Defn -> Bool)
    -> (Defn -> Defn -> Bool)
    -> (Defn -> Defn -> Bool)
    -> (Defn -> Defn -> Defn)
    -> (Defn -> Defn -> Defn)
    -> Ord Defn
    Defn -> Defn -> Bool
    Defn -> Defn -> Ordering
    Defn -> Defn -> Defn
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Defn -> Defn -> Defn
    $cmin :: Defn -> Defn -> Defn
    max :: Defn -> Defn -> Defn
    $cmax :: Defn -> Defn -> Defn
    >= :: Defn -> Defn -> Bool
    $c>= :: Defn -> Defn -> Bool
    > :: Defn -> Defn -> Bool
    $c> :: Defn -> Defn -> Bool
    <= :: Defn -> Defn -> Bool
    $c<= :: Defn -> Defn -> Bool
    < :: Defn -> Defn -> Bool
    $c< :: Defn -> Defn -> Bool
    compare :: Defn -> Defn -> Ordering
    $ccompare :: Defn -> Defn -> Ordering
    $cp1Ord :: Eq Defn
    Ord,Int -> Defn -> ShowS
    [Defn] -> ShowS
    Defn -> String
    (Int -> Defn -> ShowS)
    -> (Defn -> String) -> ([Defn] -> ShowS) -> Show Defn
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Defn] -> ShowS
    $cshowList :: [Defn] -> ShowS
    show :: Defn -> String
    $cshow :: Defn -> String
    showsPrec :: Int -> Defn -> ShowS
    $cshowsPrec :: Int -> Defn -> ShowS
    Show,Typeable Defn
    Constr
    DataType
    Typeable Defn =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Defn -> c Defn)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Defn)
    -> (Defn -> Constr)
    -> (Defn -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Defn))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn))
    -> ((forall b. Data b => b -> b) -> Defn -> Defn)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Defn -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Defn -> m Defn)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Defn -> m Defn)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Defn -> m Defn)
    -> Data Defn
    Defn -> Constr
    Defn -> DataType
    (forall b. Data b => b -> b) -> Defn -> Defn
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Defn -> c Defn
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Defn
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
    forall u. (forall d. Data d => d -> u) -> Defn -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Defn -> m Defn
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Defn -> m Defn
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Defn
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Defn -> c Defn
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Defn)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
    $cDefn :: Constr
    $tDefn :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Defn -> m Defn
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Defn -> m Defn
    gmapMp :: (forall d. Data d => d -> m d) -> Defn -> m Defn
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Defn -> m Defn
    gmapM :: (forall d. Data d => d -> m d) -> Defn -> m Defn
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Defn -> m Defn
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Defn -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
    gmapQ :: (forall d. Data d => d -> u) -> Defn -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Defn -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
    gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn
    $cgmapT :: (forall b. Data b => b -> b) -> Defn -> Defn
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Defn)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Defn)
    dataTypeOf :: Defn -> DataType
    $cdataTypeOf :: Defn -> DataType
    toConstr :: Defn -> Constr
    $ctoConstr :: Defn -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Defn
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Defn
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Defn -> c Defn
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Defn -> c Defn
    $cp1Data :: Typeable Defn
    Data,Typeable)

    data Literal  = LitBV Integer Integer   -- ^ value, width (in bits)
                  | LitNum Integer
                  | LitFrac Rational
                  | LitStr String
                    deriving (Literal -> Literal -> Bool
    (Literal -> Literal -> Bool)
    -> (Literal -> Literal -> Bool) -> Eq Literal
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Literal -> Literal -> Bool
    $c/= :: Literal -> Literal -> Bool
    == :: Literal -> Literal -> Bool
    $c== :: Literal -> Literal -> Bool
    Eq,Eq Literal
    Eq Literal =>
    (Literal -> Literal -> Ordering)
    -> (Literal -> Literal -> Bool)
    -> (Literal -> Literal -> Bool)
    -> (Literal -> Literal -> Bool)
    -> (Literal -> Literal -> Bool)
    -> (Literal -> Literal -> Literal)
    -> (Literal -> Literal -> Literal)
    -> Ord Literal
    Literal -> Literal -> Bool
    Literal -> Literal -> Ordering
    Literal -> Literal -> Literal
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Literal -> Literal -> Literal
    $cmin :: Literal -> Literal -> Literal
    max :: Literal -> Literal -> Literal
    $cmax :: Literal -> Literal -> Literal
    >= :: Literal -> Literal -> Bool
    $c>= :: Literal -> Literal -> Bool
    > :: Literal -> Literal -> Bool
    $c> :: Literal -> Literal -> Bool
    <= :: Literal -> Literal -> Bool
    $c<= :: Literal -> Literal -> Bool
    < :: Literal -> Literal -> Bool
    $c< :: Literal -> Literal -> Bool
    compare :: Literal -> Literal -> Ordering
    $ccompare :: Literal -> Literal -> Ordering
    $cp1Ord :: Eq Literal
    Ord,Int -> Literal -> ShowS
    [Literal] -> ShowS
    Literal -> String
    (Int -> Literal -> ShowS)
    -> (Literal -> String) -> ([Literal] -> ShowS) -> Show Literal
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Literal] -> ShowS
    $cshowList :: [Literal] -> ShowS
    show :: Literal -> String
    $cshow :: Literal -> String
    showsPrec :: Int -> Literal -> ShowS
    $cshowsPrec :: Int -> Literal -> ShowS
    Show,Typeable Literal
    Constr
    DataType
    Typeable Literal =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Literal -> c Literal)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Literal)
    -> (Literal -> Constr)
    -> (Literal -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Literal))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal))
    -> ((forall b. Data b => b -> b) -> Literal -> Literal)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Literal -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Literal -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Literal -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Literal -> m Literal)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Literal -> m Literal)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Literal -> m Literal)
    -> Data Literal
    Literal -> Constr
    Literal -> DataType
    (forall b. Data b => b -> b) -> Literal -> Literal
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Literal -> c Literal
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Literal
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
    forall u. (forall d. Data d => d -> u) -> Literal -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Literal -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Literal -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Literal -> m Literal
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Literal -> m Literal
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Literal
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Literal -> c Literal
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Literal)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
    $cLitStr :: Constr
    $cLitFrac :: Constr
    $cLitNum :: Constr
    $cLitBV :: Constr
    $tLiteral :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Literal -> m Literal
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Literal -> m Literal
    gmapMp :: (forall d. Data d => d -> m d) -> Literal -> m Literal
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Literal -> m Literal
    gmapM :: (forall d. Data d => d -> m d) -> Literal -> m Literal
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Literal -> m Literal
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Literal -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Literal -> u
    gmapQ :: (forall d. Data d => d -> u) -> Literal -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Literal -> [u]
    gmapQr :: (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Literal -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Literal -> r
    gmapQl :: (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Literal -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Literal -> r
    gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal
    $cgmapT :: (forall b. Data b => b -> b) -> Literal -> Literal
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Literal)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Literal)
    dataTypeOf :: Literal -> DataType
    $cdataTypeOf :: Literal -> DataType
    toConstr :: Literal -> Constr
    $ctoConstr :: Literal -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Literal
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Literal
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Literal -> c Literal
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Literal -> c Literal
    $cp1Data :: Typeable Literal
    Data,Typeable)

    data Type     = TApp Ident [Type]
                  | TVar Name
                    deriving (Type -> Type -> Bool
    (Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Type -> Type -> Bool
    $c/= :: Type -> Type -> Bool
    == :: Type -> Type -> Bool
    $c== :: Type -> Type -> Bool
    Eq,Eq Type
    Eq Type =>
    (Type -> Type -> Ordering)
    -> (Type -> Type -> Bool)
    -> (Type -> Type -> Bool)
    -> (Type -> Type -> Bool)
    -> (Type -> Type -> Bool)
    -> (Type -> Type -> Type)
    -> (Type -> Type -> Type)
    -> Ord Type
    Type -> Type -> Bool
    Type -> Type -> Ordering
    Type -> Type -> Type
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Type -> Type -> Type
    $cmin :: Type -> Type -> Type
    max :: Type -> Type -> Type
    $cmax :: Type -> Type -> Type
    >= :: Type -> Type -> Bool
    $c>= :: Type -> Type -> Bool
    > :: Type -> Type -> Bool
    $c> :: Type -> Type -> Bool
    <= :: Type -> Type -> Bool
    $c<= :: Type -> Type -> Bool
    < :: Type -> Type -> Bool
    $c< :: Type -> Type -> Bool
    compare :: Type -> Type -> Ordering
    $ccompare :: Type -> Type -> Ordering
    $cp1Ord :: Eq Type
    Ord,Int -> Type -> ShowS
    [Type] -> ShowS
    Type -> String
    (Int -> Type -> ShowS)
    -> (Type -> String) -> ([Type] -> ShowS) -> Show Type
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Type] -> ShowS
    $cshowList :: [Type] -> ShowS
    show :: Type -> String
    $cshow :: Type -> String
    showsPrec :: Int -> Type -> ShowS
    $cshowsPrec :: Int -> Type -> ShowS
    Show,Typeable Type
    Constr
    DataType
    Typeable Type =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Type -> c Type)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Type)
    -> (Type -> Constr)
    -> (Type -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Type))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type))
    -> ((forall b. Data b => b -> b) -> Type -> Type)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Type -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Type -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Type -> m Type)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Type -> m Type)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Type -> m Type)
    -> Data Type
    Type -> Constr
    Type -> DataType
    (forall b. Data b => b -> b) -> Type -> Type
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Type -> c Type
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Type
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
    forall u. (forall d. Data d => d -> u) -> Type -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Type -> m Type
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Type -> m Type
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Type
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Type -> c Type
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Type)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
    $cTVar :: Constr
    $cTApp :: Constr
    $tType :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Type -> m Type
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Type -> m Type
    gmapMp :: (forall d. Data d => d -> m d) -> Type -> m Type
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Type -> m Type
    gmapM :: (forall d. Data d => d -> m d) -> Type -> m Type
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Type -> m Type
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
    gmapQ :: (forall d. Data d => d -> u) -> Type -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
    gmapT :: (forall b. Data b => b -> b) -> Type -> Type
    $cgmapT :: (forall b. Data b => b -> b) -> Type -> Type
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Type)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Type)
    dataTypeOf :: Type -> DataType
    $cdataTypeOf :: Type -> DataType
    toConstr :: Type -> Constr
    $ctoConstr :: Type -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Type
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Type
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Type -> c Type
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Type -> c Type
    $cp1Data :: Typeable Type
    Data,Typeable)

    data Expr     = Lit Literal
                  | App Ident (Maybe Type) [Expr]
                  | Quant Quant [Binder] Expr
                  | Let [Defn] Expr
                  | Annot Expr [Attr]
                    deriving (Expr -> Expr -> Bool
    (Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Expr -> Expr -> Bool
    $c/= :: Expr -> Expr -> Bool
    == :: Expr -> Expr -> Bool
    $c== :: Expr -> Expr -> Bool
    Eq,Eq Expr
    Eq Expr =>
    (Expr -> Expr -> Ordering)
    -> (Expr -> Expr -> Bool)
    -> (Expr -> Expr -> Bool)
    -> (Expr -> Expr -> Bool)
    -> (Expr -> Expr -> Bool)
    -> (Expr -> Expr -> Expr)
    -> (Expr -> Expr -> Expr)
    -> Ord Expr
    Expr -> Expr -> Bool
    Expr -> Expr -> Ordering
    Expr -> Expr -> Expr
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Expr -> Expr -> Expr
    $cmin :: Expr -> Expr -> Expr
    max :: Expr -> Expr -> Expr
    $cmax :: Expr -> Expr -> Expr
    >= :: Expr -> Expr -> Bool
    $c>= :: Expr -> Expr -> Bool
    > :: Expr -> Expr -> Bool
    $c> :: Expr -> Expr -> Bool
    <= :: Expr -> Expr -> Bool
    $c<= :: Expr -> Expr -> Bool
    < :: Expr -> Expr -> Bool
    $c< :: Expr -> Expr -> Bool
    compare :: Expr -> Expr -> Ordering
    $ccompare :: Expr -> Expr -> Ordering
    $cp1Ord :: Eq Expr
    Ord,Int -> Expr -> ShowS
    [Expr] -> ShowS
    Expr -> String
    (Int -> Expr -> ShowS)
    -> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Expr] -> ShowS
    $cshowList :: [Expr] -> ShowS
    show :: Expr -> String
    $cshow :: Expr -> String
    showsPrec :: Int -> Expr -> ShowS
    $cshowsPrec :: Int -> Expr -> ShowS
    Show,Typeable Expr
    Constr
    DataType
    Typeable Expr =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Expr -> c Expr)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Expr)
    -> (Expr -> Constr)
    -> (Expr -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Expr))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr))
    -> ((forall b. Data b => b -> b) -> Expr -> Expr)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Expr -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Expr -> m Expr)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Expr -> m Expr)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Expr -> m Expr)
    -> Data Expr
    Expr -> Constr
    Expr -> DataType
    (forall b. Data b => b -> b) -> Expr -> Expr
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Expr -> c Expr
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Expr
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u
    forall u. (forall d. Data d => d -> u) -> Expr -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Expr -> m Expr
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Expr -> m Expr
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Expr
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Expr -> c Expr
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Expr)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr)
    $cAnnot :: Constr
    $cLet :: Constr
    $cQuant :: Constr
    $cApp :: Constr
    $cLit :: Constr
    $tExpr :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Expr -> m Expr
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Expr -> m Expr
    gmapMp :: (forall d. Data d => d -> m d) -> Expr -> m Expr
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Expr -> m Expr
    gmapM :: (forall d. Data d => d -> m d) -> Expr -> m Expr
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Expr -> m Expr
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u
    gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Expr -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
    gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr
    $cgmapT :: (forall b. Data b => b -> b) -> Expr -> Expr
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Expr)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Expr)
    dataTypeOf :: Expr -> DataType
    $cdataTypeOf :: Expr -> DataType
    toConstr :: Expr -> Constr
    $ctoConstr :: Expr -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Expr
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Expr
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Expr -> c Expr
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Expr -> c Expr
    $cp1Data :: Typeable Expr
    Data,Typeable)

    data Attr     = Attr { Attr -> Name
    attrName :: Name , Attr -> Maybe Expr
    attrVal :: Maybe AttrVal }
                    deriving (Attr -> Attr -> Bool
    (Attr -> Attr -> Bool) -> (Attr -> Attr -> Bool) -> Eq Attr
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Attr -> Attr -> Bool
    $c/= :: Attr -> Attr -> Bool
    == :: Attr -> Attr -> Bool
    $c== :: Attr -> Attr -> Bool
    Eq,Eq Attr
    Eq Attr =>
    (Attr -> Attr -> Ordering)
    -> (Attr -> Attr -> Bool)
    -> (Attr -> Attr -> Bool)
    -> (Attr -> Attr -> Bool)
    -> (Attr -> Attr -> Bool)
    -> (Attr -> Attr -> Attr)
    -> (Attr -> Attr -> Attr)
    -> Ord Attr
    Attr -> Attr -> Bool
    Attr -> Attr -> Ordering
    Attr -> Attr -> Attr
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Attr -> Attr -> Attr
    $cmin :: Attr -> Attr -> Attr
    max :: Attr -> Attr -> Attr
    $cmax :: Attr -> Attr -> Attr
    >= :: Attr -> Attr -> Bool
    $c>= :: Attr -> Attr -> Bool
    > :: Attr -> Attr -> Bool
    $c> :: Attr -> Attr -> Bool
    <= :: Attr -> Attr -> Bool
    $c<= :: Attr -> Attr -> Bool
    < :: Attr -> Attr -> Bool
    $c< :: Attr -> Attr -> Bool
    compare :: Attr -> Attr -> Ordering
    $ccompare :: Attr -> Attr -> Ordering
    $cp1Ord :: Eq Attr
    Ord,Int -> Attr -> ShowS
    [Attr] -> ShowS
    Attr -> String
    (Int -> Attr -> ShowS)
    -> (Attr -> String) -> ([Attr] -> ShowS) -> Show Attr
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Attr] -> ShowS
    $cshowList :: [Attr] -> ShowS
    show :: Attr -> String
    $cshow :: Attr -> String
    showsPrec :: Int -> Attr -> ShowS
    $cshowsPrec :: Int -> Attr -> ShowS
    Show,Typeable Attr
    Constr
    DataType
    Typeable Attr =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Attr -> c Attr)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Attr)
    -> (Attr -> Constr)
    -> (Attr -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Attr))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr))
    -> ((forall b. Data b => b -> b) -> Attr -> Attr)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Attr -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Attr -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Attr -> m Attr)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Attr -> m Attr)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Attr -> m Attr)
    -> Data Attr
    Attr -> Constr
    Attr -> DataType
    (forall b. Data b => b -> b) -> Attr -> Attr
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Attr -> c Attr
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Attr
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Attr -> u
    forall u. (forall d. Data d => d -> u) -> Attr -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Attr -> m Attr
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Attr -> m Attr
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Attr
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Attr -> c Attr
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Attr)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr)
    $cAttr :: Constr
    $tAttr :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Attr -> m Attr
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Attr -> m Attr
    gmapMp :: (forall d. Data d => d -> m d) -> Attr -> m Attr
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Attr -> m Attr
    gmapM :: (forall d. Data d => d -> m d) -> Attr -> m Attr
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Attr -> m Attr
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Attr -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Attr -> u
    gmapQ :: (forall d. Data d => d -> u) -> Attr -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Attr -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r
    gmapT :: (forall b. Data b => b -> b) -> Attr -> Attr
    $cgmapT :: (forall b. Data b => b -> b) -> Attr -> Attr
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Attr)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Attr)
    dataTypeOf :: Attr -> DataType
    $cdataTypeOf :: Attr -> DataType
    toConstr :: Attr -> Constr
    $ctoConstr :: Attr -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Attr
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Attr
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Attr -> c Attr
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Attr -> c Attr
    $cp1Data :: Typeable Attr
    Data,Typeable)

    type AttrVal  = Expr    -- A bit of an approximation....

    data Option
      = OptPrintSuccess Bool
      | OptExpandDefinitions Bool
      | OptInteractiveMode Bool
      | OptProduceProofs Bool
      | OptProduceUnsatCores Bool
      | OptProduceModels Bool
      | OptProduceAssignments Bool
      | OptRegularOutputChannel String
      | OptDiagnosticOutputChannel String
      | OptRandomSeed Integer
      | OptVerbosity Integer
      | OptAttr Attr
      deriving (Typeable Option
    Constr
    DataType
    Typeable Option =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Option -> c Option)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Option)
    -> (Option -> Constr)
    -> (Option -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Option))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Option))
    -> ((forall b. Data b => b -> b) -> Option -> Option)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Option -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Option -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Option -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Option -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Option -> m Option)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Option -> m Option)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Option -> m Option)
    -> Data Option
    Option -> Constr
    Option -> DataType
    (forall b. Data b => b -> b) -> Option -> Option
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Option -> c Option
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Option
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Option -> u
    forall u. (forall d. Data d => d -> u) -> Option -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Option -> m Option
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Option -> m Option
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Option
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Option -> c Option
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Option)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Option)
    $cOptAttr :: Constr
    $cOptVerbosity :: Constr
    $cOptRandomSeed :: Constr
    $cOptDiagnosticOutputChannel :: Constr
    $cOptRegularOutputChannel :: Constr
    $cOptProduceAssignments :: Constr
    $cOptProduceModels :: Constr
    $cOptProduceUnsatCores :: Constr
    $cOptProduceProofs :: Constr
    $cOptInteractiveMode :: Constr
    $cOptExpandDefinitions :: Constr
    $cOptPrintSuccess :: Constr
    $tOption :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Option -> m Option
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Option -> m Option
    gmapMp :: (forall d. Data d => d -> m d) -> Option -> m Option
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Option -> m Option
    gmapM :: (forall d. Data d => d -> m d) -> Option -> m Option
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Option -> m Option
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Option -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Option -> u
    gmapQ :: (forall d. Data d => d -> u) -> Option -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Option -> [u]
    gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
    gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Option -> r
    gmapT :: (forall b. Data b => b -> b) -> Option -> Option
    $cgmapT :: (forall b. Data b => b -> b) -> Option -> Option
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Option)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Option)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Option)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Option)
    dataTypeOf :: Option -> DataType
    $cdataTypeOf :: Option -> DataType
    toConstr :: Option -> Constr
    $ctoConstr :: Option -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Option
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Option
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Option -> c Option
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Option -> c Option
    $cp1Data :: Typeable Option
    Data,Typeable)

    data InfoFlag
      = InfoAllStatistics
      | InfoErrorBehavior
      | InfoName
      | InfoAuthors
      | InfoVersion
      | InfoStatus
      | InfoReasonUnknown
      | InfoAttr Attr
      deriving (Typeable InfoFlag
    Constr
    DataType
    Typeable InfoFlag =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> InfoFlag -> c InfoFlag)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c InfoFlag)
    -> (InfoFlag -> Constr)
    -> (InfoFlag -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c InfoFlag))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoFlag))
    -> ((forall b. Data b => b -> b) -> InfoFlag -> InfoFlag)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r)
    -> (forall u. (forall d. Data d => d -> u) -> InfoFlag -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> InfoFlag -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag)
    -> Data InfoFlag
    InfoFlag -> Constr
    InfoFlag -> DataType
    (forall b. Data b => b -> b) -> InfoFlag -> InfoFlag
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> InfoFlag -> c InfoFlag
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c InfoFlag
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> InfoFlag -> u
    forall u. (forall d. Data d => d -> u) -> InfoFlag -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c InfoFlag
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> InfoFlag -> c InfoFlag
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c InfoFlag)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoFlag)
    $cInfoAttr :: Constr
    $cInfoReasonUnknown :: Constr
    $cInfoStatus :: Constr
    $cInfoVersion :: Constr
    $cInfoAuthors :: Constr
    $cInfoName :: Constr
    $cInfoErrorBehavior :: Constr
    $cInfoAllStatistics :: Constr
    $tInfoFlag :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
    gmapMp :: (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
    gmapM :: (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> InfoFlag -> m InfoFlag
    gmapQi :: Int -> (forall d. Data d => d -> u) -> InfoFlag -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> InfoFlag -> u
    gmapQ :: (forall d. Data d => d -> u) -> InfoFlag -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> InfoFlag -> [u]
    gmapQr :: (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
    gmapQl :: (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> InfoFlag -> r
    gmapT :: (forall b. Data b => b -> b) -> InfoFlag -> InfoFlag
    $cgmapT :: (forall b. Data b => b -> b) -> InfoFlag -> InfoFlag
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoFlag)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoFlag)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c InfoFlag)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c InfoFlag)
    dataTypeOf :: InfoFlag -> DataType
    $cdataTypeOf :: InfoFlag -> DataType
    toConstr :: InfoFlag -> Constr
    $ctoConstr :: InfoFlag -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c InfoFlag
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c InfoFlag
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> InfoFlag -> c InfoFlag
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> InfoFlag -> c InfoFlag
    $cp1Data :: Typeable InfoFlag
    Data,Typeable)

    data Command
      = CmdSetLogic Name
      | CmdSetOption Option
      | CmdSetInfo Attr
      | CmdDeclareType Name Integer
      | CmdDefineType Name [Name] Type
      | CmdDeclareConst Name Type
      | CmdDeclareFun Name [Type] Type
      | CmdDefineFun Name [Binder] Type Expr
      | CmdPush Integer
      | CmdPop Integer
      | CmdAssert Expr
      | CmdCheckSat
      | CmdGetAssertions
      | CmdGetValue [Expr]
      | CmdGetProof
      | CmdGetUnsatCore
      | CmdGetInfo InfoFlag
      | CmdGetOption Name
      | CmdComment String
      | CmdExit
      deriving (Typeable Command
    Constr
    DataType
    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 d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Command -> c Command
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c 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)
    $cCmdExit :: Constr
    $cCmdComment :: Constr
    $cCmdGetOption :: Constr
    $cCmdGetInfo :: Constr
    $cCmdGetUnsatCore :: Constr
    $cCmdGetProof :: Constr
    $cCmdGetValue :: Constr
    $cCmdGetAssertions :: Constr
    $cCmdCheckSat :: Constr
    $cCmdAssert :: Constr
    $cCmdPop :: Constr
    $cCmdPush :: Constr
    $cCmdDefineFun :: Constr
    $cCmdDeclareFun :: Constr
    $cCmdDeclareConst :: Constr
    $cCmdDefineType :: Constr
    $cCmdDeclareType :: Constr
    $cCmdSetInfo :: Constr
    $cCmdSetOption :: Constr
    $cCmdSetLogic :: Constr
    $tCommand :: DataType
    gmapMo :: (forall d. Data d => d -> m d) -> Command -> m Command
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Command -> m Command
    gmapMp :: (forall d. Data d => d -> m d) -> Command -> m Command
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Command -> m Command
    gmapM :: (forall d. Data d => d -> m d) -> Command -> m Command
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Command -> m Command
    gmapQi :: Int -> (forall d. Data d => d -> u) -> Command -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Command -> u
    gmapQ :: (forall d. Data d => d -> u) -> Command -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Command -> [u]
    gmapQr :: (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Command -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Command -> r
    gmapQl :: (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Command -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Command -> r
    gmapT :: (forall b. Data b => b -> b) -> Command -> Command
    $cgmapT :: (forall b. Data b => b -> b) -> Command -> Command
    dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command)
    dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Command)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Command)
    dataTypeOf :: Command -> DataType
    $cdataTypeOf :: Command -> DataType
    toConstr :: Command -> Constr
    $ctoConstr :: Command -> Constr
    gunfold :: (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Command
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Command
    gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Command -> c Command
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Command -> c Command
    $cp1Data :: Typeable Command
    Data,Typeable)

    newtype Script = Script [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 -> Name
    N
    instance IsString Ident     where fromString :: String -> Ident
    fromString x :: String
    x = Name -> [Integer] -> Ident
    I (String -> Name
    forall a. IsString a => String -> a
    fromString String
    x) []
    instance IsString Type      where fromString :: String -> Type
    fromString x :: String
    x = Ident -> [Type] -> Type
    TApp (String -> Ident
    forall a. IsString a => String -> a
    fromString String
    x) []
    instance IsString Expr      where fromString :: String -> Expr
    fromString   = Literal -> Expr
    Lit (Literal -> Expr) -> (String -> Literal) -> String -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Literal
    LitStr (String -> Literal) -> ShowS -> String -> Literal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ShowS
    forall a. IsString a => String -> a
    fromString

    -- Integers

    -- NOTE: Some of these might not mean anything, depending on the theory.
    instance Num Expr where
      fromInteger :: Integer -> Expr
    fromInteger x :: Integer
    x = Literal -> Expr
    Lit (Integer -> Literal
    LitNum Integer
    x)
      x :: Expr
    x + :: Expr -> Expr -> Expr
    + y :: Expr
    y         = Ident -> [Expr] -> Expr
    app "+"      [Expr
    x,Expr
    y]
      x :: Expr
    x - :: Expr -> Expr -> Expr
    - y :: Expr
    y         = Ident -> [Expr] -> Expr
    app "-"      [Expr
    x,Expr
    y]
      x :: Expr
    x * :: Expr -> Expr -> Expr
    * y :: Expr
    y         = Ident -> [Expr] -> Expr
    app "*"      [Expr
    x,Expr
    y]
      signum :: Expr -> Expr
    signum x :: Expr
    x      = Ident -> [Expr] -> Expr
    app "signum" [Expr
    x]
      abs :: Expr -> Expr
    abs x :: Expr
    x         = Ident -> [Expr] -> Expr
    app "abs"    [Expr
    x]

    -- Fractional numbers
    instance Fractional Expr where
      fromRational :: Rational -> Expr
    fromRational x :: Rational
    x  = Literal -> Expr
    Lit (Rational -> Literal
    LitFrac Rational
    x)
      x :: Expr
    x / :: Expr -> Expr -> Expr
    / y :: Expr
    y           = Ident -> [Expr] -> Expr
    app "/" [Expr
    x,Expr
    y]

    app :: Ident -> [Expr] -> Expr
    app :: Ident -> [Expr] -> Expr
    app f :: Ident
    f es :: [Expr]
    es = Ident -> Maybe Type -> [Expr] -> Expr
    App Ident
    f Maybe Type
    forall a. Maybe a
    Nothing [Expr]
    es