--- A DSL for constructing Kudos exchange intents
module Kudos.IntentDsl;

import Stdlib.Prelude open hiding {for; any; all};
import Anoma open public;
import Kudos.ExampleKinds open public;
import Kudos.Asset open;

type Quantifier :=
  | Any
  | All;

type QuantifiedAssets :=
  mkAssets {
    quantifier : Quantifier;
    assets : List Asset
  };

syntax operator of_ additive;
syntax alias of_ := mkAsset;

type Intention :=
  | Want
  | Give;

type Clause :=
  mkClause {
    lhs : Intention × QuantifiedAssets;
    rhs : QuantifiedAssets
  };

any (as : List Asset) : QuantifiedAssets :=
  mkAssets@{
    quantifier := Any;
    assets := as
  };

all (as : List Asset) : QuantifiedAssets :=
  mkAssets@{
    quantifier := All;
    assets := as
  };

exactly (a : Asset) : QuantifiedAssets :=
  mkAssets@{
    quantifier := All;
    assets := [a]
  };

want (a : QuantifiedAssets) : Intention × QuantifiedAssets := Want, a;

give (a : QuantifiedAssets) : Intention × QuantifiedAssets := Give, a;

syntax operator for pair;

for (l : Intention × QuantifiedAssets) (qs : QuantifiedAssets) : Clause :=
  mkClause@{
    lhs := l;
    rhs := qs
  };

kudosIntent (clauses : List Clause) : Transaction := mkKudosIntent clauses;

axiom mkKudosIntent : List Clause -> Transaction;