182 lines
5.4 KiB
Perl
182 lines
5.4 KiB
Perl
# TL;DR
|
|
|
|
To run the tests, run
|
|
|
|
```
|
|
dune runtest
|
|
```
|
|
|
|
from the root of the project directory. If this outputs
|
|
nothing, the testsuite passes. If this outputs a diff, it
|
|
means that there is a mismatch between the recorded/reference
|
|
output and the behavior of your program.
|
|
|
|
To *promote* the tests outputs (that is, to modify the reference
|
|
output to match the current behavior of your program), run
|
|
|
|
```
|
|
dune runtest
|
|
dune promote
|
|
```
|
|
|
|
When you submit your project, please check that `dune runtest` does
|
|
not produce a diff -- the recorded output should match your
|
|
program. If some outputs are wrong / not what you would expect, please
|
|
explain this in the present file.
|
|
|
|
|
|
# Intro
|
|
|
|
This file is a "dune cram test" as explained at
|
|
> https://dune.readthedocs.io/en/stable/tests.html#cram-tests
|
|
|
|
The idea is to write 2-indented command lines prefixed by
|
|
a dollar sign. The tool will run the command and check that
|
|
the output corresponds to the output recorded in the file.
|
|
|
|
$ echo example
|
|
example
|
|
|
|
To run the tests, just run `dune runtest` at the root of the
|
|
project. This will show you a diff between the observed
|
|
output and the recorded output of the test -- we consider
|
|
that the test 'passes' if the diff is empty.
|
|
In particular, if you run `dune runtest` and you see no
|
|
output, this is good! It means there was no change in the
|
|
test output.
|
|
|
|
If you think that the new output is better than the previous
|
|
output, run `dune promote`; dune will rewrite the recorded
|
|
outputs to match the observed outputs. (You can also modify
|
|
outputs by hand but this is more cumbersome.)
|
|
|
|
It is totally okay to have some test outputs recorded in
|
|
your repository that are known to be broken -- because there
|
|
is a bug, or some feature is not documented yet. Feel free
|
|
to use the free-form comments in run.t to mention explicitly
|
|
that the output is broken. (But then please remember, as the
|
|
output changes in the future, to also update your comments.)
|
|
|
|
|
|
# The tests
|
|
|
|
The tests below use the `minihell` program defined in
|
|
../bin/minihell.ml, called on the *.test files stored in the
|
|
present directory. If you want to add new tests, just add
|
|
new test files and then new commands below to exercise them.
|
|
|
|
`minihell` takes untyped programs as input and will
|
|
type-check and elaborate them. It can show many things
|
|
depending on the input flags passed. By default we ask
|
|
`minihell` to repeat the source file (to make the recorded
|
|
output here more pleasant to read) and to show the generated
|
|
constraint. It will also show the result type and the
|
|
elaborated term.
|
|
|
|
$ FLAGS="--show-source --show-constraint"
|
|
|
|
Remark: You can call minihell from the command-line yourself
|
|
by using either
|
|
> dune exec bin/minihell.exe -- <arguments>
|
|
or
|
|
> dune exec minihell -- <arguments>
|
|
(The latter short form, used in the tests below, is available thanks
|
|
to the bin/dune content.)
|
|
|
|
|
|
## Simple tests
|
|
|
|
`id_poly` is just the polymorphic identity.
|
|
|
|
$ minihell $FLAGS id_poly.test
|
|
Input term:
|
|
lambda x. x
|
|
|
|
Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
|
|
[2]
|
|
|
|
`id_int` is the monomorphic identity on the type `int`. Note
|
|
that we have not implemented support for a built-in `int`
|
|
type, this is just an abstract/rigid type variable: `Constr
|
|
(Var ...)` at type `STLC.ty`.
|
|
|
|
$ minihell $FLAGS id_int.test
|
|
Input term:
|
|
lambda x. (x : int)
|
|
|
|
Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
|
|
[2]
|
|
|
|
## Logging the constraint-solving process
|
|
|
|
You can ask `minihell` to show how the constraint evolves as
|
|
the solver progresses and accumulates more information on
|
|
the inference variables.
|
|
|
|
$ minihell $FLAGS --log-solver id_int.test
|
|
Input term:
|
|
lambda x. (x : int)
|
|
|
|
Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
|
|
[2]
|
|
|
|
## An erroneous program
|
|
|
|
$ minihell $FLAGS error.test
|
|
Input term:
|
|
(lambda x. (x : int)) (lambda y. y)
|
|
|
|
Fatal error: exception Failure("Infer.has_type: App case: not implemented yet")
|
|
[2]
|
|
|
|
## Examples with products
|
|
|
|
$ minihell $FLAGS curry.test
|
|
Input term:
|
|
lambda f. lambda x. lambda y. f (x, y)
|
|
|
|
Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
|
|
[2]
|
|
|
|
$ minihell $FLAGS uncurry.test
|
|
Input term:
|
|
lambda f. lambda p. let (x, y) = p in f x y
|
|
|
|
Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
|
|
[2]
|
|
## Cyclic types
|
|
|
|
Unification can sometimes create cyclic types. We decide to reject
|
|
these situations with an error. (We could also accept those as they
|
|
preserve type-safety, but they have the issue, just like the
|
|
OCaml -rectypes option, that they allow to write somewhat-nonsensical
|
|
program, and our random term generator will be very good at finding
|
|
a lot of those.)
|
|
|
|
$ minihell $FLAGS --log-solver selfapp.test
|
|
Input term:
|
|
lambda x. x x
|
|
|
|
Fatal error: exception Failure("Infer.has_type: Abs case: not implemented yet")
|
|
[2]
|
|
## Generator tests
|
|
|
|
This gives example outputs for my implementation. It is completely
|
|
fine if your own implementation produces different (sensible) results.
|
|
|
|
There are not many programs with depth 3, 4 and 5.
|
|
|
|
$ minigen --exhaustive --depth 3 --count 100
|
|
Fatal error: exception Failure("MSeq.delay: not implemented yet")
|
|
[2]
|
|
|
|
$ minigen --exhaustive --depth 4 --count 100
|
|
Fatal error: exception Failure("MSeq.delay: not implemented yet")
|
|
[2]
|
|
|
|
An example of random sampling output at higher depth.
|
|
|
|
$ minigen --seed 42 --depth 6 --count 10
|
|
Fatal error: exception Failure("MRand.delay: not implemented yet")
|
|
[2]
|