adapt examples & fix tests

c-runtime/wasi-libc/c-runtime.h

@@ -102,7 +102,7 @@ prim_io prim_printString(prim_string s) { return putStr(s); }
 prim_io prim_printBool(prim_bool b) { return putStr(b ? "true" : "false"); }
 
 prim_io prim_readline(juvix_function_t* f) {
-    ((prim_io(*)(juvix_function_t*, prim_string))f->fun)(f, readline());
+    return ((prim_io(*)(juvix_function_t*, prim_string))f->fun)(f, readline());
 }
 
 prim_string prim_natToString(prim_nat n) { return intToStr(n); }

c-runtime/wasi-standalone/c-runtime.h

@@ -259,7 +259,7 @@ char* readline() {
 }
 
 prim_io prim_readline(juvix_function_t* f) {
-    ((prim_io(*)(juvix_function_t*, prim_string))f->fun)(f, readline());
+    return ((prim_io(*)(juvix_function_t*, prim_string))f->fun)(f, readline());
 }
 
 prim_string prim_natToString(prim_nat n) { return intToStr(n); }

examples/milestone/Collatz/Collatz.juvix

@@ -23,20 +23,6 @@ module Collatz;
 
   -- IO
   --- -----------------------------------------------------------------------------
-  axiom readline : String;
-
-  compile readline {
-    c ↦ "readline()";
-  };
-
-  axiom parsePositiveInt : String → Nat;
-
-  compile parsePositiveInt {
-    c ↦ "parsePositiveInt";
-  };
-
-  getInitial : Nat;
-  getInitial := parsePositiveInt (readline);
 
   output : Nat → Nat × IO;
   output n := n , printNatLn n;
@@ -50,5 +36,5 @@ module Collatz;
   welcome := "Collatz calculator\n------------------\n\nType a number then ENTER";
 
   main : IO;
-  main := printStringLn welcome >> run collatz getInitial;
+  main := printStringLn welcome >> readLn (run collatz ∘ stringToNat);
 end;

examples/milestone/Hanoi/Hanoi.juvix

@@ -16,14 +16,6 @@
 module Hanoi;
   open import Stdlib.Prelude;
 
-  infixr 5 ++str;
-  --- Concatenation of ;String;s
-  axiom ++str : String → String → String;
-
-  compile ++str {
-    c ↦ "concat";
-  };
-
   --- Concatenates a list of strings
 
   --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
@@ -46,7 +38,7 @@ module Hanoi;
   --- Produce a ;String; representation of a ;List Nat;
   showList : List Nat → String;
   showList xs := "["
-    ++str intercalate "," (map natToStr xs)
+    ++str intercalate "," (map natToString xs)
     ++str "]";
 
   --- A Peg represents a peg in the towers of Hanoi game

examples/milestone/PascalsTriangle/PascalsTriangle.juvix

@@ -23,14 +23,6 @@ module PascalsTriangle;
   singleton : {A : Type} → A → List A;
   singleton a := a :: nil;
 
-  infixr 5 ++str;
-  --- Concatenation of ;String;s
-  axiom ++str : String → String → String;
-
-  compile ++str {
-    c ↦ "concat";
-  };
-
   --- Concatenates a list of strings
 
   --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
@@ -48,7 +40,7 @@ module PascalsTriangle;
 
   showList : List Nat → String;
   showList xs := "["
-    ++str intercalate "," (map natToStr xs)
+    ++str intercalate "," (map natToString xs)
     ++str "]";
 
   --- Compute the next row of Pascal's triangle

examples/milestone/TicTacToe/CLI/TicTacToe.juvix

@@ -12,25 +12,6 @@ module CLI.TicTacToe;
   open import Stdlib.Prelude;
   open import Logic.Game;
 
-  axiom readline : String;
-
-  compile readline {
-    c ↦ "readline()";
-  };
-
-  axiom parsePositiveInt : String → Nat;
-
-  compile parsePositiveInt {
-    c ↦ "parsePositiveInt";
-  };
-
-  --- Reads a ;Nat; from stdin
-  getMove : Maybe Nat;
-  getMove := validMove (parsePositiveInt (readline));
-
-  do : IO × GameState → GameState;
-  do (_ , s) := playMove getMove s;
-
   --- A ;String; that prompts the user for their input
   prompt : GameState → String;
   prompt x := "\n"
@@ -39,26 +20,26 @@ module CLI.TicTacToe;
     ++str showSymbol (player x)
     ++str ": ";
 
+  nextMove : GameState → String → GameState;
+  nextMove s := flip playMove s ∘ validMove ∘ stringToNat;
+
   --- Main loop
   terminating
-  run : (IO × GameState → GameState) → GameState → IO;
-  run _ (state b p (terminate msg)) := printStringLn
+  run : GameState → IO;
+  run (state b p (terminate msg)) := printStringLn
     ("\n"
     ++str showGameState (state b p noError)
     ++str "\n"
     ++str msg);
-  run f (state b p (continue msg)) := run
-    f
-    (f
-      (printString (msg ++str prompt (state b p noError))
-      , state b p noError));
-  run f x := run f (f (printString (prompt x) , x));
+  run (state b p (continue msg)) := printString (msg ++str prompt (state b p noError)) >>
+    readLn (run ∘ nextMove (state b p noError));
+  run x := printString (prompt x) >> readLn (run ∘ nextMove x);
 
   --- The welcome message
   welcome : String;
   welcome := "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";
 
   --- The entry point of the program
   main : IO;
-  main := printStringLn welcome >> run do beginState;
+  main := printStringLn welcome >> run beginState;
 end;

examples/milestone/TicTacToe/Logic/Extra.juvix

@@ -3,19 +3,9 @@ module Logic.Extra;
   open import Stdlib.Data.Nat.Ord;
   open import Stdlib.Prelude;
 
-  infixr 5 ++str;
-  --- Primitive concatenation of ;String;s
-  axiom ++str : String → String → String;
-
-  compile ++str {
-    c ↦ "concat";
-  };
-
   --- Concatenates a list of strings
 
-  --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
-  :: "b"
-  :: nil;
+  --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
   concat : List String → String;
   concat := foldl (++str) "";
 

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -19,7 +19,7 @@ module Logic.Square;
 
   --- Textual representation of a ;Square;
   showSquare : Square → String;
-  showSquare (empty n) := " " ++str natToStr n ++str " ";
+  showSquare (empty n) := " " ++str natToString n ++str " ";
   showSquare (occupied s) := " " ++str showSymbol s ++str " ";
 
   replace : Symbol → Nat → Square → Square;

examples/milestone/TicTacToe/Web/TicTacToe.juvix

@@ -99,7 +99,7 @@ module Web.TicTacToe;
 
   renderNumber : Nat → Nat → Nat → IO;
   renderNumber n row col := renderText
-    (natToStr n)
+    (natToString n)
     row
     col
     center;