{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable, OverloadedStrings, LambdaCase, DataKinds, GADTs, QuasiQuotes #-}

{-# OPTIONS_GHC -Werror=incomplete-patterns #-}

-- | from internal representation to XML, and back

module TPDB.CPF.Proof.Write where

import TPDB.CPF.Proof.Type as Type
import qualified TPDB.Data as T

import TPDB.Xml 
import Text.XML
import TPDB.Data.Xml
import Text.Hamlet.XML

import Data.List ( nub )
import Data.Char ( toLower )
import Data.Map (Map)
import qualified Data.Map as Map

import qualified Data.Text as T
import qualified Data.Time as T
import Control.Monad
import Data.Typeable
import Data.Ratio
import Data.String (fromString)

tox :: CertificationProblem -> Document 
tox :: CertificationProblem -> Document
tox CertificationProblem
p = 
    let style :: Instruction
style = Text -> Text -> Instruction
Instruction
          Text
"xml-stylesheet" Text
"type=\"text/xsl\" href=\"cpfHTML.xsl\""
        pro :: Prologue
pro = [Miscellaneous] -> Maybe Doctype -> [Miscellaneous] -> Prologue
Prologue [ Instruction -> Miscellaneous
MiscInstruction Instruction
style ] Maybe Doctype
forall a. Maybe a
Nothing []
        [ NodeElement Element
e ] = CertificationProblem -> [Node]
forall a. XmlContent a => a -> [Node]
toContents CertificationProblem
p
    in  Prologue -> Element -> [Miscellaneous] -> Document
Document Prologue
pro Element
e []

instance XmlContent CertificationProblem where
   parseContents :: Cursor -> [CertificationProblem]
parseContents = [Char] -> Cursor -> [CertificationProblem]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: CertificationProblem -> [Node]
toContents CertificationProblem
cp = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"certificationProblem"
         [ Name -> [Node] -> Node
mkel Name
"input" ([Node] -> Node) -> [Node] -> Node
forall a b. (a -> b) -> a -> b
$ CertificationProblemInput -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ( CertificationProblem -> CertificationProblemInput
input CertificationProblem
cp )
         , Name -> [Node] -> Node
mkel Name
"cpfVersion" [ Text -> Node
nospaceString (Text -> Node) -> Text -> Node
forall a b. (a -> b) -> a -> b
$ CertificationProblem -> Text
cpfVersion CertificationProblem
cp ]
         , Name -> [Node] -> Node
mkel Name
"proof" ([Node] -> Node) -> [Node] -> Node
forall a b. (a -> b) -> a -> b
$ Proof -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ( CertificationProblem -> Proof
proof CertificationProblem
cp )
         , Name -> [Node] -> Node
mkel Name
"origin" ([Node] -> Node) -> [Node] -> Node
forall a b. (a -> b) -> a -> b
$ Origin -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ( CertificationProblem -> Origin
origin CertificationProblem
cp )
         ]

instance XmlContent Origin where
   parseContents :: Cursor -> [Origin]
parseContents = [Char] -> Cursor -> [Origin]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Origin -> [Node]
toContents Origin
o = case Origin
o of
       ProofOrigin Tool
t -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"proofOrigin" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Tool -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Tool
t

instance XmlContent Tool where
   parseContents :: Cursor -> [Tool]
parseContents = [Char] -> Cursor -> [Tool]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Tool -> [Node]
toContents Tool
t = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"tool" 
         [ Name -> [Node] -> Node
mkel Name
"name"    [ Text -> Node
nospaceString (Text -> Node) -> Text -> Node
forall a b. (a -> b) -> a -> b
$ Tool -> Text
name    Tool
t ]
         , Name -> [Node] -> Node
mkel Name
"version" [ Text -> Node
nospaceString (Text -> Node) -> Text -> Node
forall a b. (a -> b) -> a -> b
$ Tool -> Text
version Tool
t ]
         ]

instance XmlContent CertificationProblemInput where
   parseContents :: Cursor -> [CertificationProblemInput]
parseContents = [Char] -> Cursor -> [CertificationProblemInput]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: CertificationProblemInput -> [Node]
toContents CertificationProblemInput
i = case CertificationProblemInput
i of
      TrsInput {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"trsInput" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (CertificationProblemInput -> Trs
trsinput_trs CertificationProblemInput
i )
      ComplexityInput {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"complexityInput" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"trsInput" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ CertificationProblemInput -> Trs
trsinput_trs CertificationProblemInput
i
          ]
      ACRewriteSystem {} -> [Char] -> [Node]
forall a. HasCallStack => [Char] -> a
error [Char]
"toContents ACRewriteSystem"    

instance XmlContent ( T.TRS Identifier Symbol ) where
   parseContents :: Cursor -> [Trs]
parseContents = [Char] -> Cursor -> [Trs]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Trs -> [Node]
toContents Trs
s = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"trs" 
       ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rules" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Node]] -> [Node]) -> [[Node]] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Rule (Term Identifier Symbol) -> [Node])
-> [Rule (Term Identifier Symbol)] -> [[Node]]
forall a b. (a -> b) -> [a] -> [b]
map Rule (Term Identifier Symbol) -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ([Rule (Term Identifier Symbol)] -> [[Node]])
-> [Rule (Term Identifier Symbol)] -> [[Node]]
forall a b. (a -> b) -> a -> b
$ Trs -> [Rule (Term Identifier Symbol)]
forall s r. RS s r -> [Rule r]
T.rules Trs
s

instance ( Typeable t, XmlContent t  ) 
        => XmlContent ( T.Rule t) where
   parseContents :: Cursor -> [Rule t]
parseContents = [Char] -> Cursor -> [Rule t]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Rule t -> [Node]
toContents Rule t
u = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rule" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"lhs" ( t -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (t -> [Node]) -> t -> [Node]
forall a b. (a -> b) -> a -> b
$ Rule t -> t
forall a. Rule a -> a
T.lhs Rule t
u )
      , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rhs" ( t -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (t -> [Node]) -> t -> [Node]
forall a b. (a -> b) -> a -> b
$ Rule t -> t
forall a. Rule a -> a
T.rhs Rule t
u )
      ]

instance XmlContent Proof where
   parseContents :: Cursor -> [Proof]
