Add bank example (#2037)

This PR adds the Juvix program for the `Bank` example provided in the
[Leo
workshop
repository](https://github.com/AleoHQ/workshop/blob/master/basic_bank/src/main.leo).

Makefile

@@ -10,6 +10,7 @@ EXAMPLES= Collatz/Collatz.juvix \
 	HelloWorld/HelloWorld.juvix \
 	PascalsTriangle/PascalsTriangle.juvix \
 	TicTacToe/CLI/TicTacToe.juvix \
+	Bank/Bank.juvix \
 	Tutorial/Tutorial.juvix
 
 DEMO_EXAMPLE=examples/demo/Demo.juvix

examples/milestone/Bank/Bank.juvix

@@ -0,0 +1,138 @@
+--- This example is taken from the Leo workshop:
+---
+--- https://github.com/AleoHQ/workshop/tree/master/basic_bank
+module Bank;
+
+open import Stdlib.Prelude;
+open import Stdlib.Debug.Fail;
+
+open import Stdlib.Data.Nat.Ord;
+
+import Stdlib.Data.Nat as Nat;
+
+Address : Type;
+Address := Nat;
+
+bankAddress : Address;
+bankAddress := 1234;
+
+--- Some field type.
+axiom Field : Type;
+
+--- Equality test for ;Field;.
+axiom eqField : Field -> Field -> Bool;
+
+module Token;
+  type Token :=
+    | --- Arguments are: owner, gates, amount.
+      mkToken : Address -> Nat -> Nat -> Token;
+
+  --- Retrieves the owner from a ;Token;
+  getOwner : Token -> Address;
+  getOwner (mkToken o _ _) := o;
+
+  --- Retrieves the amount from a ;Token;
+  getAmount : Token -> Nat;
+  getAmount (mkToken _ _ a) := a;
+
+  --- Retrieves the gates from a ;Token;
+  getGates : Token -> Nat;
+  getGates (mkToken _ g _) := g;
+end;
+
+open Token;
+
+--- This module defines the type for balances and its associated operations.
+module Balances;
+  Balances : Type;
+  Balances := List (Field × Nat);
+
+  --- Increments the amount associated with a certain ;Field;.
+  increment : Field -> Nat -> Balances -> Balances;
+  increment f n nil := (f, n) :: nil;
+  increment f n ((b, bn) :: bs) :=
+    if
+      (eqField f b)
+      ((b, bn + n) :: bs)
+      ((b, bn) :: increment f n bs);
+
+  --- Decrements the amount associated with a certain ;Field;.
+  --- If the ;Field; is not found, it does nothing.
+  --- Subtraction is truncated to ;zero;.
+  decrement : Field -> Nat -> Balances -> Balances;
+  decrement _ _ nil := nil;
+  decrement f n ((b, bn) :: bs) :=
+    if
+      (eqField f b)
+      ((b, sub bn n) :: bs)
+      ((b, bn) :: decrement f n bs);
+
+  emtpyBalances : Balances;
+  emtpyBalances := nil;
+
+  --- Commit balances changes to the chain.
+  axiom commitBalances : Balances -> IO;
+end;
+
+open Balances;
+
+--- Runs an ;IO; action on the chain.
+axiom runOnChain : {B : Type} -> IO -> B -> B;
+
+--- Computes the hash associated with an ;Address;.
+axiom hashAddress : Address -> Field;
+
+--- Returns the total amount of tokens after compounding interest.
+calculateInterest : Nat -> Nat -> Nat -> Nat;
+calculateInterest principal rate periods :=
+  let
+    amount : Nat := principal;
+    incrAmount : Nat -> Nat;
+    incrAmount a := div (a * rate) 10000;
+  in iterate (min 100 periods) incrAmount amount;
+
+--- Asserts some ;Bool; condition.
+assert : {A : Type} -> Bool -> A -> A;
+assert c a := if c a (fail "assertion failed");
+
+--- Returns a new ;Token;. Arguments are:
+---
+--- `owner`: The address of the account to issue the token to
+---
+--- `amount`: The amount of  tokens to issue
+---
+--- `caller`: Who is creating the transaction. It must be the bank.
+issue : Address -> Address -> Nat -> Token;
+issue caller owner amount :=
+  assert (caller == bankAddress) (mkToken owner 0 amount);
+
+--- Deposits some amount of money into the bank.
+deposit : Balances -> Token -> Nat -> Token;
+deposit bal token amount :=
+  let
+    difference : Nat := sub (getAmount token) amount;
+    remaining :
+        Token :=
+          mkToken (getOwner token) (getGates token) difference;
+    hash : Field := hashAddress (getOwner token);
+    bal' : Balances := increment hash amount bal;
+  in runOnChain (commitBalances bal') remaining;
+
+--- Returns a new ;Token; containing the amount of money withdrawn.
+withdraw :
+  Balances
+    -> Address
+    -> Address
+    -> Nat
+    -> Nat
+    -> Nat
+    -> Token;
+withdraw bal caller recipient amount rate periods :=
+  assert
+    (caller == bankAddress)
+    (let
+      hash : Field := hashAddress recipient;
+      total : Nat := calculateInterest amount rate periods;
+      token : Token := mkToken recipient 0 total;
+      bal' : Balances := decrement hash amount bal;
+    in runOnChain (commitBalances bal') token);

examples/milestone/Bank/juvix.yaml

@@ -0,0 +1,4 @@
+dependencies:
+- .juvix-build/stdlib/
+name: bank
+version: 0.0.0

examples/milestone/PascalsTriangle/PascalsTriangle.juvix

@@ -19,9 +19,9 @@ zipWith f _ nil := nil;
 zipWith f (x :: xs) (y :: ys) := f x y :: zipWith f xs ys;
 
 --- Return a list of repeated applications of a given function
-iterate : {A : Type} → Nat → (A → A) → A → List A;
-iterate zero _ _ := nil;
-iterate (suc n) f a := a :: iterate n f (f a);
+scanIterate : {A : Type} → Nat → (A → A) → A → List A;
+scanIterate zero _ _ := nil;
+scanIterate (suc n) f a := a :: scanIterate n f (f a);
 
 --- Produce a singleton List
 singleton : {A : Type} → A → List A;
@@ -55,7 +55,7 @@ pascalNextRow row :=
 
 --- Produce Pascal's triangle to a given depth
 pascal : Nat → List (List Nat);
-pascal rows := iterate rows pascalNextRow (singleton 1);
+pascal rows := scanIterate rows pascalNextRow (singleton 1);
 
 main : IO;
 main := printStringLn (unlines (map showList (pascal 10)));

juvix-stdlib

@@ -1 +1 @@
-Subproject commit 3ae758a5049263790350298ee9758bf1f97bb14c
+Subproject commit 059d502b1f989faed5470271e97571c2b1deaa10

tests/Compilation/positive/test030.juvix

@@ -1,7 +1,7 @@
 -- Ackermann function (higher-order definition)
 module test030;
 
-open import Stdlib.Prelude;
+open import Stdlib.Prelude hiding {iterate};
 
 iterate : {A : Type} → (A → A) → Nat → A → A;
 -- clauses with differing number of patterns not yet supported