diff --git a/src/TPDB/CPF/Proof/Read.hs b/src/TPDB/CPF/Proof/Read.hs --- a/src/TPDB/CPF/Proof/Read.hs +++ b/src/TPDB/CPF/Proof/Read.hs @@ -63,8 +63,8 @@ fromDoc :: Cursor -> [ CertificationProblem ] fromDoc = element1 "certificationProblem" >=> \ c -> ( CertificationProblem - <$> (c $/ element "input" &/ getInput ) - <*> (c $/ element "cpfVersion" &/ content ) + <$> (c $/ element "cpfVersion" &/ content ) + <*> (c $/ element "input" &/ getInput ) <*> (c $/ element "proof" &/ getProof) <*> (c $/ element "origin" >=> return [ignoredOrigin] ) ) diff --git a/src/TPDB/CPF/Proof/Type.hs b/src/TPDB/CPF/Proof/Type.hs --- a/src/TPDB/CPF/Proof/Type.hs +++ b/src/TPDB/CPF/Proof/Type.hs @@ -28,11 +28,30 @@ import GHC.Generics import Data.Hashable import Data.Kind +import Numeric.Natural import qualified Data.Text.Lazy as TL +cp :: CertificationProblem +cp = CertificationProblem + { cpfVersion = "3.4" + , input = TrsInput + { trsinput_trs = RS { rules = [ ru ] } + } + , proof = TrsTerminationProof RIsEmpty + , origin = ignoredOrigin + } + +ru = let a = SymName $ mk 0 "s" in Rule + { top = False + , relation = TPDB.Data.Strict + , lhs = Node a [] + , rhs = Node a [] + , original_variable = Nothing + } + data CertificationProblem = - CertificationProblem { input :: CertificationProblemInput - , cpfVersion :: Text + CertificationProblem { cpfVersion :: Text + , input :: CertificationProblemInput , proof :: Proof , origin :: Origin } @@ -156,7 +175,8 @@ SIsEmpty :: { trsTerminationProof_Standard :: !(TrsTerminationProof Standard) } -> TrsTerminationProof Relative RuleRemoval :: { rr_orderingConstraintProof :: !OrderingConstraintProof - , trs :: !Trs + , trs_deleted :: !Trs + , trs_remaining :: !Trs , trsTerminationProof :: !(TrsTerminationProof k) } -> TrsTerminationProof k EqualityRemoval :: { trsTerminationProof_Relative :: !(TrsTerminationProof Relative) @@ -272,7 +292,16 @@ Matrix_Interpretation { domain :: Domain, dimension :: Int , strictDimension :: Int } + | Core_Matrix_Interpretation + { domain :: Domain + , dimension :: Int + , indices :: [Natural] + , mode :: Mode + } deriving ( Typeable, Eq, Generic ) + +data Mode = E | M + deriving ( Typeable, Eq, Generic ) data Domain = Naturals | Rationals Rational diff --git a/src/TPDB/CPF/Proof/Write.hs b/src/TPDB/CPF/Proof/Write.hs --- a/src/TPDB/CPF/Proof/Write.hs +++ b/src/TPDB/CPF/Proof/Write.hs @@ -1,4 +1,4 @@ -{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable, OverloadedStrings, LambdaCase, DataKinds, GADTs, QuasiQuotes #-} +{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable, OverloadedStrings, LambdaCase, DataKinds, GADTs, QuasiQuotes, TypeApplications #-} {-# OPTIONS_GHC -Werror=incomplete-patterns #-} @@ -24,6 +24,7 @@ import Control.Monad import Data.Typeable import Data.Ratio +import Numeric.Natural import Data.String (fromString) tox :: CertificationProblem -> Document @@ -38,8 +39,11 @@ parseContents = error "parseContents not implemented" toContents cp = rmkel "certificationProblem" - [ mkel "input" $ toContents ( input cp ) - , mkel "cpfVersion" [ nospaceString $ cpfVersion cp ] + [ mkel "cpfVersion" [ nospaceString $ cpfVersion cp ] + , mkel "lookupTables" [] + , mkel "input" $ toContents ( input cp ) + , mkel "property" $ rmkel "termination" [] + , mkel "answer" $ rmkel "yes" [] -- FIXME (no?) , mkel "proof" $ toContents ( proof cp ) , mkel "origin" $ toContents ( origin cp ) ] @@ -79,8 +83,8 @@ parseContents = error "parseContents not implemented" toContents u = rmkel "rule" $ concat - [ rmkel "lhs" ( toContents $ T.lhs u ) - , rmkel "rhs" ( toContents $ T.rhs u ) + [ toContents $ T.lhs u + , toContents $ T.rhs u ] instance XmlContent Proof where @@ -134,7 +138,7 @@ ] RuleRemoval {} -> rmkel "ruleRemoval" $ concat [ toContents $ rr_orderingConstraintProof p - , toContents $ trs p + , toContents $ trs_deleted p , toContents $ trsTerminationProof p ] Bounds {} -> rmkel "bounds" $ concat @@ -297,13 +301,16 @@ instance XmlContent OrderingConstraintProof where parseContents = error "parseContents not implemented" - toContents (OCPRedPair rp) = rmkel "orderingConstraintProof" - $ toContents rp + toContents (OCPRedPair rp) = id + -- $ rmkel "orderingConstraintProof" + $ toContents rp instance XmlContent RedPair where parseContents = error "parseContents not implemented" - toContents rp = rmkel "redPair" $ case rp of + toContents rp = id + -- $ rmkel "redPair" + $ case rp of RPInterpretation i -> toContents i RPPathOrder o -> toContents o @@ -317,11 +324,23 @@ instance XmlContent Interpretation_Type where parseContents = error "parseContents not implemented" - toContents t = rmkel "matrixInterpretation" $ concat + toContents (t@Matrix_Interpretation {}) = rmkel "matrixInterpretation" $ concat [ toContents ( domain t ) , rmkel "dimension" $ toContents $ dimension t , rmkel "strictDimension" $ toContents $ strictDimension t ] + toContents (t@Core_Matrix_Interpretation {}) = rmkel "coreMatrixInterpretation" $ concat + [ toContents ( domain t ) + , rmkel "dimension" $ toContents $ dimension t + , rmkel "indices" $ concatMap toContents $ indices t + , toContents (mode t) + ] + +instance XmlContent Natural where + parseContents = error "parsecContents not implemented" + + toContents d = + rmkel "nat" $ toContents $ fromIntegral @Natural @Integer d instance XmlContent Domain where parseContents = error "parseContents not implemented" @@ -333,6 +352,13 @@ Arctic d -> rmkel "arctic" $ toContents d Tropical d -> rmkel "tropical" $ toContents d +instance XmlContent Mode where + parseContents = error "parseContents not implemented" + + toContents d = rmkel "mode" $ case d of + E -> rmkel "E" [] + M -> rmkel "M" [] + instance XmlContent Rational where parseContents = error "parseContents not implemented" @@ -360,10 +386,14 @@ instance XmlContent Polynomial where parseContents = error "parseContents not implemented" - toContents p = rmkel "polynomial" $ case p of + toContents p = id + -- $ rmkel "polynomial" + $ case p of Sum ps -> rmkel "sum" $ concat ( map toContents ps ) Product ps -> rmkel "product" $ concat ( map toContents ps ) - Polynomial_Coefficient c -> rmkel "coefficient" $ toContents c + Polynomial_Coefficient c -> id + -- $ rmkel "coefficient" + $ toContents c Polynomial_Variable v -> rmkel "variable" [ nospaceString v ] instance XmlContent ArithFunction where @@ -384,8 +414,9 @@ toContents v = case v of Matrix vs -> rmkel "matrix" $ concat ( map toContents vs ) Vector cs -> rmkel "vector" $ concat ( map toContents cs ) - Coefficient_Coefficient i -> - rmkel "coefficient" $ toContents i + Coefficient_Coefficient i -> id + -- $ rmkel "coefficient" + $ toContents i instance XmlContent Exotic where parseContents = error "parseContents not implemented" diff --git a/src/TPDB/Data/Xml.hs b/src/TPDB/Data/Xml.hs --- a/src/TPDB/Data/Xml.hs +++ b/src/TPDB/Data/Xml.hs @@ -53,7 +53,7 @@ [xml| ^{no_sharp_name_HACK ( toContents f )} $forall arg <- args - ^{toContents arg} + ^{toContents arg} |] @@ -73,8 +73,8 @@ => XmlContent ( Rule ( Term v c ) ) where toContents u = [xml| - ^{toContents $ lhs u} - ^{toContents $ rhs u} + ^{toContents $ lhs u} + ^{toContents $ rhs u} |] diff --git a/tpdb.cabal b/tpdb.cabal --- a/tpdb.cabal +++ b/tpdb.cabal @@ -1,7 +1,7 @@ Cabal-Version: 3.0 Name: tpdb -Version: 2.7.3 +Version: 2.8.0 Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann