Safe Haskell | None |
---|
internal representation of Rainbow termination proofs, see http://color.loria.fr/ this file is modelled after rainbow/proof.ml it omits constructors not needed for matrix interpretations (for the moment)
- data Vector a = Vector [a]
- data Matrix a = Matrix [Vector a]
- data MaxPlus
- data MinPlus
- data Mi_Fun a = Mi_Fun {}
- data Poly_Fun a = Poly_Fun {
- coefficients :: [a]
- type Matrix_Int = Interpretation Mi_Fun
- type Polynomial_Int = Interpretation Poly_Fun
- data Interpretation f = forall k a . (XmlContent k, XmlContent a, ToExotic a, Typeable a) => Interpretation {}
- data Domain
- = Natural
- | Arctic
- | Arctic_Below_Zero
- | Tropical
- data Red_Ord
- data Usable_Rules = Usable_Rules [Identifier]
- data Simple_Projection = Simple_Projection [(Identifier, Int)]
- data Claim = Claim {}
- data Proof = Proof {}
- data Property
- = Termination
- | Top_Termination
- | Complexity (Function, Function)
- data Function
- = Unknown
- | Polynomial { }
- | Exponential
- data Reason
- data Over_Graph
- = HDE
- | HDE_Marked
- data Marked a
Documentation
Vector [a] |
Typeable1 Vector | |
(Typeable a, XmlContent a) => XmlContent (Vector a) | |
XRead a => XRead (Vector a) |
Typeable1 Matrix | |
(Typeable a, XmlContent a) => XmlContent (Matrix a) | |
XRead a => XRead (Matrix a) |
Typeable1 Mi_Fun | |
XmlContent Matrix_Int | |
XRead Matrix_Int | |
(Typeable a, XmlContent a) => XmlContent (Mi_Fun a) | |
XRead a => XRead (Mi_Fun a) |
type Matrix_Int = Interpretation Mi_FunSource
data Interpretation f Source
forall k a . (XmlContent k, XmlContent a, ToExotic a, Typeable a) => Interpretation | |
data Simple_Projection Source
see specification: http:termination-portal.orgwikiComplexity