tpdb-0.8.2: Data Type for Rewriting Systems

Safe HaskellNone

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

data Matrix a Source

Constructors

Matrix [Vector a] 

Instances

data Poly_Fun a Source

Constructors

Poly_Fun 

Fields

coefficients :: [a]
 

Instances

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)]
 

data Claim Source

Constructors

Claim 

Instances

data Function Source

see specification: http:termination-portal.orgwikiComplexity

Constructors

Unknown 
Polynomial 

Fields

degree :: Maybe Int
 
Exponential 

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

data Marked a Source

Constructors

Hd_Mark a 
Int_Mark a 

Instances

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