Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Haskell.FreeTheorems.Syntax

Contents

Declarations
Type expressions
Identifiers

Description

Declars data types describing the abstract syntax of a subset of Haskell in the FreeTheorems library. Only declarations and type expressions are covered by these data types.

Note that the data types of this module do not reflect Haskell98. This is because they are able to express higher-rank functions which are not part of Haskell98. Also, in type expressions, a type variable must not be applied to any type expression. Thus, for example, the type m a, as occuring in the functions of the Monad type class, is not expressable. The reason for this restriction is that the FreeTheorems library cannot handle such types.

Synopsis

data Declaration
getDeclarationName :: Declaration -> Identifier
getDeclarationArity :: Declaration -> Maybe Int
data DataDeclaration = Data {
- dataName :: Identifier
- dataVars :: [TypeVariable]
- dataCons :: [DataConstructorDeclaration]
}
data NewtypeDeclaration = Newtype {
- newtypeName :: Identifier
- newtypeVars :: [TypeVariable]
- newtypeCon :: Identifier
- newtypeRhs :: TypeExpression
}
data TypeDeclaration = Type {
- typeName :: Identifier
- typeVars :: [TypeVariable]
- typeRhs :: TypeExpression
}
data ClassDeclaration = Class {
- superClasses :: [TypeClass]
- className :: Identifier
- classVar :: TypeVariable
- classFuns :: [Signature]
}
data Signature = Signature {
- signatureName :: Identifier
- signatureType :: TypeExpression
}
data DataConstructorDeclaration = DataCon {
- dataConName :: Identifier
- dataConTypes :: [BangTypeExpression]
}
data BangTypeExpression
- = Banged {
  - withoutBang :: TypeExpression
  }
- | Unbanged {
  - withoutBang :: TypeExpression
  }
data TypeExpression
data TypeConstructor
- = ConUnit
- | ConList
- | ConTuple Int
- | ConInt
- | ConInteger
- | ConFloat
- | ConDouble
- | ConChar
- | Con Identifier
newtype TypeClass = TC Identifier
newtype TypeVariable = TV Identifier
newtype FixedTypeExpression = TF Identifier
newtype Identifier = Ident {
- unpackIdent :: String
}

Declarations

data Declaration Source #

A Haskell declaration which corresponds to a type, data, newtype, class or type signature declaration.

In type expressions, type variables must not be applied to type expressions. Thus, for example, the functions of the Monad class are not expressible. However, in extension to Haskell98, higher-rank types can be expressed.

This data type does not reflect all information of a declaration. Only the aspects needed by the FreeTheorems library are covered.

Constructors

TypeDecl TypeDeclaration	A `type` declaration.
DataDecl DataDeclaration	A `data` declaration.
NewtypeDecl NewtypeDeclaration	A `newtype` declaration.
ClassDecl ClassDeclaration	A `class` declaration.
TypeSig Signature	A type signature.

Instances

Instances details

Data Declaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Declaration -> c Declaration # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Declaration # toConstr :: Declaration -> Constr # dataTypeOf :: Declaration -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Declaration) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Declaration) # gmapT :: (forall b. Data b => b -> b) -> Declaration -> Declaration # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r # gmapQ :: (forall d. Data d => d -> u) -> Declaration -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Declaration -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration #
Show Declaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> Declaration -> ShowS # show :: Declaration -> String # showList :: [Declaration] -> ShowS #
Eq Declaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: Declaration -> Declaration -> Bool # (/=) :: Declaration -> Declaration -> Bool #

getDeclarationName :: Declaration -> Identifier Source #

Gets the name of the item declared by a declaration. This is the type constructor for data, newtype and type declarations, the name of a class for a class declaration or the name of a type signature.

getDeclarationArity :: Declaration -> Maybe Int Source #

Gets the arity of a type constructor or Nothing if this is not a data, newtype or type declaration.

data DataDeclaration Source #

A data declaration for an algebraic data type.

Note that the context and the deriving parts of a data declaration are ignored.

Constructors

Data
Fields dataName :: Identifier The name of the type constructor. dataVars :: [TypeVariable] The type variables on the left-hand side. dataCons :: [DataConstructorDeclaration] The declarations of the data constructors on the right-hand side.