parseContents = [Char] -> Cursor -> [Proof]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Proof -> [Node]
toContents Proof
p = 
     let missing :: Name -> m Node
missing Name
t = Name -> [Node] -> m Node
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
t ([Node] -> m Node) -> [Node] -> m Node
forall a b. (a -> b) -> a -> b
$ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"missing-toContents-instance" [] 
     in  case Proof
p of
       TrsTerminationProof TrsTerminationProof 'Standard
p -> TrsTerminationProof 'Standard -> [Node]
forall a. XmlContent a => a -> [Node]
toContents TrsTerminationProof 'Standard
p
       TrsNonterminationProof TrsNonterminationProof 'Standard
p -> TrsNonterminationProof 'Standard -> [Node]
forall a. XmlContent a => a -> [Node]
toContents TrsNonterminationProof 'Standard
p
       RelativeTerminationProof TrsTerminationProof 'Relative
p -> TrsTerminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents TrsTerminationProof 'Relative
p
       RelativeNonterminationProof TrsNonterminationProof 'Relative
p -> TrsNonterminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents TrsNonterminationProof 'Relative
p
       ComplexityProof ComplexityProof
p -> Name -> [Node]
forall {m :: * -> *}. Monad m => Name -> m Node
missing Name
"ComplexityProof"
       ACTerminationProof ACTerminationProof
p -> Name -> [Node]
forall {m :: * -> *}. Monad m => Name -> m Node
missing Name
"ACTerminationProof"

instance XmlContent DPS where
   parseContents :: Cursor -> [DPS]
parseContents = [Char] -> Cursor -> [DPS]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: DPS -> [Node]
toContents ( DPS [Rule (Term Identifier Symbol)]
rules ) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"dps" 
        ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rules" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [Rule (Term Identifier Symbol)]
rules [Rule (Term Identifier Symbol)]
-> (Rule (Term Identifier Symbol) -> [Node]) -> [Node]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rule (Term Identifier Symbol) -> [Node]
forall a. XmlContent a => a -> [Node]
toContents

instance XmlContent (TrsTerminationProof Standard) where
   parseContents :: Cursor -> [TrsTerminationProof 'Standard]
parseContents = [Char] -> Cursor -> [TrsTerminationProof 'Standard]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: TrsTerminationProof 'Standard -> [Node]
toContents TrsTerminationProof 'Standard
p = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"trsTerminationProof" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ case TrsTerminationProof 'Standard
p of
      TrsTerminationProof 'Standard
RIsEmpty -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rIsEmpty" []
      DpTrans {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"dpTrans" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ DPS -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (DPS -> [Node]) -> DPS -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> DPS
dptrans_dps TrsTerminationProof 'Standard
p
          , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"markedSymbols" [ Text -> Node
nospaceString Text
"true" ]
          , DpProof -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (DpProof -> [Node]) -> DpProof -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> DpProof
dptrans_dpProof TrsTerminationProof 'Standard
p
          ]
      StringReversal {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"stringReversal" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Standard
p
          , TrsTerminationProof 'Standard -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Standard -> [Node])
-> TrsTerminationProof 'Standard -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> TrsTerminationProof 'Standard
forall (k :: Kind). TrsTerminationProof k -> TrsTerminationProof k
trsTerminationProof TrsTerminationProof 'Standard
p
          ]
      FlatContextClosure {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"flatContextClosure" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"flatContexts" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Context -> [Node]) -> [Context] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Context -> [Node]
forall a. XmlContent a => a -> [Node]
toContents
               ([Context] -> [Node]) -> [Context] -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> [Context]
forall (k :: Kind). TrsTerminationProof k -> [Context]
flatContexts TrsTerminationProof 'Standard
p
          , Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Standard
p
          , TrsTerminationProof 'Standard -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Standard -> [Node])
-> TrsTerminationProof 'Standard -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> TrsTerminationProof 'Standard
forall (k :: Kind). TrsTerminationProof k -> TrsTerminationProof k
trsTerminationProof TrsTerminationProof 'Standard
p
          ]
      Semlab {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"semlab" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Model -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Model -> [Node]) -> Model -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> Model
forall (k :: Kind). TrsTerminationProof k -> Model
model TrsTerminationProof 'Standard
p
          , Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Standard
p
          , TrsTerminationProof 'Standard -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Standard -> [Node])
-> TrsTerminationProof 'Standard -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> TrsTerminationProof 'Standard
forall (k :: Kind). TrsTerminationProof k -> TrsTerminationProof k
trsTerminationProof TrsTerminationProof 'Standard
p
          ]
      Split {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"split" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Standard
p
          , TrsTerminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Relative -> [Node])
-> TrsTerminationProof 'Relative -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> TrsTerminationProof 'Relative
forall (k :: Kind).
TrsTerminationProof k -> TrsTerminationProof 'Relative
remove TrsTerminationProof 'Standard
p
          , TrsTerminationProof 'Standard -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Standard -> [Node])
-> TrsTerminationProof 'Standard -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> TrsTerminationProof 'Standard
forall (k :: Kind). TrsTerminationProof k -> TrsTerminationProof k
remain TrsTerminationProof 'Standard
p
          ]
      RuleRemoval {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"ruleRemoval" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ OrderingConstraintProof -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (OrderingConstraintProof -> [Node])
-> OrderingConstraintProof -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> OrderingConstraintProof
forall (k :: Kind).
TrsTerminationProof k -> OrderingConstraintProof
rr_orderingConstraintProof TrsTerminationProof 'Standard
p
          , Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Standard
p
          , TrsTerminationProof 'Standard -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Standard -> [Node])
-> TrsTerminationProof 'Standard -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> TrsTerminationProof 'Standard
forall (k :: Kind). TrsTerminationProof k -> TrsTerminationProof k
trsTerminationProof TrsTerminationProof 'Standard
p
          ]
      Bounds {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"bounds" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"type" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Bounds_Type -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Bounds_Type -> [Node]) -> Bounds_Type -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> Bounds_Type
bounds_type TrsTerminationProof 'Standard
p
          , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"bound" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Int -> [Node]) -> Int -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> Int
