Ppr.hs

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 = to_HPJ_Doc . Ppr.ppr

showTheoremSource :: TheoremSource -> Doc
showTheoremSource (LawDefn n) =
  text "definition of" <+> colorize lawColor (text $ show n)
showTheoremSource (Interaction a b) =
  hsep
    [ text "implied by"
    , colorize lawColor $ text $ show $ min a b
    , text "and"
    , colorize lawColor $ text $ show $ max a b
    ]

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

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

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

showSaneTheorem :: Theorem -> Doc
showSaneTheorem (Law n a b) = hang (text "•") 2 $
  sep
  [ hang (colorize exprColor $ ppr $ deModuleName a) 6
      . hang (text "=") 2
      . colorize exprColor
      . ppr
      $ deModuleName b
  , nest 2 $ parens $ showTheoremSource n
  ]

showContradictoryTheorem :: Theorem -> TheoremProblem -> Doc
showContradictoryTheorem (Law n a b) (Contradiction reason) = hang (text "•") 2 $
  sep
  [ vcat
      [ backcolorize Red $ hang (ppr $ deModuleName a) 6
          . hang (text "=") 2
          . ppr
          $ deModuleName b
      , nest 2 $ pprContradiction reason
      ]
  , nest 2 $ parens $ showTheoremSource n
  ]
showContradictoryTheorem (Law n a b) (Dodgy reason) = hang (text "•") 2 $
  sep
  [ vcat
      [ hang (backcolorize Black $ ppr $ deModuleName a) 6
          . hang (text "=") 2
          . backcolorize Black
          . ppr
          $ deModuleName b
      , nest 2 $ pprDodgy reason
      ]
  , nest 2 $ parens $ showTheoremSource n
  ]

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

pprContradiction :: ContradictionReason -> Doc
pprContradiction (UnboundMatchableVars vars) =
  sep
    [ text "the"
    , plural "variable" "variables" vars
    , sep $ punctuate (char ',') $ fmap ppr vars
    , nest 4 $ sep
        [ plural "is" "are" vars
        , text "undetermined"
        ]
    ]
pprContradiction (UnknownConstructors vars) =
  sep
    [ text "the"
    , plural "constructor" "constructors" vars
    , sep $ punctuate (char ',') $ fmap ppr vars
    , nest 4 $ sep
        [ plural "does" "do" vars
        , text "not exist"
        ]
    ]
pprContradiction UnequalValues =
  text "unequal values"

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


exprColor :: Color
exprColor = Blue

lawColor :: Color
lawColor = Yellow