Use assertTrue / assertFalse (exercism#105)

[no important files changed]

Author: keiravillekode

exercises/practice/armstrong-numbers/ArmstrongNumbersTest.lean

@@ -6,27 +6,27 @@ open LeanTest
 def armstrongNumbersTests : TestSuite :=
   (TestSuite.empty "ArmstrongNumbers")
   |>.addTest "Zero is an Armstrong number" (do
-      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 0))
+      return assertTrue (ArmstrongNumbers.isArmstrongNumber 0))
   |>.addTest "Single-digit numbers are Armstrong numbers" (do
-      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 5))
+      return assertTrue (ArmstrongNumbers.isArmstrongNumber 5))
   |>.addTest "There are no two-digit Armstrong numbers" (do
-      return assertEqual false (ArmstrongNumbers.isArmstrongNumber 10))
+      return assertFalse (ArmstrongNumbers.isArmstrongNumber 10))
   |>.addTest "Three-digit number that is an Armstrong number" (do
-      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 153))
+      return assertTrue (ArmstrongNumbers.isArmstrongNumber 153))
   |>.addTest "Three-digit number that is not an Armstrong number" (do
-      return assertEqual false (ArmstrongNumbers.isArmstrongNumber 100))
+      return assertFalse (ArmstrongNumbers.isArmstrongNumber 100))
   |>.addTest "Four-digit number that is an Armstrong number" (do
-      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 9474))
+      return assertTrue (ArmstrongNumbers.isArmstrongNumber 9474))
   |>.addTest "Four-digit number that is not an Armstrong number" (do
-      return assertEqual false (ArmstrongNumbers.isArmstrongNumber 9475))
+      return assertFalse (ArmstrongNumbers.isArmstrongNumber 9475))
   |>.addTest "Seven-digit number that is an Armstrong number" (do
-      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 9926315))
+      return assertTrue (ArmstrongNumbers.isArmstrongNumber 9926315))
   |>.addTest "Seven-digit number that is not an Armstrong number" (do
-      return assertEqual false (ArmstrongNumbers.isArmstrongNumber 9926314))
+      return assertFalse (ArmstrongNumbers.isArmstrongNumber 9926314))
   |>.addTest "Armstrong number containing seven zeroes" (do
-      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 186709961001538790100634132976990))
+      return assertTrue (ArmstrongNumbers.isArmstrongNumber 186709961001538790100634132976990))
   |>.addTest "The largest and last Armstrong number" (do
-      return assertEqual true (ArmstrongNumbers.isArmstrongNumber 115132219018763992565095597973971522401))
+      return assertTrue (ArmstrongNumbers.isArmstrongNumber 115132219018763992565095597973971522401))
 
 def main : IO UInt32 := do
   runTestSuitesWithExitCode [armstrongNumbersTests]

exercises/practice/leap/LeapTest.lean

@@ -6,23 +6,23 @@ open LeanTest
 def leapTests : TestSuite :=
   (TestSuite.empty "Leap")
   |>.addTest "year not divisible by 4 in common year" (do
-      return assertEqual false (Leap.leapYear 2015))
+      return assertFalse (Leap.leapYear 2015))
   |>.addTest "year divisible by 2, not divisible by 4 in common year" (do
-      return assertEqual false (Leap.leapYear 1970))
+      return assertFalse (Leap.leapYear 1970))
   |>.addTest "year divisible by 4, not divisible by 100 in leap year" (do
-      return assertEqual true (Leap.leapYear 1996))
+      return assertTrue (Leap.leapYear 1996))
   |>.addTest "year divisible by 4 and 5 is still a leap year" (do
-      return assertEqual true (Leap.leapYear 1960))
+      return assertTrue (Leap.leapYear 1960))
   |>.addTest "year divisible by 100, not divisible by 400 in common year" (do
-      return assertEqual false (Leap.leapYear 2100))
+      return assertFalse (Leap.leapYear 2100))
   |>.addTest "year divisible by 100 but not by 3 is still not a leap year" (do
-      return assertEqual false (Leap.leapYear 1900))
+      return assertFalse (Leap.leapYear 1900))
   |>.addTest "year divisible by 400 is leap year" (do
-      return assertEqual true (Leap.leapYear 2000))
+      return assertTrue (Leap.leapYear 2000))
   |>.addTest "year divisible by 400 but not by 125 is still a leap year" (do
-      return assertEqual true (Leap.leapYear 2400))
+      return assertTrue (Leap.leapYear 2400))
   |>.addTest "year divisible by 200, not divisible by 400 in common year" (do
-      return assertEqual false (Leap.leapYear 1800))
+      return assertFalse (Leap.leapYear 1800))
 
   def main : IO UInt32 := do
     runTestSuitesWithExitCode [leapTests]