bounds_bound TrsTerminationProof 'Standard
p 
          , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"finalStates" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
             ([[Node]] -> [Node]) -> [[Node]] -> [Node]
forall a b. (a -> b) -> a -> b
$ (State -> [Node]) -> [State] -> [[Node]]
forall a b. (a -> b) -> [a] -> [b]
map State -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ([State] -> [[Node]]) -> [State] -> [[Node]]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> [State]
bounds_finalStates TrsTerminationProof 'Standard
p
          , TreeAutomaton -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TreeAutomaton -> [Node]) -> TreeAutomaton -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> TreeAutomaton
bounds_closedTreeAutomaton TrsTerminationProof 'Standard
p
          , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"criterion" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Criterion -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Criterion -> [Node]) -> Criterion -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Standard -> Criterion
bounds_criterion TrsTerminationProof 'Standard
p
          ]

instance XmlContent (TrsTerminationProof Relative) where
   parseContents :: Cursor -> [TrsTerminationProof 'Relative]
parseContents = [Char] -> Cursor -> [TrsTerminationProof 'Relative]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: TrsTerminationProof 'Relative -> [Node]
toContents TrsTerminationProof 'Relative
p = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"relativeTerminationProof" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ case TrsTerminationProof 'Relative
p of
      TrsTerminationProof 'Relative
RIsEmpty -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rIsEmpty" []
      SIsEmpty {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"sIsEmpty" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ TrsTerminationProof 'Standard -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Standard -> [Node])
-> TrsTerminationProof 'Standard -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> TrsTerminationProof 'Standard
trsTerminationProof_Standard TrsTerminationProof 'Relative
p
          ]
      StringReversal {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"stringReversal" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ Trs -> Trs
forall {s} {r2}. RS s r2 -> RS s r2
standard (Trs -> Trs) -> Trs -> Trs
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Relative
p
          , Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ Trs -> Trs
forall {s} {r2}. RS s r2 -> RS s r2
relative (Trs -> Trs) -> Trs -> Trs
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Relative
p
          , TrsTerminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Relative -> [Node])
-> TrsTerminationProof 'Relative -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> TrsTerminationProof 'Relative
forall (k :: Kind). TrsTerminationProof k -> TrsTerminationProof k
trsTerminationProof TrsTerminationProof 'Relative
p
          ]
      FlatContextClosure {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"flatContextClosure" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"flatContexts" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Context -> [Node]) -> [Context] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Context -> [Node]
forall a. XmlContent a => a -> [Node]
toContents
               ([Context] -> [Node]) -> [Context] -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> [Context]
forall (k :: Kind). TrsTerminationProof k -> [Context]
flatContexts TrsTerminationProof 'Relative
p
          , Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ Trs -> Trs
forall {s} {r2}. RS s r2 -> RS s r2
standard (Trs -> Trs) -> Trs -> Trs
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Relative
p
          , Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ Trs -> Trs
forall {s} {r2}. RS s r2 -> RS s r2
relative (Trs -> Trs) -> Trs -> Trs
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Relative
p
          , TrsTerminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Relative -> [Node])
-> TrsTerminationProof 'Relative -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> TrsTerminationProof 'Relative
forall (k :: Kind). TrsTerminationProof k -> TrsTerminationProof k
trsTerminationProof TrsTerminationProof 'Relative
p
          ]
      Semlab {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"semlab" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Model -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Model -> [Node]) -> Model -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> Model
forall (k :: Kind). TrsTerminationProof k -> Model
model TrsTerminationProof 'Relative
p
          , Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ Trs -> Trs
forall {s} {r2}. RS s r2 -> RS s r2
standard (Trs -> Trs) -> Trs -> Trs
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Relative
p
          , Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ Trs -> Trs
forall {s} {r2}. RS s r2 -> RS s r2
relative (Trs -> Trs) -> Trs -> Trs
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Relative
p
          , TrsTerminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Relative -> [Node])
-> TrsTerminationProof 'Relative -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> TrsTerminationProof 'Relative
forall (k :: Kind). TrsTerminationProof k -> TrsTerminationProof k
trsTerminationProof TrsTerminationProof 'Relative
p
          ]
      RuleRemoval {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"ruleRemoval" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ OrderingConstraintProof -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (OrderingConstraintProof -> [Node])
-> OrderingConstraintProof -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> OrderingConstraintProof
forall (k :: Kind).
TrsTerminationProof k -> OrderingConstraintProof
rr_orderingConstraintProof TrsTerminationProof 'Relative
p
          , Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ Trs -> Trs
forall {s} {r2}. RS s r2 -> RS s r2
standard (Trs -> Trs) -> Trs -> Trs
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Relative
p
          , Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ Trs -> Trs
forall {s} {r2}. RS s r2 -> RS s r2
relative (Trs -> Trs) -> Trs -> Trs
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Relative
p
          , TrsTerminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Relative -> [Node])
-> TrsTerminationProof 'Relative -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> TrsTerminationProof 'Relative
forall (k :: Kind). TrsTerminationProof k -> TrsTerminationProof k
trsTerminationProof TrsTerminationProof 'Relative
p
          ]
      EqualityRemoval {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"equalityRemoval" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ TrsTerminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Relative -> [Node])
-> TrsTerminationProof 'Relative -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> TrsTerminationProof 'Relative
trsTerminationProof_Relative TrsTerminationProof 'Relative
p
          ]
      Split {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"split" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Trs -> [Node]) -> Trs -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> Trs
forall (k :: Kind). TrsTerminationProof k -> Trs
trs TrsTerminationProof 'Relative
p
          , TrsTerminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Relative -> [Node])
-> TrsTerminationProof 'Relative -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> TrsTerminationProof 'Relative
forall (k :: Kind).
TrsTerminationProof k -> TrsTerminationProof 'Relative
remove TrsTerminationProof 'Relative
p
          , TrsTerminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (TrsTerminationProof 'Relative -> [Node])
-> TrsTerminationProof 'Relative -> [Node]
forall a b. (a -> b) -> a -> b
$ TrsTerminationProof 'Relative -> TrsTerminationProof 'Relative
forall (k :: Kind). TrsTerminationProof k -> TrsTerminationProof k
remain TrsTerminationProof 'Relative
p
          ]

