mirror of
https://github.com/anoma/juvix.git
synced 2024-11-30 05:42:26 +03:00
Add a test suite for milestone examples (#1920)
In this PR I will add tests for the example programs in `examples/milestone`. There's currently an runtime assertion error generated by the Hanoi example https://github.com/anoma/juvix/issues/1919, so it'd be good to test these programs in the future.
This commit is contained in:
parent
86c18f37af
commit
4044676628
@ -1,42 +1,34 @@
|
||||
module Collatz;
|
||||
|
||||
open import Stdlib.Prelude;
|
||||
|
||||
mapMaybe :
|
||||
{A : Type} → {B : Type} → (A → B) → Maybe A → Maybe B;
|
||||
mapMaybe _ nothing := nothing;
|
||||
mapMaybe f (just x) := just (f x);
|
||||
|
||||
div2 : Nat → Maybe Nat;
|
||||
div2 zero := just zero;
|
||||
div2 (suc (suc n)) := mapMaybe suc (div2 n);
|
||||
div2 _ := nothing;
|
||||
open import Stdlib.Data.Nat.Ord;
|
||||
|
||||
collatzNext : Nat → Nat;
|
||||
collatzNext n := fromMaybe (suc (3 * n)) (div2 n);
|
||||
collatzNext n := if (mod n 2 == 0) (div n 2) (3 * n + 1);
|
||||
|
||||
collatz : Nat → Nat;
|
||||
collatz zero := zero;
|
||||
collatz (suc zero) := suc zero;
|
||||
collatz (suc (suc n)) := collatzNext (suc (suc n));
|
||||
|
||||
--- -----------------------------------------------------------------------------
|
||||
|
||||
-- IO
|
||||
--- -----------------------------------------------------------------------------
|
||||
output : Nat → Nat × IO;
|
||||
output n := n, printNatLn n;
|
||||
collatz n := collatzNext n;
|
||||
|
||||
terminating
|
||||
run : (Nat → Nat) → Nat → IO;
|
||||
run _ (suc zero) := printStringLn "Finished!";
|
||||
run f n := run f (fst (output (f n)));
|
||||
run _ (suc zero) :=
|
||||
printNatLn 1 >> printStringLn "Finished!";
|
||||
run f n := printNatLn n >> run f (f n);
|
||||
|
||||
welcome : String;
|
||||
welcome :=
|
||||
"Collatz calculator\n------------------\n\nType a number then ENTER";
|
||||
|
||||
resultHeading : String;
|
||||
resultHeading := "Collatz sequence:";
|
||||
|
||||
main : IO;
|
||||
main :=
|
||||
printStringLn welcome
|
||||
>> readLn (run collatz ∘ stringToNat);
|
||||
>> readLn
|
||||
λ {
|
||||
| s := printStringLn resultHeading
|
||||
>> run collatz (stringToNat s)
|
||||
};
|
||||
|
@ -10,4 +10,4 @@ fibonacci : Nat → Nat;
|
||||
fibonacci n := fib n 0 1;
|
||||
|
||||
main : IO;
|
||||
main := printNatLn (fibonacci 25);
|
||||
main := readLn (printNatLn ∘ fibonacci ∘ stringToNat);
|
||||
|
7
test/Examples.hs
Normal file
7
test/Examples.hs
Normal file
@ -0,0 +1,7 @@
|
||||
module Examples where
|
||||
|
||||
import Base
|
||||
import Examples.Positive qualified as P
|
||||
|
||||
allTests :: TestTree
|
||||
allTests = testGroup "Juvix milestone examples compilation tests" [P.allTests]
|
87
test/Examples/Positive.hs
Normal file
87
test/Examples/Positive.hs
Normal file
@ -0,0 +1,87 @@
|
||||
module Examples.Positive where
|
||||
|
||||
import Base
|
||||
import Compilation.Base
|
||||
|
||||
data PosTest = PosTest
|
||||
{ _name :: String,
|
||||
_dir :: Path Abs Dir,
|
||||
_file :: Path Abs File,
|
||||
_expectedFile :: Path Abs File,
|
||||
_stdin :: Text
|
||||
}
|
||||
|
||||
makeLenses ''PosTest
|
||||
|
||||
srcRoot :: Path Abs Dir
|
||||
srcRoot = relToProject $(mkRelDir "examples/")
|
||||
|
||||
expectedRoot :: Path Abs Dir
|
||||
expectedRoot = relToProject $(mkRelDir "tests/examplesExpected")
|
||||
|
||||
toTestDescr :: PosTest -> TestDescr
|
||||
toTestDescr PosTest {..} =
|
||||
TestDescr
|
||||
{ _testRoot = _dir,
|
||||
_testName = _name,
|
||||
_testAssertion = Steps $ compileAssertion (CompileOnly _stdin) _file _expectedFile
|
||||
}
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
testGroup
|
||||
"Compile and test examples"
|
||||
(map (mkTest . toTestDescr) tests)
|
||||
|
||||
posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> Text -> PosTest
|
||||
posTest _name rdir rfile routfile _stdin =
|
||||
let _dir = srcRoot <//> rdir
|
||||
_file = _dir <//> rfile
|
||||
_expectedFile = expectedRoot <//> routfile
|
||||
in PosTest {..}
|
||||
|
||||
tests :: [PosTest]
|
||||
tests =
|
||||
[ posTest
|
||||
"Fibonacci"
|
||||
$(mkRelDir "milestone/Fibonacci")
|
||||
$(mkRelFile "Fibonacci.juvix")
|
||||
$(mkRelFile "Fibonacci/expected.golden")
|
||||
"25\n",
|
||||
posTest
|
||||
"Hello World"
|
||||
$(mkRelDir "milestone/HelloWorld")
|
||||
$(mkRelFile "HelloWorld.juvix")
|
||||
$(mkRelFile "HelloWorld/expected.golden")
|
||||
"",
|
||||
posTest
|
||||
"Collatz calculator"
|
||||
$(mkRelDir "milestone/Collatz")
|
||||
$(mkRelFile "Collatz.juvix")
|
||||
$(mkRelFile "Collatz/expected.golden")
|
||||
"123\n",
|
||||
posTest
|
||||
"Pascal's triangle"
|
||||
$(mkRelDir "milestone/PascalsTriangle")
|
||||
$(mkRelFile "PascalsTriangle.juvix")
|
||||
$(mkRelFile "PascalsTriangle/expected.golden")
|
||||
"",
|
||||
posTest
|
||||
"Demo"
|
||||
$(mkRelDir "demo")
|
||||
$(mkRelFile "Demo.juvix")
|
||||
$(mkRelFile "Demo/expected.golden")
|
||||
"",
|
||||
posTest
|
||||
"TicTacToe"
|
||||
$(mkRelDir "milestone/TicTacToe")
|
||||
$(mkRelFile "CLI/TicTacToe.juvix")
|
||||
$(mkRelFile "TicTacToe/expected.golden")
|
||||
"aaa\n0\n10\n1\n2\n3\n3\n4\n5\n6\n7\n8\n9\n",
|
||||
posTest
|
||||
"Towers of Hanoi"
|
||||
$(mkRelDir "milestone/Hanoi")
|
||||
$(mkRelFile "Hanoi.juvix")
|
||||
$(mkRelFile "Hanoi/expected.golden")
|
||||
""
|
||||
]
|
@ -6,6 +6,7 @@ import BackendGeb qualified
|
||||
import Base
|
||||
import Compilation qualified
|
||||
import Core qualified
|
||||
import Examples qualified
|
||||
import Format qualified
|
||||
import Internal qualified
|
||||
import Parsing qualified
|
||||
@ -24,7 +25,8 @@ slowTests =
|
||||
Asm.allTests,
|
||||
Core.allTests,
|
||||
Internal.allTests,
|
||||
Compilation.allTests
|
||||
Compilation.allTests,
|
||||
Examples.allTests
|
||||
]
|
||||
|
||||
fastTests :: TestTree
|
||||
|
@ -2,6 +2,8 @@ Collatz calculator
|
||||
------------------
|
||||
|
||||
Type a number then ENTER
|
||||
Collatz sequence:
|
||||
123
|
||||
370
|
||||
185
|
||||
556
|
||||
|
5
tests/examplesExpected/Demo/expected.golden
Normal file
5
tests/examplesExpected/Demo/expected.golden
Normal file
@ -0,0 +1,5 @@
|
||||
Hello!
|
||||
2 :: 7 :: 3 :: 1 :: 0 :: nil
|
||||
0 :: 1 :: 2 :: 3 :: 7 :: nil
|
||||
1
|
||||
7
|
1
tests/examplesExpected/HelloWorld/expected.golden
Normal file
1
tests/examplesExpected/HelloWorld/expected.golden
Normal file
@ -0,0 +1 @@
|
||||
hello world!
|
Loading…
Reference in New Issue
Block a user