Safe Haskell	None
Language	Haskell98

TPDB.Rainbow.Proof.Type

Description

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)

Synopsis

Documentation

data Vector a Source

Constructors

Vector [a]

Instances

(Typeable * a, XmlContent a) => XmlContent (Vector a)
XRead a => XRead (Vector a)
Typeable (* -> *) Vector

data Matrix a Source

Constructors

Matrix [Vector a]

Instances

(Typeable * a, XmlContent a) => XmlContent (Matrix a)
XRead a => XRead (Matrix a)
Typeable (* -> *) Matrix

data MaxPlus Source

Constructors

MinusInfinite
MaxPlusFinite Integer

Instances

Read MaxPlus
Show MaxPlus
XmlContent MaxPlus
ToExotic MaxPlus
Typeable * MaxPlus

data MinPlus Source

Constructors

MinPlusFinite Integer
PlusInfinite

Instances

Read MinPlus
Show MinPlus
ToExotic MinPlus
Typeable * MinPlus

data Mi_Fun a Source

Constructors

Mi_Fun
Fields mi_const :: Vector a mi_args :: [Matrix a]

Instances

XmlContent Matrix_Int
XRead Matrix_Int
(Typeable * a, XmlContent a) => XmlContent (Mi_Fun a)
XRead a => XRead (Mi_Fun a)
Typeable (* -> *) Mi_Fun

data Poly_Fun a Source

Constructors

Poly_Fun
Fields coefficients :: [a]

Instances

Typeable (* -> *) Poly_Fun

type Matrix_Int = Interpretation Mi_Fun Source

type Polynomial_Int = Interpretation Poly_Fun Source

data Interpretation f Source

Constructors

forall k a . (XmlContent k, XmlContent a, ToExotic a, Typeable a) => Interpretation
Fields mi_domain :: Domain mi_dim :: Integer mi_duration :: NominalDiffTime this is an extension mi_start :: UTCTime mi_end :: UTCTime mi_int :: [(k, f a)]

Instances

XmlContent Matrix_Int
XRead Matrix_Int
Typeable ((* -> ) -> ) Interpretation

data Domain Source

Constructors

Natural
Arctic
Arctic_Below_Zero
Tropical

Instances

Eq Domain
Ord Domain
Show Domain
XmlContent Domain
Pretty Domain
Typeable * Domain

data Red_Ord Source

Constructors

Red_Ord_Matrix_Int Matrix_Int
Red_Ord_Polynomial_Int Polynomial_Int
Red_Ord_Simple_Projection Simple_Projection
Red_Ord_Usable_Rules Usable_Rules

Instances

XmlContent Red_Ord
XRead Red_Ord
Typeable * Red_Ord

data Usable_Rules Source

Constructors

Usable_Rules [Identifier]

Instances

Pretty Usable_Rules
Typeable * Usable_Rules

data Simple_Projection Source

Constructors

Simple_Projection [(Identifier, Int)]

Instances

XmlContent Simple_Projection
Pretty Simple_Projection
XRead Simple_Projection
Typeable * Simple_Projection

data Claim Source

Constructors

Claim
Fields system :: TRS Identifier Identifier property :: Property

Instances

Typeable * Claim

data Proof Source

Constructors

Proof
Fields claim :: Claim reason :: Reason

Instances

XmlContent Proof
HTypeable Proof
XRead Proof
Typeable * Proof

data Property Source

Constructors

Termination
Top_Termination
Complexity (Function, Function)

Instances

Show Property
Pretty Property
Typeable * Property

data Function Source

see specification: http://termination-portal.org/wiki/Complexity

Constructors

Unknown
Polynomial
Fields degree :: Maybe Int
Exponential

Instances

Show Function
Pretty Function
Typeable * Function

data Reason Source

Constructors

Trivial
MannaNess Red_Ord Proof
MarkSymb Proof
DP Proof
Reverse Proof
As_TRS Proof
As_SRS Proof
SCC [Proof]	proposed extension
RFC Proof	experimental (not in Rainbow)
Undo_RFC Proof	experimental (not in Rainbow)
Bounded_Matrix_Interpretation Proof	TODO add more info

Instances

Typeable * Reason

data Over_Graph Source

Constructors

HDE
HDE_Marked

Instances

Show Over_Graph
XmlContent Over_Graph
Typeable * Over_Graph

data Marked a Source

Constructors

Hd_Mark a
Int_Mark a

Instances

Eq a => Eq (Marked a)
Ord a => Ord (Marked a)
(Typeable * a, XmlContent a) => XmlContent (Marked a)
(Typeable * a, XmlContent a) => XRead (Marked a)
Typeable (* -> *) Marked