Support partial application and closure passing in C backend (#190)

* Add support for parital application eval/apply

* include string.h in libc runtime

* Add wasm SimpleFungibleTokenImplicit to tests

* Update VP example to new syntax

* propagate types from all reachable modules

* Change prelude import ordering to workaround minic issue

* Pre-declare inductive typedefs in C backend

This generates the typedefs corresponding to each inductive type.

e.g

```
inductive Bool { .. }
```

is translated to:

```
typedef struct Bool_3_s Bool_3_t;
```

This means that C code can reference these typedefs before they have
been fully defined. (all references to inductive types go through these typedefs
names).

This fixes an issue with the ordering of delcarations when modules are included.

* Use common Lib for MiniC tests

* libc runtime: flush stdout after writing to it

* Adds MiniTicTacToe example using common example lib

In MonoJuvixToMiniC we emit the inductive type typedefs before anything
else to support includes ordering

* Adds tests for mutually recrusive functions

* Add golden tests for milestone examples

* Example: Remove commented out code

* Test error handling behaviour in MiniTicTacToe

* Fail clang compilation on warnings

* Add test for Nested list types

* Add PrettyCode instances for NonEmpty and ConcreteType

* Ignore IsImplicit field in Eq and Hashable of TypeApplication

This is to workaround a crash in Micro->Mono translation when looking up
a concrete type

* Fix formatting

* hlint fixes

* Formatting fixes not reported by local pre-commit

* Refactor MonoJuvixToMiniC

* Fix shelltest

NB: We cannot check the order of the 'Writing' lines because this
depends on the order of files returned by the FS which is
non-deterministic between systems

* Refactor Base to CBuilder

* Refactor using applyOnFunStatement

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>

examples/milestone/Lib/Data/Bool.mjuvix

@@ -19,6 +19,10 @@ infixr 3 &&;
 && false _ ≔ false;
 && true a ≔ a;
 
+not : Bool → Bool;
+not true ≔ false;
+not false ≔ true;
+
 if : {A : Type} → Bool → A → A → A;
 if true a _ ≔ a;
 if false _ b ≔ b;

examples/milestone/Lib/Data/Int.mjuvix

@@ -3,6 +3,9 @@ module Data.Int;
 import Data.Bool;
 open Data.Bool;
 
+import Data.String;
+open Data.String;
+
 axiom Int : Type;
 compile Int {
   c ↦ "int";
@@ -62,4 +65,10 @@ compile + {
   ghc ↦ "(+)";
 };
 
+axiom intToStr : Int → String;
+
+compile intToStr {
+  c ↦ "intToStr";
+};
+
 end;

examples/milestone/Lib/Data/List.mjuvix

@@ -0,0 +1,57 @@
+module Data.List;
+
+import Data.Bool;
+open Data.Bool;
+
+infixr 5 ∷;
+inductive 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;
+
+map : {A : Type} → {B : Type} → (A → B) → List A → List B;
+map f nil ≔ nil;
+map f (h ∷ hs) ≔ f h ∷ map f hs;
+
+null : {A : Type} → List A → Bool;
+null nil ≔ true;
+null _ ≔ false;
+
+head : {A : Type} → List A → A;
+head (x ∷ _) ≔ x;
+
+tail : {A : Type} → List A → List A;
+tail (_ ∷ xs) ≔ xs;
+
+terminating
+transpose : {A : Type} → List (List A) → List (List A);
+transpose (nil ∷ _) ≔ nil;
+transpose xss ≔ (map head xss) ∷ (transpose (map tail xss));
+
+concatList : {A : Type} → List A → List A → List A;
+concatList nil xss ≔ xss;
+concatList (x ∷ xs) xss ≔ x ∷ (concatList xs xss);
+
+flatten : {A : Type} → List (List A) → List A;
+flatten ≔ foldl concatList nil;
+
+prependToAll : {A : Type} → A → List A → List A;
+prependToAll _ nil ≔ nil;
+prependToAll sep (x ∷ xs) ≔ sep ∷ x ∷ prependToAll sep xs;
+
+intersperse : {A : Type} → A → List A → List A;
+intersperse _ nil ≔ nil;
+intersperse sep (x ∷ xs) ≔ x ∷ prependToAll sep xs;
+
+any : {A : Type} → (A → Bool) → List A → Bool;
+any f xs ≔ foldl (||) false (map f xs);
+
+end;

examples/milestone/Lib/Data/Maybe.mjuvix

@@ -11,11 +11,16 @@ inductive Maybe (A : Type) {
  just : A → Maybe A;
 };
 
--- from-int : Int → Maybe Int;
--- from-int i ≔ if (i < 0) nothing (just i);
-
 maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B;
 maybe b _ nothing ≔ b;
 maybe _ f (just x) ≔ f x;
 
+fmapMaybe : {A : Type} → {B : Type} → (A → B) → Maybe A → Maybe B;
+fmapMaybe _ nothing ≔ nothing;
+fmapMaybe f (just a) ≔ just (f a);
+
+bindMaybe : {A : Type} → {B : Type} → (A → Maybe B) → Maybe A → Maybe B;
+bindMaybe _ nothing ≔ nothing;
+bindMaybe f (just a) ≔ f a;
+
 end;

examples/milestone/Lib/Data/Nat.mjuvix

@@ -0,0 +1,98 @@
+module Data.Nat;
+
+import Data.Bool;
+open Data.Bool;
+
+import Data.Int;
+open Data.Int;
+
+import Data.String;
+open Data.String;
+
+inductive Nat {
+  zero : Nat;
+  suc : Nat → Nat;
+};
+
+==Nat : Nat → Nat → Bool;
+==Nat zero zero ≔ true;
+==Nat (suc m) (suc n) ≔ ==Nat m n;
+==Nat _ _ ≔ false;
+
+one : Nat;
+one ≔ suc zero;
+
+two : Nat;
+two ≔ suc one;
+
+three : Nat;
+three ≔ suc two;
+
+four : Nat;
+four ≔ suc three;
+
+five : Nat;
+five ≔ suc four;
+
+six : Nat;
+six ≔ suc five;
+
+seven : Nat;
+seven ≔ suc six;
+
+eight : Nat;
+eight ≔ suc seven;
+
+nine : Nat;
+nine ≔ suc eight;
+
+ten : Nat;
+ten ≔ suc nine;
+
+plusNat : Nat → Nat → Nat;
+plusNat zero n ≔ n;
+plusNat (suc m) n ≔ suc (plusNat m n);
+
+natToInt : Nat → Int;
+natToInt zero ≔ 0;
+natToInt (suc n) ≔ 1 + (natToInt n);
+
+natToStr : Nat → String;
+natToStr n ≔ intToStr (natToInt n);
+
+infix 4 <Nat;
+<Nat : Nat → Nat → Bool;
+<Nat zero _ ≔ true;
+<Nat _ zero ≔ false;
+<Nat (suc m) (suc n) ≔ m <Nat n;
+
+infix 4 >Nat;
+>Nat : Nat → Nat → Bool;
+>Nat _ zero ≔ true;
+>Nat zero _ ≔ false;
+>Nat (suc m) (suc n) ≔ m >Nat n;
+
+infix 4 <=Nat;
+<=Nat : Nat → Nat → Bool;
+<=Nat l r ≔ (l <Nat r) || (==Nat l r);
+
+infix 4 >=Nat;
+>=Nat : Nat → Nat → Bool;
+>=Nat l r ≔ (l >Nat r) || (==Nat l r);
+
+foreign c {
+  void* natInd(int n, void* a1, minijuvix_function_t* a2) {
+    if (n <= 0) return a1;
+    return ((void* (*) (minijuvix_function_t*, void*))a2->fun)(a2, natInd(n - 1, a1, a2));
+  \}
+};
+
+axiom natInd : Int → Nat → (Nat → Nat) → Nat;
+compile natInd {
+  c ↦ "natInd";
+};
+
+from-backendNat : Int → Nat;
+from-backendNat bb ≔ natInd bb zero suc;
+
+end;

examples/milestone/Lib/Data/Pair.mjuvix

@@ -6,4 +6,7 @@ inductive × (A : Type) (B : Type) {
   , : A → B → A × B;
 };
 
+fst : {A : Type} → {B : Type} → A × B → A;
+fst (a , _) ≔ a;
+
 end;

examples/milestone/Lib/Data/String.mjuvix

@@ -25,4 +25,16 @@ infix 4 ==String;
 ==String : String → String → Bool;
 ==String s1 s2 ≔ from-backend-bool (eqString s1 s2);
 
+boolToStr : Bool → String;
+boolToStr true ≔ "true";
+boolToStr false ≔ "false";
+
+infixr 5 ++;
+axiom ++ : String → String → String;
+
+compile ++ {
+  c ↦ "concat";
+};
+
+
 end;

examples/milestone/Lib/Prelude.mjuvix

@@ -0,0 +1,37 @@
+module Prelude;
+
+import Data.Bool;
+import Data.Int;
+import Data.Nat;
+import Data.String;
+import Data.List;
+import Data.Maybe;
+import Data.Pair;
+import System.IO;
+
+open Data.Bool public;
+open Data.Int public;
+open Data.Nat public;
+open Data.String public;
+open Data.List public;
+open Data.Maybe public;
+open Data.Pair public;
+open System.IO public;
+
+--------------------------------------------------------------------------------
+-- Functions
+--------------------------------------------------------------------------------
+
+axiom int-to-str : Int → String;
+
+compile int-to-str {
+  c ↦ "intToStr";
+};
+
+const : (A : Type) → (B : Type) → A → B → A;
+const _ _ a _ ≔ a;
+
+id : {A : Type} → A → A;
+id a ≔ a;
+
+end;

examples/milestone/Lib/System/IO.mjuvix

@@ -41,4 +41,10 @@ show-result : Bool → String;
 show-result true ≔ "OK";
 show-result false ≔ "FAIL";
 
+axiom readline : String;
+
+compile readline {
+  c ↦ "readline()";
+};
+
 end;

examples/milestone/MiniTicTacToe/Data

@@ -0,0 +1 @@
+../Lib/Data

examples/milestone/MiniTicTacToe/MiniTicTacToe.mjuvix

@@ -0,0 +1,191 @@
+module MiniTicTacToe;
+
+import Prelude;
+open Prelude;
+
+--------------------------------------------------------------------------------
+-- Render Utils
+--------------------------------------------------------------------------------
+
+concat : List String → String;
+concat ≔ foldl (++) "";
+
+surround : String → List String → List String;
+surround x xs ≔ concatList (x ∷ intersperse x xs) (x ∷ nil);
+
+intercalate : String → List String → String;
+intercalate sep xs ≔ concat (intersperse sep xs);
+
+unlines : List String → String;
+unlines ≔ intercalate "\n";
+
+--------------------------------------------------------------------------------
+-- Symbol
+--------------------------------------------------------------------------------
+
+inductive Symbol {
+  O : Symbol;
+  X : Symbol;
+};
+
+==Symbol : Symbol → Symbol → Bool;
+==Symbol O O ≔ true;
+==Symbol X X ≔ true;
+==Symbol _ _ ≔ false;
+
+switch : Symbol → Symbol;
+switch O ≔ X;
+switch X ≔ O;
+
+showSymbol : Symbol → String;
+showSymbol O ≔ "O";
+showSymbol X ≔ "X";
+
+--------------------------------------------------------------------------------
+-- Square
+--------------------------------------------------------------------------------
+
+inductive Square {
+  empty : Nat → Square;
+  occupied : Symbol → Square;
+};
+
+==Square : Square → Square → Bool;
+==Square (empty m) (empty n) ≔ ==Nat m n;
+==Square (occupied s) (occupied t) ≔ ==Symbol s t;
+==Square _ _ ≔ false;
+
+showSquare : Square → String;
+showSquare (empty n) ≔ " " ++ natToStr n ++ " ";
+showSquare (occupied s) ≔ " " ++ showSymbol s ++ " ";
+
+--------------------------------------------------------------------------------
+-- Board
+--------------------------------------------------------------------------------
+
+inductive Board {
+  board : List (List Square) → Board;
+};
+
+possibleMoves : List Square → List Nat;
+possibleMoves nil ≔ nil;
+possibleMoves ((empty n) ∷ xs) ≔ n ∷ possibleMoves xs;
+possibleMoves (_ ∷ xs) ≔ possibleMoves xs;
+
+full : List Square → Bool;
+full (a ∷ b ∷ c ∷ nil) ≔ (==Square a b) && (==Square b c);
+
+diagonals : List (List Square) → List (List Square);
+diagonals ((a1 ∷ _ ∷ b1 ∷ nil) ∷ (_ ∷ c ∷ _ ∷ nil) ∷ (b2 ∷ _ ∷ a2 ∷ nil) ∷ nil) ≔ (a1 ∷ c ∷ a2 ∷ nil) ∷ (b1 ∷ c ∷ b2 ∷ nil) ∷ nil;
+
+columns : List (List Square) → List (List Square);
+columns ≔ transpose;
+
+rows : List (List Square) → List (List Square);
+rows ≔ id;
+
+showRow : List Square → String;
+showRow xs ≔ concat (surround "|" (map showSquare xs));
+
+showBoard : Board → String;
+showBoard (board squares) ≔ unlines (surround "+---+---+---+" (map showRow squares));
+
+--------------------------------------------------------------------------------
+-- Error
+--------------------------------------------------------------------------------
+
+inductive Error {
+  noError : Error;
+  continue : String → Error;
+  terminate : String → Error;
+};
+
+--------------------------------------------------------------------------------
+-- GameState
+--------------------------------------------------------------------------------
+
+inductive GameState {
+  state : Board → Symbol → Error → GameState;
+};
+
+showGameState : GameState → String;
+showGameState (state b _ _) ≔ showBoard b;
+
+player : GameState → Symbol;
+player (state _ p _) ≔ p;
+
+beginState : GameState;
+beginState ≔ state
+     (board (map (map empty) ((one ∷ two ∷ three ∷ nil) ∷ (four ∷ five ∷ six ∷ nil) ∷ (seven ∷ eight ∷ nine ∷ nil) ∷ nil)))
+     X
+     noError;
+
+won : GameState → Bool;
+won (state (board squares) _ _) ≔ any full (concatList (diagonals squares) (concatList (rows squares) (columns squares)));
+
+draw : GameState → Bool;
+draw (state (board squares) _ _) ≔ null (possibleMoves (flatten squares));
+
+--------------------------------------------------------------------------------
+-- Move
+--------------------------------------------------------------------------------
+
+replace : Symbol → Nat → Square → Square;
+replace player k (empty n) ≔ if (==Nat n k) (occupied player) (empty n);
+replace _ _ s ≔ s;
+
+checkState : GameState → GameState;
+checkState (state b p e) ≔
+  if (won (state b p e))
+     (state b p (terminate ("Player " ++ (showSymbol (switch p)) ++ " wins!")))
+     (if (draw (state b p e))
+         (state b p (terminate "It's a draw!"))
+         (state b p e));
+
+playMove : Maybe Nat → GameState → GameState;
+playMove nothing (state b p _) ≔
+    state b p (continue "\nInvalid number, try again\n");
+playMove (just k) (state (board s) player e) ≔
+    if (not (elem ==Nat k (possibleMoves (flatten s))))
+        (state (board s) player (continue "\nThe square is already occupied, try again\n"))
+        (checkState (state (board (map (map (replace player k)) s))
+                           (switch player)
+                           noError));
+
+--------------------------------------------------------------------------------
+-- IO
+--------------------------------------------------------------------------------
+
+axiom parsePositiveInt : String → Int;
+
+compile parsePositiveInt {
+  c ↦ "parsePositiveInt";
+};
+
+positiveInt : Int → Maybe Int;
+positiveInt i ≔ if (i < 0) nothing (just i);
+
+validMove : Nat → Maybe Nat;
+validMove n ≔ if ((n <=Nat nine) && (n >=Nat one)) (just n) nothing;
+
+getMove : Maybe Nat;
+getMove ≔ bindMaybe validMove (fmapMaybe from-backendNat (positiveInt (parsePositiveInt (readline))));
+
+do : Action × GameState -> GameState;
+do (_ , s) ≔ playMove getMove s;
+
+prompt : GameState → String;
+prompt x ≔ "\n" ++ (showGameState x) ++ "\nPlayer " ++ showSymbol (player x) ++ ": ";
+
+terminating
+run : (Action × GameState → GameState) → GameState → Action;
+run _ (state b p (terminate msg)) ≔ putStrLn ("\n" ++ (showGameState (state b p noError)) ++ "\n" ++ msg);
+run f (state b p (continue msg)) ≔ run f (f (putStr (msg ++ prompt (state b p noError)) , state b p noError));
+run f x ≔ run f (f (putStr (prompt x) , x));
+
+welcome : String;
+welcome ≔ "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";
+
+main : Action;
+main ≔ putStrLn welcome >> run do beginState;
+end;

examples/milestone/MiniTicTacToe/Prelude.mjuvix

@@ -0,0 +1 @@
+../Lib/Prelude.mjuvix

examples/milestone/MiniTicTacToe/System

@@ -0,0 +1 @@
+../Lib/System

examples/milestone/ValidityPredicates/Data

@@ -0,0 +1 @@
+../Lib/Data

examples/milestone/ValidityPredicates/Data/List.mjuvix

@@ -1,20 +0,0 @@
-module Data.List;
-
-import Data.Bool;
-open Data.Bool;
-
-infixr 5 ∷;
-inductive 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;
-
-end;

examples/milestone/ValidityPredicates/Prelude.mjuvix

@@ -1,29 +0,0 @@
-module Prelude;
-
-import Data.Bool;
-import Data.Int;
-import Data.String;
-import Data.List;
-import Data.Maybe;
-import Data.Pair;
-import System.IO;
-
-open Data.Bool public;
-open Data.Int public;
-open Data.String public;
-open Data.List public;
-open Data.Maybe public;
-open Data.Pair public;
-open System.IO public;
-
---------------------------------------------------------------------------------
--- Functions
---------------------------------------------------------------------------------
-
-const : (A : Type) → (B : Type) → A → B → A;
-const _ _ a _ ≔ a;
-
-id : {A : Type} → A → A;
-id a ≔ a;
-
-end;

examples/milestone/ValidityPredicates/Prelude.mjuvix

@@ -0,0 +1 @@
+../Lib/Prelude.mjuvix

examples/milestone/ValidityPredicates/System

@@ -0,0 +1 @@
+../Lib/System

minic-runtime/libc/minic-runtime.h

@@ -3,6 +3,7 @@
 
 #include <stdlib.h>
 #include <stdio.h>
+#include <string.h>
 
 typedef __UINTPTR_TYPE__ uintptr_t;
 
@@ -17,12 +18,76 @@ char* intToStr(int i) {
     return str;
 }
 
+char* concat(const char* s1, const char* s2) {
+    const size_t len1 = strlen(s1);
+    const size_t len2 = strlen(s2);
+    int i,j=0,count=0;
+    char* result = (char*)malloc(len1 + len2 + 1);
+
+    for(i=0; i < len1; i++) {
+        result[i] = s1[i];
+        count++;
+    }
+
+    for(i=count; j < len2; i++) {
+        result[i] = s2[j];
+        j++;
+    }
+
+    result[len1 + len2] = '\0';
+    return result;
+}
+
+// Tries to parse str as a positive integer.
+// Returns -1 if parsing fails.
+int parsePositiveInt(char *str) {
+    int result = 0;
+    char* p = str;
+    size_t len = strlen(str);
+    while ((*str >= '0') && (*str <= '9'))
+    {
+        result = (result * 10) + ((*str) - '0');
+        str++;
+    }
+    if (str - p != len) return -1;
+    return result;
+}
+
+char* readline() {
+    int i = 0, bytesAlloced = 64;
+    char* buffer = (char*) malloc(bytesAlloced);
+    int bufferSize = bytesAlloced;
+
+    for (;;++i) {
+        int ch;
+
+        if (i == bufferSize - 1) {
+            bytesAlloced += bytesAlloced;
+            buffer = (char*) realloc(buffer, bytesAlloced);
+            bufferSize = bytesAlloced;
+        }
+
+        ch = getchar();
+        if (ch == -1) {
+            free(buffer);
+            return 0;
+        }
+        if (ch == '\n') break;
+        buffer[i] = ch;
+    }
+
+    buffer[i] = '\0';
+    return buffer;
+}
+
 int putStr(const char* str) {
-    return fputs(str, stdout);
+    fputs(str, stdout);
+    return fflush(stdout);
 }
 
 int putStrLn(const char* str) {
-    return puts(str);
+    puts(str);
+    return fflush(stdout);
 }
 
 #endif // MINIC_RUNTIME_H_

minic-runtime/standalone/minic-runtime.h

@@ -18,6 +18,24 @@ typedef struct minijuvix_function {
 void *malloc(size_t size);
 void free(void *p);
 
+void* memcpy(void *dest, const void *src, size_t n) {
+    char *csrc = (char*) src;
+    char *cdest = (char*) dest;
+
+    for (int i=0; i < n; i++) {
+        cdest[i] = csrc[i];
+    }
+    return dest;
+}
+
+void* realloc(void *ptr, size_t n) {
+    void* newptr;
+    newptr = malloc(n);
+    memcpy(newptr, ptr, n);
+    free(ptr);
+    return newptr;
+}
+
 /**
  * WASI Definitions
  */
@@ -33,6 +51,12 @@ uint16_t fd_write(uint32_t fd, Ciovec_t *iovs_ptr, uint32_t iovs_len, uint32_t *
                 __import_name__("fd_write"),
                    ));
 
+uint16_t fd_read(uint32_t fd, Ciovec_t *iovs_ptr, uint32_t iovs_len, uint32_t *read)
+    __attribute__((
+                __import_module__("wasi_snapshot_preview1"),
+                __import_name__("fd_read"),
+                   ));
+
 _Noreturn void proc_exit(uint32_t rval)
     __attribute__((
                 __import_module__("wasi_snapshot_preview1"),
@@ -127,9 +151,30 @@ char* intToStr(int i) {
     return buf;
 }
 
+int strToInt(char *str)
+{
+  int result;
+  int puiss;
+
+  result = 0;
+  puiss = 1;
+  while (('-' == (*str)) || ((*str) == '+'))
+  {
+      if (*str == '-')
+        puiss = puiss * -1;
+      str++;
+  }
+  while ((*str >= '0') && (*str <= '9'))
+  {
+      result = (result * 10) + ((*str) - '0');
+      str++;
+  }
+  return (result * puiss);
+}
+
 int putStr(const char* str) {
     size_t n = strlen(str);
-    Ciovec_t vec = {.buf = (uint8_t*)str, .buf_len=n};
+    Ciovec_t vec = {.buf = (uint8_t*)str, .buf_len=(uint32_t)n};
     return fd_write(1, &vec, 1, 0);
 }
 
@@ -137,5 +182,74 @@ int putStrLn(const char* str) {
     return putStr(str) || putStr("\n");
 }
 
+// Tries to parse str as a positive integer.
+// Returns -1 if parsing fails.
+int parsePositiveInt(char *str) {
+    int result = 0;
+    char* p = str;
+    size_t len = strlen(str);
+    while ((*str >= '0') && (*str <= '9'))
+    {
+        result = (result * 10) + ((*str) - '0');
+        str++;
+    }
+    if (str - p != len) return -1;
+    return result;
+}
+
+
+char* concat(const char* s1, const char* s2) {
+    const size_t len1 = strlen(s1);
+    const size_t len2 = strlen(s2);
+    int i,j=0,count=0;
+    char* result = (char*)malloc(len1 + len2 + 1);
+
+    for(i=0; i < len1; i++) {
+        result[i] = s1[i];
+        count++;
+    }
+
+    for(i=count; j < len2; i++) {
+        result[i] = s2[j];
+        j++;
+    }
+
+    result[len1 + len2] = '\0';
+    return result;
+}
+
+int getchar() {
+    int ch;
+    Ciovec_t v = {.buf = (uint8_t*) &ch, .buf_len=1};
+    if (fd_read(0, &v, 1, 0) != 0) return -1;
+    return ch;
+}
+
+char* readline() {
+    int i = 0, bytesAlloced = 64;
+    char* buffer = (char*) malloc(bytesAlloced);
+    int bufferSize = bytesAlloced;
+
+    for (;;++i) {
+        int ch;
+
+        if (i == bufferSize - 1) {
+            bytesAlloced += bytesAlloced;
+            buffer = (char*) realloc(buffer, bytesAlloced);
+            bufferSize = bytesAlloced;
+        }
+
+        ch = getchar();
+        if (ch == -1) {
+            free(buffer);
+            return 0;
+        }
+        if (ch == '\n') break;
+        buffer[i] = ch;
+    }
+
+    buffer[i] = '\0';
+    return buffer;
+}
 
 #endif // MINIC_RUNTIME_H_

src/MiniJuvix/Syntax/MicroJuvix/Language.hs

@@ -134,9 +134,15 @@ data TypeApplication = TypeApplication
     _typeAppRight :: Type,
     _typeAppImplicit :: IsImplicit
   }
-  deriving stock (Generic, Eq)
 
-instance Hashable TypeApplication
+-- TODO: Eq and Hashable instances ignore the _typAppImplicit field
+--  to workaround a crash in Micro->Mono translation when looking up
+-- a concrete type.
+instance Eq TypeApplication where
+  (TypeApplication l r _) == (TypeApplication l' r' _) = (l == l') && (r == r')
+
+instance Hashable TypeApplication where
+  hashWithSalt salt TypeApplication {..} = hashWithSalt salt (_typeAppLeft, _typeAppRight)
 
 data TypeAbstraction = TypeAbstraction
   { _typeAbsVar :: VarName,

src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs

@@ -451,3 +451,20 @@ getTypeName = \case
   (TypeIden (TypeIdenInductive tyName)) -> Just tyName
   (TypeApp (TypeApplication l _ _)) -> getTypeName l
   _ -> Nothing
+
+reachableModules :: Module -> [Module]
+reachableModules = fst . run . runOutputList . evalState (mempty :: HashSet Name) . go
+  where
+    go :: forall r. Members '[State (HashSet Name), Output Module] r => Module -> Sem r ()
+    go m = do
+      s <- get
+      unless
+        (HashSet.member (m ^. moduleName) s)
+        (output m >> goBody (m ^. moduleBody))
+      where
+        goBody :: ModuleBody -> Sem r ()
+        goBody = mapM_ goStatement . (^. moduleStatements)
+        goStatement :: Statement -> Sem r ()
+        goStatement = \case
+          StatementInclude (Include inc) -> go inc
+          _ -> return ()

src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs

@@ -10,6 +10,7 @@ import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
 import MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi qualified as Ansi
 import MiniJuvix.Syntax.MicroJuvix.Pretty.Base
 import MiniJuvix.Syntax.MicroJuvix.Pretty.Options
+import Prettyprinter.Render.Terminal qualified as Ansi
 
 newtype PPOutput = PPOutput (Doc Ann)
 
@@ -19,6 +20,9 @@ ppOutDefault = AnsiText . PPOutput . doc defaultOptions
 ppOut :: PrettyCode c => Options -> c -> AnsiText
 ppOut o = AnsiText . PPOutput . doc o
 
+ppSimple :: PrettyCode c => c -> Text
+ppSimple = Ansi.renderStrict . reAnnotateS Ansi.stylize . layoutPretty defaultLayoutOptions . doc defaultOptions
+
 instance HasAnsiBackend PPOutput where
   toAnsiStream (PPOutput o) = reAnnotateS Ansi.stylize (layoutPretty defaultLayoutOptions o)
   toAnsiDoc (PPOutput o) = reAnnotate Ansi.stylize o

src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs

@@ -381,3 +381,11 @@ ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -
 ppCodeAtom c = do
   p' <- ppCode c
   return $ if isAtomic c then p' else parens p'
+
+instance PrettyCode a => PrettyCode (NonEmpty a) where
+  ppCode x = do
+    cs <- mapM ppCode (toList x)
+    return $ encloseSep "(" ")" ", " cs
+
+instance PrettyCode ConcreteType where
+  ppCode ConcreteType {..} = ppCode _unconcreteType

src/MiniJuvix/Syntax/MiniC/Language.hs

@@ -122,6 +122,12 @@ data CDeclType = CDeclType
   }
   deriving stock (Show, Eq)
 
+data CFunType = CFunType
+  { _cFunArgTypes :: [CDeclType],
+    _cFunReturnType :: CDeclType
+  }
+  deriving stock (Show, Eq)
+
 uIntPtrType :: DeclType
 uIntPtrType = DeclTypeDefType "uintptr_t"
 
@@ -161,6 +167,15 @@ castToType cDecl e =
         }
     )
 
+cDeclToNamedDecl :: Text -> CDeclType -> Declaration
+cDeclToNamedDecl name CDeclType {..} =
+  Declaration
+    { _declType = _typeDeclType,
+      _declIsPtr = _typeIsPtr,
+      _declName = Just name,
+      _declInitializer = Nothing
+    }
+
 cDeclToDecl :: CDeclType -> Declaration
 cDeclToDecl CDeclType {..} =
   Declaration
@@ -267,6 +282,15 @@ typeDefType typName declName =
       _declInitializer = Nothing
     }
 
