-- |
-- Module      : Test.Speculate.Pretty
-- Copyright   : (c) 2016-2024 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of Speculate.
--
-- Pretty printing of Equations, Inequalities and Conditional Equations
module Test.Speculate.Pretty
  ( prettyThy, prettyEquations
  , prettyShy, prettySemiEquations
  , prettyChy, prettyCondEquations
  )
where

import Test.Speculate.Expr
import Test.Speculate.Utils.PrettyPrint
import Test.Speculate.Reason     (Thy, finalEquations)
import Test.Speculate.SemiReason (Shy, finalSemiEquations)
import Test.Speculate.CondReason (Chy, finalCondEquations)

type Equation = (Expr,Expr)
type CondEquation = (Expr,Expr,Expr)

prettyThy :: (Equation -> Bool) -> Instances -> Thy -> String
prettyThy :: (Equation -> Bool) -> Instances -> Thy -> String
prettyThy Equation -> Bool
shouldShow Instances
ti = [Equation] -> String
prettyEquations ([Equation] -> String) -> (Thy -> [Equation]) -> Thy -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> Bool) -> Instances -> Thy -> [Equation]
finalEquations Equation -> Bool
shouldShow Instances
ti

prettyChy :: (CondEquation -> Bool) -> Chy -> String
prettyChy :: (CondEquation -> Bool) -> Chy -> String
prettyChy CondEquation -> Bool
shouldShow = [CondEquation] -> String
prettyCondEquations ([CondEquation] -> String)
-> (Chy -> [CondEquation]) -> Chy -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CondEquation -> Bool) -> Chy -> [CondEquation]
finalCondEquations CondEquation -> Bool
shouldShow

prettyShy :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> String
prettyShy :: (Equation -> Bool)
-> Instances -> (Expr -> Expr -> Bool) -> Shy -> String
prettyShy Equation -> Bool
shouldShow Instances
insts Expr -> Expr -> Bool
equivalentInstanceOf =
  [Equation] -> String
prettySemiEquations ([Equation] -> String) -> (Shy -> [Equation]) -> Shy -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> Bool)
-> Instances -> (Expr -> Expr -> Bool) -> Shy -> [Equation]
finalSemiEquations Equation -> Bool
shouldShow Instances
insts Expr -> Expr -> Bool
equivalentInstanceOf

prettyEquations :: [Equation] -> String
prettyEquations :: [Equation] -> String
prettyEquations =
  String -> [[String]] -> String
table String
"r l l" ([[String]] -> String)
-> ([Equation] -> [[String]]) -> [Equation] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> [String]) -> [Equation] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map Equation -> [String]
showEquation
  where
  showEquation :: Equation -> [String]
showEquation (Expr
e1,Expr
e2)
--  | typ e1 == boolTy
--  = [showOpExpr "<==>" e1, "<==>", showOpExpr "<==>" e2]
--  | otherwise
    = [String -> Expr -> String
showOpExpr String
"==" Expr
e1, String
"==", String -> Expr -> String
showOpExpr String
"==" Expr
e2]

prettySemiEquations :: [Equation] -> String
prettySemiEquations :: [Equation] -> String
prettySemiEquations =
  String -> [[String]] -> String
table String
"r l l" ([[String]] -> String)
-> ([Equation] -> [[String]]) -> [Equation] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> [String]) -> [Equation] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map Equation -> [String]
showSELine
  where
  showSELine :: Equation -> [String]
showSELine (Expr
e1,Expr
e2) = String -> Equation -> [String]
showLineWithOp (if Expr -> TypeRep
typ Expr
e1 TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep
boolTy then String
"==>" else String
"<=") (Expr
e1,Expr
e2)
  showLineWithOp :: String -> Equation -> [String]
showLineWithOp String
o (Expr
e1,Expr
e2) = [String -> Expr -> String
showOpExpr String
o Expr
e1, String
o, String -> Expr -> String
showOpExpr String
o Expr
e2]

prettyCondEquations :: [CondEquation] -> String
prettyCondEquations :: [CondEquation] -> String
prettyCondEquations =
  String -> [[String]] -> String
table String
"r r r l l" ([[String]] -> String)
-> ([CondEquation] -> [[String]]) -> [CondEquation] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CondEquation -> [String]) -> [CondEquation] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map CondEquation -> [String]
showCELine
  where
  showCELine :: CondEquation -> [String]
showCELine (Expr
ce,Expr
e1,Expr
e2) = [ String -> Expr -> String
showOpExpr String
"==>" Expr
ce
                          , String
"==>", String -> Expr -> String
showOpExpr String
"==" Expr
e1
                          , String
"==",  String -> Expr -> String
showOpExpr String
"==" Expr
e2 ]