1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-24 07:57:58 +03:00
Commit Graph

273 Commits

Author SHA1 Message Date
Jan Mas Rovira
2c8a364143
New syntax for function definitions (#2243)
- 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
2023-07-10 19:57:55 +02:00
Jan Mas Rovira
d69d8c6eca
Remove abstract (#2219)
- Closes #2002 
- Closes #1690 
- Closes #2224
- Closes #2237
2023-06-30 15:01:46 +02:00
Jan Mas Rovira
6fb7bbff2d
Move termination checker to Internal (#2209)
- Closes #2203
2023-06-20 11:02:37 +02:00
Paul Cadman
5f3fdb9c08
Support juvix format with no argument to format a project (#2208)
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
2023-06-20 06:32:17 +01:00
Paul Cadman
7840f9fa79
Always print source of formatted file unless --check is specified (#2205)
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
2023-06-19 15:14:59 +01:00
Veronika Romashkina
8e59624ff5
Format returns 0 when file is not formatted (#2181)
`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
2023-06-07 13:53:10 +02:00
Łukasz Czajka
9db16ca87f
Fix 'function not found' error in juvix eval (#2178)
* Closes #2176

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-06-06 13:26:43 +02:00
Łukasz Czajka
5d85cb44f2
Print values in juvix eval (#2179)
* Closes #2177
2023-06-06 12:35:01 +02:00
Paul Cadman
108ccf7dcf
Do not filter unreachable symbols when compiling for REPL (#2172)
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>
2023-06-05 16:52:52 +01:00
Jan Mas Rovira
f4aa70b13d
Finish the new pretty printing algorithm and delete the old one (#2151)
- 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.
2023-06-02 13:02:35 +02:00
Łukasz Czajka
c4c92d5fcf
Allow to specify VampIR variable names (#2141)
* 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;
```
2023-06-01 17:36:47 +02:00
Paul Cadman
40e6648ae1
Use theJUVIX_LLVM_DIST_PATH environment variable to search for the clang executable (#2152)
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
2023-06-01 12:18:31 +02:00
Jan Mas Rovira
88c5dabb6d
Add Semigroup instance for AnsiText (#2140)
`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>
2023-05-31 08:53:08 +01:00
Jan Mas Rovira
f56110b87e
Add :doc command to the repl (#2142) 2023-05-30 18:19:39 +02:00
Jan Mas Rovira
e944f85074
Add :def command to the repl (#2119)
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.
2023-05-30 10:19:09 +02:00
Jan Mas Rovira
4fcb881ebc
Add main field to juvix.yaml (#2120)
- 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>
2023-05-24 15:42:20 +02:00
Veronika Romashkina
acb8b0c773
Fix baseUrl for juvix docs in Doctor command (#2122)
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.
2023-05-24 12:14:30 +02:00
Veronika Romashkina
b4e7dbc7fd
Remove --no-format option (#2121)
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
2023-05-24 10:46:18 +02:00
Paul Cadman
4a1c7a101e
Pass through compile optimization flag to C compiler and disable optimization for --debug (#2106)
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>
2023-05-19 15:29:52 +01:00
Łukasz Czajka
fe78ff451c
Direct translation from normalized JuvixCore to VampIR (#2086)
* 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).
2023-05-19 14:43:45 +02:00
Paul Cadman
ad3607f104
Fix extra whitespace in text rendering of indented empty lines (#2101)
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.
2023-05-19 11:41:28 +02:00
Łukasz Czajka
336a934d18
Normalization by Evaluation (#2038)
* 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`.
2023-05-15 18:01:40 +02:00
Łukasz Czajka
8aa54ecc28
Inlining (#2036)
* 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.
2023-05-15 17:27:05 +02:00
Paul Cadman
8eb4c64f5d
Improve error message when input path doesn't exist (#2092)
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
```
2023-05-15 11:03:09 +02:00
Jan Mas Rovira
b0c566f52d
Partial incremental highlighting (#2053) 2023-05-10 13:09:48 +02:00
Veronika Romashkina
4e1fee1c03
Fix: topCommandInputFile for Format command (#2063)
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
2023-05-10 08:52:23 +02:00
Paul Cadman
6894300e5a
Support module imports in Juvix REPL (#2029)
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>
2023-05-08 12:23:15 +02:00
Jan Mas Rovira
aace4ca514
Fix pipeline setup in the repl (#2046)
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>
2023-05-03 19:04:31 +01:00
Veronika Romashkina
8ab4ccd73b
Make format command's filepath optional (#2028)
# 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>
2023-04-27 17:33:08 +02:00
Łukasz Czajka
c31e373c88
Add: pragma support (#1997)
* 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>
2023-04-26 15:26:13 +02:00
Paul Cadman
d59fca6786
Add juvix clean to remove project build artifact directory (#2018)
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
2023-04-21 14:21:31 +02:00
janmasrovira
3d012cc8fb
Support more paths (#2000)
- 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>
2023-04-19 15:56:48 +01:00
janmasrovira
b2f926d50f
Ide improvements (#2009)
This pr includes the necessary machinery to have type and judoc
information for every identifier. This information is showed in
juvix-mode as a child-frame on the top right corner as showed in the
following screenshot.

![image](https://user-images.githubusercontent.com/5511599/232927816-dbf48ea9-e717-42f2-9c92-14a27a650c87.png)
2023-04-19 10:46:58 +01:00
Paul Cadman
e1a23c677c
Write compile output file to invoke dir by default (#1999)
This PR fixes the issue below and also adds smoke tests for the target
option of the compile command.

* Closes https://github.com/anoma/juvix/issues/1998
2023-04-13 19:57:49 +02:00
Jonathan Cubides
0fcf22f693
Fix: add supported targets as option for compile commands (#1983)
- Closes #1882
2023-04-13 14:16:07 +02:00
janmasrovira
5de0026d83
Add juvix global project under xdg directory and other improvements (#1963)
Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-04-13 11:27:39 +02:00
Łukasz Czajka
34b0969141
Pretty print JuvixCore values consistently with Juvix syntax (#1988)
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
2023-04-12 12:52:40 +02:00
Łukasz Czajka
6d83ba597f
Refactor Core datastructures (#1975)
* Closes #1972 
* Introduces lookup functions for the InfoTable to avoid using HashMap
explicitly and reduce code duplication
2023-04-04 18:58:05 +02:00
Łukasz Czajka
cc2f0608bb
Update the tutorial (#1967)
* 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)
2023-04-03 16:46:53 +02:00
Paul Cadman
9e1e72d6b6
repl: Run disambiguateNames on result node (#1961)
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
2023-04-03 10:58:08 +02:00
Paul Cadman
5d4cb904e8
Add juvix dev repl command (#1941)
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
2023-03-31 00:57:44 +02:00
janmasrovira
23824610c2
Update typecheck command to check for coverage (#1952) 2023-03-30 19:36:38 +02:00
janmasrovira
90a7a5e7e0
Fix REPL state to include enough information to rerun the pipeline (#1911)
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>
2023-03-30 13:39:27 +02:00
Łukasz Czajka
bcf1d0f779
Option --show-args-num (#1946)
* Adds an options to display the `_identifierArgsNum` field when
printing Core definitions.
2023-03-30 12:23:40 +01:00
Paul Cadman
1ab3aa06da
Add juvix format command (#1886)
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>
2023-03-29 15:51:04 +02:00
Łukasz Czajka
3c3e442c81
End-to-end Geb compilation tests (#1942)
* 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)
2023-03-29 14:02:40 +02:00
Łukasz Czajka
df27dc8e3f
Add the --unroll option (#1935)
* Closes #1928

---------

Co-authored-by: janmasrovira <janmasrovira@gmail.com>
2023-03-28 11:41:05 +02:00
Łukasz Czajka
09d307c37b
Polymorphic type inference in Core (#1931)
* 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.
2023-03-27 19:27:10 +02:00
Jonathan Cubides
9f22eaa1cf
Test core to geb translation (#1865)
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
2023-03-27 15:32:03 +02:00
Łukasz Czajka
c9b8cdd5e9
Pattern matching compilation (#1874)
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
2023-03-27 10:42:27 +02:00
Jonathan Cubides
c7e4056077
Add --numeric-version flag (#1918)
As the title says. 

```
❯ juvix --numeric-version
0.3.0
```
2023-03-24 10:45:53 +01:00
Łukasz Czajka
2803f3feee
Fix JuvixAsm validation (#1903)
Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-03-20 12:01:35 +00:00
Łukasz Czajka
ac6d08e259
Add errors to the Core pipeline and check GEB prerequisites (#1871)
* 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
2023-03-20 10:13:07 +01:00
Łukasz Czajka
98b1daec7d
Print JuvixCore correctly (#1875)
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>
2023-03-15 16:41:39 +01:00
Łukasz Czajka
1eadbc4f81
Remove the old C backend (#1862)
* 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
2023-03-14 17:22:32 +01:00
Łukasz Czajka
2d798ec31c
New compilation pipeline (#1832)
* 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>
2023-03-14 16:24:07 +01:00
Jonathan Cubides
0ef464668d
Fix Core-To-Geb translation (#1863)
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.
2023-02-28 18:49:44 +01:00
Jonathan Cubides
9a4da4cab8
Add Geb Backend Evaluator with some extra subcommands (#1808)
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)
2023-02-22 15:27:40 +01:00
janmasrovira
098c256da8
Allow shadowing local variables with let function definitions (#1847)
Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-02-22 10:26:54 +01:00
janmasrovira
f897fc2cc0
Fix juvix init (#1835) 2023-02-10 17:53:23 +01:00
janmasrovira
33a0675c99
Respect the juvix dev highlight --format flag when outputting errors (#1820)
Currently errors were always being highlighted using the emacs backend.
Now they properly depend on the `--format` flag.
2023-02-10 13:43:13 +01:00
janmasrovira
207b1594f8
Add dev core from-concrete command (#1833) 2023-02-10 12:37:28 +01:00
Paul Cadman
e0337c18e4
Add internal core-eval option to evaluate named function identifier (#1819) 2023-02-08 17:23:11 +01:00
Łukasz Czajka
151bba5113
Output proper GEB Lisp programs (#1810)
* Closes #1807
2023-02-08 10:36:22 +01:00
janmasrovira
50aca6f74c
Autocompletion for dev core compilation --target (#1803) 2023-02-02 18:09:22 +01:00
Paul Cadman
672e400a2a
Add REPL option to apply Core transformations (#1796)
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
2023-02-01 13:00:06 +00:00
Łukasz Czajka
a5d19c5881
Basic Geb integration (#1748)
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.
2023-02-01 12:04:05 +01:00
janmasrovira
447f2f1dcf
Keep regular comments in html output (#1766)
- 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.
2023-01-27 13:24:28 +01:00
Paul Cadman
efb7f2abd0
Parse JuvixCore with absolute paths (#1770)
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.
2023-01-26 11:55:06 +00:00
Paul Cadman
b5ffa658ee
Use absolute path in Core Evaluator to generate source file location (#1769)
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.
2023-01-26 09:14:06 +00:00
janmasrovira
88ab622353
Print comments when pretty printing concrete syntax (#1737) 2023-01-24 16:15:24 +01:00
Jonathan Cubides
807b3b1770
Update CI to install Smoke, Github actions, and Makefile fixes (#1735)
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>
2023-01-24 11:50:23 +01:00
Jonathan Cubides
22027f137c
Refactor html command with extra options (#1725)
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.
2023-01-17 18:11:59 +01:00
janmasrovira
f7205915a5
Typecheck let expressions (#1712) 2023-01-17 09:41:07 +01:00
Łukasz Czajka
f2298bd674
JuvixCore to JuvixAsm translation (#1665)
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
2023-01-09 18:21:30 +01:00
Jonathan Cubides
f12648954e
Replace --output-dir flag by --internal-build-dir (#1707) 2023-01-09 15:09:02 +01:00
Jonathan Cubides
5b495681c6
Compiler output (#1705)
Add a global flag `--output-dir to specify where to put the compiler output.
2023-01-06 17:54:13 +01:00
Łukasz Czajka
e928ae7a8d
Add --show-de-bruijn option to juvix repl (#1694) 2023-01-04 17:09:41 +01:00
janmasrovira
af63c36574
Support basic dependencies (#1622) 2022-12-20 13:05:40 +01:00
Paul Cadman
028aaf4b57
Add option to specify Core transformations to dev internal core-eval (#1669)
Add option to specify Core transformations to `internal core-eval`
2022-12-15 08:52:26 +00:00
Łukasz Czajka
d9b020ec27
Remove type arguments and type abstractions from Nodes (#1655) 2022-12-12 14:58:25 +01:00
Łukasz Czajka
73c8bafd09
Add pretty printing to JuvixAsm code (#1650) 2022-12-08 17:09:56 +01:00
Łukasz Czajka
f5de5faaef
Translation from JuvixAsm to C (#1619) 2022-12-06 11:33:20 +01:00
janmasrovira
ebfe412d6f
Auto complete argument of 'dev core read -t' (#1616)
autocomplete transformation list in 'dev core read -t'
2022-11-14 16:29:48 +00:00
janmasrovira
169155690b
Eta expansion at the top of each core function definition (#1481) (#1571) 2022-11-14 16:03:28 +01:00
Paul Cadman
df4036d600
Compute new entrypoint root when loading a file in the REPL (#1615)
* 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
2022-11-10 11:26:38 +00:00
Paul Cadman
6d66d0ab13
Add juvix-repl-mode for emacs (#1612)
* 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
2022-11-09 16:36:40 +01:00
Łukasz Czajka
9d4f843262
Precompute maximum heap allocation (#1608) 2022-11-08 13:42:40 +01:00
Paul Cadman
5d0123beba
Improvements to Juvix REPL (#1607)
* 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
2022-11-07 17:43:30 +00:00
Paul Cadman
a3b2aa6940
Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
Łukasz Czajka
74bfe592f5
Juvix C runtime (#1580) 2022-11-03 09:38:09 +01:00
janmasrovira
b02f2f8e82
Letrec lifting (#1579) 2022-10-21 19:13:06 +02:00
Paul Cadman
9e7a8a98d4
Support go to definition for the standard library (#1592)
* 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
2022-10-19 15:55:16 +01:00
janmasrovira
2062d3d8e5
Properly newline expressions in the pretty printer (#1581) 2022-10-18 17:38:31 +02:00
Łukasz Czajka
f0ade4be7c
JuvixAsm (#1432) 2022-09-29 17:44:55 +02:00
Paul Cadman
a246d57bff
Autocomplete ".jvc" input files for core {eval, read} commands (#1542)
Complete ".jvc" input files for core {eval, read} commands
2022-09-15 16:02:20 +01:00
Paul Cadman
b6f1ecac73
Add --show-de-bruijn to core eval command (#1540)
This option was removed as part of one of the cli refactors
2022-09-15 15:26:02 +01:00
janmasrovira
60d4f0433a
Refactor CLI (#1527) 2022-09-14 16:16:15 +02:00
janmasrovira
380ade56dc
Add CanonicalProjection (#1526)
add CanonicalProjection
2022-09-12 09:44:00 +01:00
janmasrovira
42d8c6fcf6
Enable autocompletion for the --theme flag (#1519) 2022-09-06 16:15:57 +02:00