{-# 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 'Maybe' functions -} module Predicate.Data.Maybe ( -- ** boolean predicates IsNothing , IsJust -- ** constructors , MkNothing , MkNothing' , MkJust -- ** get rid of Maybe , Just' , JustDef , JustFail , MapMaybe , CatMaybes , MaybeIn , MaybeBool ) where import Predicate.Core import Predicate.Util import Predicate.Data.Foldable (ConcatMap) import Predicate.Data.Monoid (MEmptyP) import Data.Proxy import Data.Kind (Type) -- $setup -- >>> :set -XDataKinds -- >>> :set -XTypeApplications -- >>> :set -XTypeOperators -- >>> :set -XOverloadedStrings -- >>> :set -XNoOverloadedLists -- >>> import qualified Data.Map.Strict as M -- >>> import Predicate.Prelude -- >>> import qualified Data.Semigroup as SG -- | similar to 'Data.Maybe.fromJust' -- -- >>> pz @(Just' >> Succ Id) (Just 20) -- PresentT 21 -- -- >>> pz @(Just' >> Succ Id) Nothing -- FailT "Just' found Nothing" -- data Just' instance (Show a ) => P Just' (Maybe a) where type PP Just' (Maybe a) = a eval _ opts lr = let msg0 = "Just'" in pure $ case lr of Nothing -> mkNode opts (FailT (msg0 <> " found Nothing")) "" [] Just a -> mkNode opts (PresentT a) (msg0 <> " " <> showL opts a) [] -- | constructs a Nothing for a given type data MkNothing' t -- works always! MaybeBool is a good alternative and then dont need the extra 't' -- for this to be useful has to have 't' else we end up with tons of problems instance P (MkNothing' t) a where type PP (MkNothing' t) a = Maybe (PP t a) eval _ opts _ = let msg0 = "MkNothing" in pure $ mkNode opts (PresentT Nothing) msg0 [] -- | constructs a Nothing for a given type data MkNothing (t :: Type) type MkNothingT (t :: Type) = MkNothing' (Hole t) instance P (MkNothing t) x where type PP (MkNothing t) x = PP (MkNothingT t) x eval _ = eval (Proxy @(MkNothingT t)) -- | 'GHC.Maybe.Just' constructor -- -- >>> pz @(MkJust Id) 44 -- PresentT (Just 44) -- data MkJust p instance ( PP p x ~ a , P p x , Show a ) => P (MkJust p) x where type PP (MkJust p) x = Maybe (PP p x) eval _ opts x = do let msg0 = "MkJust" pp <- eval (Proxy @p) opts x pure $ case getValueLR opts msg0 pp [] of Left e -> e Right p -> let d = Just p in mkNode opts (PresentT d) (msg0 <> " Just " <> showL opts p) [hh pp] -- | similar to 'Data.Maybe.maybe' -- -- provides a Proxy to the result of \'q\' but does not provide the surrounding context -- -- >>> pz @(MaybeIn "foundnothing" (ShowP (Pred Id))) (Just 20) -- PresentT "19" -- -- >>> pz @(MaybeIn "found nothing" (ShowP (Pred Id))) Nothing -- PresentT "found nothing" -- -- >>> pl @(MaybeIn 'True Id) (Nothing @Bool) -- need @() else breaks -- True (MaybeIn(Nothing) True | Proxy) -- TrueT -- -- >>> pl @(MaybeIn (Failt _ "failed4") Id) (Just 10) -- Present 10 (MaybeIn(Just) 10 | 10) -- PresentT 10 -- -- >>> pl @(MaybeIn 'False Id) (Nothing @Bool) -- breaks otherwise -- False (MaybeIn(Nothing) False | Proxy) -- FalseT -- -- >>> pl @(MaybeIn MEmptyP Id) (Just [1,2,3]) -- Present [1,2,3] (MaybeIn(Just) [1,2,3] | [1,2,3]) -- PresentT [1,2,3] -- -- >>> pl @(MaybeIn MEmptyP Id) (Nothing @[Int]) -- Present [] (MaybeIn(Nothing) [] | Proxy) -- PresentT [] -- -- >>> pl @(MaybeIn (Failp "err") (Succ Id)) (Just 116) -- Present 117 (MaybeIn(Just) 117 | 116) -- PresentT 117 -- -- >>> pl @(MaybeIn 99 (Succ Id)) (Nothing @Int) -- Present 99 (MaybeIn(Nothing) 99 | Proxy) -- PresentT 99 -- -- >>> pl @(MaybeIn (Failp "someval") (Succ Id)) (Nothing @()) -- Error someval (MaybeIn(Nothing)) -- FailT "someval" -- -- >>> pl @(MaybeIn 'True 'False) (Nothing @()) -- True (MaybeIn(Nothing) True | Proxy) -- TrueT -- -- >>> pl @(MaybeIn 'True 'False) (Just "aa") -- False (MaybeIn(Just) False | "aa") -- FalseT -- -- >>> pl @(MaybeIn MEmptyP (Fst Id ==! Snd Id)) (Just ('x','z')) -- Present LT (MaybeIn(Just) LT | ('x','z')) -- PresentT LT -- -- >>> pl @(MaybeIn MEmptyP (Fst Id ==! Snd Id)) (Nothing @(Char,Char)) -- Present EQ (MaybeIn(Nothing) EQ | Proxy) -- PresentT EQ -- -- >>> pl @(MaybeIn (Failp "failed20") 'False) (Nothing @Int) -- Error failed20 (MaybeIn(Nothing)) -- FailT "failed20" -- -- >>> pl @(MaybeIn ('False >> FailS "failed21") 'False) (Nothing @Double) -- Error failed21 (MaybeIn(Nothing)) -- FailT "failed21" -- -- >>> pl @(MaybeIn (Failp "err") Id) (Nothing @Int) -- Error err (MaybeIn(Nothing)) -- FailT "err" -- -- >>> pl @(MaybeIn (Failp "err") Id) (Nothing @()) -- Error err (MaybeIn(Nothing)) -- FailT "err" -- -- >>> pl @(MaybeIn MEmptyP Id) (Just (M.fromList [(1,'a')])) -- Present fromList [(1,'a')] (MaybeIn(Just) fromList [(1,'a')] | fromList [(1,'a')]) -- PresentT (fromList [(1,'a')]) -- -- >>> pl @(MaybeIn MEmptyP Id) (Nothing @(M.Map () ())) -- Present fromList [] (MaybeIn(Nothing) fromList [] | Proxy) -- PresentT (fromList []) -- -- >>> pl @(MaybeIn MEmptyP (Ones Id)) (Just @String "abc") -- Present ["a","b","c"] (MaybeIn(Just) ["a","b","c"] | "abc") -- PresentT ["a","b","c"] -- -- >>> pl @(MaybeIn 99 Id) (Just 12) -- Present 12 (MaybeIn(Just) 12 | 12) -- PresentT 12 -- -- >>> pl @(MaybeIn 99 Id) Nothing -- Present 99 (MaybeIn(Nothing) 99 | Proxy) -- PresentT 99 -- -- >>> pl @(MaybeIn (99 -% 1) Id) Nothing -- Present (-99) % 1 (MaybeIn(Nothing) (-99) % 1 | Proxy) -- PresentT ((-99) % 1) -- -- >>> pl @(MaybeIn 123 Id) (Nothing @Int) -- Present 123 (MaybeIn(Nothing) 123 | Proxy) -- PresentT 123 -- -- >>> pl @(MaybeIn 123 Id) (Just 9) -- Present 9 (MaybeIn(Just) 9 | 9) -- PresentT 9 -- -- >>> pl @(Uncons >> MaybeIn '(1,MEmptyT _) Id) [] -- Present (1,[]) ((>>) (1,[]) | {MaybeIn(Nothing) (1,[]) | Proxy}) -- PresentT (1,[]) -- -- >>> pl @(MaybeIn MEmptyP (Ones (ShowP Id))) (Just 123) -- Present ["1","2","3"] (MaybeIn(Just) ["1","2","3"] | 123) -- PresentT ["1","2","3"] -- -- >>> pl @(MaybeIn MEmptyP (Ones (ShowP Id))) (Nothing @String) -- Present [] (MaybeIn(Nothing) [] | Proxy) -- PresentT [] -- -- >>> pl @(MaybeIn MEmptyP (Ones Id)) (Just @String "ab") -- Present ["a","b"] (MaybeIn(Just) ["a","b"] | "ab") -- PresentT ["a","b"] -- -- >>> pl @(MaybeIn MEmptyP (Ones Id)) (Nothing @String) -- Present [] (MaybeIn(Nothing) [] | Proxy) -- PresentT [] -- data MaybeIn p q -- tricky: the nothing case is the proxy of PP q a: ie proxy of the final result instance (P q a , Show a , Show (PP q a) , PP p (Proxy (PP q a)) ~ PP q a , P p (Proxy (PP q a)) ) => P (MaybeIn p q) (Maybe a) where type PP (MaybeIn p q) (Maybe a) = PP q a eval _ opts ma = do let msg0 = "MaybeIn" case ma of Nothing -> do let msg1 = msg0 <> "(Nothing)" pp <- eval (Proxy @p) opts (Proxy @(PP q a)) pure $ case getValueLR opts msg1 pp [] of Left e -> e Right b -> mkNode opts (_tBool pp) (msg1 <> " " <> showL opts b <> " | Proxy") [hh pp] Just a -> do let msg1 = msg0 <> "(Just)" qq <- eval (Proxy @q) opts a pure $ case getValueLR opts msg1 qq [] of Left e -> e Right b -> mkNode opts (_tBool qq) (show01 opts msg1 b a) [hh qq] -- | similar to 'Data.Maybe.isJust' -- -- >>> pz @(IsJust Id) Nothing -- FalseT -- -- >>> pz @(IsJust Id) (Just 'a') -- TrueT -- data IsJust p instance ( P p x , PP p x ~ Maybe a ) => P (IsJust p) x where type PP (IsJust p) x = Bool eval _ opts x = do let msg0 = "IsJust" pp <- eval (Proxy @p) opts x let hhs = [hh pp] pure $ case getValueLR opts msg0 pp [] of Left e -> e Right (Just _) -> mkNodeB opts True msg0 hhs Right Nothing -> mkNodeB opts False msg0 hhs -- | similar to 'Data.Maybe.isNothing' -- -- >>> pz @(IsNothing Id) (Just 123) -- FalseT -- -- >>> pz @(IsNothing Id) Nothing -- TrueT -- -- >>> pl @(Not (IsNothing Id) &&& ('Just Id >> Id + 12)) (Just 1) -- Present (True,13) (W '(True,13)) -- PresentT (True,13) -- -- >>> pl @(Not (IsNothing Id) &&& ('Just Id >> Id + 12)) Nothing -- Error 'Just(empty) (W '(,)) -- FailT "'Just(empty)" -- data IsNothing p instance ( P p x , PP p x ~ Maybe a ) => P (IsNothing p) x where type PP (IsNothing p) x = Bool eval _ opts x = do let msg0 = "IsNothing" pp <- eval (Proxy @p) opts x let hhs = [hh pp] pure $ case getValueLR opts msg0 pp [] of Left e -> e Right (Just _) -> mkNodeB opts False msg0 hhs Right Nothing -> mkNodeB opts True msg0 hhs -- | like 'Data.Maybe.mapMaybe' -- -- >>> pl @(MapMaybe (MaybeBool (Le 3) Id) Id) [1..5] -- Present [1,2,3] (Concat [1,2,3] | [[1],[2],[3],[],[]]) -- PresentT [1,2,3] -- -- >>> pl @(MapMaybe (MaybeBool (Gt 3) Id) Id) [1..5] -- Present [4,5] (Concat [4,5] | [[],[],[],[4],[5]]) -- PresentT [4,5] -- data MapMaybe p q type MapMaybeT p q = ConcatMap (p >> MaybeIn MEmptyP '[Id]) q instance P (MapMaybeT p q) x => P (MapMaybe p q) x where type PP (MapMaybe p q) x = PP (MapMaybeT p q) x eval _ = eval (Proxy @(MapMaybeT p q)) -- | similar to 'Data.Maybe.catMaybes' -- -- >>> pl @(CatMaybes Id) [Just 'a',Nothing,Just 'c',Just 'd',Nothing] -- Present "acd" (Concat "acd" | ["a","","c","d",""]) -- PresentT "acd" -- data CatMaybes q type CatMaybesT q = MapMaybe Id q instance P (CatMaybesT q) x => P (CatMaybes q) x where type PP (CatMaybes q) x = PP (CatMaybesT q) x eval _ = eval (Proxy @(CatMaybesT q)) -- | Convenient method to convert a value \'p\' to a 'Maybe' based on a predicate \'b\' -- if \'b\' then Just \'p\' else Nothing -- -- >>> pz @(MaybeBool (Id > 4) Id) 24 -- PresentT (Just 24) -- -- >>> pz @(MaybeBool (Id > 4) Id) (-5) -- PresentT Nothing -- data MaybeBool b p instance (Show (PP p a) , P b a , P p a , PP b a ~ Bool ) => P (MaybeBool b p) a where type PP (MaybeBool b p) a = Maybe (PP p a) eval _ opts z = do let msg0 = "MaybeBool" bb <- evalBool (Proxy @b) opts z case getValueLR opts (msg0 <> " b failed") bb [] of Left e -> pure e Right True -> do pp <- eval (Proxy @p) opts z pure $ case getValueLR opts (msg0 <> " p failed") pp [hh bb] of Left e -> e Right p -> mkNode opts (PresentT (Just p)) (msg0 <> "(False) Just " <> showL opts p) [hh bb, hh pp] Right False -> pure $ mkNode opts (PresentT Nothing) (msg0 <> "(True)") [hh bb] -- | extract the value from a 'Maybe' otherwise use the default value: similar to 'Data.Maybe.fromMaybe' -- -- >>> pz @(JustDef (1 % 4) Id) (Just 20.4) -- PresentT (102 % 5) -- -- >>> pz @(JustDef (1 % 4) Id) Nothing -- PresentT (1 % 4) -- -- >>> pz @(JustDef (MEmptyT _) Id) (Just "xy") -- PresentT "xy" -- -- >>> pz @(JustDef (MEmptyT _) Id) Nothing -- PresentT () -- -- >>> pz @(JustDef (MEmptyT (SG.Sum _)) Id) Nothing -- PresentT (Sum {getSum = 0}) -- -- >>> pl @(JustDef 0 Id) (Just 123) -- Present 123 (JustDef Just) -- PresentT 123 -- -- >>> pl @(JustDef 0 Id) Nothing -- Present 0 (JustDef Nothing) -- PresentT 0 -- -- >>> pl @(JustDef 99 Id) (Just 12) -- Present 12 (JustDef Just) -- PresentT 12 -- -- >>> pl @(JustDef 99 Id) Nothing -- Present 99 (JustDef Nothing) -- PresentT 99 -- -- >>> pl @(JustDef (99 -% 1) Id) Nothing -- Present (-99) % 1 (JustDef Nothing) -- PresentT ((-99) % 1) -- -- >>> pl @(JustDef (MEmptyT _) Id) (Just (SG.Sum 123)) -- Present Sum {getSum = 123} (JustDef Just) -- PresentT (Sum {getSum = 123}) -- -- >>> pl @(JustDef (MEmptyT _) Id) (Nothing @(SG.Sum _)) -- Present Sum {getSum = 0} (JustDef Nothing) -- PresentT (Sum {getSum = 0}) -- data JustDef p q instance ( PP p x ~ a , PP q x ~ Maybe a , P p x , P q x) => P (JustDef p q) x where type PP (JustDef p q) x = MaybeT (PP q x) eval _ opts x = do let msg0 = "JustDef" qq <- eval (Proxy @q) opts x case getValueLR opts msg0 qq [] of Left e -> pure e Right q -> case q of Just b -> pure $ mkNode opts (PresentT b) (msg0 <> " Just") [hh qq] Nothing -> do pp <- eval (Proxy @p) opts x pure $ case getValueLR opts msg0 pp [hh qq] of Left e -> e Right b -> mkNode opts (PresentT b) (msg0 <> " Nothing") [hh qq, hh pp] -- | extract the value from a 'Maybe' or fail with the given message -- -- >>> pz @(JustFail "nope" Id) (Just 99) -- PresentT 99 -- -- >>> pz @(JustFail "nope" Id) Nothing -- FailT "nope" -- -- >>> pz @(JustFail (PrintF "oops=%d" (Snd Id)) (Fst Id)) (Nothing, 123) -- FailT "oops=123" -- -- >>> pz @(JustFail (PrintF "oops=%d" (Snd Id)) (Fst Id)) (Just 'x', 123) -- PresentT 'x' -- data JustFail p q instance ( PP p x ~ String , PP q x ~ Maybe a , P p x , P q x) => P (JustFail p q) x where type PP (JustFail p q) x = MaybeT (PP q x) eval _ opts x = do let msg0 = "JustFail" qq <- eval (Proxy @q) opts x case getValueLR opts msg0 qq [] of Left e -> pure e Right q -> case q of Just b -> pure $ mkNode opts (PresentT b) (msg0 <> " Just") [hh qq] Nothing -> do pp <- eval (Proxy @p) opts x pure $ case getValueLR opts msg0 pp [hh qq] of Left e -> e Right p -> mkNode opts (FailT p) (msg0 <> " Nothing") [hh qq, hh pp]