Safe Haskell | None |
---|
Data structures to describe theorems generated from types.
- type Theorem = Formula
- data Formula
- = ForallRelations RelationVariable (TypeExpression, TypeExpression) [Restriction] Formula
- | ForallFunctions (Either TermVariable TermVariable) (TypeExpression, TypeExpression) [Restriction] Formula
- | ForallPairs (TermVariable, TermVariable) Relation Formula
- | ForallVariables TermVariable TypeExpression Formula
- | Equivalence Formula Formula
- | Implication Formula Formula
- | Conjunction Formula Formula
- | Predicate Predicate
- data Restriction
- = Strict
- | Continuous
- | Total
- | BottomReflecting
- | LeftClosed
- | RespectsClasses [TypeClass]
- data Predicate
- data Term
- = TermVar TermVariable
- | TermIns Term TypeExpression
- | TermApp Term Term
- | TermComp [Term]
- newtype TermVariable = TVar String
- data Relation
- = RelVar RelationInfo RelationVariable
- | FunVar RelationInfo (Either Term Term)
- | RelBasic RelationInfo
- | RelLift RelationInfo TypeConstructor [Relation]
- | RelFun RelationInfo Relation Relation
- | RelFunLab RelationInfo Relation Relation
- | RelAbs RelationInfo RelationVariable (TypeExpression, TypeExpression) [Restriction] Relation
- | FunAbs RelationInfo (Either TermVariable TermVariable) (TypeExpression, TypeExpression) [Restriction] Relation
- relationInfo :: Relation -> RelationInfo
- data RelationInfo = RelationInfo {}
- newtype RelationVariable = RVar String
- data UnfoldedLift = UnfoldedLift Relation [UnfoldedDataCon]
- data UnfoldedDataCon
- data DataConstructor
- = DConEmptyList
- | DConConsList
- | DConTuple Int
- | DCon String
- data UnfoldedClass = UnfoldedClass [TypeClass] TypeClass (Either RelationVariable TermVariable) [Formula]
Documentation
Logical formula constituting automatically generated theorems.
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.
Predicates occurring in formulas.
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 |
Terms consisting of variables, applications and instantiations.
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 |
newtype TermVariable Source
Variables occurring in terms.
Relations are the foundations of free theorems.
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.
RelationInfo | |
|
newtype RelationVariable Source
A relation variable.
data UnfoldedLift Source
Describes unfolded lift relations.
data UnfoldedDataCon Source
A relational descriptions of a data constructor.
data DataConstructor Source
Data 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.