standard :: RS s r2 -> RS s r2
standard RS s r2
trs = RS s r2
trs RS s r2 -> [Rule r2] -> RS s r2
forall {s} {r1} {r2}. RS s r1 -> [Rule r2] -> RS s r2
`T.with_rules` (Rule r2 -> Bool) -> [Rule r2] -> [Rule r2]
forall a. (a -> Bool) -> [a] -> [a]
filter Rule r2 -> Bool
forall a. Rule a -> Bool
T.strict (RS s r2 -> [Rule r2]
forall s r. RS s r -> [Rule r]
T.rules RS s r2
trs)
relative :: RS s r2 -> RS s r2
relative RS s r2
trs = RS s r2
trs RS s r2 -> [Rule r2] -> RS s r2
forall {s} {r1} {r2}. RS s r1 -> [Rule r2] -> RS s r2
`T.with_rules` (Rule r2 -> Bool) -> [Rule r2] -> [Rule r2]
forall a. (a -> Bool) -> [a] -> [a]
filter Rule r2 -> Bool
forall a. Rule a -> Bool
T.weak   (RS s r2 -> [Rule r2]
forall s r. RS s r -> [Rule r]
T.rules RS s r2
trs)

symbolize :: RS Identifier (Term v Identifier) -> RS Symbol (Term v Symbol)
symbolize RS Identifier (Term v Identifier)
trs = 
    ( (Term v Identifier -> Term v Symbol)
-> RS Identifier (Term v Identifier)
-> RS Identifier (Term v Symbol)
forall a b. (a -> b) -> RS Identifier a -> RS Identifier b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Identifier -> Symbol) -> Term v Identifier -> Term v Symbol
forall {t} {s} {v}. (t -> s) -> Term v t -> Term v s
T.tmap Identifier -> Symbol
SymName) RS Identifier (Term v Identifier)
trs )
    { T.signature = map SymName $ T.signature trs }

instance XmlContent Bounds_Type where
  toContents :: Bounds_Type -> [Node]
toContents Bounds_Type
t = case Bounds_Type
t of
    Bounds_Type
Roof -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"roof" []
    Bounds_Type
Match -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"match" []

instance XmlContent State where
  toContents :: State -> [Node]
toContents (State Text
s) =
    Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"state"  [xml|#{fromString $ escape $ T.unpack s}|]

instance XmlContent Criterion where
  toContents :: Criterion -> [Node]
toContents Criterion
c = case Criterion
c of
    Criterion
Compatibility -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"compatibility" []

instance XmlContent TreeAutomaton where
  toContents :: TreeAutomaton -> [Node]
toContents TreeAutomaton
a = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"treeAutomaton" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"finalStates" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
       ([[Node]] -> [Node]) -> [[Node]] -> [Node]
forall a b. (a -> b) -> a -> b
$ (State -> [Node]) -> [State] -> [[Node]]
forall a b. (a -> b) -> [a] -> [b]
map State -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ([State] -> [[Node]]) -> [State] -> [[Node]]
forall a b. (a -> b) -> a -> b
$ TreeAutomaton -> [State]
ta_finalStates TreeAutomaton
a
    , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"transitions" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
       ([[Node]] -> [Node]) -> [[Node]] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Transition -> [Node]) -> [Transition] -> [[Node]]
forall a b. (a -> b) -> [a] -> [b]
map Transition -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ([Transition] -> [[Node]]) -> [Transition] -> [[Node]]
forall a b. (a -> b) -> a -> b
$ TreeAutomaton -> [Transition]
ta_transitions TreeAutomaton
a
    ]

instance XmlContent Transition where
  toContents :: Transition -> [Node]
toContents Transition
t = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"transition" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"lhs" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Transition_Lhs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Transition_Lhs -> [Node]) -> Transition_Lhs -> [Node]
forall a b. (a -> b) -> a -> b
$ Transition -> Transition_Lhs
transition_lhs Transition
t
    , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rhs" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ State -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (State -> [Node]) -> State -> [Node]
forall a b. (a -> b) -> a -> b
$ Transition -> State
transition_rhs Transition
t
    ]

instance XmlContent Transition_Lhs where
  toContents :: Transition_Lhs -> [Node]
toContents Transition_Lhs
s = case Transition_Lhs
s of
    Transition_Symbol {} -> [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Symbol -> [Node]) -> Symbol -> [Node]
forall a b. (a -> b) -> a -> b
$ Transition_Lhs -> Symbol
tr_symbol Transition_Lhs
s
      , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"height" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Int -> [Node]) -> Int -> [Node]
forall a b. (a -> b) -> a -> b
$ Transition_Lhs -> Int
tr_height Transition_Lhs
s
      , [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Node]] -> [Node]) -> [[Node]] -> [Node]
forall a b. (a -> b) -> a -> b
$ (State -> [Node]) -> [State] -> [[Node]]
forall a b. (a -> b) -> [a] -> [b]
map State -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ([State] -> [[Node]]) -> [State] -> [[Node]]
forall a b. (a -> b) -> a -> b
$ Transition_Lhs -> [State]
tr_arguments Transition_Lhs
s
      ]
    Transition_Epsilon State
s -> State -> [Node]
forall a. XmlContent a => a -> [Node]
toContents State
s

instance XmlContent Model where
  parseContents :: Cursor -> [Model]
parseContents = [Char] -> Cursor -> [Model]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

  toContents :: Model -> [Node]
toContents Model
model = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"model" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ case Model
model of
    FiniteModel Int
carrierSize [Interpret]
interprets ->
      Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"finiteModel" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"carrierSize"  ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Int
carrierSize
        , (Interpret -> [Node]) -> [Interpret] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Interpret -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [Interpret]
interprets
        ]
    Model
RootLabeling -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rootLabeling" []    

instance XmlContent DpProof where
  parseContents :: Cursor -> [DpProof]
parseContents = [Char] -> Cursor -> [DpProof]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

  toContents :: DpProof -> [Node]
toContents DpProof
p = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"dpProof" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ case DpProof
p of
    DpProof
PIsEmpty -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"pIsEmpty" []
    RedPairProc {} ->
      let name :: Name
name = case DpProof -> Maybe DPS
rppUsableRules DpProof
p of
            Maybe DPS
