{-# LANGUAGE OverloadedStrings #-}

-- | Parses simple Sexp-formatted logical propositions
module SimpleParser.Examples.Direct.Prop where

import qualified Data.Map.Strict as Map
import Data.Sequence (Seq (..))
import qualified Data.Sequence as Seq
import Data.Text (Text)
import Data.Void (Void)
import SimpleParser.Examples.Direct.Ast (AstLabel (..), AstParserC, AstParserM, Ctor (..), CtorDefns, astParser,
                                         identAstParser)

type PropParserC s = AstParserC s
type PropParserM s a = AstParserM s Void a

data SProp v =
    SPropVar !v
  | SPropBool !Bool
  | SPropNot (SProp v)
  | SPropAnd !(Seq (SProp v))
  | SPropOr !(Seq (SProp v))
  | SPropIf !(Seq (SProp v)) (SProp v)
  | SPropIff (SProp v) (SProp v)
  deriving stock (SProp v -> SProp v -> Bool
(SProp v -> SProp v -> Bool)
-> (SProp v -> SProp v -> Bool) -> Eq (SProp v)
forall v. Eq v => SProp v -> SProp v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SProp v -> SProp v -> Bool
$c/= :: forall v. Eq v => SProp v -> SProp v -> Bool
== :: SProp v -> SProp v -> Bool
$c== :: forall v. Eq v => SProp v -> SProp v -> Bool
Eq, Int -> SProp v -> ShowS
[SProp v] -> ShowS
SProp v -> String
(Int -> SProp v -> ShowS)
-> (SProp v -> String) -> ([SProp v] -> ShowS) -> Show (SProp v)
forall v. Show v => Int -> SProp v -> ShowS
forall v. Show v => [SProp v] -> ShowS
forall v. Show v => SProp v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SProp v] -> ShowS
$cshowList :: forall v. Show v => [SProp v] -> ShowS
show :: SProp v -> String
$cshow :: forall v. Show v => SProp v -> String
showsPrec :: Int -> SProp v -> ShowS
$cshowsPrec :: forall v. Show v => Int -> SProp v -> ShowS
Show, a -> SProp b -> SProp a
(a -> b) -> SProp a -> SProp b
(forall a b. (a -> b) -> SProp a -> SProp b)
-> (forall a b. a -> SProp b -> SProp a) -> Functor SProp
forall a b. a -> SProp b -> SProp a
forall a b. (a -> b) -> SProp a -> SProp b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SProp b -> SProp a
$c<$ :: forall a b. a -> SProp b -> SProp a
fmap :: (a -> b) -> SProp a -> SProp b
$cfmap :: forall a b. (a -> b) -> SProp a -> SProp b
Functor, SProp a -> Bool
(a -> m) -> SProp a -> m
(a -> b -> b) -> b -> SProp a -> b
(forall m. Monoid m => SProp m -> m)
-> (forall m a. Monoid m => (a -> m) -> SProp a -> m)
-> (forall m a. Monoid m => (a -> m) -> SProp a -> m)
-> (forall a b. (a -> b -> b) -> b -> SProp a -> b)
-> (forall a b. (a -> b -> b) -> b -> SProp a -> b)
-> (forall b a. (b -> a -> b) -> b -> SProp a -> b)
-> (forall b a. (b -> a -> b) -> b -> SProp a -> b)
-> (forall a. (a -> a -> a) -> SProp a -> a)
-> (forall a. (a -> a -> a) -> SProp a -> a)
-> (forall a. SProp a -> [a])
-> (forall a. SProp a -> Bool)
-> (forall a. SProp a -> Int)
-> (forall a. Eq a => a -> SProp a -> Bool)
-> (forall a. Ord a => SProp a -> a)
-> (forall a. Ord a => SProp a -> a)
-> (forall a. Num a => SProp a -> a)
-> (forall a. Num a => SProp a -> a)
-> Foldable SProp
forall a. Eq a => a -> SProp a -> Bool
forall a. Num a => SProp a -> a
forall a. Ord a => SProp a -> a
forall m. Monoid m => SProp m -> m
forall a. SProp a -> Bool
forall a. SProp a -> Int
forall a. SProp a -> [a]
forall a. (a -> a -> a) -> SProp a -> a
forall m a. Monoid m => (a -> m) -> SProp a -> m
forall b a. (b -> a -> b) -> b -> SProp a -> b
forall a b. (a -> b -> b) -> b -> SProp a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: SProp a -> a
$cproduct :: forall a. Num a => SProp a -> a
sum :: SProp a -> a
$csum :: forall a. Num a => SProp a -> a
minimum :: SProp a -> a
$cminimum :: forall a. Ord a => SProp a -> a
maximum :: SProp a -> a
$cmaximum :: forall a. Ord a => SProp a -> a
elem :: a -> SProp a -> Bool
$celem :: forall a. Eq a => a -> SProp a -> Bool
length :: SProp a -> Int
$clength :: forall a. SProp a -> Int
null :: SProp a -> Bool
$cnull :: forall a. SProp a -> Bool
toList :: SProp a -> [a]
$ctoList :: forall a. SProp a -> [a]
foldl1 :: (a -> a -> a) -> SProp a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SProp a -> a
foldr1 :: (a -> a -> a) -> SProp a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SProp a -> a
foldl' :: (b -> a -> b) -> b -> SProp a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SProp a -> b
foldl :: (b -> a -> b) -> b -> SProp a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SProp a -> b
foldr' :: (a -> b -> b) -> b -> SProp a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SProp a -> b
foldr :: (a -> b -> b) -> b -> SProp a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> SProp a -> b
foldMap' :: (a -> m) -> SProp a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SProp a -> m
foldMap :: (a -> m) -> SProp a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SProp a -> m
fold :: SProp m -> m
$cfold :: forall m. Monoid m => SProp m -> m
Foldable, Functor SProp
Foldable SProp
Functor SProp
-> Foldable SProp
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SProp a -> f (SProp b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    SProp (f a) -> f (SProp a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SProp a -> m (SProp b))
-> (forall (m :: * -> *) a. Monad m => SProp (m a) -> m (SProp a))
-> Traversable SProp
(a -> f b) -> SProp a -> f (SProp b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => SProp (m a) -> m (SProp a)
forall (f :: * -> *) a. Applicative f => SProp (f a) -> f (SProp a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SProp a -> m (SProp b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SProp a -> f (SProp b)
sequence :: SProp (m a) -> m (SProp a)
$csequence :: forall (m :: * -> *) a. Monad m => SProp (m a) -> m (SProp a)
mapM :: (a -> m b) -> SProp a -> m (SProp b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SProp a -> m (SProp b)
sequenceA :: SProp (f a) -> f (SProp a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => SProp (f a) -> f (SProp a)
traverse :: (a -> f b) -> SProp a -> f (SProp b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SProp a -> f (SProp b)
$cp2Traversable :: Foldable SProp
$cp1Traversable :: Functor SProp
Traversable)

guard2 :: MonadFail m => Seq a -> m (Seq a)
guard2 :: Seq a -> m (Seq a)
guard2 Seq a
ss = if Seq a -> Int
forall a. Seq a -> Int
Seq.length Seq a
ss Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 then String -> m (Seq a)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"must have at least two subterms" else Seq a -> m (Seq a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Seq a
ss

guardLast :: MonadFail m => Seq a -> m (Seq a, a)
guardLast :: Seq a -> m (Seq a, a)
guardLast Seq a
ss = case Seq a
ss of { Seq a
xs :|> a
x | Bool -> Bool
not (Seq a -> Bool
forall a. Seq a -> Bool
Seq.null Seq a
xs) -> (Seq a, a) -> m (Seq a, a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Seq a
xs, a
x); Seq a
_ -> String -> m (Seq a, a)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"must have at least two subterms" }

mkPropCtors :: PropParserM s (SProp Text) -> CtorDefns s Void (SProp Text)
mkPropCtors :: PropParserM s (SProp Text) -> CtorDefns s Void (SProp Text)
mkPropCtors PropParserM s (SProp Text)
root = [(Text, Ctor s Void (SProp Text))] -> CtorDefns s Void (SProp Text)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  [ (Text
"<=>", (SProp Text -> SProp Text -> CtorRes Void (SProp Text))
-> PropParserM s (SProp Text)
-> PropParserM s (SProp Text)
-> Ctor s Void (SProp Text)
forall a b e t s.
(a -> b -> CtorRes e t)
-> AstParserM s e a -> AstParserM s e b -> Ctor s e t
Ctor2 (\SProp Text
a SProp Text
b -> SProp Text -> CtorRes Void (SProp Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SProp Text -> SProp Text -> SProp Text
forall v. SProp v -> SProp v -> SProp v
SPropIff SProp Text
a SProp Text
b)) PropParserM s (SProp Text)
root PropParserM s (SProp Text)
root)
  , (Text
"not", (SProp Text -> CtorRes Void (SProp Text))
-> PropParserM s (SProp Text) -> Ctor s Void (SProp Text)
forall a e t s.
(a -> CtorRes e t) -> AstParserM s e a -> Ctor s e t
Ctor1 (SProp Text -> CtorRes Void (SProp Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SProp Text -> CtorRes Void (SProp Text))
-> (SProp Text -> SProp Text)
-> SProp Text
-> CtorRes Void (SProp Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SProp Text -> SProp Text
forall v. SProp v -> SProp v
SPropNot) PropParserM s (SProp Text)
root)
  , (Text
"and", (Seq (SProp Text) -> CtorRes Void (SProp Text))
-> PropParserM s (SProp Text) -> Ctor s Void (SProp Text)
forall a e t s.
(Seq a -> CtorRes e t) -> AstParserM s e a -> Ctor s e t
CtorN ((Seq (SProp Text) -> SProp Text)
-> CtorRes Void (Seq (SProp Text)) -> CtorRes Void (SProp Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Seq (SProp Text) -> SProp Text
forall v. Seq (SProp v) -> SProp v
SPropAnd (CtorRes Void (Seq (SProp Text)) -> CtorRes Void (SProp Text))
-> (Seq (SProp Text) -> CtorRes Void (Seq (SProp Text)))
-> Seq (SProp Text)
-> CtorRes Void (SProp Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (SProp Text) -> CtorRes Void (Seq (SProp Text))
forall (m :: * -> *) a. MonadFail m => Seq a -> m (Seq a)
guard2) PropParserM s (SProp Text)
root)
  , (Text
"or", (Seq (SProp Text) -> CtorRes Void (SProp Text))
-> PropParserM s (SProp Text) -> Ctor s Void (SProp Text)
forall a e t s.
(Seq a -> CtorRes e t) -> AstParserM s e a -> Ctor s e t
CtorN ((Seq (SProp Text) -> SProp Text)
-> CtorRes Void (Seq (SProp Text)) -> CtorRes Void (SProp Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Seq (SProp Text) -> SProp Text
forall v. Seq (SProp v) -> SProp v
SPropOr (CtorRes Void (Seq (SProp Text)) -> CtorRes Void (SProp Text))
-> (Seq (SProp Text) -> CtorRes Void (Seq (SProp Text)))
-> Seq (SProp Text)
-> CtorRes Void (SProp Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (SProp Text) -> CtorRes Void (Seq (SProp Text))
forall (m :: * -> *) a. MonadFail m => Seq a -> m (Seq a)
guard2) PropParserM s (SProp Text)
root)
  , (Text
"=>", (Seq (SProp Text) -> CtorRes Void (SProp Text))
-> PropParserM s (SProp Text) -> Ctor s Void (SProp Text)
forall a e t s.
(Seq a -> CtorRes e t) -> AstParserM s e a -> Ctor s e t
CtorN (((Seq (SProp Text), SProp Text) -> SProp Text)
-> CtorRes Void (Seq (SProp Text), SProp Text)
-> CtorRes Void (SProp Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Seq (SProp Text) -> SProp Text -> SProp Text)
-> (Seq (SProp Text), SProp Text) -> SProp Text
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Seq (SProp Text) -> SProp Text -> SProp Text
forall v. Seq (SProp v) -> SProp v -> SProp v
SPropIf) (CtorRes Void (Seq (SProp Text), SProp Text)
 -> CtorRes Void (SProp Text))
-> (Seq (SProp Text)
    -> CtorRes Void (Seq (SProp Text), SProp Text))
-> Seq (SProp Text)
-> CtorRes Void (SProp Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (SProp Text) -> CtorRes Void (Seq (SProp Text), SProp Text)
forall (m :: * -> *) a. MonadFail m => Seq a -> m (Seq a, a)
guardLast) PropParserM s (SProp Text)
root)
  ]

mkPropAtom :: PropParserC s => PropParserM s (SProp Text)
mkPropAtom :: PropParserM s (SProp Text)
mkPropAtom = do
  Text
ident <- Maybe AstLabel -> AstParserM s Void Text
forall s e. AstParserC s => Maybe AstLabel -> AstParserM s e Text
identAstParser (AstLabel -> Maybe AstLabel
forall a. a -> Maybe a
Just (Text -> AstLabel
AstLabelCustom Text
"atom"))
  case Text
ident of
    Text
"true" -> SProp Text -> PropParserM s (SProp Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> SProp Text
forall v. Bool -> SProp v
SPropBool Bool
True)
    Text
"false" -> SProp Text -> PropParserM s (SProp Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> SProp Text
forall v. Bool -> SProp v
SPropBool Bool
False)
    Text
_ -> SProp Text -> PropParserM s (SProp Text)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> SProp Text
forall v. v -> SProp v
SPropVar Text
ident)

propParser :: PropParserC s => PropParserM s (SProp Text)
propParser :: PropParserM s (SProp Text)
propParser = PropParserM s (SProp Text)
-> (PropParserM s (SProp Text) -> CtorDefns s Void (SProp Text))
-> PropParserM s (SProp Text)
forall s e t.
AstParserC s =>
AstParserM s e t
-> (AstParserM s e t -> CtorDefns s e t) -> AstParserM s e t
astParser PropParserM s (SProp Text)
forall s. PropParserC s => PropParserM s (SProp Text)
mkPropAtom PropParserM s (SProp Text) -> CtorDefns s Void (SProp Text)
forall s.
PropParserM s (SProp Text) -> CtorDefns s Void (SProp Text)
mkPropCtors