+namedDeclType :: Text -> DeclType -> Declaration
+namedDeclType name typ =
+  Declaration
+    { _declType = typ,
+      _declIsPtr = False,
+      _declName = Just name,
+      _declInitializer = Nothing
+    }
+
 equals :: Expression -> Expression -> Expression
 equals e1 e2 =
   ExpressionBinary
@@ -319,3 +343,4 @@ makeLenses ''Declaration
 makeLenses ''CDeclType
 makeLenses ''FunctionSig
 makeLenses ''Function
+makeLenses ''CFunType

src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs

@@ -9,8 +9,9 @@ data ConstructorInfo = ConstructorInfo
     _constructorInfoInductive :: InductiveName
   }
 
-newtype FunctionInfo = FunctionInfo
-  { _functionInfoType :: Type
+data FunctionInfo = FunctionInfo
+  { _functionInfoType :: Type,
+    _functionInfoPatterns :: Int
   }
 
 newtype AxiomInfo = AxiomInfo
@@ -38,7 +39,7 @@ buildTable m = InfoTable {..}
     _infoFunctions :: HashMap Name FunctionInfo
     _infoFunctions =
       HashMap.fromList
-        [ (f ^. funDefName, FunctionInfo (f ^. funDefType))
+        [ (f ^. funDefName, FunctionInfo (f ^. funDefType) (length (head (f ^. funDefClauses) ^. clausePatterns)))
           | StatementFunction f <- ss
         ]
     _infoAxioms :: HashMap Name AxiomInfo

src/MiniJuvix/Translation/MicroJuvixToMonoJuvix/TypePropagation.hs

@@ -12,10 +12,15 @@ collectTypeCalls res = run (execState emptyCalls (runReader typesTable (runReade
     goTopLevel :: Members '[State TypeCalls, Reader TypeCallsMap, Reader InfoTable] r => Sem r ()
     goTopLevel = mapM_ goConcreteFun entries
       where
-        -- the list of functions defined in the Main module with concrete types.
+        allModules :: [Module]
+        allModules = reachableModules main
+        -- the list of functions defined in any module with concrete types.
         entries :: [FunctionDef]
         entries =
-          [ f | StatementFunction f <- main ^. moduleBody . moduleStatements, hasConcreteType f
+          [ f
+            | m <- allModules,
+              StatementFunction f <- m ^. moduleBody . moduleStatements,
+              hasConcreteType f
           ]
           where
             hasConcreteType :: FunctionDef -> Bool

src/MiniJuvix/Translation/MonoJuvixToMiniC.hs

@@ -1,7 +1,10 @@
-module MiniJuvix.Translation.MonoJuvixToMiniC where
+module MiniJuvix.Translation.MonoJuvixToMiniC
+  ( module MiniJuvix.Translation.MonoJuvixToMiniC,
+    module MiniJuvix.Translation.MonoJuvixToMiniC.Types,
+  )
+where
 
 import Data.HashMap.Strict qualified as HashMap
-import Data.Text qualified as T
 import MiniJuvix.Internal.Strings qualified as Str
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Backends
@@ -13,37 +16,9 @@ import MiniJuvix.Syntax.MiniC.Serialization
 import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
 import MiniJuvix.Syntax.NameId
 import MiniJuvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
-
-newtype MiniCResult = MiniCResult
-  { _resultCCode :: Text
-  }
-
-data CFunType = CFunType
-  { _cFunArgTypes :: [CDeclType],
-    _cFunReturnType :: CDeclType
-  }
-  deriving stock (Show, Eq)
-
-data BindingInfo = BindingInfo
-  { _bindingInfoExpr :: Expression,
-    _bindingInfoType :: CFunType
-  }
-
-newtype PatternInfoTable = PatternInfoTable
-  {_patternBindings :: HashMap Text BindingInfo}
-
-data ClosureInfo = ClosureInfo
-  { _closureNameId :: Mono.NameId,
-    _closureRootName :: Text,
-    _closureFunType :: CFunType
-  }
-  deriving stock (Show, Eq)
-
-makeLenses ''MiniCResult
-makeLenses ''CFunType
-makeLenses ''PatternInfoTable
-makeLenses ''BindingInfo
-makeLenses ''ClosureInfo
+import MiniJuvix.Translation.MonoJuvixToMiniC.Base
+import MiniJuvix.Translation.MonoJuvixToMiniC.Closure
+import MiniJuvix.Translation.MonoJuvixToMiniC.Types
 
 entryMiniC :: Mono.MonoJuvixResult -> Sem r MiniCResult
 entryMiniC i = return (MiniCResult (serialize cunitResult))
@@ -69,53 +44,47 @@ entryMiniC i = return (MiniCResult (serialize cunitResult))
     cmodules = do
       m <- toList (i ^. Mono.resultModules)
       let buildTable = Mono.buildTable m
-      run (runReader compileInfo (genCTypes m))
+      genStructDefs m
+        <> run (runReader compileInfo (genAxioms m))
+        <> genCTypes m
         <> genFunctionSigs m
         <> run (runReader buildTable (genClosures m))
         <> run (runReader buildTable (genFunctionDefs m))
 
-unsupported :: Text -> a
-unsupported msg = error (msg <> " Mono to C: not yet supported")
+genStructDefs :: Mono.Module -> [CCode]
+genStructDefs Mono.Module {..} =
+  concatMap go (_moduleBody ^. Mono.moduleStatements)
+  where
+    go :: Mono.Statement -> [CCode]
+    go = \case
+      Mono.StatementInductive d -> mkInductiveTypeDef d
+      _ -> []
 
-genCTypes :: forall r. Members '[Reader Mono.CompileInfoTable] r => Mono.Module -> Sem r [CCode]
-genCTypes Mono.Module {..} =
+genAxioms :: forall r. Members '[Reader Mono.CompileInfoTable] r => Mono.Module -> Sem r [CCode]
+genAxioms Mono.Module {..} =
   concatMapM go (_moduleBody ^. Mono.moduleStatements)
   where
     go :: Mono.Statement -> Sem r [CCode]
     go = \case
-      Mono.StatementInductive d -> return (goInductiveDef d)
+      Mono.StatementInductive {} -> return []
       Mono.StatementAxiom d -> goAxiom d
-      Mono.StatementForeign d -> return (goForeign d)
+      Mono.StatementForeign {} -> return []
       Mono.StatementFunction {} -> return []
 
-genFunctionSigs :: Mono.Module -> [CCode]
-genFunctionSigs Mono.Module {..} =
-  go =<< _moduleBody ^. Mono.moduleStatements
+genCTypes :: Mono.Module -> [CCode]
+genCTypes Mono.Module {..} =
+  concatMap go (_moduleBody ^. Mono.moduleStatements)
   where
     go :: Mono.Statement -> [CCode]
     go = \case
-      Mono.StatementFunction d -> genFunctionSig d
-      Mono.StatementForeign {} -> []
+      Mono.StatementInductive d -> goInductiveDef d
       Mono.StatementAxiom {} -> []
-      Mono.StatementInductive {} -> []
+      Mono.StatementForeign d -> goForeign d
+      Mono.StatementFunction {} -> []
 
-genClosures ::
-  forall r.
-  Member (Reader Mono.InfoTable) r =>
-  Mono.Module ->
-  Sem r [CCode]
-genClosures Mono.Module {..} = do
-  closureInfos <- concatMapM go (_moduleBody ^. Mono.moduleStatements)
-  let cs :: [Function] = genClosure =<< nub closureInfos
-      ecs :: [CCode] = ExternalFunc <$> cs
-  return ecs
-  where
-    go :: Mono.Statement -> Sem r [ClosureInfo]
-    go = \case
-      Mono.StatementFunction d -> functionDefClosures d
-      Mono.StatementForeign {} -> return []
-      Mono.StatementAxiom {} -> return []
-      Mono.StatementInductive {} -> return []
+genFunctionSigs :: Mono.Module -> [CCode]
+genFunctionSigs Mono.Module {..} =
+  applyOnFunStatement genFunctionSig =<< _moduleBody ^. Mono.moduleStatements
 
 genFunctionDefs ::
   Members '[Reader Mono.InfoTable] r =>
@@ -128,124 +97,77 @@ genFunctionDefsBody ::
   Mono.ModuleBody ->
   Sem r [CCode]
 genFunctionDefsBody Mono.ModuleBody {..} =
-  concatMapM genFunctionDefsStatement _moduleStatements
-
-genFunctionDefsStatement ::
-  Members '[Reader Mono.InfoTable] r =>
-  Mono.Statement ->
-  Sem r [CCode]
-genFunctionDefsStatement = \case
-  Mono.StatementFunction d -> goFunctionDef d
-  Mono.StatementForeign {} -> return []
-  Mono.StatementAxiom {} -> return []
-  Mono.StatementInductive {} -> return []
-
-asStruct :: Text -> Text
-asStruct n = n <> "_s"
-
-asTypeDef :: Text -> Text
-asTypeDef n = n <> "_t"
-
-asTag :: Text -> Text
-asTag n = n <> "_tag"
-
-asField :: Text -> Text
-asField n = n <> "_field"
-
-asNullary :: Text -> Text
-asNullary n = n <> "_nullary"
-
-asCast :: Text -> Text
-asCast n = "as_" <> n
-
-asIs :: Text -> Text
-asIs n = "is_" <> n
-
-asNew :: Text -> Text
-asNew n = "new_" <> n
-
-asFun :: Text -> Text
-asFun n = n <> "_fun"
-
-asFunArg :: Text -> Text
-asFunArg n = "fa" <> n
-
-asCtorArg :: Text -> Text
-asCtorArg n = "ca" <> n
-
-mkArgs :: (Text -> Text) -> [Text]
-mkArgs f = map (f . show) [0 :: Integer ..]
-
-funArgs :: [Text]
-funArgs = mkArgs asFunArg
-
-ctorArgs :: [Text]
-ctorArgs = mkArgs asCtorArg
-
-mkName :: Mono.Name -> Text
-mkName n =
-  adaptFirstLetter lexeme <> nameTextSuffix
-  where
-    lexeme
-      | T.null lexeme' = "v"
-      | otherwise = lexeme'
-      where
-        lexeme' = T.filter isValidChar (n ^. Mono.nameText)
-    isValidChar :: Char -> Bool
-    isValidChar c = isLetter c && isAscii c
-    adaptFirstLetter :: Text -> Text
-    adaptFirstLetter t = case T.uncons t of
-      Nothing -> impossible
-      Just (h, r) -> T.cons (capitalize h) r
-      where
-        capitalize :: Char -> Char
-        capitalize
-          | capital = toUpper
-          | otherwise = toLower
-        capital = case n ^. Mono.nameKind of
-          Mono.KNameConstructor -> True
-          Mono.KNameInductive -> True
-          Mono.KNameTopModule -> True
-          Mono.KNameLocalModule -> True
-          _ -> False
-    nameTextSuffix :: Text
-    nameTextSuffix = case n ^. Mono.nameKind of
-      Mono.KNameTopModule -> mempty
-      Mono.KNameFunction ->
-        if n ^. Mono.nameText == Str.main then mempty else idSuffix
-      _ -> idSuffix
-    idSuffix :: Text
-    idSuffix = "_" <> show (n ^. Mono.nameId . unNameId)
+  concatMapM (applyOnFunStatement goFunctionDef) _moduleStatements
 
 isNullary :: Text -> CFunType -> Bool
 isNullary funName funType = null (funType ^. cFunArgTypes) && funName /= Str.main_
 
-cFunTypeToFunSig :: Text -> CFunType -> FunctionSig
-cFunTypeToFunSig name CFunType {..} =
-  FunctionSig
-    { _funcReturnType = _cFunReturnType ^. typeDeclType,
-      _funcIsPtr = _cFunReturnType ^. typeIsPtr,
-      _funcQualifier = None,
-      _funcName = name,
-      _funcArgs = namedArgs asFunArg _cFunArgTypes
+mkFunctionSig :: Mono.FunctionDef -> FunctionSig
+mkFunctionSig Mono.FunctionDef {..} =
+  cFunTypeToFunSig funName funType
+  where
+    -- Assumption: All clauses have the same number of patterns
+    nPatterns :: Int
+    nPatterns = length (head _funDefClauses ^. Mono.clausePatterns)
+
+    baseFunType :: CFunType
+    baseFunType = typeToFunType _funDefType
+
+    funType :: CFunType
+    funType =
+      if
+          | nPatterns == length (baseFunType ^. cFunArgTypes) -> baseFunType
+          | otherwise ->
+              CFunType
+                { _cFunArgTypes = take nPatterns (baseFunType ^. cFunArgTypes),
+                  _cFunReturnType = declFunctionPtrType
                 }
 
-genFunctionSig :: Mono.FunctionDef -> [CCode]
-genFunctionSig Mono.FunctionDef {..} =
-  [ExternalFuncSig (cFunTypeToFunSig funName funType)]
-    <> (ExternalMacro . CppDefineParens <$> toList nullaryDefine)
-  where
-    funType :: CFunType
-    funType = typeToFunType _funDefType
     funIsNullary :: Bool
     funIsNullary = isNullary funcBasename funType
+
     funcBasename :: Text
     funcBasename = mkName _funDefName
+
     funName :: Text
     funName =
       if
           | funIsNullary -> asNullary funcBasename
           | otherwise -> funcBasename
+
+genFunctionSig :: Mono.FunctionDef -> [CCode]
+genFunctionSig d@(Mono.FunctionDef {..}) =
+  [ExternalFuncSig (mkFunctionSig d)]
+    <> (ExternalMacro . CppDefineParens <$> toList nullaryDefine)
+  where
+    nPatterns :: Int
+    nPatterns = length (head _funDefClauses ^. Mono.clausePatterns)
+
+    baseFunType :: CFunType
+    baseFunType = typeToFunType _funDefType
+
+    funType :: CFunType
+    funType =
+      if
+          | nPatterns == length (baseFunType ^. cFunArgTypes) -> baseFunType
+          | otherwise ->
+              CFunType
+                { _cFunArgTypes = take nPatterns (baseFunType ^. cFunArgTypes),
+                  _cFunReturnType = declFunctionPtrType
+                }
+
+    funIsNullary :: Bool
+    funIsNullary = isNullary funcBasename funType
+
+    funcBasename :: Text
+    funcBasename = mkName _funDefName
+
+    funName :: Text
+    funName =
+      if
+          | funIsNullary -> asNullary funcBasename
+          | otherwise -> funcBasename
+
     nullaryDefine :: Maybe Define
     nullaryDefine =
       if
@@ -257,18 +179,11 @@ genFunctionSig Mono.FunctionDef {..} =
                   }
           | otherwise -> Nothing
 
-functionDefClosures ::
-  Member (Reader Mono.InfoTable) r =>
-  Mono.FunctionDef ->
-  Sem r [ClosureInfo]
-functionDefClosures Mono.FunctionDef {..} =
-  concatMapM (clauseClosures (fst (unfoldFunType _funDefType))) (toList _funDefClauses)
-
 goFunctionDef ::
   Members '[Reader Mono.InfoTable] r =>
   Mono.FunctionDef ->
   Sem r [CCode]
-goFunctionDef Mono.FunctionDef {..} = do
+goFunctionDef d@(Mono.FunctionDef {..}) = do
   fc <- mapM (goFunctionClause (fst (unfoldFunType _funDefType))) (toList _funDefClauses)
   let bodySpec = fst <$> fc
   let preDecls :: [Function] = snd =<< fc
@@ -276,7 +191,7 @@ goFunctionDef Mono.FunctionDef {..} = do
     (ExternalFunc <$> preDecls)
       <> [ ExternalFunc $
              Function
-               { _funcSig = cFunTypeToFunSig funName funType,
+               { _funcSig = mkFunctionSig d,
                  _funcBody = maybeToList (BodyStatement <$> mkBody bodySpec)
                }
          ]
@@ -300,21 +215,6 @@ goFunctionDef Mono.FunctionDef {..} = do
               )
           )
 
-    funIsNullary :: Bool
-    funIsNullary = isNullary funcBasename funType
-
-    funcBasename :: Text
-    funcBasename = mkName _funDefName
-
-    funName :: Text
-    funName =
-      if
-          | funIsNullary -> asNullary funcBasename
-          | otherwise -> funcBasename
-
-    funType :: CFunType
-    funType = typeToFunType _funDefType
-
     fallback :: Statement
     fallback =
       StatementCompound
@@ -337,21 +237,6 @@ goFunctionDef Mono.FunctionDef {..} = do
             )
         ]
 
-typeToFunType :: Mono.Type -> CFunType
-typeToFunType t =
-  let (_cFunArgTypes, _cFunReturnType) =
-        bimap (map goType) goType (unfoldFunType t)
-   in CFunType {..}
-
-clauseClosures ::
-  Members '[Reader Mono.InfoTable] r =>
-  [Mono.Type] ->
-  Mono.FunctionClause ->
-  Sem r [ClosureInfo]
-clauseClosures argTyps clause = do
-  bindings <- buildPatternInfoTable argTyps clause
-  runReader bindings (genClosureExpression (clause ^. Mono.clauseBody))
-
 goFunctionClause ::
   forall r.
   Members '[Reader Mono.InfoTable] r =>
@@ -407,153 +292,23 @@ goFunctionClause argTyps clause = do
       (decls :: [Function], clauseResult) <- runOutputList (runReader bindings (goExpression (clause ^. Mono.clauseBody)))
       return (StatementReturn (Just clauseResult), decls)
 
-genClosure :: ClosureInfo -> [Function]
-genClosure ClosureInfo {..} =
-  let returnType :: CDeclType
-      returnType = _closureFunType ^. cFunReturnType
-      argTypes :: [CDeclType]
-      argTypes = _closureFunType ^. cFunArgTypes
-      localName :: Text
-      localName = "f"
-      funName :: Text
-      funName = asFun _closureRootName
-   in [ Function
-          { _funcSig =
-              FunctionSig
-                { _funcReturnType = returnType ^. typeDeclType,
-                  _funcIsPtr = returnType ^. typeIsPtr,
-                  _funcQualifier = None,
-                  _funcName = funName,
-                  _funcArgs = namedArgs asFunArg (declFunctionPtrType : argTypes)
-                },
-            _funcBody =
-              [ returnStatement
-                  ( functionCall
-                      (ExpressionVar _closureRootName)
-                      (ExpressionVar <$> take (length argTypes) (drop 1 funArgs))
-                  )
-              ]
-          },
-        Function
-          { _funcSig =
-              FunctionSig
-                { _funcReturnType = declFunctionType,
-                  _funcIsPtr = True,
-                  _funcQualifier = None,
-                  _funcName = asNew funName,
-                  _funcArgs = []
-                },
-            _funcBody =
-              [ BodyDecl
-                  ( Declaration
-                      { _declType = declFunctionType,
-                        _declIsPtr = True,
-                        _declName = Just localName,
-                        _declInitializer = Just $ ExprInitializer (mallocSizeOf Str.minijuvixFunctionT)
-                      }
-                  ),
-                BodyStatement
-                  ( StatementExpr
-                      ( ExpressionAssign
-                          ( Assign
-                              { _assignLeft = memberAccess Pointer (ExpressionVar localName) "fun",
-                                _assignRight =
-                                  castToType
-                                    ( CDeclType
-                                        { _typeDeclType = uIntPtrType,
-                                          _typeIsPtr = False
-                                        }
-                                    )
-                                    (ExpressionVar funName)
-                              }
-                          )
-                      )
-                  ),
-                returnStatement (ExpressionVar localName)
-              ]
-          }
-      ]
-
-genClosureExpression ::
-  forall r.
-  Members '[Reader Mono.InfoTable, Reader PatternInfoTable] r =>
-  Mono.Expression ->
-  Sem r [ClosureInfo]
-genClosureExpression = \case
-  Mono.ExpressionIden i -> do
-    let rootFunMonoName = Mono.getName i
-        rootFunNameId = rootFunMonoName ^. Mono.nameId
-        rootFunName = mkName rootFunMonoName
-    case i of
-      Mono.IdenVar {} -> return []
-      _ -> do
-        t <- getType i
-        let argTyps = t ^. cFunArgTypes
-        if
-            | null argTyps -> return []
-            | otherwise ->
-                return
-                  [ ClosureInfo
-                      { _closureNameId = rootFunNameId,
-                        _closureRootName = rootFunName,
-                        _closureFunType = t
-                      }
-                  ]
-  Mono.ExpressionApplication a -> exprApplication a
-  Mono.ExpressionLiteral {} -> return []
-  where
-    exprApplication :: Mono.Application -> Sem r [ClosureInfo]
-    exprApplication Mono.Application {..} = case _appLeft of
-      Mono.ExpressionApplication x -> do
-        rightClosures <- genClosureExpression _appRight
-        uf <- exprApplication x
-        return (rightClosures <> uf)
-      Mono.ExpressionIden {} -> genClosureExpression _appRight
-      Mono.ExpressionLiteral {} -> impossible
-
 goExpression :: Members '[Reader Mono.InfoTable, Reader PatternInfoTable] r => Mono.Expression -> Sem r Expression
 goExpression = \case
   Mono.ExpressionIden i -> do
     let rootFunMonoName = Mono.getName i
         rootFunName = mkName rootFunMonoName
-        funName = asFun rootFunName
-        newFunName = asNew funName
-
+        evalFunName = asEval (rootFunName <> "_0")
     case i of
       Mono.IdenVar {} -> goIden i
       _ -> do
-        t <- getType i
+        (t, _) <- getType i
         let argTyps = t ^. cFunArgTypes
         if
             | null argTyps -> goIden i
-            | otherwise -> return $ functionCall (ExpressionVar newFunName) []
+            | otherwise -> return $ functionCall (ExpressionVar evalFunName) []
   Mono.ExpressionApplication a -> goApplication a
   Mono.ExpressionLiteral l -> return (ExpressionLiteral (goLiteral l))
 
-getType ::
-  Members '[Reader Mono.InfoTable, Reader PatternInfoTable] r =>
-  Mono.Iden ->
-  Sem r CFunType
-getType = \case
-  Mono.IdenFunction n -> do
-    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoFunctions)
-    return $ typeToFunType (fInfo ^. Mono.functionInfoType)
-  Mono.IdenConstructor n -> do
-    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoConstructors)
-    return
-      ( CFunType
-          { _cFunArgTypes = goType <$> (fInfo ^. Mono.constructorInfoArgs),
-            _cFunReturnType =
-              goType
-                (Mono.TypeIden (Mono.TypeIdenInductive (fInfo ^. Mono.constructorInfoInductive)))
-          }
-      )
-  Mono.IdenAxiom n -> do
-    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoAxioms)
-    return $ typeToFunType (fInfo ^. Mono.axiomInfoType)
-  Mono.IdenVar n ->
-    (^. bindingInfoType) . HashMap.lookupDefault impossible (n ^. Mono.nameText) <$> asks (^. patternBindings)
-
 goIden :: Members '[Reader PatternInfoTable, Reader Mono.InfoTable] r => Mono.Iden -> Sem r Expression
 goIden = \case
   Mono.IdenFunction n -> return (ExpressionVar (mkName n))