Instances

Instances details

Data DataDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataDeclaration -> c DataDeclaration # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataDeclaration # toConstr :: DataDeclaration -> Constr # dataTypeOf :: DataDeclaration -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataDeclaration) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDeclaration) # gmapT :: (forall b. Data b => b -> b) -> DataDeclaration -> DataDeclaration # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataDeclaration -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDeclaration -> r # gmapQ :: (forall d. Data d => d -> u) -> DataDeclaration -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DataDeclaration -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataDeclaration -> m DataDeclaration # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDeclaration -> m DataDeclaration # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDeclaration -> m DataDeclaration #
Show DataDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> DataDeclaration -> ShowS # show :: DataDeclaration -> String # showList :: [DataDeclaration] -> ShowS #
Eq DataDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: DataDeclaration -> DataDeclaration -> Bool # (/=) :: DataDeclaration -> DataDeclaration -> Bool #

data NewtypeDeclaration Source #

A newtype declaration for a type renaming.

Note that the context and the deriving parts of a newtype declaration are ignored.

Constructors

Newtype
Fields newtypeName :: Identifier The name of the type constructor. newtypeVars :: [TypeVariable] The type variables of the left-hand side. newtypeCon :: Identifier The name of the data constructor on the right-hand side. newtypeRhs :: TypeExpression The type expression on the right-hand side.

Instances

Instances details

Data NewtypeDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NewtypeDeclaration -> c NewtypeDeclaration # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NewtypeDeclaration # toConstr :: NewtypeDeclaration -> Constr # dataTypeOf :: NewtypeDeclaration -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NewtypeDeclaration) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NewtypeDeclaration) # gmapT :: (forall b. Data b => b -> b) -> NewtypeDeclaration -> NewtypeDeclaration # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NewtypeDeclaration -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NewtypeDeclaration -> r # gmapQ :: (forall d. Data d => d -> u) -> NewtypeDeclaration -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NewtypeDeclaration -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NewtypeDeclaration -> m NewtypeDeclaration # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NewtypeDeclaration -> m NewtypeDeclaration # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NewtypeDeclaration -> m NewtypeDeclaration #
Show NewtypeDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> NewtypeDeclaration -> ShowS # show :: NewtypeDeclaration -> String # showList :: [NewtypeDeclaration] -> ShowS #
Eq NewtypeDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: NewtypeDeclaration -> NewtypeDeclaration -> Bool # (/=) :: NewtypeDeclaration -> NewtypeDeclaration -> Bool #

data TypeDeclaration Source #

A type declaration for a type synonym.

Constructors

Type
Fields typeName :: Identifier The type constructor name. typeVars :: [TypeVariable] The type variables on the left-hand side. typeRhs :: TypeExpression The type expression on the right-hand side.

Instances

Instances details

Data TypeDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeDeclaration -> c TypeDeclaration # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeDeclaration # toConstr :: TypeDeclaration -> Constr # dataTypeOf :: TypeDeclaration -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeDeclaration) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeDeclaration) # gmapT :: (forall b. Data b => b -> b) -> TypeDeclaration -> TypeDeclaration # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeDeclaration -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeDeclaration -> r # gmapQ :: (forall d. Data d => d -> u) -> TypeDeclaration -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeDeclaration -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeDeclaration -> m TypeDeclaration # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeDeclaration -> m TypeDeclaration # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeDeclaration -> m TypeDeclaration #
Show TypeDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> TypeDeclaration -> ShowS # show :: TypeDeclaration -> String # showList :: [TypeDeclaration] -> ShowS #
Eq TypeDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: TypeDeclaration -> TypeDeclaration -> Bool # (/=) :: TypeDeclaration -> TypeDeclaration -> Bool #

data ClassDeclaration Source #

A class declaration for a type class.

Note that, except of type signatures of class methods, all other declarations inside the class are ignored.

Constructors

Class
Fields superClasses :: [TypeClass] The superclasses of this class. className :: Identifier The name of this type class. classVar :: TypeVariable The type variable constrained by this type class. classFuns :: [Signature] The type signatures of the class methods.

Instances

Instances details

