Agda.Utils.WithDefault

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.

Documentation

data WithDefault' a (b :: Bool)

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.

Constructors

Default

Value !a

Instances

(EmbPrj a, Typeable b) => EmbPrj (WithDefault' a b)

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: WithDefault' a b -> S Int32

icod_ :: WithDefault' a b -> S Int32

value :: Int32 -> R (WithDefault' a b)

Null (WithDefault' a b)

The null value of 'WithDefault b' is Default.

Defined in Agda.Utils.WithDefault

Methods

empty :: WithDefault' a b

null :: WithDefault' a b -> Bool

Show a => Show (WithDefault' a b)

Defined in Agda.Utils.WithDefault

Methods

showsPrec :: Int -> WithDefault' a b -> ShowS

show :: WithDefault' a b -> String

showList :: [WithDefault' a b] -> ShowS

NFData (WithDefault' a b)

Defined in Agda.Utils.WithDefault

Methods

rnf :: WithDefault' a b -> ()

Eq a => Eq (WithDefault' a b)

Defined in Agda.Utils.WithDefault

Methods

(==) :: WithDefault' a b -> WithDefault' a b -> Bool

(/=) :: WithDefault' a b -> WithDefault' a b -> Bool

type WithDefault (b :: Bool) = WithDefault' Bool b

setDefault :: forall a (b :: Bool). Boolean a => a -> WithDefault' a b -> WithDefault' a b

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.

mapValue :: forall a (b :: Bool). Boolean a => (a -> a) -> WithDefault' a b -> WithDefault' a b

Only modify non-Default values.

collapseDefault :: forall a (b :: Bool). (Boolean a, KnownBool b) => WithDefault' a b -> a

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.

lensCollapseDefault :: forall a (b :: Bool). (Boolean a, KnownBool b) => Lens' (WithDefault' a b) a

Focus, overwriting Default.

lensKeepDefault :: forall a (b :: Bool). (Boolean a, Eq a, KnownBool b) => Lens' (WithDefault' a b) a

Update, but keep Default when new value is default value.