@@ -570,7 +325,36 @@ goApplication a = do
     Mono.IdenVar n -> do
       BindingInfo {..} <- HashMap.lookupDefault impossible (n ^. Mono.nameText) <$> asks (^. patternBindings)
       return $ juvixFunctionCall _bindingInfoType _bindingInfoExpr (reverse fArgs)
+    Mono.IdenFunction n -> do
+      nPatterns <- (^. Mono.functionInfoPatterns) . HashMap.lookupDefault impossible n <$> asks (^. Mono.infoFunctions)
+      (idenType, _) <- getType iden
+      let nArgTyps = length (idenType ^. cFunArgTypes)
+      if
+          | length fArgs < nArgTyps -> do
+              let name = mkName (Mono.getName iden)
+                  evalName = asEval (name <> "_" <> show (length fArgs))
+              return $ functionCall (ExpressionVar evalName) (reverse fArgs)
+          | nPatterns < nArgTyps -> do
+              idenExp <- goIden iden
+              let callTyp = idenType {_cFunArgTypes = drop nPatterns (idenType ^. cFunArgTypes)}
+                  args = reverse fArgs
+                  patternArgs = take nPatterns args
+                  funCall =
+                    if
+                        | null patternArgs -> idenExp
+                        | otherwise -> functionCall idenExp patternArgs
+              return $ juvixFunctionCall callTyp funCall (drop nPatterns args)
+          | otherwise -> do
+              idenExp <- goIden iden
+              return $ functionCall idenExp (reverse fArgs)
     _ -> do
