{-# 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 NoStarIsType #-}
{-# LANGUAGE EmptyDataDeriving #-}
module Predicate.Data.Index (
Ix
, Ix'
, IxL
, type (!!)
, type (!!?)
, Lookup
, LookupDef
, LookupDef'
, LookupFail
, LookupFail'
) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Predicate.Data.Maybe (JustDef, JustFail)
import Control.Lens
import GHC.TypeLits (Nat, KnownNat)
import Data.Proxy (Proxy(..))
data LookupDef' v w p q deriving Int -> LookupDef' v w p q -> ShowS
[LookupDef' v w p q] -> ShowS
LookupDef' v w p q -> String
(Int -> LookupDef' v w p q -> ShowS)
-> (LookupDef' v w p q -> String)
-> ([LookupDef' v w p q] -> ShowS)
-> Show (LookupDef' v w p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
Int -> LookupDef' v w p q -> ShowS
forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
[LookupDef' v w p q] -> ShowS
forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
LookupDef' v w p q -> String
showList :: [LookupDef' v w p q] -> ShowS
$cshowList :: forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
[LookupDef' v w p q] -> ShowS
show :: LookupDef' v w p q -> String
$cshow :: forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
LookupDef' v w p q -> String
showsPrec :: Int -> LookupDef' v w p q -> ShowS
$cshowsPrec :: forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
Int -> LookupDef' v w p q -> ShowS
Show
type LookupDefT' v w p q = JustDef p (q >> Lookup v w)
instance P (LookupDefT' v w p q) x => P (LookupDef' v w p q) x where
type PP (LookupDef' v w p q) x = PP (LookupDefT' v w p q) x
eval :: proxy (LookupDef' v w p q)
-> POpts -> x -> m (TT (PP (LookupDef' v w p q) x))
eval proxy (LookupDef' v w p q)
_ = Proxy (LookupDefT' v w p q)
-> POpts -> x -> m (TT (PP (LookupDefT' v w p q) 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 (LookupDefT' v w p q)
forall k (t :: k). Proxy t
Proxy @(LookupDefT' v w p q))
data LookupDef v w p deriving Int -> LookupDef v w p -> ShowS
[LookupDef v w p] -> ShowS
LookupDef v w p -> String
(Int -> LookupDef v w p -> ShowS)
-> (LookupDef v w p -> String)
-> ([LookupDef v w p] -> ShowS)
-> Show (LookupDef v w p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (v :: k) k (w :: k) k (p :: k).
Int -> LookupDef v w p -> ShowS
forall k (v :: k) k (w :: k) k (p :: k). [LookupDef v w p] -> ShowS
forall k (v :: k) k (w :: k) k (p :: k). LookupDef v w p -> String
showList :: [LookupDef v w p] -> ShowS
$cshowList :: forall k (v :: k) k (w :: k) k (p :: k). [LookupDef v w p] -> ShowS
show :: LookupDef v w p -> String
$cshow :: forall k (v :: k) k (w :: k) k (p :: k). LookupDef v w p -> String
showsPrec :: Int -> LookupDef v w p -> ShowS
$cshowsPrec :: forall k (v :: k) k (w :: k) k (p :: k).
Int -> LookupDef v w p -> ShowS
Show
type LookupDefT v w p = LookupDef' v w p Id
instance P (LookupDefT v w p) x => P (LookupDef v w p) x where
type PP (LookupDef v w p) x = PP (LookupDefT v w p) x
eval :: proxy (LookupDef v w p)
-> POpts -> x -> m (TT (PP (LookupDef v w p) x))
eval proxy (LookupDef v w p)
_ = Proxy (LookupDefT v w p)
-> POpts -> x -> m (TT (PP (LookupDefT v w 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 (LookupDefT v w p)
forall k (t :: k). Proxy t
Proxy @(LookupDefT v w p))
data LookupFail' msg v w q deriving Int -> LookupFail' msg v w q -> ShowS
[LookupFail' msg v w q] -> ShowS
LookupFail' msg v w q -> String
(Int -> LookupFail' msg v w q -> ShowS)
-> (LookupFail' msg v w q -> String)
-> ([LookupFail' msg v w q] -> ShowS)
-> Show (LookupFail' msg v w q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
Int -> LookupFail' msg v w q -> ShowS
forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
[LookupFail' msg v w q] -> ShowS
forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
LookupFail' msg v w q -> String
showList :: [LookupFail' msg v w q] -> ShowS
$cshowList :: forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
[LookupFail' msg v w q] -> ShowS
show :: LookupFail' msg v w q -> String
$cshow :: forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
LookupFail' msg v w q -> String
showsPrec :: Int -> LookupFail' msg v w q -> ShowS
$cshowsPrec :: forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
Int -> LookupFail' msg v w q -> ShowS
Show
type LookupFailT' msg v w q = JustFail msg (q >> Lookup v w)
instance P (LookupFailT' msg v w q) x => P (LookupFail' msg v w q) x where
type PP (LookupFail' msg v w q) x = PP (LookupFailT' msg v w q) x
eval :: proxy (LookupFail' msg v w q)
-> POpts -> x -> m (TT (PP (LookupFail' msg v w q) x))
eval proxy (LookupFail' msg v w q)
_ = Proxy (LookupFailT' msg v w q)
-> POpts -> x -> m (TT (PP (LookupFailT' msg v w q) 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 (LookupFailT' msg v w q)
forall k (t :: k). Proxy t
Proxy @(LookupFailT' msg v w q))
data LookupFail msg v w deriving Int -> LookupFail msg v w -> ShowS
[LookupFail msg v w] -> ShowS
LookupFail msg v w -> String
(Int -> LookupFail msg v w -> ShowS)
-> (LookupFail msg v w -> String)
-> ([LookupFail msg v w] -> ShowS)
-> Show (LookupFail msg v w)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (msg :: k) k (v :: k) k (w :: k).
Int -> LookupFail msg v w -> ShowS
forall k (msg :: k) k (v :: k) k (w :: k).
[LookupFail msg v w] -> ShowS
forall k (msg :: k) k (v :: k) k (w :: k).
LookupFail msg v w -> String
showList :: [LookupFail msg v w] -> ShowS
$cshowList :: forall k (msg :: k) k (v :: k) k (w :: k).
[LookupFail msg v w] -> ShowS
show :: LookupFail msg v w -> String
$cshow :: forall k (msg :: k) k (v :: k) k (w :: k).
LookupFail msg v w -> String
showsPrec :: Int -> LookupFail msg v w -> ShowS
$cshowsPrec :: forall k (msg :: k) k (v :: k) k (w :: k).
Int -> LookupFail msg v w -> ShowS
Show
type LookupFailT msg v w = LookupFail' msg v w Id
instance P (LookupFailT msg v w) x => P (LookupFail msg v w) x where
type PP (LookupFail msg v w) x = PP (LookupFailT msg v w) x
eval :: proxy (LookupFail msg v w)
-> POpts -> x -> m (TT (PP (LookupFail msg v w) x))
eval proxy (LookupFail msg v w)
_ = Proxy (LookupFailT msg v w)
-> POpts -> x -> m (TT (PP (LookupFailT msg v w) 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 (LookupFailT msg v w)
forall k (t :: k). Proxy t
Proxy @(LookupFailT msg v w))
data Ix (n :: Nat) def deriving Int -> Ix n def -> ShowS
[Ix n def] -> ShowS
Ix n def -> String
(Int -> Ix n def -> ShowS)
-> (Ix n def -> String) -> ([Ix n def] -> ShowS) -> Show (Ix n def)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) k (def :: k). Int -> Ix n def -> ShowS
forall (n :: Nat) k (def :: k). [Ix n def] -> ShowS
forall (n :: Nat) k (def :: k). Ix n def -> String
showList :: [Ix n def] -> ShowS
$cshowList :: forall (n :: Nat) k (def :: k). [Ix n def] -> ShowS
show :: Ix n def -> String
$cshow :: forall (n :: Nat) k (def :: k). Ix n def -> String
showsPrec :: Int -> Ix n def -> ShowS
$cshowsPrec :: forall (n :: Nat) k (def :: k). Int -> Ix n def -> ShowS
Show
instance ( P def (Proxy a)
, PP def (Proxy a) ~ a
, KnownNat n
, Show a
, [a] ~ x
) => P (Ix n def) x where
type PP (Ix n def) x = ExtractAFromTA x
eval :: proxy (Ix n def) -> POpts -> x -> m (TT (PP (Ix n def) x))
eval proxy (Ix n def)
_ POpts
opts x
as = do
let n :: Int
n = forall a. (KnownNat n, Num a) => a
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n
msg0 :: String
msg0 = String
"Ix(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
case x
as x -> Getting (First a) x a -> Maybe a
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index x -> Traversal' x (IxValue x)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Int
Index x
n of
Maybe a
Nothing -> do
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" not found"
TT a
pp <- Proxy def -> POpts -> Proxy a -> m (TT (PP def (Proxy a)))
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 def
forall k (t :: k). Proxy t
Proxy @def) POpts
opts (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
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 a -> [Tree PE] -> Either (TT a) a
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
Inline POpts
opts String
msg1 TT a
pp [] of
Left TT a
e -> TT a
e
Right a
_ -> POpts -> TT a -> String -> [Tree PE] -> TT a
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT a
pp String
msg1 [TT a -> Tree PE
forall a. TT a -> Tree PE
hh TT a
pp]
Just a
a -> 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
a) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a) []
data Ix' (n :: Nat) deriving Int -> Ix' n -> ShowS
[Ix' n] -> ShowS
Ix' n -> String
(Int -> Ix' n -> ShowS)
-> (Ix' n -> String) -> ([Ix' n] -> ShowS) -> Show (Ix' n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat). Int -> Ix' n -> ShowS
forall (n :: Nat). [Ix' n] -> ShowS
forall (n :: Nat). Ix' n -> String
showList :: [Ix' n] -> ShowS
$cshowList :: forall (n :: Nat). [Ix' n] -> ShowS
show :: Ix' n -> String
$cshow :: forall (n :: Nat). Ix' n -> String
showsPrec :: Int -> Ix' n -> ShowS
$cshowsPrec :: forall (n :: Nat). Int -> Ix' n -> ShowS
Show
type IxT' (n :: Nat) = Ix n (FailP "Ix index not found")
instance P (IxT' n) x => P (Ix' n) x where
type PP (Ix' n) x = PP (IxT' n) x
eval :: proxy (Ix' n) -> POpts -> x -> m (TT (PP (Ix' n) x))
eval proxy (Ix' n)
_ = Proxy (IxT' n) -> POpts -> x -> m (TT (PP (IxT' n) 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 (IxT' n)
forall k (t :: k). Proxy t
Proxy @(IxT' n))
data IxL p q def deriving Int -> IxL p q def -> ShowS
[IxL p q def] -> ShowS
IxL p q def -> String
(Int -> IxL p q def -> ShowS)
-> (IxL p q def -> String)
-> ([IxL p q def] -> ShowS)
-> Show (IxL p q def)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k) k (def :: k).
Int -> IxL p q def -> ShowS
forall k (p :: k) k (q :: k) k (def :: k). [IxL p q def] -> ShowS
forall k (p :: k) k (q :: k) k (def :: k). IxL p q def -> String
showList :: [IxL p q def] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (def :: k). [IxL p q def] -> ShowS
show :: IxL p q def -> String
$cshow :: forall k (p :: k) k (q :: k) k (def :: k). IxL p q def -> String
showsPrec :: Int -> IxL p q def -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (def :: k).
Int -> IxL p q def -> ShowS
Show
instance ( P q a
, P p a
, Show (PP p a)
, Ixed (PP p a)
, PP q a ~ Index (PP p a)
, Show (Index (PP p a))
, Show (IxValue (PP p a))
, P r (Proxy (IxValue (PP p a)))
, PP r (Proxy (IxValue (PP p a))) ~ IxValue (PP p a)
)
=> P (IxL p q r) a where
type PP (IxL p q r) a = IxValue (PP p a)
eval :: proxy (IxL p q r) -> POpts -> a -> m (TT (PP (IxL p q r) a))
eval proxy (IxL p q r)
_ POpts
opts a
a = do
let msg0 :: String
msg0 = String
"IxL"
Either
(TT (IxValue (PP p a)))
(PP p a, Index (PP p a), TT (PP p a), TT (Index (PP p a)))
lr <- Inline
-> String
-> Proxy p
-> Proxy q
-> POpts
-> a
-> [Tree PE]
-> m (Either
(TT (IxValue (PP p a))) (PP p a, PP q a, TT (PP p a), TT (PP q 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 p
forall k (t :: k). Proxy t
Proxy @p) (Proxy q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts a
a []
case Either
(TT (IxValue (PP p a)))
(PP p a, Index (PP p a), TT (PP p a), TT (Index (PP p a)))
lr of
Left TT (IxValue (PP p a))
e -> TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (IxValue (PP p a))
e
Right (PP p a
p,Index (PP p a)
q,TT (PP p a)
pp,TT (Index (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 -> Index (PP p a) -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts Index (PP p a)
q String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
in case PP p a
p PP p a
-> Getting (First (IxValue (PP p a))) (PP p a) (IxValue (PP p a))
-> Maybe (IxValue (PP p a))
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index (PP p a) -> Traversal' (PP p a) (IxValue (PP p a))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (PP p a)
q of
Maybe (IxValue (PP p a))
Nothing -> do
TT (IxValue (PP p a))
rr <- Proxy r
-> POpts
-> Proxy (IxValue (PP p a))
-> m (TT (PP r (Proxy (IxValue (PP p a)))))
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 r
forall k (t :: k). Proxy t
Proxy @r) POpts
opts (Proxy (IxValue (PP p a))
forall k (t :: k). Proxy t
Proxy @(IxValue (PP p a)))
TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a))))
-> TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (IxValue (PP p a))
-> [Tree PE]
-> Either (TT (IxValue (PP p a))) (IxValue (PP p a))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
Inline POpts
opts String
msg1 TT (IxValue (PP p a))
rr [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp, TT (Index (PP p a)) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Index (PP p a))
qq] of
Left TT (IxValue (PP p a))
e -> TT (IxValue (PP p a))
e
Right IxValue (PP p a)
_ -> POpts
-> TT (IxValue (PP p a))
-> String
-> [Tree PE]
-> TT (IxValue (PP p a))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (IxValue (PP p a))
rr (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" index not found") [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp, TT (Index (PP p a)) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Index (PP p a))
qq]
Just IxValue (PP p a)
ret -> TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a))))
-> TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a)))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (IxValue (PP p a))
-> String
-> [Tree PE]
-> TT (IxValue (PP p a))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (IxValue (PP p a) -> Val (IxValue (PP p a))
forall a. a -> Val a
Val IxValue (PP p a)
ret) (POpts -> String -> IxValue (PP p a) -> String -> PP p a -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> String -> a2 -> String
show3' POpts
opts String
msg1 IxValue (PP p a)
ret String
"p=" PP p a
p String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> Index (PP p a) -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | q=" Index (PP p a)
q) [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp, TT (Index (PP p a)) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Index (PP p a))
qq]
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
type BangBangT p q = IxL p q (FailP "(!!) index not found")
instance P (BangBangT p q) a => P (p !! q) a where
type PP (p !! q) a = PP (BangBangT p q) a
eval :: proxy (p !! q) -> POpts -> a -> m (TT (PP (p !! q) a))
eval proxy (p !! q)
_ = Proxy (BangBangT p q)
-> POpts -> a -> m (TT (PP (BangBangT p q) a))
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 (BangBangT p q)
forall k (t :: k). Proxy t
Proxy @(BangBangT p q))
data Lookup p q deriving Int -> Lookup p q -> ShowS
[Lookup p q] -> ShowS
Lookup p q -> String
(Int -> Lookup p q -> ShowS)
-> (Lookup p q -> String)
-> ([Lookup p q] -> ShowS)
-> Show (Lookup p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> Lookup p q -> ShowS
forall k (p :: k) k (q :: k). [Lookup p q] -> ShowS
forall k (p :: k) k (q :: k). Lookup p q -> String
showList :: [Lookup p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [Lookup p q] -> ShowS
show :: Lookup p q -> String
$cshow :: forall k (p :: k) k (q :: k). Lookup p q -> String
showsPrec :: Int -> Lookup p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> Lookup p q -> ShowS
Show
instance ( P p a
, P q a
, Show (PP q a)
, Ixed (PP q a)
, PP p a ~ Index (PP q a)
, Show (Index (PP q a))
, Show (IxValue (PP q a))
)
=> P (Lookup p q) a where
type PP (Lookup p q) a = Maybe (IxValue (PP q a))
eval :: proxy (Lookup p q) -> POpts -> a -> m (TT (PP (Lookup p q) a))
eval proxy (Lookup p q)
_ POpts
opts a
a = do
let msg0 :: String
msg0 = String
"Lookup"
Either
(TT (Maybe (IxValue (PP q a))))
(Index (PP q a), PP q a, TT (Index (PP q a)), TT (PP q a))
lr <- Inline
-> String
-> Proxy p
-> Proxy q
-> POpts
-> a
-> [Tree PE]
-> m (Either
(TT (Maybe (IxValue (PP q a))))
(PP p a, PP q a, TT (PP p a), TT (PP q 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 p
forall k (t :: k). Proxy t
Proxy @p) (Proxy q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts a
a []
TT (Maybe (IxValue (PP q a))) -> m (TT (Maybe (IxValue (PP q a))))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Maybe (IxValue (PP q a)))
-> m (TT (Maybe (IxValue (PP q a)))))
-> TT (Maybe (IxValue (PP q a)))
-> m (TT (Maybe (IxValue (PP q a))))
forall a b. (a -> b) -> a -> b
$ case Either
(TT (Maybe (IxValue (PP q a))))
(Index (PP q a), PP q a, TT (Index (PP q a)), TT (PP q a))
lr of
Left TT (Maybe (IxValue (PP q a)))
e -> TT (Maybe (IxValue (PP q a)))
e
Right (Index (PP q a)
p,PP q a
q,TT (Index (PP q a))
pp,TT (PP q 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 -> Index (PP q a) -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts Index (PP q a)
p String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
hhs :: [Tree PE]
hhs = [TT (Index (PP q a)) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Index (PP q a))
pp, TT (PP q a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q a)
qq]
in case PP q a
q PP q a
-> Getting (First (IxValue (PP q a))) (PP q a) (IxValue (PP q a))
-> Maybe (IxValue (PP q a))
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index (PP q a) -> Traversal' (PP q a) (IxValue (PP q a))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (PP q a)
p of
Maybe (IxValue (PP q a))
Nothing -> POpts
-> Val (Maybe (IxValue (PP q a)))
-> String
-> [Tree PE]
-> TT (Maybe (IxValue (PP q a)))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Maybe (IxValue (PP q a)) -> Val (Maybe (IxValue (PP q a)))
forall a. a -> Val a
Val Maybe (IxValue (PP q a))
forall a. Maybe a
Nothing) (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" not found") [Tree PE]
hhs
Just IxValue (PP q a)
ret -> POpts
-> Val (Maybe (IxValue (PP q a)))
-> String
-> [Tree PE]
-> TT (Maybe (IxValue (PP q a)))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Maybe (IxValue (PP q a)) -> Val (Maybe (IxValue (PP q a)))
forall a. a -> Val a
Val (IxValue (PP q a) -> Maybe (IxValue (PP q a))
forall a. a -> Maybe a
Just IxValue (PP q a)
ret)) (POpts -> String -> IxValue (PP q a) -> String -> PP q a -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> String -> a2 -> String
show3' POpts
opts String
msg1 IxValue (PP q a)
ret String
"q=" PP q a
q String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> Index (PP q a) -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | p=" Index (PP q a)
p) [Tree PE]
hhs
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
type BangBangQT p q = Lookup q p
instance P (BangBangQT p q) a => P (p !!? q) a where
type PP (p !!? q) a = PP (BangBangQT p q) a
eval :: proxy (p !!? q) -> POpts -> a -> m (TT (PP (p !!? q) a))
eval proxy (p !!? q)
_ = Proxy (BangBangQT p q)
-> POpts -> a -> m (TT (PP (BangBangQT p q) a))
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 (BangBangQT p q)
forall k (t :: k). Proxy t
Proxy @(BangBangQT p q))