module AlgebraCheckers.Ppr
  ( module AlgebraCheckers.Ppr
  , Doc
  , render
  , sep
  , vcat
  , hsep
  , text
  ) where

import           Control.Monad
import qualified Language.Haskell.TH as Ppr (ppr)
import           Language.Haskell.TH hiding (ppr, Arity)
import           Language.Haskell.TH.PprLib (to_HPJ_Doc)
import           Prelude hiding (exp)
import           System.Console.ANSI
import           AlgebraCheckers.Types
import           AlgebraCheckers.Unification
import qualified Text.PrettyPrint.HughesPJ as Ppr
import           Text.PrettyPrint.HughesPJ hiding ((<>))


ppr :: Ppr a => a -> Doc
ppr :: a -> Doc
ppr = Doc -> Doc
to_HPJ_Doc (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Ppr a => a -> Doc
Ppr.ppr

showTheoremSource :: TheoremSource -> Doc
showTheoremSource :: TheoremSource -> Doc
showTheoremSource (LawDefn String
n) =
  String -> Doc
text String
"definition of" Doc -> Doc -> Doc
<+> Color -> Doc -> Doc
colorize Color
lawColor (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. Show a => a -> String
show String
n)
showTheoremSource (Interaction String
a String
b) =
  [Doc] -> Doc
hsep
    [ String -> Doc
text String
"implied by"
    , Color -> Doc -> Doc
colorize Color
lawColor (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 -> String
forall a. Show a => a -> String
show (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
forall a. Ord a => a -> a -> a
min String
a String
b
    , String -> Doc
text String
"and"
    , Color -> Doc -> Doc
colorize Color
lawColor (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 -> String
forall a. Show a => a -> String
show (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
forall a. Ord a => a -> a -> a
max String
a String
b
    ]

colorize :: Color -> Doc -> Doc
colorize :: Color -> Doc -> Doc
colorize Color
c Doc
doc
       = String -> Doc
zeroWidthText ([SGR] -> String
setSGRCode [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
c])
  Doc -> Doc -> Doc
Ppr.<> Doc
doc
  Doc -> Doc -> Doc
Ppr.<> String -> Doc
zeroWidthText ([SGR] -> String
setSGRCode [ConsoleLayer -> SGR
SetDefaultColor ConsoleLayer
Foreground])

deepColorize :: Color -> Doc -> Doc
deepColorize :: Color -> Doc -> Doc
deepColorize Color
c Doc
doc
       = String -> Doc
zeroWidthText ([SGR] -> String
setSGRCode [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
c, ConsoleIntensity -> SGR
SetConsoleIntensity ConsoleIntensity
BoldIntensity])
  Doc -> Doc -> Doc
Ppr.<> Doc
doc
  Doc -> Doc -> Doc
Ppr.<> String -> Doc
zeroWidthText ([SGR] -> String
setSGRCode [ConsoleLayer -> SGR
SetDefaultColor ConsoleLayer
Foreground, ConsoleIntensity -> SGR
SetConsoleIntensity ConsoleIntensity
NormalIntensity])

backcolorize :: Color -> Doc -> Doc
backcolorize :: Color -> Doc -> Doc
backcolorize Color
c Doc
doc
       = String -> Doc
zeroWidthText ([SGR] -> String
setSGRCode [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Background ColorIntensity
Dull Color
c])
  Doc -> Doc -> Doc
Ppr.<> Doc
doc
  Doc -> Doc -> Doc
Ppr.<> String -> Doc
zeroWidthText ([SGR] -> String
setSGRCode [ConsoleLayer -> SGR
SetDefaultColor ConsoleLayer
Background])

showSaneTheorem :: Theorem -> Doc
showSaneTheorem :: Theorem -> Doc
showSaneTheorem (Law TheoremSource
n Exp
a Exp
b) = Doc -> Int -> Doc -> Doc
hang (String -> Doc
text String
"•") Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
  [Doc] -> Doc
sep
  [ Doc -> Int -> Doc -> Doc
hang (Color -> Doc -> Doc
colorize Color
exprColor (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Exp -> Doc
forall a. Ppr a => a -> Doc
ppr (Exp -> Doc) -> Exp -> Doc
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
forall a. Data a => a -> a
deModuleName Exp
a) Int
6
      (Doc -> Doc) -> (Exp -> Doc) -> Exp -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Int -> Doc -> Doc
hang (String -> Doc
text String
"=") Int
2
      (Doc -> Doc) -> (Exp -> Doc) -> Exp -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Color -> Doc -> Doc
colorize Color
exprColor
      (Doc -> Doc) -> (Exp -> Doc) -> Exp -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Doc
forall a. Ppr a => a -> Doc
ppr
      (Exp -> Doc) -> Exp -> Doc
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
forall a. Data a => a -> a
deModuleName Exp
b
  , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TheoremSource -> Doc
showTheoremSource TheoremSource
n
  ]

showContradictoryTheorem :: Theorem -> TheoremProblem -> Doc
showContradictoryTheorem :: Theorem -> TheoremProblem -> Doc
showContradictoryTheorem (Law TheoremSource
n Exp
a Exp
b) (Contradiction ContradictionReason
reason) = Doc -> Int -> Doc -> Doc
hang (String -> Doc
text String
"•") Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
  [Doc] -> Doc
sep
  [ [Doc] -> Doc
vcat
      [ Color -> Doc -> Doc
backcolorize Color
Red (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Int -> Doc -> Doc
hang (Exp -> Doc
forall a. Ppr a => a -> Doc
ppr (Exp -> Doc) -> Exp -> Doc
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
forall a. Data a => a -> a
deModuleName Exp
a) Int
6
          (Doc -> Doc) -> (Exp -> Doc) -> Exp -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Int -> Doc -> Doc
hang (String -> Doc
text String
"=") Int
2
          (Doc -> Doc) -> (Exp -> Doc) -> Exp -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Doc
forall a. Ppr a => a -> Doc
ppr
          (Exp -> Doc) -> Exp -> Doc
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
forall a. Data a => a -> a
deModuleName Exp
b
      , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ContradictionReason -> Doc
pprContradiction ContradictionReason
reason
      ]
  , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TheoremSource -> Doc
showTheoremSource TheoremSource
n
  ]
showContradictoryTheorem (Law TheoremSource
n Exp
a Exp
b) (Dodgy DodgyReason
reason) = Doc -> Int -> Doc -> Doc
hang (String -> Doc
text String
"•") Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
  [Doc] -> Doc
sep
  [ [Doc] -> Doc
vcat
      [ Doc -> Int -> Doc -> Doc
hang (Color -> Doc -> Doc
backcolorize Color
Black (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Exp -> Doc
forall a. Ppr a => a -> Doc
ppr (Exp -> Doc) -> Exp -> Doc
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
forall a. Data a => a -> a
deModuleName Exp
a) Int
6
          (Doc -> Doc) -> (Exp -> Doc) -> Exp -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Int -> Doc -> Doc
hang (String -> Doc
text String
"=") Int
2
          (Doc -> Doc) -> (Exp -> Doc) -> Exp -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Color -> Doc -> Doc
backcolorize Color
Black
          (Doc -> Doc) -> (Exp -> Doc) -> Exp -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Doc
forall a. Ppr a => a -> Doc
ppr
          (Exp -> Doc) -> Exp -> Doc
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
forall a. Data a => a -> a
deModuleName Exp
b
      , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ DodgyReason -> Doc
pprDodgy DodgyReason
reason
      ]
  , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TheoremSource -> Doc
showTheoremSource TheoremSource
n
  ]

plural :: String -> String -> [a] -> Doc
plural :: String -> String -> [a] -> Doc
plural String
one String
_ [a
_] = String -> Doc
text String
one
plural String
_ String
many [a]
_  = String -> Doc
text String
many

pprContradiction :: ContradictionReason -> Doc
pprContradiction :: ContradictionReason -> Doc
pprContradiction (UnboundMatchableVars [Name]
vars) =
  [Doc] -> Doc
sep
    [ String -> Doc
text String
"the"
    , String -> String -> [Name] -> Doc
forall a. String -> String -> [a] -> Doc
plural String
"variable" String
"variables" [Name]
vars
    , [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (Char -> Doc
char Char
',') ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> [Name] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Doc
forall a. Ppr a => a -> Doc
ppr [Name]
vars
    , Int -> Doc -> Doc
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep
        [ String -> String -> [Name] -> Doc
forall a. String -> String -> [a] -> Doc
plural String
"is" String
"are" [Name]
vars
        , String -> Doc
text String
"undetermined"
        ]
    ]
pprContradiction (UnknownConstructors [Name]
vars) =
  [Doc] -> Doc
sep
    [ String -> Doc
text String
"the"
    , String -> String -> [Name] -> Doc
forall a. String -> String -> [a] -> Doc
plural String
"constructor" String
"constructors" [Name]
vars
    , [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (Char -> Doc
char Char
',') ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> [Name] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Doc
forall a. Ppr a => a -> Doc
ppr [Name]
vars
    , Int -> Doc -> Doc
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep
        [ String -> String -> [Name] -> Doc
forall a. String -> String -> [a] -> Doc
plural String
"does" String
"do" [Name]
vars
        , String -> Doc
text String
"not exist"
        ]
    ]
pprContradiction ContradictionReason
UnequalValues =
  String -> Doc
text String
"unequal values"

pprDodgy :: DodgyReason -> Doc
pprDodgy :: DodgyReason -> Doc
pprDodgy DodgyReason
SelfRecursive =
  String -> Doc
text String
"not necessarily productive"


exprColor :: Color
exprColor :: Color
exprColor = Color
Blue

lawColor :: Color
lawColor :: Color
lawColor = Color
Yellow