szabo_car_contract.hs

daml 1.2

module Main where

template LeaseOperation
  with
    creditor : Party
    owner : Party
    car : Party
    payment : Payment
  where
    signatory creditor
    observer owner, car

    -- Things the owner can do/control
    -- nonconsuming = the original contract remains unchanged
    nonconsuming choice StartCar : ()
      controller owner
      do
        assert (payment.status /= Delinquent)
        return ()

    -- Things the creditor can do/control
    -- By default choices are consuming
    -- This one consumes the original LeaseOperation and
    -- replaces it with a new LeaseOperation
    choice ChangeDriver : ContractId LeaseOperation
      with 
        newDriver : Party
        newBankPayments : Payment
      controller creditor
      do
        -- Assertions are requirements on the choice, if they're
        -- not met then the choice will not do anything, and
        -- the original contract will remain unchanged
        assert (payment.status == Delinquent && newBankPayments.car == car)
        -- this refers to the current instance of LeaseOperation
        -- create will replace it with a new one
        create this with owner = newDriver, payment = newBankPayments
    
    -- Note the one difference between this function
    -- and StartCar is that StartCar does not consume
    -- the contract (so the owner can still use it)
    -- while RevokeLease does consume the contract
    -- and replaces it with nothing (ie. ()).
    -- So the owner can no longer use it.
    choice RevokeLease : ()
      controller creditor
      do
        assert (payment.status == Delinquent)
        return ()

-- What payment statuses can we have?
data Status = Current | Delinquent | PaidInFull deriving (Eq, Show)

template Payment
  with
    car : Party
    creditor : Party
    owner : Party
    status : Status
  where
    signatory car
    observer creditor, owner

    -- Things the car can do/control. Yes, the car.
    choice ChangePaymentStatus : ContractId Payment
      with
        newStatus : Status
      controller car
      do
        create this with status = newStatus