    {-# OPTIONS_GHC -Wunused-imports #-}

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

    -- | 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 (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)