module Input;

foreign c {
  int readPre(const char *key) {
      if (strcmp("change1-key", key)) {
          return 100;
      \} else if (strcmp("change2-key", key)) {
          return 90;
      \} else {
          return -1;
      \}
  \}

  int readPost(const char *key) {
      if (strcmp("change1-key", key)) {
          return 90;
      \} else if (strcmp("change2-key", key)) {
          return 100;
      \} else {
          return -1;
      \}
  \}

  char* isBalanceKey(const char* s1, const char* s2) {
      return "owner-address";
  \}
};

--------------------------------------------------------------------------------
-- Booleans
--------------------------------------------------------------------------------

type Bool :=
     true : Bool
  | false : Bool;

infixr 2 ||;
|| : Bool → Bool → Bool;
|| false a := a;
|| true _ := true;

infixr 3 &&;
&& : Bool → Bool → Bool;
&& false _ := false;
&& true a := a;

if : {A : Type} → Bool → A → A → A;
if true a _ := a;
if false _ b := b;

--------------------------------------------------------------------------------
-- Backend Booleans
--------------------------------------------------------------------------------

axiom BackendBool : Type;
compile BackendBool {
  c ↦ "bool";
};

axiom backend-true : BackendBool;
compile backend-true {
  c ↦ "true";
};

axiom backend-false : BackendBool;
compile backend-false {
  c ↦ "false";
};

--------------------------------------------------------------------------------
-- Backend Bridge
--------------------------------------------------------------------------------

foreign c {
  void* boolInd(bool b, void* a1, void* a2) {
    return b ? a1 : a2;
  \}
};

axiom bool : BackendBool → Bool → Bool → Bool;
compile bool {
  c ↦ "boolInd";
};

from-backend-bool : BackendBool → Bool;
from-backend-bool bb := bool bb true false;

--------------------------------------------------------------------------------
-- Functions
--------------------------------------------------------------------------------

id : {A : Type} → A → A;
id a := a;

--------------------------------------------------------------------------------
-- Integers
--------------------------------------------------------------------------------

axiom Int : Type;
axiom Int_0 : Int;

compile Int {
  c ↦ "int";
};

compile Int_0 {
  c ↦ "0";
};

foreign c {
   bool lessThan(int l, int r) {
     return l < r;
   \}

   bool eqInt(int l, int r) {
     return l == r;
   \}

   int plus(int l, int r) {
     return l + r;
   \}

   int minus(int l, int r) {
     return l - r;
   \}
};

infix 4 <';
axiom <' : Int → Int → BackendBool;
compile <' {
  c ↦ "lessThan";
};

