{-# language OverloadedStrings #-}
{-# language QuasiQuotes #-}

module TPDB.XTC.Write

( document
, writeFile, renderLBS, renderText, def
)

where

import qualified TPDB.Data as D
import qualified Data.Map as M

import qualified Data.Text as T
import qualified Text.XML as X
import Prelude hiding (writeFile)
import Text.XML (writeFile,renderLBS,renderText)
import Text.Hamlet.XML
import Data.Default (def)

document :: D.Problem D.Identifier D.Identifier -> X.Document
document :: Problem Identifier Identifier -> Document
document Problem Identifier Identifier
p = Prologue -> Element -> [Miscellaneous] -> Document
X.Document ([Miscellaneous] -> Maybe Doctype -> [Miscellaneous] -> Prologue
X.Prologue [] Maybe Doctype
forall a. Maybe a
Nothing []) Element
root [] where
    root :: Element
root = Name -> Map Name Text -> [Node] -> Element
X.Element Name
"problem"
      ([(Name, Text)] -> Map Name Text
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
"xmlns:xsi", Text
"http://www.w3.org/2001/XMLSchema-instance")
                  ,(Name
"type",Text
"termination")
                  ,(Name
"xsi:noNamespaceSchemaLocation",Text
"xtc.xsd")
                  ])
      [xml|
<trs>^{trs $ D.trs p}
$maybe s <- D.strategy p
  <strategy>^{strategy s}
|]

strategy :: Strategy -> [Node]
strategy Strategy
s = case Strategy
s of
  Strategy
D.Full -> [xml|FULL|]

trs :: D.TRS D.Identifier D.Identifier -> [X.Node]
trs :: TRS Identifier Identifier -> [Node]
trs TRS Identifier Identifier
rs = [xml|
<rules>
  $forall u <- D.strict_rules rs
    ^{rule u}
  $if not (null (D.weak_rules rs))
    <relrules>
      $forall u <- D.weak_rules rs
        ^{rule u}
<signature>
  $forall f <- D.signature rs
    <funcsym>
      <name>#{T.pack $ show f}
      <arity>#{T.pack $ show $ D.arity f}
|]

rule :: (Term Identifier Identifier, Term Identifier Identifier) -> [Node]
rule (Term Identifier Identifier
l,Term Identifier Identifier
r) = [xml|
<rule>
  <lhs>^{term l}
  <rhs>^{term r}
|]
  
term :: D.Term D.Identifier D.Identifier -> [X.Node]
term :: Term Identifier Identifier -> [Node]
term Term Identifier Identifier
t = case Term Identifier Identifier
t of
  D.Var Identifier
v -> [xml|
<var>#{T.pack $ show v}
|]
  D.Node Identifier
f [Term Identifier Identifier]
args -> [xml|
<funapp>
  <name>#{T.pack $ show f}
  $forall arg <- args
     <arg>^{term arg}
|]