This PR implements pretty printing of evaluation results consistently
with Juvix syntax. The printed values do not necessarily originate
directly from the source code. All functions/lambdas are printed as
`<fun>`.
The same mechanism is used to implement pretty printing of unmatched
pattern examples.
Juvix REPL now uses the new value printing mechanism to display
evaluation results. Typing `nil` in the REPL will now just display
`nil`. The command `juvix dev repl` still prints raw JuvixCore terms.
* Closes#1957
* Closes#1985
There were two bugs here:
1. The _replNoDisambiguate option was set to True for `juvix repl`.
2. The disambiguateNames pass was being applied after the result node
had already been fetched from the infotable.
* Closes https://github.com/anoma/juvix/issues/1958
The new `juvix dev repl` command is a copy of the `juvix repl` with the
addition of `--no-disambiguate` flag that is present on the `juvix dev
core from-concrete` command.
The `juvix repl` command now does not have the `--transforms`,
`--show-de-bruijn` flags as these are only relevant for compiler
developers. The eval transforms are always applied.
By default `juvix dev repl` uses the eval transforms. You can override
this by specifying the `-t` flag.
Also we now run `disambiguateNames` transform on the info table in the
`dev repl` (unless the `--no-disambiguate-names` flag is set). This is
so the output of the `juvix dev repl` will match that of `juvix dev core
from-concrete` and also so the output can be parsed by back the core
parser.
* Closes https://github.com/anoma/juvix/issues/1914
Previously we were:
* discarding the types table
* discarding the name ids state
after processing an expression in the REPL.
For example evaluating:
```
let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10
```
would loop in the REPL.
We noticed that the `n` in `suc n` was being given type `Type` instead
of `Nat`. This was because the name id given to n was incorrect, the
REPL started using name ids from 0 again.
We fixed this issue by storing information, including the types table
and name ids state in the Artifacts data structure that is returned when
we run the pipeline for the first time. This information is then used
when we call functions to compile / type check REPL expressions.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Core transformations apply to the whole InfoTable, the REPL needs to
apply Core transformations to the single node that it compiles from the
user input string.
The solution in this commit is to:
1. Compile the input string as before to obtain a Core Node.
2. Add this Node to a copy of the Core InfoTable for the loaded file.
3. Apply the (CLI specified) Core transformations to this InfoTable.
4. Extract the (now transformed) Node from the InfoTable.
We can think of a way to improve this, maybe when we tackle allowing the
user to make new definitions in the REPL.
As soon as compilation of pattern matching is complete we should enable
some (all?) Core transformations by default.
Example:
At the moment we get the following result in the REPL:
```
juvix repl
...
Stdlib.Prelude> 1 + 1
suc (suc zero)
```
After this commit we can turn on `nat-to-int` transformation:
```
juvix repl -t nat-to-int
Stdlib.Prelude> 1 + 1
2
```
* Part of https://github.com/anoma/juvix/issues/1531
* REPL support reloading
* Reformat :help and add :version command
* repl: Display the currently loaded module in the banner
* repl: Load the Prelude at launch unless --no-prelude or --no-stdlib are set