Data ClassDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ClassDeclaration -> c ClassDeclaration # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ClassDeclaration # toConstr :: ClassDeclaration -> Constr # dataTypeOf :: ClassDeclaration -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ClassDeclaration) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ClassDeclaration) # gmapT :: (forall b. Data b => b -> b) -> ClassDeclaration -> ClassDeclaration # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ClassDeclaration -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ClassDeclaration -> r # gmapQ :: (forall d. Data d => d -> u) -> ClassDeclaration -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ClassDeclaration -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ClassDeclaration -> m ClassDeclaration # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassDeclaration -> m ClassDeclaration # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassDeclaration -> m ClassDeclaration #
Show ClassDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> ClassDeclaration -> ShowS # show :: ClassDeclaration -> String # showList :: [ClassDeclaration] -> ShowS #
Eq ClassDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: ClassDeclaration -> ClassDeclaration -> Bool # (/=) :: ClassDeclaration -> ClassDeclaration -> Bool #

data Signature Source #

A type signature.

Constructors

Signature
Fields signatureName :: Identifier The name of the signature, i.e. the name of a variable or function. signatureType :: TypeExpression The type expression of the type signature.

Instances

Instances details

Data Signature Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Signature -> c Signature # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Signature # toConstr :: Signature -> Constr # dataTypeOf :: Signature -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Signature) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Signature) # gmapT :: (forall b. Data b => b -> b) -> Signature -> Signature # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r # gmapQ :: (forall d. Data d => d -> u) -> Signature -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Signature -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Signature -> m Signature # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature #
Show Signature Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> Signature -> ShowS # show :: Signature -> String # showList :: [Signature] -> ShowS #
Eq Signature Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: Signature -> Signature -> Bool # (/=) :: Signature -> Signature -> Bool #

data DataConstructorDeclaration Source #

A data constructor declaration.

Constructors

DataCon
Fields dataConName :: Identifier The name of the data constructor. dataConTypes :: [BangTypeExpression] The type arguments of the data constructor.

Instances

Instances details

Data DataConstructorDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataConstructorDeclaration -> c DataConstructorDeclaration # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataConstructorDeclaration # toConstr :: DataConstructorDeclaration -> Constr # dataTypeOf :: DataConstructorDeclaration -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataConstructorDeclaration) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataConstructorDeclaration) # gmapT :: (forall b. Data b => b -> b) -> DataConstructorDeclaration -> DataConstructorDeclaration # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataConstructorDeclaration -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataConstructorDeclaration -> r # gmapQ :: (forall d. Data d => d -> u) -> DataConstructorDeclaration -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DataConstructorDeclaration -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataConstructorDeclaration -> m DataConstructorDeclaration # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataConstructorDeclaration -> m DataConstructorDeclaration # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataConstructorDeclaration -> m DataConstructorDeclaration #
Show DataConstructorDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> DataConstructorDeclaration -> ShowS # show :: DataConstructorDeclaration -> String # showList :: [DataConstructorDeclaration] -> ShowS #
Eq DataConstructorDeclaration Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: DataConstructorDeclaration -> DataConstructorDeclaration -> Bool # (/=) :: DataConstructorDeclaration -> DataConstructorDeclaration -> Bool #

data BangTypeExpression Source #

Indicates whether in an algebraic data type declaration a strictness annotation is used.

Constructors

Banged	A type expression with a strictness flag "`!`".
Fields withoutBang :: TypeExpression
Unbanged	A type expression without a strictness flag.
Fields withoutBang :: TypeExpression

Instances

Instances details

Data BangTypeExpression Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BangTypeExpression -> c BangTypeExpression # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BangTypeExpression # toConstr :: BangTypeExpression -> Constr # dataTypeOf :: BangTypeExpression -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BangTypeExpression) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BangTypeExpression) # gmapT :: (forall b. Data b => b -> b) -> BangTypeExpression -> BangTypeExpression # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BangTypeExpression -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BangTypeExpression -> r # gmapQ :: (forall d. Data d => d -> u) -> BangTypeExpression -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BangTypeExpression -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BangTypeExpression -> m BangTypeExpression # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BangTypeExpression -> m BangTypeExpression # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BangTypeExpression -> m BangTypeExpression #
Show BangTypeExpression Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> BangTypeExpression -> ShowS # show :: BangTypeExpression -> String # showList :: [BangTypeExpression] -> ShowS #
Eq BangTypeExpression Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: BangTypeExpression -> BangTypeExpression -> Bool # (/=) :: BangTypeExpression -> BangTypeExpression -> Bool #

