module Anoma.Resource;

import Anoma.Prelude open;
import Data.ByteString open;
import Anoma.Kind open;

import Stdlib.Data.Int as Int;

--- A ;Resource; is an immutable object that represents part of an application's
--- state.
type Resource :=
  mkResource {
    -- The address of the ;Resource;'s logic function
    logicHash : LogicHash;
    -- Specifies the fungibility domain for the resource
    label : ByteString;
    -- Extra data which is not related to the fungibility of the ;Resource;
    data : ByteString;
    -- An integer used to determine balance in transactions.
    quantity : Int
  };

open Resource;

mkSimpleResource (kind : Kind) (q : Int) : Resource :=
  mkResource@{
    logicHash := 0;
    label := kind;
    data := [];
    quantity := q
  };

--- Extract the data which determines the ;Resource;'s fungibility.
kind (r : Resource) : Kind := logicHash r :: label r;

delta (r : Resource) : Kind × Int := Resource.label r, Resource.quantity r;

--- Find all the resources associated with a kind
resourcesForKind (d : Kind) (rs : List Resource) : List Resource :=
  filter λ {r := Eq.eq (kind r) d} rs;

--- Aggregate the quantities associated with a kind
quantityOfKind (d : Kind) (rs : List Resource) : Int :=
  for (acc := Int.ofNat 0) (r in resourcesForKind d rs)
    quantity r + acc;

--- Return true if the list is empty or the list has exactly 1 element and the predicate is satisfied
zeroOrOneCheck (p : Resource -> Bool) : List Resource -> Bool
  | nil := true
  | [x] := p x
  | _ := false;

exactlyOneCheck (p : Resource -> Bool) : List Resource -> Bool
  | [x] := p x
  | _ := false;

type ResourceKind :=
  | created
  | consumed;

instance
eqResourceKind : Eq ResourceKind :=
  mkEq
    λ {
      | created created := true
      | consumed consumed := true
      | _ _ := false
    };

isCreated : ResourceKind -> Bool := (==) created;

isConsumed : ResourceKind -> Bool := (==) consumed;

instance
ordResource : Ord Resource :=
  let
    prod (r : Resource) : Kind × ByteString × Int := kind r, data r, quantity r;
    
    go (r1 : Resource) (r2 : Resource) : Ordering :=
      Ord.cmp (prod r1) (prod r2);
  in mkOrd go;