From 03059fdeef67aca1f9d6cab4818d2b6a939bda0d Mon Sep 17 00:00:00 2001 From: Julian Mendez Date: Sat, 27 Apr 2024 17:38:53 +0200 Subject: [PATCH] Change structure of Item --- .../prototype/example/market/core/Market.lean | 27 ++++++---------- .../prototype/example/market/core/Market.soda | 25 ++++++--------- .../example/market/core/Package.scala | 31 +++++++------------ .../example/market/core/MarketCollection.soda | 18 +++++------ .../example/market/core/MarketSpec.soda | 4 +-- .../example/market/core/Package.scala | 22 ++++++------- 6 files changed, 52 insertions(+), 75 deletions(-) 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) )