{-# OPTIONS -Wall #-}
{-# OPTIONS -Wcompat #-}
{-# OPTIONS -Wincomplete-record-updates #-}
{-# OPTIONS -Wincomplete-uni-patterns #-}
{-# OPTIONS -Wredundant-constraints #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE NoStarIsType #-}
module Predicate.Core (
I
, Id
, IdT
, W
, Msg
, pan
, pa
, pu
, pab
, pub
, pl
, pz
, run
, P(..)
, runPQ
, runPQBool
, evalBool
, evalQuick
, prtTree'
) where
import Predicate.Util
import GHC.TypeLits (Symbol,Nat,KnownSymbol,KnownNat)
import Control.Lens ((^.))
import Data.Proxy
import Data.Typeable
import Data.Kind (Type)
import Data.These (These(..))
import Data.Functor.Identity
class P p a where
type PP (p :: k) a :: Type
eval :: MonadEval m => Proxy p -> POpts -> a -> m (TT (PP p a))
evalBool :: (MonadEval m, P p a, PP p a ~ Bool) => Proxy p -> POpts -> a -> m (TT (PP p a))
evalBool p opts a = fixBoolT <$> eval p opts a
evalQuick :: forall p i . P p i => i -> Either String (PP p i)
evalQuick i = getValLRFromTT (runIdentity (eval (Proxy @p) (getOptT @'OL) i))
data I
instance P I a where
type PP I a = a
eval _ opts a =
let msg0 = "I"
in pure $ mkNode opts (PresentT a) msg0 []
data Id
instance Show a => P Id a where
type PP Id a = a
eval _ opts a =
let msg0 = "Id"
in pure $ mkNode opts (PresentT a) (msg0 <> show0 opts " " a) []
data IdT
instance (Typeable a, Show a) => P IdT a where
type PP IdT a = a
eval _ opts a =
let msg0 = "IdT(" <> t <> ")"
t = showT @a
in pure $ mkNode opts (PresentT a) (msg0 <> show0 opts " " a) []
data W (p :: k)
instance P p a => P (W p) a where
type PP (W p) a = PP p a
eval _ = eval (Proxy @(Msg "W" p))
data Msg prt p
instance (P prt a
, PP prt a ~ String
, P p a
) => P (Msg prt p) a where
type PP (Msg prt p) a = PP p a
eval _ opts a = do
pp <- eval (Proxy @prt) opts a
case getValueLR opts "Msg" pp [] of
Left e -> pure e
Right msg -> prefixMsg msg <$> eval (Proxy @p) opts a
instance P () a where
type PP () a = ()
eval _ opts _ =
let msg0 = "()"
in pure $ mkNode opts (PresentT ()) msg0 []
instance P (Proxy t) a where
type PP (Proxy t) a = Proxy t
eval _ opts _ =
let msg0 = "Proxy"
in pure $ mkNode opts (PresentT Proxy) msg0 []
instance GetBool b => P (b :: Bool) a where
type PP b a = Bool
eval _ opts _ =
let b = getBool @b
in pure $ mkNodeB opts b ("'" <> show b) []
instance KnownSymbol s => P (s :: Symbol) a where
type PP s a = String
eval _ opts _ =
let s = symb @s
in pure $ mkNode opts (PresentT s) ("'" <> showLit0 opts "" s) []
instance (P p a, P q a) => P '(p,q) a where
type PP '(p,q) a = (PP p a, PP q a)
eval _ opts a = do
let msg = "'(,)"
lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
mkNode opts (PresentT (p,q)) msg [hh pp, hh qq]
instance (P p a
, P q a
, P r a
) => P '(p,q,r) a where
type PP '(p,q,r) a = (PP p a, PP q a, PP r a)
eval _ opts a = do
let msg = "'(,,)"
lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
let hhs0 = [hh pp, hh qq]
rr <- eval (Proxy @r) opts a
pure $ case getValueLR opts msg rr hhs0 of
Left e -> e
Right r ->
let hhs1 = hhs0 <> [hh rr]
in mkNode opts (PresentT (p,q,r)) msg hhs1
instance (P p a
, P q a
, P r a
, P s a
) => P '(p,q,r,s) a where
type PP '(p,q,r,s) a = (PP p a, PP q a, PP r a, PP s a)
eval _ opts a = do
let msg = "'(,,,)"
lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
let hhs0 = [hh pp, hh qq]
lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
pure $ case lr1 of
Left e -> e
Right (r,s,rr,ss) ->
let hhs1 = hhs0 ++ [hh rr, hh ss]
in mkNode opts (PresentT (p,q,r,s)) msg hhs1
instance (P p a
, P q a
, P r a
, P s a
, P t a
) => P '(p,q,r,s,t) a where
type PP '(p,q,r,s,t) a = (PP p a, PP q a, PP r a, PP s a, PP t a)
eval _ opts a = do
let msg = "'(,,,,)"
lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
let hhs0 = [hh pp, hh qq]
lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
case lr1 of
Left e -> pure e
Right (r,s,rr,ss) -> do
let hhs1 = hhs0 ++ [hh rr, hh ss]
tt <- eval (Proxy @t) opts a
pure $ case getValueLR opts msg tt hhs1 of
Left e -> e
Right t ->
let hhs2 = hhs1 <> [hh tt]
in mkNode opts (PresentT (p,q,r,s,t)) msg hhs2
instance (P p a
, P q a
, P r a
, P s a
, P t a
, P u a
) => P '(p,q,r,s,t,u) a where
type PP '(p,q,r,s,t,u) a = (PP p a, PP q a, PP r a, PP s a, PP t a, PP u a)
eval _ opts a = do
let msg = "'(,,,,,)"
lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
let hhs0 = [hh pp, hh qq]
lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
case lr1 of
Left e -> pure e
Right (r,s,rr,ss) -> do
let hhs1 = hhs0 ++ [hh rr, hh ss]
lr2 <- runPQ msg (Proxy @t) (Proxy @u) opts a hhs1
pure $ case lr2 of
Left e -> e
Right (t,u,tt,uu) ->
let hhs2 = hhs1 ++ [hh tt, hh uu]
in mkNode opts (PresentT (p,q,r,s,t,u)) msg hhs2
instance (P p a
, P q a
, P r a
, P s a
, P t a
, P u a
, P v a
) => P '(p,q,r,s,t,u,v) a where
type PP '(p,q,r,s,t,u,v) a = (PP p a, PP q a, PP r a, PP s a, PP t a, PP u a, PP v a)
eval _ opts a = do
let msg = "'(,,,,,,)"
lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
let hhs0 = [hh pp, hh qq]
lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
case lr1 of
Left e -> pure e
Right (r,s,rr,ss) -> do
let hhs1 = hhs0 ++ [hh rr, hh ss]
lr2 <- runPQ msg (Proxy @t) (Proxy @u) opts a hhs1
case lr2 of
Left e -> pure e
Right (t,u,tt,uu) -> do
vv <- eval (Proxy @v) opts a
let hhs2 = hhs1 ++ [hh tt, hh uu]
pure $ case getValueLR opts msg vv hhs2 of
Left e -> e
Right v ->
let hhs3 = hhs2 ++ [hh vv]
in mkNode opts (PresentT (p,q,r,s,t,u,v)) msg hhs3
instance (P p a
, P q a
, P r a
, P s a
, P t a
, P u a
, P v a
, P w a
) => P '(p,q,r,s,t,u,v,w) a where
type PP '(p,q,r,s,t,u,v,w) a = (PP p a, PP q a, PP r a, PP s a, PP t a, PP u a, PP v a, PP w a)
eval _ opts a = do
let msg = "'(,,,,,,,)"
lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
let hhs0 = [hh pp, hh qq]
lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
case lr1 of
Left e -> pure e
Right (r,s,rr,ss) -> do
let hhs1 = hhs0 ++ [hh rr, hh ss]
lr2 <- runPQ msg (Proxy @t) (Proxy @u) opts a hhs1
case lr2 of
Left e -> pure e
Right (t,u,tt,uu) -> do
let hhs2 = hhs1 ++ [hh tt, hh uu]
lr3 <- runPQ msg (Proxy @v) (Proxy @w) opts a hhs2
pure $ case lr3 of
Left e -> e
Right (v,w,vv,ww) ->
let hhs3 = hhs2 ++ [hh vv, hh ww]
in mkNode opts (PresentT (p,q,r,s,t,u,v,w)) msg hhs3
instance GetOrdering cmp => P (cmp :: Ordering) a where
type PP cmp a = Ordering
eval _ opts _a =
let cmp = getOrdering @cmp
msg = "'" <> show cmp
in pure $ mkNode opts (PresentT cmp) msg []
instance KnownNat n => P (n :: Nat) a where
type PP n a = Int
eval _ opts _ =
let n = nat @n
in pure $ mkNode opts (PresentT n) ("'" <> show n) []
instance P '() a where
type PP '() a = ()
eval _ opts _ = pure $ mkNode opts (PresentT ()) "'()" []
instance P ('[] :: [k]) a where
type PP ('[] :: [k]) a = [a]
eval _ opts _ = pure $ mkNode opts (PresentT mempty) "'[]" []
instance (Show (PP p a), Show a, P p a) => P '[p] a where
type PP '[p] a = [PP p a]
eval _ opts a = do
pp <- eval (Proxy @p) opts a
let msg0 = ""
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right b -> mkNode opts (PresentT [b]) ("'" <> show0 opts "" [b] <> show1 opts " | " a) [hh pp]
instance (Show (PP p a)
, Show a
, P (p1 ': ps) a
, PP (p1 ': ps) a ~ [PP p1 a]
, P p a
, PP p a ~ PP p1 a
) => P (p ': p1 ': ps) a where
type PP (p ': p1 ': ps) a = [PP p a]
eval _ opts a = do
let msg0 = "'(p':q)"
lr <- runPQ msg0 (Proxy @p) (Proxy @(p1 ': ps)) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let ret = p:q
in mkNode opts (PresentT ret) ("'" <> show0 opts "" ret <> show1 opts " | " a) [hh pp, hh qq]
instance (Show (PP p a)
, P p a
, Show a
) => P ('Just p) (Maybe a) where
type PP ('Just p) (Maybe a) = PP p a
eval _ opts ma = do
let msg0 = "'Just"
case ma of
Just a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right b -> mkNode opts (PresentT b) (show01 opts msg0 b ma) [hh pp]
Nothing -> pure $ mkNode opts (FailT (msg0 <> " found Nothing")) (msg0 <> " found Nothing") []
instance P 'Nothing (Maybe a) where
type PP 'Nothing (Maybe a) = Proxy a
eval _ opts ma =
let msg0 = "'Nothing"
in pure $ case ma of
Nothing -> mkNode opts (PresentT Proxy) msg0 []
Just _ -> mkNode opts (FailT (msg0 <> " found Just")) (msg0 <> " found Just") []
instance (Show a
, Show (PP p a)
, P p a
) => P ('Left p) (Either a x) where
type PP ('Left p) (Either a x) = PP p a
eval _ opts lr =
let msg0 = "'Left"
in case lr of
Right _ -> pure $ mkNode opts (FailT (msg0 <> " found Right")) (msg0 <> " found Right") []
Left a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right b -> mkNode opts (_tBool pp) (show01' opts msg0 b "Left " a) [hh pp]
instance (Show a
, Show (PP p a)
, P p a
) => P ('Right p) (Either x a) where
type PP ('Right p) (Either x a) = PP p a
eval _ opts lr = do
let msg0 = "'Right"
case lr of
Left _ -> pure $ mkNode opts (FailT (msg0 <> " found Left")) (msg0 <> " found Left") []
Right a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right b -> mkNode opts (_tBool pp) (show01' opts msg0 b "Right " a) [hh pp]
instance (Show a
, Show (PP p a)
, P p a
) => P ('This p) (These a x) where
type PP ('This p) (These a x) = PP p a
eval _ opts th = do
let msg0 = "'This"
case th of
This a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right b -> mkNode opts (_tBool pp) (show01' opts msg0 b "This " a) [hh pp]
_ -> pure $ mkNode opts (FailT (msg0 <> " found " <> showThese th)) (msg0 <> " found " <> showThese th) []
instance (Show a
, Show (PP p a)
, P p a
) => P ('That p) (These x a) where
type PP ('That p) (These x a) = PP p a
eval _ opts th = do
let msg0 = "'That"
case th of
That a -> do
pp <- eval (Proxy @p) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right b -> mkNode opts (_tBool pp) (show01' opts msg0 b "That " a) [hh pp]
_ -> pure $ mkNode opts (FailT (msg0 <> " found " <> showThese th)) (msg0 <> " found " <> showThese th) []
instance (Show a
, Show b
, P p a
, P q b
, Show (PP p a)
, Show (PP q b)
) => P ('These p q) (These a b) where
type PP ('These p q) (These a b) = (PP p a, PP q b)
eval _ opts th = do
let msg0 = "'These"
case th of
These a b -> do
pp <- eval (Proxy @p) opts a
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
qq <- eval (Proxy @q) opts b
pure $ case getValueLR opts (msg0 <> " q failed p=" <> show p) qq [hh pp] of
Left e -> e
Right q ->
let ret =(p,q)
in mkNode opts (PresentT ret) (show01 opts msg0 ret (These a b)) [hh pp, hh qq]
_ -> pure $ mkNode opts (FailT (msg0 <> " found " <> showThese th)) (msg0 <> " found " <> showThese th) []
instance Show a => P 'Proxy a where
type PP 'Proxy a = Proxy a
eval _ opts a =
let b = Proxy @a
in pure $ mkNode opts (PresentT b) ("'Proxy" <> show1 opts " | " a) []
pan, pa, pu, pl, pz, pab, pub :: forall p a . (Show (PP p a), P p a) => a -> IO (BoolT (PP p a))
pz = run @'OZ @p
pl = run @'OL @p
pan = run @'OAN @p
pa = run @'OA @p
pab = run @'OAB @p
pu = run @'OU @p
pub = run @'OUB @p
run :: forall opts p a
. ( OptTC opts
, Show (PP p a)
, P p a)
=> a
-> IO (BoolT (PP p a))
run a = do
let opts = getOptT @opts
pp <- eval (Proxy @p) opts a
let r = pp ^. tBool
putStr $ prtTree' opts pp
return r
prtTree' :: Show x => POpts -> TT x -> String
prtTree' opts pp =
let r = pp ^. tBool
in case oDebug opts of
DZero -> ""
DLite ->
formatOMsg opts " >>> "
<> colorBoolT' opts r
<> " "
<> topMessage pp
<> "\n"
_ -> formatOMsg opts "\n"
<> prtTreePure opts (fromTT pp)
runPQ :: (P p a, P q a, MonadEval m)
=> String
-> Proxy p
-> Proxy q
-> POpts
-> a
-> [Holder]
-> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
runPQ msg0 proxyp proxyq opts a hhs = do
pp <- eval proxyp opts a
case getValueLR opts msg0 pp hhs of
Left e -> pure $ Left e
Right p -> do
qq <- eval proxyq opts a
pure $ case getValueLR opts msg0 qq (hhs <> [hh pp]) of
Left e -> Left e
Right q -> Right (p, q, pp, qq)
runPQBool :: (P p a, PP p a ~ Bool, P q a, PP q a ~ Bool, MonadEval m)
=> String
-> Proxy p
-> Proxy q
-> POpts
-> a
-> [Holder]
-> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
runPQBool msg0 proxyp proxyq opts a hhs = do
pp <- evalBool proxyp opts a
case getValueLR opts msg0 pp hhs of
Left e -> pure $ Left e
Right p -> do
qq <- evalBool proxyq opts a
pure $ case getValueLR opts msg0 qq (hhs <> [hh pp]) of
Left e -> Left e
Right q -> Right (p, q, pp, qq)
instance GetBoolT x b => P (b :: BoolT x) a where
type PP b a = Bool
eval _ opts _ = do
let msg0 = "'BoolT"
let ret = getBoolT @x @b
pure $ case ret of
Left b -> mkNodeB opts b (if b then "TrueT" else "FalseT") []
Right True -> mkNode opts (PresentT False) (msg0 <> " PresentT") []
Right False -> mkNode opts (FailT "'FailT _") (msg0 <> " FailT") []