Update examples

examples/src/main/scala/soda/example/forlean/algorithms/Package.scala

@@ -76,61 +76,51 @@ case class TripleIntStringIntMod_ () extends TripleIntStringIntMod
 /*
 directive lean
 notation:max "Nil" => List.nil
-*/
-
-/*
-directive lean
 notation:max "Boolean" => Bool
-*/
-
-/*
-directive lean
 notation:max "Zero_ ()" => Nat.zero
-*/
-
-/*
-directive lean
 notation:max "Succ_" => Nat.succ
 */
 
-/*
+/**
  * This class contains tail recursive auxiliary functions.
  */
 
 trait RecursionForLean
 {
 
-  private def _tailrec_fold4 [A , B ] (sequence : List [A] ) (current : B)
-      (next_value : B => A => B) (condition : B => A => Boolean) : B =
-    sequence match  {
+
+
+  private def _tailrec_fold4 [A , B ] (list : List [A] ) (current : B)
+      (next : B => A => B) (condition : B => A => Boolean) : B =
+    list match  {
+      case Nil => current
       case (head) :: (tail) =>
-         if ( (! (condition (current) (head) ) )
-         ) current
-         else
-           _tailrec_fold4 [A, B] (tail) (next_value (current) (head) ) (next_value) (condition)
-      case otherwise => current
+        if ( (! (condition (current) (head) ) )
+        ) current
+        else _tailrec_fold4 [A, B] (tail) (next (current) (head) ) (next) (condition)
     }
 
-  def fold4 [A , B ] (sequence : List [A] ) (initial_value : B)
-      (next_value : B => A => B) (condition : B => A => Boolean) : B =
-    _tailrec_fold4 [A, B] (sequence) (initial_value) (next_value) (condition)
+  def fold4 [A , B ] (list : List [A] ) (initial_value : B)
+      (next : B => A => B) (condition : B => A => Boolean) : B =
+    _tailrec_fold4 [A, B] (list) (initial_value) (next) (condition)
 
-  private def _tailrec_fold3 [A , B ] (sequence : List [A] ) (current : B)
-      (next_value : B => A => B) : B =
-    sequence match  {
+  private def _tailrec_fold3 [A , B ] (list : List [A] ) (current : B)
+      (next : B => A => B) : B =
+    list match  {
+      case Nil => current
       case (head) :: (tail) =>
-        _tailrec_fold3 [A, B] (tail) (next_value (current) (head) ) (next_value)
-      case otherwise => current
+        _tailrec_fold3 [A, B] (tail) (next (current) (head) ) (next)
     }
 
-  def fold3 [A , B ] (sequence : List [A] ) (initial_value : B)
-      (next_value : B => A => B) : B =
-    _tailrec_fold3 [A, B] (sequence) (initial_value) (next_value)
+  def fold3 [A , B ] (list : List [A] ) (initial_value : B)
+      (next : B => A => B) : B =
+    _tailrec_fold3 [A, B] (list) (initial_value) (next)
 
-  private def _tailrec_range (n : Nat) (sequence : List [Nat] ) : List [Nat] =
+  private def _tailrec_range (n : Nat) (list : List [Nat] ) : List [Nat] =
     n match  {
-      case Zero_ () => sequence
-      case Succ_ (k) => _tailrec_range (k) (k :: sequence)
+      case Zero_ () => list
+      case Succ_ (k) =>
+        _tailrec_range (k) ( (k) :: (list) )
     }
 
   def range (length : Nat) : List [Nat] =
@@ -141,45 +131,32 @@ trait RecursionForLean
 case class RecursionForLean_ () extends RecursionForLean
 
 
-/*
-directive coq
-Definition Nat : Type := nat .
-*/
-
 trait PairExample
 {
 
-  def   left : Nat
-  def   right : Nat
+  def   left : Int
+  def   right : Int
 
 }
 
-case class PairExample_ (left : Nat, right : Nat) extends PairExample
+case class PairExample_ (left : Int, right : Int) extends PairExample
 
 trait SwapExample
 {
 
+
+
   def swap (pair : PairExample) : PairExample =
     PairExample_ (pair .right, pair .left)
 
 /*
   directive lean
   theorem
-    swap_of_swap (x : Nat) (y : Nat) : (swap (swap (PairExample_ (x, y) ) ) ) = PairExample_ (x, y) :=
+    swap_of_swap (x : Int) (y : Int) : (swap (swap (PairExample_ (x, y) ) ) ) = PairExample_ (x, y) :=
       by
         constructor
 */
 
-/*
-  directive coq
-  Theorem
-    swap_of_swap : forall (x : nat) (y : nat) , (swap (swap (PairExample_ (x, y) ) ) ) =
-    PairExample_ (x, y) .
-  Proof.
-    auto.
-  Qed.
-*/
-
 }
 
 case class SwapExample_ () extends SwapExample

examples/src/main/scala/soda/example/forlean/algorithms/RecursionForLean.lean

@@ -1,51 +1,56 @@
 notation:max "Nil" => List.nil
-
 notation:max "Boolean" => Bool
-
 notation:max "Zero_ ()" => Nat.zero
-
 notation:max "Succ_" => Nat.succ
 
-/- This class contains tail recursive auxiliary functions.
+/-- This class contains tail recursive auxiliary functions.
 -/
 
+class RecursionForLean
+
+where
+  RecursionForLean_ ::
+
+  deriving DecidableEq
+
 namespace RecursionForLean
 
-def   _tailrec_fold4 ( A : Type ) ( B : Type ) (sequence : List ( A ) ) (current : B)
-       (next_value : B -> A -> B) (condition : B -> A -> Boolean) : B :=
-    match sequence with
+
+private def   _tailrec_fold4 ( A : Type ) ( B : Type ) (list : List ( A ) ) (current : B)
+       (next : B -> A -> B) (condition : B -> A -> Boolean) : B :=
+    match list with
+      | [] => current
       | (head) :: (tail) =>
-         if (not (condition (current) (head) ) )
-         then current
-         else
-           _tailrec_fold4 ( A ) ( B ) (tail) (next_value (current) (head) ) (next_value) (condition)
-      | otherwise => current
+        if (not (condition (current) (head) ) )
+        then current
+        else _tailrec_fold4 ( A ) ( B ) (tail) (next (current) (head) ) (next) (condition)
 
 
 
-def   fold4 ( A : Type ) ( B : Type ) (sequence : List ( A ) ) (initial_value : B)
-       (next_value : B -> A -> B) (condition : B -> A -> Boolean) : B :=
-    _tailrec_fold4 ( A ) ( B ) (sequence) (initial_value) (next_value) (condition)
+def   fold4 ( A : Type ) ( B : Type ) (list : List ( A ) ) (initial_value : B)
+       (next : B -> A -> B) (condition : B -> A -> Boolean) : B :=
+    _tailrec_fold4 ( A ) ( B ) (list) (initial_value) (next) (condition)
 
 
-def   _tailrec_fold3 ( A : Type ) ( B : Type ) (sequence : List ( A ) ) (current : B)
-       (next_value : B -> A -> B) : B :=
-    match sequence with
+private def   _tailrec_fold3 ( A : Type ) ( B : Type ) (list : List ( A ) ) (current : B)
+       (next : B -> A -> B) : B :=
+    match list with
+      | [] => current
       | (head) :: (tail) =>
-        _tailrec_fold3 ( A ) ( B ) (tail) (next_value (current) (head) ) (next_value)
-      | otherwise => current
+        _tailrec_fold3 ( A ) ( B ) (tail) (next (current) (head) ) (next)
 
 
 
-def   fold3 ( A : Type ) ( B : Type ) (sequence : List ( A ) ) (initial_value : B)
-       (next_value : B -> A -> B) : B :=
-    _tailrec_fold3 ( A ) ( B ) (sequence) (initial_value) (next_value)
+def   fold3 ( A : Type ) ( B : Type ) (list : List ( A ) ) (initial_value : B)
+       (next : B -> A -> B) : B :=
+    _tailrec_fold3 ( A ) ( B ) (list) (initial_value) (next)
 
 
- def   _tailrec_range (n : Nat) (sequence : List ( Nat ) ) : List ( Nat ) :=
+ private def   _tailrec_range (n : Nat) (list : List ( Nat ) ) : List ( Nat ) :=
     match n with
-      | Zero_ () => sequence
-      | Succ_ (k) => _tailrec_range (k) (k :: sequence)
+      | Zero_ () => list
+      | Succ_ (k) =>
+        _tailrec_range (k) ( (k) :: (list) )
 
 
 

examples/src/main/scala/soda/example/forlean/algorithms/RecursionForLean.soda

@@ -1,52 +1,48 @@
 
 directive lean
 notation:max "Nil" => List.nil
-
-directive lean
 notation:max "Boolean" => Bool
-
-directive lean
 notation:max "Zero_ ()" => Nat.zero
-
-directive lean
 notation:max "Succ_" => Nat.succ
 
 
-/*
+/**
  * This class contains tail recursive auxiliary functions.
  */
 
 class RecursionForLean
 
-  _tailrec_fold4 [A : Type] [B : Type] (sequence : List [A] ) (current : B)
-      (next_value : B -> A -> B) (condition : B -> A -> Boolean) : B =
-    match sequence
+  abstract
+
+  _tailrec_fold4 [A : Type] [B : Type] (list : List [A] ) (current : B)
+      (next : B -> A -> B) (condition : B -> A -> Boolean) : B =
+    match list
+      case Nil ==> current
       case (head) :: (tail) ==>
-         if (not (condition (current) (head) ) )
-         then current
-         else
-           _tailrec_fold4 [A] [B] (tail) (next_value (current) (head) ) (next_value) (condition)
-      case otherwise ==> current
-
-  fold4 [A : Type] [B : Type] (sequence : List [A] ) (initial_value : B)
-      (next_value : B -> A -> B) (condition : B -> A -> Boolean) : B =
-    _tailrec_fold4 [A] [B] (sequence) (initial_value) (next_value) (condition)
-
-  _tailrec_fold3 [A : Type] [B : Type] (sequence : List [A] ) (current : B)
-      (next_value : B -> A -> B) : B =
-    match sequence
+        if (not (condition (current) (head) ) )
+        then current
+        else _tailrec_fold4 [A] [B] (tail) (next (current) (head) ) (next) (condition)
+
+  fold4 [A : Type] [B : Type] (list : List [A] ) (initial_value : B)
+      (next : B -> A -> B) (condition : B -> A -> Boolean) : B =
+    _tailrec_fold4 [A] [B] (list) (initial_value) (next) (condition)
+
+  _tailrec_fold3 [A : Type] [B : Type] (list : List [A] ) (current : B)
+      (next : B -> A -> B) : B =
+    match list
+      case Nil ==> current
       case (head) :: (tail) ==>
-        _tailrec_fold3 [A] [B] (tail) (next_value (current) (head) ) (next_value)
-      case otherwise ==> current
+        _tailrec_fold3 [A] [B] (tail) (next (current) (head) ) (next)
 
-  fold3 [A : Type] [B : Type] (sequence : List [A] ) (initial_value : B)
-      (next_value : B -> A -> B) : B =
-    _tailrec_fold3 [A] [B] (sequence) (initial_value) (next_value)
+  fold3 [A : Type] [B : Type] (list : List [A] ) (initial_value : B)
+      (next : B -> A -> B) : B =
+    _tailrec_fold3 [A] [B] (list) (initial_value) (next)
 
-  _tailrec_range (n : Nat) (sequence : List [Nat] ) : List [Nat] =
+  _tailrec_range (n : Nat) (list : List [Nat] ) : List [Nat] =
     match n
-      case Zero_ () ==> sequence
-      case Succ_ (k) ==> _tailrec_range (k) (k :: sequence)
+      case Zero_ () ==> list
+      case Succ_ (k) ==>
+        _tailrec_range (k) ( (k) :: (list) )
 
   range (length : Nat) : List [Nat] =
     _tailrec_range (length) (Nil)

examples/src/main/scala/soda/example/forlean/algorithms/SwapExample.lean

@@ -1,14 +1,9 @@
-/-
-directive coq
-Definition Nat : Type := nat.
--/
+class PairExample
 
-namespace PairExample
-
-class PairExample where
+where
   PairExample_ ::
-    left : Nat
-    right : Nat
+    left : Int
+    right : Int
   deriving DecidableEq
 
 namespace PairExample
@@ -18,27 +13,25 @@ end PairExample
 
 open PairExample
 
+class SwapExample
+
+where
+  SwapExample_ ::
+
+  deriving DecidableEq
+
 namespace SwapExample
 
+
  def   swap (pair : PairExample) : PairExample :=
     PairExample_ (pair.right) (pair.left)
 
 
   theorem
-    swap_of_swap (x : Nat) (y : Nat) : (swap (swap (PairExample_ (x) (y) ) ) ) = PairExample_ (x) (y) :=
+    swap_of_swap (x : Int) (y : Int) : (swap (swap (PairExample_ (x) (y) ) ) ) = PairExample_ (x) (y) :=
       by
         constructor
 
-/-
-  directive coq
-  Theorem
-    swap_of_swap : forall (x : nat) (y : nat) , (swap (swap (PairExample_ (x) (y) ) ) ) =
-    PairExample_ (x) (y).
-  Proof.
-    auto.
-  Qed.
--/
-
 end SwapExample
 
 open SwapExample

examples/src/main/scala/soda/example/forlean/algorithms/SwapExample.soda

@@ -1,33 +1,24 @@
 
-directive coq
-Definition Nat : Type := nat .
-
 class PairExample
 
   abstract
-    left : Nat
-    right : Nat
+    left : Int
+    right : Int
 
 end
 
 class SwapExample
 
+  abstract
+
   swap (pair : PairExample) : PairExample =
     PairExample_ (pair .right) (pair .left)
 
   directive lean
   theorem
-    swap_of_swap (x : Nat) (y : Nat) : (swap (swap (PairExample_ (x) (y) ) ) ) = PairExample_ (x) (y) :=
+    swap_of_swap (x : Int) (y : Int) : (swap (swap (PairExample_ (x) (y) ) ) ) = PairExample_ (x) (y) :=
       by
         constructor
 
-  directive coq
-  Theorem
-    swap_of_swap : forall (x : nat) (y : nat) , (swap (swap (PairExample_ (x) (y) ) ) ) =
-    PairExample_ (x) (y) .
-  Proof.
-    auto.
-  Qed.
-
 end