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

Safe HaskellNone

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.

data Restriction Source

Restrictions on functions and relations.

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

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

newtype TermVariable Source

Variables occurring in terms.

Constructors

TVar String 

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.

relationInfo :: Relation -> RelationInfoSource

Extracts the relation information from a relation.

data RelationInfo Source

The relation information stored with every relation.

Constructors

RelationInfo 

Fields

relationLanguageSubset :: LanguageSubset

The language subset in which a relation was generated.

relationLeftType :: TypeExpression

The type of the first components of pairs contained in a relation.

relationRightType :: TypeExpression

The type of the second components of pairs contained in a relation.

newtype RelationVariable Source

A relation variable.

Constructors

RVar String 

data UnfoldedLift Source

Describes unfolded lift relations.

data UnfoldedDataCon Source

A relational descriptions of a data constructor.

data DataConstructor Source

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.

data UnfoldedClass Source

A relational description of a class declaration.