diff --git a/Soda/se/umu/cs/soda/prototype/example/market/core/Market.lean b/Soda/se/umu/cs/soda/prototype/example/market/core/Market.lean
index 2f9f4ea..80977ea 100644
--- a/Soda/se/umu/cs/soda/prototype/example/market/core/Market.lean
+++ b/Soda/se/umu/cs/soda/prototype/example/market/core/Market.lean
@@ -10,7 +10,6 @@ where
mk ::
owner : Nat
price : Money
- advertised : Bool
deriving DecidableEq
namespace Item
@@ -97,7 +96,7 @@ private def _reassign_item (items : List ( Item ) ) (item_id : Nat) (user_id:
: List ( Item ) :=
match (_mm.get ( Item ) (items) (item_id) ) with
| Option.some (item) =>
- _mm.set ( Item ) (items) (item_id) (Item.mk (user_id) (item.price) (item.advertised) )
+ _mm.set ( Item ) (items) (item_id) (Item.mk (user_id) (item.price) )
| Option.none => items
@@ -105,7 +104,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) (false) :: items
+ then Item.mk (user_id) (0) :: items
else _reassign_item (items) (item_id) (user_id)
@@ -113,15 +112,11 @@ private def _assign_to_user (items : List ( Item ) ) (item_id : Nat) (user_id:
Market.mk (m.accounts) (_assign_to_user (m.items) (item_id) (user_id) )
- def auto_advertise (p : Money) : Bool :=
- p > 0
-
-
private def _price_item (items : List ( Item ) ) (item_id : Nat) (p : Money)
: List ( Item ) :=
match (_mm.get ( Item ) (items) (item_id) ) with
| Option.some (item) =>
- _mm.set ( Item ) (items) (item_id) (Item.mk (item.owner) (p) (auto_advertise (p) ) )
+ _mm.set ( Item ) (items) (item_id) (Item.mk (item.owner) (p) )
| Option.none => items
@@ -130,22 +125,18 @@ private def _price_item (items : List ( Item ) ) (item_id : Nat) (p : Money)
Market.mk (m.accounts) (_price_item (m.items) (item_id) (p) )
- private def _advertise (items : List ( Item ) ) (item_id : Nat) : List ( Item ) :=
- match (_mm.get ( Item ) (items) (item_id) ) with
+ def is_advertised (market : Market) (item_id : Nat) : Bool :=
+ match (_mm.get ( Item ) (market.items) (item_id) ) with
| Option.some (item) =>
- _mm.set ( Item ) (items) (item_id) (Item_ (item.owner) (item.price) (true) )
- | Option.none => items
+ item.price > 0
+ | Option.none => false
- def advertise (market : Market) (item_id : Nat) : Market :=
- Market.mk (market.accounts) (_advertise (market.items) (item_id) )
-
-
private def _remove_ad (items : List ( Item ) ) (item_id : Nat) : List ( Item ) :=
match (_mm.get ( Item ) (items) (item_id) ) with
| Option.some (item) =>
- _mm.set ( Item ) (items) (item_id) (Item_ (item.owner) (item.price) (false) )
+ _mm.set ( Item ) (items) (item_id) (Item.mk (item.owner) (0) )
| Option.none => items
@@ -184,7 +175,7 @@ private def _transfer (accounts : List ( Money ) ) (origin : Nat) (target : Na
| Option.some (item) =>
Market.mk (
_transfer (market.accounts) (buyer) (item.owner) (item.price) ) (
- _mm.set ( Item ) (market.items) (item_id) (Item_ (buyer) (item.price) (false) )
+ _mm.set ( Item ) (market.items) (item_id) (Item.mk (buyer) (0) )
)
| Option.none => market
diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Market.soda b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Market.soda
index 8ba34a0..47cca7f 100644
--- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Market.soda
+++ b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Market.soda
@@ -12,7 +12,6 @@ class Item
abstract
owner : Nat
price : Money
- advertised : Boolean
end
@@ -77,44 +76,38 @@ class MarketMod
: List [Item] =
match (_mm .get [Item] (items) (item_id) )
case Some (item) ==>
- _mm .set [Item] (items) (item_id) (Item .mk (user_id) (item .price) (item .advertised) )
+ _mm .set [Item] (items) (item_id) (Item .mk (user_id) (item .price) )
case None ==> items
_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) (false) :: items
+ then Item .mk (user_id) (0) :: items
else _reassign_item (items) (item_id) (user_id)
assign (m : Market) (item_id : Nat) (user_id : Nat) : Market =
Market .mk (m .accounts) (_assign_to_user (m .items) (item_id) (user_id) )
- auto_advertise (p : Money) : Boolean =
- p > 0
-
_price_item (items : List [Item] ) (item_id : Nat) (p : Money)
: List [Item] =
match (_mm .get [Item] (items) (item_id) )
case Some (item) ==>
- _mm .set [Item] (items) (item_id) (Item .mk (item .owner) (p) (auto_advertise (p) ) )
+ _mm .set [Item] (items) (item_id) (Item .mk (item .owner) (p) )
case None ==> items
price_item (m : Market) (item_id : Nat) (p : Money) : Market =
Market .mk (m .accounts) (_price_item (m .items) (item_id) (p) )
- _advertise (items : List [Item] ) (item_id : Nat) : List [Item] =
- match (_mm .get [Item] (items) (item_id) )
+ is_advertised (market : Market) (item_id : Nat) : Boolean =
+ match (_mm .get [Item] (market .items) (item_id) )
case Some (item) ==>
- _mm .set [Item] (items) (item_id) (Item_ (item .owner) (item .price) (true) )
- case None ==> items
-
- advertise (market : Market) (item_id : Nat) : Market =
- Market.mk (market .accounts) (_advertise (market .items) (item_id) )
+ item .price > 0
+ case None ==> false
_remove_ad (items : List [Item] ) (item_id : Nat) : List [Item] =
match (_mm .get [Item] (items) (item_id) )
case Some (item) ==>
- _mm .set [Item] (items) (item_id) (Item_ (item .owner) (item .price) (false) )
+ _mm .set [Item] (items) (item_id) (Item .mk (item .owner) (0) )
case None ==> items
remove_ad (market : Market) (item_id : Nat) : Market =
@@ -145,7 +138,7 @@ class MarketMod
case Some (item) ==>
Market .mk (
_transfer (market .accounts) (buyer) (item .owner) (item .price) ) (
- _mm .set [Item] (market .items) (item_id) (Item_ (buyer) (item .price) (false) )
+ _mm .set [Item] (market .items) (item_id) (Item .mk (buyer) (0) )
)
case None ==> market
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 8ee45e5..2c47717 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
@@ -37,15 +37,14 @@ trait Item
def owner : Nat
def price : Money
- def advertised : Boolean
}
-case class Item_ (owner : Nat, price : Money, advertised : Boolean) extends Item
+case class Item_ (owner : Nat, price : Money) extends Item
object Item {
- def mk (owner : Nat) (price : Money) (advertised : Boolean) : Item =
- Item_ (owner, price, advertised)
+ def mk (owner : Nat) (price : Money) : Item =
+ Item_ (owner, price)
}
trait Market
@@ -120,47 +119,41 @@ trait MarketMod
: List [Item] =
(_mm .get [Item] (items) (item_id) ) match {
case Some (item) =>
- _mm .set [Item] (items) (item_id) (Item .mk (user_id) (item .price) (item .advertised) )
+ _mm .set [Item] (items) (item_id) (Item .mk (user_id) (item .price) )
case None => items
}
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) (false) :: items
+ ) Item .mk (user_id) (0) :: items
else _reassign_item (items) (item_id) (user_id)
def assign (m : Market) (item_id : Nat) (user_id : Nat) : Market =
Market .mk (m .accounts) (_assign_to_user (m .items) (item_id) (user_id) )
- def auto_advertise (p : Money) : Boolean =
- p > 0
-
private def _price_item (items : List [Item] ) (item_id : Nat) (p : Money)
: List [Item] =
(_mm .get [Item] (items) (item_id) ) match {
case Some (item) =>
- _mm .set [Item] (items) (item_id) (Item .mk (item .owner) (p) (auto_advertise (p) ) )
+ _mm .set [Item] (items) (item_id) (Item .mk (item .owner) (p) )
case None => items
}
def price_item (m : Market) (item_id : Nat) (p : Money) : Market =
Market .mk (m .accounts) (_price_item (m .items) (item_id) (p) )
- private def _advertise (items : List [Item] ) (item_id : Nat) : List [Item] =
- (_mm .get [Item] (items) (item_id) ) match {
+ def is_advertised (market : Market) (item_id : Nat) : Boolean =
+ (_mm .get [Item] (market .items) (item_id) ) match {
case Some (item) =>
- _mm .set [Item] (items) (item_id) (Item_ (item .owner, item .price, true) )
- case None => items
+ item .price > 0
+ case None => false
}
- def advertise (market : Market) (item_id : Nat) : Market =
- Market.mk (market .accounts) (_advertise (market .items) (item_id) )
-
private def _remove_ad (items : List [Item] ) (item_id : Nat) : List [Item] =
(_mm .get [Item] (items) (item_id) ) match {
case Some (item) =>
- _mm .set [Item] (items) (item_id) (Item_ (item .owner, item .price, false) )
+ _mm .set [Item] (items) (item_id) (Item .mk (item .owner) (0) )
case None => items
}
@@ -194,7 +187,7 @@ trait MarketMod
case Some (item) =>
Market .mk (
_transfer (market .accounts) (buyer) (item .owner) (item .price) ) (
- _mm .set [Item] (market .items) (item_id) (Item_ (buyer, item .price, false) )
+ _mm .set [Item] (market .items) (item_id) (Item .mk (buyer) (0) )
)
case None => market
}
diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketCollection.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketCollection.soda
index 73c6357..397e306 100644
--- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketCollection.soda
+++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketCollection.soda
@@ -8,9 +8,9 @@ class Market01
items : List [Item] =
List [Item] (
- Item_ (0) (125) (false) ,
- Item_ (1) (375) (false) ,
- Item_ (1) (10) (false)
+ Item .mk (0) (125) ,
+ Item .mk (1) (0) ,
+ Item .mk (1) (10)
)
end
@@ -24,9 +24,9 @@ class Market02
items : List [Item] =
List [Item] (
- Item_ (0) (125) (false) ,
- Item_ (1) (375) (true) ,
- Item_ (1) (10) (false)
+ Item .mk (0) (125) ,
+ Item .mk (1) (375) ,
+ Item .mk (1) (10)
)
end
@@ -40,9 +40,9 @@ class Market03
items : List [Item] =
List [Item] (
- Item_ (0) (125) (false) ,
- Item_ (2) (375) (false) ,
- Item_ (1) (10) (false)
+ Item .mk (0) (125) ,
+ Item .mk (2) (0) ,
+ Item .mk (1) (10)
)
end
diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketSpec.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketSpec.soda
index ab6947e..39ae19c 100644
--- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketSpec.soda
+++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketSpec.soda
@@ -15,9 +15,9 @@ class MarketSpec ()
market03 : Market = Market03_ ()
- test ("should advertise an item") (
+ test ("should price an item") (
check (
- obtained := module .advertise (market01) (1)
+ obtained := module .price_item (market01) (1) (375)
) (
expected := module .as_market (market02)
)
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 364b0d1..4e424da 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
@@ -22,9 +22,9 @@ trait Market01
lazy val items : List [Item] =
List [Item] (
- Item_ (0, 125, false) ,
- Item_ (1, 375, false) ,
- Item_ (1, 10, false)
+ Item .mk (0) (125) ,
+ Item .mk (1) (0) ,
+ Item .mk (1) (10)
)
}
@@ -46,9 +46,9 @@ trait Market02
lazy val items : List [Item] =
List [Item] (
- Item_ (0, 125, false) ,
- Item_ (1, 375, true) ,
- Item_ (1, 10, false)
+ Item .mk (0) (125) ,
+ Item .mk (1) (375) ,
+ Item .mk (1) (10)
)
}
@@ -70,9 +70,9 @@ trait Market03
lazy val items : List [Item] =
List [Item] (
- Item_ (0, 125, false) ,
- Item_ (2, 375, false) ,
- Item_ (1, 10, false)
+ Item .mk (0) (125) ,
+ Item .mk (2) (0) ,
+ Item .mk (1) (10)
)
}
@@ -101,9 +101,9 @@ case class MarketSpec ()
lazy val market03 : Market = Market03_ ()
- test ("should advertise an item") (
+ test ("should price an item") (
check (
- obtained = module .advertise (market01) (1)
+ obtained = module .price_item (market01) (1) (375)
) (
expected = module .as_market (market02)
)