From c7b08a25c0e1f7a30f6da332c0fa35adef1e03be Mon Sep 17 00:00:00 2001 From: stefan-hoeck Date: Mon, 21 Aug 2023 21:21:44 +0200 Subject: [PATCH] [ style ] adhere to coding style guide --- src/Text/Show/Diff.idr | 60 ++++++++++++++++------------- src/Text/Show/PrettyVal.idr | 4 +- src/Text/Show/PrettyVal/Derive.idr | 7 +++- test/src/Main.idr | 7 +--- test/src/PP.idr | 62 +++++++++++++++--------------- test/src/Parser.idr | 50 ++++++++++++------------ test/src/Test/Mini.idr | 45 +++++++++++++--------- 7 files changed, 128 insertions(+), 107 deletions(-) diff --git a/src/Text/Show/Diff.idr b/src/Text/Show/Diff.idr index d604ab9..4443af5 100644 --- a/src/Text/Show/Diff.idr +++ b/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 diff --git a/src/Text/Show/PrettyVal.idr b/src/Text/Show/PrettyVal.idr index 6a8a533..bd14234 100644 --- a/src/Text/Show/PrettyVal.idr +++ b/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 [] diff --git a/src/Text/Show/PrettyVal/Derive.idr b/src/Text/Show/PrettyVal/Derive.idr index 187120e..fd4c339 100644 --- a/src/Text/Show/PrettyVal/Derive.idr +++ b/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 diff --git a/test/src/Main.idr b/test/src/Main.idr index d3681a5..0132550 100644 --- a/test/src/Main.idr +++ b/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 diff --git a/test/src/PP.idr b/test/src/PP.idr index 558bd47..55756ed 100644 --- a/test/src/PP.idr +++ b/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)" + ] + ] diff --git a/test/src/Parser.idr b/test/src/Parser.idr index 4ba9b40..fd9b7b9 100644 --- a/test/src/Parser.idr +++ b/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 + ] diff --git a/test/src/Test/Mini.idr b/test/src/Test/Mini.idr index 464c864..d9e7d6c 100644 --- a/test/src/Test/Mini.idr +++ b/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