Add test cases for serializer

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

@@ -50,6 +50,7 @@ namespace MarketMod
   notation "_mm.get" => MyList.get
   notation "_mm.set" => MyList.set
   notation "_mm.foldl" => MyList.foldl
+  notation "_mm.append" => MyList.append
 
  def   as_market (market : Market) : Market :=
     Market.mk (market.accounts) (market.items)
@@ -82,7 +83,7 @@ private def   _deposit_into_known_account (accounts : List ( Money ) ) (user_id
 private def   _deposit_into_accounts (accounts : List ( Money ) ) (user_id : Nat) (amount : Money)
        : List ( Money ) :=
     if user_id == accounts.length
-    then amount :: accounts
+    then _mm.append ( Money ) (accounts) (amount)
     else _deposit_into_known_account (accounts) (user_id) (amount)
 
 
@@ -104,7 +105,7 @@ private def   _reassign_item (items : List ( Item ) ) (item_id : Nat) (user_id:
 private def   _assign_to_user (items : List ( Item ) ) (item_id : Nat) (user_id: Nat)
        : List ( Item ) :=
     if item_id == items.length
-    then Item.mk (user_id) (0) :: items
+    then _mm.append ( Item ) (items) (Item.mk (user_id) (0) )
     else _reassign_item (items) (item_id) (user_id)
 
 

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

@@ -284,6 +284,10 @@ def   foldl ( A : Type ) ( B : Type ) (list : List ( A ) ) (initial : B)
     )
 
 
+ def   append ( A : Type ) (first : List ( A ) ) (element : A) : List ( A ) :=
+    reverse_fl ( A )  (element :: reverse_fl ( A ) (first) )
+
+
  def   monus1 (index : Nat) : Nat :=
     match index with
       | Succ_ (k) => k

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

@@ -36,6 +36,7 @@ class MarketMod
   notation "_mm.get" => MyList.get
   notation "_mm.set" => MyList.set
   notation "_mm.foldl" => MyList.foldl
+  notation "_mm.append" => MyList.append
 
   as_market (market : Market) : Market =
     Market.mk (market .accounts) (market .items)
@@ -64,7 +65,7 @@ class MarketMod
   _deposit_into_accounts (accounts : List [Money] ) (user_id : Nat) (amount : Money)
       : List [Money] =
     if user_id == accounts .length
-    then amount :: accounts
+    then _mm .append [Money] (accounts) (amount)
     else _deposit_into_known_account (accounts) (user_id) (amount)
 
   deposit (m : Market) (user_id : Nat) (amount : Money) : Market =
@@ -82,7 +83,7 @@ class MarketMod
   _assign_to_user (items : List [Item] ) (item_id : Nat) (user_id: Nat)
       : List [Item] =
     if item_id == items .length
-    then Item .mk (user_id) (0) :: items
+    then _mm .append [Item] (items) (Item .mk (user_id) (0) )
     else _reassign_item (items) (item_id) (user_id)
 
   assign (m : Market) (item_id : Nat) (user_id : Nat) : Market =

core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/OperationProcessor.soda → core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketBuilder.soda

@@ -1,3 +1,4 @@
+
 class OperationProcessor
 
   abstract
@@ -12,3 +13,18 @@ class OperationProcessor
 
 end
 
+
+class MarketBuilder
+
+  abstract
+
+  operation_processor = OperationProcessor .mk
+
+  empty_market = Market .mk (List [Money] () ) (List [Item] () )
+
+  build (operations : List [Operation] ) : Option [Market] =
+    operation_processor
+      .process (Some (empty_market) ) (operations)
+
+end
+

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

@@ -169,7 +169,6 @@ class MyList
   reverse_tr [A : Type] (list : List [A] ) : List [A] =
     _tailrec_reverse [A] (list) (Nil)
 
-
   reverse_fl [A : Type] (list : List [A] ) : List [A] =
     _tailrec_foldl [A] [List [A] ] (list) (Nil) (
       lambda (accum : List [A] ) -->
@@ -260,6 +259,9 @@ class MyList
           (elem) :: (accum)
     )
 
+  append [A : Type] (first : List [A] ) (element : A) : List [A] =
+    reverse_fl [A]  (element :: reverse_fl [A] (first) )
+
   monus1 (index : Nat) : Nat =
     match index
       case Succ_ (k) ==> k

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

@@ -74,6 +74,7 @@ trait MarketMod
   notation "_mm.get" => MyList.get
   notation "_mm.set" => MyList.set
   notation "_mm.foldl" => MyList.foldl
+  notation "_mm.append" => MyList.append
 */
 
   def as_market (market : Market) : Market =
@@ -107,7 +108,7 @@ trait MarketMod
   private def _deposit_into_accounts (accounts : List [Money] ) (user_id : Nat) (amount : Money)
       : List [Money] =
     if ( user_id == accounts .length
-    ) amount :: accounts
+    ) _mm .append [Money] (accounts) (amount)
     else _deposit_into_known_account (accounts) (user_id) (amount)
 
   def deposit (m : Market) (user_id : Nat) (amount : Money) : Market =
