{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

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
    -- , parenthesize
    , 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)

-- | A class to extract the fixity of a formula so they can be
-- properly parenthesized.
--
-- The Haskell FixityDirection type is concerned with how to interpret
-- a formula formatted in a certain way, but here we are concerned
-- with how to format a formula given its interpretation.  As such,
-- one case the Haskell type does not capture is whether the operator
-- follows the associative law, so we can omit parentheses in an
-- expression such as @a & b & c@.  Hopefully, we can generate
-- formulas so that an associative operator with left associative
-- fixity direction appears as (a+b)+c rather than a+(b+c).
class HasFixity x where
    precedence :: x -> Precedence
    precedence x
_ = a
Precedence
leafPrec
    associativity :: x -> Associativity
    associativity x
_ = Associativity
InfixL

-- | Use the same precedence type as the pretty package
type Precedence = forall a. Num a => a

data Associativity
    = InfixL  -- Left-associative - a-b-c == (a-b)-c
    | InfixR  -- Right-associative - a=>b=>c == a=>(b=>c)
    | InfixN  -- Non-associative - a>b>c is an error
    | InfixA  -- Associative - a+b+c == (a+b)+c == a+(b+c), ~~a == ~(~a)
    deriving Int -> Associativity -> ShowS
[Associativity] -> ShowS
Associativity -> String
(Int -> Associativity -> ShowS)
-> (Associativity -> String)
-> ([Associativity] -> ShowS)
-> Show Associativity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Associativity -> ShowS
showsPrec :: Int -> Associativity -> ShowS
$cshow :: Associativity -> String
show :: Associativity -> String
$cshowList :: [Associativity] -> ShowS
showList :: [Associativity] -> ShowS
Show

-- | What side of the parent formula are we rendering?
data Side = Top | LHS | RHS | Unary deriving Int -> Side -> ShowS
[Side] -> ShowS
Side -> String
(Int -> Side -> ShowS)
-> (Side -> String) -> ([Side] -> ShowS) -> Show Side
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Side -> ShowS
showsPrec :: Int -> Side -> ShowS
$cshow :: Side -> String
show :: Side -> String
$cshowList :: [Side] -> ShowS
showList :: [Side] -> ShowS
Show

-- | Decide whether to parenthesize based on which side of the parent binary
-- operator we are rendering, the parent operator's precedence, and the precedence
-- and associativity of the operator we are rendering.
-- testParen :: Side -> Precedence -> Precedence -> Associativity -> Bool
testParen :: (Eq a, Ord a, Num a) => Side -> a -> a -> Associativity -> Bool
testParen :: forall a.
(Eq a, Ord a, Num a) =>
Side -> a -> a -> Associativity -> Bool
testParen Side
side a
parentPrec a
childPrec Associativity
childAssoc =
    Bool
testPrecedence Bool -> Bool -> Bool
|| (a
parentPrec a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
childPrec Bool -> Bool -> Bool
&& Bool
testAssoc)
    -- parentPrec > childPrec || (parentPrec == childPrec && testAssoc)
    where
      testPrecedence :: Bool
testPrecedence =
          a
parentPrec a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
childPrec Bool -> Bool -> Bool
||
          (a
parentPrec a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
Precedence
orPrec Bool -> Bool -> Bool
&& a
childPrec a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
Precedence
andPrec) -- Special case - I can't keep these straight
      testAssoc :: Bool
testAssoc = case (Side
side, Associativity
childAssoc) of
                    (Side
LHS, Associativity
InfixL) -> Bool
False
                    (Side
RHS, Associativity
InfixR) -> Bool
False
                    (Side
_, Associativity
InfixA) -> Bool
False
                    -- Tests from the previous version.
                    -- (RHS, InfixL) -> True
                    -- (LHS, InfixR) -> True
                    -- (Unary, _) -> braces pp -- not sure
                    -- (_, InfixN) -> error ("Nested non-associative operators: " ++ show pp)
                    (Side, Associativity)
_ -> Bool
True

instance Pretty a => Pretty (Set a) where
    pPrint :: Set a -> Doc
pPrint = Doc -> Doc
brackets (Doc -> Doc) -> (Set a -> Doc) -> Set a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep ([Doc] -> Doc) -> (Set a -> [Doc]) -> Set a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> (Set a -> [Doc]) -> Set a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pPrint ([a] -> [Doc]) -> (Set a -> [a]) -> Set a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toAscList

instance (Pretty v, Pretty term) => Pretty (Map v term) where
    pPrint :: Map v term -> Doc
pPrint = [(v, term)] -> Doc
forall a. Pretty a => a -> Doc
pPrint ([(v, term)] -> Doc)
-> (Map v term -> [(v, term)]) -> Map v term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map v term -> [(v, term)]
forall k a. Map k a -> [(k, a)]
Map.toList

-- | Version of assertEqual that uses the pretty printer instead of show.
assertEqual' :: (
#ifndef ghcjs_HOST_OS
                 ?loc :: CallStack,
#endif
                 Eq a, Pretty a) =>
                String -- ^ The message prefix
             -> a      -- ^ The expected value
             -> a      -- ^ The actual value
             -> Assertion
assertEqual' :: forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
preface a
expected a
actual =
  Bool -> Assertion -> Assertion
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (a
actual a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
expected) (String -> Assertion
forall a. HasCallStack => String -> IO a
assertFailure String
msg)
 where msg :: String
msg = (if String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
preface then String
"" else String
preface String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n") String -> ShowS
forall a. [a] -> [a] -> [a]
++
             String
"expected: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Pretty a => a -> String
prettyShow a
expected String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n but got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Pretty a => a -> String
prettyShow a
actual

testEquals :: String -> ExpQ
testEquals :: String -> ExpQ
testEquals String
label = [| \expected actual -> TestLabel $(Lit -> ExpQ
forall (m :: * -> *). Quote m => Lit -> m Exp
litE (String -> Lit
stringL String
label)) $ TestCase $ assertEqual' $(Lit -> ExpQ
forall (m :: * -> *). Quote m => Lit -> m Exp
litE (String -> Lit
stringL String
label)) expected actual|]

leafPrec :: Num a => a
leafPrec :: Precedence
leafPrec = a
9

atomPrec :: Num a => a
atomPrec :: Precedence
atomPrec = a
7
notPrec :: Num a => a
notPrec :: Precedence
notPrec = a
6
andPrec :: Num a => a
andPrec :: Precedence
andPrec = a
5
orPrec :: Num a => a
orPrec :: Precedence
orPrec = a
4
impPrec :: Num a => a
impPrec :: Precedence
impPrec = a
3
iffPrec :: Num a => a
iffPrec :: Precedence
iffPrec = a
2
boolPrec :: Num a => a
boolPrec :: Precedence
boolPrec = a
Precedence
leafPrec
quantPrec :: Num a => a
quantPrec :: Precedence
quantPrec = a
1
eqPrec :: Num a => a
eqPrec :: Precedence
eqPrec = a
6
pAppPrec :: Num a => a
pAppPrec :: Precedence
pAppPrec = a
9