{-# LANGUAGE DeriveDataTypeable #-}

-- | Declares the available Haskell language subsets and the result types for
--   generating free theorems. 

module Language.Haskell.FreeTheorems.LanguageSubsets where



import Data.Generics (Typeable, Data)



-- | Descriptions of the Haskell language subsets for which free theorems can
--   be generated.

data LanguageSubset
  = BasicSubset
        -- ^ This subset describes only terms in which no undefinedness may.
        --   This excludes terms defined using general recursion or selective
        --   strictness (as offered by @seq@).

  | SubsetWithFix TheoremType
        -- ^ This subset describes terms in which undefined values may occur
        --   such as introduced by a fixpoint combinator or possibly failing
        --   pattern matches (if not all cases are covered).
        --   This excludes any term based on @seq@.

  | SubsetWithSeq TheoremType
        -- ^ Additionally to the fix subset, this subset allows terms to
        --   be defined using @seq@.

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



-- | Returns the theorem type for a given language subset.

theoremType :: LanguageSubset -> TheoremType
theoremType :: LanguageSubset -> TheoremType
theoremType LanguageSubset
l = case LanguageSubset
l of
  LanguageSubset
BasicSubset     -> TheoremType
EquationalTheorem
  SubsetWithFix TheoremType
t -> TheoremType
t
  SubsetWithSeq TheoremType
t -> TheoremType
t



-- | The result type for generating free theorems.

data TheoremType
  = EquationalTheorem
        -- ^ An equational free theorem should be generated.

  | InequationalTheorem
        -- ^ Two inequational free theorems should be generated.

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