module TPDB.Rainbow.Proof.Type
where
import TPDB.Data hiding ( Type (..))
import TPDB.Pretty
import TPDB.Plain.Write ()
import qualified TPDB.CPF.Proof.Type as C
import Text.XML.HaXml.XmlContent.Haskell hiding ( text )
import qualified Text.Parsec as P
import qualified Data.Time as T
import Data.Typeable
import Data.String (fromString)
data Vector a = Vector [ a ]
deriving Typeable
data Matrix a = Matrix [ Vector a ]
deriving Typeable
data MaxPlus = MinusInfinite | MaxPlusFinite Integer
deriving ( Show, Read, Typeable )
data MinPlus = MinPlusFinite Integer | PlusInfinite
deriving ( Show, Read, Typeable )
data Mi_Fun a =
Mi_Fun { mi_const :: Vector a
, mi_args :: [ Matrix a ]
}
deriving Typeable
data Poly_Fun a =
Poly_Fun { coefficients :: [a]
}
deriving Typeable
type Matrix_Int = Interpretation Mi_Fun
type Polynomial_Int = Interpretation Poly_Fun
data Interpretation f = forall k a
. ( XmlContent k, XmlContent a, C.ToExotic a, Typeable a )
=>
Interpretation { mi_domain :: Domain
, mi_dim :: Integer
, mi_duration :: T.NominalDiffTime
, mi_start :: T.UTCTime
, mi_end :: T.UTCTime
, mi_int :: [ (k , f a ) ]
} deriving Typeable
data Domain = Natural | Arctic | Arctic_Below_Zero | Tropical
deriving ( Show, Eq, Ord, Typeable )
instance Pretty Domain where pretty = fromString . show
instance Pretty T.NominalDiffTime where pretty = fromString . show
instance Pretty T.UTCTime where pretty = fromString . show
data Red_Ord
= Red_Ord_Matrix_Int Matrix_Int
| Red_Ord_Polynomial_Int Polynomial_Int
| Red_Ord_Simple_Projection Simple_Projection
| Red_Ord_Usable_Rules Usable_Rules
deriving Typeable
data Usable_Rules = Usable_Rules [ Identifier ]
deriving Typeable
instance Pretty Usable_Rules where
pretty (Usable_Rules sp) = "Usable_Rules" <+> pretty sp
data Simple_Projection = Simple_Projection [ ( Identifier, Int ) ]
deriving Typeable
instance Pretty Simple_Projection where
pretty (Simple_Projection sp) = "Simple_Projection" <+> pretty sp
data Claim =
Claim { system :: TRS Identifier Identifier
, property :: Property
}
deriving Typeable
data Proof =
Proof { claim :: Claim
, reason :: Reason
}
deriving Typeable
data Property
= Termination
| Top_Termination
| Complexity ( Function, Function )
deriving ( Typeable )
instance Show Property where show = render . pretty
instance Pretty Property where
pretty p = case p of
Termination -> "YES # Termination"
Top_Termination -> "YES # Top_Termination"
Complexity ( lo, hi ) -> "YES" <+> pretty ( lo, hi )
data Function
= Unknown
| Polynomial { degree :: Maybe Int }
| Exponential
deriving ( Typeable )
instance Show Function where show = render . pretty
instance Pretty Function where
pretty f = case f of
Unknown -> "?"
Polynomial { degree = Nothing } ->
"POLY"
Polynomial { degree = Just 0 } ->
"O(1)"
Polynomial { degree = Just d } ->
"O" <+> parens ( "n^" <> pretty d)
data Reason
= Trivial
| MannaNess Red_Ord Proof
| MarkSymb Proof
| DP Proof
| Reverse Proof
| As_TRS Proof
| As_SRS Proof
| SCC [ Proof ]
| RFC Proof
| Undo_RFC Proof
| Bounded_Matrix_Interpretation Proof
deriving Typeable
data Over_Graph = HDE | HDE_Marked
deriving ( Show, Typeable )
data Marked a = Hd_Mark a | Int_Mark a
deriving ( Eq, Ord, Typeable )
instance C.ToExotic Integer where
toExotic = C.E_Integer
instance C.ToExotic MaxPlus where
toExotic a = case a of
MinusInfinite -> C.Minus_Infinite
MaxPlusFinite f -> C.E_Integer f
instance C.ToExotic MinPlus where
toExotic a = case a of
MinPlusFinite f -> C.E_Integer f
PlusInfinite -> C.Plus_Infinite