-- | 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 :: Identifier -> Doc ann
pretty Identifier
i = 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 ( Pretty v, Pretty s ) => Pretty ( Term v s ) where
    pretty :: Term v s -> Doc ann
pretty Term v s
t = case Term v s
t of
        Var v
v -> 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 a ann. Pretty a => a -> Doc ann
pretty s
f 
            [Term v s]
_  -> 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
pretty [Term v s]
xs )

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

instance PrettyTerm a => Pretty ( Rule a ) where
    pretty :: Rule a -> Doc ann
pretty Rule a
u = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
sep [ 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 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 :: [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 a ann. Pretty a => a -> Doc ann
pretty [s]
xs

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

instance ( Pretty s, PrettyTerm r, Variables (RS s r)
  , Pretty (Var (RS s r)))
  => Pretty ( RS s r ) where
    pretty :: RS s r -> Doc ann
pretty RS s r
sys = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat 
        [ 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
	  in if [Var (RS s r)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var (RS s r)]
vs
	     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
"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
pretty [Var (RS s r)]
vs)
	, 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
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 
               )
        -- FIXME: output strategy, theory
        ]

instance ( Pretty s, Pretty r, Variables (Term s r) ) => Pretty ( Problem s r ) where
    pretty :: Problem s r -> Doc ann
pretty Problem s r
p = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
       [ TRS s r -> Doc ann
forall a ann. Pretty a => a -> 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 
       , 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 ) ] 
       ]