[ style ] adhere to coding style guide (#61)

stefan-hoeck · Aug 22, 2023 · 42f6d05 · 42f6d05
1 parent 29ecd85
commit 42f6d05
Show file tree

Hide file tree

Showing 17 changed files with 301 additions and 250 deletions.
diff --git a/docs/src/Examples/Balls.md b/docs/src/Examples/Balls.md
@@ -121,7 +121,7 @@ wallThickness = 0.20
 -- walls and floor of the room.
 walls : Shape
 walls =
-  let hwt = wallThickness / 2
+  let hwt := wallThickness / 2
    in polyLine [(-hwt, 0), (-hwt, w+hwt), (w+hwt,w+hwt), (w+hwt,0)]
 ```
 
@@ -160,12 +160,13 @@ content : Node Ev
 content =
   div [ class ballsContent ]
     [ lbl "Number of balls:" lblCount
-    , input [ ref txtCount
-            , onInput (const NumIn)
-            , onEnterDown Run
-            , class widget
-            , placeholder "Range: [1,1000]"
-            ] []
+    , input
+        [ ref txtCount
+        , onInput (const NumIn)
+        , onEnterDown Run
+        , class widget
+        , placeholder "Range: [1,1000]"
+        ] []
     , button [ref btnRun, onClick Run, classes [widget,btn]] ["Run"]
     , div [ref log] []
     , canvas [ref out, width wcanvas, height wcanvas] []
@@ -208,9 +209,9 @@ checkBounds b@(MkBall c [px,py] [vx,vy]) =
 -- by adjusting its position and velocity
 nextBall : DTime -> Ball -> Ball
 nextBall delta (MkBall c p v) =
-  let dt   = cast delta / the Double 1000 -- time in seconds
-      v2   = v ^+^ (dt *^ acc)
-      p2   = p ^+^ (dt / 2 *^ (v ^+^ v2))
+  let dt := cast delta / the Double 1000 -- time in seconds
+      v2 := v ^+^ (dt *^ acc)
+      p2 := p ^+^ (dt / 2 *^ (v ^+^ v2))
    in checkBounds (MkBall c p2 v2)
 ```
 
@@ -224,23 +225,25 @@ slightly different colors and starting velocities:
 export
 initialBalls : (n : Nat) -> List Ball
 initialBalls n = go n Nil
-  where col : Bits8 -> Color
-        col 0 = comp100
-        col 1 = comp80
-        col 2 = comp60
-        col 3 = comp40
-        col _ = comp20
-
-        ball : Nat -> Ball
-        ball k =
-          let factor = cast {to = Double} k / (cast n - 1.0)
-              phi    = pi * factor
-              x0     = 1.0 + factor * 8
-           in MkBall (col $ cast k `mod` 5) [x0,9] (v0 *^ [sin phi, cos phi])
-
-        go : (k : Nat) -> List Ball -> List Ball
-        go 0     bs = bs
-        go (S k) bs = go k $ ball k :: bs
+
+  where
+    col : Bits8 -> Color
+    col 0 = comp100
+    col 1 = comp80
+    col 2 = comp60
+    col 3 = comp40
+    col _ = comp20
+
+    ball : Nat -> Ball
+    ball k =
+      let factor = cast {to = Double} k / (cast n - 1.0)
+          phi    = pi * factor
+          x0     = 1.0 + factor * 8
+       in MkBall (col $ cast k `mod` 5) [x0,9] (v0 *^ [sin phi, cos phi])
+
+    go : (k : Nat) -> List Ball -> List Ball
+    go 0     bs = bs
+    go (S k) bs = go k $ ball k :: bs
 ```
 
 The controller handling the animation will use a state
@@ -250,7 +253,8 @@ number of milliseconds:
 ```idris
 renderBalls : List Ball -> JSIO ()
 renderBalls bs =
-  liftJSIO . render $ MkCanvas out (cast wcanvas) (cast wcanvas) (ballsToScene bs)
+  liftJSIO . render $
+    MkCanvas out (cast wcanvas) (cast wcanvas) (ballsToScene bs)
 
 animation : List Ball -> MSF JSIO Ev ()
 animation bs =
@@ -266,20 +270,23 @@ input and running the application:
 ```idris
 read : String -> Either String (List Ball)
 read s =
-  let n = cast {to = Nat} s
+  let n := cast {to = Nat} s
    in if 0 < n && n <= 1000
         then Right (initialBalls n)
         else Left "Enter a number between 1 and 1000"
 
 msf : MSF JSIO Ev ()
 msf = drswitchWhen neutral initialBalls animation
-  where readInit : MSF JSIO Ev (Either String (List Ball))
-        readInit =    getInput NumIn read txtCount
-                 >>>  observeWith (isLeft ^>> disabledAt btnRun)
 
-        initialBalls : MSF JSIO Ev (MSFEvent $ List Ball)
-        initialBalls =   fan [readInit, is Run]
-                     >>> rightOnEvent
+  where
+    readInit : MSF JSIO Ev (Either String (List Ball))
+    readInit =
+          getInput NumIn read txtCount
+      >>> observeWith (isLeft ^>> disabledAt btnRun)
+
+    initialBalls : MSF JSIO Ev (MSFEvent $ List Ball)
+    initialBalls =
+      fan [readInit, is Run] >>> rightOnEvent
 
 export
 ui : Handler JSIO Ev => JSIO (MSF JSIO Ev (), JSIO ())

diff --git a/docs/src/Examples/CSS.md b/docs/src/Examples/CSS.md
@@ -44,13 +44,14 @@ be found in the corresponding submodules).
 ```idris
 export
 allRules : String
-allRules =  fastUnlines . map interpolate
-         $  coreCSS
-         ++ Balls.css
-         ++ Fractals.css
-         ++ MathGame.css
-         ++ Performance.css
-         ++ Reset.css
+allRules =
+  fastUnlines . map interpolate
+    $  coreCSS
+    ++ Balls.css
+    ++ Fractals.css
+    ++ MathGame.css
+    ++ Performance.css
+    ++ Reset.css
 ```
 
 <!-- vi: filetype=idris2:syntax=markdown

diff --git a/docs/src/Examples/Fractals.idr b/docs/src/Examples/Fractals.idr
@@ -38,9 +38,10 @@ record Iterations where
 
 namespace Iterations
   export
-  fromInteger :  (n : Integer)
-              -> {auto 0 prf : LTE (fromInteger n) MaxIter}
-              -> Iterations
+  fromInteger :
+       (n : Integer)
+    -> {auto 0 prf : LTE (fromInteger n) MaxIter}
+    -> Iterations
   fromInteger n = MkIterations (cast n) prf
 
   export
@@ -81,21 +82,25 @@ record Config where
 
 msf : (timer : RedrawAfter -> JSIO ()) -> MSF JSIO Ev ()
 msf timer = drswitchWhen neutral config fractal
-  where fractal : Config -> MSF JSIO Ev ()
-        fractal c =
-          let Element dragons prf = mkDragons c.iterations.value
-           in ifIs Inc $ cycle dragons >>> innerHtml out
-
-        readAll : MSF JSIO Ev (Either String Config)
-        readAll =    MkConfig Dragon
-                <$$> getInput Iter   read txtIter
-                <**> getInput Redraw read txtRedraw
-                >>>  observeWith (isLeft ^>> disabledAt btnRun)
-
-        config : MSF JSIO Ev (MSFEvent Config)
-        config =   fan [readAll, is Run]
-               >>> rightOnEvent
-               >>> observeWith (ifEvent $ arrM (liftJSIO . timer . redraw))
+
+  where
+    fractal : Config -> MSF JSIO Ev ()
+    fractal c =
+      let Element dragons prf := mkDragons c.iterations.value
+       in ifIs Inc $ cycle dragons >>> innerHtml out
+
+    readAll : MSF JSIO Ev (Either String Config)
+    readAll =
+           MkConfig Dragon
+      <$$> getInput Iter   read txtIter
+      <**> getInput Redraw read txtRedraw
+      >>>  observeWith (isLeft ^>> disabledAt btnRun)
+
+    config : MSF JSIO Ev (MSFEvent Config)
+    config =
+          fan [readAll, is Run]
+      >>> rightOnEvent
+      >>> observeWith (ifEvent $ arrM (liftJSIO . timer . redraw))
 
 --------------------------------------------------------------------------------
 --          View
@@ -105,19 +110,21 @@ content : Node Ev
 content =
   div [ class fractalContent ]
     [ lbl "Number of iterations:" lblIter
-    , input [ ref txtIter
-            , onInput (const Iter)
-            , onEnterDown Run
-            , class widget
-            , placeholder "Range: [0, \{show MaxIter}]"
-            ] []
+    , input
+        [ ref txtIter
+        , onInput (const Iter)
+        , onEnterDown Run
+        , class widget
+        , placeholder "Range: [0, \{show MaxIter}]"
+        ] []
     , lbl "Iteration delay [ms]:" lblDelay
-    , input [ ref txtRedraw
-            , onInput (const Redraw)
-            , onEnterDown Run
-            , class widget
-            , placeholder "Range: [100,10'000]"
-            ] []
+    , input
+        [ ref txtRedraw
+        , onInput (const Redraw)
+        , onEnterDown Run
+        , class widget
+        , placeholder "Range: [100,10'000]"
+        ] []
     , button [ref btnRun, onClick Run, classes [widget,btn]] ["Run"]
     , div [ref out] []
     ]

diff --git a/docs/src/Examples/Fractals/Dragon.idr b/docs/src/Examples/Fractals/Dragon.idr
@@ -28,10 +28,11 @@ rotateAround90 o p = rotate90 (p - o) + o
 Dragon : Type
 Dragon = Subset (List Point) NonEmpty
 
-0 lemma :  (as : List a)
-        -> (v : a)
-        -> (as2 : List a)
-        -> NonEmpty (as ++ v :: as2)
+0 lemma :
+     (as : List a)
+  -> (v : a)
+  -> (as2 : List a)
+  -> NonEmpty (as ++ v :: as2)
 lemma []       v as2 = IsNonEmpty
 lemma (h :: t) v as2 = IsNonEmpty
 
@@ -45,17 +46,19 @@ nextDragon (Element (h :: t) prf) =
 
 dragonSVG : (n : Nat) -> Dragon -> String
 dragonSVG n (Element ps _) =
-  let fact = pow 2 (cast (n + 2) / 2.0)
-      scale = 1.0 / fact
+  let fact   := pow 2 (cast (n + 2) / 2.0)
+      scale  := 1.0 / fact
 
-      attr = fastConcat $ map (\(P x y) => #"\#{show x}, \#{show y} "#) ps
-      header =
-        the String #"""
-                   <svg version="1.1"
-                        width="100%"
-                        viewBox="0 0 1000 1000"
-                        xmlns="http://www.w3.org/2000/svg">
-                   """#
+      attr   := fastConcat $ map (\(P x y) => #"\#{show x}, \#{show y} "#) ps
+      header :=
+        the
+          String
+          #"""
+          <svg version="1.1"
+               width="100%"
+               viewBox="0 0 1000 1000"
+               xmlns="http://www.w3.org/2000/svg">
+          """#
    in #"""
       \#{header}
         <polyline points="\#{attr}"
@@ -70,10 +73,12 @@ dragonSVG n (Element ps _) =
 export
 mkDragons : (n : Nat) -> Subset (List String) NonEmpty
 mkDragons n =
-  let fd   = firstDragon
+  let fd := firstDragon
    in Element (dragonSVG 0 fd :: go fd n 1) IsNonEmpty
-  where go : Dragon -> (rem : Nat) -> (iter : Nat) -> List String
-        go _  0     _ = Nil
-        go dr (S k) n =
-          let nextDr = nextDragon dr
-           in dragonSVG n nextDr :: go nextDr k (n+1)
+
+  where
+    go : Dragon -> (rem : Nat) -> (iter : Nat) -> List String
+    go _  0     _ = Nil
+    go dr (S k) n =
+      let nextDr := nextDragon dr
+       in dragonSVG n nextDr :: go nextDr k (n+1)