+      (idenType, _) <- getType iden
+      if
+          | (length fArgs < length (idenType ^. cFunArgTypes)) -> do
+              let name = mkName (Mono.getName iden)
+                  evalName = asEval (name <> "_" <> show (length fArgs))
+              return $ functionCall (ExpressionVar evalName) (reverse fArgs)
+          | otherwise -> do
               idenExp <- goIden iden
               return $ functionCall idenExp (reverse fArgs)
   where
@@ -620,7 +404,8 @@ goAxiom a = do
     getCode :: BackendItem -> Maybe Text
     getCode b =
       guard (BackendC == b ^. backendItemBackend)
-        $> b ^. backendItemCode
+        $> b
+        ^. backendItemCode
     lookupBackends ::
       Member (Reader Mono.CompileInfoTable) r =>
       NameId ->
@@ -638,23 +423,10 @@ mkInductiveName i = mkName (i ^. Mono.inductiveName)
 mkInductiveConstructorNames :: Mono.InductiveDef -> [Text]
 mkInductiveConstructorNames i = mkName . view Mono.constructorName <$> i ^. Mono.inductiveConstructors
 
-goInductiveDef :: Mono.InductiveDef -> [CCode]
-goInductiveDef i =
-  [ ExternalDecl structTypeDef,
-    ExternalDecl tagsType
-  ]
-    <> (i ^. Mono.inductiveConstructors >>= goInductiveConstructorDef)
-    <> [ExternalDecl inductiveDecl]
-    <> (i ^. Mono.inductiveConstructors >>= goInductiveConstructorNew i)
-    <> (ExternalFunc . isFunction <$> constructorNames)
-    <> (ExternalFunc . asFunction <$> constructorNames)
+mkInductiveTypeDef :: Mono.InductiveDef -> [CCode]
+mkInductiveTypeDef i =
+  [ExternalDecl structTypeDef]
   where
-    baseName :: Text
-    baseName = mkName (i ^. Mono.inductiveName)
-
-    constructorNames :: [Text]
-    constructorNames = mkInductiveConstructorNames i
-
     structTypeDef :: Declaration
     structTypeDef =
       typeDefWrap
@@ -668,6 +440,25 @@ goInductiveDef i =
             )
         )
 
+    baseName :: Text
+    baseName = mkName (i ^. Mono.inductiveName)
+
+goInductiveDef :: Mono.InductiveDef -> [CCode]
+goInductiveDef i =
+  [ ExternalDecl tagsType
+  ]
+    <> (i ^. Mono.inductiveConstructors >>= goInductiveConstructorDef)
+    <> [ExternalDecl inductiveDecl]
+    <> (i ^. Mono.inductiveConstructors >>= goInductiveConstructorNew i)
+    <> (ExternalFunc . isFunction <$> constructorNames)
+    <> (ExternalFunc . asFunction <$> constructorNames)
+  where
+    baseName :: Text
+    baseName = mkName (i ^. Mono.inductiveName)
+
+    constructorNames :: [Text]
+    constructorNames = mkInductiveConstructorNames i
+
     tagsType :: Declaration
     tagsType =
       typeDefWrap