Type expressions

data TypeExpression Source #

A Haskell type expression. This data type supports also higher-rank functions. Unlike in Haskell98, a type variable must not be applied to type expressions.

Constructors

TypeVar TypeVariable	A type variable.
TypeCon TypeConstructor [TypeExpression]	A type constructor. This covers algebraic data types, type synonyms, and type renamings as well as predefined standard data types like lists and tuples.
TypeFun TypeExpression TypeExpression	The function type constructor `->`.
TypeFunLab TypeExpression TypeExpression	The function type constructor `->^o` for the non-bottom-reflecting logical relation for functions in the languagesubset with seq for equational theorems.
TypeAbs TypeVariable [TypeClass] TypeExpression	The type abstraction constructor `forall`.
TypeAbsLab TypeVariable [TypeClass] TypeExpression	The type abstraction constructor `forall^o`, allowing non-bottom-reflecting logical relations for types the type variable is instantiated with in the calculus with seq.
TypeExp FixedTypeExpression	A variable representing a fixed type expression.

Instances

Instances details

Data TypeExpression Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeExpression -> c TypeExpression # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeExpression # toConstr :: TypeExpression -> Constr # dataTypeOf :: TypeExpression -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeExpression) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeExpression) # gmapT :: (forall b. Data b => b -> b) -> TypeExpression -> TypeExpression # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeExpression -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeExpression -> r # gmapQ :: (forall d. Data d => d -> u) -> TypeExpression -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeExpression -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeExpression -> m TypeExpression # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeExpression -> m TypeExpression # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeExpression -> m TypeExpression #
Show TypeExpression Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> TypeExpression -> ShowS # show :: TypeExpression -> String # showList :: [TypeExpression] -> ShowS #
Eq TypeExpression Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: TypeExpression -> TypeExpression -> Bool # (/=) :: TypeExpression -> TypeExpression -> Bool #

data TypeConstructor Source #

The data type for type constructors.

Constructors

ConUnit	The unit type constructor `()`.
ConList	The list type constructor `[]`.
ConTuple Int	The tuple type constructors with given arity.
ConInt	The Haskell type `Int`.
ConInteger	The Haskell type `Integer`.
ConFloat	The Haskell type `Float`.
ConDouble	The Haskell type `Double`.
ConChar	The Haskell type `Char`.
Con Identifier	Any other type constructor with a given name.

Instances

Instances details

Data TypeConstructor Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeConstructor -> c TypeConstructor # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeConstructor # toConstr :: TypeConstructor -> Constr # dataTypeOf :: TypeConstructor -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeConstructor) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeConstructor) # gmapT :: (forall b. Data b => b -> b) -> TypeConstructor -> TypeConstructor # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeConstructor -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeConstructor -> r # gmapQ :: (forall d. Data d => d -> u) -> TypeConstructor -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeConstructor -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeConstructor -> m TypeConstructor # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeConstructor -> m TypeConstructor # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeConstructor -> m TypeConstructor #
Eq TypeConstructor Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: TypeConstructor -> TypeConstructor -> Bool # (/=) :: TypeConstructor -> TypeConstructor -> Bool #

newtype TypeClass Source #

Identifies a Haskell type class.

Constructors

TC Identifier

Instances

Instances details

Data TypeClass Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeClass -> c TypeClass # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeClass # toConstr :: TypeClass -> Constr # dataTypeOf :: TypeClass -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeClass) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeClass) # gmapT :: (forall b. Data b => b -> b) -> TypeClass -> TypeClass # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeClass -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeClass -> r # gmapQ :: (forall d. Data d => d -> u) -> TypeClass -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeClass -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeClass -> m TypeClass # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeClass -> m TypeClass # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeClass -> m TypeClass #
Show TypeClass Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> TypeClass -> ShowS # show :: TypeClass -> String # showList :: [TypeClass] -> ShowS #
Eq TypeClass Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: TypeClass -> TypeClass -> Bool # (/=) :: TypeClass -> TypeClass -> Bool #

newtype TypeVariable Source #

