-- This file is part of the 'term-rewriting' library. It is licensed
-- under an MIT license. See the accompanying 'LICENSE' file for details.
--
-- Authors: Martin Avanzini

module Data.Rewriting.Problem.Pretty (
    prettyProblem,
    prettyWST,
    prettyWST',
) where

import Data.Maybe (isJust, fromJust)
import Data.List (nub)
import Data.Rewriting.Problem.Type
import Data.Rewriting.Rule (prettyRule)
import Text.PrettyPrint.ANSI.Leijen

printWhen :: Bool -> Doc -> Doc
printWhen :: Bool -> Doc -> Doc
printWhen Bool
False Doc
_ = Doc
empty
printWhen Bool
True  Doc
p = Doc
p


prettyWST' :: (Pretty f, Pretty v) => Problem f v -> Doc
prettyWST' :: forall f v. (Pretty f, Pretty v) => Problem f v -> Doc
prettyWST' = (f -> Doc) -> (v -> Doc) -> Problem f v -> Doc
forall f v. (f -> Doc) -> (v -> Doc) -> Problem f v -> Doc
prettyWST f -> Doc
forall a. Pretty a => a -> Doc
pretty v -> Doc
forall a. Pretty a => a -> Doc
pretty

prettyWST :: (f -> Doc) -> (v -> Doc) -> Problem f v -> Doc
prettyWST :: forall f v. (f -> Doc) -> (v -> Doc) -> Problem f v -> Doc
prettyWST f -> Doc
fun v -> Doc
var Problem f v
prob =
    Bool -> Doc -> Doc
printWhen (StartTerms
sterms StartTerms -> StartTerms -> Bool
forall a. Eq a => a -> a -> Bool
/= StartTerms
AllTerms) (String -> Doc -> Doc
block String
"STARTTERM" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"CONSTRUCTOR-BASED")
    Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Bool -> Doc -> Doc
printWhen (Strategy
strat Strategy -> Strategy -> Bool
forall a. Eq a => a -> a -> Bool
/= Strategy
Full) (String -> Doc -> Doc
block String
"STRATEGY" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Strategy -> Doc
ppStrat Strategy
strat)
    Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String
-> (Problem f v -> Maybe [Theory f v])
-> ([Theory f v] -> Doc)
-> Doc
forall {t}. String -> (Problem f v -> Maybe t) -> (t -> Doc) -> Doc
maybeblock String
"THEORY" Problem f v -> Maybe [Theory f v]
forall f v. Problem f v -> Maybe [Theory f v]
theory [Theory f v] -> Doc
ppTheories
    Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc -> Doc
block String
"VAR" ([v] -> Doc
ppVars ([v] -> Doc) -> [v] -> Doc
forall a b. (a -> b) -> a -> b
$ Problem f v -> [v]
forall f v. Problem f v -> [v]
variables Problem f v
prob)
    Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String
-> (Problem f v -> Maybe [(f, Int)]) -> ([(f, Int)] -> Doc) -> Doc
forall {t}. String -> (Problem f v -> Maybe t) -> (t -> Doc) -> Doc
maybeblock String
"SIG" Problem f v -> Maybe [(f, Int)]
forall f v. Problem f v -> Maybe [(f, Int)]
signature [(f, Int)] -> Doc
ppSignature
    Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc -> Doc
block String
"RULES" (RulesPair f v -> Doc
ppRules (RulesPair f v -> Doc) -> RulesPair f v -> Doc
forall a b. (a -> b) -> a -> b
$ Problem f v -> RulesPair f v
forall f v. Problem f v -> RulesPair f v
rules Problem f v
prob)
    Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> (Problem f v -> Maybe String) -> (String -> Doc) -> Doc
forall {t}. String -> (Problem f v -> Maybe t) -> (t -> Doc) -> Doc
maybeblock String
"COMMENT" Problem f v -> Maybe String
forall f v. Problem f v -> Maybe String
comment String -> Doc
text

  where block :: String -> Doc -> Doc
