{-# OPTIONS -Wall #-}
{-# OPTIONS -Wcompat #-}
{-# OPTIONS -Wincomplete-record-updates #-}
{-# OPTIONS -Wincomplete-uni-patterns #-}
{-# OPTIONS -Wredundant-constraints #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TupleSections #-}
{-# 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 (
Id
, IdT
, I
, W
, Msg
, MsgI
, Hide
, Width
, Hole
, Unproxy
, Len
, Length
, Map
, Do
, Pure
, Coerce
, OneP
, type (>>)
, pan
, panv
, pa
, pu
, pab
, pub
, pav
, puv
, pl
, pz
, run
, runs
, P(..)
, runPQ
, runPQBool
, evalBool
, evalBoolHide
, evalHide
, evalQuick
, Unwrap
, Wrap
, Wrap'
, Fail
, Failp
, Failt
, FailS
, Fst
, Snd
, Thd
, L1
, L2
, L3
, L4
, L5
, L6
, type (&&)
, type (&&~)
, type (||)
, type (||~)
, type (~>)
, Not
, Between
, All
, Any
, IdBool
, type (<..>)
, type (<<)
, Swap
, SwapC(..)
, type ($)
, type (&)
) where
import Predicate.Util
import qualified GHC.TypeLits as GL
import GHC.TypeLits (Symbol,Nat,KnownSymbol,KnownNat)
import Control.Lens
import Data.Foldable (toList)
import Data.Proxy
import Data.Typeable
import Data.Kind (Type)
import Data.These (These(..))
import Control.Monad
import Data.List
import Data.Coerce
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 @(MsgI "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 (setOtherEffects opts msg <> " ") <$> eval (Proxy @p) opts a
data MsgI prt p
instance (P prt a
, PP prt a ~ String
, P p a
) => P (MsgI prt p) a where
type PP (MsgI prt p) a = PP p a
eval _ opts a = do
pp <- eval (Proxy @prt) opts a
case getValueLR opts "MsgI" 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 .~ []
data Hole (t :: Type)
instance Typeable t => P (Hole t) a where
type PP (Hole t) a = t
eval _ opts _a =
let msg0 = "Hole(" <> showT @t <> ")"
in pure $ mkNode opts (FailT msg0) "you probably meant to get access to the type of PP only and not evaluate" []
data Width (n :: Nat) p
instance (KnownNat n
, P p a
) => P (Width n p) a where
type PP (Width n p) a = PP p a
eval _ opts a = do
let opts' = opts { oWidth = nat @n }
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) ("'" <> litL opts ("\"" <> s <> "\"")) []
instance ( P p a
, P q a
, Show (PP p a)
, Show (PP 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)) ("'(" <> showL opts p <> "," <> showL opts q <> ")") [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 a
, PP p x ~ Maybe a
, P p x
) => P ('Just p) x where
type PP ('Just p) x = MaybeT (PP p x)
eval _ opts x = do
let msg0 = "'Just"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
case p of
Nothing -> mkNode opts (FailT (msg0 <> "(empty)")) "" [hh pp]
Just d -> mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
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 ( PP p x ~ Either a b
, P p x)
=> P ('Left p) x where
type PP ('Left p) x = LeftT (PP p x)
eval _ opts x = do
let msg0 = "'Left"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
case p of
Left a -> mkNode opts (PresentT a) "Left" [hh pp]
Right _b -> mkNode opts (FailT (msg0 <> " found Right")) "" [hh pp]
instance ( PP p x ~ Either a b
, P p x)
=> P ('Right p) x where
type PP ('Right p) x = RightT (PP p x)
eval _ opts x = do
let msg0 = "'Right"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
case p of
Left _a -> mkNode opts (FailT (msg0 <> " found Left")) "" [hh pp]
Right b -> mkNode opts (PresentT b) "Right" [hh pp]
instance ( PP p x ~ These a b
, P p x)
=> P ('This p) x where
type PP ('This p) x = ThisT (PP p x)
eval _ opts x = do
let msg0 = "'This"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
case p of
This a -> mkNode opts (PresentT a) "This" [hh pp]
That _b -> mkNode opts (FailT (msg0 <> " found That")) "" [hh pp]
These _a _b -> mkNode opts (FailT (msg0 <> " found These")) "" [hh pp]
instance ( PP p x ~ These a b
, P p x)
=> P ('That p) x where
type PP ('That p) x = ThatT (PP p x)
eval _ opts x = do
let msg0 = "'That"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
case p of
This _a -> mkNode opts (FailT (msg0 <> " found This")) "" [hh pp]
That b -> mkNode opts (PresentT b) "That" [hh pp]
These _a _b -> mkNode opts (FailT (msg0 <> " found These")) "" [hh pp]
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
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 p a m
. (MonadEval m, P p a, PP p a ~ Bool)
=> 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 p a m
. (MonadEval m, P p a)
=> POpts
-> a
-> m (TT (PP p a))
evalHide opts =
if isVerbose opts then eval (Proxy @p) opts
else eval (Proxy @(Hide p)) opts
data p >> q
infixr 1 >>
instance (Show (PP p a)
, Show (PP q (PP p a))
, P p a
, P q (PP p a)
) => P (p >> q) a where
type PP (p >> q) a = PP q (PP p a)
eval _ opts a = do
let msg0 = "(>>)"
pp <- eval (Proxy @p) opts a
case getValueLR opts "(>>) lhs failed" pp [] of
Left e -> pure e
Right p -> do
qq <- eval (Proxy @q) opts p
pure $ case getValueLR opts (show p <> " (>>) rhs failed") qq [hh pp] of
Left e -> e
Right q -> mkNode opts (_tBool qq) (lit01 opts msg0 q "" (topMessageEgregious qq)) [hh pp, hh qq]
data p << q
type LeftArrowsT p q = q >> p
infixr 1 <<
instance P (LeftArrowsT p q) x => P (p << q) x where
type PP (p << q) x = PP (LeftArrowsT p q) x
eval _ = eval (Proxy @(LeftArrowsT p q))
topMessageEgregious :: TT a -> String
topMessageEgregious pp = innermost (pp ^. tString)
where innermost = ('{':) . reverse . ('}':) . takeWhile (/='{') . dropWhile (=='}') . reverse
data Unwrap p
instance (PP p x ~ s
, P p x
, Show s
, Show (Unwrapped s)
, Wrapped s
) => P (Unwrap p) x where
type PP (Unwrap p) x = Unwrapped (PP p x)
eval _ opts x = do
let msg0 = "Unwrap"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = p ^. _Wrapped'
in mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
data Wrap' t p
instance (Show (PP p x)
, P p x
, Unwrapped (PP s x) ~ PP p x
, Wrapped (PP s x)
, Show (PP s x)
) => P (Wrap' s p) x where
type PP (Wrap' s p) x = PP s x
eval _ opts x = do
let msg0 = "Wrap"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = p ^. _Unwrapped'
in mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
data Wrap (t :: Type) p
type WrapT (t :: Type) p = Wrap' (Hole t) p
instance P (WrapT t p) x => P (Wrap t p) x where
type PP (Wrap t p) x = PP (WrapT t p) x
eval _ = eval (Proxy @(WrapT t p))
data Unproxy
instance Typeable a => P Unproxy (Proxy (a :: Type)) where
type PP Unproxy (Proxy a) = a
eval _ opts _a =
let msg0 = "Unproxy(" <> showT @a <> ")"
in pure $ mkNode opts (FailT msg0) "you probably meant to get access to the type of PP only and not evaluate" []
data Len
instance ( Show a
, as ~ [a]
) => P Len as where
type PP Len as = Int
eval _ opts as =
let msg0 = "Len"
n = length as
in pure $ mkNode opts (PresentT n) (show01 opts msg0 n as) []
data Length p
instance (PP p x ~ t a
, P p x
, Show (t a)
, Foldable t) => P (Length p) x where
type PP (Length p) x = Int
eval _ opts x = do
let msg0 = "Length"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let n = length p
in mkNode opts (PresentT n) (show01 opts msg0 n p) [hh pp]
data Not p
instance ( PP p x ~ Bool
, P p x
) => P (Not p) x where
type PP (Not p) x = Bool
eval _ opts x = do
let msg0 = "Not"
pp <- evalBool (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = not p
in mkNodeB opts b (msg0 <> litVerbose opts " " (topMessage pp)) [hh pp]
data IdBool p
instance ( PP p x ~ Bool
, P p x
) => P (IdBool p) x where
type PP (IdBool p) x = Bool
eval _ opts x = do
let msg0 = "IdBool"
pp <- evalBool (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = p
in mkNodeB opts b (msg0 <> litVerbose opts " " (topMessage pp)) [hh pp]
data Fail t prt
instance (P prt a
, PP prt a ~ String
) => P (Fail t prt) a where
type PP (Fail t prt) a = PP t a
eval _ opts a = do
let msg0 = "Fail"
pp <- eval (Proxy @prt) opts a
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right s -> mkNode opts (FailT s) (msg0 <> " " <> s) [hh pp | isVerbose opts]
data FailS p
instance P (Fail I p) x => P (FailS p) x where
type PP (FailS p) x = PP (Fail I p) x
eval _ = eval (Proxy @(Fail I p))
data Failt (t :: Type) p
instance P (Fail (Hole t) p) x => P (Failt t p) x where
type PP (Failt t p) x = PP (Fail (Hole t) p) x
eval _ = eval (Proxy @(Fail (Hole t) p))
data Failp p
instance P (Fail Unproxy p) x => P (Failp p) x where
type PP (Failp p) x = PP (Fail Unproxy p) x
eval _ = eval (Proxy @(Fail Unproxy p))
data OneP p
instance (Foldable t
, PP p x ~ t a
, P p x
) => P (OneP p) x where
type PP (OneP p) x = ExtractAFromTA (PP p x)
eval _ opts x = do
let msg0 = "OneP"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p -> case toList p of
[] -> mkNode opts (FailT (msg0 <> " empty")) "expected one element" [hh pp]
[a] -> mkNode opts (PresentT a) msg0 [hh pp]
as -> let n = length as
in mkNode opts (FailT (msg0 <> " " <> show n <> " elements")) "expected one element" [hh pp]
data Between p q r
instance (Ord (PP p x)
, Show (PP p x)
, PP r x ~ PP p x
, PP r x ~ PP q x
, P p x
, P q x
, P r x
) => P (Between p q r) x where
type PP (Between p q r) x = Bool
eval _ opts x = do
let msg0 = "Between"
rr <- eval (Proxy @r) opts x
case getValueLR opts msg0 rr [] of
Left e -> pure e
Right r -> do
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x [hh rr]
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh rr, hh pp, hh qq]
in if p <= r && r <= q then mkNodeB opts True (showL opts p <> " <= " <> showL opts r <> " <= " <> showL opts q) hhs
else if p > r then mkNodeB opts False (showL opts p <> " <= " <> showL opts r) hhs
else mkNodeB opts False (showL opts r <> " <= " <> showL opts q) hhs
data p <..> q
infix 4 <..>
type BetweenT p q = Between p q Id
instance P (BetweenT p q) x => P (p <..> q) x where
type PP (p <..> q) x = PP (BetweenT p q) x
eval _ = evalBool (Proxy @(BetweenT p q))
data All p q
instance (P p a
, PP p a ~ Bool
, PP q x ~ f a
, P q x
, Show a
, Foldable f
) => P (All p q) x where
type PP (All p q) x = Bool
eval _ opts x = do
let msg0 = "All"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q ->
case chkSize opts msg0 q [hh qq] of
Left e -> pure e
Right () -> do
ts <- zipWithM (\i a -> ((i, a),) <$> evalBoolHide @p opts a) [0::Int ..] (toList q)
pure $ case splitAndAlign opts msg0 ts of
Left e -> e
Right abcs ->
let hhs = hh qq : map (hh . fixit) ts
msg1 = msg0 ++ "(" ++ show (length q) ++ ")"
in case find (not . view _1) abcs of
Nothing -> mkNodeB opts True msg1 hhs
Just (_,(i,_),tt) ->
mkNodeB opts False (msg1 <> " i=" ++ showIndex i ++ " " <> topMessage tt) hhs
data Any p q
instance (P p a
, PP p a ~ Bool
, PP q x ~ f a
, P q x
, Show a
, Foldable f
) => P (Any p q) x where
type PP (Any p q) x = Bool
eval _ opts x = do
let msg0 = "Any"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q ->
case chkSize opts msg0 q [hh qq] of
Left e -> pure e
Right () -> do
ts <- zipWithM (\i a -> ((i, a),) <$> evalBoolHide @p opts a) [0::Int ..] (toList q)
pure $ case splitAndAlign opts msg0 ts of
Left e -> e
Right abcs ->
let hhs = hh qq : map (hh . fixit) ts
msg1 = msg0 ++ "(" ++ show (length q) ++ ")"
in case find (view _1) abcs of
Nothing -> mkNodeB opts False msg1 hhs
Just (_,(i,_),tt) ->
mkNodeB opts True (msg1 <> " i=" ++ showIndex i ++ " " <> topMessage tt) hhs
data Fst p
instance (Show (ExtractL1T (PP p x))
, ExtractL1C (PP p x)
, P p x
, Show (PP p x)
) => P (Fst p) x where
type PP (Fst p) x = ExtractL1T (PP p x)
eval _ opts x = do
let msg0 = "Fst"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL1C p
in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
data L1 p
type L1T p = Fst p
instance P (L1T p) x => P (L1 p) x where
type PP (L1 p) x = PP (L1T p) x
eval _ = eval (Proxy @(L1T p))
class ExtractL1C tp where
type ExtractL1T tp
extractL1C :: tp -> ExtractL1T tp
instance ExtractL1C (a,b) where
type ExtractL1T (a,b) = a
extractL1C (a,_) = a
instance ExtractL1C (a,b,c) where
type ExtractL1T (a,b,c) = a
extractL1C (a,_,_) = a
instance ExtractL1C (a,b,c,d) where
type ExtractL1T (a,b,c,d) = a
extractL1C (a,_,_,_) = a
instance ExtractL1C (a,b,c,d,e) where
type ExtractL1T (a,b,c,d,e) = a
extractL1C (a,_,_,_,_) = a
instance ExtractL1C (a,b,c,d,e,f) where
type ExtractL1T (a,b,c,d,e,f) = a
extractL1C (a,_,_,_,_,_) = a
data Snd p
instance (Show (ExtractL2T (PP p x))
, ExtractL2C (PP p x)
, P p x
, Show (PP p x)
) => P (Snd p) x where
type PP (Snd p) x = ExtractL2T (PP p x)
eval _ opts x = do
let msg0 = "Snd"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL2C p
in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
data L2 p
type L2T p = Snd p
instance P (L2T p) x => P (L2 p) x where
type PP (L2 p) x = PP (L2T p) x
eval _ = eval (Proxy @(L2T p))
class ExtractL2C tp where
type ExtractL2T tp
extractL2C :: tp -> ExtractL2T tp
instance ExtractL2C (a,b) where
type ExtractL2T (a,b) = b
extractL2C (_,b) = b
instance ExtractL2C (a,b,c) where
type ExtractL2T (a,b,c) = b
extractL2C (_,b,_) = b
instance ExtractL2C (a,b,c,d) where
type ExtractL2T (a,b,c,d) = b
extractL2C (_,b,_,_) = b
instance ExtractL2C (a,b,c,d,e) where
type ExtractL2T (a,b,c,d,e) = b
extractL2C (_,b,_,_,_) = b
instance ExtractL2C (a,b,c,d,e,f) where
type ExtractL2T (a,b,c,d,e,f) = b
extractL2C (_,b,_,_,_,_) = b
data Thd p
instance (Show (ExtractL3T (PP p x))
, ExtractL3C (PP p x)
, P p x
, Show (PP p x)
) => P (Thd p) x where
type PP (Thd p) x = ExtractL3T (PP p x)
eval _ opts x = do
let msg0 = "Thd"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL3C p
in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
data L3 p
type L3T p = Thd p
instance P (L3T p) x => P (L3 p) x where
type PP (L3 p) x = PP (L3T p) x
eval _ = eval (Proxy @(L3T p))
class ExtractL3C tp where
type ExtractL3T tp
extractL3C :: tp -> ExtractL3T tp
instance ExtractL3C (a,b) where
type ExtractL3T (a,b) = GL.TypeError ('GL.Text "Thd doesn't work for 2-tuples")
extractL3C _ = errorInProgram "Thd doesn't work for 2-tuples"
instance ExtractL3C (a,b,c) where
type ExtractL3T (a,b,c) = c
extractL3C (_,_,c) = c
instance ExtractL3C (a,b,c,d) where
type ExtractL3T (a,b,c,d) = c
extractL3C (_,_,c,_) = c
instance ExtractL3C (a,b,c,d,e) where
type ExtractL3T (a,b,c,d,e) = c
extractL3C (_,_,c,_,_) = c
instance ExtractL3C (a,b,c,d,e,f) where
type ExtractL3T (a,b,c,d,e,f) = c
extractL3C (_,_,c,_,_,_) = c
data L4 p
instance (Show (ExtractL4T (PP p x))
, ExtractL4C (PP p x)
, P p x
, Show (PP p x)
) => P (L4 p) x where
type PP (L4 p) x = ExtractL4T (PP p x)
eval _ opts x = do
let msg0 = "L4"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL4C p
in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
class ExtractL4C tp where
type ExtractL4T tp
extractL4C :: tp -> ExtractL4T tp
instance ExtractL4C (a,b) where
type ExtractL4T (a,b) = GL.TypeError ('GL.Text "L4 doesn't work for 2-tuples")
extractL4C _ = errorInProgram "L4 doesn't work for 2-tuples"
instance ExtractL4C (a,b,c) where
type ExtractL4T (a,b,c) = GL.TypeError ('GL.Text "L4 doesn't work for 3-tuples")
extractL4C _ = errorInProgram "L4 doesn't work for 3-tuples"
instance ExtractL4C (a,b,c,d) where
type ExtractL4T (a,b,c,d) = d
extractL4C (_,_,_,d) = d
instance ExtractL4C (a,b,c,d,e) where
type ExtractL4T (a,b,c,d,e) = d
extractL4C (_,_,_,d,_) = d
instance ExtractL4C (a,b,c,d,e,f) where
type ExtractL4T (a,b,c,d,e,f) = d
extractL4C (_,_,_,d,_,_) = d
data L5 p
instance (Show (ExtractL5T (PP p x))
, ExtractL5C (PP p x)
, P p x
, Show (PP p x)
) => P (L5 p) x where
type PP (L5 p) x = ExtractL5T (PP p x)
eval _ opts x = do
let msg0 = "L5"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL5C p
in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
class ExtractL5C tp where
type ExtractL5T tp
extractL5C :: tp -> ExtractL5T tp
instance ExtractL5C (a,b) where
type ExtractL5T (a,b) = GL.TypeError ('GL.Text "L5 doesn't work for 2-tuples")
extractL5C _ = errorInProgram "L5 doesn't work for 2-tuples"
instance ExtractL5C (a,b,c) where
type ExtractL5T (a,b,c) = GL.TypeError ('GL.Text "L5 doesn't work for 3-tuples")
extractL5C _ = errorInProgram "L5 doesn't work for 3-tuples"
instance ExtractL5C (a,b,c,d) where
type ExtractL5T (a,b,c,d) = GL.TypeError ('GL.Text "L5 doesn't work for 4-tuples")
extractL5C _ = errorInProgram "L5 doesn't work for 4-tuples"
instance ExtractL5C (a,b,c,d,e) where
type ExtractL5T (a,b,c,d,e) = e
extractL5C (_,_,_,_,e) = e
instance ExtractL5C (a,b,c,d,e,f) where
type ExtractL5T (a,b,c,d,e,f) = e
extractL5C (_,_,_,_,e,_) = e
data L6 p
instance (Show (ExtractL6T (PP p x))
, ExtractL6C (PP p x)
, P p x
, Show (PP p x)
) => P (L6 p) x where
type PP (L6 p) x = ExtractL6T (PP p x)
eval _ opts x = do
let msg0 = "L6"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = extractL6C p
in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
class ExtractL6C tp where
type ExtractL6T tp
extractL6C :: tp -> ExtractL6T tp
instance ExtractL6C (a,b) where
type ExtractL6T (a,b) = GL.TypeError ('GL.Text "L6 doesn't work for 2-tuples")
extractL6C _ = errorInProgram "L6 doesn't work for 2-tuples"
instance ExtractL6C (a,b,c) where
type ExtractL6T (a,b,c) = GL.TypeError ('GL.Text "L6 doesn't work for 3-tuples")
extractL6C _ = errorInProgram "L6 doesn't work for 3-tuples"
instance ExtractL6C (a,b,c,d) where
type ExtractL6T (a,b,c,d) = GL.TypeError ('GL.Text "L6 doesn't work for 4-tuples")
extractL6C _ = errorInProgram "L6 doesn't work for 4-tuples"
instance ExtractL6C (a,b,c,d,e) where
type ExtractL6T (a,b,c,d,e) = GL.TypeError ('GL.Text "L6 doesn't work for 5-tuples")
extractL6C _ = errorInProgram "L6 doesn't work for 5-tuples"
instance ExtractL6C (a,b,c,d,e,f) where
type ExtractL6T (a,b,c,d,e,f) = f
extractL6C (_,_,_,_,_,f) = f
data Both p q
instance ( ExtractL1C (PP q x)
, ExtractL2C (PP q x)
, P p (ExtractL1T (PP q x))
, P p (ExtractL2T (PP q x))
, P q x
) => P (Both p q) x where
type PP (Both p q) x = (PP p (ExtractL1T (PP q x)), PP p (ExtractL2T (PP q x)))
eval _ opts x = do
let msg0 = "Both"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
let (a,a') = (extractL1C q, extractL2C q)
pp <- eval (Proxy @p) opts a
case getValueLR opts msg0 pp [hh qq] of
Left e -> pure e
Right b -> do
pp' <- eval (Proxy @p) opts a'
pure $ case getValueLR opts msg0 pp' [hh qq, hh pp] of
Left e -> e
Right b' ->
mkNode opts (PresentT (b,b')) msg0 [hh qq, hh pp, hh pp']
data Map p q
instance (Show (PP p a)
, P p a
, PP q x ~ f a
, P q x
, Show a
, Show (f a)
, Foldable f
) => P (Map p q) x where
type PP (Map p q) x = [PP p (ExtractAFromTA (PP q x))]
eval _ opts x = do
let msg0 = "Map"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q -> do
ts <- zipWithM (\i a -> ((i, a),) <$> evalHide @p opts a) [0::Int ..] (toList q)
pure $ case splitAndAlign opts msg0 ts of
Left e -> e
Right abcs ->
let vals = map (view _1) abcs
in mkNode opts (PresentT vals) (show01 opts msg0 vals q) (hh qq : map (hh . fixit) ts)
data Do (ps :: [k])
instance (P (DoExpandT ps) a) => P (Do ps) a where
type PP (Do ps) a = PP (DoExpandT ps) a
eval _ = eval (Proxy @(DoExpandT ps))
type family DoExpandT (ps :: [k]) :: Type where
DoExpandT '[] = GL.TypeError ('GL.Text "'[] invalid: requires at least one predicate in the list")
DoExpandT '[p] = Id >> p
DoExpandT (p ': p1 ': ps) = p >> DoExpandT (p1 ': ps)
data p && q
infixr 3 &&
instance (P p a
, P q a
, PP p a ~ Bool
, PP q a ~ Bool
) => P (p && q) a where
type PP (p && q) a = Bool
eval _ opts a = do
let msg0 = "&&"
lr <- runPQBool msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let zz = case (p,q) of
(True, True) -> ""
(False, True) -> topMessage pp
(True, False) -> topMessage qq
(False, False) -> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
in mkNodeB opts (p&&q) (showL opts p <> " " <> msg0 <> " " <> showL opts q <> (if null zz then zz else " | " <> zz)) [hh pp, hh qq]
data p &&~ q
infixr 3 &&~
instance (P p a
, P q a
, PP p a ~ Bool
, PP q a ~ Bool
) => P (p &&~ q) a where
type PP (p &&~ q) a = Bool
eval _ opts a = do
let msg0 = "&&~"
pp <- eval (Proxy @p) opts a
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right False ->
pure $ mkNodeB opts False ("False " <> msg0 <> " _" <> litVerbose opts " | " (topMessage pp)) [hh pp]
Right True -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts msg0 qq [hh pp] of
Left e -> e
Right q ->
let zz = if q then ""
else " | " <> topMessage qq
in mkNodeB opts q ("True " <> msg0 <> " " <> showL opts q <> litVerbose opts "" zz) [hh pp, hh qq]
data p || q
infixr 2 ||
instance (P p a
, P q a
, PP p a ~ Bool
, PP q a ~ Bool
) => P (p || q) a where
type PP (p || q) a = Bool
eval _ opts a = do
let msg0 = "||"
lr <- runPQBool msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let zz = case (p,q) of
(False,False) -> " | " <> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
_ -> ""
in mkNodeB opts (p||q) (showL opts p <> " " <> msg0 <> " " <> showL opts q <> zz) [hh pp, hh qq]
data p ||~ q
infixr 2 ||~
instance (P p a
, P q a
, PP p a ~ Bool
, PP q a ~ Bool
) => P (p ||~ q) a where
type PP (p ||~ q) a = Bool
eval _ opts a = do
let msg0 = "||~"
pp <- eval (Proxy @p) opts a
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right False -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts msg0 qq [hh pp] of
Left e -> e
Right q ->
let zz = if q then ""
else " | " <> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
in mkNodeB opts q ("False " <> msg0 <> " " <> showL opts q <> litVerbose opts "" zz) [hh pp, hh qq]
Right True ->
pure $ mkNodeB opts True ("True " <> msg0 <> " _" <> litVerbose opts " | " (topMessage pp)) [hh pp]
data p ~> q
infixr 1 ~>
instance (P p a
, P q a
, PP p a ~ Bool
, PP q a ~ Bool
) => P (p ~> q) a where
type PP (p ~> q) a = Bool
eval _ opts a = do
let msg0 = "~>"
lr <- runPQBool msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let zz = case (p,q) of
(True,False) -> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
_ -> ""
in mkNodeB opts (p~>q) (showL opts p <> " " <> msg0 <> " " <> showL opts q <> (if null zz then zz else " | " <> zz)) [hh pp, hh qq]
data Swap
class Bifunctor p => SwapC p where
swapC :: p a b -> p b a
instance SwapC Either where
swapC (Left a) = Right a
swapC (Right a) = Left a
instance SwapC These where
swapC (This a) = That a
swapC (That b) = This b
swapC (These a b) = These b a
instance SwapC (,) where
swapC (a,b) = (b,a)
instance (Show (p a b)
, SwapC p
, Show (p b a)
) => P Swap (p a b) where
type PP Swap (p a b) = p b a
eval _ opts pabx =
let msg0 = "Swap"
d = swapC pabx
in pure $ mkNode opts (PresentT d) (show01 opts msg0 d pabx) []
data (p :: k -> k1) $ (q :: k)
infixr 0 $
instance P (p q) a => P (p $ q) a where
type PP (p $ q) a = PP (p q) a
eval _ = eval (Proxy @(p q))
data (q :: k) & (p :: k -> k1)
infixl 1 &
instance P (p q) a => P (q & p) a where
type PP (q & p) a = PP (p q) a
eval _ = eval (Proxy @(p q))
data Pure (t :: Type -> Type) p
instance (P p x
, Show (PP p x)
, Show (t (PP p x))
, Applicative t
) => P (Pure t p) x where
type PP (Pure t p) x = t (PP p x)
eval _ opts x = do
let msg0 = "Pure"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right a ->
let b = pure a
in mkNode opts (PresentT b) (show01 opts msg0 b a) [hh pp]
data Coerce (t :: k)
instance (Show a
, Show t
, Coercible t a
) => P (Coerce t) a where
type PP (Coerce t) a = t
eval _ opts a =
let msg0 = "Coerce"
d = a ^. coerced
in pure $ mkNode opts (PresentT d) (show01 opts msg0 d a) []