Nothing -> case DpProof -> Mono
rppMono DpProof
p of
              Mono
Weak -> Name
"redPairProc"; Mono
Strict -> Name
"monoRedPairProc"
            Just DPS
_ ->  case DpProof -> Mono
rppMono DpProof
p of
              Mono
Weak -> Name
"redPairUrProc"; Mono
Strict -> Name
"monoRedPairUrProc" 
      in  Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
name ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ OrderingConstraintProof -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (OrderingConstraintProof -> [Node])
-> OrderingConstraintProof -> [Node]
forall a b. (a -> b) -> a -> b
$ DpProof -> OrderingConstraintProof
rppOrderingConstraintProof DpProof
p
        , DPS -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (DPS -> [Node]) -> DPS -> [Node]
forall a b. (a -> b) -> a -> b
$ DpProof -> DPS
rppDps DpProof
p
        , case DpProof -> Maybe Trs
rppTrs DpProof
p of
            Maybe Trs
Nothing -> []
            Just Trs
sys -> Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Trs
sys
        , case DpProof -> Maybe DPS
rppUsableRules DpProof
p of
            Maybe DPS
Nothing -> []
            Just (DPS [Rule (Term Identifier Symbol)]
ur) -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"usableRules"
              ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rules" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Rule (Term Identifier Symbol) -> [Node])
-> [Rule (Term Identifier Symbol)] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Rule (Term Identifier Symbol) -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [Rule (Term Identifier Symbol)]
ur
        , DpProof -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (DpProof -> [Node]) -> DpProof -> [Node]
forall a b. (a -> b) -> a -> b
$ DpProof -> DpProof
rppDpProof DpProof
p
        ]
    DepGraphProc [DepGraphComponent]
cs -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"depGraphProc" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Node]] -> [Node]) -> [[Node]] -> [Node]
forall a b. (a -> b) -> a -> b
$ (DepGraphComponent -> [Node]) -> [DepGraphComponent] -> [[Node]]
forall a b. (a -> b) -> [a] -> [b]
map DepGraphComponent -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [DepGraphComponent]
cs

    SemLabProc {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"semlabProc" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ Model -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Model -> [Node]) -> Model -> [Node]
forall a b. (a -> b) -> a -> b
$ DpProof -> Model
slpModel DpProof
p
      , DPS -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (DPS -> [Node]) -> DPS -> [Node]
forall a b. (a -> b) -> a -> b
$ DpProof -> DPS
slpDps DpProof
p
      , case DpProof -> DPS
slpTrs DpProof
p of
          DPS [Rule (Term Identifier Symbol)]
rules -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"trs" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rules" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [Rule (Term Identifier Symbol)]
rules [Rule (Term Identifier Symbol)]
-> (Rule (Term Identifier Symbol) -> [Node]) -> [Node]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rule (Term Identifier Symbol) -> [Node]
forall a. XmlContent a => a -> [Node]
toContents

      , DpProof -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (DpProof -> [Node]) -> DpProof -> [Node]
forall a b. (a -> b) -> a -> b
$ DpProof -> DpProof
slpDpProof DpProof
p
      ]

    UnlabProc {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"unlabProc" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ DPS -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (DPS -> [Node]) -> DPS -> [Node]
forall a b. (a -> b) -> a -> b
$ DpProof -> DPS
ulpDps DpProof
p
      , case DpProof -> DPS
ulpTrs DpProof
p of
          DPS [Rule (Term Identifier Symbol)]
rules -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"trs" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rules" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [Rule (Term Identifier Symbol)]
rules [Rule (Term Identifier Symbol)]
-> (Rule (Term Identifier Symbol) -> [Node]) -> [Node]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rule (Term Identifier Symbol) -> [Node]
forall a. XmlContent a => a -> [Node]
toContents
      , DpProof -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (DpProof -> [Node]) -> DpProof -> [Node]
forall a b. (a -> b) -> a -> b
$ DpProof -> DpProof
ulpDpProof DpProof
p
      ]

instance XmlContent DepGraphComponent where
    toContents :: DepGraphComponent -> [Node]
toContents DepGraphComponent
dgc = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"component" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Node]] -> [Node]) -> [[Node]] -> [Node]
forall a b. (a -> b) -> a -> b
$
        [ {- rmkel "dps" $ -} DPS -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (DPS -> [Node]) -> DPS -> [Node]
forall a b. (a -> b) -> a -> b
$ DepGraphComponent -> DPS
dgcDps DepGraphComponent
dgc
        , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"realScc" 
           --  $ toContents $ dgcRealScc dgc
           -- NO, Bool is encoded as text, not as attribute
            ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Bool -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Bool -> [Node]) -> Bool -> [Node]
forall a b. (a -> b) -> a -> b
$ DepGraphComponent -> Bool
dgcRealScc DepGraphComponent
dgc 
        ] [[Node]] -> [[Node]] -> [[Node]]
forall a. [a] -> [a] -> [a]
++ 
        [ {- rmkel "dpProof" $ -} DpProof -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (DpProof -> [Node]) -> DpProof -> [Node]
forall a b. (a -> b) -> a -> b
$ DepGraphComponent -> DpProof
dgcDpProof DepGraphComponent
dgc
        | DepGraphComponent -> Bool
dgcRealScc DepGraphComponent
dgc
        ]

instance XmlContent OrderingConstraintProof where
  parseContents :: Cursor -> [OrderingConstraintProof]
parseContents = [Char] -> Cursor -> [OrderingConstraintProof]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

  toContents :: OrderingConstraintProof -> [Node]
toContents (OCPRedPair RedPair
rp) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"orderingConstraintProof" 
                             ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ RedPair -> [Node]
forall a. XmlContent a => a -> [Node]
toContents RedPair
rp
           
instance XmlContent RedPair where
  parseContents :: Cursor -> [RedPair]
parseContents = [Char] -> Cursor -> [RedPair]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

  toContents :: RedPair -> [Node]
toContents RedPair
rp = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"redPair" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ case RedPair
rp of
    RPInterpretation Interpretation
i -> Interpretation -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Interpretation
i
    RPPathOrder      PathOrder
o -> PathOrder -> [Node]
forall a. XmlContent a => a -> [Node]
toContents PathOrder
o

