{-# 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, Data, Eq)



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

theoremType :: LanguageSubset -> TheoremType
theoremType l = case l of
  BasicSubset     -> EquationalTheorem
  SubsetWithFix t -> t
  SubsetWithSeq t -> 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, Data, Eq)