`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.
* Closes#2032.
* Adds the `juvix dev core normalize` command.
* Adds the `:n` command in JuvixCore REPL.
* Adds the `--normalize` flag to `juvix dev core read` and `juvix dev
core from-concrete`.
* Adds `pipeline-normalize` which denotes pipeline steps necessary
before normalization.
* Adds normalization tests in `tests/VampIR/positive/Core`.
* Closes#1989
* Adds optimization phases to the pipline (specified by
`opt-phase-eval`, `opt-phase-exec` and `opt-phase-geb` transformations).
* Adds the `-O` option to the `compile` command to specify the
optimization level.
* Functions can be declared for inlining with the `inline` pragma:
```
{-# inline: true #-}
const : {A B : Type} -> A -> B -> A;
const x _ := x;
```
By default, the function is inlined only if it's fully applied. One can
specify that a function (partially) applied to at least `n` explicit
arguments should be inlined.
```
{-# inline: 2 #-}
compose : {A B C : Type} -> (B -> C) -> (A -> B) -> A -> C;
compose f g x := f (g x);
```
Then `compose f g` will be inlined, even though it's not fully applied.
But `compose f` won't be inlined.
* Non-recursive fully applied functions are automatically inlined if the
height of the body term does not exceed the inlining depth limit, which
can be specified with the `--inline` option to the `compile` command.
* The pragma `inline: false` disables automatic inlining on a
per-function basis.
Currently we typecheck and check formatting of juvix examples. However
the make target redundantly traverses the juvix files within the
.juvix-build directory contained in each project (which has been created
during previous tests).
This commit cleans the .juvix-build directories before performing each
of these checks.
This pr includes some small adjustments to the Core prettyprinter.
Currently printing core code usually generates very long lines. In order
to improve that, now let and lambda bodies are printed in the following
line if they do not fit in the current line.
- Closes#2039
- Closes#2055
- Depends on #2053
Changes in this pr:
- Local modules are removed (flattened) in the translation abstract ->
internal.
- In the translation abstract -> internal we group definitions in
mutually recursive blocks. These blocks can contain function definitions
and type definitions. Previously we only handled functions.
- The translation of Internal has been enhanced to handle these mutually
recursive blocks.
- Some improvements the pretty printer for internal (e.g. we now print
builtin tags properly).
- A "hack" that puts the builtin bool definition at the beginning of a
module if present. This was the easiest way to handle the implicit
dependency of the builtin stringToNat with bool in the internal-to-core
translation.
- A moderately sized test defining a simple lambda calculus involving
and an evaluator for it. This example showcases mutually recursive types
in juvix.
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
This PR upgrades our Haskell configurations to compile with version
9.2.7. The checklist below can serve as a guide for similar future
updates:
- [x] Update Stack resolver in `stack.yaml`
- [x] Modify `tested-with` section in `package.yaml`
- [x] Build and push the new compiler docker image, see instructions
here
[docker/README.md](https://github.com/anoma/juvix/blob/main/docker/README.md):
`ghcr.io/paulcadman/ghc-alpine:9.2.7 container`.
- [x] Update Linux Github Action workflow in
`.github/workflows/linux-static-binary.yaml` and adjust
`docker/Dockerfile-ghc-alpine-9.2.7`
- [x] Revise GHC/Stack/Cabal versions in `.devcontainer/Dockerfile`
- [x] Refresh Cabal configuration in `cabal-project`
Previously if you call Juvix on a file that doesn't exist you get the
error:
```
$ juvix compile /i/don't/exist.juvix
juvix: /i/dont: changeWorkingDirectory: does not exist (No such file or directory)
```
After this change you will see:
```
$ juvix compile /i/don't/exist.juvix
The input path "/i/dont/exist.juvix" does not exist
```
This PR fixes the behaviour of the `format` command when run on a
project that contains subprojects. Files in subprojects must not be
processed by the formatter.
The format issue was caused by a bug in the `walkDirRel` function that
is used to traverse a file system tree:
9a64184253/src/Juvix/Data/Effect/Files.hs (L36)
In this function, the passed handler can return a function that
determines if a candidate subdirectory should be traversed. The first
argument of this function indicates if the candidate subdirectory
contains a juvix.yaml file. In the formatter and the path resolver we
use this argument to exclude such subdirectories from the traversal.
Previously the first argument was calculated from the files in the
current directory instead of the candidate subdirectory - which was the
source of the bug.
The callers of walkDirRel are also fixed to match the updated behaviour.
* Closes https://github.com/anoma/juvix/issues/2077
This pr fixes the following:
This example causes the compiler to crash with "implicitness mismatch".
```
f : id Bool -> Bool;
f _ := false;
```
The reason is that `id` expects an implicit argument but finds `Bool`,
which is explicit. The arity checker was not inserting any hole because
it was ignoring the whole type. Moreover the aritychecker was never
checking `->` types as we never expected to
have to insert holes in `->` types (since the only fragment of defined
functions that we accept in types are those which do not have implicit
arguments).
We now properly arity check all types and process the function type `->`
correctly.
This change, instead of changing the `FormatOptions` data type to have
some `AppPath *`, it just adds the special case on how to handle this
specific command to figure out its input directory.
- Fixes#2058
The binary inside the Juvix release archive is now named `juvix` so this
PR updates the script that unzips and adds the juvix binary to the
devcontainer PATH to expect this.
Also see: https://github.com/anoma/juvix-docs/pull/8
# Description
This PR fixes#1943. The primary issue stemmed from an incorrect
insertion in the set designated for storing negative type parameters.
Additionally, there was a call site intended to use the variable `typ`,
but I mistakenly used `ty` (which was for something else). To prevent
such silly typos better to adopt more meaningful names.
This PR adds support for importing modules from within a Juvix project
in the Juvix REPL.
The imported module is checked (parsed, arity-checked, type-checked etc)
as normal and added to the REPL session scope. Any errors during the
checking phase is reported to the user.
### Notes:
* You must load a file before using `import`. This is because the REPL
needs to know which Juvix project is active.
* You may only import modules from within the same Juvix project.
### Examples
After launching `juvix repl`:
#### `open import`
```
Stdlib.Prelude> open import Stdlib.Data.Int.Ord
Stdlib.Prelude> 1 == 1
true
```
#### `import as`
```
Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int
Stdlib.Prelude> 1 Int.== 1
true
```
#### `import`then `open`
```
Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int
Stdlib.Prelude> open Int
Stdlib.Prelude> 1 == 1
true
```
#### Line-terminating semicolons are ignored:
```
Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int;;;;;
Stdlib.Prelude> 1 Int.== 1
true
```
* Closes https://github.com/anoma/juvix/issues/1951
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
This PR updates the juvix-stdlib submodule. In particular the update
contains the new traits implemented in
https://github.com/anoma/juvix-stdlib/pull/54.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
This pr fixes a bug where the repl would crash if it had the implicit
stdlib dependency and the .juvix-build/stdlib directory did not yet
exist. This bug was not exposed in the smoke tests because the
.juvix-build was never cleared.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
