
   0 | module JS.Attribute
   1 | 
   2 | import Control.Monad.Either
   3 | import JS.Callback
   4 | import JS.Marshall
   5 | import JS.Nullable
   6 | import JS.Undefined
   7 | import JS.Util
   8 | 
   9 | %default total
  10 | 
  11 | ||| A read-write attribute of a JS object.
  12 | |||
  13 | ||| @alwaysReturns : Bool index if the attribute's getter can
  14 | |||                  always return a value that is neither
  15 | |||                  `null` nor `undefined`. This means, that the
  16 | |||                  attribute is non-nullable and either mandatory
  17 | |||                  or optional with a proper default value.
  18 | |||
  19 | ||| @f             : Context of values represented by the attribute.
  20 | |||                  This is `Maybe` if the attribute is nullable,
  21 | |||                  `Optional` if it is an optional attribute on
  22 | |||                  a dictionary type, or `id` if it is mandatory
  23 | |||                  and non-nullable.
  24 | |||
  25 | ||| @              : Type of values stored in the attribute
  26 | public export
  27 | data Attribute :  (alwaysReturns : Bool)
  28 |                -> (f : Type -> Type)
  29 |                -> (a : Type)
  30 |                -> Type where
  31 | 
  32 |   ||| A non-optional attribute.
  33 |   |||
  34 |   ||| This is for data types, which are guaranteed to always return
  35 |   ||| a value that is neither `null` nor `undefined`.
  36 |   Attr : (get : JSIO a) -> (set : a -> JSIO ()) -> Attribute True Prelude.id a
  37 | 
  38 |   ||| A nullable, non-optional attribute.
  39 |   NullableAttr :
  40 |        (get : JSIO (Maybe a))
  41 |     -> (set : Maybe a -> JSIO ())
  42 |     -> Attribute False Maybe a
  43 | 
  44 |   ||| An optional attribute with a predefined default value.
  45 |   OptionalAttr :
  46 |        (get : JSIO (Optional a))
  47 |     -> (set : Optional a -> JSIO ())
  48 |     -> (def : a)
  49 |     -> Attribute True Optional a
  50 | 
  51 |   ||| An optional attribute without default value.
  52 |   OptionalAttrNoDefault :
  53 |        (get : JSIO (Optional a))
  54 |     -> (set : Optional a -> JSIO ())
  55 |     -> Attribute False Optional a
  56 | 
  57 | ||| Returns the value of an attribute in its proper context.
  58 | ||| Typically used in infix notation.
  59 | |||
  60 | ||| ```idris example
  61 | ||| textField `get` value
  62 | ||| ```
  63 | export
  64 | get : (o : obj) -> (attr : obj -> Attribute b f a) -> JSIO $ f a
  65 | get o g = case g o of
  66 |   Attr                  gt _   => gt
  67 |   NullableAttr          gt _   => gt
  68 |   OptionalAttr          gt _ _ => gt
  69 |   OptionalAttrNoDefault gt _   => gt
  70 | 
  71 | ||| Maps a function over the value retrieved from an `Attribute`.
  72 | export
  73 | over : (a -> b) -> (attr : Attribute x f a) -> JSIO $ f b
  74 | over f (Attr gt _)                  = map f gt
  75 | over f (NullableAttr gt _)          = map f <$> gt
  76 | over f (OptionalAttr gt _ _)        = map f <$> gt
  77 | over f (OptionalAttrNoDefault gt _) = map f <$> gt
  78 | 
  79 | ||| Flipped version of `get`. This is useful when
  80 | ||| combined with the bind operator:
  81 | |||
  82 | ||| ```idris example
  83 | ||| body >>= to className
  84 | ||| ```
  85 | export
  86 | to : (attr : obj -> Attribute b f a) -> (o : obj) -> JSIO $ f a
  87 | to = flip get
  88 | 
  89 | 
  90 | ||| Sets the value of an `Attribute`.
  91 | export
  92 | set' : (attr : Attribute b f a) -> f a -> JSIO ()
  93 | set' (Attr                  _ s)   = s
  94 | set' (NullableAttr          _ s)   = s
  95 | set' (OptionalAttr          _ s _) = s
  96 | set' (OptionalAttrNoDefault _ s)   = s
  97 | 
  98 | ||| Gets the value of an `Attribute`. Since this operates
  99 | ||| on an `Attribute True`, it is guaranteed to always yield
 100 | ||| a non-nullable value.
 101 | export
 102 | getDef : (o : obj) -> (attr : obj -> Attribute True f a) -> JSIO a
 103 | getDef o g = case g o of
 104 |   Attr         gt _     => gt
 105 |   OptionalAttr gt _ def => map (fromOptional def) gt
 106 | 
 107 | ||| Maps a function over the value retrieved from an `Attribute`.
 108 | ||| Since this operates
 109 | ||| on an `Attribute True`, it is guaranteed to always yield
 110 | ||| a non-nullable value.
 111 | export
 112 | overDef : (a -> b) -> (attr : Attribute True f a) -> JSIO b
 113 | overDef f a = f <$> getDef () (const a)
 114 | 
 115 | ||| Flipped version of `getDef`.
 116 | export
 117 | toDef : (attr : obj -> Attribute True f a) -> (o : obj) -> JSIO a
 118 | toDef = flip getDef
 119 | 
 120 | ||| Sets the value of an `Attribute`.
 121 | |||
 122 | ||| ```idris example
 123 | ||| disabled btn `set` True
 124 | ||| ```
 125 | export
 126 | set : Attribute b f a -> a -> JSIO ()
 127 | set (Attr         _ s)          y = s y
 128 | set (NullableAttr _ s)          y = s (Just y)
 129 | set (OptionalAttr _ s _)        y = s (Def y)
 130 | set (OptionalAttrNoDefault _ s) y = s (Def y)
 131 | 
 132 | ||| Modifies the stored value of an `Attribute`.
 133 | |||
 134 | ||| Please note, that this will NOT change the attribute's
 135 | ||| values, if the attribute is unset or `null`.
 136 | export
 137 | mod : Attribute b f a -> (a -> a) -> JSIO ()
 138 | mod (Attr         g s)          f = g >>= s . f
 139 | mod (NullableAttr g s)          f = g >>= s . map f
 140 | mod (OptionalAttr g s _)        f = g >>= s . map f
 141 | mod (OptionalAttrNoDefault g s) f = g >>= s . map f
 142 | 
 143 | ||| Unsets the value of an optional or nullable attribute.
 144 | export
 145 | unset : Alternative f => (o : obj) -> (obj -> Attribute b f a) -> JSIO ()
 146 | unset o g = set' (g o) empty
 147 | 
 148 | export infix 1 .=, =., %=, =%
 149 | 
 150 | ||| Operator version of `set`.
 151 | |||
 152 | ||| ```idris example
 153 | ||| disabled btn .= True
 154 | ||| ```
 155 | export
 156 | (.=) : Attribute b f a -> a -> JSIO ()
 157 | (.=) = set
 158 | 
 159 | ||| Operator version of `mod`.
 160 | |||
 161 | ||| As with `mod`, this will NOT change the attribute's
 162 | ||| values, if the attribute is unset or `null`.
 163 | |||
 164 | ||| ```idris example
 165 | ||| toggleCheckBox : HTMLInputElement -> JSIO ()
 166 | ||| toggleCheckBox cbx = checked cbx %= not
 167 | ||| ```
 168 | export
 169 | (%=) : Attribute b f a -> (a -> a) -> JSIO ()
 170 | (%=) = mod
 171 | 
 172 | ||| Like `set`, but useful when the object, on which
 173 | ||| an attribute should operate, is supposed to
 174 | ||| be the last argument (for instance, when
 175 | ||| iterating over a foldable):
 176 | |||
 177 | ||| ```idris example
 178 | ||| disableAll : List HTMLButtonElement -> JSIO ()
 179 | ||| disableAll buttons = for_ buttons $ disabled =. True
 180 | ||| ```
 181 | export
 182 | (=.) : (obj -> Attribute b f a) -> a -> obj -> JSIO ()
 183 | (=.) f v o = set (f o) v
 184 | 
 185 | ||| Like `mod`, but useful when the object, on which
 186 | ||| an attribute should operate, is supposed to
 187 | ||| be the last argument (for instance, when
 188 | ||| iterating over a foldable):
 189 | |||
 190 | ||| ```idris example
 191 | ||| toggleAll : List HTMLInputElement -> JSIO ()
 192 | ||| toggleAll cbxs = for_ cbxs $ checked =% not
 193 | ||| ```
 194 | export
 195 | (=%) : (obj -> Attribute b f a) -> (a -> a) -> obj -> JSIO ()
 196 | (=%) f g o = mod (f o) g
 197 | 
 198 | export infixr 0 !>, ?>
 199 | 
 200 | ||| Sets a callback function at an attribute.
 201 | |||
 202 | ||| ```idris
 203 | ||| onclick btn !> consoleLog . jsShow
 204 | ||| ```
 205 | export
 206 | (!>) : Callback a fun => Attribute b f a -> fun -> JSIO ()
 207 | a !> cb = callback cb >>= set a
 208 | 
 209 | ||| Sets a callback action at an attribute. This is like `(!>)`
 210 | ||| but ignores its input.
 211 | |||
 212 | ||| ```idris
 213 | ||| onclick btn ?> consoleLog "Boom!"
 214 | ||| ```
 215 | export
 216 | (?>) : Callback a (x -> y) => Attribute b f a -> y -> JSIO ()
 217 | a ?> v = a !> const v
 218 | 
 219 | --------------------------------------------------------------------------------
 220 | --          Creating Attributes
 221 | --------------------------------------------------------------------------------
 222 | 
 223 | export
 224 | fromPrim :
 225 |      {auto _ : ToFFI a b}
 226 |   -> {auto _ : FromFFI a b}
 227 |   -> String
 228 |   -> (obj -> PrimIO b)
 229 |   -> (obj -> b -> PrimIO ())
 230 |   -> obj
 231 |   -> Attribute True Prelude.id a
 232 | fromPrim msg g s o =
 233 |   Attr (tryJS msg $ g o) (\a => primJS $ s o (toFFI a))
 234 | 
 235 | export
 236 | fromNullablePrim :
 237 |      {auto _ : ToFFI a b}
 238 |   -> {auto _ : FromFFI a b}
 239 |   -> String
 240 |   -> (obj -> PrimIO $ Nullable b)
 241 |   -> (obj -> Nullable b -> PrimIO ())
 242 |   -> obj
 243 |   -> Attribute False Maybe a
 244 | fromNullablePrim msg g s o =
 245 |   NullableAttr (tryJS msg $ g o) (\a => primJS $ s o (toFFI a))
 246 | 
 247 | export
 248 | fromUndefOrPrim :
 249 |      {auto _ : ToFFI a b}
 250 |   -> {auto _ : FromFFI a b}
 251 |   -> String
 252 |   -> (obj -> PrimIO $ UndefOr b)
 253 |   -> (obj -> UndefOr b -> PrimIO ())
 254 |   -> a
 255 |   -> obj
 256 |   -> Attribute True Optional a
 257 | fromUndefOrPrim msg g s def o =
 258 |   OptionalAttr (tryJS msg $ g o) (\a => primJS $ s o (toFFI a)) def
 259 | 
 260 | export
 261 | fromUndefOrPrimNoDefault :
 262 |      {auto _ : ToFFI a b}
 263 |   -> {auto _ : FromFFI a b}
 264 |   -> String
 265 |   -> (obj -> PrimIO $ UndefOr b)
 266 |   -> (obj -> UndefOr b -> PrimIO ())
 267 |   -> obj
 268 |   -> Attribute False Optional a
 269 | fromUndefOrPrimNoDefault msg g s o =
 270 |   OptionalAttrNoDefault (tryJS msg $ g o) (\a => primJS $ s o (toFFI a))
 271 |