tpdb 2.7.3 → 2.8.0
raw patch · 5 files changed
+83/−23 lines, 5 files
Files
- src/TPDB/CPF/Proof/Read.hs +2/−2
- src/TPDB/CPF/Proof/Type.hs +32/−3
- src/TPDB/CPF/Proof/Write.hs +45/−14
- src/TPDB/Data/Xml.hs +3/−3
- tpdb.cabal +1/−1
src/TPDB/CPF/Proof/Read.hs view
@@ -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] ) )
src/TPDB/CPF/Proof/Type.hs view
@@ -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
src/TPDB/CPF/Proof/Write.hs view
@@ -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"
src/TPDB/Data/Xml.hs view
@@ -53,7 +53,7 @@ [xml|<funapp> ^{no_sharp_name_HACK ( toContents f )} $forall arg <- args- <arg>^{toContents arg}+ ^{toContents arg} |] @@ -73,8 +73,8 @@ => XmlContent ( Rule ( Term v c ) ) where toContents u = [xml|<rule>- <lhs>^{toContents $ lhs u}- <rhs>^{toContents $ rhs u}+ ^{toContents $ lhs u}+ ^{toContents $ rhs u} |]
tpdb.cabal view
@@ -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