free-theorems-0.3.2.0: Automatic generation of free theorems.

Safe Haskell None

Language.Haskell.FreeTheorems.Theorems

Description

Data structures to describe theorems generated from types.

Synopsis

# Documentation

type Theorem = FormulaSource

A theorem which is generated from a type signature.

data Formula Source

Logical formula constituting automatically generated theorems.

Constructors

 ForallRelations RelationVariable (TypeExpression, TypeExpression) [Restriction] Formula Quantifies a relation variable and two type expressions. ForallFunctions (Either TermVariable TermVariable) (TypeExpression, TypeExpression) [Restriction] Formula Quantifies a function variable and two type expressions. ForallPairs (TermVariable, TermVariable) Relation Formula Quantifies two term variables taken from a relation. ForallVariables TermVariable TypeExpression Formula Quantifies a term variable of a certain type. Equivalence Formula Formula Two formulas are equivalent. Implication Formula Formula The first formula implies the second formula. Conjunction Formula Formula The first formula and the second formula. Predicate Predicate A basic formula.

Instances

 Data Formula Typeable Formula

Restrictions on functions and relations.

Constructors

 Strict Continuous Total BottomReflecting LeftClosed RespectsClasses [TypeClass]

Instances

 Eq Restriction Data Restriction Typeable Restriction

data Predicate Source

Predicates occurring in formulas.

Constructors

 IsMember Term Term Relation The pair of two terms is contained in a relation. IsEqual Term Term Two terms are equal. IsLessEq Term Term The first term is less defined than the second one, based on the semantical approximation order. IsNotBot Term The term is not equal to `_|_`. IsTrue Constant True Predicate

Instances

 Data Predicate Typeable Predicate

data Term Source

Terms consisting of variables, applications and instantiations.

Constructors

 TermVar TermVariable A term variable. TermIns Term TypeExpression Instantiation of a term. TermApp Term Term Application of a term to a term. TermComp [Term] Composition of function terms

Instances

 Eq Term Data Term Typeable Term

newtype TermVariable Source

Variables occurring in terms.

Constructors

 TVar String

Instances

 Eq TermVariable Data TermVariable Typeable TermVariable

data Relation Source

Relations are the foundations of free theorems.

Constructors

 RelVar RelationInfo RelationVariable A relation variable. FunVar RelationInfo (Either Term Term) A function variable. It might be either a function to be applied on the left side (in equational and inequational cases) or on the right side (in inequational cases only). In inequational cases, the term is additionally composed with the semantic approximation partial order. RelBasic RelationInfo A basic relation corresponding to a nullary type constructor. Depending on the theorem type, this can be either an equivalence relation or the semantic approximation partial order. RelLift RelationInfo TypeConstructor [Relation] A lifted relation for any nonnullary type constructor. The semantics of lifted relations is differs with the language subset: In inequational subsets lifted relations explicitly require left-closedness by composition with the semantic approximation partial order. In equational subsets with fix or seq, this relation requires strictness explicitly by relating the undefined value with itself. RelFun RelationInfo Relation Relation A relation corresponding to a function type constructor. The semantics of this relation differs with the language subset: In the equational subset with seq, this relation is explicitly requiring bottom-reflectiveness of its members. In the inequational subset with seq, this relation is explicitly requiring totality of its members. RelFunLab RelationInfo Relation Relation A relation corresponding to a function type constructor. The semantics of this relation differs with the language subset: Apart from the equational subset with seq, it is equal to RelFun. In the equational subset with Seq, this relation is _not_ explicitly requiring bottom-reflectiveness of its members. RelAbs RelationInfo RelationVariable (TypeExpression, TypeExpression) [Restriction] Relation A relation corresponding to a type abstraction. FunAbs RelationInfo (Either TermVariable TermVariable) (TypeExpression, TypeExpression) [Restriction] Relation A quantified function.

Instances

 Eq Relation Data Relation Typeable Relation

Extracts the relation information from a relation.

The relation information stored with every relation.

Constructors

 RelationInfo FieldsrelationLanguageSubset :: LanguageSubsetThe language subset in which a relation was generated. relationLeftType :: TypeExpressionThe type of the first components of pairs contained in a relation. relationRightType :: TypeExpressionThe type of the second components of pairs contained in a relation.

Instances

 Eq RelationInfo Data RelationInfo Typeable RelationInfo

newtype RelationVariable Source

A relation variable.

Constructors

 RVar String

Describes unfolded lift relations.

Constructors

 UnfoldedLift Relation [UnfoldedDataCon]

Instances

 Data UnfoldedLift Typeable UnfoldedLift

A relational descriptions of a data constructor.

Constructors

 BotPair ConPair DataConstructor ConMore DataConstructor [TermVariable] [TermVariable] Formula

Instances

 Data UnfoldedDataCon Typeable UnfoldedDataCon

Data constructors.

Constructors

 DConEmptyList The nullary data constructor `[]`. DConConsList The binary data constructor `:`. DConTuple Int The n-ary tuple data constructor. DCon String Any other data constructor.

Instances

 Data DataConstructor Typeable DataConstructor

A relational description of a class declaration.

Constructors

 UnfoldedClass [TypeClass] TypeClass (Either RelationVariable TermVariable) [Formula]

Instances

 Data UnfoldedClass Typeable UnfoldedClass