Juvix testing framework

[lukaszcz]

Add a first version of the testing framework discussed at HHH2024.Q3.

Add testing pragmas which specify that a function is a test and how the test should be executed. For now, let's have three possibilities.

1. test: eval indicates that the zero-argument boolean property function should be evaluated with the Core evaluator and the result compared with true. Example:

   module Tests;
   {-# test: eval #-}
   prop-reverseReverseIsIdentity : Bool :=
   let xs := [1; 2; 3; 4; 5] in
   xs == reverse (reverse xs);
   end;

2. test-cases: ident indicates that the property function should be tested for the argument values specified by Juvix identifier ident. Example:

   module Tests;
   cases-reverseReverseIsIdentity : List (List Int)) := [
   [1; 2; 3; 4; 5;];
   [2; 4; 9; 8; 7];
   [1; 90; 9];
   []
   ];
   
   {-# test-cases: cases-reverseReverseIsIdentity #-}
   prop-reverseReverseIsIdentity (xs : List Int) : Bool :=
   xs == reverse (reverse xs);
   end;

3. test: rand specifies that the juvix-quickcheck library should be used to generate random test cases Example:

   module Tests;
   {-# test: rand #-}
   prop-reverseReverseIsIdentity (xs : List Int) : Bool :=
   xs == reverse (reverse xs);
   end;

The command juvix test would collect all tests declared in all modules in the project and run them according to the test pragmas. It would take care under the hood of all details like setting the random seed and using juvix-quickcheck correctly.

[janmasrovira]

I think we should replace (if possible) the pragmas by Juvix code. Even if the available options in this proposal are minimal, they are bound to grow. So we should take advantage of all the Juvix facilities that we have already implemented, such as default arguments, go to definition, documentation on mouse over, etc.

[lukaszcz]

Better alternative: have builtin data structure(s) that represent tests, e.g., similar to how Tasty does it.