Add tests for Nat ranges and fix bad range [1,2..1] behaviour. (#1794)

Co-authored-by: Marcin Pastudzki <[email protected]>

Author: Sventimir

libs/prelude/Prelude/Types.idr

@@ -820,7 +820,7 @@ Range Nat where
     EQ => pure x
     GT => assert_total $ takeUntil (<= y) (countFrom x (\n => minus n 1))
   rangeFromThenTo x y z = case compare x y of
-    LT => if z > x
+    LT => if z >= x
              then assert_total $ takeBefore (> z) (countFrom x (plus (minus y x)))
              else Nil
     EQ => if x == z then pure x else Nil

tests/prelude/nat001/expected

@@ -0,0 +1 @@
+1/1: Building nats (nats.idr)

tests/prelude/nat001/nats.idr

@@ -0,0 +1,36 @@
+nats : List Nat -> List Nat
+nats = the (List Nat)
+
+singletonRange : nats [1..1] = nats [1]
+singletonRange = Refl
+
+basicIncreasingRange : nats [1..3] = nats [1, 2 , 3]
+basicIncreasingRange = Refl
+
+basicDecreasingRange : nats [3..1] = nats [3, 2, 1]
+basicDecreasingRange = Refl
+
+
+increasingRangeWithStep : nats [3, 5..11] = nats [3, 5, 7, 9, 11]
+increasingRangeWithStep = Refl
+
+increaingRangeWithStepEmpty : nats [3, 5..1] = nats []
+increaingRangeWithStepEmpty = Refl
+
+singletonRangeWithStep : nats [3, 4..3] = nats [3]
+singletonRangeWithStep = Refl
+
+zeroStepEmptyList : nats [3, 3..5] = nats []
+zeroStepEmptyList = Refl
+
+zeroStepWhenBoundEqual : nats [1, 1..1] = nats [1]
+zeroStepWhenBoundEqual = Refl
+
+decreasingRangeWithStep : nats [11, 8..1] = nats [11, 8, 5, 2]
+decreasingRangeWithStep = Refl
+
+decreasingRangeWithStepEmpty : nats [9, 8..10] = nats []
+decreasingRangeWithStepEmpty = Refl
+
+decreasingSingletonRangeWithStep : nats [9, 8..9] = nats [9]
+decreasingSingletonRangeWithStep = Refl

tests/prelude/nat001/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --check nats.idr