Skip to content

Commit

Permalink
Change structure of Item
Browse files Browse the repository at this point in the history
  • Loading branch information
@julianmendez
julianmendez committed Apr 27, 2024
1 parent 285eb6a commit 03059fd
Show file tree
Hide file tree
Showing 6 changed files with 52 additions and 75 deletions.
27 changes: 9 additions & 18 deletions Soda/se/umu/cs/soda/prototype/example/market/core/Market.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ where
mk ::
owner : Nat
price : Money
advertised : Bool
deriving DecidableEq

namespace Item
Expand Down Expand Up @@ -97,31 +96,27 @@ 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



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)


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) : 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


Expand All @@ -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


Expand Down Expand Up @@ -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

Expand Down
25 changes: 9 additions & 16 deletions core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Market.soda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ class Item
abstract
owner : Nat
price : Money
advertised : Boolean

end

Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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

Expand Down
31 changes: 12 additions & 19 deletions core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
}

Expand Down Expand Up @@ -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
}
Expand Down
18 changes: 9 additions & 9 deletions core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketCollection.soda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
4 changes: 2 additions & 2 deletions core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketSpec.soda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
)
Expand Down
22 changes: 11 additions & 11 deletions core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
)

}
Expand All @@ -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)
)

}
Expand All @@ -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)
)

}
Expand Down Expand Up @@ -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)
)
Expand Down

0 comments on commit 03059fd

Please sign in to comment.