Update examples

julianmendez · Feb 24, 2024 · 21d47fb · 21d47fb
1 parent 9023447
commit 21d47fb
Show file tree

Hide file tree

Showing 9 changed files with 450 additions and 20 deletions.
diff --git a/examples/src/main/scala/soda/example/mathematics/FiboAlternativeExample.soda b/examples/src/main/scala/soda/example/mathematics/FiboAlternativeExample.soda
@@ -0,0 +1,58 @@
+
+class NonNegativeMod
+
+  invariant (v : Int) : Boolean =
+    v >= 0
+
+  mko (v : Int) : Option [Int] =
+    if invariant (v)
+    then Some (v)
+    else None
+
+  _plus (v : Int) (b : Option [Int] ) : Option [Int] =
+    match b
+      case Some (w) ==> mko (v + w)
+      case None ==> None
+
+  plus (a : Option [Int] ) (b : Option [Int] ) : Option [Int] =
+    match a
+      case Some (v) ==> _plus (v) (b)
+      case None ==> None
+
+  _minus1 (v : Int) : Option [Int] =
+    if v > 0
+    then Option [Int] (v - 1)
+    else None
+
+  minus1 (a : Option [Int]) : Option [Int] =
+    match a
+      case Some (v) ==> _minus1 (v)
+      case None ==> None
+
+end
+
+
+class FiboAlternativeExampleInSoda
+
+  abstract
+
+  _mm = NonNegativeMod .mk
+
+  _zero = _mm .mko (0)
+
+  _one = _mm .mko (1)
+
+  _rec (m : Option [Int] ) (a : Option [Int] ) (b : Option [Int] ) : Option [Int] =
+    if m == _zero then a
+    else if m == _one then b
+    else _rec (_mm .minus1 (m) ) (b) (_mm .plus (a) (b) )
+
+  _apply (n : Option [Int] ) : Option [Int] =
+    _rec (n) (_zero) (_one)
+
+  apply (n : Int) : Int =
+    match _apply (_mm .mko (n) )
+      case Some (v) ==> v
+      case None ==> -1
+
+end
diff --git a/examples/src/main/scala/soda/example/mathematics/FiboExample.soda b/examples/src/main/scala/soda/example/mathematics/FiboExample.soda
@@ -1,14 +1,44 @@
 
+
+class NonNegative
+
+  abstract
+    v : Int
+
+  invariant : Boolean =
+    v >= 0
+
+  check : Option [NonNegative] =
+    if invariant
+    then Some (this)
+    else None
+
+end
+
+
 class FiboExampleInSoda
 
   abstract
 
-  _rec (m : Int) (a : Int) (b : Int) : Int =
-    if m == 0 then a
-    else if m == 1 then b
-    else _rec (m - 1) (b) (a + b)
+  _plus (a : NonNegative) (b : NonNegative) : NonNegative =
+    NonNegative .mk (a .v + b .v)
+
+ _monus1 (a : NonNegative) : NonNegative =
+   if a .v > 0
+   then NonNegative .mk (a .v - 1)
+   else a
+
+  _rec (m : NonNegative) (a : NonNegative) (b : NonNegative) : NonNegative =
+    if m .v == 0 then a
+    else if m .v == 1 then b
+    else _rec (_monus1 (m) ) (b) (_plus (a) (b) )
+
+  _apply (n : NonNegative) : NonNegative =
+    _rec (n) (NonNegative .mk (0) ) (NonNegative .mk (1) )
 
   apply (n : Int) : Int =
-    _rec (n) (0) (1)
+    match NonNegative .mk (n) .check
+      case Some (non_negative) ==> (_apply (non_negative) ) .v
+      case None ==> -1
 
 end
diff --git a/examples/src/main/scala/soda/example/mathematics/Package.scala b/examples/src/main/scala/soda/example/mathematics/Package.scala
@@ -102,18 +102,134 @@ object FactorialWithFold {
 }
 
 
+trait NonNegativeMod
+{
+
+  def invariant (v : Int) : Boolean =
+    v >= 0
+
+  def mko (v : Int) : Option [Int] =
+    if ( invariant (v)
+    ) Some (v)
+    else None
+
+  private def _plus (v : Int) (b : Option [Int] ) : Option [Int] =
+    b match  {
+      case Some (w) => mko (v + w)
+      case None => None
+    }
+
+  def plus (a : Option [Int] ) (b : Option [Int] ) : Option [Int] =
+    a match  {
+      case Some (v) => _plus (v) (b)
+      case None => None
+    }
+
+  private def _minus1 (v : Int) : Option [Int] =
+    if ( v > 0
+    ) Option [Int] (v - 1)
+    else None
+
+  def minus1 (a : Option [Int]) : Option [Int] =
+    a match  {
+      case Some (v) => _minus1 (v)
+      case None => None
+    }
+
+}
+
+case class NonNegativeMod_ () extends NonNegativeMod
+
+object NonNegativeMod {
+  def mk : NonNegativeMod =
+    NonNegativeMod_ ()
+}
+
+trait FiboAlternativeExampleInSoda
+{
+
+
+
+  private lazy val _mm = NonNegativeMod .mk
+
+  private lazy val _zero = _mm .mko (0)
+
+  private lazy val _one = _mm .mko (1)
+
+  private def _rec (m : Option [Int] ) (a : Option [Int] ) (b : Option [Int] ) : Option [Int] =
+    if ( m == _zero ) a
+    else if ( m == _one ) b
+    else _rec (_mm .minus1 (m) ) (b) (_mm .plus (a) (b) )
+
+  private def _apply (n : Option [Int] ) : Option [Int] =
+    _rec (n) (_zero) (_one)
+
+  def apply (n : Int) : Int =
+    _apply (_mm .mko (n) ) match  {
+      case Some (v) => v
+      case None => -1
+    }
+
+}
+
+case class FiboAlternativeExampleInSoda_ () extends FiboAlternativeExampleInSoda
+
+object FiboAlternativeExampleInSoda {
+  def mk : FiboAlternativeExampleInSoda =
+    FiboAlternativeExampleInSoda_ ()
+}
+
+
+
+
+trait NonNegative
+{
+
+  def   v : Int
+
+  lazy val invariant : Boolean =
+    v >= 0
+
+  lazy val check : Option [NonNegative] =
+    if ( invariant
+    ) Some (this)
+    else None
+
+}
+
+case class NonNegative_ (v : Int) extends NonNegative
+
+object NonNegative {
+  def mk (v : Int) : NonNegative =
+    NonNegative_ (v)
+}
+
 trait FiboExampleInSoda
 {
 
 
 
-  private def _rec (m : Int) (a : Int) (b : Int) : Int =
-    if ( m == 0 ) a
-    else if ( m == 1 ) b
-    else _rec (m - 1) (b) (a + b)
+  private def _plus (a : NonNegative) (b : NonNegative) : NonNegative =
+    NonNegative .mk (a .v + b .v)
+
+ private def _monus1 (a : NonNegative) : NonNegative =
+   if ( a .v > 0
+   ) NonNegative .mk (a .v - 1)
+   else a
+
+  private def _rec (m : NonNegative) (a : NonNegative) (b : NonNegative) : NonNegative =
+    if ( m .v == 0 ) a
+    else if ( m .v == 1 ) b
+    else _rec (_monus1 (m) ) (b) (_plus (a) (b) )
+
+  private def _apply (n : NonNegative) : NonNegative =
+    _rec (n) (NonNegative .mk (0) ) (NonNegative .mk (1) )
 
   def apply (n : Int) : Int =
-    _rec (n) (0) (1)
+    NonNegative .mk (n) .check match  {
+      case Some (non_negative) => (_apply (non_negative) ) .v
+      case None => -1
+    }
 
 }
 

diff --git a/examples/src/test/scala/soda/example/mathematics/FiboExampleSpec.soda b/examples/src/test/scala/soda/example/mathematics/FiboExampleSpec.soda
@@ -23,5 +23,17 @@ class FiboExampleSpec ()
     )
   )
 
+  _fibo_alternative_example_in_soda = FiboAlternativeExampleInSoda_ ()
+
+  test ("should test an alternative implementation of the fibonacci function") (
+    check (
+      obtained := fibonacci_values
+        .map (lambda pair --> pair ._1)
+        .map (lambda n --> Tuple2 (n , _fibo_alternative_example_in_soda .apply (n) ) )
+    ) (
+      expected := fibonacci_values
+    )
+  )
+
 end
 
diff --git a/examples/src/test/scala/soda/example/mathematics/Package.scala b/examples/src/test/scala/soda/example/mathematics/Package.scala
@@ -93,6 +93,18 @@ case class FiboExampleSpec ()
     )
   )
 
+  private lazy val _fibo_alternative_example_in_soda = FiboAlternativeExampleInSoda_ ()
+
+  test ("should test an alternative implementation of the fibonacci function") (
+    check (
+      obtained = fibonacci_values
+        .map ( pair => pair ._1)
+        .map ( n => Tuple2 (n , _fibo_alternative_example_in_soda .apply (n) ) )
+    ) (
+      expected = fibonacci_values
+    )
+  )
+
 }
 
 

diff --git a/...lator/src/test/resources/soda/translator/example/mathematics/FiboAlternativeExample.scala b/...lator/src/test/resources/soda/translator/example/mathematics/FiboAlternativeExample.scala
@@ -0,0 +1,76 @@
+trait NonNegativeMod
+{
+
+  def invariant (v : Int) : Boolean =
+    v >= 0
+
+  def mko (v : Int) : Option [Int] =
+    if ( invariant (v)
+    ) Some (v)
+    else None
+
+  private def _plus (v : Int) (b : Option [Int] ) : Option [Int] =
+    b match  {
+      case Some (w) => mko (v + w)
+      case None => None
+    }
+
+  def plus (a : Option [Int] ) (b : Option [Int] ) : Option [Int] =
+    a match  {
+      case Some (v) => _plus (v) (b)
+      case None => None
+    }
+
+  private def _minus1 (v : Int) : Option [Int] =
+    if ( v > 0
+    ) Option [Int] (v - 1)
+    else None
+
+  def minus1 (a : Option [Int]) : Option [Int] =
+    a match  {
+      case Some (v) => _minus1 (v)
+      case None => None
+    }
+
+}
+
+case class NonNegativeMod_ () extends NonNegativeMod
+
+object NonNegativeMod {
+  def mk : NonNegativeMod =
+    NonNegativeMod_ ()
+}
+
+trait FiboAlternativeExampleInSoda
+{
+
+
+
+  private lazy val _mm = NonNegativeMod .mk
+
+  private lazy val _zero = _mm .mko (0)
+
+  private lazy val _one = _mm .mko (1)
+
+  private def _rec (m : Option [Int] ) (a : Option [Int] ) (b : Option [Int] ) : Option [Int] =
+    if ( m == _zero ) a
+    else if ( m == _one ) b
+    else _rec (_mm .minus1 (m) ) (b) (_mm .plus (a) (b) )
+
+  private def _apply (n : Option [Int] ) : Option [Int] =
+    _rec (n) (_zero) (_one)
+
+  def apply (n : Int) : Int =
+    _apply (_mm .mko (n) ) match  {
+      case Some (v) => v
+      case None => -1
+    }
+
+}
+
+case class FiboAlternativeExampleInSoda_ () extends FiboAlternativeExampleInSoda
+
+object FiboAlternativeExampleInSoda {
+  def mk : FiboAlternativeExampleInSoda =
+    FiboAlternativeExampleInSoda_ ()
+}