{-# 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
, Hide
, pan
, panv
, pa
, pu
, pab
, pub
, pav
, puv
, pl
, pz
, run
, runs
, P(..)
, runPQ
, runPQBool
, evalBool
, evalBoolHide
, evalHide
, 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 <> " " <> showL 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 <> " " <> showL 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
data Hide p
instance P p x => P (Hide p) x where
type PP (Hide p) x = PP p x
eval _ opts x = do
tt <- eval (Proxy @p) opts x
pure $ tt & tForest .~ []
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) ("'" <> litL 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]) ("'" <> showL opts [b] <> showVerbose 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)"
pp <- eval (Proxy @p) opts a
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
qq <- eval (Proxy @(p1 ': ps)) opts a
pure $ case getValueLR opts msg0 qq [hh pp] of
Left e -> e
Right q ->
let ret = p:q
in mkNode opts (PresentT ret) ("'" <> showL opts ret <> litVerbose opts " " (topMessage pp) <> showVerbose opts " | " a) ([hh pp | isVerbose opts] <> [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")) "" []
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")) "" []
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")) "" []
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")) "" []
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)) "" []
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)) "" []
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=" <> showL opts 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)) "" []
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" <> showVerbose opts " | " a) []
instance GetBoolT x b => P (b :: BoolT x) a where
type PP b a = Bool
eval _ opts _ = do
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) "'PresentT _" []
Right False -> mkNode opts (FailT "'FailT _") "BoolT" []
pan, panv, pa, pu, pl, pz, pab, pub, pav, puv
:: 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
panv = run @OANV @p
pa = run @OA @p
pab = run @OAB @p
pav = run @OAV @p
pu = run @OU @p
pub = run @OUB @p
puv = run @OUV @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
runs :: forall optss p a
. ( OptTC (OptTT optss)
, Show (PP p a)
, P p a)
=> a
-> IO (BoolT (PP p a))
runs = run @(OptTT optss) @p
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
-> proxy1 p
-> proxy2 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
-> proxy1 p
-> proxy2 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)
evalBoolHide :: forall m p a proxy
. (MonadEval m, P p a, PP p a ~ Bool)
=> proxy p
-> POpts
-> a
-> m (TT (PP p a))
evalBoolHide _ opts =
if isVerbose opts then evalBool (Proxy @p) opts
else evalBool (Proxy @(Hide p)) opts
evalHide :: forall m p a proxy
. (MonadEval m, P p a)
=> proxy p
-> POpts
-> a
-> m (TT (PP p a))
evalHide _ opts =
if isVerbose opts then eval (Proxy @p) opts
else eval (Proxy @(Hide p)) opts