From 650f99156a82e4f40f0a12806f01aebe8173219d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stefan=20H=C3=B6ck?= Date: Sun, 20 Aug 2023 22:25:20 +0200 Subject: [PATCH] [ style ] adhere to coding style (#51) --- docs/src/Tutorial.md | 89 +++++++++-------- js/src/JS/Array.idr | 196 ++++++++++++++++++++++---------------- js/src/JS/Attribute.idr | 93 ++++++++++-------- js/src/JS/Boolean.idr | 7 +- js/src/JS/Inheritance.idr | 25 +++-- js/src/JS/Marshall.idr | 4 +- js/src/JS/Nullable.idr | 17 ++-- js/src/JS/Object.idr | 39 ++++---- js/src/JS/Undefined.idr | 26 +++-- js/src/JS/Util.idr | 22 +++-- js/test/src/Array.idr | 54 ++++++----- js/test/src/Main.idr | 7 +- js/test/src/Object.idr | 70 ++++++++------ js/test/src/Util.idr | 62 ++++++------ src/Web/Dom.idr | 23 ++--- src/Web/Html.idr | 14 +-- 16 files changed, 420 insertions(+), 328 deletions(-) diff --git a/docs/src/Tutorial.md b/docs/src/Tutorial.md index 5eeb454..ff2c61a 100644 --- a/docs/src/Tutorial.md +++ b/docs/src/Tutorial.md @@ -76,29 +76,31 @@ checkPalindrome s = export prog : JSIO () -prog = do btn <- createElement Button - textContent btn .= "Click me!" - Element.id btn .= "the_button" - - txt <- newElement Input [ HTMLInputElement.type =. "text" - , placeholder =. "Enter your name here." - ] - - txtDiv <- createElement Div - lenDiv <- createElement Div - outDiv <- createElement Div - - onclick btn ?> do name <- txt `get` value - textContent outDiv .= #"Hello \#{name}!"# - - oninput txt ?> do reply <- checkPalindrome `over` value txt - textContent lenDiv .= reply - - ignore $ (!body `appendChild` btn) *> - (!body `appendChild` txtDiv) *> - (!body `appendChild` outDiv) *> - (!body `appendChild` lenDiv) *> - (txtDiv `appendChild` txt) +prog = do + btn <- createElement Button + textContent btn .= "Click me!" + Element.id btn .= "the_button" + + txt <- newElement Input [ HTMLInputElement.type =. "text" + , placeholder =. "Enter your name here." + ] + + txtDiv <- createElement Div + lenDiv <- createElement Div + outDiv <- createElement Div + + onclick btn ?> do name <- txt `get` value + textContent outDiv .= #"Hello \#{name}!"# + + oninput txt ?> do reply <- checkPalindrome `over` value txt + textContent lenDiv .= reply + + ignore $ + (!body `appendChild` btn) *> + (!body `appendChild` txtDiv) *> + (!body `appendChild` outDiv) *> + (!body `appendChild` lenDiv) *> + (txtDiv `appendChild` txt) ``` You can give this a try in the browser by replacing the @@ -167,10 +169,12 @@ the proper type. We can use `safeCast` for this: ```idris export disableBtn : JSIO () -disableBtn = do maybeElem <- getElementById !document "the_button" - let maybeBtn = maybeElem >>= castTo HTMLButtonElement - for_ maybeBtn $ \btn => do disabled btn .= True - consoleLog "Disabled button" +disableBtn = do + maybeElem <- getElementById !document "the_button" + let maybeBtn = maybeElem >>= castTo HTMLButtonElement + for_ maybeBtn $ \btn => do + disabled btn .= True + consoleLog "Disabled button" ``` You can try the action above by modifying our original @@ -188,8 +192,9 @@ and `htmlElementById` in `Web.Dom`: ```idris export disableBtn2 : JSIO () -disableBtn2 = do maybeBtn <- htmlElementById Button "the_button" - for_ maybeBtn $ disabled =. True +disableBtn2 = do + maybeBtn <- htmlElementById Button "the_button" + for_ maybeBtn $ disabled =. True ``` ### Attributes @@ -272,9 +277,10 @@ implementation of `FromFFI`: ```idris FromFFI Answer Boolean where - fromFFI v = if eqv v true then Just Yes - else if eqv v false then Just No - else Nothing + fromFFI v = + if eqv v true then Just Yes + else if eqv v false then Just No + else Nothing ``` Most of the time, foreign function calls wrap their result in `PrimIO`. @@ -325,10 +331,11 @@ complainOnClick : HTMLButtonElement -> JSIO () complainOnClick btn = onclick btn ?> consoleLog "Don't touch me!" doComplain : MouseEvent -> JSIO () -doComplain me = do shiftPressed <- shiftKey me - if shiftPressed - then consoleLog "DON'T TOUCH ME!" - else consoleLog "Don't touch me!" +doComplain me = do + shiftPressed <- shiftKey me + if shiftPressed + then consoleLog "DON'T TOUCH ME!" + else consoleLog "Don't touch me!" export complainSomeMore : HTMLButtonElement -> JSIO () @@ -558,10 +565,12 @@ nodes to the body like so: ```idris addNodes : HTMLButtonElement -> HTMLDivElement -> HTMLDivElement -> JSIO () addNodes btn txtDiv outDiv = - ignore $ (!body `append` [ Here $ btn :> Node - , Here $ txtDiv :> Node - , Here $ outDiv :> Node - ]) + ignore $ + (!body `append` + [ Here $ btn :> Node + , Here $ txtDiv :> Node + , Here $ outDiv :> Node + ]) ``` In this case, we wouldn't have gained much, as we'd need to diff --git a/js/src/JS/Array.idr b/js/src/JS/Array.idr index 701fbc9..cb7612f 100644 --- a/js/src/JS/Array.idr +++ b/js/src/JS/Array.idr @@ -55,18 +55,19 @@ public export zipWithIndex : (as : List a) -> List (Ix $ len32 as, a) zipWithIndex as = run [] 0 as -- being pragmatic here and going via `believe_me` - where run : List (Ix $ len32 as, a) -> Bits32 -> List a -> List (Ix $ len32 as, a) - run acc _ [] = reverse acc - run acc n (x :: xs) = - run ((Element n $ believe_me (Refl {x}), x) :: acc) (n+1) xs + where + run : List (Ix $ len32 as, a) -> Bits32 -> List a -> List (Ix $ len32 as, a) + run acc _ [] = reverse acc + run acc n (x :: xs) = + run ((Element n $ believe_me (Refl {x}), x) :: acc) (n+1) xs ||| Tries to convert a number into an index for ||| an array of the given size. public export toIx : (size : Bits32) -> Bits32 -> Maybe (Ix size) toIx size x = case decEq (x < size) True of - Yes prf => Just $ Element x prf - No _ => Nothing + Yes prf => Just $ Element x prf + No _ => Nothing -------------------------------------------------------------------------------- -- FFI @@ -189,34 +190,39 @@ export sameElements : (IArrayLike arr el, Eq el) => arr -> arr -> Bool sameElements a1 a2 = case decEq (size a2) (size a1) of - Yes prf => run prf 0 - No _ => False - where run : (0 _ : size a2 = size a1) -> Bits32 -> Bool - run refl ix = - case decEq (ix < size a1) True of - No _ => True - Yes prf => - read a1 (Element ix prf) == - read a2 (Element ix (rewrite refl in prf)) && - run refl (assert_smaller ix $ ix+1) - -export -foldlArray : IArrayLike arr el - => (acc -> el -> acc) -> acc -> arr -> acc + Yes prf => run prf 0 + No _ => False + + where + run : (0 _ : size a2 = size a1) -> Bits32 -> Bool + run refl ix = + case decEq (ix < size a1) True of + No _ => True + Yes prf => + read a1 (Element ix prf) == + read a2 (Element ix (rewrite refl in prf)) && + run refl (assert_smaller ix $ ix+1) + +export +foldlArray : + IArrayLike arr el => (acc -> el -> acc) -> acc -> arr -> acc foldlArray f ini arr = run 0 ini - where run : Bits32 -> acc -> acc - run n res = case readMaybe arr n of - Just el => run (assert_smaller n $ n+1) (f res el) - Nothing => res + + where + run : Bits32 -> acc -> acc + run n res = case readMaybe arr n of + Just el => run (assert_smaller n $ n+1) (f res el) + Nothing => res export -foldrArray : IArrayLike arr el - => (el -> acc -> acc) -> acc -> arr -> acc +foldrArray : + IArrayLike arr el => (el -> acc -> acc) -> acc -> arr -> acc foldrArray f ini arr = run 0 - where run : Bits32 -> acc - run n = case readMaybe arr n of - Just el => f el $ run (assert_smaller n $ n+1) - Nothing => ini + where + run : Bits32 -> acc + run n = case readMaybe arr n of + Just el => f el $ run (assert_smaller n $ n+1) + Nothing => ini export arrayToList : IArrayLike arr el => arr -> List el @@ -257,12 +263,16 @@ arrayDataFrom arr = primIO $ prim__fromArrayLikeIO arr export fromListIO : HasIO io => List a -> io (Array a) -fromListIO as = let len = the Bits32 (fromInteger . natToInteger $ length as) - in newArrayIO len >>= fill 0 as - where fill : Bits32 -> List a -> Array a -> io (Array a) - fill _ [] arr = pure arr - fill n (x :: xs) arr = do writeIO arr n x - fill (n+1) xs arr +fromListIO as = + let len := the Bits32 (fromInteger . natToInteger $ length as) + in newArrayIO len >>= fill 0 as + + where + fill : Bits32 -> List a -> Array a -> io (Array a) + fill _ [] arr = pure arr + fill n (x :: xs) arr = do + writeIO arr n x + fill (n+1) xs arr export fromFoldableIO : (HasIO io, Foldable t) => t a -> io (Array a) @@ -317,17 +327,19 @@ emptyArray : (1 _ : (1 _ : LinArray 0 a) -> b) -> b emptyArray f = f (MkLinArray $ prim__emptyArray) export -newArray : (val : a) - -> (sze : Bits32) - -> (1 _ : (1 _ : LinArray sze a) -> b) - -> b +newArray : + (val : a) + -> (sze : Bits32) + -> (1 _ : (1 _ : LinArray sze a) -> b) + -> b newArray v sze f = f (MkLinArray $ prim__newArray (toFFI sze) v) export -withArray : IArrayLike arr el - => (v : arr) - -> (1 _ : (1 _ : LinArray (size v) el) -> a) - -> a +withArray : + {auto _ : IArrayLike arr el} + -> (v : arr) + -> (1 _ : (1 _ : LinArray (size v) el) -> a) + -> a withArray array f = f (MkLinArray $ prim__fromArray array) export @@ -335,9 +347,10 @@ write : (1 _ : LinArray sze a) -> (ix : Ix sze) -> a -> LinArray sze a write arr (Element n _) = unsafeWrite arr n export -lread : (1 _ : LinArray sze a) - -> (ix : Ix sze) - -> Res a (const $ LinArray sze a) +lread : + (1 _ : LinArray sze a) + -> (ix : Ix sze) + -> Res a (const $ LinArray sze a) lread (MkLinArray arr) (Element ix _) = prim__read arr (toFFI ix) # MkLinArray arr @@ -346,59 +359,74 @@ lsize : (1 _ : LinArray sze a) -> Res Bits32 (\s => LinArray s a) lsize (MkLinArray arr) = fromInteger (cast $ prim__size arr) # MkLinArray arr export -iterate' : (sze : Bits32) - -> (Ix sze -> a) - -> ((1 _ : LinArray sze a) -> b) - -> b +iterate' : + (sze : Bits32) + -> (Ix sze -> a) + -> ((1 _ : LinArray sze a) -> b) + -> b iterate' sze f g = undefArray sze (run 0) - where run : Bits32 -> (1 _ : LinArray sze a) -> b - run n arr = case toIx sze n of - Nothing => g arr - Just ix => run (assert_smaller n $ n+1) (write arr ix (f ix)) + + where + run : Bits32 -> (1 _ : LinArray sze a) -> b + run n arr = case toIx sze n of + Nothing => g arr + Just ix => run (assert_smaller n $ n+1) (write arr ix (f ix)) export fromList' : (as : List a) -> ((1 _ : LinArray (len32 as) a) -> b) -> b fromList' as f = undefArray (len32 as) (run $ zipWithIndex as) - where run : List (Ix $ len32 as, a) -> (1 _ : LinArray (len32 as) a) -> b - run [] linA = f linA - run ((ix,a) :: t) linA = run t (write linA ix a) + + where + run : List (Ix $ len32 as, a) -> (1 _ : LinArray (len32 as) a) -> b + run [] linA = f linA + run ((ix,a) :: t) linA = run t (write linA ix a) export -map' : IArrayLike arr a => - (vs : arr) -> ((1 _ : LinArray (size vs) b) -> c) -> (a -> b) -> c +map' : + {auto _ : IArrayLike arr a} + -> (vs : arr) + -> ((1 _ : LinArray (size vs) b) -> c) + -> (a -> b) + -> c map' vs fromArr f = iterate' (size vs) (\ix => f (read vs ix)) fromArr export -totalSize : (IArrayLike arr1 arr2, IArrayLike arr2 el) - => arr1 -> Bits32 +totalSize : + (IArrayLike arr1 arr2, IArrayLike arr2 el) => arr1 -> Bits32 totalSize = foldlArray (\n,vs => n + size vs) 0 ||| Concatenates to nested layers of immutable ||| array-like objects. export -join' : (IArrayLike arr1 arr2, IArrayLike arr2 el) - => (vss : arr1) - -> ((1 _ : LinArray (totalSize {arr2} vss) el) -> a) - -> a +join' : + {auto _ : IArrayLike arr1 arr2} + -> {auto _ : IArrayLike arr2 el} + -> (vss : arr1) + -> ((1 _ : LinArray (totalSize {arr2} vss) el) -> a) + -> a join' vss f = undefArray (totalSize {arr2} vss) (outer 0 0) - where inner : (n : Bits32) - -> (pos : Bits32) - -> arr2 - -> (1 _ : LinArray (totalSize {arr2} vss) el) - -> LinArray (totalSize {arr2} vss) el - inner n pos as la = - case readMaybe as n of - Just v => inner (assert_smaller n $ n+1) pos as (unsafeWrite la (pos + n) v) - Nothing => la - - outer : (n : Bits32) - -> (pos : Bits32) - -> (1 _ : LinArray (totalSize {arr2} vss) el) - -> a - outer n pos la = - case readMaybe vss n of - Just v => outer (assert_smaller n $ n+1) (pos + size v) (inner 0 pos v la) - Nothing => f la + + where + inner : + (n : Bits32) + -> (pos : Bits32) + -> arr2 + -> (1 _ : LinArray (totalSize {arr2} vss) el) + -> LinArray (totalSize {arr2} vss) el + inner n pos as la = + case readMaybe as n of + Just v => inner (assert_smaller n $ n+1) pos as (unsafeWrite la (pos + n) v) + Nothing => la + + outer : + (n : Bits32) + -> (pos : Bits32) + -> (1 _ : LinArray (totalSize {arr2} vss) el) + -> a + outer n pos la = + case readMaybe vss n of + Just v => outer (assert_smaller n $ n+1) (pos + size v) (inner 0 pos v la) + Nothing => f la -------------------------------------------------------------------------------- -- Immutable Arrays diff --git a/js/src/JS/Attribute.idr b/js/src/JS/Attribute.idr index 66eb338..7e6e31b 100644 --- a/js/src/JS/Attribute.idr +++ b/js/src/JS/Attribute.idr @@ -37,20 +37,23 @@ data Attribute : (alwaysReturns : Bool) Attr : (get : JSIO a) -> (set : a -> JSIO ()) -> Attribute True Prelude.id a ||| A nullable, non-optional attribute. - NullableAttr : (get : JSIO (Maybe a)) - -> (set : Maybe a -> JSIO ()) - -> Attribute False Maybe a + NullableAttr : + (get : JSIO (Maybe a)) + -> (set : Maybe a -> JSIO ()) + -> Attribute False Maybe a ||| An optional attribute with a predefined default value. - OptionalAttr : (get : JSIO (Optional a)) - -> (set : Optional a -> JSIO ()) - -> (def : a) - -> Attribute True Optional a + OptionalAttr : + (get : JSIO (Optional a)) + -> (set : Optional a -> JSIO ()) + -> (def : a) + -> Attribute True Optional a ||| An optional attribute without default value. - OptionalAttrNoDefault : (get : JSIO (Optional a)) - -> (set : Optional a -> JSIO ()) - -> Attribute False Optional a + OptionalAttrNoDefault : + (get : JSIO (Optional a)) + -> (set : Optional a -> JSIO ()) + -> Attribute False Optional a ||| Returns the value of an attribute in its proper context. ||| Typically used in infix notation. @@ -61,10 +64,10 @@ data Attribute : (alwaysReturns : Bool) export get : (o : obj) -> (attr : obj -> Attribute b f a) -> JSIO $ f a get o g = case g o of - Attr gt _ => gt - NullableAttr gt _ => gt - OptionalAttr gt _ _ => gt - OptionalAttrNoDefault gt _ => gt + Attr gt _ => gt + NullableAttr gt _ => gt + OptionalAttr gt _ _ => gt + OptionalAttrNoDefault gt _ => gt ||| Maps a function over the value retrieved from an `Attribute`. export @@ -99,8 +102,8 @@ set' (OptionalAttrNoDefault _ s) = s export getDef : (o : obj) -> (attr : obj -> Attribute True f a) -> JSIO a getDef o g = case g o of - Attr gt _ => gt - OptionalAttr gt _ def => map (fromOptional def) gt + Attr gt _ => gt + OptionalAttr gt _ def => map (fromOptional def) gt ||| Maps a function over the value retrieved from an `Attribute`. ||| Since this operates @@ -219,42 +222,50 @@ a ?> v = a !> const v -------------------------------------------------------------------------------- export -fromPrim : (ToFFI a b, FromFFI a b) - => String - -> (obj -> PrimIO b) - -> (obj -> b -> PrimIO ()) - -> obj - -> Attribute True Prelude.id a +fromPrim : + {auto _ : ToFFI a b} + -> {auto _ : FromFFI a b} + -> String + -> (obj -> PrimIO b) + -> (obj -> b -> PrimIO ()) + -> obj + -> Attribute True Prelude.id a fromPrim msg g s o = Attr (tryJS msg $ g o) (\a => primJS $ s o (toFFI a)) export -fromNullablePrim : (ToFFI a b, FromFFI a b) - => String - -> (obj -> PrimIO $ Nullable b) - -> (obj -> Nullable b -> PrimIO ()) - -> obj - -> Attribute False Maybe a +fromNullablePrim : + {auto _ : ToFFI a b} + -> {auto _ : FromFFI a b} + -> String + -> (obj -> PrimIO $ Nullable b) + -> (obj -> Nullable b -> PrimIO ()) + -> obj + -> Attribute False Maybe a fromNullablePrim msg g s o = NullableAttr (tryJS msg $ g o) (\a => primJS $ s o (toFFI a)) export -fromUndefOrPrim : (ToFFI a b, FromFFI a b) - => String - -> (obj -> PrimIO $ UndefOr b) - -> (obj -> UndefOr b -> PrimIO ()) - -> a - -> obj - -> Attribute True Optional a +fromUndefOrPrim : + {auto _ : ToFFI a b} + -> {auto _ : FromFFI a b} + -> String + -> (obj -> PrimIO $ UndefOr b) + -> (obj -> UndefOr b -> PrimIO ()) + -> a + -> obj + -> Attribute True Optional a fromUndefOrPrim msg g s def o = OptionalAttr (tryJS msg $ g o) (\a => primJS $ s o (toFFI a)) def export -fromUndefOrPrimNoDefault : (ToFFI a b, FromFFI a b) - => String - -> (obj -> PrimIO $ UndefOr b) - -> (obj -> UndefOr b -> PrimIO ()) - -> obj - -> Attribute False Optional a +fromUndefOrPrimNoDefault : + {auto _ : ToFFI a b} + -> {auto _ : FromFFI a b} + -> String + -> (obj -> PrimIO $ UndefOr b) + -> (obj -> UndefOr b -> PrimIO ()) + -> obj + -> Attribute False Optional a fromUndefOrPrimNoDefault msg g s o = OptionalAttrNoDefault (tryJS msg $ g o) (\a => primJS $ s o (toFFI a)) diff --git a/js/src/JS/Boolean.idr b/js/src/JS/Boolean.idr index 26590e8..9e92251 100644 --- a/js/src/JS/Boolean.idr +++ b/js/src/JS/Boolean.idr @@ -24,9 +24,10 @@ ToFFI Bool Boolean where export FromFFI Bool Boolean where - fromFFI v = if eqv v true then Just True - else if eqv v false then Just False - else Nothing + fromFFI v = + if eqv v true then Just True + else if eqv v false then Just False + else Nothing export SafeCast Boolean where diff --git a/js/src/JS/Inheritance.idr b/js/src/JS/Inheritance.idr index 5e04b1d..5279ae5 100644 --- a/js/src/JS/Inheritance.idr +++ b/js/src/JS/Inheritance.idr @@ -51,7 +51,12 @@ infixl 1 :> ||| Operator version of `up`. public export %inline -(:>) : (0 _ : JSType a) => a -> (0 b : Type) -> {auto 0 _ : Elem b (Types a)} -> b +(:>) : + {auto 0 _ : JSType a} + -> a + -> (0 b : Type) + -> {auto 0 _ : Elem b (Types a)} + -> b a :> _ = up a -------------------------------------------------------------------------------- @@ -143,16 +148,18 @@ SafeCast String where -- String here export SafeCast Char where - safeCast v = safeCast v >>= \s => case strM s of - StrCons x "" => Just x - _ => Nothing + safeCast v = safeCast v >>= \s => + case strM s of + StrCons x "" => Just x + _ => Nothing export bounded : Num a => (min : Integer) -> (max : Integer) -> x -> Maybe a bounded min max ptr = - safeCast ptr >>= \n => if n >= min && n <= max - then Just (fromInteger n) - else Nothing + safeCast ptr >>= \n => + if n >= min && n <= max + then Just (fromInteger n) + else Nothing export SafeCast Bits8 where @@ -193,8 +200,8 @@ SafeCast Int where export tryCast : SafeCast a => (fun : Lazy String) -> x -> JSIO a tryCast fun val = case safeCast val of - Just a => pure a - Nothing => throwError $ CastErr fun val + Just a => pure a + Nothing => throwError $ CastErr fun val export tryCast_ : (0 a : Type) -> SafeCast a => (fun : Lazy String) -> x -> JSIO a diff --git a/js/src/JS/Marshall.idr b/js/src/JS/Marshall.idr index d299a09..2ae464f 100644 --- a/js/src/JS/Marshall.idr +++ b/js/src/JS/Marshall.idr @@ -120,8 +120,8 @@ FromFFI WindowProxy WindowProxy where fromFFI = Just export tryFromFFI : FromFFI a ffiRepr => (fun : Lazy String) -> ffiRepr -> JSIO a tryFromFFI fun ptr = case fromFFI ptr of - Nothing => throwError $ CastErr fun ptr - Just v => pure v + Nothing => throwError $ CastErr fun ptr + Just v => pure v export tryJS : FromFFI a ffiRepr => (fun : Lazy String) -> PrimIO ffiRepr -> JSIO a diff --git a/js/src/JS/Nullable.idr b/js/src/JS/Nullable.idr index d2a2d1e..71e3cbe 100644 --- a/js/src/JS/Nullable.idr +++ b/js/src/JS/Nullable.idr @@ -31,7 +31,11 @@ maybeToNullable : Maybe a -> Nullable a maybeToNullable = maybe null nonNull export -mayUp : (0 _ : JSType a) => Maybe a -> {auto 0 _ : Elem b (Types a)} -> Nullable b +mayUp : + {auto 0 _ : JSType a} + -> Maybe a + -> {auto 0 _ : Elem b (Types a)} + -> Nullable b mayUp x = maybe null (\v => nonNull $ up v) x export @@ -45,11 +49,12 @@ ToFFI a b => ToFFI (Maybe a) (Nullable b) where export FromFFI a b => FromFFI (Maybe a) (Nullable b) where fromFFI v = case nullableToMaybe v of - Nothing => Just Nothing - Just x => map Just $ fromFFI x + Nothing => Just Nothing + Just x => map Just $ fromFFI x export SafeCast a => SafeCast (Nullable a) where - safeCast ptr = if isNull ptr - then Just null - else map nonNull $ safeCast ptr + safeCast ptr = + if isNull ptr + then Just null + else map nonNull $ safeCast ptr diff --git a/js/src/JS/Object.idr b/js/src/JS/Object.idr index 6ece302..9413f18 100644 --- a/js/src/JS/Object.idr +++ b/js/src/JS/Object.idr @@ -137,9 +137,11 @@ lsetVal o f v = lset o f (toFFI $ toAny v) export withPairs : List (String,Value) -> ((1 _ : LinObject) -> a) -> a withPairs ps f = newObj (run ps) - where run : List (String,Value) -> (1 _ : LinObject) -> a - run [] o = f o - run ((s,v) :: ps) o = run ps (lsetVal o s v) + + where + run : List (String,Value) -> (1 _ : LinObject) -> a + run [] o = f o + run ((s,v) :: ps) o = run ps (lsetVal o s v) export pairs : List (String,Value) -> Value @@ -154,23 +156,28 @@ vals = Arr . fromList -------------------------------------------------------------------------------- toVal : Any -> Maybe Value -toVal (MkAny ptr) = (Str <$> safeCast ptr) - <|> (Boolean <$> (safeCast ptr >>= fromFFI)) - <|> (if isArray ptr then array ptr else Nothing) - <|> (if isNull ptr then Just Null else Nothing) - <|> (Num <$> safeCast ptr) - <|> (Obj . MkIObject <$> unsafeCastOnTypeof "object" ptr) +toVal (MkAny ptr) = + (Str <$> safeCast ptr) + <|> (Boolean <$> (safeCast ptr >>= fromFFI)) + <|> (if isArray ptr then array ptr else Nothing) + <|> (if isNull ptr then Just Null else Nothing) + <|> (Num <$> safeCast ptr) + <|> (Obj . MkIObject <$> unsafeCastOnTypeof "object" ptr) - where array : a -> Maybe Value - array a = let arr = the (IArray Any) (believe_me a) - in assert_total $ Arr <$> traverse toVal arr + where + array : a -> Maybe Value + array a = + let arr := the (IArray Any) (believe_me a) + in assert_total $ Arr <$> traverse toVal arr export parse : String -> Either JSErr Value -parse s = do ptr <- try prim__parse s - maybe (Left $ Caught #"Unable to decode JSON: \#{s}"#) - Right - (toVal (MkAny ptr)) +parse s = do + ptr <- try prim__parse s + maybe + (Left $ Caught #"Unable to decode JSON: \#{s}"#) + Right + (toVal (MkAny ptr)) export parseMaybe : String -> Maybe Value diff --git a/js/src/JS/Undefined.idr b/js/src/JS/Undefined.idr index c016722..4a9147d 100644 --- a/js/src/JS/Undefined.idr +++ b/js/src/JS/Undefined.idr @@ -65,9 +65,10 @@ def = believe_me export SafeCast a => SafeCast (UndefOr a) where - safeCast ptr = if isUndefined ptr - then Just undef - else map def $ safeCast ptr + safeCast ptr = + if isUndefined ptr + then Just undef + else map def $ safeCast ptr -------------------------------------------------------------------------------- -- Optional @@ -149,14 +150,19 @@ optionalToUndefOr : Optional a -> UndefOr a optionalToUndefOr = optional undef def export -optUp : (0 _ : JSType a) => Optional a -> {auto 0 _ : Elem b (Types a)} -> UndefOr b +optUp : + {auto 0 _ : JSType a} + -> Optional a + -> {auto 0 _ : Elem b (Types a)} + -> UndefOr b optUp x = optional undef (\v => def $ up v) x export -omyUp : (0 _ : JSType a) - => Optional (Maybe a) - -> {auto 0 _ : Elem b (Types a)} - -> UndefOr (Nullable b) +omyUp : + {auto 0 _ : JSType a} + -> Optional (Maybe a) + -> {auto 0 _ : Elem b (Types a)} + -> UndefOr (Nullable b) omyUp x = optionalToUndefOr $ map (\m => mayUp m) x public export @@ -182,5 +188,5 @@ ToFFI a b => ToFFI (Optional a) (UndefOr b) where export FromFFI a b => FromFFI (Optional a) (UndefOr b) where fromFFI v = case undeforToOptional v of - Undef => Just Undef - Def x => map Def $ fromFFI x + Undef => Just Undef + Def x => map Def $ fromFFI x diff --git a/js/src/JS/Util.idr b/js/src/JS/Util.idr index d4efc9c..5737698 100644 --- a/js/src/JS/Util.idr +++ b/js/src/JS/Util.idr @@ -119,9 +119,9 @@ primJS = primIO export unMaybe : (callSite : String) -> JSIO (Maybe a) -> JSIO a -unMaybe callSite io = do Just a <- io - | Nothing => throwError $ IsNothing callSite - pure a +unMaybe callSite io = do + Just a <- io | Nothing => throwError $ IsNothing callSite + pure a -------------------------------------------------------------------------------- -- Error handling @@ -140,18 +140,20 @@ prim__errTag : AnyPtr -> Double prim__errVal : AnyPtr -> AnyPtr toEither : AnyPtr -> Either JSErr a -toEither ptr = if 1 == prim__errTag ptr - then Right (believe_me (prim__errVal ptr)) - else Left $ Caught (believe_me (prim__errVal ptr)) +toEither ptr = + if 1 == prim__errTag ptr + then Right (believe_me (prim__errVal ptr)) + else Left $ Caught (believe_me (prim__errVal ptr)) ||| Tries to execute an IO action, wrapping any runtime exception ||| in its stringified version in a `Left . Caught`. export tryIO : IO a -> JSIO a -tryIO io = do ptr <- primIO $ prim__tryIO io - if 1 == prim__errTag ptr - then pure (believe_me (prim__errVal ptr)) - else throwError $ Caught (believe_me (prim__errVal ptr)) +tryIO io = do + ptr <- primIO $ prim__tryIO io + if 1 == prim__errTag ptr + then pure (believe_me (prim__errVal ptr)) + else throwError $ Caught (believe_me (prim__errVal ptr)) ||| Error handling in pure functions. This should only be used ||| in foreign function calls that might fail but or otherwise diff --git a/js/test/src/Array.idr b/js/test/src/Array.idr index c8a07b7..6938472 100644 --- a/js/test/src/Array.idr +++ b/js/test/src/Array.idr @@ -14,42 +14,44 @@ arrInt : Gen (IArray Int) arrInt = map fromList ints prop_sizeEmpty : Property -prop_sizeEmpty = - property $ do ns <- forAll (pure $ the (List Int32) Nil) - size (JS.Array.fromList ns) === 0 +prop_sizeEmpty = property $ do + ns <- forAll (pure $ the (List Int32) Nil) + size (JS.Array.fromList ns) === 0 prop_size : Property -prop_size = - property $ do ns <- forAll ints - size (JS.Array.fromList ns) === - fromInteger (natToInteger $ length ns) +prop_size = property $ do + ns <- forAll ints + size (JS.Array.fromList ns) === fromInteger (natToInteger $ length ns) prop_fromListToList : Property -prop_fromListToList = - property $ do ns <- forAll ints - ns === arrayToList (JS.Array.fromList ns) +prop_fromListToList = property $ do + ns <- forAll ints + ns === arrayToList (JS.Array.fromList ns) prop_fromString : Property -prop_fromString = - property $ do s <- forAll $ string (linear 0 20) ascii - unpack s === arrayToList (fromString s) +prop_fromString = property $ do + s <- forAll $ string (linear 0 20) ascii + unpack s === arrayToList (fromString s) prop_map : Property -prop_map = property $ do arr <- forAll arrInt - map id arr === arr +prop_map = property $ do + arr <- forAll arrInt + map id arr === arr prop_join : Property -prop_join = property $ do iss <- forAll intss - join iss === - (arrayToList . JS.Array.concat) (fromList $ map fromList iss) +prop_join = property $ do + iss <- forAll intss + join iss === + (arrayToList . JS.Array.concat) (fromList $ map fromList iss) export test : IO () -test = ignore . checkGroup . withTests 100 $ MkGroup "Arrays" [ - ("prop_sizeEmpty", prop_sizeEmpty) - , ("prop_size", prop_size) - , ("prop_fromListToList", prop_fromListToList) - , ("prop_fromString", prop_fromString) - , ("prop_map", prop_map) - , ("prop_join", prop_join) - ] +test = + ignore . checkGroup . withTests 100 $ MkGroup "Arrays" + [ ("prop_sizeEmpty", prop_sizeEmpty) + , ("prop_size", prop_size) + , ("prop_fromListToList", prop_fromListToList) + , ("prop_fromString", prop_fromString) + , ("prop_map", prop_map) + , ("prop_join", prop_join) + ] diff --git a/js/test/src/Main.idr b/js/test/src/Main.idr index 482e4d2..7c28bcc 100644 --- a/js/test/src/Main.idr +++ b/js/test/src/Main.idr @@ -5,6 +5,7 @@ import Object import Util main : IO () -main = do Array.test - Util.test - Object.test +main = do + Array.test + Util.test + Object.test diff --git a/js/test/src/Object.idr b/js/test/src/Object.idr index 023aaf4..9b93608 100644 --- a/js/test/src/Object.idr +++ b/js/test/src/Object.idr @@ -23,22 +23,25 @@ toStr s = #"{"street":\#{show s.street},"nr":\#{show s.nr},"zip":\#{show s.zip}, -- Encoding via `stringify`. toJSON : Address -> String -toJSON a = let ps = [ ("street",Str a.street) - , ("nr", Num . fromInteger $ cast a.nr) - , ("zip", Str a.zip) - , ("city", Str a.city) - ] - in stringify (pairs ps) +toJSON a = + let ps := + [ ("street",Str a.street) + , ("nr", Num . fromInteger $ cast a.nr) + , ("zip", Str a.zip) + , ("city", Str a.city) + ] + in stringify (pairs ps) export fromJSON : String -> Maybe Address -fromJSON s = - do val <- parseMaybe s - obj <- getObject val - [| MkAddress (valueAt obj "street" >>= getStr) - (valueAt obj "nr" >>= map (fromInteger . cast) . getNum) - (valueAt obj "zip" >>= getStr) - (valueAt obj "city" >>= getStr) |] +fromJSON s = do + val <- parseMaybe s + obj <- getObject val + [| MkAddress + (valueAt obj "street" >>= getStr) + (valueAt obj "nr" >>= map (fromInteger . cast) . getNum) + (valueAt obj "zip" >>= getStr) + (valueAt obj "city" >>= getStr) |] -------------------------------------------------------------------------------- -- Generators @@ -50,34 +53,39 @@ plainString = string (linear 1 10) alphaNum export addresses : Gen Address -addresses = [| MkAddress plainString - (bits32 $ linear 0 50) - plainString - plainString |] +addresses = + [| MkAddress + plainString + (bits32 $ linear 0 50) + plainString + plainString |] -------------------------------------------------------------------------------- -- Properties -------------------------------------------------------------------------------- prop_toJSON : Property -prop_toJSON = property $ do a <- forAll addresses - toStr a === toJSON a +prop_toJSON = property $ do + a <- forAll addresses + toStr a === toJSON a prop_decode : Property -prop_decode = property $ do a <- forAll addresses - case parse (toJSON a) of - Left e => do footnote (dispErr e) - assert False - Right _ => assert True +prop_decode = property $ do + a <- forAll addresses + case parse (toJSON a) of + Left e => do footnote (dispErr e) + assert False + Right _ => assert True prop_roundTrip : Property -prop_roundTrip = property $ do a <- forAll addresses - Just a === fromJSON (toJSON a) +prop_roundTrip = property $ do + a <- forAll addresses + Just a === fromJSON (toJSON a) export test : IO () -test = ignore . checkGroup . withTests 100 $ MkGroup "Object" [ - ("prop_toJSON", prop_toJSON) - , ("prop_decode", prop_decode) - , ("prop_roundTrip", prop_roundTrip) - ] +test = ignore . checkGroup . withTests 100 $ MkGroup "Object" + [ ("prop_toJSON", prop_toJSON) + , ("prop_decode", prop_decode) + , ("prop_roundTrip", prop_roundTrip) + ] diff --git a/js/test/src/Util.idr b/js/test/src/Util.idr index c435051..63f7259 100644 --- a/js/test/src/Util.idr +++ b/js/test/src/Util.idr @@ -9,34 +9,34 @@ import Data.Either -------------------------------------------------------------------------------- prop_int_notUndefined : Property -prop_int_notUndefined = - property $ do n <- forAll (int (linear 0 1000)) - assert (not $ isUndefined n) +prop_int_notUndefined = property $ do + n <- forAll (int (linear 0 1000)) + assert (not $ isUndefined n) prop_string_notUndefined : Property -prop_string_notUndefined = - property $ do n <- forAll (string (linear 0 20) unicode) - assert (not $ isUndefined n) +prop_string_notUndefined = property $ do + n <- forAll (string (linear 0 20) unicode) + assert (not $ isUndefined n) prop_undefinedIsUndefined : Property -prop_undefinedIsUndefined = - withTests 1 . property $ do u <- forAll (pure undefined) - assert (isUndefined u) +prop_undefinedIsUndefined = withTests 1 . property $ do + u <- forAll (pure undefined) + assert (isUndefined u) prop_int_notNull : Property -prop_int_notNull = - property $ do n <- forAll (int (linear 0 1000)) - assert (not $ isNull n) +prop_int_notNull = property $ do + n <- forAll (int (linear 0 1000)) + assert (not $ isNull n) prop_string_notNull : Property -prop_string_notNull = - property $ do n <- forAll (string (linear 0 20) unicode) - assert (not $ isNull n) +prop_string_notNull = property $ do + n <- forAll (string (linear 0 20) unicode) + assert (not $ isNull n) prop_undefinedIsNull : Property -prop_undefinedIsNull = - withTests 1 . property $ do u <- forAllWith (const "null") (pure $ null {a = Int}) - assert (isNull u) +prop_undefinedIsNull = withTests 1 . property $ do + u <- forAllWith (const "null") (pure $ null {a = Int}) + assert (isNull u) invalidJSON : Gen String invalidJSON = ("{" ++) <$> string (linear 0 10) alphaNum @@ -45,20 +45,22 @@ invalidJSON = ("{" ++) <$> string (linear 0 10) alphaNum prim__parse : String -> AnyPtr prop_try : Property -prop_try = property $ do s <- forAll invalidJSON - assert $ isLeft (try prim__parse s) +prop_try = property $ do + s <- forAll invalidJSON + assert $ isLeft (try prim__parse s) undefinedProps : Group -undefinedProps = MkGroup "Undefined and Null" - [ ("prop_int_notUndefined", prop_int_notUndefined) - , ("prop_string_notUndefined", prop_string_notUndefined) - , ("prop_undefinedIsUndefined", prop_undefinedIsUndefined) - , ("prop_int_notNull", prop_int_notNull) - , ("prop_string_notNull", prop_string_notNull) - , ("prop_undefinedIsNull", prop_undefinedIsNull) - , ("prop_try", prop_try) - ] +undefinedProps = + MkGroup "Undefined and Null" + [ ("prop_int_notUndefined", prop_int_notUndefined) + , ("prop_string_notUndefined", prop_string_notUndefined) + , ("prop_undefinedIsUndefined", prop_undefinedIsUndefined) + , ("prop_int_notNull", prop_int_notNull) + , ("prop_string_notNull", prop_string_notNull) + , ("prop_undefinedIsNull", prop_undefinedIsNull) + , ("prop_try", prop_try) + ] export test : IO () -test = do ignore $ checkGroup undefinedProps +test = ignore $ checkGroup undefinedProps diff --git a/src/Web/Dom.idr b/src/Web/Dom.idr index 285a250..7812e17 100644 --- a/src/Web/Dom.idr +++ b/src/Web/Dom.idr @@ -394,10 +394,10 @@ newElement : -> (0 e : ElementType tag t) -> (mods : List (t -> JSIO ())) -> JSIO t -newElement e mods = - do res <- createElement e - for_ mods $ \m => m res - pure res +newElement e mods = do + res <- createElement e + for_ mods $ \m => m res + pure res -------------------------------------------------------------------------------- -- Finding Elements @@ -481,9 +481,8 @@ Callback EventListener (Event -> JSIO ()) where callback f = toEventListener (runJS . f) export -Callback MutationCallback ( Array MutationRecord - -> MutationObserver - -> JSIO () ) where +Callback MutationCallback + (Array MutationRecord -> MutationObserver -> JSIO ()) where callback f = toMutationCallback $ \a,m => runJS (f a m) ||| In case of an error, the error is logged to the console and @@ -494,7 +493,9 @@ Callback NodeFilter (Node -> JSIO Bits16) where export Callback XPathNSResolver (Maybe String -> JSIO (Maybe String) ) where - callback f = toXPathNSResolver $ map maybeToNullable - . runJSWithDefault Nothing - . f - . nullableToMaybe + callback f = + toXPathNSResolver $ + map maybeToNullable + . runJSWithDefault Nothing + . f + . nullableToMaybe diff --git a/src/Web/Html.idr b/src/Web/Html.idr index c8a2845..e0783bf 100644 --- a/src/Web/Html.idr +++ b/src/Web/Html.idr @@ -40,12 +40,14 @@ Callback OnErrorEventHandlerNonNull ( HSum [Event, String] -> JSIO Any ) where callback f = toOnErrorEventHandlerNonNull $ \u,b,c,d,e => - map toFFI $ runJSWithDefault (MkAny ()) $ - do ns <- tryFromFFI "JS.Html.ErrorEventHandlerNonNull.callback" u - f ns (undeforToOptional b) - (undeforToOptional c) - (undeforToOptional d) - (MkAny <$> undeforToOptional e) + map toFFI $ runJSWithDefault (MkAny ()) $ do + ns <- tryFromFFI "JS.Html.ErrorEventHandlerNonNull.callback" u + f + ns + (undeforToOptional b) + (undeforToOptional c) + (undeforToOptional d) + (MkAny <$> undeforToOptional e) export Callback FocusEventHandler (FocusEvent -> JSIO ()) where