diff --git a/Soda/se/umu/cs/soda/prototype/example/market/core/MyList.lean b/Soda/se/umu/cs/soda/prototype/example/market/core/MyList.lean index fd3897c..f199058 100644 --- a/Soda/se/umu/cs/soda/prototype/example/market/core/MyList.lean +++ b/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. -/ diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyList.soda b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyList.soda index 8bffe21..462cae8 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyList.soda +++ b/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. diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala index 2c47717..950c0ab 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala +++ b/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. diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyListSpec.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyListSpec.soda index 0f7ec43..5903ff4 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyListSpec.soda +++ b/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) diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala index 4e424da..a6ebc4c 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala +++ b/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)