{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
module Agda.Utils.WithDefault where
import Control.DeepSeq
import Agda.Utils.Boolean
import Agda.Utils.Lens
import Agda.Utils.Null
import Agda.Utils.TypeLits
data WithDefault' a (b :: Bool) = Default | Value !a
deriving (WithDefault' a b -> WithDefault' a b -> Bool
(WithDefault' a b -> WithDefault' a b -> Bool)
-> (WithDefault' a b -> WithDefault' a b -> Bool)
-> Eq (WithDefault' a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a (b :: Bool).
Eq a =>
WithDefault' a b -> WithDefault' a b -> Bool
$c== :: forall a (b :: Bool).
Eq a =>
WithDefault' a b -> WithDefault' a b -> Bool
== :: WithDefault' a b -> WithDefault' a b -> Bool
$c/= :: forall a (b :: Bool).
Eq a =>
WithDefault' a b -> WithDefault' a b -> Bool
/= :: WithDefault' a b -> WithDefault' a b -> Bool
Eq, Int -> WithDefault' a b -> ShowS
[WithDefault' a b] -> ShowS
WithDefault' a b -> String
(Int -> WithDefault' a b -> ShowS)
-> (WithDefault' a b -> String)
-> ([WithDefault' a b] -> ShowS)
-> Show (WithDefault' a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a (b :: Bool). Show a => Int -> WithDefault' a b -> ShowS
forall a (b :: Bool). Show a => [WithDefault' a b] -> ShowS
forall a (b :: Bool). Show a => WithDefault' a b -> String
$cshowsPrec :: forall a (b :: Bool). Show a => Int -> WithDefault' a b -> ShowS
showsPrec :: Int -> WithDefault' a b -> ShowS
$cshow :: forall a (b :: Bool). Show a => WithDefault' a b -> String
show :: WithDefault' a b -> String
$cshowList :: forall a (b :: Bool). Show a => [WithDefault' a b] -> ShowS
showList :: [WithDefault' a b] -> ShowS
Show)
type WithDefault b = WithDefault' Bool b
instance NFData (WithDefault' a b) where
rnf :: WithDefault' a b -> ()
rnf WithDefault' a b
Default = ()
rnf (Value a
_) = ()
instance Null (WithDefault' a b) where
empty :: WithDefault' a b
empty = WithDefault' a b
forall a (b :: Bool). WithDefault' a b
Default
null :: WithDefault' a b -> Bool
null = \case
WithDefault' a b
Default -> Bool
True
Value a
_ -> Bool
False
setDefault :: Boolean a => a -> WithDefault' a b -> WithDefault' a b
setDefault :: forall a (b :: Bool).
Boolean a =>
a -> WithDefault' a b -> WithDefault' a b
setDefault a
b = \case
WithDefault' a b
Default -> a -> WithDefault' a b
forall a (b :: Bool). a -> WithDefault' a b
Value a
b
WithDefault' a b
t -> WithDefault' a b
t
mapValue :: Boolean a => (a -> a) -> WithDefault' a b -> WithDefault' a b
mapValue :: forall a (b :: Bool).
Boolean a =>
(a -> a) -> WithDefault' a b -> WithDefault' a b
mapValue a -> a
f = \case
WithDefault' a b
Default -> WithDefault' a b
forall a (b :: Bool). WithDefault' a b
Default
Value a
b -> a -> WithDefault' a b
forall a (b :: Bool). a -> WithDefault' a b
Value (a -> a
f a
b)
collapseDefault :: (Boolean a, KnownBool b) => WithDefault' a b -> a
collapseDefault :: forall a (b :: Bool).
(Boolean a, KnownBool b) =>
WithDefault' a b -> a
collapseDefault = \case
w :: WithDefault' a b
w@WithDefault' a b
Default -> Bool -> a
forall a. Boolean a => Bool -> a
fromBool (WithDefault' a b -> Bool
forall (proxy :: Bool -> *) (b :: Bool).
KnownBool b =>
proxy b -> Bool
boolVal WithDefault' a b
w)
Value a
b -> a
b
lensCollapseDefault :: (Boolean a, KnownBool b) => Lens' (WithDefault' a b) a
lensCollapseDefault :: forall a (b :: Bool).
(Boolean a, KnownBool b) =>
Lens' (WithDefault' a b) a
lensCollapseDefault a -> f a
f WithDefault' a b
w = a -> WithDefault' a b
forall a (b :: Bool). a -> WithDefault' a b
Value (a -> WithDefault' a b) -> f a -> f (WithDefault' a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f (WithDefault' a b -> a
forall a (b :: Bool).
(Boolean a, KnownBool b) =>
WithDefault' a b -> a
collapseDefault WithDefault' a b
w)
lensKeepDefault :: (Boolean a, Eq a, KnownBool b) => Lens' (WithDefault' a b) a
lensKeepDefault :: forall a (b :: Bool).
(Boolean a, Eq a, KnownBool b) =>
Lens' (WithDefault' a b) a
lensKeepDefault a -> f a
f = \case
Value a
b -> a -> WithDefault' a b
forall a (b :: Bool). a -> WithDefault' a b
Value (a -> WithDefault' a b) -> f a -> f (WithDefault' a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f a
b
w :: WithDefault' a b
w@WithDefault' a b
Default -> a -> f a
f a
b f a -> (a -> WithDefault' a b) -> f (WithDefault' a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ a
b' -> if a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b' then WithDefault' a b
forall a (b :: Bool). WithDefault' a b
Default else a -> WithDefault' a b
forall a (b :: Bool). a -> WithDefault' a b
Value a
b'
where
b :: a
b = Bool -> a
forall a. Boolean a => Bool -> a
fromBool (WithDefault' a b -> Bool
forall (proxy :: Bool -> *) (b :: Bool).
KnownBool b =>
proxy b -> Bool
boolVal WithDefault' a b
w)