Miles

Introduction#

This contract stores miles per owners. Miles have an expiration date and valid miles can be consumed.

See this contract in action in the Fidelity Program Dapp example.

API#

Storage#

NameTypeDescription
adminaddressAdmin address to call add entrypoint.
milecollectionA mile is defined by:
  • id
  • amount
  • expiration date
ownercollectionA mile owner is defined by:
  • an address
  • a collection of mile

A mile is owned by one and only one owner: this is ensured by the use of partition collection type (see code below).

Entrypoints#

NameParametersDescription
addow, nm_id, nm_amount, nm_expCalled by admin to grant owner ow with nm_amount miles that expire on nm_exp.
consumeow, quantityCalled by admin to consume quantity valid miles (ie. miles with expiration date in the future) from owner ow.
clear_expiredRemoves expired miles.

Code#

miles.arl
archetype miles(admin : address)
asset mile identified by id {
id : string;
amount : nat;
expiration : date
}
asset owner identified by addr {
addr : address;
miles : partition<mile> = []
}
entry add (
ow : address,
nm_id : string,
nm_amount : nat,
nm_exp : date) {
called by admin
failif {
c2 : mile.contains(nm_id);
}
effect {
owner.addupdate (ow, { miles += [{
id = nm_id;
amount = nm_amount;
expiration = nm_exp
}] })
}
}
entry consume (ow : address, quantity : nat) {
called by admin
effect {
var lview = owner[ow].miles.sort(expiration).select(the.expiration >= now);
dorequire (lview.sum(the.amount) >= quantity, "NotEnoughMiles");
var remainder = quantity;
for : loop m in lview do
if remainder > 0 then begin
if mile[m].amount > remainder then begin
mile.update(m, { amount -= remainder });
remainder := 0
end else if mile[m].amount = remainder then begin
remainder := 0;
owner[ow].miles.remove(m)
end else begin
remainder -= mile[m].amount;
owner[ow].miles.remove(m)
end
end
done;
assert p1
}
}
entry clear_expired () {
for : loop2 o in owner do
owner[o].miles.removeif(the.expiration < now)
done
}