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/ValidityPredicates/Data/Bool.mjuvix → 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/ValidityPredicates/Data/Int.mjuvix → 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/ValidityPredicates/Data/Maybe.mjuvix → 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/ValidityPredicates/Data/Pair.mjuvix → 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/ValidityPredicates/Data/String.mjuvix → 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/ValidityPredicates/System/IO.mjuvix → 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