Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.WithDefault

Description

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.

Synopsis

- data WithDefault' a (b :: Bool)
  - = Default
  - | Value !a
- type WithDefault (b :: Bool) = WithDefault' Bool b
- setDefault :: forall a (b :: Bool). Boolean a => a -> WithDefault' a b -> WithDefault' a b
- mapValue :: forall a (b :: Bool). Boolean a => (a -> a) -> WithDefault' a b -> WithDefault' a b
- collapseDefault :: forall a (b :: Bool). (Boolean a, KnownBool b) => WithDefault' a b -> a
- lensCollapseDefault :: forall a (b :: Bool). (Boolean a, KnownBool b) => Lens' (WithDefault' a b) a
- lensKeepDefault :: forall a (b :: Bool). (Boolean a, Eq a, KnownBool b) => Lens' (WithDefault' a b) a

# Documentation

data WithDefault' a (b :: Bool) Source #

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

Instances details

(EmbPrj a, Typeable b) => EmbPrj (WithDefault' a b) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithDefault' a b -> S Word32 Source # icod_ :: WithDefault' a b -> S Word32 Source # value :: Word32 -> R (WithDefault' a b) Source #
Null (WithDefault' a b) Source # | The null value of 'WithDefault b' is `Default`.
Instance details Defined in Agda.Utils.WithDefault Methods empty :: WithDefault' a b Source # null :: WithDefault' a b -> Bool Source #
NFData (WithDefault' a b) Source # |
Instance details Defined in Agda.Utils.WithDefault Methods rnf :: WithDefault' a b -> () Source #
Show a => Show (WithDefault' a b) Source # |
Instance details Defined in Agda.Utils.WithDefault Methods showsPrec :: Int -> WithDefault' a b -> ShowS Source # show :: WithDefault' a b -> String Source # showList :: [WithDefault' a b] -> ShowS Source #
Eq a => Eq (WithDefault' a b) Source # |
Instance details Defined in Agda.Utils.WithDefault Methods (==) :: WithDefault' a b -> WithDefault' a b -> Bool Source # (/=) :: WithDefault' a b -> WithDefault' a b -> Bool Source #

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

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

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 Source #

Only modify non-`Default` values.

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

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 Source #

Focus, overwriting `Default`.

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

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