module Data.Logic.ATP.Pretty
( (<>)
, Pretty(pPrint, pPrintPrec)
, module Text.PrettyPrint.HughesPJClass
, Associativity(InfixL, InfixR, InfixN, InfixA)
, Precedence
, HasFixity(precedence, associativity)
, Side(Top, LHS, RHS, Unary)
, testParen
, assertEqual'
, testEquals
, leafPrec
, boolPrec
, notPrec
, atomPrec
, andPrec
, orPrec
, impPrec
, iffPrec
, quantPrec
, eqPrec
, pAppPrec
) where
import Control.Monad (unless)
import Data.Map.Strict as Map (Map, toList)
import Data.Monoid ((<>))
import Data.Set as Set (Set, toAscList)
import GHC.Stack
import Language.Haskell.TH (ExpQ, litE, stringL)
import Test.HUnit (Assertion, assertFailure, Test(TestLabel, TestCase))
import Text.PrettyPrint.HughesPJClass (brackets, comma, Doc, fsep, hcat, nest, Pretty(pPrint, pPrintPrec), prettyShow, punctuate, text)
class HasFixity x where
precedence :: x -> Precedence
precedence _ = leafPrec
associativity :: x -> Associativity
associativity _ = InfixL
type Precedence = forall a. Num a => a
data Associativity
= InfixL
| InfixR
| InfixN
| InfixA
deriving Show
data Side = Top | LHS | RHS | Unary deriving Show
testParen :: (Eq a, Ord a, Num a) => Side -> a -> a -> Associativity -> Bool
testParen side parentPrec childPrec childAssoc =
testPrecedence || (parentPrec == childPrec && testAssoc)
where
testPrecedence =
parentPrec > childPrec ||
(parentPrec == orPrec && childPrec == andPrec)
testAssoc = case (side, childAssoc) of
(LHS, InfixL) -> False
(RHS, InfixR) -> False
(_, InfixA) -> False
_ -> True
instance Pretty a => Pretty (Set a) where
pPrint = brackets . fsep . punctuate comma . map pPrint . Set.toAscList
instance (Pretty v, Pretty term) => Pretty (Map v term) where
pPrint = pPrint . Map.toList
assertEqual' :: (
#ifndef ghcjs_HOST_OS
?loc :: CallStack,
#endif
Eq a, Pretty a) =>
String
-> a
-> a
-> Assertion
assertEqual' preface expected actual =
unless (actual == expected) (assertFailure msg)
where msg = (if null preface then "" else preface ++ "\n") ++
"expected: " ++ prettyShow expected ++ "\n but got: " ++ prettyShow actual
testEquals :: String -> ExpQ
testEquals label = [| \expected actual -> TestLabel $(litE (stringL label)) $ TestCase $ assertEqual' $(litE (stringL label)) expected actual|]
leafPrec :: Num a => a
leafPrec = 9
atomPrec :: Num a => a
atomPrec = 7
notPrec :: Num a => a
notPrec = 6
andPrec :: Num a => a
andPrec = 5
orPrec :: Num a => a
orPrec = 4
impPrec :: Num a => a
impPrec = 3
iffPrec :: Num a => a
iffPrec = 2
boolPrec :: Num a => a
boolPrec = leafPrec
quantPrec :: Num a => a
quantPrec = 1
eqPrec :: Num a => a
eqPrec = 6
pAppPrec :: Num a => a
pAppPrec = 9