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

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

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

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

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

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

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

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

type Sort     = Ident

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

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

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

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

data FunDecl  = FunDecl { FunDecl -> Sort
funName   :: Ident
                        , FunDecl -> [Sort]
funArgs   :: [Sort]
                        , FunDecl -> Sort
funRes    :: Sort
                        , FunDecl -> [Annot]
funAnnots :: [Annot]
                        }
  deriving (Typeable FunDecl
Typeable FunDecl
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> FunDecl -> c FunDecl)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FunDecl)
-> (FunDecl -> Constr)
-> (FunDecl -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FunDecl))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl))
-> ((forall b. Data b => b -> b) -> FunDecl -> FunDecl)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FunDecl -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FunDecl -> r)
-> (forall u. (forall d. Data d => d -> u) -> FunDecl -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> FunDecl -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl)
-> Data FunDecl
FunDecl -> Constr
FunDecl -> DataType
(forall b. Data b => b -> b) -> FunDecl -> FunDecl
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> FunDecl -> u
forall u. (forall d. Data d => d -> u) -> FunDecl -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDecl
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDecl -> c FunDecl
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunDecl)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDecl -> c FunDecl
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDecl -> c FunDecl
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDecl
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDecl
$ctoConstr :: FunDecl -> Constr
toConstr :: FunDecl -> Constr
$cdataTypeOf :: FunDecl -> DataType
dataTypeOf :: FunDecl -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunDecl)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunDecl)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl)
$cgmapT :: (forall b. Data b => b -> b) -> FunDecl -> FunDecl
gmapT :: (forall b. Data b => b -> b) -> FunDecl -> FunDecl
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FunDecl -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FunDecl -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> FunDecl -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FunDecl -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FunDecl -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDecl -> m FunDecl
Data,Typeable)

data PredDecl = PredDecl { PredDecl -> Sort
predName   :: Ident
                         , PredDecl -> [Sort]
predArgs   :: [Sort]
                         , PredDecl -> [Annot]
predAnnots :: [Annot]
                         }
  deriving (Typeable PredDecl
Typeable PredDecl
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> PredDecl -> c PredDecl)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PredDecl)
-> (PredDecl -> Constr)
-> (PredDecl -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PredDecl))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl))
-> ((forall b. Data b => b -> b) -> PredDecl -> PredDecl)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PredDecl -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PredDecl -> r)
-> (forall u. (forall d. Data d => d -> u) -> PredDecl -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PredDecl -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl)
-> Data PredDecl
PredDecl -> Constr
PredDecl -> DataType
(forall b. Data b => b -> b) -> PredDecl -> PredDecl
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PredDecl -> u
forall u. (forall d. Data d => d -> u) -> PredDecl -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredDecl
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredDecl -> c PredDecl
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PredDecl)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredDecl -> c PredDecl
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PredDecl -> c PredDecl
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredDecl
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PredDecl
$ctoConstr :: PredDecl -> Constr
toConstr :: PredDecl -> Constr
$cdataTypeOf :: PredDecl -> DataType
dataTypeOf :: PredDecl -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PredDecl)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PredDecl)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl)
$cgmapT :: (forall b. Data b => b -> b) -> PredDecl -> PredDecl
gmapT :: (forall b. Data b => b -> b) -> PredDecl -> PredDecl
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PredDecl -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PredDecl -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> PredDecl -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PredDecl -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PredDecl -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PredDecl -> m PredDecl
Data,Typeable)

data Status   = Sat | Unsat | Unknown
  deriving (Typeable Status
Typeable Status
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Status -> c Status)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Status)
-> (Status -> Constr)
-> (Status -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Status))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status))
-> ((forall b. Data b => b -> b) -> Status -> Status)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Status -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Status -> r)
-> (forall u. (forall d. Data d => d -> u) -> Status -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Status -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Status -> m Status)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Status -> m Status)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Status -> m Status)
-> Data Status
Status -> Constr
Status -> DataType
(forall b. Data b => b -> b) -> Status -> Status
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Status -> u
forall u. (forall d. Data d => d -> u) -> Status -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Status -> m Status
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Status
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Status -> c Status
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Status)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Status -> c Status
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Status -> c Status
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Status
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Status
$ctoConstr :: Status -> Constr
toConstr :: Status -> Constr
$cdataTypeOf :: Status -> DataType
dataTypeOf :: Status -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Status)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Status)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status)
$cgmapT :: (forall b. Data b => b -> b) -> Status -> Status
gmapT :: (forall b. Data b => b -> b) -> Status -> Status
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Status -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Status -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Status -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Status -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Status -> m Status
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Status -> m Status
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Status -> m Status
Data,Typeable)

