Airline Model - CheckIn Choice

Hi Team,

Can you please explain the following code for the choice “CheckIn” in Airline model

do
flight ← fetch flightCid
flight.flightNumber === flightNumber
flight.airline === airline
assert $ fromSome (TM.lookup seat flight.seatClasses) <= ticketClass
boardingPasssCid ← create BoardingPass with
seatNumber = seat
ticket = this
newFlightCid ← exercise flightCid AssignSeat with
passenger; seat; ticketRef
return (boardingPasssCid, newFlightCid)

Thank you
Erum

do
  -- First, we get the data corresponding to the Contract ID `flightCid`
  flight <- fetch flightCid
  -- `===` means "abort if not equal", or alternatively "ensure is equal"
  -- We check that we have the expected flight number
  flight.flightNumber === flightNumber
  -- and the expected airline
  flight.airline === airline
  -- and that the class of the seat is lower than or equal to the class of the ticket
  -- (`assert` aborts if the argument is not "true")
  assert $ fromSome (TM.lookup seat flight.seatClasses) <= ticketClass
  -- Now that we know all of the relevant attributes match,
  -- we can create a boarding pass
  boardingPasssCid <- create BoardingPass with
                              seatNumber = seat
                              ticket = this
  -- and we "update" the flight contract to record
  -- that this seat is no longer available
  newFlightCid <- exercise flightCid AssignSeat with
  -- these are syntactic shortcuts for
  -- passenger = passenger
  -- seat = seat
  -- ticketRef = ticketRef
  -- where the left part is the name of the attribute of the
  -- AssignSeat data structure, and the right side is the
  -- name of the local variable containing the desired value
                                       passenger;
                                       seat;
                                       ticketRef
  -- we return the Contract IDs of the two contracts we have created
  -- (the boarding pass, and the new "state" of the flight)
  return (boardingPasssCid, newFlightCid)

Happy to answer more specific questions if anything is still unclear.

Gary_Verhaegen:

-- and that the class of the seat is lower than or equal to the class of the ticket
  -- (`assert` aborts if the argument is not "true")
  assert $ fromSome (TM.lookup seat flight.seatClasses) <= ticketClass

Thank you so much for detailed reply. Can you explain this part "Class of Seat? and Class of Ticket?

Disclaimer: I have not looked at the project at all, I’m only reading the code you shared here. I may be getting the context wrong.

Let’s deconstruct this line. It is equivalent to the more explicit and verbose version:

do
  let optSeatClass = TM.lookup seat flight.seatClasses
  let seatClass = fromSome optSeatClass
  let isTicketValidForSeat = seatClass <= ticketClass
  assert isTicketValidForSeat

Looking at this one line at a time:

• I’m assuming TM is the TextMap module. So, from context, it looks like seat is the seat we are trying to book, and flight.seatClasses is a mapping from “seat ID” to “class”. When looking up a key in a TextMap, we get back an Optional: None if the seat ID is not in the map, and Some class if the seat ID is in the map (and thus maps to a given class). That Some wrapper around the class is annoying, so we get to the next line.
• fromSome “unwraps” an Optional, provided it is Some. If it happens to be None, we crash. So now seatClass is the class of the seat we are trying to book, and ticketClass is the class of the ticket.
• We consider a ticket valid for a seat if the ticket is at least as high as the seat. In other words, a passenger with a first-class ticket is allowed to book an economy seat, but not the reverse.
• Finally, assert is a “function” of one boolean argument that does nothing if the argument is True and crashes if the argument is False.

The code as originally written uses the priority rules of Daml and the special operator $ to reduce the number of parentheses. That’s a stylistic choice; in case that helps, a fully-parenthesised version would look like:

assert ((fromSome (TM.lookup seat flight.seatClasses)) <= ticketClass)

Thank you so much and its really helpful and clear now.

Great commenting, makes this clearer to me also.

Thank you