{-# 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
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
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, 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
<$ :: forall a b. a -> SProp b -> SProp a
$c<$ :: forall a b. a -> SProp b -> SProp a
fmap :: forall a b. (a -> b) -> SProp a -> SProp b
$cfmap :: forall a b. (a -> b) -> SProp a -> SProp b
Functor, 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 :: forall a. Num a => SProp a -> a
$cproduct :: forall a. Num a => SProp a -> a
sum :: forall a. Num a => SProp a -> a
$csum :: forall a. Num a => SProp a -> a
minimum :: forall a. Ord a => SProp a -> a
$cminimum :: forall a. Ord a => SProp a -> a
maximum :: forall a. Ord a => SProp a -> a
$cmaximum :: forall a. Ord a => SProp a -> a
elem :: forall a. Eq a => a -> SProp a -> Bool
$celem :: forall a. Eq a => a -> SProp a -> Bool
length :: forall a. SProp a -> Int
$clength :: forall a. SProp a -> Int
null :: forall a. SProp a -> Bool
$cnull :: forall a. SProp a -> Bool
toList :: forall a. SProp a -> [a]
$ctoList :: forall a. SProp a -> [a]
foldl1 :: forall a. (a -> a -> a) -> SProp a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SProp a -> a
foldr1 :: forall a. (a -> a -> a) -> SProp a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SProp a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> SProp a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SProp a -> b
foldl :: forall b a. (b -> a -> b) -> b -> SProp a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SProp a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> SProp a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SProp a -> b
foldr :: forall a b. (a -> b -> b) -> b -> SProp a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> SProp a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> SProp a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SProp a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> SProp a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SProp a -> m
fold :: forall m. Monoid m => SProp m -> m
$cfold :: forall m. Monoid m => SProp m -> m
Foldable, Functor SProp
Foldable SProp
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 :: forall (m :: * -> *) a. Monad m => SProp (m a) -> m (SProp a)
$csequence :: forall (m :: * -> *) a. Monad m => SProp (m a) -> m (SProp a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SProp a -> m (SProp b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SProp a -> m (SProp b)
sequenceA :: forall (f :: * -> *) a. Applicative f => SProp (f a) -> f (SProp a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => SProp (f a) -> f (SProp a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SProp a -> f (SProp b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SProp a -> f (SProp b)
Traversable)

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

guardLast :: MonadFail m => Seq a -> m (Seq a, a)
guardLast :: forall (m :: * -> *) a. MonadFail m => Seq a -> m (Seq a, a)
guardLast Seq a
ss = case Seq a
ss of { Seq a
xs :|> a
x | Bool -> Bool
not (forall a. Seq a -> Bool
Seq.null Seq a
xs) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Seq a
xs, a
x); Seq 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 :: forall s.
PropParserM s (SProp Text) -> CtorDefns s Void (SProp Text)
mkPropCtors PropParserM s (SProp Text)
root = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  [ (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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (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", forall a e t s.
(a -> CtorRes e t) -> AstParserM s e a -> Ctor s e t
Ctor1 (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. SProp v -> SProp v
SPropNot) PropParserM s (SProp Text)
root)
  , (Text
"and", forall a e t s.
(Seq a -> CtorRes e t) -> AstParserM s e a -> Ctor s e t
CtorN (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall v. Seq (SProp v) -> SProp v
SPropAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadFail m => Seq a -> m (Seq a)
guard2) PropParserM s (SProp Text)
root)
  , (Text
"or", forall a e t s.
(Seq a -> CtorRes e t) -> AstParserM s e a -> Ctor s e t
CtorN (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall v. Seq (SProp v) -> SProp v
SPropOr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadFail m => Seq a -> m (Seq a)
guard2) PropParserM s (SProp Text)
root)
  , (Text
"=>", forall a e t s.
(Seq a -> CtorRes e t) -> AstParserM s e a -> Ctor s e t
CtorN (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall v. Seq (SProp v) -> SProp v -> SProp v
SPropIf) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall s. PropParserC s => PropParserM s (SProp Text)
mkPropAtom = do
  Text
ident <- forall s e. AstParserC s => Maybe AstLabel -> AstParserM s e Text
identAstParser (forall a. a -> Maybe a
Just (Text -> AstLabel
AstLabelCustom Text
"atom"))
  case Text
ident of
    Text
"true" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall v. Bool -> SProp v
SPropBool Bool
True)
    Text
"false" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall v. Bool -> SProp v
SPropBool Bool
False)
    Text
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall v. v -> SProp v
SPropVar Text
ident)

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