{-# OPTIONS -Wall #-} {-# OPTIONS -Wno-compat #-} {-# 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 GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE NoOverloadedLists #-} {-# LANGUAGE NoStarIsType #-} {- | promoted indexing functions -} module Predicate.Data.Index ( -- ** indexing expressions Ix , Ix' , IxL , type (!!) , type (!!?) , Lookup , LookupDef , LookupDef' , LookupFail , LookupFail' -- ** list to tuples , Tuple2 , Tuple3 , Tuple4 , Tuple5 , Tuple6 ) where import Predicate.Core import Predicate.Util import Predicate.Data.Maybe (JustDef, JustFail) import Control.Lens hiding (iall) import GHC.TypeLits (Nat, KnownNat) import Data.Proxy -- $setup -- >>> :set -XDataKinds -- >>> :set -XTypeApplications -- >>> :set -XTypeOperators -- >>> :set -XOverloadedStrings -- >>> :set -XNoOverloadedLists -- >>> import qualified Data.Map.Strict as M -- >>> import qualified Data.Set as Set -- >>> import qualified Data.Text as T -- >>> import Predicate.Prelude -- >>> import qualified Data.Semigroup as SG -- | index a value in an 'Ixed' container and if not found return the given default value -- -- >>> pl @(LookupDef' (Fst Id) (Snd Id) (Char1 "xx") Id) (['a'..'e'],2) -- Present 'c' (JustDef Just) -- PresentT 'c' -- -- >>> pl @(LookupDef' (Fst Id) (Snd Id) (Char1 "xx") Id) (['a'..'e'],999) -- Present 'x' (JustDef Nothing) -- PresentT 'x' -- -- >>> pl @(LookupDef' (Fst Id) (Snd Id) (Char1 "xx") Id) ([],2) -- Present 'x' (JustDef Nothing) -- PresentT 'x' -- -- >>> pl @(LookupDef' (Fst Id) (Snd Id) (Char1 "xx") (Snd Id)) ('w',([],2)) -- Present 'x' (JustDef Nothing) -- PresentT 'x' -- -- >>> pl @(LookupDef' (Fst Id) (Snd Id) (Fst Id) (Snd Id)) ('x',(['a'..'e'],2)) -- Present 'c' (JustDef Just) -- PresentT 'c' -- -- >>> pl @(LookupDef' (Fst Id) (Snd Id) (MEmptyT _) (Snd Id)) ('x',(map SG.Min [10..15::Int], 3)) -- Present Min {getMin = 13} (JustDef Just) -- PresentT (Min {getMin = 13}) -- data LookupDef' v w p q 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 _ = eval (Proxy @(LookupDefT' v w p q)) -- | index a value in an 'Ixed' container and if not found return the given default value -- -- >>> pl @(LookupDef '[1,2,3,4,5,6] 4 Id) 23 -- Present 5 (JustDef Just) -- PresentT 5 -- -- >>> pl @(LookupDef '[1,2,3,4,5,6] 4 (Fst Id)) (23,'x') -- Present 5 (JustDef Just) -- PresentT 5 -- -- >>> pl @(LookupDef '[1,2,3,4,5,6] 99 Id) 23 -- Present 23 (JustDef Nothing) -- PresentT 23 -- -- >>> pl @(LookupDef '[1,2,3,4,5,6] 99 (Fst Id)) (23,'x') -- Present 23 (JustDef Nothing) -- PresentT 23 -- -- >>> pl @(LookupDef '[1,2,3,4,5,6] 4 999) (23,'x') -- Present 5 (JustDef Just) -- PresentT 5 -- -- >>> pl @(LookupDef '[1,2,3,4,5,6] 40 999) (23,'x') -- Present 999 (JustDef Nothing) -- PresentT 999 -- -- >>> pl @(LookupDef (Fst Id) 4 (MEmptyT _)) (map SG.Min [1::Int .. 10],'x') -- Present Min {getMin = 5} (JustDef Just) -- PresentT (Min {getMin = 5}) -- -- >>> pl @(LookupDef (Fst Id) 999 (MEmptyT _)) (map SG.Min [1::Int .. 10],'x') -- Present Min {getMin = 9223372036854775807} (JustDef Nothing) -- PresentT (Min {getMin = 9223372036854775807}) -- data LookupDef v w p type LookupDefT v w p = LookupDef' v w p I 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 _ = eval (Proxy @(LookupDefT v w p)) -- | index a value in an 'Ixed' container and if not found fail with the given message data LookupFail' msg v w q 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 _ = eval (Proxy @(LookupFailT' msg v w q)) -- | index a value in an 'Ixed' container and if not found fail with the given message -- -- >>> pl @(LookupFail "someval" (Fst Id) 999) (map SG.Min [1::Int .. 10],'x') -- Error someval (JustFail Nothing) -- FailT "someval" -- -- >>> pl @(LookupFail (PrintF "char=%c" (Snd Id)) (Fst Id) 49) (map SG.Min [1::Int ..10],'x') -- Error char=x (JustFail Nothing) -- FailT "char=x" -- data LookupFail msg v w type LookupFailT msg v w = LookupFail' msg v w I 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 _ = eval (Proxy @(LookupFailT msg v w)) -- | similar to 'Data.List.!!' using an 'Ixed' container -- -- >>> pz @(Ix 4 "not found") ["abc","D","eF","","G"] -- PresentT "G" -- -- >>> pz @(Ix 40 "not found") ["abc","D","eF","","G"] -- PresentT "not found" -- -- >>> pl @(Fst Id >> Dup >> (Ix 1 (Failp "failed5") *** Ix 3 (Failp "failed5")) >> Id) ([10,12,3,5],"ss") -- Present (12,5) ((>>) (12,5) | {Id (12,5)}) -- PresentT (12,5) -- -- >>> pl @(Fst Id >> Dup >> (Ix 1 (Failp "failed5") *** Ix 3 (Failp "failed5")) >> Fst Id < Snd Id) ([10,12,3,5],"ss") -- False ((>>) False | {12 < 5}) -- FalseT -- -- >>> pl @(Fst Id >> Dup >> (Ix 1 (Failp "failed5") *** Ix 3 (Failp "failed5")) >> Fst Id > Snd Id) ([10,12,3,5],"ss") -- True ((>>) True | {12 > 5}) -- TrueT -- -- >>> pl @(Snd Id >> Len &&& Ix 3 (Failp "someval1") >> Fst Id == Snd Id) ('x',[1..5]) -- False ((>>) False | {5 == 4}) -- FalseT -- -- >>> pl @(Snd Id >> Len &&& Ix 3 (Failp "someval2") >> Fst Id < Snd Id) ('x',[1..5]) -- False ((>>) False | {5 < 4}) -- FalseT -- -- >>> pl @(Snd Id >> Len &&& Ix 3 (Failp "someval3") >> Fst Id > Snd Id) ('x',[1..5]) -- True ((>>) True | {5 > 4}) -- TrueT -- -- >>> pl @(Map Len Id >> Ix 3 (Failp "lhs") &&& Ix 0 5 >> Fst Id == Snd Id) [[1..4],[4..5]] -- Error lhs ([4,2] (>>) rhs failed) -- FailT "lhs" -- -- >>> pl @(Map Len Id >> Ix 0 (Failp "lhs") &&& Ix 1 5 >> Fst Id == Snd Id) [[1..4],[4..5]] -- False ((>>) False | {4 == 2}) -- FalseT -- -- >>> pl @(Map Len Id >> Ix 1 (Failp "lhs") &&& Ix 3 (Failp "rhs") >> Fst Id == Snd Id) [[1..4],[4..5]] -- Error rhs ([4,2] (>>) rhs failed) -- FailT "rhs" -- -- >>> pl @(Map Len Id >> Ix 10 (Failp "lhs") &&& Ix 1 (Failp "rhs") >> Fst Id == Snd Id) [[1..4],[4..5]] -- Error lhs ([4,2] (>>) rhs failed) -- FailT "lhs" -- -- >>> pl @(Map Len Id >> Ix 0 (Failp "lhs") &&& Ix 10 (Failp "rhs") >> Fst Id == Snd Id) [[1..4],[4..5]] -- Error rhs ([4,2] (>>) rhs failed) -- FailT "rhs" -- -- >>> pl @(Map Len Id >> Ix 10 3 &&& Ix 1 (Failp "rhs") >> Fst Id == Snd Id) [[1..4],[4..5]] -- False ((>>) False | {3 == 2}) -- FalseT -- -- >>> pl @(Map Len Id >> Ix 3 3 &&& Ix 1 4 >> Fst Id == Snd Id) [[1..4],[4..5]] -- False ((>>) False | {3 == 2}) -- FalseT -- -- >>> pl @(Map Len Id >> Ix 10 3 &&& Ix 1 4 >> Fst Id == Snd Id) [[1..4],[4..5]] -- False ((>>) False | {3 == 2}) -- FalseT -- -- >>> pl @(Map Len Id >> Ix 10 5 &&& Ix 1 4 >> Fst Id == Snd Id) [[1..4],[4..5]] -- False ((>>) False | {5 == 2}) -- FalseT -- -- >>> pl @(Map Len Id >> Ix 10 2 &&& Ix 1 4 >> Fst Id == Snd Id) [[1..4],[4..5]] -- True ((>>) True | {2 == 2}) -- TrueT -- data Ix (n :: Nat) def instance (P def (Proxy a) , PP def (Proxy a) ~ a , KnownNat n , Show a ) => P (Ix n def) [a] where type PP (Ix n def) [a] = a eval _ opts as = do let n = nat @n msg0 = "Ix(" <> show n <> ")" case as ^? ix n of Nothing -> do let msg1 = msg0 <> " not found" pp <- eval (Proxy @def) opts (Proxy @a) pure $ case getValueLR opts msg1 pp [] of Left e -> e Right _ -> mkNode opts (_tBool pp) msg1 [hh pp] Just a -> pure $ mkNode opts (PresentT a) (msg0 <> " " <> showL opts a) [] data Ix' (n :: Nat) 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 _ = eval (Proxy @(IxT' n)) -- | similar to 'Data.List.!!' leveraging 'Ixed' -- -- >>> pz @(IxL Id 2 "notfound") ["abc","D","eF","","G"] -- PresentT "eF" -- -- >>> pz @(IxL Id 20 "notfound") ["abc","D","eF","","G"] -- PresentT "notfound" -- -- >>> pl @(IxL Id 1 (Char1 "x")) ("123" :: T.Text) -- Present '2' (IxL(1) '2' | p="123" | q=1) -- PresentT '2' -- -- >>> pl @(IxL Id 15 (Char1 "x")) ("123" :: T.Text) -- Present 'x' (IxL(15) index not found) -- PresentT 'x' -- data IxL p q def -- p is the big value and q is the index and def is the default 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 _ opts a = do let msg0 = "IxL" lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a [] case lr of Left e -> pure e Right (p,q,pp,qq) -> let msg1 = msg0 <> "(" <> show q <> ")" in case p ^? ix q of Nothing -> do rr <- eval (Proxy @r) opts (Proxy @(IxValue (PP p a))) pure $ case getValueLR opts msg1 rr [hh pp, hh qq] of Left e -> e Right _ -> mkNode opts (_tBool rr) (msg1 <> " index not found") [hh pp, hh qq] Just ret -> pure $ mkNode opts (PresentT ret) (show01' opts msg1 ret "p=" p <> showVerbose opts " | q=" q) [hh pp, hh qq] -- | similar to 'Data.List.!!' leveraging 'Ixed' -- -- >>> pz @(Id !! 2) ["abc","D","eF","","G"] -- PresentT "eF" -- -- >>> pz @(Id !! 20) ["abc","D","eF","","G"] -- FailT "(!!) index not found" -- -- >>> pz @(Id !! "eF") (M.fromList (flip zip [0..] ["abc","D","eF","","G"])) -- PresentT 2 -- -- >>> pl @(Id !! 3) ("asfd" :: T.Text) -- Present 'd' (IxL(3) 'd' | p="asfd" | q=3) -- PresentT 'd' -- -- >>> pl @(Id !! 4) ("asfd" :: T.Text) -- Error (!!) index not found (IxL(4)) -- FailT "(!!) index not found" -- -- >>> pl @(Id !! MEmptyT _) (Just "a") -- Present "a" (IxL(()) "a" | p=Just "a" | q=()) -- PresentT "a" -- -- >>> pl @(Id !! MEmptyT _) (Nothing @()) -- had to add @() to keep this happy: ghci is fine -- Error (!!) index not found (IxL(())) -- FailT "(!!) index not found" -- -- >>> pl @(Id !! 0) ('a','b','c') -- Present 'a' (IxL(0) 'a' | p=('a','b','c') | q=0) -- PresentT 'a' -- -- >>> pl @(Id !! Failt _ "err") ('a','b','c') -- Error err (IxL) -- FailT "err" -- -- >>> pl @(Id !! "d") (M.fromList $ zip (map (:[]) "abcd") [0 ..]) -- Present 3 (IxL("d") 3 | p=fromList [("a",0),("b",1),("c",2),("d",3)] | q="d") -- PresentT 3 -- -- >>> pl @(Id !! Head "d") (M.fromList $ zip "abcd" [0 ..]) -- had to String (instead of _) to keep this happy: ghci is fine -- Present 3 (IxL('d') 3 | p=fromList [('a',0),('b',1),('c',2),('d',3)] | q='d') -- PresentT 3 -- -- >>> pl @(Id !! Head "d") (Set.fromList "abcd") -- had to String (instead of _) to keep this happy: ghci is fine -- Present () (IxL('d') () | p=fromList "abcd" | q='d') -- PresentT () -- -- >>> pl @(Id !! HeadFail "failedn" "e") (Set.fromList "abcd") -- had to String (instead of _) to keep this happy: ghci is fine -- Error (!!) index not found (IxL('e')) -- FailT "(!!) index not found" -- -- >>> pl @(Id !! Head "d") (M.fromList $ zip "abcd" [0 ..]) -- use Char1 "d" instead of "d" >> Head -- Present 3 (IxL('d') 3 | p=fromList [('a',0),('b',1),('c',2),('d',3)] | q='d') -- PresentT 3 -- -- >>> pl @(Id !! MEmptyT _) (Just 10) -- Present 10 (IxL(()) 10 | p=Just 10 | q=()) -- PresentT 10 -- -- >>> pl @(Id !! MEmptyT _) (Nothing @()) -- Error (!!) index not found (IxL(())) -- FailT "(!!) index not found" -- -- >>> pl @(Id !! 6) ['a'..'z'] -- Present 'g' (IxL(6) 'g' | p="abcdefghijklmnopqrstuvwxyz" | q=6) -- PresentT 'g' -- -- >>> pl @(Snd Id !! Fst Id) (3,"abcde" :: String) -- Present 'd' (IxL(3) 'd' | p="abcde" | q=3) -- PresentT 'd' -- -- >>> pl @(Snd Id !! Fst Id) (4,[9,8]) -- Error (!!) index not found (IxL(4)) -- FailT "(!!) index not found" -- -- >>> pl @(2 &&& Id >> Snd Id !! Fst Id) ("abcdef" :: String) -- Present 'c' ((>>) 'c' | {IxL(2) 'c' | p="abcdef" | q=2}) -- PresentT 'c' -- -- >>> pl @((Len >> Pred Id) &&& Id >> Snd Id !! Fst Id) "abcdef" -- Present 'f' ((>>) 'f' | {IxL(5) 'f' | p="abcdef" | q=5}) -- PresentT 'f' -- -- >>> pl @(Id !! 3) ('a','b','c','d','e') -- Present 'd' (IxL(3) 'd' | p=('a','b','c','d','e') | q=3) -- PresentT 'd' -- -- >>> pl @(Id !! "s") $ M.fromList [("t",1), ("s", 20), ("s", 99)] -- Present 99 (IxL("s") 99 | p=fromList [("s",99),("t",1)] | q="s") -- PresentT 99 -- -- >>> pl @(Id !! Char1 "d") (M.fromList $ zip "abcd" [0 ..]) -- Present 3 (IxL('d') 3 | p=fromList [('a',0),('b',1),('c',2),('d',3)] | q='d') -- PresentT 3 -- -- >>> pl @(Id !! FromString _ "d" &&& (Map (Snd Id >> Gt 3 >> Coerce SG.Any) (IToList _ Id) >> MConcat Id)) (M.fromList $ zip (map T.singleton "abcdefgh") [0 ..]) -- Present (3,Any {getAny = True}) (W '(3,Any {getAny = True})) -- PresentT (3,Any {getAny = True}) -- -- >>> pl @(Id !! FromString _ "d" &&& (Map (Snd Id >> Gt 3 >> Wrap SG.Any Id) (IToList _ Id) >> MConcat Id >> Unwrap Id)) (M.fromList $ zip (map T.singleton "abcdefgh") [0 ..]) -- Present (3,True) (W '(3,True)) -- PresentT (3,True) -- -- >>> pl @(Id !! FromString _ "d") (M.fromList $ zip (map T.singleton "abcd") [0 ..]) -- Present 3 (IxL("d") 3 | p=fromList [("a",0),("b",1),("c",2),("d",3)] | q="d") -- PresentT 3 -- -- >>> pl @(Id !! FromString _ "d") (M.fromList $ zip (map T.singleton "abcd") [0 ..]) -- Present 3 (IxL("d") 3 | p=fromList [("a",0),("b",1),("c",2),("d",3)] | q="d") -- PresentT 3 -- -- >>> pl @(Id !! 2 !! 0) [[1..5],[10..14],[100..110]] -- Present 100 (IxL(0) 100 | p=[100,101,102,103,104,105,106,107,108,109,110] | q=0) -- PresentT 100 -- -- >>> pl @(Id !! 1 !! 7) [[1..5],[10..14],[100..110]] -- Error (!!) index not found (IxL(7)) -- FailT "(!!) index not found" -- -- >>> pl @(Id !! 1) [('x',14),('y',3),('z',5)] -- Present ('y',3) (IxL(1) ('y',3) | p=[('x',14),('y',3),('z',5)] | q=1) -- PresentT ('y',3) -- -- >>> pl @(Id !! 14) [('x',14),('y',3),('z',5)] -- Error (!!) index not found (IxL(14)) -- FailT "(!!) index not found" -- data p !! q 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 _ = eval (Proxy @(BangBangT p q)) -- | 'lookup' leveraging 'Ixed' -- -- >>> pz @(Lookup Id 2) ["abc","D","eF","","G"] -- PresentT (Just "eF") -- -- >>> pz @(Lookup Id 20) ["abc","D","eF","","G"] -- PresentT Nothing -- -- >>> pl @(FromList (M.Map _ _) >> Lookup Id (Char1 "y")) [('x',True),('y',False)] -- Present Just False ((>>) Just False | {Lookup('y') False | p=fromList [('x',True),('y',False)] | q='y'}) -- PresentT (Just False) -- -- >>> pl @(FromList (M.Map _ _) >> Lookup Id (Char1 "z")) [('x',True),('y',False)] -- Present Nothing ((>>) Nothing | {Lookup('z') not found}) -- PresentT Nothing -- -- >>> pl @(FromList (M.Map _ _) >> Lookup Id %% Char1 "y") [('x',True),('y',False)] -- Present Just False ((>>) Just False | {Lookup('y') False | p=fromList [('x',True),('y',False)] | q='y'}) -- PresentT (Just False) -- -- >>> pl @(Lookup Id 1) [('x',14),('y',3),('z',5)] -- Present Just ('y',3) (Lookup(1) ('y',3) | p=[('x',14),('y',3),('z',5)] | q=1) -- PresentT (Just ('y',3)) -- -- >>> pl @(Lookup Id 14) [('x',14),('y',3),('z',5)] -- Present Nothing (Lookup(14) not found) -- PresentT Nothing -- -- >>> pl @(Lookup "abcdef" 3) () -- Present Just 'd' (Lookup(3) 'd' | p="abcdef" | q=3) -- PresentT (Just 'd') -- -- >>> pl @(Lookup '[1,2,3,4,5,6] 4) () -- Present Just 5 (Lookup(4) 5 | p=[1,2,3,4,5,6] | q=4) -- PresentT (Just 5) -- -- >>> pl @(FromList (M.Map _ _)) [(4,"x"),(5,"dd")] -- Present fromList [(4,"x"),(5,"dd")] (FromList fromList [(4,"x"),(5,"dd")]) -- PresentT (fromList [(4,"x"),(5,"dd")]) -- data Lookup p q 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 (Lookup p q) a where type PP (Lookup p q) a = Maybe (IxValue (PP p a)) eval _ opts a = do let msg0 = "Lookup" lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a [] pure $ case lr of Left e -> e Right (p,q,pp,qq) -> let msg1 = msg0 <> "(" <> show q <> ")" hhs = [hh pp, hh qq] in case p ^? ix q of Nothing -> mkNode opts (PresentT Nothing) (msg1 <> " not found") hhs Just ret -> mkNode opts (PresentT (Just ret)) (show01' opts msg1 ret "p=" p <> showVerbose opts " | q=" q) hhs -- | type operator version of 'Lookup' -- -- >>> pl @((Id !!? Char1 "d") > MkJust 99 || Length Id <= 3) (M.fromList $ zip "abcd" [1..]) -- False (False || False | (Just 4 > Just 99) || (4 <= 3)) -- FalseT -- -- >>> pz @((Id !!? Char1 "d") > MkJust 2 || Length Id <= 3) (M.fromList $ zip "abcd" [1..]) -- TrueT -- data p !!? q type BangBangQT p q = Lookup p q instance P (BangBangQT p q) a => P (p !!? q) a where type PP (p !!? q) a = PP (BangBangQT p q) a eval _ = eval (Proxy @(BangBangQT p q)) -- | convert a list to a 2-tuple type Tuple2 p = '(p !! 0, p !! 1) -- | convert a list to a 3-tuple type Tuple3 p = '(p !! 0, p !! 1, p !! 2) -- | convert a list to a 4-tuple type Tuple4 p = '(p !! 0, p !! 1, p !! 2, p !! 3) -- | convert a list to a 5-tuple type Tuple5 p = '(p !! 0, p !! 1, p !! 2, p !! 3, p !! 4) -- | convert a list to a 6-tuple type Tuple6 p = '(p !! 0, p !! 1, p !! 2, p !! 3, p !! 4, p !! 5)