Skip to content

Commit

Permalink
[ style ] adhere to coding style (#51)
Browse files Browse the repository at this point in the history
  • Loading branch information
@stefan-hoeck
stefan-hoeck authored Aug 20, 2023
1 parent 9b68ee4 commit 650f991
Show file tree
Hide file tree
Showing 16 changed files with 420 additions and 328 deletions.
89 changes: 49 additions & 40 deletions docs/src/Tutorial.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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`.
Expand Down Expand Up @@ -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 ()
Expand Down Expand Up @@ -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
Expand Down
196 changes: 112 additions & 84 deletions js/src/JS/Array.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -317,27 +327,30 @@ 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
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

Expand All @@ -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
Expand Down
Loading

0 comments on commit 650f991

Please sign in to comment.