FreeTheoremsContentsIndex
FreeTheorems
Contents
Types and theorems
Parsing of types
Generation and deduction of theorems
Pretty-printing
Description

This module is the interface to the FreeTheorems library. It exposes all types and functions needed to parse types, generate theorems for them and pretty-print types and theorems.

Although every type below is an instance of the class Show, the provided pretty-printing classes should be used to display them. The standard show function is only available for debugging purposes.

Synopsis
data LanguageModel
= BasicModel
| FixModel
data NamedType = NamedType TermVariable Type
data TermVariable
data Type
data Theorem
data RelationVariable
data UnfoldedRelation
data TheoremData
parseNamedType :: String -> Either ParseError NamedType
parseType :: (String -> Bool) -> String -> Either ParseError NamedType
getSupportedAlgebraicDatatypes :: [(String, Int)]
getSupportedTypeSynonyms :: [(String, Int)]
generateTheorem :: LanguageModel -> NamedType -> (Theorem, TheoremData)
extractLiftRelations :: (Theorem, TheoremData) -> Bool -> [UnfoldedRelation]
extractRelationVariables :: Theorem -> [RelationVariable]
instantiateRelation :: (Theorem, TheoremData) -> RelationVariable -> (Theorem, TheoremData)
omitInstantiations :: Theorem -> Theorem
class PrettyPrintAsText a where
printAsText :: a -> String
Types and theorems
data LanguageModel
Specifies the Haskell language model used in generating theorems.
Constructors
BasicModelMost restrictive language model which does not allow any of the relaxations the other models are providing.
FixModelAllows fixpoints and _|_ in the used Haskell subset.
show/hide Instances
data NamedType
A Haskell type with an associated name.
Constructors
NamedType TermVariable Type
show/hide Instances
data TermVariable
Describes a variable occurring in terms.
show/hide Instances
data Type
Describes Haskell types. This algebraic datatype is powerful enough to not only model Haskell98 types, but also higher-rank function types.
show/hide Instances
Eq Type
Show Type
data Theorem
Defines a structure to describe free theorems.
show/hide Instances
data RelationVariable
Specifies relation variable or function variables as a special case of a relation.
show/hide Instances
data UnfoldedRelation
Gives a means to describe unfolded relations, i.e. relations and corresponding sets which specify explicitely the members of that relation.
show/hide Instances
data TheoremData
Stores information used to create unique indices. It is used while generating theorems for types.
Parsing of types
parseNamedType
:: StringThe string to be parsed.
-> Either ParseError NamedTypeReturns the parsed named type or a parser error.

Parses a Haskell type string and creates a named type.

The content of the string argument has to be conforming to the following EBNF syntax: 

 NamedType ::= Name :: TypeTerm

where Name is a token starting with a lower letter or _, and consisting of alphanumeric letters and the characters _ and ' from the second character onwards. A Name starting with _ has to be at least two characters long, because _ is a reserved identifier in Haskell.

Alternatively, a Name can also be an operator which has to be enclosed in parentheses. Allowed characters of operators are 

 ! | # | $ | % | & | * | + | . | / | < | = | > | ? | @ | \ | ^ | | | - | ~

and the colon : from the second although character onwards. Note that the following operators are restricted keywords in Haskell and can not be used as names of types: 

 .. | : | :: | = | \ | | | <- | -> | @ | ~ | =>

For the syntax of a TypeTerm see parseType.

parseType
:: (String -> Bool)When parseType is trying to automatically create a name for the type, this function is asked if a name is acceptable.
-> StringThe string to be parsed.
-> Either ParseError NamedTypeReturns the parsed named type with the generated name or an parser error.

Parses a Haskell type string and creates a named type.

A type string has to be conforming to the following EBNF syntax: 

 TypeTerm ::= SimpleTypeTerm
            | SimpleTypeTerm "->" TypeTerm
            | "forall" TypeVariableList "." TypeTerm

 SimpleTypeTerm ::= ATypeTerm
                  | TypeConstructor ATypeTermList
                  | "[]" ATypeTerm
                  | "(,)" ATypeTerm ATypeTerm
                  | "(,,)" ATypeTerm ATypeTerm ATypeTerm
                  | ...
                  | {- tuple in prefix notation of arity 15 -}
                  | "(->)" ATypeTerm ATypeTerm

 ATypeTerm ::= "Char" | "Int" | "Integer" | "Float" | "Double"
             | TypeVariable
             | "()"
             | "[" TypeTerm "]"
             | "(" TypeTerm "," TypeTerm ")"
             | "(" TypeTerm "," TypeTerm "," TypeTerm ")"
             | ...
             | {- tuple of arity 15 -}
             | "(" TypeTerm ")"

 ATypeTermList ::= ATypeTerm
                 | ATypeTermList ATypeTerm

 TypeVariableList ::= TypeVariable
                    | TypeVariableList TypeVariable

where TypeVariable is a token starting with a lower letter or _, while TypeConstructor starts with a capital letter. Every of these two tokens may consist of alphanumeric letters and the characters _ and ' from the second character onwards. A TypeVariable starting with _ has to be at least two characters long, because _ is a reserved identifier in Haskell. Type constructors can not be formed from symbols.

Although tuples are restricted to an arity of 15, tuples in the usual non-prefixed way can be arbitrary large. However, applications should not rely on this possibility.

An additional rule limits the valid type terms: The number of type arguments for a type constructor must match the type constructors arity.

getSupportedAlgebraicDatatypes :: [(String, Int)]
Returns the list of algebraic datatypes being supported by the FreeTheorems library. For each algebraic datatype, its name and arity are returned.
getSupportedTypeSynonyms :: [(String, Int)]
Returns the list of type synonyms being supported by the FreeTheorems library. For each type synonym, its name and arity are returned.
Generation and deduction of theorems
generateTheorem :: LanguageModel -> NamedType -> (Theorem, TheoremData)
Generates a theorem for a named type using a certain language model.
extractLiftRelations :: (Theorem, TheoremData) -> Bool -> [UnfoldedRelation]
Creates a list of all lifted relations occurring in the given theorem. Lifted relations are lift relations as well as functional relations and relational abstractions. The lifted relations are returned together with their unfolded description.
extractRelationVariables :: Theorem -> [RelationVariable]

Returns all relation variables of a theorem which can be specialized to a function. Relation variables being quantified on the left-hand side of an implication can not be specialized. However, relation variables being quantified like 

   ((forall R. theorem) ==> theorem1) ==> theorem2

can be specialized. Thus, the position relative to implications decides whether a relation variable is returned by this function.

instantiateRelation :: (Theorem, TheoremData) -> RelationVariable -> (Theorem, TheoremData)
Instantiates a relation variable found by extractRelationVariables in the given theorem. A new function symbol is created to replace the relation variable.
omitInstantiations :: Theorem -> Theorem
Omits all instantiations in the terms of the given theorem.
Pretty-printing
class PrettyPrintAsText a where
Conversion of values to Strings. Derived instances of PrettyPrintAsText show their values using printAsText. The pretty-printed text is optimized consoles or text files having a line length of at least 75 characters.
Methods
printAsText :: a -> String
Pretty-prints a value as plain text with a maximum line length of 75 characters.
show/hide Instances
Produced by Haddock version 0.7