exercises/practice/triangle/TriangleTest.lean

@@ -6,47 +6,47 @@ open LeanTest
 def triangleTests : TestSuite :=
   (TestSuite.empty "Triangle")
   |>.addTest "equilateral triangle -> all sides are equal" (do
-      return assertEqual true (Triangle.equilateral [2, 2, 2]))
+      return assertTrue (Triangle.equilateral [2, 2, 2]))
   |>.addTest "equilateral triangle -> any side is unequal" (do
-      return assertEqual false (Triangle.equilateral [2, 3, 2]))
+      return assertFalse (Triangle.equilateral [2, 3, 2]))
   |>.addTest "equilateral triangle -> no sides are equal" (do
-      return assertEqual false (Triangle.equilateral [5, 4, 6]))
+      return assertFalse (Triangle.equilateral [5, 4, 6]))
   |>.addTest "equilateral triangle -> all zero sides is not a triangle" (do
-      return assertEqual false (Triangle.equilateral [0, 0, 0]))
+      return assertFalse (Triangle.equilateral [0, 0, 0]))
   |>.addTest "equilateral triangle -> sides may be floats" (do
-      return assertEqual true (Triangle.equilateral [0.5, 0.5, 0.5]))
+      return assertTrue (Triangle.equilateral [0.5, 0.5, 0.5]))
   |>.addTest "isosceles triangle -> last two sides are equal" (do
-      return assertEqual true (Triangle.isosceles [3, 4, 4]))
+      return assertTrue (Triangle.isosceles [3, 4, 4]))
   |>.addTest "isosceles triangle -> first two sides are equal" (do
-      return assertEqual true (Triangle.isosceles [4, 4, 3]))
+      return assertTrue (Triangle.isosceles [4, 4, 3]))
   |>.addTest "isosceles triangle -> first and last sides are equal" (do
-      return assertEqual true (Triangle.isosceles [4, 3, 4]))
+      return assertTrue (Triangle.isosceles [4, 3, 4]))
   |>.addTest "isosceles triangle -> equilateral triangles are also isosceles" (do
-      return assertEqual true (Triangle.isosceles [4, 4, 4]))
+      return assertTrue (Triangle.isosceles [4, 4, 4]))
   |>.addTest "isosceles triangle -> no sides are equal" (do
-      return assertEqual false (Triangle.isosceles [2, 3, 4]))
+      return assertFalse (Triangle.isosceles [2, 3, 4]))
   |>.addTest "isosceles triangle -> first triangle inequality violation" (do
-      return assertEqual false (Triangle.isosceles [1, 1, 3]))
+      return assertFalse (Triangle.isosceles [1, 1, 3]))
   |>.addTest "isosceles triangle -> second triangle inequality violation" (do
-      return assertEqual false (Triangle.isosceles [1, 3, 1]))
+      return assertFalse (Triangle.isosceles [1, 3, 1]))
   |>.addTest "isosceles triangle -> third triangle inequality violation" (do
-      return assertEqual false (Triangle.isosceles [3, 1, 1]))
+      return assertFalse (Triangle.isosceles [3, 1, 1]))
   |>.addTest "isosceles triangle -> sides may be floats" (do
-      return assertEqual true (Triangle.isosceles [0.5, 0.4, 0.5]))
+      return assertTrue (Triangle.isosceles [0.5, 0.4, 0.5]))
   |>.addTest "scalene triangle -> no sides are equal" (do
-      return assertEqual true (Triangle.scalene [5, 4, 6]))
+      return assertTrue (Triangle.scalene [5, 4, 6]))
   |>.addTest "scalene triangle -> all sides are equal" (do
-      return assertEqual false (Triangle.scalene [4, 4, 4]))
+      return assertFalse (Triangle.scalene [4, 4, 4]))
   |>.addTest "scalene triangle -> first and second sides are equal" (do
-      return assertEqual false (Triangle.scalene [4, 4, 3]))
+      return assertFalse (Triangle.scalene [4, 4, 3]))
   |>.addTest "scalene triangle -> first and third sides are equal" (do
-      return assertEqual false (Triangle.scalene [3, 4, 3]))
+      return assertFalse (Triangle.scalene [3, 4, 3]))
   |>.addTest "scalene triangle -> second and third sides are equal" (do
-      return assertEqual false (Triangle.scalene [4, 3, 3]))
+      return assertFalse (Triangle.scalene [4, 3, 3]))
   |>.addTest "scalene triangle -> may not violate triangle inequality" (do
-      return assertEqual false (Triangle.scalene [7, 3, 2]))
+      return assertFalse (Triangle.scalene [7, 3, 2]))
   |>.addTest "scalene triangle -> sides may be floats" (do
-      return assertEqual true (Triangle.scalene [0.5, 0.4, 0.6]))
+      return assertTrue (Triangle.scalene [0.5, 0.4, 0.6]))
 
   def main : IO UInt32 := do
     runTestSuitesWithExitCode [triangleTests]

