search

jwaldmann / haskell-tpdb

parser and prettyprinter for TPDB syntax (termination problem data base)
2 stars 2 forks source link

CPF: add RelativeTerminationProof, use for Spilt transform, remove Unlabel #33

Open jwaldmann opened 2 years ago

jwaldmann commented 2 years ago

split transform: http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/0e6dfe9f5ac7/xml/cpf.xsd#l4053

intended application in standard termination proofs: https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/437#note_43678

of course it can also be used for certificates for relative termination.

Currently I have

data Proof = TrsTerminationProof TrsTerminationProof
           | ...
           | RelativeTerminationProof TrsTerminationProof

both using the same argument - because our TRS contains both strict and weak rules. Still they'd need to be printed separately for CPF, and it's best to make this distinction visible through types.

jwaldmann commented 2 years ago

the plan is

data Kind = Standard | Relative

data Proof = TrsTerminationProof (TrsTerminationProof Standard)
           | TrsNonterminationProof (TrsNonterminationProof Standard)
           | RelativeTerminationProof (TrsTerminationProof Relative)
           | RelativeNonterminationProof (TrsNonterminationProof Relative)
 ...

then proof constructors use a common name, but have distinct types (as GADTs)

data TrsTerminationProof (k :: Kind) where
  RIsEmpty :: TrsTerminationProof k
  SIsEmpty :: { trsTerminationProof_Standard :: TrsTerminationProof Standard }
    -> TrsTerminationProof Relative
  RuleRemoval :: { rr_orderingConstraintProof :: OrderingConstraintProof
                   , trs :: Trs
                   , trsTerminationProof :: TrsTerminationProof k
                   } -> TrsTerminationProof k