- 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#2060
- Closes#2189
- This pr adds support for the syntax described in #2189. It does not
drop support for the old syntax.
It is possible to automatically translate juvix files to the new syntax
by using the formatter with the `--new-function-syntax` flag. E.g.
```
juvix format --in-place --new-function-syntax
```
# Syntax changes
Type signatures follow this pattern:
```
f (a1 : Expr) .. (an : Expr) : Expr
```
where each `ai` is a non-empty list of symbols. Braces are used instead
of parentheses when the argument is implicit.
Then, we have these variants:
1. Simple body. After the signature we have `:= Expr;`.
2. Clauses. The function signature is followed by a non-empty sequence
of clauses. Each clause has the form:
```
| atomPat .. atomPat := Expr
```
# Mutual recursion
Now identifiers **do not need to be defined before they are used**,
making it possible to define mutually recursive functions/types without
any special syntax.
There are some exceptions to this. We cannot forward reference a symbol
`f` in some statement `s` if between `s` and the definition of `f` there
is one of the following statements:
1. Local module
2. Import statement
3. Open statement
I think it should be possible to drop the restriction for local modules
and import statements
When `juvix format` is invoked from some directory within a juvix
project then the formatter is run on all the files contained in the
project.
If `juvix format` is run from some directory outside of a Juvix project
then an error is reported. The user gets the same error as they would
get if
`juvix format` was run with a directory argument that is not within a
Juvix project.
* Closes https://github.com/anoma/juvix/issues/2087
This PR was already merged in https://github.com/anoma/juvix/pull/2173,
but main was subsequently forced pushed as part of the 0.4.0 release and
these changes were erased by mistake.
This PR changes the behaviour of the formatter when run on files that
are already formatted. Previously the source of a file that was already
formatted was not output by the formatter.
After this PR, the formatter always outputs the contents of a formatted
file (when used on a single file, and if the --check option is not
specified).
If the `format: false` pragma is set then the source is echoed verbatim,
without highlighting (because it's not possible to get the highlighting
without the formatting).
This probably helps implementing the formatter in the vscode extension,
see https://github.com/anoma/vscode-juvix/issues/98
`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.
* 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>
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>
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
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.
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 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
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 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>
# 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#1965
* Implements the `unroll` pragma to control the unrolling depth on a
per-function basis.
* Implements parsing of the `inline` pragma.
---------
Co-authored-by: janmasrovira <janmasrovira@gmail.com>
This PR adds the `juvix clean` command to the CLI that removes the Juvix
project build directory.
It respects the `--internal-build-dir` global option:
```
$ juvix compile Foo.juvix --internal-build-dir /tmp/build
$ juvix clean --internal-build-dir /tmp/build
```
In addition this PR fixes the `juvix format` program brief description
string. This was too long for the `juvix --help` display. The longer
description is now only displayed when `juvix format --help` is run.
* Closes https://github.com/anoma/juvix/issues/2017
- 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
* Removes the discussion of IO from the tutorial
* Expands the section about coverage checking
* Fixes typos and language mistakes
* Updates the changelog in the docs folder (this doesn't happen
automatically with the new release)
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>
This PR adds `juvix format` that can be used to format either a single
Juvix file or all files in a Juvix project.
## Usage
```
$ juvix format --help
Usage: juvix format JUVIX_FILE_OR_PROJECT [--check] [--in-place]
Format a Juvix file or Juvix project
When the command is run with an unformatted file it prints the reformatted source to standard output.
When the command is run with a project directory it prints a list of unformatted files in the project.
Available options:
JUVIX_FILE_OR_PROJECT Path to a .juvix file or to a directory containing a
Juvix project.
--check Do not print reformatted sources or unformatted file
paths to standard output.
--in-place Do not print reformatted sources to standard output.
Overwrite the target's contents with the formatted
version if the formatted version differs from the
original content.
-h,--help Show this help text
```
## Location of main implementation
The implementation is split into two components:
* The src API: `format` and `formatProject`
73952ba15c/src/Juvix/Formatter.hs
* The CLI interface:
73952ba15c/app/Commands/Format.hs
## in-place uses polysemy Resource effect
The `--in-place` option makes a backup of the target file and restores
it if there's an error during processing to avoid data loss. The
implementation of this uses the polysemy [Resource
effect](https://hackage.haskell.org/package/polysemy-1.9.0.0/docs/Polysemy-Resource.html).
The recommended way to interpret the resource effect is to use
`resourceToIOFinal` which makes it necessary to change the effects
interpretation in main to use `Final IO`:
73952ba15c/app/Main.hs (L15)
## Format input is `FilePath`
The format options uses `FilePath` instead of `AppFile f` for the input
file/directory used by other commands. This is because we cannot
determine if the input string is a file or directory in the CLI parser
(we require IO). I discussed some ideas with @janmasrovira on how to
improve this in a way that would also solve other issues with CLI input
file/parsing but I want to defer this to a separate PR as this one is
already quite large.
One consequence of Format using `FilePath` as the input option is that
the code that changes the working directory to the root of the project
containing the CLI input file is changed to work with `FilePath`:
f715ef6a53/app/TopCommand/Options.hs (L33)
## New dependencies
This PR adds new dependencies on `temporary` and `polysemy-zoo`.
`temporary` is used for `emptySystemTempFile` in the implementation of
the TempFile interpreter for IO:
73952ba15c/src/Juvix/Data/Effect/Files/IO.hs (L49)
`polysemy-zoo` is used for the `Fresh` effect and `absorbMonadThrow` in
the implementation of the pure TempFile interpreter:
73952ba15c/src/Juvix/Data/Effect/Files/Pure.hs (L91)
NB: The pure TempFile interpreter is not used, but it seemed a good idea
to include it while it's fresh in my mind.
* Closes https://github.com/anoma/juvix/issues/1777
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
* 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)
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
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.
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 converts the Core evaluator filepath to an absolute path
before calling `mkLoc`.
Before this fix, the Core evaluator would crash if it encountered an
error instead of displaying the error if called on a relative path.
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
* Add shelltests for `juvix repl`
* repl: Compute entrypoint root when loading a file
Previously the REPL would use app root (which could be the current
directory or the project root of the initially loaded file). Thus files
in a different project could not be loaded.
The entrypoint root must be computed each time a new file is `:load`ed.
Adds shell-tests for REPL commands
* Move preludePath to Juvix.Extra.Paths
* Adds a major mode for juvix-repl
* juvix-mode: C-c C-l loads file into REPL, if the REPL is running
* Detect ANSI support in Emacs REPL / shell by using hSupportsANSIColor API
* Disable comint echo handling. Juvix REPL does not echo
* repl: whitespace strip input to compile/eval/infer commands
* 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
* Remove ParserParams
ParserParams is only used to record the root of the project, which is
used to prefix source file paths. However source file paths are always
absolute so this is not required.
* Add GetAbsPath to Files effect
The Files effect is not responsible for resolving a relative module
path into an absolute path on disk. This will allow us to resolve
relative module paths to alternative paths, for example to point to the
standard library on disk.
* Files effect getAbsPath returns paths within the registered standard
library
This means that the standard library can exist on disk at a different
location to the Juvix project.
A command line flag --stdlib-path can be specified to point to a
standard library, otherwise the embedded standard library is written to
disk at $PROJ_DIR/.juvix-build/stdlib and this is used instead.
* Recreate stdlib dir only when juvix version changes
* Add UpdateStdlib to the Files effect
* Add comment for stdlibOrFile
* Remove spurious import
* Export all functions with alphanum names in entrypoint
Set the export_name attribute on every function signature that has a
fully alpha numeric name.
* Adds a non-WASI target to compile command
WASM libraries we want to run in the browser and in Anoma VM do not have
access to the WASI runtime. For this usecase we need a target runtime
that does not use the WASI runtime.
A `wasi-` prefix is added to existing compile targets and introduce a new
standalone target. This target does not have IO functions like
`putStrLn` and `exit` calls `__builtin_trap` which corresponds to the
`unreachable` WASM instruction.
In the non-exhaustive case error a debug message is emitted to tell the
user which function had the error. This is now abstracted to a `debug`
function in the runtime which calls `putStrLn` in the case of WASI and
is no-op in the case of non-WASI.
Tests are added which check that exported names can be called with the
correct name and result.
* Moves walloc to a common directory
* w.i.p
* Added strict positivity condition for datatypes w.i.p
* Add negative test for str.postivity check
* Add some revisions
* the branch is back to feet
* w.i.p add lots of traces to check alg.
* Add more test and revisions
* Add negative and positive test to the new flag and the keyword
* Fix shell tests.
* Make pre-commit happy
* Fix rebase conflicts
* Make pre-commit happy
* Add shell test, rename keyword, fix error msg
* Revert change
* Necessary changes
* Remove wrong unless
* Move the positivity checker to its own folder
* Add missing juvix.yaml
* Add a negative test thanks to jan
* make some style changes
* Make ormolu happy
* Remove unnecessary instance of Show
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Renaming MiniJuvix to Juvix
* Make Ormolu happy
* Make Hlint happy
* Remove redundant imports
* Fix shell tests and add target ci to our Makefile
* Make pre-commit happy
* Embed stdlib in minijuvix library
We add a new step at the beginning of the pipeline called Setup that
registers the modules in the standard library with the Files effect. The
standard library is then used when the Scoper queries the Files effect
for modules as it resolves import statements.
Use of the standard library can be disabled using the global
`--no-stdlib` command-line option.
* CI: Checkout submodules recursively for stdlib
* Add a new `--no-stdlib` option to shell check
* Poke CI
* CI: Checkout submodules in the test job
* match inductive definitions
* progress towards builtins
* more progress towards builtin types
* add more builtins
* add some errors
* add reverse table to builtins
* Squashed commit of the following:
commit 93333de502d8dd546eb8edf697ca7eef972ea105
Author: Paul Cadman <git@paulcadman.dev>
Date: Mon Jun 27 18:21:30 2022 +0100
Use builtin names for match and project functions
Add an implementation of nat for the standalone backend
commit 868d2098ee57b7acbca84512b6e096650eeeb22d
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon Jun 27 18:15:29 2022 +0200
add builtin information to ClosureInfo
commit 32c78aceb19ee4010d66090a3c4e6025621b5c1f
Author: Paul Cadman <git@paulcadman.dev>
Date: Mon Jun 27 12:52:10 2022 +0100
Refactor BuiltinEnum to sum type of each Builtin
commit 55bb72ab12a8fb7d10070c2dee5875482453b7c6
Author: Paul Cadman <git@paulcadman.dev>
Date: Fri Jun 24 14:44:28 2022 +0100
Add Builtin information to Mono InfoTable
commit a72368f2e3af20baaf44c5e21fa7e6a469cf1ac5
Author: Paul Cadman <git@paulcadman.dev>
Date: Fri Jun 24 14:41:51 2022 +0100
Add Bitraversable to Prelude
commit afa3153d82a9509b0882e7ca99830040fad9ef65
Author: Paul Cadman <git@paulcadman.dev>
Date: Fri Jun 24 14:41:39 2022 +0100
Remove unused import
commit ea0b7848fb80970e03a0561be3fb4448486a89a9
Author: Paul Cadman <git@paulcadman.dev>
Date: Thu Jun 23 13:54:58 2022 +0100
Use projection functions instead of direct member access
* Avoid shadowing C runtime names in foreign block
* Fix formatting
* Update C names for builtin functions
* Add prim_ prefix to builtin C names
Implement builtins for standalone and libc backends
* Update ormolu action
* ci: run all tests for draft PRs
Co-authored-by: Paul Cadman <git@paulcadman.dev>
* work in progress towards implicit arguments
* Wip towards implicit types
* improve arity checker
* Add version of SimpleFungibleToken with implicit arguments
* guess arity of body before checking the lhs of a clause
* add ArityUnknown and fix some tests
* wip: proper errors in arity checker
* fix bugs, improve errors and add tests
* format
* set hlint version to 3.4 in the ci
* update pre-commit version to 3.0.0
* minor changes
* added more revisions
* minor
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
* Remove input file fields from command opts
* [cli] Make version and help commands
* Fix on reviews
* Fixes for dealing with global options inside subcmds
* Fix minijuvix emacs mode and add some instance to GlobalOpts
* Remove unrelated code
* Propagate globals opts in each cmd parser
* Add initial shell tests
* Add test-shell to makefile and CI
* Fix CI: adding .local/bin to PATH
* Fixing CI
* Installing shelltest just before running it
* Install app for shell testing
* Hide global flags after cmd. Fix shell tests accordingly.
* Fixing CI
* Shell test only run on ubuntu for now
* [app] Add compile command
The compile command drives the (external) clang compiler to build a WASM
binary from a minijuvix file.
The intermediate C files are stored in .minijuvix-build directory
relative to the directory where the command is executed.
The user can specify which runtime (standalone and libc) to build
against.
The file-embed library is used to embed the runtime files into the
minijuvix binary.
* TemplateHaskell is a default extension
* [app] Add the .minijuvix-build dir in the root of the project
* [app] Derive the default output filename from the inputfile
* [chore] Add .minijuvix-build to .gitignore
* [WIP] EntryPoint now has options. --no-termination is a new global opt.
* Add TerminationChecking to the pipeline
* Add TerminationChecking to the pipeline
* Keep GlobalOptions in App
* Fix reviewer's comments
* delete unnecessary parens
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* w.i.p adoption of generic error type
* harmonize
* Remove the use of Error effect for internal bugs
* add location information to expression atom list
* Add GenericError instance for PatternAtoms
* Remove Maybe GenericError occurrences
* [ci] fix draft job's condition
* minor changes
* [stack] macos support ghc-opts
* Fix reviewer's comments
* remove accidentally commited file
* refactor to avoid duplication
* fix
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* add face and handling of not in scope symbol error
* small fix
* generic errors wip
* add App effect
* format
* add flycheck-minijuvix
* use absolute paths and refactor
* fix dir0
* add generic error instances and improve some errors
* format
* qualify strings
* use AnsiText
* add ToGenericError instances for the type checker errors
* improve error message
* improve handling of parsing errors
* [cbackend] Adds an AST for C
This should cover enough C to implement the microjuvix backend.
* [cbackend] Add C serializer using language-c library
We may decide to write our own serializer for the C AST but this
demonstrates that the C AST is sufficient at least.
* [cbackend] Declarations will always be typed
* [cbackend] Add CPP support to AST
* [cbackend] Rename some names for clarity
* [cbackend] Add translation of InductiveDef to C
* [cbackend] Add CLI for C backend
* [cbackend] Add stdbool.h to file header
* [cbackend] Allow Cpp and Verbatim code inline
* [cbackend] Add a newline after printing C
* [cbackend] Support foreign blocks
* [cbackend] Add support for axioms
* [cbackend] Remove code examples
* [cbackend] wip FunctionDef including Expressions
* [parser] Support esacping '}' inside a foreign block
* [cbackend] Add support for patterns in functions
* [cbackend] Add foreign C support to HelloWorld.mjuvix
* hlint fixes
* More hlint fixes not picked up by pre-commit
* [cbackend] Remove CompileStatement from MonoJuvix
* [cbackend] Add support for compile blocks
* [cbackend] Move compileInfo extraction to MonoJuvixResult
* [minihaskell] Fix compile block support
* [chore] Remove ununsed isBackendSupported function
* [chore] Remove unused imports
* [cbackend] Use a Reader for pattern bindings
* [cbackend] Fix compiler warnings
* [cbackend] Add support for nested patterns
* [cbackend] Use functions to instantiate argument names
* [cbackend] Add non-exhaustive pattern error message
* [cbackend] Adds test for c to WASM compile and execution
* [cbackend] Add links to test dependencies in quickstart
* [cbackend] Add test with inductive types and patterns
* [cbackend] Fix indentation
* [cbackend] Remove ExpressionTyped case
https://github.com/heliaxdev/minijuvix/issues/79
* [lexer] Fix lexing of \ inside a foreign block
* [cbackend] PR review fixes
* [chore] Remove unused import
* [cbackend] Rename CJuvix to MiniC
* [cbackend] Rename MonoJuvixToC to MonoJuvixToMiniC
* [cbackend] Add test for polymorphic function
* [cbackend] Add module for string literals
* Parsing terminating keyword
* cosmetics
* Add support for `terminating` keyword to function decl.
* Minor replacement
* Fix .mjuxix to .mjuvix and the module name