data Command
  = CmdLogic Ident
  | CmdAssumption Formula
  | CmdFormula Formula
  | CmdStatus Status
  | CmdExtraSorts [ Sort ]
  | CmdExtraFuns  [ FunDecl ]
  | CmdExtraPreds [ PredDecl ]
  | CmdNotes String
  | CmdAnnot Annot
  deriving (Typeable Command
Typeable Command
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Command -> c Command)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Command)
-> (Command -> Constr)
-> (Command -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Command))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command))
-> ((forall b. Data b => b -> b) -> Command -> Command)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Command -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Command -> r)
-> (forall u. (forall d. Data d => d -> u) -> Command -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Command -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Command -> m Command)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Command -> m Command)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Command -> m Command)
-> Data Command
Command -> Constr
Command -> DataType
(forall b. Data b => b -> b) -> Command -> Command
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Command -> u
forall u. (forall d. Data d => d -> u) -> Command -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Command -> m Command
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Command
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Command -> c Command
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Command)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Command -> c Command
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Command -> c Command
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Command
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Command
$ctoConstr :: Command -> Constr
toConstr :: Command -> Constr
$cdataTypeOf :: Command -> DataType
dataTypeOf :: Command -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Command)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Command)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command)
$cgmapT :: (forall b. Data b => b -> b) -> Command -> Command
gmapT :: (forall b. Data b => b -> b) -> Command -> Command
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Command -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Command -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Command -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Command -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Command -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Command -> m Command
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Command -> m Command
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Command -> m Command
Data,Typeable)

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


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

-- Strings
instance IsString Name      where fromString :: String -> Name
fromString String
x = String -> Name
N String
x
instance IsString Ident     where fromString :: String -> Sort
fromString String
x = Name -> [Integer] -> Sort
I (String -> Name
forall a. IsString a => String -> a
fromString String
x) []
instance IsString Term      where fromString :: String -> Term
fromString String
x = Literal -> Term
Lit (String -> Literal
LitStr String
x)

-- Integral operations
instance Num Term where
  fromInteger :: Integer -> Term
fromInteger = Literal -> Term
Lit (Literal -> Term) -> (Integer -> Literal) -> Integer -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
LitNum
  Term
x + :: Term -> Term -> Term
+ Term
y       = Sort -> [Term] -> Term
App Sort
"+" [Term
x,Term
y]
  Term
x - :: Term -> Term -> Term
- Term
y       = Sort -> [Term] -> Term
App Sort
"-" [Term
x,Term
y]
  Term
x * :: Term -> Term -> Term
* Term
y       = Sort -> [Term] -> Term
App Sort
"*" [Term
x,Term
y]
  signum :: Term -> Term
signum Term
x    = Sort -> [Term] -> Term
App Sort
"signum" [Term
x]
  abs :: Term -> Term
abs Term
x       = Sort -> [Term] -> Term
App Sort
"abs" [Term
x]

-- Fractional numbers
instance Fractional Term where
  fromRational :: Rational -> Term
fromRational  = Literal -> Term
Lit (Literal -> Term) -> (Rational -> Literal) -> Rational -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Literal
LitFrac (Rational -> Literal)
-> (Rational -> Rational) -> Rational -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Fractional a => Rational -> a
fromRational
  Term
x / :: Term -> Term -> Term
/ Term
y         = Sort -> [Term] -> Term
App Sort
"/" [Term
x,Term
y]

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

(===) :: Term -> Term -> Formula
Term
x === :: Term -> Term -> Formula
=== Term
y   = Sort -> [Term] -> Formula
FPred Sort
"=" [Term
x,Term
y]

(=/=) :: Term -> Term -> Formula
Term
x =/= :: Term -> Term -> Formula
=/= Term
y   = Sort -> [Term] -> Formula
FPred Sort
"distinct" [Term
x,Term
y]

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

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

tInt :: Sort
tInt :: Sort
tInt = Sort
"Int"

funDef :: Ident -> [Sort] -> Sort -> Command
funDef :: Sort -> [Sort] -> Sort -> Command
funDef Sort
x [Sort]
as Sort
b = [FunDecl] -> Command
CmdExtraFuns [ FunDecl { funName :: Sort
funName = Sort
x
                                       , funArgs :: [Sort]
funArgs = [Sort]
as
                                       , funRes :: Sort
funRes = Sort
b
                                       , funAnnots :: [Annot]
funAnnots = []
                                       } ]

constDef :: Ident -> Sort -> Command
constDef :: Sort -> Sort -> Command
constDef Sort
x Sort
t = Sort -> [Sort] -> Sort -> Command
funDef Sort
x [] Sort
t


logic :: Ident -> Command
logic :: Sort -> Command
logic = Sort -> Command
CmdLogic

assume :: Formula -> Command
assume :: Formula -> Command
assume = Formula -> Command
CmdAssumption

goal :: Formula -> Command
goal :: Formula -> Command
goal = Formula -> Command
CmdFormula