
  0 | module Libraries.Data.WithDefault
  1 | 
  2 | export
  3 | data WithDefault : (0 a : Type) -> (0 def : a) -> Type where
  4 |   DefaultedValue : WithDefault a def
  5 |   SpecifiedValue : a -> WithDefault a def
  6 | 
  7 | export
  8 | specified : a -> WithDefault a def
  9 | specified = SpecifiedValue
 10 | 
 11 | export
 12 | defaulted : WithDefault a def
 13 | defaulted = DefaultedValue
 14 | 
 15 | export
 16 | specifyValue : a -> WithDefault a def -> WithDefault a def
 17 | specifyValue v DefaultedValue = SpecifiedValue v
 18 | specifyValue _ v              = v
 19 | 
 20 | export
 21 | replaceSpecified : WithDefault a def -> WithDefault a def'
 22 | replaceSpecified DefaultedValue     = DefaultedValue
 23 | replaceSpecified (SpecifiedValue v) = SpecifiedValue v
 24 | 
 25 | export
 26 | collapseDefault : {def : a} -> WithDefault a def -> a
 27 | collapseDefault DefaultedValue     = def
 28 | collapseDefault (SpecifiedValue v) = v
 29 | 
 30 | export
 31 | onWithDefault : (defHandler : Lazy b) ->
 32 |                 (valHandler : a -> b) ->
 33 |                 WithDefault a def ->
 34 |                 b
 35 | onWithDefault defHandler _ DefaultedValue     = defHandler
 36 | onWithDefault _ valHandler (SpecifiedValue v) = valHandler v
 37 | 
 38 | export
 39 | collapseDefaults : Eq a =>
 40 |                    {def : a} ->
 41 |                    WithDefault a def ->
 42 |                    WithDefault a def ->
 43 |                    Either (a, a) a
 44 | collapseDefaults (SpecifiedValue x) (SpecifiedValue y) = if x /= y
 45 |                                                          then Left (x, y)
 46 |                                                          else Right x
 47 | collapseDefaults (SpecifiedValue x) DefaultedValue   = Right x
 48 | collapseDefaults DefaultedValue   (SpecifiedValue y) = Right y
 49 | collapseDefaults DefaultedValue   DefaultedValue     = Right def
 50 | 
 51 | export
 52 | isDefaulted : WithDefault a def -> Bool
 53 | isDefaulted DefaultedValue = True
 54 | isDefaulted _              = False
 55 | 
 56 | export
 57 | isSpecified : WithDefault a def -> Bool
 58 | isSpecified DefaultedValue = False
 59 | isSpecified _              = True
 60 | 
 61 | public export
 62 | Eq a => Eq (WithDefault a def) where
 63 |   DefaultedValue   == DefaultedValue   = True
 64 |   DefaultedValue   == SpecifiedValue _ = False
 65 |   SpecifiedValue _ == DefaultedValue   = False
 66 |   SpecifiedValue x == SpecifiedValue y = x == y
 67 | 
 68 | public export
 69 | Ord a => Ord (WithDefault a def) where
 70 |   compare DefaultedValue   DefaultedValue       = EQ
 71 |   compare DefaultedValue   (SpecifiedValue _)   = LT
 72 |   compare (SpecifiedValue _) DefaultedValue     = GT
 73 |   compare (SpecifiedValue x) (SpecifiedValue y) = compare x y
 74 |