instance XmlContent Interpretation where
   parseContents :: Cursor -> [Interpretation]
parseContents = [Char] -> Cursor -> [Interpretation]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Interpretation -> [Node]
toContents Interpretation
i = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"interpretation" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$
        Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"type" ( Interpretation_Type -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Interpretation_Type -> [Node]) -> Interpretation_Type -> [Node]
forall a b. (a -> b) -> a -> b
$ Interpretation -> Interpretation_Type
interpretation_type Interpretation
i )
     [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ (Interpret -> [Node]) -> [Interpret] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Interpret -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ( Interpretation -> [Interpret]
interprets Interpretation
i )
      
instance XmlContent Interpretation_Type where
   parseContents :: Cursor -> [Interpretation_Type]
parseContents = [Char] -> Cursor -> [Interpretation_Type]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Interpretation_Type -> [Node]
toContents Interpretation_Type
t = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"matrixInterpretation" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat 
      [ Domain -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ( Interpretation_Type -> Domain
domain Interpretation_Type
t )
      , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"dimension"       ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Int -> [Node]) -> Int -> [Node]
forall a b. (a -> b) -> a -> b
$ Interpretation_Type -> Int
dimension Interpretation_Type
t 
      , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"strictDimension" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Int -> [Node]) -> Int -> [Node]
forall a b. (a -> b) -> a -> b
$ Interpretation_Type -> Int
strictDimension Interpretation_Type
t
      ]
     
instance XmlContent Domain where
   parseContents :: Cursor -> [Domain]
parseContents = [Char] -> Cursor -> [Domain]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Domain -> [Node]
toContents Domain
d = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"domain" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ case Domain
d of
       Domain
Naturals -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"naturals" []
       Rationals Rational
delta -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rationals" 
         ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"delta" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Rational -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Rational
delta
       Arctic Domain
d -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"arctic" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Domain -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Domain
d
       Tropical Domain
d -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel  Name
"tropical" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Domain -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Domain
d

instance XmlContent Rational where
    parseContents :: Cursor -> [Rational]
parseContents = [Char] -> Cursor -> [Rational]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

    toContents :: Rational -> [Node]
toContents Rational
r = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rational" 
        [ Name -> [Node] -> Node
mkel Name
"numerator"   ([Node] -> Node) -> [Node] -> Node
forall a b. (a -> b) -> a -> b
$ Integer -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Integer -> [Node]) -> Integer -> [Node]
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a. Ratio a -> a
numerator   Rational
r 
        , Name -> [Node] -> Node
mkel Name
"denominator" ([Node] -> Node) -> [Node] -> Node
forall a b. (a -> b) -> a -> b
$ Integer -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Integer -> [Node]) -> Integer -> [Node]
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r 
        ]

instance XmlContent Interpret  where
   parseContents :: Cursor -> [Interpret]
parseContents = [Char] -> Cursor -> [Interpret]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Interpret -> [Node]
toContents Interpret
i = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"interpret" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                    [ Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Symbol -> [Node]) -> Symbol -> [Node]
forall a b. (a -> b) -> a -> b
$ Interpret -> Symbol
symbol Interpret
i
                    , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"arity" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Int -> [Node]) -> Int -> [Node]
forall a b. (a -> b) -> a -> b
$ Interpret -> Int
arity Interpret
i 
                    , Value -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Value -> [Node]) -> Value -> [Node]
forall a b. (a -> b) -> a -> b
$ Interpret -> Value
value Interpret
i
                    ]

instance XmlContent Value where
   parseContents :: Cursor -> [Value]
parseContents = [Char] -> Cursor -> [Value]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Value -> [Node]
toContents Value
v = case Value
v of
      Polynomial Polynomial
p -> Polynomial -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Polynomial
p
      ArithFunction ArithFunction
f -> ArithFunction -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ArithFunction
f

instance XmlContent Polynomial where
   parseContents :: Cursor -> [Polynomial]
parseContents = [Char] -> Cursor -> [Polynomial]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Polynomial -> [Node]
toContents Polynomial
p = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"polynomial" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ case Polynomial
p of
       Sum     [Polynomial]
ps -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"sum"     ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ( (Polynomial -> [Node]) -> [Polynomial] -> [[Node]]
forall a b. (a -> b) -> [a] -> [b]
map Polynomial -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [Polynomial]
ps )
       Product [Polynomial]
ps -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"product" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ( (Polynomial -> [Node]) -> [Polynomial] -> [[Node]]
forall a b. (a -> b) -> [a] -> [b]
map Polynomial -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [Polynomial]
ps )
       Polynomial_Coefficient Coefficient
c -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"coefficient" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Coefficient -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Coefficient
c
       Polynomial_Variable Text
v -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"variable" [ Text -> Node
nospaceString Text
v ]

instance XmlContent ArithFunction where
  parseContents :: Cursor -> [ArithFunction]
parseContents = [Char] -> Cursor -> [ArithFunction]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

  toContents :: ArithFunction -> [Node]
toContents ArithFunction
af = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"arithFunction" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ case ArithFunction
af of
    AFNatural  Integer
n      -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"natural"  ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Integer -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Integer
n 
    AFVariable Integer
n      -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"variable" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Integer -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Integer
n 
    AFSum     [ArithFunction]
afs     -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"sum"      ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (ArithFunction -> [Node]) -> [ArithFunction] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ArithFunction -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [ArithFunction]
afs
    AFProduct [ArithFunction]
afs     -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"product"  ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (ArithFunction -> [Node]) -> [ArithFunction] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ArithFunction -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [ArithFunction]
afs
    AFMin     [ArithFunction]
afs     -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"min"      ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (ArithFunction -> [Node]) -> [ArithFunction] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ArithFunction -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [ArithFunction]
afs
    AFMax     [ArithFunction]
afs     -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"max"      ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (ArithFunction -> [Node]) -> [ArithFunction] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ArithFunction -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [ArithFunction]
afs
    AFIfEqual ArithFunction
a ArithFunction
b ArithFunction
t ArithFunction
f -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"ifEqual"  ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (ArithFunction -> [Node]) -> [ArithFunction] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ArithFunction -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [ArithFunction
a,ArithFunction
b,ArithFunction
t,ArithFunction
f]