@@ -918,12 +709,6 @@ goInductiveConstructorNew i ctor = ctorNewFun
             )
         )
 
-namedArgs :: (Text -> Text) -> [CDeclType] -> [Declaration]
-namedArgs prefix = zipWith goTypeDecl argLabels
-  where
-    argLabels :: [Text]
-    argLabels = prefix . show <$> [0 :: Integer ..]
-
 inductiveCtorArgs :: Mono.InductiveConstructorDef -> [Declaration]
 inductiveCtorArgs ctor = namedArgs asCtorArg (goType <$> ctorParams)
   where
@@ -960,120 +745,3 @@ goInductiveConstructorDef ctor =
               _structMembers = Just (inductiveCtorArgs ctor)
             }
         )
-
--- | a -> (b -> c)  ==> ([a, b], c)
-unfoldFunType :: Mono.Type -> ([Mono.Type], Mono.Type)
-unfoldFunType t = case t of
-  Mono.TypeFunction (Mono.Function l r) -> first (l :) (unfoldFunType r)
-  _ -> ([], t)
-
-goType :: Mono.Type -> CDeclType
-goType t = case t of
-  Mono.TypeIden ti -> getMonoType ti
-  Mono.TypeFunction {} -> declFunctionPtrType
-  Mono.TypeUniverse {} -> unsupported "TypeUniverse"
-  where
-    getMonoType :: Mono.TypeIden -> CDeclType
-    getMonoType = \case
-      Mono.TypeIdenInductive mn ->
-        CDeclType
-          { _typeDeclType = DeclTypeDefType (asTypeDef (mkName mn)),
-            _typeIsPtr = True
-          }
-      Mono.TypeIdenAxiom mn ->
-        CDeclType
-          { _typeDeclType = DeclTypeDefType (mkName mn),
-            _typeIsPtr = False
-          }
-
-buildPatternInfoTable :: forall r. Member (Reader Mono.InfoTable) r => [Mono.Type] -> Mono.FunctionClause -> Sem r PatternInfoTable
-buildPatternInfoTable argTyps Mono.FunctionClause {..} =
-  PatternInfoTable . HashMap.fromList <$> patBindings
-  where
-    funArgBindings :: [(Expression, CFunType)]
-    funArgBindings = bimap ExpressionVar typeToFunType <$> zip funArgs argTyps
-
-    patArgBindings :: [(Mono.Pattern, (Expression, CFunType))]
-    patArgBindings = zip _clausePatterns funArgBindings
-
-    patBindings :: Sem r [(Text, BindingInfo)]
-    patBindings = concatMapM go patArgBindings
-
-    go :: (Mono.Pattern, (Expression, CFunType)) -> Sem r [(Text, BindingInfo)]
-    go (p, (exp, typ)) = case p of
-      Mono.PatternVariable v ->
-        return
-          [(v ^. Mono.nameText, BindingInfo {_bindingInfoExpr = exp, _bindingInfoType = typ})]
-      Mono.PatternConstructorApp Mono.ConstructorApp {..} ->
-        goConstructorApp exp _constrAppConstructor _constrAppParameters
-      Mono.PatternWildcard {} -> return []
-
-    goConstructorApp :: Expression -> Mono.Name -> [Mono.Pattern] -> Sem r [(Text, BindingInfo)]
-    goConstructorApp exp constructorName ps = do
-      ctorInfo' <- ctorInfo
-      let ctorArgBindings :: [(Expression, CFunType)] =
-            bimap (memberAccess Object asConstructor) typeToFunType <$> zip ctorArgs ctorInfo'
-          patternCtorArgBindings :: [(Mono.Pattern, (Expression, CFunType))] = zip ps ctorArgBindings
-      concatMapM go patternCtorArgBindings
-      where
-        ctorInfo :: Sem r [Mono.Type]
-        ctorInfo = do
-          p' :: HashMap Mono.Name Mono.ConstructorInfo <- asks (^. Mono.infoConstructors)
-          let fInfo = HashMap.lookupDefault impossible constructorName p'
-          return $ fInfo ^. Mono.constructorInfoArgs
-
-        asConstructor :: Expression
-        asConstructor = functionCall (ExpressionVar (asCast (mkName constructorName))) [exp]
-
-goTypeDecl :: Text -> CDeclType -> Declaration
-goTypeDecl n CDeclType {..} =
-  Declaration
-    { _declType = _typeDeclType,
-      _declIsPtr = _typeIsPtr,
-      _declName = Just n,
-      _declInitializer = Nothing
-    }
-
-goTypeDecl'' :: CDeclType -> Declaration
-goTypeDecl'' CDeclType {..} =
-  Declaration
-    { _declType = _typeDeclType,
-      _declIsPtr = _typeIsPtr,
-      _declName = Nothing,
-      _declInitializer = Nothing
-    }
-
-mallocSizeOf :: Text -> Expression
-mallocSizeOf typeName =
-  functionCall (ExpressionVar Str.malloc) [functionCall (ExpressionVar Str.sizeof) [ExpressionVar typeName]]
-
-declFunctionType :: DeclType
-declFunctionType = DeclTypeDefType Str.minijuvixFunctionT
-
-declFunctionPtrType :: CDeclType
-declFunctionPtrType =
-  CDeclType
-    { _typeDeclType = declFunctionType,
-      _typeIsPtr = True
-    }
-
-funPtrType :: CFunType -> CDeclType
-funPtrType CFunType {..} =
-  CDeclType
-    { _typeDeclType =
-        DeclFunPtr
-          ( FunPtr
-              { _funPtrReturnType = _cFunReturnType ^. typeDeclType,
-                _funPtrIsPtr = _cFunReturnType ^. typeIsPtr,
-                _funPtrArgs = _cFunArgTypes
-              }
-          ),
-      _typeIsPtr = False
-    }
-
-juvixFunctionCall :: CFunType -> Expression -> [Expression] -> Expression
-juvixFunctionCall funType funParam args =
-  functionCall (castToType (funPtrType fTyp) (memberAccess Pointer funParam "fun")) (funParam : args)
-  where
-    fTyp :: CFunType
-    fTyp = funType {_cFunArgTypes = declFunctionPtrType : (funType ^. cFunArgTypes)}

src/MiniJuvix/Translation/MonoJuvixToMiniC/Base.hs

@@ -0,0 +1,162 @@
+module MiniJuvix.Translation.MonoJuvixToMiniC.Base
+  ( module MiniJuvix.Translation.MonoJuvixToMiniC.Base,
+    module MiniJuvix.Translation.MonoJuvixToMiniC.Types,
+    module MiniJuvix.Translation.MonoJuvixToMiniC.CNames,
+    module MiniJuvix.Translation.MonoJuvixToMiniC.CBuilder,
+  )
+where
+
+import Data.HashMap.Strict qualified as HashMap
+import Data.Text qualified as T
+import MiniJuvix.Internal.Strings qualified as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Language qualified as Micro
+import MiniJuvix.Syntax.MiniC.Language
+import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
+import MiniJuvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
+import MiniJuvix.Translation.MonoJuvixToMiniC.CBuilder
+import MiniJuvix.Translation.MonoJuvixToMiniC.CNames
+import MiniJuvix.Translation.MonoJuvixToMiniC.Types
+
+unsupported :: Text -> a
+unsupported msg = error (msg <> " Mono to C: not yet supported")
+
+unfoldFunType :: Mono.Type -> ([Mono.Type], Mono.Type)
+unfoldFunType t = case t of
+  Mono.TypeFunction (Mono.Function l r) -> first (l :) (unfoldFunType r)
+  _ -> ([], t)
+
+mkName :: Mono.Name -> Text
+mkName n =
+  adaptFirstLetter lexeme <> nameTextSuffix
+  where
+    lexeme
+      | T.null lexeme' = "v"
+      | otherwise = lexeme'
+      where
+        lexeme' = T.filter isValidChar (n ^. Mono.nameText)
+    isValidChar :: Char -> Bool
+    isValidChar c = isLetter c && isAscii c
+    adaptFirstLetter :: Text -> Text
+    adaptFirstLetter t = case T.uncons t of
+      Nothing -> impossible
+      Just (h, r) -> T.cons (capitalize h) r
+      where
+        capitalize :: Char -> Char
+        capitalize
+          | capital = toUpper
+          | otherwise = toLower
+        capital = case n ^. Mono.nameKind of
+          Mono.KNameConstructor -> True
+          Mono.KNameInductive -> True
+          Mono.KNameTopModule -> True
+          Mono.KNameLocalModule -> True
+          _ -> False
+    nameTextSuffix :: Text
+    nameTextSuffix = case n ^. Mono.nameKind of
+      Mono.KNameTopModule -> mempty
+      Mono.KNameFunction ->
+        if n ^. Mono.nameText == Str.main then mempty else idSuffix
+      _ -> idSuffix
+    idSuffix :: Text
+    idSuffix = "_" <> show (n ^. Mono.nameId . Micro.unNameId)
+
+goType :: Mono.Type -> CDeclType
+goType t = case t of
+  Mono.TypeIden ti -> getMonoType ti
+  Mono.TypeFunction {} -> declFunctionPtrType
+  Mono.TypeUniverse {} -> unsupported "TypeUniverse"
+  where
+    getMonoType :: Mono.TypeIden -> CDeclType
+    getMonoType = \case
+      Mono.TypeIdenInductive mn ->
+        CDeclType
+          { _typeDeclType = DeclTypeDefType (asTypeDef (mkName mn)),
+            _typeIsPtr = True
+          }
+      Mono.TypeIdenAxiom mn ->
+        CDeclType
+          { _typeDeclType = DeclTypeDefType (mkName mn),
+            _typeIsPtr = False
+          }
+
+typeToFunType :: Mono.Type -> CFunType
+typeToFunType t =
+  let (_cFunArgTypes, _cFunReturnType) =
+        bimap (map goType) goType (unfoldFunType t)
+   in CFunType {..}
+
+applyOnFunStatement ::
+  forall a. Monoid a => (Mono.FunctionDef -> a) -> Mono.Statement -> a
+applyOnFunStatement f = \case
+  Mono.StatementFunction x -> f x
+  Mono.StatementForeign {} -> mempty
+  Mono.StatementAxiom {} -> mempty
+  Mono.StatementInductive {} -> mempty
+
+buildPatternInfoTable :: forall r. Member (Reader Mono.InfoTable) r => [Mono.Type] -> Mono.FunctionClause -> Sem r PatternInfoTable
+buildPatternInfoTable argTyps Mono.FunctionClause {..} =
+  PatternInfoTable . HashMap.fromList <$> patBindings
+  where
+    funArgBindings :: [(Expression, CFunType)]
+    funArgBindings = bimap ExpressionVar typeToFunType <$> zip funArgs argTyps
+
+    patArgBindings :: [(Mono.Pattern, (Expression, CFunType))]
+    patArgBindings = zip _clausePatterns funArgBindings
+
+    patBindings :: Sem r [(Text, BindingInfo)]
+    patBindings = concatMapM go patArgBindings
+
+    go :: (Mono.Pattern, (Expression, CFunType)) -> Sem r [(Text, BindingInfo)]
+    go (p, (exp, typ)) = case p of
+      Mono.PatternVariable v ->
+        return
+          [(v ^. Mono.nameText, BindingInfo {_bindingInfoExpr = exp, _bindingInfoType = typ})]
+      Mono.PatternConstructorApp Mono.ConstructorApp {..} ->
+        goConstructorApp exp _constrAppConstructor _constrAppParameters
+      Mono.PatternWildcard {} -> return []
+
+    goConstructorApp :: Expression -> Mono.Name -> [Mono.Pattern] -> Sem r [(Text, BindingInfo)]
+    goConstructorApp exp constructorName ps = do
+      ctorInfo' <- ctorInfo
+      let ctorArgBindings :: [(Expression, CFunType)] =
+            bimap (memberAccess Object asConstructor) typeToFunType <$> zip ctorArgs ctorInfo'
+          patternCtorArgBindings :: [(Mono.Pattern, (Expression, CFunType))] = zip ps ctorArgBindings
+      concatMapM go patternCtorArgBindings
+      where
+        ctorInfo :: Sem r [Mono.Type]
+        ctorInfo = do
+          p' :: HashMap Mono.Name Mono.ConstructorInfo <- asks (^. Mono.infoConstructors)
+          let fInfo = HashMap.lookupDefault impossible constructorName p'
+          return $ fInfo ^. Mono.constructorInfoArgs
+
+        asConstructor :: Expression
+        asConstructor = functionCall (ExpressionVar (asCast (mkName constructorName))) [exp]
+
+getType ::
+  Members '[Reader Mono.InfoTable, Reader PatternInfoTable] r =>
+  Mono.Iden ->
+  Sem r (CFunType, CArity)
+getType = \case
+  Mono.IdenFunction n -> do
+    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoFunctions)
+    return (typeToFunType (fInfo ^. Mono.functionInfoType), fInfo ^. Mono.functionInfoPatterns)
+  Mono.IdenConstructor n -> do
+    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoConstructors)
+    let argTypes = goType <$> (fInfo ^. Mono.constructorInfoArgs)
+    return
+      ( CFunType
+          { _cFunArgTypes = argTypes,
+            _cFunReturnType =
+              goType
+                (Mono.TypeIden (Mono.TypeIdenInductive (fInfo ^. Mono.constructorInfoInductive)))
+          },
+        length argTypes
+      )
+  Mono.IdenAxiom n -> do
+    fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoAxioms)
+    let t = typeToFunType (fInfo ^. Mono.axiomInfoType)
+    return (t, length (t ^. cFunArgTypes))
+  Mono.IdenVar n -> do
+    t <- (^. bindingInfoType) . HashMap.lookupDefault impossible (n ^. Mono.nameText) <$> asks (^. patternBindings)
+    return (t, length (t ^. cFunArgTypes))

src/MiniJuvix/Translation/MonoJuvixToMiniC/CBuilder.hs

