-- | the "old" TPDB format 
-- cf. <http://www.lri.fr/~marche/tpdb/format.html>

{-# language FlexibleContexts #-}
{-# language OverloadedStrings #-}
{-# language UndecidableInstances #-}

module TPDB.Plain.Write where

import TPDB.Data
import TPDB.Pretty

import Data.List ( nub )
import Data.String ( fromString )
import qualified Data.Set as S
import qualified Data.Text as T

instance Pretty Identifier where
    pretty :: forall ann. Identifier -> Doc ann
pretty Identifier
i = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ Identifier -> Text
name Identifier
i

instance ( TermC v s, Pretty v, Pretty s ) => Pretty ( Term v s ) where
    pretty :: forall ann. Term v s -> Doc ann
pretty Term v s
t = case Term v s
t of
        Var v
v -> v -> Doc ann
forall ann. v -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty v
v
        Node s
f [Term v s]
xs -> case [Term v s]
xs of
            [] -> s -> Doc ann
forall ann. s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty s
f 
            [Term v s]
_  -> s -> Doc ann
forall ann. s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty s
f Doc ann -> Doc ann -> Doc ann
forall {ann}. Doc ann -> Doc ann -> Doc ann
<+> ( Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
fsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ (Term v s -> Doc ann) -> [Term v s] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term v s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term v s -> Doc ann
pretty [Term v s]
xs )

class PrettyTerm a where 
    prettyTerm :: a -> Doc ann

instance PrettyTerm a => Pretty ( Rule a ) where
    pretty :: forall ann. Rule a -> Doc ann
pretty Rule a
u = [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
sep [ a -> Doc ann
forall ann. a -> Doc ann
forall a ann. PrettyTerm a => a -> Doc ann
prettyTerm (a -> Doc ann) -> a -> Doc ann
forall a b. (a -> b) -> a -> b
$ Rule a -> a
forall a. Rule a -> a
lhs Rule a
u
                   , ( case Rule a -> Relation
forall a. Rule a -> Relation
relation Rule a
u of 
                         Relation
Strict -> Doc ann
"->" 
                         Relation
Weak -> Doc ann
"->="
                         Relation
Equal -> Doc ann
"=" 
                   -- FIXME: implement "top" annotation
                     ) Doc ann -> Doc ann -> Doc ann
forall {ann}. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. PrettyTerm a => a -> Doc ann
prettyTerm ( Rule a -> a
forall a. Rule a -> a
rhs Rule a
u )
                   ]

instance Pretty s => PrettyTerm [s] where    
    prettyTerm :: forall ann. [s] -> Doc ann
prettyTerm [s]
xs = [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (s -> Doc ann) -> [s] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map s -> Doc ann
forall ann. s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [s]
xs

instance ( TermC v s, Pretty v, Pretty s ) => PrettyTerm ( Term v s ) where
    prettyTerm :: forall ann. Term v s -> Doc ann
prettyTerm = Term v s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term v s -> Doc ann
pretty

instance ( Pretty s, PrettyTerm r, Variables (RS s r)
  , Pretty (Var (RS s r)))
  => Pretty ( RS s r ) where
    pretty :: forall ann. RS s r -> Doc ann
pretty RS s r
sys =
      let vs :: [Var (RS s r)]
vs = Set (Var (RS s r)) -> [Var (RS s r)]
forall a. Set a -> [a]
S.toList (Set (Var (RS s r)) -> [Var (RS s r)])
-> Set (Var (RS s r)) -> [Var (RS s r)]
forall a b. (a -> b) -> a -> b
$ RS s r -> Set (Var (RS s r))
forall t. Variables t => t -> Set (Var t)
variables RS s r
sys
          vars :: Doc ann
vars = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"VAR" Doc ann -> Doc ann -> Doc ann
forall {ann}. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
vcat ((Var (RS s r) -> Doc ann) -> [Var (RS s r)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Var (RS s r) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Var (RS s r) -> Doc ann
pretty [Var (RS s r)]
vs)
          ruls :: Doc ann
ruls = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"RULES" Doc ann -> Doc ann -> Doc ann
forall {ann}. Doc ann -> Doc ann -> Doc ann
<+>
            [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
vcat ( ( if RS s r -> Bool
forall s r. RS s r -> Bool
separate RS s r
sys then Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma else [Doc ann] -> [Doc ann]
forall a. a -> a
id )
                 ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ (Rule r -> Doc ann) -> [Rule r] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Rule r -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Rule r -> Doc ann
pretty ([Rule r] -> [Doc ann]) -> [Rule r] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ RS s r -> [Rule r]
forall s r. RS s r -> [Rule r]
rules RS s r
sys 
                 )
      in  if [Var (RS s r)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var (RS s r)]
vs then Doc ann
forall ann. Doc ann
ruls else [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
vcat [Doc ann
forall ann. Doc ann
vars, Doc ann
forall ann. Doc ann
ruls]
        -- FIXME: output strategy, theory

instance ( TermC s r, Pretty s, Pretty r, Variables (Term s r) ) => Pretty ( Problem s r ) where
    pretty :: forall ann. Problem s r -> Doc ann
pretty Problem s r
p =
      let rms :: [Doc ann]
rms = case Problem s r -> Signature
forall v s. Problem v s -> Signature
full_signature Problem s r
p of
            Signature
HigherOrderSignature -> []
            Signature [Funcsym]
fs -> do
              Funcsym
f <- [Funcsym]
fs
              case Funcsym -> Maybe Replacementmap
fs_replacementmap Funcsym
f of
                Maybe Replacementmap
Nothing -> []
                Just (Replacementmap [Int]
ps) ->
                  Doc ann -> [Doc ann]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc ann -> [Doc ann]) -> Doc ann -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
sep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Funcsym -> Text
fs_name Funcsym
f) Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Int -> Doc ann) -> [Int] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Int]
ps
      in  [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
vcat
       [ TRS s r -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TRS s r -> Doc ann
pretty (TRS s r -> Doc ann) -> TRS s r -> Doc ann
forall a b. (a -> b) -> a -> b
$ Problem s r -> TRS s r
forall v s. Problem v s -> TRS v s
trs Problem s r
p
       , if [Doc Any] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc Any]
forall {ann}. [Doc ann]
rms then Doc ann
forall ann. Doc ann
empty
         else Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
sep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"STRATEGY" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: Doc ann
"CONTEXTSENSITIVE" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: [Doc ann]
forall {ann}. [Doc ann]
rms
       , case Problem s r -> Maybe Strategy
forall v s. Problem v s -> Maybe Strategy
strategy Problem s r
p of  
             Maybe Strategy
Nothing -> Doc ann
forall ann. Doc ann
empty
             Just Strategy
s -> [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
sep [ Doc ann
"strategy"
                            , String -> Doc ann
forall a. IsString a => String -> a
fromString ( Strategy -> String
forall a. Show a => a -> String
show Strategy
s ) ]
       , case Problem s r -> Maybe Startterm
forall v s. Problem v s -> Maybe Startterm
startterm Problem s r
p of  
             Maybe Startterm
Nothing -> Doc ann
forall ann. Doc ann
empty
             Just Startterm
s -> [Doc ann] -> Doc ann
forall {ann}. [Doc ann] -> Doc ann
sep [ Doc ann
"startterm"
                            , String -> Doc ann
forall a. IsString a => String -> a
fromString ( Startterm -> String
forall a. Show a => a -> String
show Startterm
s ) ] 
       ]