instance XmlContent Coefficient where
   parseContents :: Cursor -> [Coefficient]
parseContents = [Char] -> Cursor -> [Coefficient]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

   toContents :: Coefficient -> [Node]
toContents Coefficient
v = case Coefficient
v of
       Matrix [Coefficient]
vs -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"matrix" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ( (Coefficient -> [Node]) -> [Coefficient] -> [[Node]]
forall a b. (a -> b) -> [a] -> [b]
map Coefficient -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [Coefficient]
vs )
       Vector [Coefficient]
cs -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"vector" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ( (Coefficient -> [Node]) -> [Coefficient] -> [[Node]]
forall a b. (a -> b) -> [a] -> [b]
map Coefficient -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [Coefficient]
cs )
       Coefficient_Coefficient a
i -> 
          Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"coefficient" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ a -> [Node]
forall a. XmlContent a => a -> [Node]
toContents a
i

instance XmlContent Exotic where
    parseContents :: Cursor -> [Exotic]
parseContents = [Char] -> Cursor -> [Exotic]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

    toContents :: Exotic -> [Node]
toContents Exotic
e = case Exotic
e of
       Exotic
Minus_Infinite -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"minusInfinity" []
       E_Integer Integer
i -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"integer" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Integer -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Integer
i
       E_Rational Rational
r -> {- rmkel "rational" $ -} Rational -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Rational
r
       Exotic
Plus_Infinite -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"plusInfinity" []

-- see remark in TPDB.Data.Xml (sharp_name_HACK)

instance XmlContent Symbol where
  parseContents :: Cursor -> [Symbol]
parseContents = [Char] -> Cursor -> [Symbol]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

  toContents :: Symbol -> [Node]
toContents (SymName Identifier
id) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"name" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Identifier -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Identifier
id
  toContents (SymSharp Symbol
sym) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"sharp" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Symbol
sym
  toContents (SymLabel Symbol
sym Label
label) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"labeledSymbol" 
                                  ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Symbol
sym [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ (Label -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Label
label)

instance XmlContent Label where
  parseContents :: Cursor -> [Label]
parseContents = [Char] -> Cursor -> [Label]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

  toContents :: Label -> [Node]
toContents (LblNumber [Integer]
is) = 
    Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"numberLabel" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Integer -> Node) -> [Integer] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\Integer
i -> Name -> [Node] -> Node
mkel Name
"number" ([Node] -> Node) -> [Node] -> Node
forall a b. (a -> b) -> a -> b
$ Integer -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Integer
i ) [Integer]
is

  toContents (LblSymbol [Symbol]
ss) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"symbolLabel" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Symbol -> [Node]) -> [Symbol] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [Symbol]
ss

instance XmlContent PathOrder where
  parseContents :: Cursor -> [PathOrder]
parseContents = [Char] -> Cursor -> [PathOrder]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

  toContents :: PathOrder -> [Node]
toContents (PathOrder [PrecedenceEntry]
ps [ArgumentFilterEntry]
as) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"pathOrder" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"statusPrecedence" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (PrecedenceEntry -> [Node]) -> [PrecedenceEntry] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PrecedenceEntry -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [PrecedenceEntry]
ps
    , if [ArgumentFilterEntry] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ArgumentFilterEntry]
as then []
      else Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"argumentFilter" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (ArgumentFilterEntry -> [Node]) -> [ArgumentFilterEntry] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ArgumentFilterEntry -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [ArgumentFilterEntry]
as
    ]

instance XmlContent PrecedenceEntry where
  parseContents :: Cursor -> [PrecedenceEntry]
parseContents = [Char] -> Cursor -> [PrecedenceEntry]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

  toContents :: PrecedenceEntry -> [Node]
toContents (PrecedenceEntry Symbol
s Int
a Integer
p) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"statusPrecedenceEntry" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Symbol
s
    , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"arity"      ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Int
a
    , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"precedence" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Integer -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Integer
p
    , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"lex"        [ ]
    ]

instance XmlContent ArgumentFilterEntry where
  parseContents :: Cursor -> [ArgumentFilterEntry]
parseContents = [Char] -> Cursor -> [ArgumentFilterEntry]
forall a. HasCallStack => [Char] -> a
error [Char]
"parseContents not implemented"

  toContents :: ArgumentFilterEntry -> [Node]
toContents (ArgumentFilterEntry Symbol
s Int
a Either Int [Int]
f) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"argumentFilterEntry" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Symbol
s
    , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"arity" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Int
a
    , case Either Int [Int]
f of 
        Left Int
i   -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"collapsing" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Int
i 
        Right [Int]
is -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"nonCollapsing" 
                  ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Int -> Node) -> [Int] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Name -> [Node] -> Node
mkel Name
"position" ([Node] -> Node) -> [Node] -> Node
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Int
i) [Int]
is
    ]

instance XmlContent (TrsNonterminationProof Standard) where
  toContents :: TrsNonterminationProof 'Standard -> [Node]
toContents TrsNonterminationProof 'Standard
tnp = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"trsNonterminationProof" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ case TrsNonterminationProof 'Standard
tnp of
    TrsNonterminationProof 'Standard
VariableConditionViolated -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"variableConditionViolated" []
    TNP_RuleRemoval Trs
sys TrsNonterminationProof 'Standard
sub -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"ruleRemoval"
      ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Trs
sys, TrsNonterminationProof 'Standard -> [Node]
forall a. XmlContent a => a -> [Node]
toContents TrsNonterminationProof 'Standard
sub ]
    TNP_StringReversal Trs
sys TrsNonterminationProof 'Standard
sub -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"stringReversal"
      ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Trs
sys , TrsNonterminationProof 'Standard -> [Node]
forall a. XmlContent a => a -> [Node]
toContents TrsNonterminationProof 'Standard
sub ]
    Loop {rewriteSequence :: forall (k :: Kind). TrsNonterminationProof k -> RewriteSequence
rewriteSequence = RewriteSequence
rs, substitution :: forall (k :: Kind). TrsNonterminationProof k -> Substitution
substitution = Substitution
sub, context :: forall (k :: Kind). TrsNonterminationProof k -> Context
context = Context
ctx } -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"loop"
        ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat  [ RewriteSequence -> [Node]
forall a. XmlContent a => a -> [Node]
toContents RewriteSequence
rs, Substitution -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Substitution
sub, Context -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Context
ctx ]

