{-# 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
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
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 -> 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 -> forall (proxy :: Bool -> *) (b :: Bool).
KnownBool b =>
proxy b -> Bool
boolVal WithDefault b
w
  Value Bool
b -> Bool
b