block String
n Doc
pp = (Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Int -> Doc -> Doc
hang Int
3 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
n Doc -> Doc -> Doc
<$$> Doc
pp) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
linebreak) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
linebreak
        maybeblock :: String -> (Problem f v -> Maybe t) -> (t -> Doc) -> Doc
maybeblock String
n Problem f v -> Maybe t
f t -> Doc
fpp = case Problem f v -> Maybe t
f Problem f v
prob of
                               Just t
e -> String -> Doc -> Doc
block String
n (t -> Doc
fpp t
e)
                               Maybe t
Nothing -> Doc
empty

        ppStrat :: Strategy -> Doc
ppStrat Strategy
Innermost = String -> Doc
text String
"INNERMOST"
        ppStrat Strategy
Outermost = String -> Doc
text String
"OUTERMOST"

        ppVars :: [v] -> Doc
ppVars [v]
vs = Doc -> Doc
align (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fillSep [ v -> Doc
var v
v | v
v <- [v]
vs]

        ppTheories :: [Theory f v] -> Doc
ppTheories [Theory f v]
thys = Doc -> Doc
align (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [Theory f v -> Doc
ppThy Theory f v
thy | Theory f v
thy <- [Theory f v]
thys]
            where ppThy :: Theory f v -> Doc
ppThy (SymbolProperty String
p [f]
fs) = String -> Doc -> Doc
block String
p (Doc -> Doc
align (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fillSep [ f -> Doc
fun f
f | f
f <- [f]
fs ])
                  ppThy (Equations [Rule f v]
rs)        = String -> Doc -> Doc
block String
"EQUATIONS" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [String -> Rule f v -> Doc
ppRule String
"==" Rule f v
r | Rule f v
r <- [Rule f v]
rs]

        ppSignature :: [(f, Int)] -> Doc
ppSignature [(f, Int)]
sigs = Doc -> Doc
align (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fillSep [(f, Int) -> Doc
ppSig (f, Int)
sig | (f, Int)
sig <- [(f, Int)]
sigs]
            where ppSig :: (f, Int) -> Doc
ppSig (f
f,Int
i) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ f -> Doc
fun f
f Doc -> Doc -> Doc
<+> Int -> Doc
int Int
i

        ppRules :: RulesPair f v -> Doc
ppRules RulesPair f v
rp = Doc -> Doc
align (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([String -> Rule f v -> Doc
ppRule String
"->" Rule f v
r | Rule f v
r <- RulesPair f v -> [Rule f v]
forall f v. RulesPair f v -> [Rule f v]
strictRules RulesPair f v
rp]
                                   [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Rule f v -> Doc
ppRule String
"->=" Rule f v
r | Rule f v
r <- RulesPair f v -> [Rule f v]
forall f v. RulesPair f v -> [Rule f v]
weakRules RulesPair f v
rp])

        ppRule :: String -> Rule f v -> Doc
ppRule String
sep = Doc -> (f -> Doc) -> (v -> Doc) -> Rule f v -> Doc
forall f v. Doc -> (f -> Doc) -> (v -> Doc) -> Rule f v -> Doc
prettyRule (String -> Doc
text String
sep) f -> Doc
fun v -> Doc
var

        sterms :: StartTerms
sterms = Problem f v -> StartTerms
forall f v. Problem f v -> StartTerms
startTerms Problem f v
prob
        strat :: Strategy
strat  = Problem f v -> Strategy
forall f v. Problem f v -> Strategy
strategy Problem f v
prob
        thry :: Maybe [Theory f v]
thry   = Problem f v -> Maybe [Theory f v]
forall f v. Problem f v -> Maybe [Theory f v]
theory Problem f v
prob


prettyProblem :: (Eq f, Eq v) => (f -> Doc) -> (v -> Doc) -> Problem f v -> Doc
prettyProblem :: forall f v.
(Eq f, Eq v) =>
(f -> Doc) -> (v -> Doc) -> Problem f v -> Doc
prettyProblem f -> Doc
fun v -> Doc
var Problem f v
prob =  String -> Doc -> Doc
block String
"Start-Terms" (StartTerms -> Doc
ppST (StartTerms -> Doc) -> (Problem f v -> StartTerms) -> Doc
forall {a} {b}. (a -> b) -> (Problem f v -> a) -> b
`on` Problem f v -> StartTerms
forall f v. Problem f v -> StartTerms
startTerms)
                              Doc -> Doc -> Doc
<$$> String -> Doc -> Doc
block String
"Strategy" (Strategy -> Doc
ppStrat (Strategy -> Doc) -> (Problem f v -> Strategy) -> Doc
forall {a} {b}. (a -> b) -> (Problem f v -> a) -> b
`on` Problem f v -> Strategy
forall f v. Problem f v -> Strategy
strategy)
                              Doc -> Doc -> Doc
<$$> String -> Doc -> Doc
block String
"Variables" ([v] -> Doc
ppVars ([v] -> Doc) -> (Problem f v -> [v]) -> Doc
forall {a} {b}. (a -> b) -> (Problem f v -> a) -> b
`on` Problem f v -> [v]
forall f v. Problem f v -> [v]
variables)
                              Doc -> Doc -> Doc
<$$> String -> Doc -> Doc
block String
"Function Symbols" ([f] -> Doc
ppSyms ([f] -> Doc) -> (Problem f v -> [f]) -> Doc
forall {a} {b}. (a -> b) -> (Problem f v -> a) -> b
`on` Problem f v -> [f]
forall f v. Problem f v -> [f]
symbols)
                              Doc -> Doc -> Doc
<$$> String
-> ([Theory f v] -> Doc)
-> (Problem f v -> Maybe [Theory f v])
-> Doc
forall {a}. String -> (a -> Doc) -> (Problem f v -> Maybe a) -> Doc
maybeblock String
"Theory" [Theory f v] -> Doc
ppTheories Problem f v -> Maybe [Theory f v]
forall f v. Problem f v -> Maybe [Theory f v]
theory
                              Doc -> Doc -> Doc
<$$> String -> Doc -> Doc
block String
"Rules" (RulesPair f v -> Doc
ppRules (RulesPair f v -> Doc) -> (Problem f v -> RulesPair f v) -> Doc
forall {a} {b}. (a -> b) -> (Problem f v -> a) -> b
`on` Problem f v -> RulesPair f v
forall f v. Problem f v -> RulesPair f v
rules)
                              Doc -> Doc -> Doc
<$$> String -> (String -> Doc) -> (Problem f v -> Maybe String) -> Doc
forall {a}. String -> (a -> Doc) -> (Problem f v -> Maybe a) -> Doc
maybeblock String
"Comment" String -> Doc
ppComment Problem f v -> Maybe String
forall f v. Problem f v -> Maybe String
comment where
  a -> b
pp on :: (a -> b) -> (Problem f v -> a) -> b
`on` Problem f v -> a
fld = a -> b
pp (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Problem f v -> a
fld Problem f v
prob
  block :: String -> Doc -> Doc
block String
n Doc
pp = Int -> Doc -> Doc
hang Int
3 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc -> Doc
underline (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":") Doc -> Doc -> Doc
<+> Doc
pp
  maybeblock :: String -> (a -> Doc) -> (Problem f v -> Maybe a) -> Doc
maybeblock String
n a -> Doc
pp Problem f v -> Maybe a
f = Bool -> Doc -> Doc
printWhen (Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (Maybe a -> Bool) -> (Problem f v -> Maybe a) -> Bool
forall {a} {b}. (a -> b) -> (Problem f v -> a) -> b
`on` Problem f v -> Maybe a
f) (String -> Doc -> Doc
block String
n (a -> Doc
pp (a -> Doc) -> (Problem f v -> a) -> Doc
forall {a} {b}. (a -> b) -> (Problem f v -> a) -> b
`on` (Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe a -> a) -> (Problem f v -> Maybe a) -> Problem f v -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Problem f v -> Maybe a
f)))
  commalist :: [Doc] -> Doc
commalist  = [Doc] -> Doc
fillSep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
",")

  ppST :: StartTerms -> Doc
ppST StartTerms
AllTerms      = String -> Doc
text String
"all"
  ppST StartTerms
BasicTerms    = String -> Doc
text String
"basic terms"
  ppStrat :: Strategy -> Doc
ppStrat Strategy
Innermost  = String -> Doc
text String
"innermost"
  ppStrat Strategy
Outermost  = String -> Doc
text String
"outermost"
  ppStrat Strategy
Full       = String -> Doc
text String
"full rewriting"
  ppVars :: [v] -> Doc
ppVars [v]
vars        = [Doc] -> Doc
commalist ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [v -> Doc
var v
v | v
v <- [v] -> [v]
forall a. Eq a => [a] -> [a]
nub [v]
vars]
  ppSyms :: [f] -> Doc
ppSyms [f]
syms        = [Doc] -> Doc
commalist ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [f -> Doc
fun f
v | f
v <- [f] -> [f]
forall a. Eq a => [a] -> [a]
nub [f]
syms]
  ppComment :: String -> Doc
ppComment String
c        = String -> Doc
text String
c
  ppTheories :: [Theory f v] -> Doc
ppTheories [Theory f v]
ths     =  Doc -> Doc
align (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [ Theory f v -> Doc
ppTheory Theory f v
th | Theory f v
th <- [Theory f v]
ths ] where
      ppTheory :: Theory f v -> Doc
ppTheory (SymbolProperty String
p [f]
fs) = String -> Doc
text (String
pString -> String -> String
forall a. [a] -> [a] -> [a]
++String
":") Doc -> Doc -> Doc
<+> Doc -> Doc
align ([Doc] -> Doc
commalist [ f -> Doc
fun f
f | f
f <- [f]
fs])
      ppTheory (Equations [Rule f v]
rs)        = Doc -> Doc
align (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [String -> Rule f v -> Doc
ppRule String
"==" Rule f v
r | Rule f v
r <- [Rule f v]
rs]
  ppRules :: RulesPair f v -> Doc
ppRules RulesPair f v
rp         = Doc -> Doc
align (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
                       [String -> Rule f v -> Doc
ppRule String
"->" Rule f v
r | Rule f v
r <- RulesPair f v -> [Rule f v]
forall f v. RulesPair f v -> [Rule f v]
strictRules RulesPair f v
rp]
                       [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Rule f v -> Doc
ppRule String
"->=" Rule f v
r | Rule f v
r <- RulesPair f v -> [Rule f v]
forall f v. RulesPair f v -> [Rule f v]
weakRules RulesPair f v
rp]
  ppRule :: String -> Rule f v -> Doc
ppRule String
sep         = Doc -> (f -> Doc) -> (v -> Doc) -> Rule f v -> Doc
forall f v. Doc -> (f -> Doc) -> (v -> Doc) -> Rule f v -> Doc
prettyRule (String -> Doc
text String
sep) f -> Doc
fun v -> Doc
var

instance (Eq f, Eq v, Pretty f, Pretty v) => Pretty (Problem f v) where
  pretty :: Problem f v -> Doc
pretty = (f -> Doc) -> (v -> Doc) -> Problem f v -> Doc
forall f v.
(Eq f, Eq v) =>
(f -> Doc) -> (v -> Doc) -> Problem f v -> Doc
prettyProblem f -> Doc
forall a. Pretty a => a -> Doc
pretty v -> Doc
forall a. Pretty a => a -> Doc
pretty