- Closes#2162
This pr improves formatting of source files with comments.
The concrete ast now stores location information of almost all keywords.
We do not store location information of parentheses. Comments will be
pushed out of parentheses by the formatter.
E.g.
```
( -- comment
f x)
```
will become
```
-- comment
(f x)
```
This only occurs if the comment appears just after the `(`. So the
following will be respected
```
(f --comment
x)
```
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
`format` command now returns code `0` most of the time.
It will return `1` when:
* some error occur, so can not format
* file is unformatted and `--check` option is used
* One or more files are not formatted in a Juvix project.
- Fixes#2171
Say we have a module that import/open the Prelude:
Test.juvix
```
module Test;
import Stdlib.Prelude open;
```
When the module is compiled, we have a step in the compiler pipeline
which filters out unreachable symbols. For this module all symbols are
filtered because the module contains no definitions.
So if the module is loaded in the REPL, no symbols will be available to
process through the evaluator. The REPL is a place to explore the
symbols in the module so (like with Haskell's GHCi) it would be useful
if all symbols were available in the REPL session. That's what this PR
implements.
* Closes https://github.com/anoma/juvix/issues/2159
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- Closes#2128
- Closes#2161
This pr fully implements the monadic pretty printer based on
`ExactPrint`, which respects comments. Until now, comments inside
expressions were printed after the current statement. Now they are
printed in the correct place, except when a comment occurs before
something that we don't store its location. E.g. parentheses,
semicolons, braces, colons, etc. I proposed that we irone out this issue
in a separate pr.
Since the old non-monadic algorithm is no longer necessary, I removed
it.
This does not change any examples or documentation. The interface of the
standard library remains unchanged (except the addition of new
iterators), so this PR can be merged without side effects.
* Closes#2146
* Closes#2134
Adds the `argnames` pragma which specifies function argument names.
These will be the names used in Core and subsequently in VampIR for the
`main` function.
```
{-# argnames: [x, y] -#}
main : Nat -> Nat -> Nat;
```
If set, `JUVIX_LLVM_DIST_PATH` should point to the root of a LLVM
installation, i.e clang should be present
in`$JUVIX_LLVM_DIST_PATH`/bin/clang.
If `JUVIX_LLVM_DIST_PATH` is not set, or `clang` is not available there
then the system PATH is used instead, (this is the current behaviour).
The `juvix doctor` clang checks use the same logic as `juvix compile` to
find and check the `clang` executable.
To help with debugging the clang location, this PR also adds `juvix
doctor --verbose` which prints the location of the `clang` executable
and whether it was found using the system PATH or the
JUVIX_LLVM_DIST_PATH environment variable:
```
juvix doctor --verbose
> Checking for clang...
| Found clang at "/Users/paul/.local/share/juvix/llvmbox/bin/clang" using JUVIX_LLVM_DIST_PATH environment variable
```
or
```
juvix doctor --verbose
> Checking for clang...
| Found clang at "/Users/paul/.local/bin/clang" using system PATH
```
* Closes https://github.com/anoma/juvix/issues/2133
`AnsiText` is a type that represents some text that can be printed with
`Ansi` formatting annotations, or as plain text. It is expected that it
should have a `Semigroup` instance. This pr adds that.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
* Closes#1992
A function identifier `fun` can be declared as an iterator with
```
syntax iterator fun;
```
For example:
```haskell
syntax iterator for;
for : {A B : Type} -> (A -> B -> A) -> A -> List B -> List A;
for f acc nil := acc;
for f acc (x :: xs) := for (f acc x) xs;
```
Iterator application syntax allows for a finite number of initializers
`acc := a` followed by a finite number of ranges `x in xs`. For example:
```
for (acc := 0) (x in lst) acc + x
```
The number of initializers plus the number of ranges must be non-zero.
An iterator application
```
fun (acc1 := a1; ..; accn := an) (x1 in b1; ..; xk in bk) body
```
gets desugared to
```
fun \{acc1 .. accn x1 .. xk := body} a1 .. an b1 .. bk
```
The `acc1`, ..., `accn`, `x1`, ..., `xk` can be patterns.
The desugaring works on a purely syntactic level. Without further
restrictions, it is not checked if the number of initializers/ranges
matches the type of the identifier. The restrictions on the number of
initializers/ranges can be specified in iterator declaration:
```
syntax iterator fun {init: n, range: k};
syntax iterator for {init: 1, range: 1};
syntax iterator map {init: 0, range: 1};
```
The attributes (`init`, `range`) in between braces are parsed as YAML to
avoid inventing and parsing a new attribute language. Both attributes
are optional.
This pr adds a new command, `:def` to the repl. This command expects a
single identifier that must be in scope and then prints its definition.
For constructors, the whole type definition is printed.
It also applies some refactors to the code for repl command.
1. Before there was a mega `where` block of definitions. I have hoisted
most of the definitions there to the top level. I feel like now it is
easier to navigate and read.
2. Use `ExceptT` instead of local `case` expressions for errors.
3. Use forks of `haskeline` and `repline`. These forks are necessary
because these libraries do not export the constructors `HaskelineT` and
`InputT` respectively, thus, making it impossible to catch errors in
their underlying monad.
- Closes#2067
This pr adds the field `main` to `juvix.yaml`. This field is optional
and should contain a path to a juvix file that is meant to be used for
the `compile` (and `dev compile`) command when no file is given as an
argument in the CLI. This makes it possible to simply run `juvix
compile` if the `main` is specified in the `jvuix.yaml`.
I have updated the `juvix.yaml` of the milestone examples.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
This PR installs the `gnu-sed` for the macOS build.
It can be called with the name `sed`, no `gsed`.
NB: The environmental variables set in one step are only reflected in
the subsequent steps.
Currently generated links for fixing errors in the `juvix doctor`
command are broken.
Fixing that by updating the base Url link.
Also fixed the link to the installation of juvix in the contributing
guide.
Instead, always act as `--no-format` option is set to `False` as
previous default.
The change seem to not affect any current formatting, so I assume it
passes the checks on testing.
Fixes#2084
# Checklist:
- [x] My code follows the style guidelines of this project
- [ ] I have made corresponding changes to the documentation
- [x] My changes generate no new warnings
- Closes#2056
- Depends on #2103
I am not sure about the implementation of `isType` for `NBot`. (solved).
The `Eq` instance returns `True` for every two `Bottom` terms,
regardless of their type.
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
* Closes#2035
* Depends on #2086
* Depends on #2096
* Adds end-to-end tests for the Juvix-to-VampIR compilation pipeline.
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
This PR:
- Makes `vamp-ir` available in the CI (pre-release 0.1.2)
- [Use a setup-wasmer action to install
`wasmer`](https://github.com/marketplace/actions/setup-wasmer)
- Fixes cache option value for `jaxxstorm/action-install-gh-release`'s
usages
Adds support for:
- #2103
Related:
- https://github.com/anoma/vamp-ir/issues/90
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- Closes#2089
Now the symbols inside `using {..}` and `hiding {..}` are properly
scoped, which means that they will be properly colored and will have
goto information. If the referenced module does not contain a symbol in
the list, an error will be thrown.
This PR resolves a few bugs in the Makefile targets for formatting and
type checking Juvix files, which were preventing the capture of type
checking errors for our examples and bad formatting for all the Juvix
files in the repository. With this PR, our code should now be clean, and
we can expect every file to be properly formatted and type checked.
Changes made:
- [x] Updated `make format-juvix-files`
- [x] Updated `make check-format-juvix-files`
- [x] Formatted all Juvix files
- [x] Comment a fragment in `examples/milestone/Bank/Bank.juvix`
In the future, we will drastically simplify the Makefile once we improve
the `format` and the `type check` command for example posted here:
- #2066
- #2087
Related:
- #2063
- #2040 (due to some typechecking errors we're not capturing before)
- #2105
- https://github.com/anoma/juvix/issues/2059
In this PR we pass through the `juvix compile` optimization flag to the
C compiler in the native compilation.
NB: Clang supports -On for any positive n. -O4 and higher is equivalent
to -O3
Also we disable optimizations when the `-g` / `--debug` option is
specified.
* Closes https://github.com/anoma/juvix/issues/2104
---------
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
* Closes#2034.
* Adds the `vampir` target to the `compile` command.
* Adds two tests which are not yet enabled because `vamp-ir` is not
available in the CI (these and more tests will be enabled in #2103).
- Closes#2050
This pr adds the possibility to give judoc documentation in blocks
delimited by `{--` and `--}`.
- Inside these blocks, normal comments are disabled.
- It is allowed to have multiple blocks associated with the same
identifier, e.g.
```
{-- an axiom --}
{-- of type ;Type; --}
axiom a : Type;
```
- Nested blocks are *not* allowed.
- Blocks can be empty: `{-- --}`.
- The formatter respects line breaks inside blocks.
- The formatter normalizes whitespace at both ends of the block to a
single whitespace.
The prettyprinter library takes care avoid adding whitespace to empty
lines when it is rendering indented text.
See:
7e32c010ec/prettyprinter/src/Prettyprinter/Internal.hs (L1999)
However it only does this for unannotated text.
In our code we were stripping annotations from renderings within
`toTextStream` but we must remove the annotations before calling
`layoutPretty` to get the proper handling of whitespace with
indentations. That's what this PR does.
