{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE EmptyDataDeriving #-}
module Predicate.Data.Monoid (
type (<>)
, MConcat
, SConcat
, STimes
, Sap
, type S
, MEmptyT
, MEmptyT'
, MEmptyP
) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Data.Proxy (Proxy(Proxy))
import Data.Kind (Type)
import qualified Data.Semigroup as SG
import Data.List.NonEmpty (NonEmpty(..))
data p <> q deriving Int -> (p <> q) -> ShowS
[p <> q] -> ShowS
(p <> q) -> String
(Int -> (p <> q) -> ShowS)
-> ((p <> q) -> String) -> ([p <> q] -> ShowS) -> Show (p <> q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> (p <> q) -> ShowS
forall k (p :: k) k (q :: k). [p <> q] -> ShowS
forall k (p :: k) k (q :: k). (p <> q) -> String
showList :: [p <> q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [p <> q] -> ShowS
show :: (p <> q) -> String
$cshow :: forall k (p :: k) k (q :: k). (p <> q) -> String
showsPrec :: Int -> (p <> q) -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> (p <> q) -> ShowS
Show
infixr 6 <>
instance ( Semigroup (PP p x)
, PP p x ~ PP q x
, P p x
, Show (PP q x)
, P q x
) => P (p <> q) x where
type PP (p <> q) x = PP p x
eval :: proxy (p <> q) -> POpts -> x -> m (TT (PP (p <> q) x))
eval proxy (p <> q)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"<>"
Either (TT (PP q x)) (PP q x, PP q x, TT (PP q x), TT (PP q x))
lr <- Inline
-> String
-> Proxy p
-> Proxy q
-> POpts
-> x
-> [Tree PE]
-> m (Either
(TT (PP q x)) (PP p x, PP q x, TT (PP p x), TT (PP q x)))
forall k1 k2 (p :: k1) a (q :: k2) (m :: Type -> Type)
(proxy1 :: k1 -> Type) (proxy2 :: k2 -> Type) x.
(P p a, P q a, MonadEval m) =>
Inline
-> String
-> proxy1 p
-> proxy2 q
-> POpts
-> a
-> [Tree PE]
-> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
runPQ Inline
NoInline String
msg0 (Proxy p
forall k (t :: k). Proxy t
Proxy @p) (Proxy q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts x
x []
TT (PP q x) -> m (TT (PP q x))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP q x) -> m (TT (PP q x))) -> TT (PP q x) -> m (TT (PP q x))
forall a b. (a -> b) -> a -> b
$ case Either (TT (PP q x)) (PP q x, PP q x, TT (PP q x), TT (PP q x))
lr of
Left TT (PP q x)
e -> TT (PP q x)
e
Right (PP q x
p,PP q x
q,TT (PP q x)
pp,TT (PP q x)
qq) ->
let d :: PP q x
d = PP q x
p PP q x -> PP q x -> PP q x
forall a. Semigroup a => a -> a -> a
<> PP q x
q
in POpts -> Val (PP q x) -> String -> [Tree PE] -> TT (PP q x)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (PP q x -> Val (PP q x)
forall a. a -> Val a
Val PP q x
d) (POpts -> PP q x -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP q x
p String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" <> " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP q x -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP q x
q String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" = " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP q x -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP q x
d) [TT (PP q x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q x)
pp, TT (PP q x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q x)
qq]
type S a = SG.WrappedMonoid a
data Sap (t :: Type) deriving Int -> Sap t -> ShowS
[Sap t] -> ShowS
Sap t -> String
(Int -> Sap t -> ShowS)
-> (Sap t -> String) -> ([Sap t] -> ShowS) -> Show (Sap t)
forall t. Int -> Sap t -> ShowS
forall t. [Sap t] -> ShowS
forall t. Sap t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sap t] -> ShowS
$cshowList :: forall t. [Sap t] -> ShowS
show :: Sap t -> String
$cshow :: forall t. Sap t -> String
showsPrec :: Int -> Sap t -> ShowS
$cshowsPrec :: forall t. Int -> Sap t -> ShowS
Show
type SapT (t :: Type) = Wrap t Fst <> Wrap t Snd >> Unwrap
instance P (SapT t) x => P (Sap t) x where
type PP (Sap t) x = PP (SapT t) x
eval :: proxy (Sap t) -> POpts -> x -> m (TT (PP (Sap t) x))
eval proxy (Sap t)
_ = Proxy (SapT t) -> POpts -> x -> m (TT (PP (SapT t) x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (SapT t)
forall k (t :: k). Proxy t
Proxy @(SapT t))
data MConcat deriving Int -> MConcat -> ShowS
[MConcat] -> ShowS
MConcat -> String
(Int -> MConcat -> ShowS)
-> (MConcat -> String) -> ([MConcat] -> ShowS) -> Show MConcat
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MConcat] -> ShowS
$cshowList :: [MConcat] -> ShowS
show :: MConcat -> String
$cshow :: MConcat -> String
showsPrec :: Int -> MConcat -> ShowS
$cshowsPrec :: Int -> MConcat -> ShowS
Show
instance ( x ~ [a]
, Show a
, Monoid a
) => P MConcat x where
type PP MConcat x = ExtractAFromList x
eval :: proxy MConcat -> POpts -> x -> m (TT (PP MConcat x))
eval proxy MConcat
_ POpts
opts x
x =
let msg0 :: String
msg0 = String
"MConcat"
b :: a
b = [a] -> a
forall a. Monoid a => [a] -> a
mconcat x
[a]
x
in TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
b) (POpts -> String -> a -> x -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msg0 a
b x
x) []
data SConcat p deriving Int -> SConcat p -> ShowS
[SConcat p] -> ShowS
SConcat p -> String
(Int -> SConcat p -> ShowS)
-> (SConcat p -> String)
-> ([SConcat p] -> ShowS)
-> Show (SConcat p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k). Int -> SConcat p -> ShowS
forall k (p :: k). [SConcat p] -> ShowS
forall k (p :: k). SConcat p -> String
showList :: [SConcat p] -> ShowS
$cshowList :: forall k (p :: k). [SConcat p] -> ShowS
show :: SConcat p -> String
$cshow :: forall k (p :: k). SConcat p -> String
showsPrec :: Int -> SConcat p -> ShowS
$cshowsPrec :: forall k (p :: k). Int -> SConcat p -> ShowS
Show
instance ( PP p x ~ NonEmpty a
, P p x
, Show a
, Semigroup a
) => P (SConcat p) x where
type PP (SConcat p) x = ExtractAFromTA (PP p x)
eval :: proxy (SConcat p) -> POpts -> x -> m (TT (PP (SConcat p) x))
eval proxy (SConcat p)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"SConcat"
TT (NonEmpty a)
pp <- Proxy p -> POpts -> x -> m (TT (PP p x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts x
x
TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (NonEmpty a)
-> [Tree PE]
-> Either (TT a) (NonEmpty a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (NonEmpty a)
pp [] of
Left TT a
e -> TT a
e
Right NonEmpty a
p ->
let b :: a
b = NonEmpty a -> a
forall a. Semigroup a => NonEmpty a -> a
SG.sconcat NonEmpty a
p
in POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
b) (POpts -> String -> a -> NonEmpty a -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msg0 a
b NonEmpty a
p) [TT (NonEmpty a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (NonEmpty a)
pp]
data MEmptyT' t deriving Int -> MEmptyT' t -> ShowS
[MEmptyT' t] -> ShowS
MEmptyT' t -> String
(Int -> MEmptyT' t -> ShowS)
-> (MEmptyT' t -> String)
-> ([MEmptyT' t] -> ShowS)
-> Show (MEmptyT' t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (t :: k). Int -> MEmptyT' t -> ShowS
forall k (t :: k). [MEmptyT' t] -> ShowS
forall k (t :: k). MEmptyT' t -> String
showList :: [MEmptyT' t] -> ShowS
$cshowList :: forall k (t :: k). [MEmptyT' t] -> ShowS
show :: MEmptyT' t -> String
$cshow :: forall k (t :: k). MEmptyT' t -> String
showsPrec :: Int -> MEmptyT' t -> ShowS
$cshowsPrec :: forall k (t :: k). Int -> MEmptyT' t -> ShowS
Show
instance ( Show (PP t a)
, Monoid (PP t a)
) => P (MEmptyT' t) a where
type PP (MEmptyT' t) a = PP t a
eval :: proxy (MEmptyT' t) -> POpts -> a -> m (TT (PP (MEmptyT' t) a))
eval proxy (MEmptyT' t)
_ POpts
opts a
_ =
let msg0 :: String
msg0 = String
"MEmptyT"
b :: PP t a
b = Monoid (PP t a) => PP t a
forall a. Monoid a => a
mempty @(PP t a)
in TT (PP t a) -> m (TT (PP t a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP t a) -> m (TT (PP t a))) -> TT (PP t a) -> m (TT (PP t a))
forall a b. (a -> b) -> a -> b
$ POpts -> Val (PP t a) -> String -> [Tree PE] -> TT (PP t a)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (PP t a -> Val (PP t a)
forall a. a -> Val a
Val PP t a
b) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP t a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP t a
b) []
data MEmptyT (t :: Type) deriving Int -> MEmptyT t -> ShowS
[MEmptyT t] -> ShowS
MEmptyT t -> String
(Int -> MEmptyT t -> ShowS)
-> (MEmptyT t -> String)
-> ([MEmptyT t] -> ShowS)
-> Show (MEmptyT t)
forall t. Int -> MEmptyT t -> ShowS
forall t. [MEmptyT t] -> ShowS
forall t. MEmptyT t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MEmptyT t] -> ShowS
$cshowList :: forall t. [MEmptyT t] -> ShowS
show :: MEmptyT t -> String
$cshow :: forall t. MEmptyT t -> String
showsPrec :: Int -> MEmptyT t -> ShowS
$cshowsPrec :: forall t. Int -> MEmptyT t -> ShowS
Show
type MEmptyTT (t :: Type) = MEmptyT' (Hole t)
instance P (MEmptyTT t) x => P (MEmptyT t) x where
type PP (MEmptyT t) x = PP (MEmptyTT t) x
eval :: proxy (MEmptyT t) -> POpts -> x -> m (TT (PP (MEmptyT t) x))
eval proxy (MEmptyT t)
_ = Proxy (MEmptyTT t) -> POpts -> x -> m (TT (PP (MEmptyTT t) x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy (MEmptyTT t)
forall k (t :: k). Proxy t
Proxy @(MEmptyTT t))
data MEmptyP deriving Int -> MEmptyP -> ShowS
[MEmptyP] -> ShowS
MEmptyP -> String
(Int -> MEmptyP -> ShowS)
-> (MEmptyP -> String) -> ([MEmptyP] -> ShowS) -> Show MEmptyP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MEmptyP] -> ShowS
$cshowList :: [MEmptyP] -> ShowS
show :: MEmptyP -> String
$cshow :: MEmptyP -> String
showsPrec :: Int -> MEmptyP -> ShowS
$cshowsPrec :: Int -> MEmptyP -> ShowS
Show
type MEmptyPT = MEmptyT' UnproxyT
instance P MEmptyPT x => P MEmptyP x where
type PP MEmptyP x = PP MEmptyPT x
eval :: proxy MEmptyP -> POpts -> x -> m (TT (PP MEmptyP x))
eval proxy MEmptyP
_ = Proxy MEmptyPT -> POpts -> x -> m (TT (PP MEmptyPT x))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy MEmptyPT
forall k (t :: k). Proxy t
Proxy @MEmptyPT)
data STimes n p deriving Int -> STimes n p -> ShowS
[STimes n p] -> ShowS
STimes n p -> String
(Int -> STimes n p -> ShowS)
-> (STimes n p -> String)
-> ([STimes n p] -> ShowS)
-> Show (STimes n p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (n :: k) k (p :: k). Int -> STimes n p -> ShowS
forall k (n :: k) k (p :: k). [STimes n p] -> ShowS
forall k (n :: k) k (p :: k). STimes n p -> String
showList :: [STimes n p] -> ShowS
$cshowList :: forall k (n :: k) k (p :: k). [STimes n p] -> ShowS
show :: STimes n p -> String
$cshow :: forall k (n :: k) k (p :: k). STimes n p -> String
showsPrec :: Int -> STimes n p -> ShowS
$cshowsPrec :: forall k (n :: k) k (p :: k). Int -> STimes n p -> ShowS
Show
instance ( P n a
, Integral (PP n a)
, Semigroup (PP p a)
, P p a
, Show (PP p a)
) => P (STimes n p) a where
type PP (STimes n p) a = PP p a
eval :: proxy (STimes n p) -> POpts -> a -> m (TT (PP (STimes n p) a))
eval proxy (STimes n p)
_ POpts
opts a
a = do
let msg0 :: String
msg0 = String
"STimes"
Either (TT (PP p a)) (PP n a, PP p a, TT (PP n a), TT (PP p a))
lr <- Inline
-> String
-> Proxy n
-> Proxy p
-> POpts
-> a
-> [Tree PE]
-> m (Either
(TT (PP p a)) (PP n a, PP p a, TT (PP n a), TT (PP p a)))
forall k1 k2 (p :: k1) a (q :: k2) (m :: Type -> Type)
(proxy1 :: k1 -> Type) (proxy2 :: k2 -> Type) x.
(P p a, P q a, MonadEval m) =>
Inline
-> String
-> proxy1 p
-> proxy2 q
-> POpts
-> a
-> [Tree PE]
-> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
runPQ Inline
NoInline String
msg0 (Proxy n
forall k (t :: k). Proxy t
Proxy @n) (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
a []
TT (PP p a) -> m (TT (PP p a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP p a) -> m (TT (PP p a))) -> TT (PP p a) -> m (TT (PP p a))
forall a b. (a -> b) -> a -> b
$ case Either (TT (PP p a)) (PP n a, PP p a, TT (PP n a), TT (PP p a))
lr of
Left TT (PP p a)
e -> TT (PP p a)
e
Right (PP n a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral -> Int
n::Int,PP p a
p,TT (PP n a)
pp,TT (PP p a)
qq) ->
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Int -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts Int
n String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" p=" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP p a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP p a
p
b :: PP p a
b = Int -> PP p a -> PP p a
forall a b. (Semigroup a, Integral b) => b -> a -> a
SG.stimes Int
n PP p a
p
in POpts -> Val (PP p a) -> String -> [Tree PE] -> TT (PP p a)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (PP p a -> Val (PP p a)
forall a. a -> Val a
Val PP p a
b) (POpts -> String -> PP p a -> String -> Int -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> String -> a2 -> String
show3' POpts
opts String
msg1 PP p a
b String
"n=" Int
n String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> PP p a -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | " PP p a
p) [TT (PP n a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP n a)
pp, TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
qq]