@@ -0,0 +1,66 @@
+module MiniJuvix.Translation.MonoJuvixToMiniC.CBuilder where
+
+import MiniJuvix.Internal.Strings qualified as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MiniC.Language
+import MiniJuvix.Translation.MonoJuvixToMiniC.CNames
+
+namedArgs :: (Text -> Text) -> [CDeclType] -> [Declaration]
+namedArgs prefix = zipWith goTypeDecl argLabels
+  where
+    argLabels :: [Text]
+    argLabels = prefix . show <$> [0 :: Integer ..]
+
+goTypeDecl :: Text -> CDeclType -> Declaration
+goTypeDecl n CDeclType {..} =
+  Declaration
+    { _declType = _typeDeclType,
+      _declIsPtr = _typeIsPtr,
+      _declName = Just n,
+      _declInitializer = Nothing
+    }
+
+declFunctionType :: DeclType
+declFunctionType = DeclTypeDefType Str.minijuvixFunctionT
+
+declFunctionPtrType :: CDeclType
+declFunctionPtrType =
+  CDeclType
+    { _typeDeclType = declFunctionType,
+      _typeIsPtr = True
+    }
+
+funPtrType :: CFunType -> CDeclType
+funPtrType CFunType {..} =
+  CDeclType
+    { _typeDeclType =
+        DeclFunPtr
+          ( FunPtr
+              { _funPtrReturnType = _cFunReturnType ^. typeDeclType,
+                _funPtrIsPtr = _cFunReturnType ^. typeIsPtr,
+                _funPtrArgs = _cFunArgTypes
+              }
+          ),
+      _typeIsPtr = False
+    }
+
+mallocSizeOf :: Text -> Expression
+mallocSizeOf typeName =
+  functionCall (ExpressionVar Str.malloc) [functionCall (ExpressionVar Str.sizeof) [ExpressionVar typeName]]
+
+juvixFunctionCall :: CFunType -> Expression -> [Expression] -> Expression
+juvixFunctionCall funType funParam args =
+  functionCall (castToType (funPtrType fTyp) (memberAccess Pointer funParam "fun")) (funParam : args)
+  where
+    fTyp :: CFunType
+    fTyp = funType {_cFunArgTypes = declFunctionPtrType : (funType ^. cFunArgTypes)}
+
+cFunTypeToFunSig :: Text -> CFunType -> FunctionSig
+cFunTypeToFunSig name CFunType {..} =
+  FunctionSig
+    { _funcReturnType = _cFunReturnType ^. typeDeclType,
+      _funcIsPtr = _cFunReturnType ^. typeIsPtr,
+      _funcQualifier = None,
+      _funcName = name,
+      _funcArgs = namedArgs asFunArg _cFunArgTypes
+    }

src/MiniJuvix/Translation/MonoJuvixToMiniC/CNames.hs

@@ -0,0 +1,63 @@
+module MiniJuvix.Translation.MonoJuvixToMiniC.CNames where
+
+import MiniJuvix.Prelude
+
+funField :: Text
+funField = "fun"
+
+asStruct :: Text -> Text
+asStruct n = n <> "_s"
+
+asTypeDef :: Text -> Text
+asTypeDef n = n <> "_t"
+
+asTag :: Text -> Text
+asTag n = n <> "_tag"
+
+asField :: Text -> Text
+asField n = n <> "_field"
+
+asNullary :: Text -> Text
+asNullary n = n <> "_nullary"
+
+asCast :: Text -> Text
+asCast n = "as_" <> n
+
+asIs :: Text -> Text
+asIs n = "is_" <> n
+
+asNew :: Text -> Text
+asNew n = "new_" <> n
+
+asFun :: Text -> Text
+asFun n = n <> "_fun"
+
+asEval :: Text -> Text
+asEval n = n <> "_eval"
+
+asApply :: Text -> Text
+asApply n = n <> "_apply"
+
+asEnv :: Text -> Text
+asEnv n = n <> "_env"
+
+asFunArg :: Text -> Text
+asFunArg n = "fa" <> n
+
+asCtorArg :: Text -> Text
+asCtorArg n = "ca" <> n
+
+asEnvArg :: Text -> Text
+asEnvArg n = "ea" <> n
+
+mkArgs :: (Text -> Text) -> [Text]
+mkArgs f = map (f . show) [0 :: Integer ..]
+
+funArgs :: [Text]
+funArgs = mkArgs asFunArg
+
+ctorArgs :: [Text]
+ctorArgs = mkArgs asCtorArg
+
+envArgs :: [Text]
+envArgs = mkArgs asEnvArg

src/MiniJuvix/Translation/MonoJuvixToMiniC/Closure.hs

@@ -0,0 +1,264 @@
+module MiniJuvix.Translation.MonoJuvixToMiniC.Closure where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MiniC.Language
+import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
+import MiniJuvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
+import MiniJuvix.Translation.MonoJuvixToMiniC.Base
+
+genClosures ::
+  forall r.
+  Member (Reader Mono.InfoTable) r =>
+  Mono.Module ->
+  Sem r [CCode]
+genClosures Mono.Module {..} = do
+  closureInfos <- concatMapM (applyOnFunStatement functionDefClosures) (_moduleBody ^. Mono.moduleStatements)
+  return (genCClosure =<< nub closureInfos)
+
+genCClosure :: ClosureInfo -> [CCode]
+genCClosure c =
+  [ ExternalDecl (genClosureEnv c),
+    ExternalFunc (genClosureApply c),
+    ExternalFunc (genClosureEval c)
+  ]
+
+functionDefClosures ::
+  Member (Reader Mono.InfoTable) r =>
+  Mono.FunctionDef ->
+  Sem r [ClosureInfo]
+functionDefClosures Mono.FunctionDef {..} =
+  concatMapM (clauseClosures (fst (unfoldFunType _funDefType))) (toList _funDefClauses)
+
+genClosureExpression ::
+  forall r.
+  Members '[Reader Mono.InfoTable, Reader PatternInfoTable] r =>
+  [Mono.Type] ->
+  Mono.Expression ->
+  Sem r [ClosureInfo]
+genClosureExpression funArgTyps = \case
+  Mono.ExpressionIden i -> do
+    let rootFunMonoName = Mono.getName i
+        rootFunNameId = rootFunMonoName ^. Mono.nameId
+        rootFunName = mkName rootFunMonoName
+    case i of
+      Mono.IdenVar {} -> return []
+      _ -> do
+        (t, patterns) <- getType i
+        let argTyps = t ^. cFunArgTypes
+        if
+            | null argTyps -> return []
+            | otherwise ->
+                return
+                  [ ClosureInfo
+                      { _closureNameId = rootFunNameId,
+                        _closureRootName = rootFunName,
+                        _closureMembers = [],
+                        _closureFunType = t,
+                        _closureCArity = patterns
+                      }
+                  ]
+  Mono.ExpressionApplication a -> exprApplication a
+  Mono.ExpressionLiteral {} -> return []
+  where
+    exprApplication :: Mono.Application -> Sem r [ClosureInfo]
+    exprApplication a = do
+      (f, appArgs) <- unfoldApp a
+      let rootFunMonoName = Mono.getName f
+          rootFunNameId = rootFunMonoName ^. Mono.nameId
+          rootFunName = mkName rootFunMonoName
+      (fType, patterns) <- getType f
+      closureArgs <- concatMapM (genClosureExpression funArgTyps) appArgs
+
+      if
+          | length appArgs < length (fType ^. cFunArgTypes) ->
+              return
+                ( [ ClosureInfo
+                      { _closureNameId = rootFunNameId,
+                        _closureRootName = rootFunName,
+                        _closureMembers = take (length appArgs) (fType ^. cFunArgTypes),
+                        _closureFunType = fType,
+                        _closureCArity = patterns
+                      }
+                  ]
+                    <> closureArgs
+                )
+          | otherwise -> return closureArgs
+
+    unfoldApp :: Mono.Application -> Sem r (Mono.Iden, [Mono.Expression])
+    unfoldApp Mono.Application {..} = case _appLeft of
+      Mono.ExpressionApplication x -> do
+        uf <- unfoldApp x
+        return (second (_appRight :) uf)
+      Mono.ExpressionIden i -> do
+        return (i, [_appRight])
+      Mono.ExpressionLiteral {} -> impossible
+
+genClosureEnv :: ClosureInfo -> Declaration
+genClosureEnv c =
+  typeDefWrap
+    (asTypeDef name)
+    ( DeclStructUnion
+        ( StructUnion
+            { _structUnionTag = StructTag,
+              _structUnionName = Just name,
+              _structMembers = Just (funDecl : members)
+            }
+        )
+    )
+  where
+    name :: Text
+    name = asEnv (closureNamedId c)
+    funDecl :: Declaration
+    funDecl = namedDeclType funField uIntPtrType
+    members :: [Declaration]
+    members = uncurry cDeclToNamedDecl <$> zip envArgs (c ^. closureMembers)
+
+genClosureApplySig :: ClosureInfo -> FunctionSig
+genClosureApplySig c = cFunTypeToFunSig (asApply (closureNamedId c)) applyFunType
+  where
+    nonEnvTyps :: [CDeclType]
+    nonEnvTyps = drop (length (c ^. closureMembers)) (c ^. closureFunType . cFunArgTypes)
+    allFunTyps :: [CDeclType]
+    allFunTyps = declFunctionPtrType : nonEnvTyps
+    applyFunType :: CFunType
+    applyFunType = (c ^. closureFunType) {_cFunArgTypes = allFunTyps}
+
+genClosureApply :: ClosureInfo -> Function
+genClosureApply c =
+  let localName :: Text
+      localName = "env"
+      localFunName :: Text
+      localFunName = "f"
+      name :: Text
+      name = closureNamedId c
+      envName :: Text
+      envName = asTypeDef (asEnv name)
+      closureEnvArgs :: [Text]
+      closureEnvArgs = take (length (c ^. closureMembers)) envArgs
+      closureEnvAccess :: [Expression]
+      closureEnvAccess = memberAccess Pointer (ExpressionVar localName) <$> closureEnvArgs
+      args :: [Expression]
+      args = take (length (c ^. closureFunType . cFunArgTypes)) (closureEnvAccess <> drop 1 (ExpressionVar <$> funArgs))
+      nPatterns :: Int
+      nPatterns = c ^. closureCArity
+      patternArgs :: [Expression]
+      patternArgs = take nPatterns args
+      funType :: CFunType
+      funType =
+        (c ^. closureFunType)
+          { _cFunArgTypes = drop nPatterns (c ^. closureFunType . cFunArgTypes)
+          }
+      funName :: Expression
+      funName = ExpressionVar (c ^. closureRootName)
+      funCall :: Expression
+      funCall =
+        if
+            | null patternArgs -> funName
+            | otherwise -> functionCall funName patternArgs
+      juvixFunCall :: [BodyItem]
+      juvixFunCall =
+        if
+            | nPatterns < length args ->
+                [ BodyDecl
+                    ( Declaration
+                        { _declType = declFunctionType,
+                          _declIsPtr = True,
+                          _declName = Just localFunName,
+                          _declInitializer = Just (ExprInitializer funCall)
+                        }
+                    ),
+                  BodyStatement . StatementReturn . Just $ juvixFunctionCall funType (ExpressionVar localFunName) (drop nPatterns args)
+                ]
+            | otherwise -> [BodyStatement . StatementReturn . Just $ functionCall (ExpressionVar (c ^. closureRootName)) args]
+      envArg :: BodyItem
+      envArg =
+        BodyDecl
+          ( Declaration
+              { _declType = DeclTypeDefType envName,
+                _declIsPtr = True,
+                _declName = Just localName,
+                _declInitializer =
+                  Just $
+                    ExprInitializer
+                      ( castToType
+                          ( CDeclType
+                              { _typeDeclType = DeclTypeDefType envName,
+                                _typeIsPtr = True
+                              }
+                          )
+                          (ExpressionVar "fa0")
+                      )
+              }
+          )
+   in Function
+        { _funcSig = genClosureApplySig c,
+          _funcBody = envArg : juvixFunCall
+        }
+
+genClosureEval :: ClosureInfo -> Function
+genClosureEval c =
+  let localName :: Text
+      localName = "f"
+      name :: Text
+      name = closureNamedId c
+      envName :: Text
+      envName = asTypeDef (asEnv name)
+      envArgToFunArg :: [(Text, Text)]
+      envArgToFunArg = take (length (c ^. closureMembers)) (zip envArgs funArgs)
+      assignments :: [Assign]
+      assignments = mkAssign <$> envArgToFunArg
+      mkAssign :: (Text, Text) -> Assign
+      mkAssign (envArg, funArg) =
+        Assign
+          { _assignLeft = memberAccess Pointer (ExpressionVar localName) envArg,
+            _assignRight = ExpressionVar funArg
+          }
+   in Function
+        { _funcSig =
+            FunctionSig
+              { _funcReturnType = declFunctionType,
+                _funcIsPtr = True,
+                _funcQualifier = None,
+                _funcName = asEval name,
+                _funcArgs = namedArgs asFunArg (c ^. closureMembers)
+              },
+          _funcBody =
+            [ BodyDecl
+                ( Declaration
+                    { _declType = DeclTypeDefType envName,
+                      _declIsPtr = True,
+                      _declName = Just localName,
+                      _declInitializer = Just $ ExprInitializer (mallocSizeOf envName)
+                    }
+                ),
+              BodyStatement
+                ( StatementExpr
+                    ( ExpressionAssign
+                        ( Assign
+                            { _assignLeft = memberAccess Pointer (ExpressionVar localName) funField,
+                              _assignRight =
+                                castToType
+                                  ( CDeclType
+                                      { _typeDeclType = uIntPtrType,
+                                        _typeIsPtr = False
+                                      }
+                                  )
+                                  (ExpressionVar (asApply name))
+                            }
+                        )
+                    )
+                )
+            ]
+              <> (BodyStatement . StatementExpr . ExpressionAssign <$> assignments)
+              <> [ returnStatement (castToType declFunctionPtrType (ExpressionVar localName))
+                 ]
+        }
+
+clauseClosures ::
+  Members '[Reader Mono.InfoTable] r =>
+  [Mono.Type] ->
+  Mono.FunctionClause ->
+  Sem r [ClosureInfo]
+clauseClosures argTyps clause = do
+  bindings <- buildPatternInfoTable argTyps clause
+  runReader bindings (genClosureExpression argTyps (clause ^. Mono.clauseBody))

