Updates tests to use the updated standard library (#253)

* Updates tests to use the updated stdlib

* Update to minijuvix-stdlib main

examples/milestone/MiniTicTacToe/Data

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

examples/milestone/MiniTicTacToe/MiniTicTacToe.mjuvix

@@ -1,17 +1,23 @@
 module MiniTicTacToe;
 
-import Prelude;
-open Prelude;
+open import Stdlib.Data.Nat.Ord;
+open import Stdlib.Prelude;
 
 --------------------------------------------------------------------------------
 -- Render Utils
 --------------------------------------------------------------------------------
 
+infixr 5 ++str;
+axiom ++str : String → String → String;
+compile ++str {
+  c ↦ "concat";
+};
+
 concat : List String → String;
-concat ≔ foldl (++) "";
+concat ≔ foldl (++str) "";
 
 surround : String → List String → List String;
-surround x xs ≔ concatList (x ∷ intersperse x xs) (x ∷ nil);
+surround x xs ≔ (x ∷ intersperse x xs) ++ (x ∷ nil);
 
 intercalate : String → List String → String;
 intercalate sep xs ≔ concat (intersperse sep xs);
@@ -46,18 +52,18 @@ showSymbol X ≔ "X";
 --------------------------------------------------------------------------------
 
 inductive Square {
-  empty : Nat → Square;
+  empty : ℕ → Square;
   occupied : Symbol → Square;
 };
 
 ==Square : Square → Square → Bool;
-==Square (empty m) (empty n) ≔ ==Nat m n;
+==Square (empty m) (empty n) ≔ 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 ++ " ";
+showSquare (empty n) ≔ " " ++str natToStr n ++str " ";
+showSquare (occupied s) ≔ " " ++str showSymbol s ++str " ";
 
 --------------------------------------------------------------------------------
 -- Board
@@ -67,7 +73,7 @@ inductive Board {
   board : List (List Square) → Board;
 };
 
-possibleMoves : List Square → List Nat;
+possibleMoves : List Square → List ℕ;
 possibleMoves nil ≔ nil;
 possibleMoves ((empty n) ∷ xs) ≔ n ∷ possibleMoves xs;
 possibleMoves (_ ∷ xs) ≔ possibleMoves xs;
@@ -121,7 +127,7 @@ beginState ≔ state
      noError;
 
 won : GameState → Bool;
-won (state (board squares) _ _) ≔ any full (concatList (diagonals squares) (concatList (rows squares) (columns squares)));
+won (state (board squares) _ _) ≔ any full (diagonals squares ++ rows squares ++ columns squares);
 
 draw : GameState → Bool;
 draw (state (board squares) _ _) ≔ null (possibleMoves (flatten squares));
@@ -130,62 +136,68 @@ 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 : Symbol → ℕ → Square → Square;
+replace player k (empty n) ≔ if (n Stdlib.Data.Nat.Ord.== 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!")))
+     (state b p (terminate ("Player " ++str (showSymbol (switch p)) ++str " 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 : Maybe ℕ → 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))))
+    if (not (elem (==) 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
+-- IO Utils
 --------------------------------------------------------------------------------
 
+axiom readline : String;
+compile readline {
+  c ↦ "readline()";
+};
+
 axiom parsePositiveInt : String → Int;
 
 compile parsePositiveInt {
   c ↦ "parsePositiveInt";
 };
 
-positiveInt : Int → Maybe Int;
-positiveInt i ≔ if (i < 0) nothing (just i);
+--------------------------------------------------------------------------------
+-- IO
+--------------------------------------------------------------------------------
 
-validMove : Nat → Maybe Nat;
-validMove n ≔ if ((n <=Nat nine) && (n >=Nat one)) (just n) nothing;
+validMove : ℕ → Maybe ℕ;
+validMove n ≔ if ((n <= nine) && (n >= one)) (just n) nothing;
 
-getMove : Maybe Nat;
-getMove ≔ bindMaybe validMove (fmapMaybe from-backendNat (positiveInt (parsePositiveInt (readline))));
+getMove : Maybe ℕ;
+getMove ≔ validMove (from-backendNat (parsePositiveInt (readline)));
 
-do : Action × GameState -> GameState;
+do : IO × GameState -> GameState;
 do (_ , s) ≔ playMove getMove s;
 
 prompt : GameState → String;
-prompt x ≔ "\n" ++ (showGameState x) ++ "\nPlayer " ++ showSymbol (player x) ++ ": ";
+prompt x ≔ "\n" ++str (showGameState x) ++str "\nPlayer " ++str showSymbol (player x) ++str ": ";
 
 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 : (IO × GameState → GameState) → GameState → IO;
+run _ (state b p (terminate msg)) ≔ putStrLn ("\n" ++str (showGameState (state b p noError)) ++str "\n" ++str msg);
+run f (state b p (continue msg)) ≔ run f (f (putStr (msg ++str 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 : IO;
 main ≔ putStrLn welcome >> run do beginState;
 end;

examples/milestone/MiniTicTacToe/Prelude.mjuvix

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

examples/milestone/MiniTicTacToe/System

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

minijuvix-stdlib

@@ -1 +1 @@
-Subproject commit eab18bdae0195ea2ca395379f66d93cd3b762a0f
+Subproject commit 23515f6c295235bf51d828287db56e0b51c67582

src/MiniJuvix/Translation/MonoJuvixToMiniC.hs

@@ -436,7 +436,7 @@ goAxiom a
       Member (Reader Mono.CompileInfoTable) r =>
       NameId ->
       Sem r [BackendItem]
-    lookupBackends f = (^. S.compileInfoBackendItems) . HashMap.lookupDefault impossible f <$> ask
+    lookupBackends f = (^. S.compileInfoBackendItems) . HashMap.lookupDefault (error (show (a ^. Mono.axiomName))) f <$> ask
 
 goForeign :: ForeignBlock -> [CCode]
 goForeign b = case b ^. foreignBackend of

test/BackendC/Examples.hs

@@ -9,7 +9,8 @@ data ExampleTest = ExampleTest
     _relDir :: FilePath,
     _mainFile :: FilePath,
     _expectedDir :: FilePath,
-    _stdinText :: Text
+    _stdinText :: Text,
+    _stdlibMode :: StdlibMode
   }
 
 makeLenses ''ExampleTest
@@ -24,7 +25,7 @@ testDescr ExampleTest {..} =
    in TestDescr
         { _testName = _name,
           _testRoot = mainRoot,
-          _testAssertion = Steps $ clangAssertion StdlibExclude _mainFile expectedFile _stdinText
+          _testAssertion = Steps $ clangAssertion _stdlibMode _mainFile expectedFile _stdinText
         }
 
 allTests :: TestTree
@@ -35,6 +36,6 @@ allTests =
 
 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"
+  [ ExampleTest "Validity Predicate example" "ValidityPredicates" "Tests.mjuvix" "ValidityPredicates" "" StdlibExclude,
+    ExampleTest "MiniTicTacToe example" "MiniTicTacToe" "MiniTicTacToe.mjuvix" "MiniTicTacToe" "aaa\n0\n10\n1\n2\n3\n3\n4\n5\n6\n7\n8\n9\n" StdlibInclude
   ]

test/Scope/Negative.hs

@@ -219,7 +219,7 @@ filesErrorTests =
   [ NegTest
       "A module that conflicts with a module in the stdlib"
       "StdlibConflict"
-      "Data/Bool.mjuvix"
+      "Stdlib/Data/Bool.mjuvix"
       $ \case
         FilesError {} -> Nothing,
     NegTest

tests/negative/230/Foo/Data/Bool.mjuvix

@@ -1,8 +1,6 @@
 module Foo.Data.Bool;
 
-open import Prelude;
-
-import Data.Bool;
+import Stdlib.Data.Bool;
 
   inductive Bool {
     true : Bool;

tests/negative/230/Prod.mjuvix

@@ -1,6 +1,6 @@
 module Prod;
 
-open import Prelude;
+open import Stdlib.Prelude;
 open import Foo;
      import Foo.Data.Bool;
 

tests/negative/StdlibConflict/Data/Bool.mjuvix

@@ -1,3 +0,0 @@
-module Data.Bool;
-
-end;

tests/negative/StdlibConflict/Input.mjuvix

@@ -1,5 +1,5 @@
 module Input;
 
-open import Data.Bool;
+open import Stdlib.Data.Bool;
 
 end;

tests/negative/StdlibConflict/Stdlib/Data/Bool.mjuvix

@@ -0,0 +1,3 @@
+module Stdlib.Data.Bool;
+
+end;

tests/positive/MiniC/StdlibImport/Input.mjuvix

@@ -2,85 +2,11 @@ module Input;
 
 
 -- import from stdlib
-open import Data.Nat;
+open import Stdlib.Data.String;
+open import Stdlib.Data.Nat;
+open import Stdlib.System.IO;
 
-
---------------------------------------------------------------------------------
--- Strings
---------------------------------------------------------------------------------
-
-axiom String : Type;
-
-compile String {
-  c ↦ "char*";
-};
-
-
---------------------------------------------------------------------------------
--- Integers
---------------------------------------------------------------------------------
-
-axiom Int : Type;
-
-compile Int {
-  c ↦ "int";
-};
-
-foreign c {
-  int plus(int l, int r) {
-    return l + r;
-  \}
-};
-
-infixl 6 +int;
-axiom +int : Int -> Int -> Int;
-
-compile +int {
-  c ↦ "plus";
-};
-
-axiom intToStr : Int → String;
-
-compile intToStr {
-  c ↦ "intToStr";
-};
-
-natToInt : ℕ → Int;
-natToInt zero ≔ 0;
-natToInt (suc n) ≔ 1 +int (natToInt n);
-
-natToStr : ℕ → String;
-natToStr n ≔ intToStr (natToInt n);
-
-
---------------------------------------------------------------------------------
--- IO
---------------------------------------------------------------------------------
-
-axiom Action : Type;
-
-compile Action {
-  c ↦ "int";
-};
-
-axiom putStrLn : String → Action;
-
-compile putStrLn {
-  c ↦ "putStrLn";
-};
-
-
---------------------------------------------------------------------------------
--- IO
---------------------------------------------------------------------------------
-
-two : ℕ;
-two ≔ suc (suc zero);
-
-three : ℕ;
-three ≔ two + (suc zero);
-
-main : Action;
+main : IO;
 main ≔ putStrLn (natToStr (two + three));
 
 end;

tests/positive/StdlibImport/StdlibImport.mjuvix

@@ -1,8 +1,7 @@
 module StdlibImport;
 
-open import Prelude;
+open import Stdlib.Prelude;
 
-open import Data.Nat;
 import A;
 
 two : ℕ;