@@ -126,7 +127,7 @@ trait MarketMod
   private def _assign_to_user (items : List [Item] ) (item_id : Nat) (user_id: Nat)
       : List [Item] =
     if ( item_id == items .length
-    ) Item .mk (user_id) (0) :: items
+    ) _mm .append [Item] (items) (Item .mk (user_id) (0) )
     else _reassign_item (items) (item_id) (user_id)
 
   def assign (m : Market) (item_id : Nat) (user_id : Nat) : Market =
@@ -208,6 +209,51 @@ object MarketMod {
 }
 
 
+trait OperationProcessor
+{
+
+
+
+  private lazy val _mm : MyList = MyList .mk (true)
+
+  def compute_next (maybe_market : Option [Market] ) (op : Operation) : Option [Market] =
+    op .process (maybe_market)
+
+  def process (maybe_market : Option [Market] ) (operations : List [Operation] ) : Option [Market] =
+    _mm .foldl [Operation, Option [Market] ] (operations) (maybe_market) (compute_next)
+
+}
+
+case class OperationProcessor_ () extends OperationProcessor
+
+object OperationProcessor {
+  def mk : OperationProcessor =
+    OperationProcessor_ ()
+}
+
+trait MarketBuilder
+{
+
+
+
+  lazy val operation_processor = OperationProcessor .mk
+
+  lazy val empty_market = Market .mk (List [Money] () ) (List [Item] () )
+
+  def build (operations : List [Operation] ) : Option [Market] =
+    operation_processor
+      .process (Some (empty_market) ) (operations)
+
+}
+
+case class MarketBuilder_ () extends MarketBuilder
+
+object MarketBuilder {
+  def mk : MarketBuilder =
+    MarketBuilder_ ()
+}
+
+
 
 
 /*
@@ -502,6 +548,9 @@ trait MyList
           (elem) :: (accum)
     )
 
+  def append [A ] (first : List [A] ) (element : A) : List [A] =
+    reverse_fl [A]  (element :: reverse_fl [A] (first) )
+
   def monus1 (index : Nat) : Nat =
     index match  {
       case Succ_ (k) => k
@@ -839,26 +888,3 @@ object OpSell {
     OpSell_ (item_id, user_id)
 }
 
-
-trait OperationProcessor
-{
-
-
-
-  private lazy val _mm : MyList = MyList .mk (true)
-
-  def compute_next (maybe_market : Option [Market] ) (op : Operation) : Option [Market] =
-    op .process (maybe_market)
-
-  def process (maybe_market : Option [Market] ) (operations : List [Operation] ) : Option [Market] =
-    _mm .foldl [Operation, Option [Market] ] (operations) (maybe_market) (compute_next)
-
-}
-
-case class OperationProcessor_ () extends OperationProcessor
-
-object OperationProcessor {
-  def mk : OperationProcessor =
-    OperationProcessor_ ()
-}
-

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

@@ -10,7 +10,9 @@ class Main
   read_file (file_name : String) : String =
     @new String (Files .readAllBytes (Paths .get (file_name) ) )
 
-  empty_market = Market .mk (List [Money] () ) (List [Item] () )
+  market_builder = MarketBuilder .mk
+
+  empty_market = market_builder .empty_market
 
   yaml_parser = YamlParser .mk
 
@@ -21,8 +23,8 @@ class Main
   operation_processor = OperationProcessor .mk
 
   process_file (file_name : String) : Option [Market] =
-    operation_processor
-      .process (Some (empty_market) ) (
+    market_builder
+      .build (
          operation_parser .parse (
            yaml_parser .parse ( @new StringReader (read_file (file_name) ) )
          )

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

@@ -12,6 +12,7 @@ import   soda.se.umu.cs.soda.prototype.example.market.core.Item
 import   soda.se.umu.cs.soda.prototype.example.market.core.Market
 import   soda.se.umu.cs.soda.prototype.example.market.core.Money
 import   soda.se.umu.cs.soda.prototype.example.market.core.OperationProcessor
+import   soda.se.umu.cs.soda.prototype.example.market.core.MarketBuilder
 import   soda.se.umu.cs.soda.prototype.example.market.parser.OperationParser
 import   soda.se.umu.cs.soda.prototype.example.market.parser.YamlParser
 import   soda.se.umu.cs.soda.prototype.example.market.serializer.YamlSerializer
@@ -28,7 +29,9 @@ trait Main
   def read_file (file_name : String) : String =
     new String (Files .readAllBytes (Paths .get (file_name) ) )
 
-  lazy val empty_market = Market .mk (List [Money] () ) (List [Item] () )
+  lazy val market_builder = MarketBuilder .mk
+
+  lazy val empty_market = market_builder .empty_market
 
   lazy val yaml_parser = YamlParser .mk
 
@@ -39,8 +42,8 @@ trait Main
   lazy val operation_processor = OperationProcessor .mk
 
   def process_file (file_name : String) : Option [Market] =
-    operation_processor
-      .process (Some (empty_market) ) (
+    market_builder
+      .build (
          operation_parser .parse (
            yaml_parser .parse ( new StringReader (read_file (file_name) ) )
          )

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

@@ -13,6 +13,7 @@ import
   soda.se.umu.cs.soda.prototype.example.market.core.Market
   soda.se.umu.cs.soda.prototype.example.market.core.Money
   soda.se.umu.cs.soda.prototype.example.market.core.OperationProcessor
+  soda.se.umu.cs.soda.prototype.example.market.core.MarketBuilder
   soda.se.umu.cs.soda.prototype.example.market.parser.OperationParser
   soda.se.umu.cs.soda.prototype.example.market.parser.YamlParser
   soda.se.umu.cs.soda.prototype.example.market.serializer.YamlSerializer

core/src/test/resources/example/example1.yaml

@@ -0,0 +1,89 @@
+---
+operations:
+- deposit 0 4500
+- deposit 1 75
+- deposit 2 1800
+- deposit 3 2000
+- deposit 4 5700
+- deposit 5 2500
+- deposit 6 1900
+- deposit 7 2200
+- deposit 8 6600
+- deposit 9 2400
+- deposit 10 1750
+- deposit 11 2150
+- deposit 12 1850
+- deposit 13 2350
+- deposit 14 1950
+- deposit 15 2100
+- deposit 16 1650
+- deposit 17 2450
+- deposit 18 7950
+- deposit 19 2250
+- deposit 20 1700
+- deposit 21 2300
+- deposit 22 1800
+- deposit 23 2400
+- deposit 24 1750
+- deposit 25 2350
+- assign 0 12
+- price 0 40
+- assign 1 7
+- price 1 50
+- assign 2 20
+- price 2 25
+- assign 3 15
+- price 3 70
+- assign 4 8
+- price 4 100
+- assign 5 23
+- price 5 60
+- assign 6 14
+- price 6 30
+- assign 7 2
+- price 7 40
+- assign 8 19
+- price 8 25
+- assign 9 5
+- price 9 20
+- assign 10 22
+- price 10 90
+- assign 11 13
+- price 11 50
+- assign 12 4
+- price 12 100
+- assign 13 18
+- price 13 150
+- assign 14 9
+- price 14 30
+- assign 15 24
+- price 15 30
+- assign 16 11
+- price 16 25
+- assign 17 3
+- price 17 200
+- assign 18 17
+- price 18 20
+- assign 19 10
+- price 19 30
+- assign 20 21
+- price 20 20
+- assign 21 16
+- price 21 100
+- assign 22 1
+- price 22 100
+- assign 23 25
+- price 23 20
+- assign 24 6
+- price 24 30
+- assign 25 0
+- price 25 20
+- assign 26 15
+- price 26 25
+- assign 27 10
+- price 27 40
+- assign 28 20
+- price 28 80
+- assign 29 5
+- price 29 100
+