generators/Generator/Generator/ArmstrongNumbersGenerator.lean

@@ -18,14 +18,17 @@ def {exercise.decapitalize}Tests : TestSuite :=
 
 def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
   let input := case.get! "input"
-  let expected := case.get! "expected"
+  let expected := case.get! "expected" |>.getBool? |> getOk
   let description := case.get! "description"
               |> (·.compress)
   let funName := getFunName (case.get! "property")
   let call := s!"({exercise}.{funName} {insertAllInputs input})"
+  let assert := match expected with
+                | true => s!"assertTrue {call}"
+                | false => s!"assertFalse {call}"
   s!"
   |>.addTest {description} (do
-      return assertEqual {expected} {call})"
+      return {assert})"
 
 def genEnd (exercise : String) : String :=
   s!"

generators/Generator/Generator/LeapGenerator.lean

@@ -1,8 +1,10 @@
 import Lean.Data.Json
 import Std
+import Helper
 
 open Lean
 open Std
+open Helper
 
 namespace LeapGenerator
 
@@ -18,15 +20,19 @@ def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
   let description := case.get! "description"
               |> (·.compress)
   let year := case.get! "input" |> (·.getObjVal? "year") |> Except.toOption |> Option.get!
-  let expected := case.get! "expected"
+  let expected := case.get! "expected" |>.getBool? |> getOk
   let funName := case.get! "property"
               |> (·.compress)
               |> String.toList
               |> (·.filter (·!='"'))
               |> List.asString
+  let call := s!"({exercise}.{funName} {year})"
+  let assert := match expected with
+                | true => s!"assertTrue {call}"
+                | false => s!"assertFalse {call}"
   s!"
   |>.addTest {description} (do
-      return assertEqual {expected} ({exercise}.{funName} {year}))"
+      return {assert})"
 
 def genEnd (exercise : String) : String :=
   s!"

generators/Generator/Generator/TriangleGenerator.lean

@@ -1,8 +1,10 @@
 import Lean.Data.Json
 import Std
+import Helper
 
 open Lean
 open Std
+open Helper
 
 namespace TriangleGenerator
 
@@ -18,15 +20,19 @@ def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
   let description := case.get! "description"
               |> (·.compress)
   let sides := case.get! "input" |> (·.getObjVal? "sides") |> Except.toOption |> Option.get!
-  let expected := case.get! "expected"
+  let expected := case.get! "expected" |>.getBool? |> getOk
   let funName := case.get! "property"
               |> (·.compress)
               |> String.toList
               |> (·.filter (·!='"'))
               |> List.asString
+  let call := s!"({exercise}.{funName} {sides})"
+  let assert := match expected with
+                | true => s!"assertTrue {call}"
+                | false => s!"assertFalse {call}"
   s!"
   |>.addTest {description} (do
-      return assertEqual {expected} ({exercise}.{funName} {sides}))"
+      return {assert})"
 
 def genEnd (exercise : String) : String :=
   s!"