instance XmlContent (TrsNonterminationProof Relative) where
  toContents :: TrsNonterminationProof 'Relative -> [Node]
toContents TrsNonterminationProof 'Relative
tnp = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"relativeNonterminationProof" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ case TrsNonterminationProof 'Relative
tnp of
    TrsNonterminationProof 'Relative
VariableConditionViolated -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"variableConditionViolated" []
    TNP_RuleRemoval Trs
sys TrsNonterminationProof 'Relative
sub -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"ruleRemoval"
      ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Trs
sys, TrsNonterminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents TrsNonterminationProof 'Relative
sub ]
    TNP_StringReversal Trs
sys TrsNonterminationProof 'Relative
sub -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"stringReversal"
      ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Trs -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Trs
sys , TrsNonterminationProof 'Relative -> [Node]
forall a. XmlContent a => a -> [Node]
toContents TrsNonterminationProof 'Relative
sub ]
    Loop {rewriteSequence :: forall (k :: Kind). TrsNonterminationProof k -> RewriteSequence
rewriteSequence = RewriteSequence
rs, substitution :: forall (k :: Kind). TrsNonterminationProof k -> Substitution
substitution = Substitution
sub, context :: forall (k :: Kind). TrsNonterminationProof k -> Context
context = Context
ctx } -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"loop"
        ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat  [ RewriteSequence -> [Node]
forall a. XmlContent a => a -> [Node]
toContents RewriteSequence
rs, Substitution -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Substitution
sub, Context -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Context
ctx ]

instance XmlContent RewriteSequence where
  toContents :: RewriteSequence -> [Node]
toContents (RewriteSequence Term Identifier Symbol
start [RewriteStep]
steps) =
    Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rewriteSequence" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"startTerm" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Term Identifier Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Term Identifier Symbol
start 
      , (RewriteStep -> [Node]) -> [RewriteStep] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RewriteStep -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [RewriteStep]
steps
      ]

instance XmlContent RewriteStep where
  toContents :: RewriteStep -> [Node]
toContents RewriteStep
rs = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"rewriteStep" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"positionInTerm"
      ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Int -> [Node]) -> [Int] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ Int
k -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"position" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Int -> [Node]
forall a. XmlContent a => a -> [Node]
toContents Int
k ) ([Int] -> [Node]) -> [Int] -> [Node]
forall a b. (a -> b) -> a -> b
$ RewriteStep -> [Int]
rs_position RewriteStep
rs
    , Rule (Term Identifier Symbol) -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Rule (Term Identifier Symbol) -> [Node])
-> Rule (Term Identifier Symbol) -> [Node]
forall a b. (a -> b) -> a -> b
$ RewriteStep -> Rule (Term Identifier Symbol)
rs_rule RewriteStep
rs
    , case Rule (Term Identifier Symbol) -> Relation
forall a. Rule a -> Relation
T.relation (Rule (Term Identifier Symbol) -> Relation)
-> Rule (Term Identifier Symbol) -> Relation
forall a b. (a -> b) -> a -> b
$ RewriteStep -> Rule (Term Identifier Symbol)
rs_rule RewriteStep
rs of
        Relation
T.Strict -> []
        Relation
T.Weak -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"relative" []
        Relation
T.Equal -> [Char] -> [Node]
forall a. HasCallStack => [Char] -> a
error [Char]
"toContents for Equal rule"
    , Term Identifier Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Term Identifier Symbol -> [Node])
-> Term Identifier Symbol -> [Node]
forall a b. (a -> b) -> a -> b
$ RewriteStep -> Term Identifier Symbol
rs_term RewriteStep
rs
    ]

instance XmlContent Substitution where
  toContents :: Substitution -> [Node]
toContents (Substitution [SubstEntry]
ses) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"substitution" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (SubstEntry -> [Node]) -> [SubstEntry] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SubstEntry -> [Node]
forall a. XmlContent a => a -> [Node]
toContents [SubstEntry]
ses
instance XmlContent SubstEntry where
  toContents :: SubstEntry -> [Node]
toContents (SubstEntry Identifier
v Term Identifier Symbol
t) = Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"substEntry" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Term Identifier Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Term Identifier Symbol -> [Node])
-> Term Identifier Symbol -> [Node]
forall a b. (a -> b) -> a -> b
$ (Identifier -> Term Identifier Symbol
forall v s. v -> Term v s
T.Var Identifier
v :: T.Term Identifier Symbol)
    , Term Identifier Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Term Identifier Symbol -> [Node])
-> Term Identifier Symbol -> [Node]
forall a b. (a -> b) -> a -> b
$ Term Identifier Symbol
t
    ]

instance XmlContent Context where
  toContents :: Context -> [Node]
toContents Context
c = case Context
c of
    Context
Box -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"box" []
    FunContext {} -> Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"funContext" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [[Node]] -> [Node]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Symbol -> [Node]) -> Symbol -> [Node]
forall a b. (a -> b) -> a -> b
$ Context -> Symbol
fc_symbol Context
c
      , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"before" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Term Identifier Symbol -> [Node])
-> [Term Identifier Symbol] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term Identifier Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ([Term Identifier Symbol] -> [Node])
-> [Term Identifier Symbol] -> [Node]
forall a b. (a -> b) -> a -> b
$ Context -> [Term Identifier Symbol]
fc_before Context
c
      , Context -> [Node]
forall a. XmlContent a => a -> [Node]
toContents (Context -> [Node]) -> Context -> [Node]
forall a b. (a -> b) -> a -> b
$ Context -> Context
fc_here Context
c
      , Name -> [Node] -> [Node]
forall {m :: * -> *}. Monad m => Name -> [Node] -> m Node
rmkel Name
"after" ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ (Term Identifier Symbol -> [Node])
-> [Term Identifier Symbol] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term Identifier Symbol -> [Node]
forall a. XmlContent a => a -> [Node]
toContents ([Term Identifier Symbol] -> [Node])
-> [Term Identifier Symbol] -> [Node]
forall a b. (a -> b) -> a -> b
$ Context -> [Term Identifier Symbol]
fc_after Context
c
      ]