[ style ] adhere to coding style guide

src/Text/Show/Diff.idr

@@ -13,29 +13,32 @@ import public Text.Show.Pretty
 --------------------------------------------------------------------------------
 
 public export
-data ValueDiff = Con VName (List ValueDiff)
-               | Rec VName (List (VName, ValueDiff))
-               | Tuple ValueDiff ValueDiff (List ValueDiff)
-               | Lst (List ValueDiff)
-               | Same Value
-               | Diff Value Value
+data ValueDiff : Type where
+  Con    : VName -> List ValueDiff -> ValueDiff
+  Rec    : VName -> List (VName, ValueDiff) -> ValueDiff
+  Tuple  : ValueDiff -> ValueDiff -> List ValueDiff -> ValueDiff
+  Lst    : List ValueDiff -> ValueDiff
+  Same   : Value -> ValueDiff
+  Diff   : Value -> Value -> ValueDiff
 
 %runElab derive "ValueDiff" [Show,Eq,PrettyVal]
 
 public export
-data LineDiff = LineSame String
-              | LineRemoved String
-              | LineAdded String
+data LineDiff : Type where
+  LineSame    : String -> LineDiff
+  LineRemoved : String -> LineDiff
+  LineAdded   : String -> LineDiff
 
 %runElab derive "LineDiff" [Show,Eq,PrettyVal]
 
 public export
-data DocDiff = DocSame Nat String
-             | DocRemoved Nat String
-             | DocAdded Nat String
-             | DocOpen Nat String
-             | DocItem Nat String (List DocDiff)
-             | DocClose Nat String
+data DocDiff : Type where
+  DocSame    : Nat -> String -> DocDiff
+  DocRemoved : Nat -> String -> DocDiff
+  DocAdded   : Nat -> String -> DocDiff
+  DocOpen    : Nat -> String -> DocDiff
+  DocItem    : Nat -> String -> List DocDiff -> DocDiff
+  DocClose   : Nat -> String -> DocDiff
 
 %runElab derive "DocDiff" [Show,Eq,PrettyVal]
 
@@ -66,11 +69,13 @@ zipDiffP sx ((n1,x) :: xs) ((n2,y) :: ys) =
 zipDiffP _ _ _ = Nothing
 
 valueDiff x@(Con nx xs) y@(Con ny ys) =
-    if nx == ny then maybe (Diff x y) (Con ny) (zipDiff [<] xs ys)
-    else Diff x y
+    if nx == ny
+       then maybe (Diff x y) (Con ny) (zipDiff [<] xs ys)
+       else Diff x y
 valueDiff x@(Rec nx xs) y@(Rec ny ys) =
-    if nx == ny then maybe (Diff x y) (Rec ny) (zipDiffP [<] xs ys)
-    else Diff x y
+    if nx == ny
+       then maybe (Diff x y) (Rec ny) (zipDiffP [<] xs ys)
+       else Diff x y
 valueDiff x@(Lst xs) y@(Lst ys) = maybe (Diff x y) Lst (zipDiff [<] xs ys)
 valueDiff x@(Tuple x1 x2 xs) y@(Tuple y1 y2 ys) = case zipDiff [<] xs ys of
   Nothing => Diff x y
@@ -86,13 +91,14 @@ take f v = case v of
   Same x       => x
   Diff x y     => f x y
 
-  where ts : List ValueDiff -> List Value
-        ts []       = []
-        ts (h :: t) = take f h :: ts t
+  where
+    ts : List ValueDiff -> List Value
+    ts []       = []
+    ts (h :: t) = take f h :: ts t
 
-        tsP : List (a,ValueDiff) -> List (a,Value)
-        tsP []           = []
-        tsP ((a,h) :: t) = (a,take f h) :: tsP t
+    tsP : List (a,ValueDiff) -> List (a,Value)
+    tsP []           = []
+    tsP ((a,h) :: t) = (a,take f h) :: tsP t
 
 export
 takeLeft : ValueDiff -> Value
@@ -223,7 +229,9 @@ collapseOpen [] = []
 
 dropLeadingSep : List DocDiff -> List DocDiff
 dropLeadingSep (DocOpen oind bra :: DocItem ind pre xs :: ys) =
-  DocOpen oind bra :: DocItem (ind + length pre) "" (dropLeadingSep xs) :: dropLeadingSep ys
+     DocOpen oind bra
+  :: DocItem (ind + length pre) "" (dropLeadingSep xs)
+  :: dropLeadingSep ys
 dropLeadingSep (DocItem ind pre xs :: ys) =
   DocItem ind pre (dropLeadingSep xs) :: dropLeadingSep ys
 dropLeadingSep (x :: xs) = x :: dropLeadingSep xs

src/Text/Show/PrettyVal.idr

