lambdabot-4.1: scripts/FT/FreeTheorems/Declarations.hs
-- Copyright 2006, Sascha Boehme.
-- | This module defines the accepted user-defined types.
-- It covers only algebraic datatypes and type synonyms.
module FreeTheorems.Declarations (
-- * Haskell type declarations
DataDeclaration(..),
DataConstructorDeclaration(..),
Type(..),
TypeDeclaration(..),
TypeConstructor,
Arity,
-- * Type information
isDefined,
getDataDecl,
getTypeDecl,
getSupportedAlgebraicDatatypes,
getSupportedTypeSynonyms,
-- testing interface
testDeclarations
) where
import FreeTheorems.Types
-- | Gives a notation for the declaration of an algebraic datatype.
-- The right-hand side is defined as a function type to replace type variables
-- easily by arbitrary types. The argument list of this function should be
-- exactly as long as the arity of the type constructor.
-- The types of the right-hand side should not contain any type synonym
-- because right-hand sides will not be prepared the same way as types
-- inputted by the user.
data DataDeclaration = DataDecl TypeConstructor Arity
([Type] -> [DataConstructorDeclaration])
-- | Denotes the declaration of a data constructor as it occurs in definitions
-- of algebraic datatypes.
data DataConstructorDeclaration = DataConDecl DataConstructor [Type]
-- | Represents the declaration of a type synonym.
-- The right-hand side is defined as a function type to replace type variables
-- easily by arbitrary types. The argument list of this function should be
-- exactly as long as the arity of the type constructor.
data TypeDeclaration = TypeDecl TypeConstructor Arity ([Type] -> Type)
-- | Used to describe the rank or arity of type constructors.
type Arity = Int
-- | Stores valid user-defined types.
-- It contains algebraic datatypes and type synonyms along with their
-- right-hand side.
data UserDefinedTypes = UserDefinedTypes {
dataDecls :: [DataDeclaration], -- ^ A list of valid algebraic data types
-- each of them with their right-hand
-- side.
typeDecls :: [TypeDeclaration] -- ^ A list of valid type synonymes each of
-- them with their right-hand side.
}
-- | Checks if a type constructor occurs in the list of accepted user-defined
-- types.
isDefined :: TypeConstructor -> Bool
isDefined t =
any (\(DataDecl t' _ _) -> (t == t')) (dataDecls userDefinedTypes)
|| any (\(TypeDecl t' _ _) -> (t == t')) (typeDecls userDefinedTypes)
-- | Returns the declaration of an algebraic datatype, if it occurs in the list
-- of accepted algebraic datatypes.
getDataDecl :: TypeConstructor -> Maybe DataDeclaration
getDataDecl t =
case (filter (\(DataDecl t' _ _)-> (t == t')) (dataDecls userDefinedTypes)) of
[] -> Nothing
(d:_) -> Just d
-- | Returns the declaration of a type synonym, if it occurs in the list of
-- accepted type synonyms.
getTypeDecl :: TypeConstructor -> Maybe TypeDeclaration
getTypeDecl t =
case (filter (\(TypeDecl t' _ _)-> (t == t')) (typeDecls userDefinedTypes)) of
[] -> Nothing
(d:_) -> Just d
-- | Returns the list of algebraic datatypes being supported by the FreeTheorems
-- library. For each algebraic datatype, its name and arity are returned.
getSupportedAlgebraicDatatypes :: [(String, Int)]
getSupportedAlgebraicDatatypes = map (\(DataDecl n i _) -> (n,i))
(dataDecls userDefinedTypes)
-- | Returns the list of type synonyms being supported by the FreeTheorems
-- library. For each type synonym, its name and arity are returned.
getSupportedTypeSynonyms :: [(String, Int)]
getSupportedTypeSynonyms = map (\(TypeDecl n i _) -> (n,i))
(typeDecls userDefinedTypes)
-- | Defines the set of valid user-defined types.
-- This sets defines all types which may occur in type terms from which
-- theorems can be generated. Except of predefined types, no more types are
-- allowed in type terms.
userDefinedTypes :: UserDefinedTypes
userDefinedTypes = UserDefinedTypes {
-- Note that the types of the right-hand side should not contain any type
-- synonym because it will not be replaced.
dataDecls = [
DataDecl "Bool" 0 (\[] ->
[DataConDecl "False" []
,DataConDecl "True" []
]),
DataDecl "Maybe" 1 (\[a] ->
[DataConDecl "Nothing" []
,DataConDecl "Just" [a]
]),
DataDecl "Either" 2 (\[a, b] ->
[DataConDecl "Left" [a]
,DataConDecl "Right" [b]
]),
DataDecl "Ordering" 0 (\[] ->
[DataConDecl "LT" []
,DataConDecl "EQ" []
,DataConDecl "GT" []
]),
DataDecl "IOMode" 0 (\[] ->
[DataConDecl "ReadMode" []
,DataConDecl "WriteMode" []
,DataConDecl "AppendMode" []
,DataConDecl "ReadWriteMode" []
]),
DataDecl "BufferMode" 0 (\[] ->
[DataConDecl "NoBuffering" []
,DataConDecl "LineBuffering" []
,DataConDecl "BlockBuffering" [TypeCon "Maybe" [TypeBasic Int]]
]),
DataDecl "SeekMode" 0 (\[] ->
[DataConDecl "AbsoluteSeek" []
,DataConDecl "RelativeSeek" []
,DataConDecl "SeekFromEnd" []
]),
DataDecl "Permissions" 0 (\[] ->
[DataConDecl "Permissions" [TypeCon "Bool" [] -- readable
,TypeCon "Bool" [] -- writable
,TypeCon "Bool" [] -- executable
,TypeCon "Bool" [] -- searchable
]]),
DataDecl "ExitCode" 0 (\[] ->
[DataConDecl "ExitSuccess" []
,DataConDecl "ExitFailure" [TypeBasic Int]
]),
DataDecl "Month" 0 (\[] ->
[DataConDecl "January" []
,DataConDecl "February" []
,DataConDecl "March" []
,DataConDecl "April" []
,DataConDecl "May" []
,DataConDecl "June" []
,DataConDecl "July" []
,DataConDecl "August" []
,DataConDecl "September" []
,DataConDecl "October" []
,DataConDecl "November" []
,DataConDecl "December" []
]),
DataDecl "Day" 0 (\[] ->
[DataConDecl "Sunday" []
,DataConDecl "Monday" []
,DataConDecl "Tuesday" []
,DataConDecl "Wednesday" []
,DataConDecl "Thursday" []
,DataConDecl "Friday" []
,DataConDecl "Saturday" []
]),
DataDecl "CalenderTime" 0 (\[] ->
[DataConDecl "CalenderTime" [TypeBasic Int -- ctYear
,TypeCon "Month" [] -- ctMonth
,TypeBasic Int -- ctDay
,TypeBasic Int -- ctHour
,TypeBasic Int -- ctMin
,TypeBasic Int -- ctSec
,TypeBasic Integer -- ctPicosec
,TypeCon "Day" [] -- ctWDay
,TypeBasic Int -- ctYDay
,TypeList (TypeBasic Char) -- ctTZName
,TypeBasic Int -- ctTZ
,TypeCon "Bool" [] -- ctIsDST
]]),
DataDecl "TimeDiff" 0 (\[] ->
[DataConDecl "TimeDiff" [TypeBasic Int -- tdYear
,TypeBasic Int -- tdMonth
,TypeBasic Int -- tdDay
,TypeBasic Int -- tdHour
,TypeBasic Int -- tdMin
,TypeBasic Int -- tdSec
,TypeBasic Integer -- tdPicosec
]]),
DataDecl "TimeLocale" 0 (\[] ->
[DataConDecl "TimeLocale"
[TypeList (TypeTuple [TypeList (TypeBasic Char)
,TypeList (TypeBasic Char)]) -- wDays
,TypeList (TypeTuple [TypeList (TypeBasic Char)
,TypeList (TypeBasic Char)]) -- months
,TypeTuple [TypeList (TypeBasic Char)
,TypeList (TypeBasic Char)] -- amPm
,TypeList (TypeBasic Char) -- dateTimeFmt
,TypeList (TypeBasic Char) -- dateFmt
,TypeList (TypeBasic Char) -- timeFmt
,TypeList (TypeBasic Char) -- time12Fmt
]])
],
typeDecls = [
TypeDecl "String" 0
(\[] -> TypeList (TypeBasic Char)),
TypeDecl "ReadS" 1
(\[a] -> TypeFun (TypeCon "String" [])
(TypeList (TypeTuple [a, TypeCon "String" []]))),
TypeDecl "ShowS" 0
(\[] -> TypeFun (TypeCon "String" []) (TypeCon "String" [])),
TypeDecl "FilePath" 0
(\[] -> TypeCon "String" [])
]
}
--------------------------------------------------------------------------------
-- A list of tests for this module.
testDeclarations = do
putStr "declarations contain no function and forall ... "
putStrLn (if test_no_fun_forall then "OK" else "FALSE")
-- Check that data declarations contain no functions and type abstractions in
-- its right-hand sides.
test_no_fun_forall = and $ map hasNoFunForall (dataDecls userDefinedTypes)
hasNoFunForall (DataDecl _ n f) =
let vs = map (\i -> TypeVar ("a" ++ show i)) [1..n]
ts = concatMap (\(DataConDecl _ ts) -> ts) (f vs)
in and $ map noFunForall ts
noFunForall t =
case t of
TypeBasic _ -> True
TypeVar _ -> True
TypeTermVar _ -> True
TypeCon _ ts -> and $ map noFunForall ts
TypeList t' -> noFunForall t'
TypeUnit -> True
TypeTuple ts -> and $ map noFunForall ts
TypeFun _ _ -> False
TypeForall _ _ -> False