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

    -- | Potentially uninitialised Booleans

    -- The initial motivation for this small library is to be able 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.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 (b :: Bool) = Default | Value !Bool
      deriving (WithDefault b -> WithDefault b -> Bool
    (WithDefault b -> WithDefault b -> Bool)
    -> (WithDefault b -> WithDefault b -> Bool) -> Eq (WithDefault b)
    forall (b :: Bool). WithDefault b -> WithDefault b -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: WithDefault b -> WithDefault b -> Bool
    $c/= :: forall (b :: Bool). WithDefault b -> WithDefault b -> Bool
    == :: WithDefault b -> WithDefault b -> Bool
    $c== :: forall (b :: Bool). WithDefault b -> WithDefault b -> Bool
    Eq, Int -> WithDefault b -> ShowS
    [WithDefault b] -> ShowS
    WithDefault b -> String
    (Int -> WithDefault b -> ShowS)
    -> (WithDefault b -> String)
    -> ([WithDefault b] -> ShowS)
    -> Show (WithDefault b)
    forall (b :: Bool). Int -> WithDefault b -> ShowS
    forall (b :: Bool). [WithDefault b] -> ShowS
    forall (b :: Bool). WithDefault b -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [WithDefault b] -> ShowS
    $cshowList :: forall (b :: Bool). [WithDefault b] -> ShowS
    show :: WithDefault b -> String
    $cshow :: forall (b :: Bool). WithDefault b -> String
    showsPrec :: Int -> WithDefault b -> ShowS
    $cshowsPrec :: forall (b :: Bool). Int -> WithDefault b -> ShowS
    Show)

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

    -- 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 already.

    setDefault :: Bool -> WithDefault b -> WithDefault b
    setDefault :: forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
    setDefault Bool
    b = \case
      WithDefault b
    Default -> Bool -> WithDefault b
    forall (b :: Bool). Bool -> WithDefault b
    Value Bool
    b
      WithDefault b
    t -> WithDefault b
    t

    -- 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 :: KnownBool b => WithDefault b -> Bool
    collapseDefault :: forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault = \case
      w :: WithDefault b
    w@WithDefault b
    Default -> WithDefault b -> Bool
    forall (proxy :: Bool -> *) (b :: Bool).
    KnownBool b =>
    proxy b -> Bool
    boolVal WithDefault b
    w
      Value Bool
    b -> Bool
    b