src/MiniJuvix/Translation/MonoJuvixToMiniC/Types.hs

@@ -0,0 +1,36 @@
+module MiniJuvix.Translation.MonoJuvixToMiniC.Types where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MiniC.Language
+import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
+
+newtype MiniCResult = MiniCResult
+  { _resultCCode :: Text
+  }
+
+data BindingInfo = BindingInfo
+  { _bindingInfoExpr :: Expression,
+    _bindingInfoType :: CFunType
+  }
+
+newtype PatternInfoTable = PatternInfoTable
+  {_patternBindings :: HashMap Text BindingInfo}
+
+type CArity = Int
+
+data ClosureInfo = ClosureInfo
+  { _closureNameId :: Mono.NameId,
+    _closureRootName :: Text,
+    _closureMembers :: [CDeclType],
+    _closureFunType :: CFunType,
+    _closureCArity :: CArity
+  }
+  deriving stock (Show, Eq)
+
+closureNamedId :: ClosureInfo -> Text
+closureNamedId ClosureInfo {..} = _closureRootName <> "_" <> show (length _closureMembers)
+
+makeLenses ''ClosureInfo
+makeLenses ''MiniCResult
+makeLenses ''PatternInfoTable
+makeLenses ''BindingInfo

test/BackendC.hs

@@ -1,7 +1,8 @@
 module BackendC where
 
+import BackendC.Examples qualified as E
 import BackendC.Positive qualified as P
 import Base
 
 allTests :: TestTree
-allTests = testGroup "Backend C tests" [P.allTests]
+allTests = testGroup "Backend C tests" [P.allTests, E.allTests]

test/BackendC/Base.hs

@@ -0,0 +1,95 @@
+module BackendC.Base where
+
+import Base
+import Data.FileEmbed
+import Data.Text.IO qualified as TIO
+import MiniJuvix.Pipeline
+import MiniJuvix.Translation.MonoJuvixToMiniC as MiniC
+import System.IO.Extra (withTempDir)
+import System.Process qualified as P
+
+clangCompile ::
+  (FilePath -> FilePath -> [String]) ->
+  MiniC.MiniCResult ->
+  Text ->
+  (String -> IO ()) ->
+  IO Text
+clangCompile mkClangArgs cResult stdinText step =
+  withTempDir
+    ( \dirPath -> do
+        let cOutputFile = dirPath </> "out.c"
+            wasmOutputFile = dirPath </> "out.wasm"
+        TIO.writeFile cOutputFile (cResult ^. MiniC.resultCCode)
+        step "WASM generation"
+        P.callProcess
+          "clang"
+          (mkClangArgs wasmOutputFile cOutputFile)
+        step "WASM execution"
+        pack <$> P.readProcess "wasmer" [wasmOutputFile] (unpack stdinText)
+    )
+
+clangAssertion :: FilePath -> FilePath -> Text -> ((String -> IO ()) -> Assertion)
+clangAssertion mainFile expectedFile stdinText step = do
+  step "Check clang and wasmer are on path"
+  assertCmdExists "clang"
+  assertCmdExists "wasmer"
+
+  step "Lookup WASI_SYSROOT_PATH"
+  sysrootPath <-
+    assertEnvVar
+      "Env var WASI_SYSROOT_PATH missing. Set to the location of the wasi-clib sysroot"
+      "WASI_SYSROOT_PATH"
+
+  step "C Generation"
+  let entryPoint = defaultEntryPoint mainFile
+  p :: MiniC.MiniCResult <- runIO (upToMiniC entryPoint)
+
+  expected <- TIO.readFile expectedFile
+
+  step "Compile C with standalone runtime"
+  actualStandalone <- clangCompile (standaloneArgs sysrootPath) p stdinText step
+  step "Compare expected and actual program output"
+  assertEqDiff ("check: WASM output = " <> expectedFile) actualStandalone expected
+
+  step "Compile C with libc runtime"
+  actualLibc <- clangCompile (libcArgs sysrootPath) p stdinText step
+  step "Compare expected and actual program output"
+  assertEqDiff ("check: WASM output = " <> expectedFile) actualLibc expected
+
+standaloneArgs :: FilePath -> FilePath -> FilePath -> [String]
+standaloneArgs sysrootPath wasmOutputFile cOutputFile =
+  [ "-nodefaultlibs",
+    "-I",
+    takeDirectory minicRuntime,
+    "-Werror",
+    "--target=wasm32-wasi",
+    "--sysroot",
+    sysrootPath,
+    "-o",
+    wasmOutputFile,
+    wallocPath,
+    cOutputFile
+  ]
+  where
+    minicRuntime :: FilePath
+    minicRuntime = $(makeRelativeToProject "minic-runtime/standalone/minic-runtime.h" >>= strToExp)
+    wallocPath :: FilePath
+    wallocPath = $(makeRelativeToProject "minic-runtime/standalone/walloc.c" >>= strToExp)
+
+libcArgs :: FilePath -> FilePath -> FilePath -> [String]
+libcArgs sysrootPath wasmOutputFile cOutputFile =
+  [ "-nodefaultlibs",
+    "-I",
+    takeDirectory minicRuntime,
+    "-Werror",
+    "-lc",
+    "--target=wasm32-wasi",
+    "--sysroot",
+    sysrootPath,
+    "-o",
+    wasmOutputFile,
+    cOutputFile
+  ]
+  where
+    minicRuntime :: FilePath
+    minicRuntime = $(makeRelativeToProject "minic-runtime/libc/minic-runtime.h" >>= strToExp)

test/BackendC/Examples.hs

@@ -0,0 +1,40 @@
+module BackendC.Examples where
+
+import BackendC.Base
+import Base
+import Data.FileEmbed
+
+data ExampleTest = ExampleTest
+  { _name :: String,
+    _relDir :: FilePath,
+    _mainFile :: FilePath,
+    _expectedDir :: FilePath,
+    _stdinText :: Text
+  }
+
+makeLenses ''ExampleTest
+
+exampleRoot :: FilePath
+exampleRoot = "examples/milestone"
+
+testDescr :: ExampleTest -> TestDescr
+testDescr ExampleTest {..} =
+  let mainRoot = exampleRoot </> _relDir
+      expectedFile = $(makeRelativeToProject "tests/examplesExpected" >>= strToExp) </> _expectedDir </> "expected.golden"
+   in TestDescr
+        { _testName = _name,
+          _testRoot = mainRoot,
+          _testAssertion = Steps $ clangAssertion _mainFile expectedFile _stdinText
+        }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Backend C milestone example tests"
+    (map (mkTest . testDescr) tests)
+
+tests :: [ExampleTest]
+tests =
+  [ ExampleTest "Validity Predicate example" "ValidityPredicates" "Tests.mjuvix" "ValidityPredicates" "",
+    ExampleTest "MiniTicTacToe example" "MiniTicTacToe" "MiniTicTacToe.mjuvix" "MiniTicTacToe" "aaa\n0\n10\n1\n2\n3\n3\n4\n5\n6\n7\n8\n9\n"
+  ]

test/BackendC/Positive.hs

@@ -1,12 +1,7 @@
 module BackendC.Positive where
 
+import BackendC.Base
 import Base
-import Data.FileEmbed
-import Data.Text.IO qualified as TIO
-import MiniJuvix.Pipeline
-import MiniJuvix.Translation.MonoJuvixToMiniC as MiniC
-import System.IO.Extra (withTempDir)
-import System.Process qualified as P
 
 data PosTest = PosTest
   { _name :: String,
@@ -30,89 +25,9 @@ testDescr PosTest {..} =
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ \step -> do
-            step "Check clang and wasmer are on path"
-            assertCmdExists "clang"
-            assertCmdExists "wasmer"
-
-            step "Lookup WASI_SYSROOT_PATH"
-            sysrootPath <-
-              assertEnvVar
-                "Env var WASI_SYSROOT_PATH missing. Set to the location of the wasi-clib sysroot"
-                "WASI_SYSROOT_PATH"
-
-            step "C Generation"
-            let entryPoint = defaultEntryPoint mainFile
-            p :: MiniC.MiniCResult <- runIO (upToMiniC entryPoint)
-
-            expected <- TIO.readFile expectedFile
-
-            step "Compile C with standalone runtime"
-            actualStandalone <- clangCompile (standaloneArgs sysrootPath) p step
-            step "Compare expected and actual program output"
-            assertEqDiff ("check: WASM output = " <> expectedFile) actualStandalone expected
-
-            step "Compile C with libc runtime"
-            actualLibc <- clangCompile (libcArgs sysrootPath) p step
-            step "Compare expected and actual program output"
-            assertEqDiff ("check: WASM output = " <> expectedFile) actualLibc expected
+          _testAssertion = Steps $ clangAssertion mainFile expectedFile ""
         }
 
-clangCompile ::
-  (FilePath -> FilePath -> [String]) ->
-  MiniC.MiniCResult ->
-  (String -> IO ()) ->
-  IO Text
-clangCompile mkClangArgs cResult step =
-  withTempDir
-    ( \dirPath -> do
-        let cOutputFile = dirPath </> "out.c"
-            wasmOutputFile = dirPath </> "out.wasm"
-        TIO.writeFile cOutputFile (cResult ^. MiniC.resultCCode)
-        step "WASM generation"
-        P.callProcess
-          "clang"
-          (mkClangArgs wasmOutputFile cOutputFile)
-        step "WASM execution"
-        pack <$> P.readProcess "wasmer" [wasmOutputFile] ""
-    )
-
-standaloneArgs :: FilePath -> FilePath -> FilePath -> [String]
-standaloneArgs sysrootPath wasmOutputFile cOutputFile =
-  [ "-nodefaultlibs",
-    "-I",
-    takeDirectory minicRuntime,
-    "--target=wasm32-wasi",
-    "--sysroot",
-    sysrootPath,
-    "-o",
-    wasmOutputFile,
-    wallocPath,
-    cOutputFile
-  ]
-  where
-    minicRuntime :: FilePath
-    minicRuntime = $(makeRelativeToProject "minic-runtime/standalone/minic-runtime.h" >>= strToExp)
-    wallocPath :: FilePath
-    wallocPath = $(makeRelativeToProject "minic-runtime/standalone/walloc.c" >>= strToExp)
-
-libcArgs :: FilePath -> FilePath -> FilePath -> [String]
-libcArgs sysrootPath wasmOutputFile cOutputFile =
-  [ "-nodefaultlibs",
-    "-I",
-    takeDirectory minicRuntime,
-    "-lc",
-    "--target=wasm32-wasi",
-    "--sysroot",
-    sysrootPath,
-    "-o",
-    wasmOutputFile,
-    cOutputFile
-  ]
-  where
-    minicRuntime :: FilePath
-    minicRuntime = $(makeRelativeToProject "minic-runtime/libc/minic-runtime.h" >>= strToExp)
-
 allTests :: TestTree
 allTests =
   testGroup
@@ -127,5 +42,9 @@ tests =
     PosTest "Multiple modules" "MultiModules",
     PosTest "Higher Order Functions" "HigherOrder",
     PosTest "Higher Order Functions and explicit holes" "PolymorphismHoles",
-    PosTest "Closures with no environment" "ClosureNoEnv"
+    PosTest "Closures with no environment" "ClosureNoEnv",
+    PosTest "Closures with environment" "ClosureEnv",
+    PosTest "SimpleFungibleTokenImplicit" "SimpleFungibleTokenImplicit",
+    PosTest "Mutually recursive function" "MutuallyRecursive",
+    PosTest "Nested List type" "NestedList"
   ]

tests/CLI/Commands/html.test

@@ -2,24 +2,15 @@ $ minijuvix html
 > /Provide.*/
 >= 1
 
-$ cd examples/milestone/ValidityPredicates/ && minijuvix html Prelude.mjuvix && cat html/Prelude.html
+$ cd examples/milestone/Lib/ && minijuvix html Prelude.mjuvix && cat html/Prelude.html
 > /<!DOCTYPE HTML>.*/
 >= 0
 
-$ rm -rf examples/html && minijuvix html examples/milestone/ValidityPredicates/Prelude.mjuvix --output-dir=./../../html && [ -d examples/html/assets ] && [ -f examples/html/Prelude.html ]
+$ rm -rf examples/html && minijuvix html examples/milestone/Lib/Prelude.mjuvix --output-dir=./../../html && [ -d examples/html/assets ] && [ -f examples/html/Prelude.html ]
 > 
 Writing Prelude.html
 >= 0
 
-$ rm -rf examples/html && minijuvix html examples/milestone/ValidityPredicates/Prelude.mjuvix --recursive --output-dir=./../../html && (ls examples/html | wc -l) && cd examples/html && [ -f Data.String.html ] && [ -f Data.Maybe.html ] && [ -f Data.Int.html ] && [ -f System.IO.html ] && [ -f Data.List.html ] && [ -f Data.Pair.html ] && [ -f Data.Bool.html ] && [ -f Prelude.html ] && [ -f assets/highlight.js   ] && [ -f assets/source-ayu-light.css ] && [ -f assets/source-nord.css ]
-> 
-Writing Data.String.html
-Writing Data.Maybe.html
-Writing Data.Int.html
-Writing System.IO.html
-Writing Data.List.html
-Writing Data.Pair.html
-Writing Data.Bool.html
-Writing Prelude.html
-9
+$ rm -rf examples/html && minijuvix html examples/milestone/Lib/Prelude.mjuvix --recursive --output-dir=./../../html && (ls examples/html | wc -l) && cd examples/html && [ -f Data.String.html ] && [ -f Data.Maybe.html ] && [ -f Data.Int.html ] && [ -f System.IO.html ] && [ -f Data.List.html ] && [ -f Data.Pair.html ] && [ -f Data.Bool.html ] && [ -f Prelude.html ] && [ -f assets/highlight.js   ] && [ -f assets/source-ayu-light.css ] && [ -f assets/source-nord.css ]
+> /Writing.*/
 >= 0

tests/examplesExpected/MiniTicTacToe/expected.golden

