1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-25 16:45:20 +03:00
Commit Graph

89 Commits

Author SHA1 Message Date
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
Ł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
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
Ł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
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