This PR:
* Modifies entry point `_entryPointBuildDir` to use the `BuildDir` type
instead of `SomeBase Dir`. This allows delayed resolution of the default
build directory which was useful for the Package -> Concrete translation
point below.
* Modifies `juvix dev root` to render the current package as a
Package.juvix file.
* Modifies the Package -> Concrete translation to recognise default
arguments. So, for example, an empty `juvix.yaml` file will be
translated into the following (instead of the `name`, `version`, and
`dependencies` arguments being populated).
module Package;
import Stdlib.Prelude open;
import PackageDescription.V1 open;
package : Package := defaultPackage;
* Adds a temporary command (removed when juvix.yaml support is removed)
`juvix dev migrate-juvix-yaml` that translates `juvix.yaml` into an
equivalent `Package.juvix` in the current project.
* Adds a temporary script `migrate-juvix-yaml.sh` (removed when
juvix.yaml support is removed) which can be run in the project to
translate all Juvix projects in the repository.
* Actually translate all of the `juvix.yaml` files to `Package.juvix`
using the script.
* Part of https://github.com/anoma/juvix/issues/2487
Depends on:
* ~~https://github.com/anoma/juvix/pull/2459~~
* https://github.com/anoma/juvix/pull/2462
This PR is part of a series implementing:
* https://github.com/anoma/juvix/issues/2336
This PR adds the package file loading function, including a file
evaluation effect. It integrates this with the existing `readPackage`
function and adds tests / smoke tests.
## Package.juvix format
Instead of `juvix.yaml` (which is still supported currently) users can
now place a `Package.juvix` file in the root of their project. The
simplest `Package.juvix` file you can write is:
```
module Package;
import PackageDescription open;
package : Package := defaultPackage;
```
The
[PackageDescription](35b2f618f0/include/package/PackageDescription.juvix)
module defines the `Package` type. Users can use "go-to definition" in
their IDE from the Package file to see the documentation and
definitions.
Users may also import `Stdlib.Prelude` in their Package file. This is
loaded from the global project. No other module imports are supported.
Notes:
* If a directory contains both `Package.juvix` and `juvix.yaml` then
`Package.juvix` is used in preference.
## Default stdlib dependency
The `Dependency` type has a constructor called `defaultStdlib`. This
means that any project can use the compiler builtin standard library
dependency. With `juvix.yaml` this dependency is only available when the
`dependencies` field is unspecified.
```
module Package;
import PackageDescription open;
package : Package := defaultPackage { dependencies := [defaultStdlib] };
```
## Validation
As well as the standard type checking validation that the Juvix compiler
provides additional validation is made on the file.
* The Package module must contain the identifier `package` and it must
have type `Package` that's obtained from the global `PackageDescription`
module.
* Every dependency specified in the Package.juvix must be unique.
* Closes https://github.com/anoma/juvix/issues/2336
## Examples
### Package with name and version
```
module Package;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0};
```
### Package with GitHub dependency
```
module Package;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0;
dependencies := [defaultStdlib;
github (org := "anoma";
repo := "juvix-containers";
ref := "v0.7.1")]};
```
## Package with main and buildDir fields
```
module Package;
import Stdlib.Prelude open;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0;
dependencies := [defaultStdlib;
github (org := "anoma";
repo := "juvix-containers";
ref := "v0.7.1")];
buildDir := just "/tmp/build";
main := just "HelloWorld.juvix"
};
```
The problem with readFile and writeFile from text
[Data.Text.IO](https://hackage.haskell.org/package/text-2.0.2/docs/Data-Text-IO.html)
is that they use the system locale to determine the text encoding
format.
Our assumption is that all Juvix source files are UTF-8 encoded.
I cannot reproduce the issue with using the old APIs on my machine, it
can be reproduced on Arch linux. I'm not sure how to write a specific
test for this.
* Closes https://github.com/anoma/juvix/issues/2472
This PR introduces FileExt type, and consequently, one can generalise
methods and matches based on the file extension; for example,
`parseInputJuvixAsmFile` is now an app. `parseInputFile FileExtJuvixAsm`
- Closes#2293.
- Closes#2319
I've added an effect for termination. It keeps track of which functions
failed the termination checker, which is run just after translating to
Internal. During typechecking, non-terminating functions are not
normalized. After typechecking, if there is at least one function which
failed the termination checker, an error is reported.
Additionally, we now properly check for termination of functions defined
in a let expression in the repl.
- Closes#2258
# Overview
When we define a type with a single constructor and one ore more fields,
a local module is generated with the same name as the inductive type.
This module contains a projection for every field. Projections can be
used as any other function.
E.g. If we have
```
type Pair (A B : Type) := mkPair {
fst : A;
snd : B;
};
```
Then we generate
```
module Pair;
fst {A B : Type} : Pair A B -> A
| (mkPair a b) := a;
snd : {A B : Type} : Pair A B -> B
| (mkPair a b) := b;
end;
```
GEB 0.3.2 introduces the following changes.
* The STLC frontend no longer requires full type information in terms.
The syntax of the terms changed.
* An error node has been introduced which allows to compile Juvix `fail`
nodes.
The following features required for compilation from Juvix are still
missing in GEB.
* Modular arithmetic types ([GEB issue
#61](https://github.com/anoma/geb/issues/61)).
* Functor/algebra iteration to implement bounded inductive types ([GEB
issue #62](https://github.com/anoma/geb/issues/62)).
- 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.