@@ -101,5 +101,5 @@ PrettyVal a => PrettyVal (Vect n a) where
 public export
 (PrettyVal a, PrettyVal b) => PrettyVal (a,b) where
   prettyVal (a,b) = case prettyVal b of
-                         Tuple v1 v2 vs => Tuple (prettyVal a) v1 (v2 :: vs)
-                         val            => Tuple (prettyVal a) val []
+    Tuple v1 v2 vs => Tuple (prettyVal a) v1 (v2 :: vs)
+    val            => Tuple (prettyVal a) val []

src/Text/Show/PrettyVal/Derive.idr

@@ -23,8 +23,10 @@ public export
 rec : String -> List (Value,String) -> Value
 rec con [] = Con (MkName con) []
 rec con ps = Rec (MkName con) $ map (\(v,n) => (MkName n, v)) ps
-  where named : Value -> String -> (VName,Value)
-        named v name = (MkName name, v)
+
+  where
+    named : Value -> String -> (VName,Value)
+    named v name = (MkName name, v)
 
 -- Displays an applied constructer with unnamed arguments.
 public export
@@ -87,6 +89,7 @@ parameters (nms : List Name)
   export
   pvClauses : (fun : Maybe Name) -> TypeInfo -> List Clause
   pvClauses fun ti = map clause ti.cons
+
     where
       lhs : TTImp -> TTImp
       lhs bc = maybe bc ((`app` bc) . var) fun

test/src/Main.idr

@@ -10,8 +10,5 @@ main : IO ()
 main = do
   res <- testAll [ lexTest, parseTest, ppTest ]
   if res
-     then putStrLn (foreground Green "\n\nAll tests passed") >>
-          exitSuccess
-
-     else putStrLn (foreground Red "\n\nSome tests failed") >>
-          exitFailure
+    then putStrLn (foreground Green "\n\nAll tests passed") >> exitSuccess
+    else putStrLn (foreground Red "\n\nSome tests failed") >> exitFailure

test/src/PP.idr

@@ -17,33 +17,35 @@ pair x = (x, x ++ "\n")
 
 export
 ppTest : IO Bool
-ppTest = testAll
-  [ testPP "naturals" $ map pair ["0","123","10000"]
-
-  , testPP "chars" $ map pair ["'a'", "'0'", "'Z'"]
-
-  , testPP "doubles" $ map pair ["1.232", "1.0e-12", "16.5E3"]
-
-  , testPP "strings" $ map pair ["\"1.232\"", "\"ab cde\"", "\"foo\""]
-
-  , testPP "negative" $ map pair ["-12", "-1.233e12", "-0"]
-
-  , testPP "lists" [ ("[1,2,3]", "[1, 2, 3]\n")
-                   , ("[]", "[]\n")
-                   , ("['a','b','c']", "['a', 'b', 'c']\n")
-                   ]
-  , testPP "identifiers" $
-      map pair ["Ident", "Foo", "H", "_foo"]
-
-  , testPP "arity 1 cons" $
-      map pair ["Ident 12", "Foo 'a'", "H ()", "_foo 1.22"]
-
-  , testPP "arity 2 cons" $
-      map pair ["Ident 12 'a'", "Foo 'a' \"bar\"", "H () 12", "_foo 1.22 (-1)"]
-
-  , testPP "nested cons" $
-      map pair ["Ident 12 (Foo 'a') (Maybe 12)"
-               , "Foo (Left 'a') (MkPair \"bar \" 1.20)"
-               , "Bracket (TH 12) (Element 12 _) (-12.1)"
-               ]
-  ]
+ppTest =
+  testAll
+    [ testPP "naturals" $ map pair ["0","123","10000"]
+    , testPP "chars" $ map pair ["'a'", "'0'", "'Z'"]
+    , testPP "doubles" $ map pair ["1.232", "1.0e-12", "16.5E3"]
+    , testPP "strings" $ map pair ["\"1.232\"", "\"ab cde\"", "\"foo\""]
+    , testPP "negative" $ map pair ["-12", "-1.233e12", "-0"]
+    , testPP
+        "lists"
+        [ ("[1,2,3]", "[1, 2, 3]\n") , ("[]", "[]\n")
+        , ("['a','b','c']", "['a', 'b', 'c']\n")
+        ]
+    , testPP "identifiers" $ map pair ["Ident", "Foo", "H", "_foo"]
+    , testPP "arity 1 cons" $
+        map pair ["Ident 12", "Foo 'a'", "H ()", "_foo 1.22"]
+    , testPP "arity 2 cons" $
+        map
+          pair
+          [ "Ident 12 'a'"
+          , "Foo 'a' \"bar\""
+          , "H () 12"
+          , "_foo 1.22 (-1)"
+          ]
+
+    , testPP "nested cons" $
+        map
+          pair
+          ["Ident 12 (Foo 'a') (Maybe 12)"
+          , "Foo (Left 'a') (MkPair \"bar \" 1.20)"
+          , "Bracket (TH 12) (Element 12 _) (-12.1)"
+          ]
+    ]