Identifies a Haskell type variable

Constructors

TV Identifier

Instances

Instances details

Data TypeVariable Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeVariable -> c TypeVariable # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeVariable # toConstr :: TypeVariable -> Constr # dataTypeOf :: TypeVariable -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeVariable) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeVariable) # gmapT :: (forall b. Data b => b -> b) -> TypeVariable -> TypeVariable # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeVariable -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeVariable -> r # gmapQ :: (forall d. Data d => d -> u) -> TypeVariable -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeVariable -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeVariable -> m TypeVariable # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeVariable -> m TypeVariable # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeVariable -> m TypeVariable #
Show TypeVariable Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> TypeVariable -> ShowS # show :: TypeVariable -> String # showList :: [TypeVariable] -> ShowS #
Eq TypeVariable Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: TypeVariable -> TypeVariable -> Bool # (/=) :: TypeVariable -> TypeVariable -> Bool #
Ord TypeVariable Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods compare :: TypeVariable -> TypeVariable -> Ordering # (<) :: TypeVariable -> TypeVariable -> Bool # (<=) :: TypeVariable -> TypeVariable -> Bool # (>) :: TypeVariable -> TypeVariable -> Bool # (>=) :: TypeVariable -> TypeVariable -> Bool # max :: TypeVariable -> TypeVariable -> TypeVariable # min :: TypeVariable -> TypeVariable -> TypeVariable #

newtype FixedTypeExpression Source #

Represents an abbreviation for some fixed type expression. It does not occur in Haskell98 source code, but it can occur in generated theorems.

Constructors

TF Identifier

Instances

Instances details

Data FixedTypeExpression Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FixedTypeExpression -> c FixedTypeExpression # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FixedTypeExpression # toConstr :: FixedTypeExpression -> Constr # dataTypeOf :: FixedTypeExpression -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FixedTypeExpression) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FixedTypeExpression) # gmapT :: (forall b. Data b => b -> b) -> FixedTypeExpression -> FixedTypeExpression # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FixedTypeExpression -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FixedTypeExpression -> r # gmapQ :: (forall d. Data d => d -> u) -> FixedTypeExpression -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FixedTypeExpression -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FixedTypeExpression -> m FixedTypeExpression # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FixedTypeExpression -> m FixedTypeExpression # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FixedTypeExpression -> m FixedTypeExpression #
Show FixedTypeExpression Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> FixedTypeExpression -> ShowS # show :: FixedTypeExpression -> String # showList :: [FixedTypeExpression] -> ShowS #
Eq FixedTypeExpression Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: FixedTypeExpression -> FixedTypeExpression -> Bool # (/=) :: FixedTypeExpression -> FixedTypeExpression -> Bool #

Identifiers

newtype Identifier Source #

An identifier. This data type tags every String occurring in a declaration or a type expression.

Constructors

Ident
Fields unpackIdent :: String

Instances

Instances details

Data Identifier Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Identifier -> c Identifier # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Identifier # toConstr :: Identifier -> Constr # dataTypeOf :: Identifier -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Identifier) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Identifier) # gmapT :: (forall b. Data b => b -> b) -> Identifier -> Identifier # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Identifier -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Identifier -> r # gmapQ :: (forall d. Data d => d -> u) -> Identifier -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Identifier -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Identifier -> m Identifier # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Identifier -> m Identifier # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Identifier -> m Identifier #
Show Identifier Source #
Instance details Defined in Language.Haskell.FreeTheorems.PrettyTypes Methods showsPrec :: Int -> Identifier -> ShowS # show :: Identifier -> String # showList :: [Identifier] -> ShowS #
Eq Identifier Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods (==) :: Identifier -> Identifier -> Bool # (/=) :: Identifier -> Identifier -> Bool #
Ord Identifier Source #
Instance details Defined in Language.Haskell.FreeTheorems.BasicSyntax Methods compare :: Identifier -> Identifier -> Ordering # (<) :: Identifier -> Identifier -> Bool # (<=) :: Identifier -> Identifier -> Bool # (>) :: Identifier -> Identifier -> Bool # (>=) :: Identifier -> Identifier -> Bool # max :: Identifier -> Identifier -> Identifier # min :: Identifier -> Identifier -> Identifier #