@@ -0,0 +1,109 @@
+MiniTicTacToe
+-------------
+
+Type a number then ENTER to make a move
+
++---+---+---+
+| 1 | 2 | 3 |
++---+---+---+
+| 4 | 5 | 6 |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player X: 
+Invalid number, try again
+
++---+---+---+
+| 1 | 2 | 3 |
++---+---+---+
+| 4 | 5 | 6 |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player X: 
+Invalid number, try again
+
++---+---+---+
+| 1 | 2 | 3 |
++---+---+---+
+| 4 | 5 | 6 |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player X: 
+Invalid number, try again
+
++---+---+---+
+| 1 | 2 | 3 |
++---+---+---+
+| 4 | 5 | 6 |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player X: 
++---+---+---+
+| X | 2 | 3 |
++---+---+---+
+| 4 | 5 | 6 |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player O: 
++---+---+---+
+| X | O | 3 |
++---+---+---+
+| 4 | 5 | 6 |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player X: 
++---+---+---+
+| X | O | X |
++---+---+---+
+| 4 | 5 | 6 |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player O: 
+The square is already occupied, try again
+
++---+---+---+
+| X | O | X |
++---+---+---+
+| 4 | 5 | 6 |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player O: 
++---+---+---+
+| X | O | X |
++---+---+---+
+| O | 5 | 6 |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player X: 
++---+---+---+
+| X | O | X |
++---+---+---+
+| O | X | 6 |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player O: 
++---+---+---+
+| X | O | X |
++---+---+---+
+| O | X | O |
++---+---+---+
+| 7 | 8 | 9 |
++---+---+---+
+Player X: 
++---+---+---+
+| X | O | X |
++---+---+---+
+| O | X | O |
++---+---+---+
+| X | 8 | 9 |
++---+---+---+
+Player X wins!

tests/examplesExpected/ValidityPredicates/expected.golden

@@ -0,0 +1 @@
+VP Status: OK

tests/positive/MiniC/ClosureEnv/Data

@@ -0,0 +1 @@
+../Lib/Data

tests/positive/MiniC/ClosureEnv/Input.mjuvix

@@ -0,0 +1,96 @@
+module Input;
+
+open import Data.IO;
+open import Data.String;
+
+axiom Int : Type;
+
+compile Int {
+  c ↦ "int";
+};
+
+axiom to-str : Int → String;
+
+compile to-str {
+  c ↦ "intToStr";
+};
+
+foreign c {
+  int cplus(int l, int r) {
+    return l + r;
+  \}
+};
+
+axiom plus : Int → Int → Int;
+
+compile plus {
+  c ↦ "cplus";
+};
+
+inductive Nat {
+  zero : Nat;
+  suc : Nat → Nat;
+};
+
+nplus : Nat → Nat → Nat;
+nplus zero n ≔ n;
+nplus (suc m) n ≔ suc (nplus m n);
+
+nplus-to-int : Nat → Int;
+nplus-to-int zero ≔ 0;
+nplus-to-int (suc n) ≔ plus 1 (nplus-to-int n);
+
+nOne : Nat;
+nOne ≔ suc zero;
+
+nplusOne : Nat → Nat → Nat;
+nplusOne n ≔ nplus nOne;
+
+one : Int;
+one ≔ 1;
+
+two : Int;
+two ≔ 2;
+
+three : Int;
+three ≔ 3;
+
+plusXIgnore2 : Int → Int → Int → Int → Int;
+plusXIgnore2 _ _ ≔ plus;
+
+plusXIgnore : Int → Int → Int → Int;
+plusXIgnore _ ≔ plus;
+
+plusXIgnore22 : Int → Int → Int → Int → Int;
+plusXIgnore22 _ ≔ plusXIgnore;
+
+plusX : Int → Int → Int;
+plusX ≔ plus;
+
+plusXThree : Int → Int;
+plusXThree ≔ plusX three;
+
+plusOne : Int → Int;
+plusOne ≔ plus one;
+
+plusOneThenTwo : Int;
+plusOneThenTwo ≔ plusOne two;
+
+plusOneThenX : Int → Int;
+plusOneThenX x ≔ plusOne x;
+
+plusOneTwo : Int;
+plusOneTwo ≔ plus one two;
+
+main : Action;
+main ≔ put-str "plusOne one: " >> put-str-ln (to-str (plusOne one))
+      >> put-str "plusOneThenTwo: " >> put-str-ln (to-str (plusOneThenTwo))
+      >> put-str "plusOneThenX three: " >> put-str-ln (to-str (plusOneThenX three))
+      >> put-str "plusOneTwo: " >> put-str-ln (to-str (plusOneTwo))
+      >> put-str "plusX three three: " >> put-str-ln (to-str (plusX three three))
+      >> put-str "plusXIgnore one three three: " >> put-str-ln (to-str (plusXIgnore one three three))
+      >> put-str "plusXIgnore2 one one three three: " >> put-str-ln (to-str (plusXIgnore2 one one three three))
+      >> put-str "plusXIgnore22 one one three two: " >> put-str-ln (to-str (plusXIgnore22 one one three two))
+
+
+end;

tests/positive/MiniC/ClosureEnv/Prelude.mjuvix

@@ -0,0 +1 @@
+../Lib/Prelude.mjuvix

tests/positive/MiniC/ClosureEnv/expected.golden

@@ -0,0 +1,8 @@
+plusOne one: 2
+plusOneThenTwo: 3
+plusOneThenX three: 4
+plusOneTwo: 3
+plusX three three: 6
+plusXIgnore one three three: 6
+plusXIgnore2 one one three three: 6
+plusXIgnore22 one one three two: 5

tests/positive/MiniC/ClosureNoEnv/Data

@@ -0,0 +1 @@
+../Lib/Data

tests/positive/MiniC/ClosureNoEnv/IO.mjuvix

@@ -1 +0,0 @@
-../MultiModules/IO.mjuvix

tests/positive/MiniC/ClosureNoEnv/Input.mjuvix

@@ -1,10 +1,7 @@
 module Input;
 
-import IO;
-open IO;
-
-import String;
-open String;
+open import Data.IO;
+open import Data.String;
 
 axiom Int : Type;
 

tests/positive/MiniC/ClosureNoEnv/Prelude.mjuvix

@@ -0,0 +1 @@
+../Lib/Prelude.mjuvix

tests/positive/MiniC/ClosureNoEnv/String.mjuvix

@@ -1 +0,0 @@
-../MultiModules/String.mjuvix

tests/positive/MiniC/Lib/Data/Bool.mjuvix

@@ -0,0 +1,18 @@
+module Data.Bool;
+
+open import Data.String;
+
+inductive Bool {
+  true : Bool;
+  false : Bool;
+};
+
+not : Bool → Bool;
+not true ≔ false;
+not false ≔ true;
+
+boolToStr : Bool → String;
+boolToStr true ≔ "true";
+boolToStr false ≔ "false";
+
+end;

tests/positive/MiniC/Lib/Data/IO.mjuvix

@@ -1,7 +1,7 @@
-module IO;
+module Data.IO;
 
-import String;
-open String;
+import Data.String;
+open Data.String;
 
 axiom Action : Type;
 

tests/positive/MiniC/Lib/Data/Int.mjuvix

@@ -0,0 +1,28 @@
+module Data.Int;
+
+open import Data.String;
+
+axiom Int : Type;
+compile Int {
+  c ↦ "int";
+};
+
+axiom intToStr : Int → String;
+
+compile intToStr {
+  c ↦ "intToStr";
+};
+
+foreign c {
+   int plus(int l, int r) {
+     return l + r;
+   \}
+};
+
+infixl 6 +;
+axiom + : Int -> Int -> Int;
+compile + {
+  c ↦ "plus";
+};
+
+end;

tests/positive/MiniC/Lib/Data/Nat.mjuvix

@@ -0,0 +1,34 @@
+module Data.Nat;
+
+open import Data.String;
+open import Data.Int;
+
+inductive Nat {
+  zero : Nat;
+  suc : Nat → Nat;
+};
+
+foreign c {
+  void* natInd(int n, void* zero, minijuvix_function_t* suc) {
+    if (n <= 0) return zero;
+    return ((void* (*) (minijuvix_function_t*, void*))suc->fun)(suc, natInd(n - 1, zero, suc));
+  \}
+};
+
+axiom natInd : Int → Nat → (Nat → Nat) → Nat;
+
+compile natInd {
+  c ↦ "natInd";
+};
+
+natToInt : Nat → Int;
+natToInt zero ≔ 0;
+natToInt (suc n) ≔ 1 + (natToInt n);
+
+natToStr : Nat → String;
+natToStr n ≔ intToStr (natToInt n);
+
+intToNat : Int → Nat;
+intToNat x ≔ natInd x zero suc;
+
+end;

tests/positive/MiniC/Lib/Data/Pair.mjuvix

@@ -1,4 +1,4 @@
-module Pair;
+module Data.Pair;
 
 inductive Pair (A : Type) (B : Type) {
  mkPair : A → B → Pair A B;

tests/positive/MiniC/Lib/Data/String.mjuvix

@@ -1,4 +1,4 @@
-module String;
+module Data.String;
 
 axiom String : Type;
 

tests/positive/MiniC/Lib/Prelude.mjuvix

@@ -0,0 +1,15 @@
+module Prelude;
+
+open import Data.String public;
+
+open import Data.Bool public;
+
+open import Data.Int public;
+
+open import Data.Pair public;
+
+open import Data.IO public;
+
+open import Data.Nat public;
+
+end;

tests/positive/MiniC/MultiModules/Bool.mjuvix

@@ -1,9 +0,0 @@
-module Bool;
-
-inductive Bool {
-  true : Bool;
-  false : Bool;
-};
-
-
-end;

tests/positive/MiniC/MultiModules/Data

@@ -0,0 +1 @@
+../Lib/Data

tests/positive/MiniC/MultiModules/Input.mjuvix

@@ -1,12 +1,12 @@
 module Input;
 
-open import String;
+open import Data.String;
 
-open import Bool;
+open import Data.Bool;
 
-open import Pair;
+open import Data.Pair;
 
-open import IO;
+open import Data.IO;
 
 -- Not needed but useful for testing
 open import Prelude;

tests/positive/MiniC/MultiModules/Prelude.mjuvix

@@ -1,11 +0,0 @@
-module Prelude;
-
-open import String public;
-
-open import Bool public;
-
-open import Pair public;
-
-open import IO public;
-
-end;

tests/positive/MiniC/MultiModules/Prelude.mjuvix

@@ -0,0 +1 @@
+../Lib/Prelude.mjuvix

tests/positive/MiniC/MutuallyRecursive/Data

@@ -0,0 +1 @@
+../Lib/Data

tests/positive/MiniC/MutuallyRecursive/Input.mjuvix

@@ -0,0 +1,32 @@
+module Input;
+
+open import Prelude;
+
+odd : Nat → Bool;
+
+even : Nat → Bool;
+
+odd zero ≔ false;
+odd (suc n) ≔ even n;
+
+even zero ≔ true;
+even (suc n) ≔ odd n;
+
+check : (Nat → Bool) → Int → String;
+check f x ≔ (boolToStr (f (intToNat x)));
+
+checkEven : Int → String;
+checkEven ≔ check even;
+
+checkOdd : Int → String;
+checkOdd ≔ check odd;
+
+main : Action;
+main ≔ put-str "even 1: " >> put-str-ln (checkEven 1)
+        >> put-str "even 4: " >> put-str-ln (checkEven 4)
+        >> put-str "even 9: " >> put-str-ln (checkEven 9)
+        >> put-str "odd 1: " >> put-str-ln (checkOdd 1)
+        >> put-str "odd 4: " >> put-str-ln (checkOdd 4)
+        >> put-str "odd 9: " >> put-str-ln (checkOdd 9)
+
+end;

tests/positive/MiniC/MutuallyRecursive/Prelude.mjuvix

@@ -0,0 +1 @@
+../Lib/Prelude.mjuvix

tests/positive/MiniC/MutuallyRecursive/expected.golden

@@ -0,0 +1,6 @@
+even 1: false
+even 4: true
+even 9: false
+odd 1: true
+odd 4: false
+odd 9: true

tests/positive/MiniC/NestedList/Data

@@ -0,0 +1 @@
+../Lib/Data

tests/positive/MiniC/NestedList/Input.mjuvix

@@ -0,0 +1,21 @@
+module Input;
+
+open import Data.IO;
+
+infixr 5 ∷;
+inductive List (A : Type) {
+  nil : List A;
+  ∷ : A → List A → List A;
+};
+
+inductive Foo {
+  a : Foo;
+};
+
+l : List (List Foo) → List (List Foo);
+l ((_ ∷ nil) ∷ nil) ≔ nil ∷ nil;
+
+main : Action;
+main ≔ put-str-ln "no errors";
+
+end;

tests/positive/MiniC/NestedList/Prelude.mjuvix

@@ -0,0 +1 @@
+../Lib/Prelude.mjuvix

tests/positive/MiniC/NestedList/expected.golden

@@ -0,0 +1 @@
+no errors

tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.mjuvix

@@ -0,0 +1,354 @@
+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
+--------------------------------------------------------------------------------
+
+inductive 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;
+compile Int {
+  c ↦ "int";
+};
+
+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);
+
+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
+--------------------------------------------------------------------------------
+
+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 ∷;
+inductive 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 ×;
+inductive × (A : Type) (B : Type) {
+  , : A → B → A × B;
+};
+
+--------------------------------------------------------------------------------
+-- Maybe
+--------------------------------------------------------------------------------
+
+inductive Maybe (A : Type) {
+ nothing : Maybe A;
+ just : A → Maybe A;
+};
+
+from-int : Int → Maybe Int;
+from-int i ≔ if (i < 0) 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 (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 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
+        (change-from-key key < 0)
+        -- 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))
+        (0 , false);
+
+check-result : Int × Bool → Bool;
+check-result (change , all-checked) ≔ (change ==Int 0) && all-checked;
+
+vp : String → List String → List String → Bool;
+vp token keys-changed verifiers ≔
+    check-result
+        (foldl
+            (check-keys token verifiers)
+            (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;

tests/positive/MiniC/SimpleFungibleTokenImplicit/expected.golden

@@ -0,0 +1 @@
+VP Status: OK