test/src/Parser.idr

@@ -93,16 +93,17 @@ symbolTokens = mapPairs (pure . symb) symbols
 
 export
 lexTest : IO Bool
-lexTest = testAll [
-    testLex "nat literals" natTokens
-  , testLex "string literals" stringTokens
-  , testLex "char literals" charTokens
-  , testLex "float literals" doubleTokens
-  , testLex "spaces" spaceTokens
-  , testLex "identifiers" identTokens
-  , testLex "operators" opTokens
-  , testLex "symbols" symbolTokens
-  ]
+lexTest =
+  testAll
+    [ testLex "nat literals" natTokens
+    , testLex "string literals" stringTokens
+    , testLex "char literals" charTokens
+    , testLex "float literals" doubleTokens
+    , testLex "spaces" spaceTokens
+    , testLex "identifiers" identTokens
+    , testLex "operators" opTokens
+    , testLex "symbols" symbolTokens
+    ]
 
 --------------------------------------------------------------------------------
 --          Parsing
@@ -166,21 +167,22 @@ export
 recs2 : List (String,Value)
 recs2 =
   [| rec3
-     (List.take 20 primsOrCons)
-     (MkName <$> List.take 2 identOrOps)
-     (MkName <$> List.take 2 identOrOps)
-     (MkName <$> List.take 2 identOrOps)
-     (List.take 5 doubleCons)
+       (List.take 20 primsOrCons)
+       (MkName <$> List.take 2 identOrOps)
+       (MkName <$> List.take 2 identOrOps)
+       (MkName <$> List.take 2 identOrOps)
+       (List.take 5 doubleCons)
   |]
 
 export
 parseTest : IO Bool
-parseTest = testAll
-  [ testParse "primitives" prims
-  , testParse "negated" negated
-  , testParse "cons arity 1" singleCons
-  , testParse "cons arity 2" doubleCons
-  , testParse "empty records" emptyRecs
-  , testParse "records of arity 1" recs1
-  , testParse "records of arity 2" recs2
-  ]
+parseTest =
+  testAll
+    [ testParse "primitives" prims
+    , testParse "negated" negated
+    , testParse "cons arity 1" singleCons
+    , testParse "cons arity 2" doubleCons
+    , testParse "empty records" emptyRecs
+    , testParse "records of arity 1" recs1
+    , testParse "records of arity 2" recs2
+    ]

test/src/Test/Mini.idr

@@ -61,19 +61,24 @@ run :  Foldable t
     -> t i
     -> Result i o
 run f = concatMap run'
-  where run' : i -> Result i o
-        run' inp = case f inp of
-                        (Left x)  => MkResult [] [x]
-                        (Right x) => MkResult [x] []
+
+  where
+    run' : i -> Result i o
+    run' inp = case f inp of
+      Left x  => MkResult [] [x]
+      Right x => MkResult [x] []
 
 public export
 runEq : (Foldable t, Eq o) => (f : i -> o) -> t (i,o) -> Result i o
 runEq f = concatMap run'
-  where run' : (i,o) -> Result i o
-        run' (inp,exp) = let res = f inp
-                          in if exp == res
-                                then MkResult [MkSuccess inp exp] []
-                                else MkResult [] [MkFailure inp res exp]
+
+  where
+    run' : (i,o) -> Result i o
+    run' (inp,exp) =
+      let res := f inp
+       in if exp == res
+            then MkResult [MkSuccess inp exp] []
+            else MkResult [] [MkFailure inp res exp]
 
 --------------------------------------------------------------------------------
 --          ANSI Colorings and Reporting
@@ -100,15 +105,19 @@ report : PrettyVal i => PrettyVal o => Result i o -> IO Bool
 report (MkResult ok [])      =
   putStrLn (greenOk ++ show (length ok) ++ " tests run") $> True
 
-report (MkResult ok (f::fs)) =
-  do putStrLn (redFailed ++ summary)
-     putStrLn "First failure"
-     dumpIO f
-     pure False
-  where summary : String
-        summary = unlines [ show (length ok + length fs + 1) ++ " tests run"
-                          , spaces ++ show (length fs + 1) ++ " tests failed"
-                          ]
+report (MkResult ok (f::fs)) = do
+  putStrLn (redFailed ++ summary)
+  putStrLn "First failure"
+  dumpIO f
+  pure False
+
+  where
+    summary : String
+    summary =
+      unlines
+        [ show (length ok + length fs + 1) ++ " tests run"
+        , spaces ++ show (length fs + 1) ++ " tests failed"
+        ]
 
 export
 testAll : List (IO Bool) -> IO Bool