{-# LANGUAGE DeriveDataTypeable #-}
module Data.Logic.Prop where

import Numeric.Natural.QuickCheck ()
import Data.Typeable (Typeable)
import Control.Applicative
import Test.QuickCheck
import Text.Read
import Data.Data (Data)

import Data.Name

-- $setup
-- >>> import Text.Show.Functions ()
-- >>> :set -XOverloadedStrings
-- >>> :set -XScopedTypeVariables
-- >>> import Data.Maybe
-- >>> import Data.List

data Prop
    = Prop Name
    | Imply Prop Prop
    deriving (Eq, Ord, Data, Typeable)
infixr `Imply`

instance Arbitrary Prop where
    arbitrary = frequency
        [ (,) 2 $ Prop <$> arbitrary
        , (,) 1 $ Imply <$> arbitrary <*> arbitrary
        ]

instance CoArbitrary Prop where
    coarbitrary (Prop a) = coarbitrary a
    coarbitrary (Imply a b) = coarbitrary a . coarbitrary b

-- | >>> Prop "a" `Imply` (Prop "b" `Imply` Prop "c")
-- a -> b -> c
-- >>> (Prop "a" `Imply` Prop "b") `Imply` Prop "c"
-- (a -> b) -> c
instance Show Prop where
    showsPrec _ (Prop a) = shows a
    showsPrec d (Imply p q) = showParen (app_prec < d) $
            showsPrec (app_prec+1) p . showString " -> " . shows q
        where app_prec = 10

-- | >>> read "a -> b -> c" :: Prop
-- a -> b -> c
-- >>> read "(a -> b) -> c" :: Prop
-- (a -> b) -> c
--
-- prop> \ (x :: Prop) -> (read . show) x == x
instance Read Prop where
    readPrec = parens (imply <++ prop) where
        prop = Prop <$> readPrec
        imply = prec app_prec $ Imply <$> step readPrec <*> (lexP >>= isArrow >> readPrec)
        isArrow (Punc "->") = return ()
        isArrow _ = pfail
        app_prec = 10
    readsPrec = readPrec_to_S readPrec
