{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds      #-}

-- | Potentially uninitialised Booleans.
--
-- The motivation for this small library is to distinguish
-- between a boolean option with a default value and an option which has been
-- set to what happens to be the default value.  In one case the default can be
-- overriden (e.g. @--cubical@ implies @--without-K@) while in the other case the
-- user has made a mistake which they need to fix.

module Agda.Utils.WithDefault where

import Control.DeepSeq

import Agda.Utils.Boolean
import Agda.Utils.Lens
import Agda.Utils.Null
import Agda.Utils.TypeLits

-- | We don't want to have to remember for each flag whether its default value
-- is @True@ or @False@. So we bake it into the representation: the flag's type
-- will mention its default value as a phantom parameter.
--
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)
  -- Note: the argument @b@ must be last, because this is matched against @proxy b@
  -- in 'Agda.Utils.TypeLits.boolVal'.
  -- Thus, we cannot make it a 'Functor' in @a@.
  -- Instead, we define 'mapValue'.

type WithDefault b = WithDefault' Bool b

instance NFData (WithDefault' a b) where
  rnf :: WithDefault' a b -> ()
rnf WithDefault' a b
Default   = ()
  rnf (Value a
_) = ()

-- | The null value of 'WithDefault b' is 'Default'.
--
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

-- | The main mode of operation of these flags, apart from setting them explicitly,
-- is to toggle them one way or the other if they hadn't been set already.
--
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

-- | Only modify non-'Default' values.
--
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)

-- | Provided that the default value is a known boolean (in practice we only use
-- @True@ or @False@), we can collapse a potentially uninitialised value to a boolean.
--
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

-- | Focus, overwriting 'Default'.
--
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)

-- | Update, but keep 'Default' when new value is default value.
--
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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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)