module Anoma.PartialTx;

import Anoma.Prelude open;
import Anoma.Resource open;

--- A partial transaction consists of consumed resources and created resources
type PartialTx :=
  mkPartialTx {
    consumedResources : List Resource;
    createdResources : List Resource
  };

open PartialTx;

{-- A function that determines whether a ;PartialTx; is valid

Arguments:

* kind: Indicating whether the resource associated with this logic function
 was consumed or created in the subject ;PartialTx;.

* partialTx: The ;PartialTx; being validated. --}

LogicFunction : Type := ResourceKind -> PartialTx -> Bool;

instance
ordPartialTx : Ord PartialTx :=
  let
    prod (r : PartialTx) : List Resource × List Resource :=
      consumedResources r, createdResources r;
    
    go (p1 : PartialTx) (p2 : PartialTx) : Ordering :=
      Ord.cmp (prod p1) (prod p2);
  in mkOrd go;