Add 'range' function

Soda/se/umu/cs/soda/prototype/example/market/core/MyList.lean

@@ -65,6 +65,19 @@ def   foldl ( A : Type ) ( B : Type ) (list : List ( A ) ) (initial : B)
     _tailrec_foldl ( A ) ( B ) (list) (initial) (next)
 
 
+ private def   _tailrec_range (n : Nat) (list : List ( Nat ) ) : List ( Nat ) :=
+    match n with
+      | Succ_ (k) => _tailrec_range (k) ( (k) :: (list) )
+      | _otherwise => list
+
+
+
+ def   range (length : Nat) : List ( Nat ) :=
+    if (0 <= length)
+    then _tailrec_range (length) (List.nil)
+    else List.nil
+
+
 /-`length` defined using fold left.
  This uses foldl, which is tail recursive.
 -/

core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyList.soda

@@ -49,6 +49,16 @@ class MyList
       (next : B -> A -> B) : B =
     _tailrec_foldl [A] [B] (list) (initial) (next)
 
+  _tailrec_range (n : Nat) (list : List [Nat] ) : List [Nat] =
+    match n
+      case Succ_ (k) ==> _tailrec_range (k) ( (k) :: (list) )
+      case _otherwise ==> list
+
+  range (length : Nat) : List [Nat] =
+    if (0 <= length)
+    then _tailrec_range (length) (Nil)
+    else Nil
+
 /*
  * `length` defined using fold left.
  * This uses foldl, which is tail recursive.

core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala

@@ -273,6 +273,17 @@ trait MyList
       (next : B => A => B) : B =
     _tailrec_foldl [A, B] (list) (initial) (next)
 
+  private def _tailrec_range (n : Nat) (list : List [Nat] ) : List [Nat] =
+    n match  {
+      case Succ_ (k) => _tailrec_range (k) ( (k) :: (list) )
+      case _otherwise => list
+    }
+
+  def range (length : Nat) : List [Nat] =
+    if ( (0 <= length)
+    ) _tailrec_range (length) (Nil)
+    else Nil
+
 /*
  * `length` defined using fold left.
  * This uses foldl, which is tail recursive.

core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyListSpec.soda

@@ -7,10 +7,16 @@ class MyListSpec ()
     assert (obtained == expected)
 
   example_list_0 : List [Int] =
-     List (0 , 1 , 1 , 2 , 3 , 5 , 8)
+    List (0 , 1 , 1 , 2 , 3 , 5 , 8)
 
   example_list_1 : List [Int] =
-     List (13 , 21 , 34 , 55 , 89 , 144)
+    List (13 , 21 , 34 , 55 , 89 , 144)
+
+  short_list : List [Nat] =
+     instance .range (100)
+
+  long_list : List [Nat] =
+     instance .range (1000000)
 
   instance : MyList =
     MyList .mk (true)
@@ -31,6 +37,22 @@ class MyListSpec ()
     )
   )
 
+  test ("length_def - short list") (
+    check (
+      obtained := instance .length_def (short_list)
+    ) (
+      expected := 100
+    )
+  )
+
+  test ("length_tr - long list") (
+    check (
+      obtained := instance .length_tr (long_list)
+    ) (
+      expected := 1000000
+    )
+  )
+
   test ("concat") (
     check (
       obtained := instance .concat [Int] (example_list_0) (example_list_1)

core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala

@@ -129,10 +129,16 @@ case class MyListSpec ()
     assert (obtained == expected)
 
   lazy val example_list_0 : List [Int] =
-     List (0 , 1 , 1 , 2 , 3 , 5 , 8)
+    List (0 , 1 , 1 , 2 , 3 , 5 , 8)
 
   lazy val example_list_1 : List [Int] =
-     List (13 , 21 , 34 , 55 , 89 , 144)
+    List (13 , 21 , 34 , 55 , 89 , 144)
+
+  lazy val short_list : List [Nat] =
+     instance .range (100)
+
+  lazy val long_list : List [Nat] =
+     instance .range (1000000)
 
   lazy val instance : MyList =
     MyList .mk (true)
@@ -153,6 +159,22 @@ case class MyListSpec ()
     )
   )
 
+  test ("length_def - short list") (
+    check (
+      obtained = instance .length_def (short_list)
+    ) (
+      expected = 100
+    )
+  )
+
+  test ("length_tr - long list") (
+    check (
+      obtained = instance .length_tr (long_list)
+    ) (
+      expected = 1000000
+    )
+  )
+
   test ("concat") (
     check (
       obtained = instance .concat [Int] (example_list_0) (example_list_1)