diff --git a/examples/milestone/ValidityPredicates/Data/Bool.mjuvix b/examples/milestone/Lib/Data/Bool.mjuvix similarity index 95% rename from examples/milestone/ValidityPredicates/Data/Bool.mjuvix rename to examples/milestone/Lib/Data/Bool.mjuvix index 77701e45cf..b114391573 100644 --- a/examples/milestone/ValidityPredicates/Data/Bool.mjuvix +++ b/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; diff --git a/examples/milestone/ValidityPredicates/Data/Int.mjuvix b/examples/milestone/Lib/Data/Int.mjuvix similarity index 88% rename from examples/milestone/ValidityPredicates/Data/Int.mjuvix rename to examples/milestone/Lib/Data/Int.mjuvix index 30c0025510..ad8146f4d4 100644 --- a/examples/milestone/ValidityPredicates/Data/Int.mjuvix +++ 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; diff --git a/examples/milestone/Lib/Data/List.mjuvix b/examples/milestone/Lib/Data/List.mjuvix new file mode 100644 index 0000000000..fce80d369a --- /dev/null +++ b/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; diff --git a/examples/milestone/ValidityPredicates/Data/Maybe.mjuvix b/examples/milestone/Lib/Data/Maybe.mjuvix similarity index 50% rename from examples/milestone/ValidityPredicates/Data/Maybe.mjuvix rename to examples/milestone/Lib/Data/Maybe.mjuvix index 6c6f0736a3..f937ffff36 100644 --- a/examples/milestone/ValidityPredicates/Data/Maybe.mjuvix +++ b/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; diff --git a/examples/milestone/Lib/Data/Nat.mjuvix b/examples/milestone/Lib/Data/Nat.mjuvix new file mode 100644 index 0000000000..ae25fb874f --- /dev/null +++ b/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 l r ≔ (l =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; diff --git a/examples/milestone/ValidityPredicates/Data/Pair.mjuvix b/examples/milestone/Lib/Data/Pair.mjuvix similarity index 62% rename from examples/milestone/ValidityPredicates/Data/Pair.mjuvix rename to examples/milestone/Lib/Data/Pair.mjuvix index 3bd4ceb696..3ce96ef039 100644 --- a/examples/milestone/ValidityPredicates/Data/Pair.mjuvix +++ b/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; diff --git a/examples/milestone/ValidityPredicates/Data/String.mjuvix b/examples/milestone/Lib/Data/String.mjuvix similarity index 71% rename from examples/milestone/ValidityPredicates/Data/String.mjuvix rename to examples/milestone/Lib/Data/String.mjuvix index ad0796120f..27313f29c7 100644 --- a/examples/milestone/ValidityPredicates/Data/String.mjuvix +++ b/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; diff --git a/examples/milestone/Lib/Prelude.mjuvix b/examples/milestone/Lib/Prelude.mjuvix new file mode 100644 index 0000000000..1ee803161f --- /dev/null +++ b/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; diff --git a/examples/milestone/ValidityPredicates/System/IO.mjuvix b/examples/milestone/Lib/System/IO.mjuvix similarity index 89% rename from examples/milestone/ValidityPredicates/System/IO.mjuvix rename to examples/milestone/Lib/System/IO.mjuvix index 3a839f97d7..fe4a6f425f 100644 --- a/examples/milestone/ValidityPredicates/System/IO.mjuvix +++ b/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; diff --git a/examples/milestone/Lib/minijuvix.yaml b/examples/milestone/Lib/minijuvix.yaml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/examples/milestone/MiniTicTacToe/Data b/examples/milestone/MiniTicTacToe/Data new file mode 120000 index 0000000000..6e2a68d952 --- /dev/null +++ b/examples/milestone/MiniTicTacToe/Data @@ -0,0 +1 @@ +../Lib/Data \ No newline at end of file diff --git a/examples/milestone/MiniTicTacToe/MiniTicTacToe.mjuvix b/examples/milestone/MiniTicTacToe/MiniTicTacToe.mjuvix new file mode 100644 index 0000000000..f0ab6aab36 --- /dev/null +++ b/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; diff --git a/examples/milestone/MiniTicTacToe/Prelude.mjuvix b/examples/milestone/MiniTicTacToe/Prelude.mjuvix new file mode 120000 index 0000000000..8fde4860a9 --- /dev/null +++ b/examples/milestone/MiniTicTacToe/Prelude.mjuvix @@ -0,0 +1 @@ +../Lib/Prelude.mjuvix \ No newline at end of file diff --git a/examples/milestone/MiniTicTacToe/System b/examples/milestone/MiniTicTacToe/System new file mode 120000 index 0000000000..b0eacaa004 --- /dev/null +++ b/examples/milestone/MiniTicTacToe/System @@ -0,0 +1 @@ +../Lib/System \ No newline at end of file diff --git a/examples/milestone/MiniTicTacToe/minijuvix.yaml b/examples/milestone/MiniTicTacToe/minijuvix.yaml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/examples/milestone/ValidityPredicates/Data b/examples/milestone/ValidityPredicates/Data new file mode 120000 index 0000000000..6e2a68d952 --- /dev/null +++ b/examples/milestone/ValidityPredicates/Data @@ -0,0 +1 @@ +../Lib/Data \ No newline at end of file diff --git a/examples/milestone/ValidityPredicates/Data/List.mjuvix b/examples/milestone/ValidityPredicates/Data/List.mjuvix deleted file mode 100644 index 0cb615658b..0000000000 --- a/examples/milestone/ValidityPredicates/Data/List.mjuvix +++ /dev/null @@ -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; diff --git a/examples/milestone/ValidityPredicates/Prelude.mjuvix b/examples/milestone/ValidityPredicates/Prelude.mjuvix deleted file mode 100644 index ab66ee0ca2..0000000000 --- a/examples/milestone/ValidityPredicates/Prelude.mjuvix +++ /dev/null @@ -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; diff --git a/examples/milestone/ValidityPredicates/Prelude.mjuvix b/examples/milestone/ValidityPredicates/Prelude.mjuvix new file mode 120000 index 0000000000..8fde4860a9 --- /dev/null +++ b/examples/milestone/ValidityPredicates/Prelude.mjuvix @@ -0,0 +1 @@ +../Lib/Prelude.mjuvix \ No newline at end of file diff --git a/examples/milestone/ValidityPredicates/System b/examples/milestone/ValidityPredicates/System new file mode 120000 index 0000000000..b0eacaa004 --- /dev/null +++ b/examples/milestone/ValidityPredicates/System @@ -0,0 +1 @@ +../Lib/System \ No newline at end of file diff --git a/minic-runtime/libc/minic-runtime.h b/minic-runtime/libc/minic-runtime.h index 672be33ae4..7a390b7b3c 100644 --- a/minic-runtime/libc/minic-runtime.h +++ b/minic-runtime/libc/minic-runtime.h @@ -3,6 +3,7 @@ #include #include +#include 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_ diff --git a/minic-runtime/standalone/minic-runtime.h b/minic-runtime/standalone/minic-runtime.h index 7ddf455b0a..a82750c4b7 100644 --- a/minic-runtime/standalone/minic-runtime.h +++ b/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_ diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs index 6d7a662ffc..d96932f7a4 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs +++ b/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, diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs index 980bf66e8f..c60a57c152 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs +++ b/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 () diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs index d40dd3f8e9..933ccbc917 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs +++ b/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 diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs index 61386ffbeb..d2f1e71a09 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs +++ b/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 diff --git a/src/MiniJuvix/Syntax/MiniC/Language.hs b/src/MiniJuvix/Syntax/MiniC/Language.hs index 42d32abe0a..0b5bef7f65 100644 --- a/src/MiniJuvix/Syntax/MiniC/Language.hs +++ b/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 diff --git a/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs b/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs index f11dd2188c..beb8cc2772 100644 --- a/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs +++ b/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 diff --git a/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix/TypePropagation.hs b/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix/TypePropagation.hs index 35e01348a9..1016701a92 100644 --- a/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix/TypePropagation.hs +++ b/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 diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC.hs index efec6db4e9..244842c776 100644 --- a/src/MiniJuvix/Translation/MonoJuvixToMiniC.hs +++ b/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 + concatMapM (applyOnFunStatement goFunctionDef) _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 +isNullary :: Text -> CFunType -> Bool +isNullary funName funType = null (funType ^. cFunArgTypes) && funName /= Str.main_ -mkArgs :: (Text -> Text) -> [Text] -mkArgs f = map (f . show) [0 :: Integer ..] +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) -funArgs :: [Text] -funArgs = mkArgs asFunArg + baseFunType :: CFunType + baseFunType = typeToFunType _funDefType -ctorArgs :: [Text] -ctorArgs = mkArgs asCtorArg + funType :: CFunType + funType = + if + | nPatterns == length (baseFunType ^. cFunArgTypes) -> baseFunType + | otherwise -> + CFunType + { _cFunArgTypes = take nPatterns (baseFunType ^. cFunArgTypes), + _cFunReturnType = declFunctionPtrType + } -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) + funIsNullary :: Bool + funIsNullary = isNullary funcBasename funType -isNullary :: Text -> CFunType -> Bool -isNullary funName funType = null (funType ^. cFunArgTypes) && funName /= Str.main_ + funcBasename :: Text + funcBasename = mkName _funDefName -cFunTypeToFunSig :: Text -> CFunType -> FunctionSig -cFunTypeToFunSig name CFunType {..} = - FunctionSig - { _funcReturnType = _cFunReturnType ^. typeDeclType, - _funcIsPtr = _cFunReturnType ^. typeIsPtr, - _funcQualifier = None, - _funcName = name, - _funcArgs = namedArgs asFunArg _cFunArgTypes - } + funName :: Text + funName = + if + | funIsNullary -> asNullary funcBasename + | otherwise -> funcBasename genFunctionSig :: Mono.FunctionDef -> [CCode] -genFunctionSig Mono.FunctionDef {..} = - [ExternalFuncSig (cFunTypeToFunSig funName funType)] +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 = typeToFunType _funDefType + 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,9 +325,38 @@ 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 - idenExp <- goIden iden - return $ functionCall idenExp (reverse fArgs) + (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 f :: Sem r (Mono.Iden, [Expression]) f = unfoldApp a @@ -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,10 +423,29 @@ mkInductiveName i = mkName (i ^. Mono.inductiveName) mkInductiveConstructorNames :: Mono.InductiveDef -> [Text] mkInductiveConstructorNames i = mkName . view Mono.constructorName <$> i ^. Mono.inductiveConstructors +mkInductiveTypeDef :: Mono.InductiveDef -> [CCode] +mkInductiveTypeDef i = + [ExternalDecl structTypeDef] + where + structTypeDef :: Declaration + structTypeDef = + typeDefWrap + (asTypeDef baseName) + ( DeclStructUnion + ( StructUnion + { _structUnionTag = StructTag, + _structUnionName = Just (asStruct baseName), + _structMembers = Nothing + } + ) + ) + + baseName :: Text + baseName = mkName (i ^. Mono.inductiveName) + goInductiveDef :: Mono.InductiveDef -> [CCode] goInductiveDef i = - [ ExternalDecl structTypeDef, - ExternalDecl tagsType + [ ExternalDecl tagsType ] <> (i ^. Mono.inductiveConstructors >>= goInductiveConstructorDef) <> [ExternalDecl inductiveDecl] @@ -655,19 +459,6 @@ goInductiveDef i = constructorNames :: [Text] constructorNames = mkInductiveConstructorNames i - structTypeDef :: Declaration - structTypeDef = - typeDefWrap - (asTypeDef baseName) - ( DeclStructUnion - ( StructUnion - { _structUnionTag = StructTag, - _structUnionName = Just (asStruct baseName), - _structMembers = Nothing - } - ) - ) - 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)} diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/Base.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/Base.hs new file mode 100644 index 0000000000..0ec56f7345 --- /dev/null +++ b/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)) diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/CBuilder.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/CBuilder.hs new file mode 100644 index 0000000000..c41554758d --- /dev/null +++ b/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 + } diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/CNames.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/CNames.hs new file mode 100644 index 0000000000..36ded0c345 --- /dev/null +++ b/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 diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/Closure.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/Closure.hs new file mode 100644 index 0000000000..0b78f92c97 --- /dev/null +++ b/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)) diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/Types.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/Types.hs new file mode 100644 index 0000000000..4ce198310d --- /dev/null +++ b/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 diff --git a/test/BackendC.hs b/test/BackendC.hs index 256824b05a..e9f4aff0eb 100644 --- a/test/BackendC.hs +++ b/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] diff --git a/test/BackendC/Base.hs b/test/BackendC/Base.hs new file mode 100644 index 0000000000..bf13ce3c00 --- /dev/null +++ b/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) diff --git a/test/BackendC/Examples.hs b/test/BackendC/Examples.hs new file mode 100644 index 0000000000..afd183fc75 --- /dev/null +++ b/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" + ] diff --git a/test/BackendC/Positive.hs b/test/BackendC/Positive.hs index fd6c555fb4..79e158cedb 100644 --- a/test/BackendC/Positive.hs +++ b/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" ] diff --git a/tests/CLI/Commands/html.test b/tests/CLI/Commands/html.test index 1c94f5ee6f..4c5ae99a7b 100644 --- a/tests/CLI/Commands/html.test +++ b/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 > /.*/ >= 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 ->= 0 \ No newline at end of file +$ 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 diff --git a/tests/examplesExpected/MiniTicTacToe/expected.golden b/tests/examplesExpected/MiniTicTacToe/expected.golden new file mode 100644 index 0000000000..24e6533d83 --- /dev/null +++ b/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! diff --git a/tests/examplesExpected/ValidityPredicates/expected.golden b/tests/examplesExpected/ValidityPredicates/expected.golden new file mode 100644 index 0000000000..7440ad4fd8 --- /dev/null +++ b/tests/examplesExpected/ValidityPredicates/expected.golden @@ -0,0 +1 @@ +VP Status: OK diff --git a/tests/positive/MiniC/ClosureEnv/Data b/tests/positive/MiniC/ClosureEnv/Data new file mode 120000 index 0000000000..6e2a68d952 --- /dev/null +++ b/tests/positive/MiniC/ClosureEnv/Data @@ -0,0 +1 @@ +../Lib/Data \ No newline at end of file diff --git a/tests/positive/MiniC/ClosureEnv/Input.mjuvix b/tests/positive/MiniC/ClosureEnv/Input.mjuvix new file mode 100644 index 0000000000..6adff67d40 --- /dev/null +++ b/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; diff --git a/tests/positive/MiniC/ClosureEnv/Prelude.mjuvix b/tests/positive/MiniC/ClosureEnv/Prelude.mjuvix new file mode 120000 index 0000000000..8fde4860a9 --- /dev/null +++ b/tests/positive/MiniC/ClosureEnv/Prelude.mjuvix @@ -0,0 +1 @@ +../Lib/Prelude.mjuvix \ No newline at end of file diff --git a/tests/positive/MiniC/ClosureEnv/expected.golden b/tests/positive/MiniC/ClosureEnv/expected.golden new file mode 100644 index 0000000000..2fab3ac3d0 --- /dev/null +++ b/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 diff --git a/tests/positive/MiniC/ClosureEnv/minijuvix.yaml b/tests/positive/MiniC/ClosureEnv/minijuvix.yaml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/positive/MiniC/ClosureNoEnv/Data b/tests/positive/MiniC/ClosureNoEnv/Data new file mode 120000 index 0000000000..6e2a68d952 --- /dev/null +++ b/tests/positive/MiniC/ClosureNoEnv/Data @@ -0,0 +1 @@ +../Lib/Data \ No newline at end of file diff --git a/tests/positive/MiniC/ClosureNoEnv/IO.mjuvix b/tests/positive/MiniC/ClosureNoEnv/IO.mjuvix deleted file mode 120000 index 69140ff667..0000000000 --- a/tests/positive/MiniC/ClosureNoEnv/IO.mjuvix +++ /dev/null @@ -1 +0,0 @@ -../MultiModules/IO.mjuvix \ No newline at end of file diff --git a/tests/positive/MiniC/ClosureNoEnv/Input.mjuvix b/tests/positive/MiniC/ClosureNoEnv/Input.mjuvix index 0c49d2f29d..230d357eba 100644 --- a/tests/positive/MiniC/ClosureNoEnv/Input.mjuvix +++ b/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; diff --git a/tests/positive/MiniC/ClosureNoEnv/Prelude.mjuvix b/tests/positive/MiniC/ClosureNoEnv/Prelude.mjuvix new file mode 120000 index 0000000000..8fde4860a9 --- /dev/null +++ b/tests/positive/MiniC/ClosureNoEnv/Prelude.mjuvix @@ -0,0 +1 @@ +../Lib/Prelude.mjuvix \ No newline at end of file diff --git a/tests/positive/MiniC/ClosureNoEnv/String.mjuvix b/tests/positive/MiniC/ClosureNoEnv/String.mjuvix deleted file mode 120000 index 0d14cb32ec..0000000000 --- a/tests/positive/MiniC/ClosureNoEnv/String.mjuvix +++ /dev/null @@ -1 +0,0 @@ -../MultiModules/String.mjuvix \ No newline at end of file diff --git a/tests/positive/MiniC/Lib/Data/Bool.mjuvix b/tests/positive/MiniC/Lib/Data/Bool.mjuvix new file mode 100644 index 0000000000..f4b1314f3f --- /dev/null +++ b/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; diff --git a/tests/positive/MiniC/MultiModules/IO.mjuvix b/tests/positive/MiniC/Lib/Data/IO.mjuvix similarity index 89% rename from tests/positive/MiniC/MultiModules/IO.mjuvix rename to tests/positive/MiniC/Lib/Data/IO.mjuvix index 84c8775c8b..c4d5372731 100644 --- a/tests/positive/MiniC/MultiModules/IO.mjuvix +++ b/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; diff --git a/tests/positive/MiniC/Lib/Data/Int.mjuvix b/tests/positive/MiniC/Lib/Data/Int.mjuvix new file mode 100644 index 0000000000..91becf5eda --- /dev/null +++ b/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; diff --git a/tests/positive/MiniC/Lib/Data/Nat.mjuvix b/tests/positive/MiniC/Lib/Data/Nat.mjuvix new file mode 100644 index 0000000000..0f6d127057 --- /dev/null +++ b/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; diff --git a/tests/positive/MiniC/MultiModules/Pair.mjuvix b/tests/positive/MiniC/Lib/Data/Pair.mjuvix similarity index 90% rename from tests/positive/MiniC/MultiModules/Pair.mjuvix rename to tests/positive/MiniC/Lib/Data/Pair.mjuvix index 17b81eb546..190bb55c85 100644 --- a/tests/positive/MiniC/MultiModules/Pair.mjuvix +++ b/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; diff --git a/tests/positive/MiniC/MultiModules/String.mjuvix b/tests/positive/MiniC/Lib/Data/String.mjuvix similarity index 81% rename from tests/positive/MiniC/MultiModules/String.mjuvix rename to tests/positive/MiniC/Lib/Data/String.mjuvix index c7209cd629..a3e1dc91c9 100644 --- a/tests/positive/MiniC/MultiModules/String.mjuvix +++ b/tests/positive/MiniC/Lib/Data/String.mjuvix @@ -1,4 +1,4 @@ -module String; +module Data.String; axiom String : Type; diff --git a/tests/positive/MiniC/Lib/Prelude.mjuvix b/tests/positive/MiniC/Lib/Prelude.mjuvix new file mode 100644 index 0000000000..17f55c867e --- /dev/null +++ b/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; diff --git a/tests/positive/MiniC/Lib/minijuvix.yaml b/tests/positive/MiniC/Lib/minijuvix.yaml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/positive/MiniC/MultiModules/Bool.mjuvix b/tests/positive/MiniC/MultiModules/Bool.mjuvix deleted file mode 100644 index 8c54f17b33..0000000000 --- a/tests/positive/MiniC/MultiModules/Bool.mjuvix +++ /dev/null @@ -1,9 +0,0 @@ -module Bool; - -inductive Bool { - true : Bool; - false : Bool; -}; - - -end; diff --git a/tests/positive/MiniC/MultiModules/Data b/tests/positive/MiniC/MultiModules/Data new file mode 120000 index 0000000000..6e2a68d952 --- /dev/null +++ b/tests/positive/MiniC/MultiModules/Data @@ -0,0 +1 @@ +../Lib/Data \ No newline at end of file diff --git a/tests/positive/MiniC/MultiModules/Input.mjuvix b/tests/positive/MiniC/MultiModules/Input.mjuvix index 2446ff75fd..ceebfba7b6 100644 --- a/tests/positive/MiniC/MultiModules/Input.mjuvix +++ b/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; diff --git a/tests/positive/MiniC/MultiModules/Prelude.mjuvix b/tests/positive/MiniC/MultiModules/Prelude.mjuvix deleted file mode 100644 index c309af1bbd..0000000000 --- a/tests/positive/MiniC/MultiModules/Prelude.mjuvix +++ /dev/null @@ -1,11 +0,0 @@ -module Prelude; - -open import String public; - -open import Bool public; - -open import Pair public; - -open import IO public; - -end; diff --git a/tests/positive/MiniC/MultiModules/Prelude.mjuvix b/tests/positive/MiniC/MultiModules/Prelude.mjuvix new file mode 120000 index 0000000000..8fde4860a9 --- /dev/null +++ b/tests/positive/MiniC/MultiModules/Prelude.mjuvix @@ -0,0 +1 @@ +../Lib/Prelude.mjuvix \ No newline at end of file diff --git a/tests/positive/MiniC/MutuallyRecursive/Data b/tests/positive/MiniC/MutuallyRecursive/Data new file mode 120000 index 0000000000..6e2a68d952 --- /dev/null +++ b/tests/positive/MiniC/MutuallyRecursive/Data @@ -0,0 +1 @@ +../Lib/Data \ No newline at end of file diff --git a/tests/positive/MiniC/MutuallyRecursive/Input.mjuvix b/tests/positive/MiniC/MutuallyRecursive/Input.mjuvix new file mode 100644 index 0000000000..0908f539b3 --- /dev/null +++ b/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; diff --git a/tests/positive/MiniC/MutuallyRecursive/Prelude.mjuvix b/tests/positive/MiniC/MutuallyRecursive/Prelude.mjuvix new file mode 120000 index 0000000000..8fde4860a9 --- /dev/null +++ b/tests/positive/MiniC/MutuallyRecursive/Prelude.mjuvix @@ -0,0 +1 @@ +../Lib/Prelude.mjuvix \ No newline at end of file diff --git a/tests/positive/MiniC/MutuallyRecursive/expected.golden b/tests/positive/MiniC/MutuallyRecursive/expected.golden new file mode 100644 index 0000000000..0394cc0413 --- /dev/null +++ b/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 diff --git a/tests/positive/MiniC/MutuallyRecursive/minijuvix.yaml b/tests/positive/MiniC/MutuallyRecursive/minijuvix.yaml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/positive/MiniC/NestedList/Data b/tests/positive/MiniC/NestedList/Data new file mode 120000 index 0000000000..6e2a68d952 --- /dev/null +++ b/tests/positive/MiniC/NestedList/Data @@ -0,0 +1 @@ +../Lib/Data \ No newline at end of file diff --git a/tests/positive/MiniC/NestedList/Input.mjuvix b/tests/positive/MiniC/NestedList/Input.mjuvix new file mode 100644 index 0000000000..94f7e2717c --- /dev/null +++ b/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; diff --git a/tests/positive/MiniC/NestedList/Prelude.mjuvix b/tests/positive/MiniC/NestedList/Prelude.mjuvix new file mode 120000 index 0000000000..8fde4860a9 --- /dev/null +++ b/tests/positive/MiniC/NestedList/Prelude.mjuvix @@ -0,0 +1 @@ +../Lib/Prelude.mjuvix \ No newline at end of file diff --git a/tests/positive/MiniC/NestedList/expected.golden b/tests/positive/MiniC/NestedList/expected.golden new file mode 100644 index 0000000000..481748b612 --- /dev/null +++ b/tests/positive/MiniC/NestedList/expected.golden @@ -0,0 +1 @@ +no errors diff --git a/tests/positive/MiniC/NestedList/minijuvix.yaml b/tests/positive/MiniC/NestedList/minijuvix.yaml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.mjuvix b/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.mjuvix new file mode 100644 index 0000000000..5ecd0dc659 --- /dev/null +++ b/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; diff --git a/tests/positive/MiniC/SimpleFungibleTokenImplicit/expected.golden b/tests/positive/MiniC/SimpleFungibleTokenImplicit/expected.golden new file mode 100644 index 0000000000..7440ad4fd8 --- /dev/null +++ b/tests/positive/MiniC/SimpleFungibleTokenImplicit/expected.golden @@ -0,0 +1 @@ +VP Status: OK diff --git a/tests/positive/MiniC/SimpleFungibleTokenImplicit/minijuvix.yaml b/tests/positive/MiniC/SimpleFungibleTokenImplicit/minijuvix.yaml new file mode 100644 index 0000000000..e69de29bb2