- 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.
`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#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>
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
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).
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.
# Description
No the filepath in the `juvix forma` command is n=made optional.
However, in that case, the `--stdin` command is required.
### Implementation details
~For now, as a quick solution, I have introduce the "fake" path that is
used for `fomat` command with stdin option.~
I needed to do a couple of big changes:
* `format` command FILE is now optional, howvere, I check that in case
of `Nothing` `--stdin` option should be present, otherwise it will fail
* `entryPointModulePaths` is now `[]` instead of `NonEmpty`
* `ScopeEff` now has `ScopeStdin` constructor as well, which would take
the input from stdin instead of having path passed around
* `RunPipelineNoFileEither` is added to the `App` with the bunch of
`*Stdin` functions that doesn't require filepath argument to be passed
Fixes#2008
## Type of change
- [x] New feature (non-breaking change which adds functionality)
# Checklist:
- [x] My code follows the style guidelines of this project
- [x] I have made corresponding changes to the documentation
- [x] My changes generate no new warnings
- [x] I have added tests that prove my fix is effective or that my
feature works:
- [x] smoke tests
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: janmasrovira <janmasrovira@gmail.com>
- Closes#1993
This pr makes it possible to use `~`, `..` and environment variables in
the `juvix.yaml` and all flags / input of the cli.
In the CLI, the shell will be responsible for replacing environment
variables with their value, so the usual syntax can be used. For the
`dependencies` field, I have implemented a parser that has some
restrictions:
1. Environment variables are given with the makefile-like syntax
`$(VAR)`
2. The three characters `$` `(` `)` are reserved for the environment
variables syntax.
They cannot be part of the path.
3. `~` is reserved for `$(HOME)`. I.e. the prepath `~~` will expand to
`$HOME$HOME`.
4. Nested environment variables are not allowed.
Thanks @paulcadman for the feedback. I think we are ready to merge this
nightmarish pr 👻
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
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
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>
* Adds end-to-end tests for compiling Juvix to Geb
* Fixes bugs in the Core-to-Geb translation (`<=` and `let`)
* Fixes a bug in the Geb evaluator (equality on integers)
* Modifies `ComputeTypeInfo` to handle polymorphism and the dynamic type
(doesn't check for correctness but infers the types under the assumption
that binder type annotations and type info for identifiers are correct).
* Add the `:t expr` command in JuvixCore repl to print the inferred
type.
* Adds a smoke test.
This PR adds testing for the core-to-geb translation.
It works as follows:
1. Parse the Juvix Core file.
2. Prepare the Juvix Core node for translation to Geb.
3. Translate the Juvix Core node to Geb.
5. Perform type checking on the translated Geb node to ensure that the
types
from the core node make sense in the Geb context and avoid any Geb
runtime
errors.
6. Evaluate the Juvix Core node to see if it produces the expected
result.
7. Translate the result of the evaluated Juvix Core node to Geb for
comparison
with the expected output later.
8. Compare the result of the evaluation of the Geb term produced in step
3
with the result of the evaluation of the Geb term produced in step 6 to
ensure consistency.
9. If step 8 succeeds, then compare the output of step 6 (the evaluation
of the core
node) with the expected output (given in Geb format) to ensure that
the program is functioning as intended.
This PR goes after:
- https://github.com/anoma/juvix/pull/1863
and
https://github.com/anoma/juvix/pull/1832
This implements a basic version of the algorithm from: Luc Maranget,
[Compiling pattern matching to good decision
trees](http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf). No
heuristics are used - the first column is always chosen.
* Closes#1798
* Closes#1225
* Closes#1926
* Adds a global `--no-coverage` option which turns off coverage checking
in favour of generating runtime failures
* Changes the representation of Match patterns in JuvixCore to achieve a
more streamlined implementation
* Adds options to the Core pipeline
* Depends on #1832
* Closes#1844
* Adds errors to the Core pipeline
* Checks for no recursion in the GEB pipeline
* Checks for no polymorphism in the GEB pipeline
* Checks for no dynamic type in the GEB pipeline
* Checks for no IO in the GEB pipeline
* Checks for no unsupported builtins in the GEB pipeline
Print JuvixCore InfoTable in such a way that it can be parsed back by
the JuvixCore parser.
* Depends on PR #1832
* Depends on PR #1862
* Closes#1841
* Adds "JuvixCore print" tests which read the files from
Core/positive/*.jvc, print them, read them back and check if the
evaluation results are preserved.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Depends on PR #1832
* Closes#1799
* Removes Backend.C.Translation.FromInternal
* Removes `foreign` and `compile` blocks
* Removes unused test files
* Removes the old C runtime
* Removes other dead code
* Depends on PR #1824
* Closes#1556
* Closes#1825
* Closes#1843
* Closes#1729
* Closes#1596
* Closes#1343
* Closes#1382
* Closes#1867
* Closes#1876
* Changes the `juvix compile` command to use the new pipeline.
* Removes the `juvix dev minic` command and the `BackendC` tests.
* Adds the `juvix eval` command.
* Fixes bugs in the Nat-to-integer conversion.
* Fixes bugs in the Internal-to-Core and Core-to-Core.Stripped
translations.
* Fixes bugs in the RemoveTypeArgs transformation.
* Fixes bugs in lambda-lifting (incorrect de Bruijn indices in the types
of added binders).
* Fixes several other bugs in the compilation pipeline.
* Adds a separate EtaExpandApps transformation to avoid quadratic
runtime in the Internal-to-Core translation due to repeated calls to
etaExpandApps.
* Changes Internal-to-Core to avoid generating matches on values which
don't have an inductive type.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: janmasrovira <janmasrovira@gmail.com>
This PR adds support for all recent changes in GEB introduced by:
- https://github.com/anoma/geb/pull/70
- Closes#1814
Summary:
- [x] Add LeftInj, RightIng, and Absurd types in GEB language
- [x] Fix FromCore translation for the new data types and minor code
styling issues.
- [x] Fix GEB-STLC type inference and checking
- [X] Add support for evaluating typed morphism "(typed ...)" in the Geb
repl and .geb files.
- [x] Simplify a bit the Geb parser
- [x] Fix `dev geb check` command
- [x] Type check files in `tests/Geb/positive`
After this PR, we should include interval location for Geb terms to
facility debugging type-checking errors.
This PR introduces an evaluator for the Geb STLC interface/fragment and
other related commands, including a REPL to interact with his backend.
-
https://github.com/anoma/geb/blob/mariari/binaries/src/specs/lambda.lisp
We have included a REPL and support for commands such as read and eval
here. Check out:
```
juvix dev geb --help
```
- [x] Add Geb evaluator with the two basic eval strategies.
- [x] Add quasi quoter: return morphisms from typed geb values.
- [x] Add type/object inference for morphisms.
- [x] All combined: morphisms-eval-to-morphisms
- [x] Parse and pretty printer Geb values (without quoting them)
- [x] Parse files containing Geb terms:
- [x] Saved in a .lisp file according to anoma/geb example (typed
object).
- [x] Store in a .geb file simple as simple lisp expression.
- [x] Add related commands to the CLI for `dev geb`:
- [x] Subcommand: eval
- [x] Subcommand: read
- [x] Subcommand: infer
- [x] Subcommand: repl
- [x] Subcommand: check
- [x] Minor changes `hom` by `!->` in the Geb prettyprinter
- [x] Add tests for:
- [x] New subcommand (smoke tests)
- [x] Eval
Issues to solve after merging this PR:
- Add location to Geb ast for proper error location.
- Add tests for all related subcommands, e.g. check, and infer.
- Check compilation from Core to Geb: (run inferObject with the type
provided by the core node).
- [x] Update the vs code-plugin to load Geb repl and eval.
(31994c8684)
This PR:
- Closes#1647
It gives compilation errors for language features that require more
substantial support (recursion, polymorphism). The additional features
are to be implemented in future separate PRs.
* Adds a new target `geb` to the CLI command `juvix dev core compile`,
which produces a `*.geb` output file in the `.juvix-build` directory.
* Adds a few tests. These are not yet checked automatically because
there is no GEB evaluator; checking the `*.geb` output would be too
brittle.
- Fixes#1723
- It refactors parsing/scoping so that the scoper does not need to read
files or parse any module. Instead, the parser takes care of parsing all
the imported modules transitively.
Filepaths within a Loc must now be absolute or an error is thrown when
mkLoc is called. This Loc is used when displaying errors.
This commit uses imaginary absolute file paths in the Core repl and Asm
commands in the cases (parsing a single expression for example).
Before this fix, the `core {repl, read, eval}` and `asm` commands would
crash if it encountered an error when invoked with a relative path, or
in the case of a repl when parsing a single expression.
This PR adds some maintenance at different levels to the CI config, the
Make file, and formatting.
- Most of the actions used by the CI related to haskell, ormolu, hlint
and pre-commit have been updated because Github requires NodeJS 16. This
change removes all the old warnings related to nodeJs.
In the case of ormolu, the new version makes us format some files that
were not formatted before, similarly with hlint.
- The CI has been updated to use the latest version of the Smoke testing
framework, which introduced installation of the dependencies for Linux
(libicu66) and macOS (icu4c) in the CI. In the case of macOS, the CI
uses a binary for smoke. For Linux, we use stack to build smoke from the
source. The source here is in a fork of [the official Smoke
repo](https://github.com/SamirTalwar/smoke). Such includes some
features/changes that are not yet in the official repo.
- The Makefile runs the ormolu and hlint targets using as a path for the
binaries the environment variables ORMOLU and HLINT. Thus, export those
variables in your environment before running `make check,` `make format`
or `make hlint`. Otherwise, the Makefile will use the binaries provided
by `stack`.
Co-authored-by: Paul Cadman <git@paulcadman.dev>
This PR redefines the `html` command unifying our previous subcommands
for the HTML backend. You should use the command in the following way to
obtain the same results as before:
- `juvix html src.juvix` -> `juvix html src.juvix --only-source`
- `juvix dev doc src.juvix` -> `juvix html src.juvix`
- Other fixes here include the flag `--non-recursive`, which replaces
the previous behavior in that we now generate all the HTML recursively
by default.
- The flag `--no-print-metadata` is now called `--no-footer`
- Also, another change introduced by this PR is asset handling; for
example, with our canonical Juvix program,
the new output is organized as follows.
```
juvix html HelloWorld.juvix --only-source && tree html/
Copying assets files to test/html/assets
Writing HelloWorld.html
html/
├── assets
│ ├── css
│ │ ├── linuwial.css
│ │ ├── source-ayu-light.css
│ │ └── source-nord.css
│ ├── images
│ │ ├── tara-magicien.png
│ │ ├── tara-seating.svg
│ │ ├── tara-smiling.png
│ │ ├── tara-smiling.svg
│ │ ├── tara-teaching.png
│ │ └── tara-teaching.svg
│ └── js
│ ├── highlight.js
│ └── tex-chtml.js
└── HelloWorld.html
├── Stdlib.Data.Bool.html
├── Stdlib.Data.List.html
├── Stdlib.Data.Maybe.html
├── Stdlib.Data.Nat.html
├── Stdlib.Data.Ord.html
├── Stdlib.Data.Product.html
├── Stdlib.Data.String.html
├── Stdlib.Function.html
├── Stdlib.Prelude.html
└── Stdlib.System.IO.html
```
In addition, for the vscode-plugin, this PR adds two flags,
`--prefix-assets` and `--prefix-url`, for which one provides input to
help vscode find resource locations and Juvix files.
PS. Make sure to run `make clean` the first time you run `make install`
for the first time.
An implementation of the translation from JuvixCore to JuvixAsm. After
merging this PR, the only remaining step to complete the basic
compilation pipeline (#1556) is the compilation of complex pattern
matching (#1531).
* Fixes several bugs in lambda-lifting.
* Fixes several bugs in the RemoveTypeArgs transformation.
* Fixes several bugs in the TopEtaExpand transformation.
* Adds the ConvertBuiltinTypes transformation which converts the builtin
bool inductive type to Core primitive bool.
* Adds the `juvix dev core strip` command.
* Adds the `juvix dev core asm` command.
* Adds the `juvix dev core compile` command.
* Adds two groups of tests:
- JuvixCore to JuvixAsm translation: translate JuvixCore tests to
JuvixAsm and run the results with the JuvixAsm interpreter,
- JuvixCore compilation: compile JuvixCore tests to native code and WASM
and execute the results.
* Closes#1520
* Closes#1549