infix 4 <;
< : Int → Int → Bool;
< i1 i2 := from-backend-bool (i1 <' i2);

isNegative : Int → Bool;
isNegative n := n < Int_0;

axiom eqInt : Int → Int → BackendBool;
compile eqInt {
  c ↦ "eqInt";
};

infix 4 ==Int;
==Int : Int → Int → Bool;
==Int i1 i2 := from-backend-bool (eqInt i1 i2);

infixl 6 -;
axiom - : Int -> Int -> Int;
compile - {
  c ↦ "minus";
};

infixl 6 +;
axiom + : Int -> Int -> Int;
compile + {
  c ↦ "plus";
};

--------------------------------------------------------------------------------
-- Strings
--------------------------------------------------------------------------------

builtin string axiom String : Type;
compile String {
  c ↦ "char*";
};

foreign c {
  bool eqString(char* l, char* r) {
    return strcmp(l, r) == 0;
  \}
};

axiom eqString : String → String → BackendBool;
compile eqString  {
  c ↦ "eqString";
};

infix 4 ==String;
==String : String → String → Bool;
==String s1 s2 := from-backend-bool (eqString s1 s2);

--------------------------------------------------------------------------------
-- Lists
--------------------------------------------------------------------------------

infixr 5 ::;
type List (A : Type) :=
  nil : List A
  | :: : A → List A → List A;

elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
elem _ _ nil := false;
elem eq s (x :: xs) := eq s x || elem eq s xs;

foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
foldl f z nil := z;
foldl f z (h :: hs) := foldl f (f z h) hs;

--------------------------------------------------------------------------------
-- Pair
--------------------------------------------------------------------------------

infixr 4 ,;
infixr 2 ×;
type × (A : Type) (B : Type) :=
  , : A → B → A × B;

--------------------------------------------------------------------------------
-- Maybe
--------------------------------------------------------------------------------

type Maybe (A : Type) :=
 nothing : Maybe A |
 just : A → Maybe A;

from-int : Int → Maybe Int;
from-int i := if (isNegative i) nothing (just i);

maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B;
maybe b _ nothing := b;
maybe _ f (just x) := f x;

from-string : String → Maybe String;
from-string s := if (s ==String "") nothing (just s);

pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool;
pair-from-optionString := maybe (Int_0, false);

--------------------------------------------------------------------------------
-- Anoma
--------------------------------------------------------------------------------

axiom readPre : String → Int;
compile readPre {
  c ↦ "readPre";
};

axiom readPost : String → Int;
compile readPost {
  c ↦ "readPost";
};

axiom isBalanceKey : String → String → String;
compile isBalanceKey {
  c ↦ "isBalanceKey";
};

read-pre : String → Maybe Int;
read-pre s := from-int (readPre s);

read-post : String → Maybe Int;
read-post s := from-int (readPost s);

is-balance-key : String → String → Maybe String;
is-balance-key token key := from-string (isBalanceKey token key);

unwrap-default : Maybe Int → Int;
unwrap-default := maybe Int_0 id;

--------------------------------------------------------------------------------
-- Validity Predicate
--------------------------------------------------------------------------------

change-from-key : String → Int;
change-from-key key := unwrap-default (read-post key) - unwrap-default (read-pre key);

check-vp : List String → String → Int → String → Int × Bool;
check-vp verifiers key change owner :=
    if
        (isNegative (change-from-key key))
        -- make sure the spender approved the transaction
        (change + (change-from-key key), elem (==String) owner verifiers)
        (change + (change-from-key key), true);

check-keys : String → List String → Int × Bool → String → Int × Bool;
check-keys token verifiers (change, is-success) key :=
    if
        is-success
        (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
        (Int_0, false);

check-result : Int × Bool → Bool;
check-result (change, all-checked) := (change ==Int Int_0) && all-checked;

vp : String → List String → List String → Bool;
vp token keys-changed verifiers :=
    check-result
        (foldl
            (check-keys token verifiers)
            (Int_0, true)
            keys-changed);

--------------------------------------------------------------------------------
-- IO
--------------------------------------------------------------------------------

axiom Action : Type;
compile Action {
  c ↦ "int";
};

axiom putStr : String → Action;
compile putStr {
  c ↦ "putStr";
};

axiom putStrLn : String → Action;
compile putStrLn {
  c ↦ "putStrLn";
};

foreign c {
  int sequence(int a, int b) {
    return a + b;
  \}
};

infixl 1 >>;
axiom >> : Action → Action → Action;
compile >> {
  c ↦ "sequence";
};

show-result : Bool → String;
show-result true := "OK";
show-result false := "FAIL";

--------------------------------------------------------------------------------
-- Testing VP
--------------------------------------------------------------------------------

token : String;
token := "owner-token";

owner-address : String;
owner-address := "owner-address";

change1-key : String;
change1-key := "change1-key";

change2-key : String;
change2-key := "change2-key";

verifiers : List String;
verifiers := owner-address :: nil;

keys-changed : List String;
keys-changed := change1-key :: change2-key :: nil;

main : Action;
main :=
    (putStr "VP Status: ")
    >> (putStrLn (show-result (vp token keys-changed verifiers)));

end;