1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-14 17:32:00 +03:00
Commit Graph

787 Commits

Author SHA1 Message Date
Paul Cadman
aac22addc1
Add builtin nat and bool types as start nodes in reachability analysis (#1775)
The integer to Nat translation in the Internal to Core translation
depends on both Nat and Bool builtin types being in the InfoTable.
544bddba43/src/Juvix/Compiler/Core/Translation/FromInternal.hs (L67)

If the root module does not contain an explicit reference to the builtin
Bool (for example) then builtin Bool type is filtered out by the
reachability analysis and therefore is not available at transltaion
time.

In this commit we add both builtin Nat and builtin Bool as start nodes
in the reachability analysis to guarantee that they will not be filtered
out.

- Fixes https://github.com/anoma/juvix/issues/1774
2023-01-27 15:21:38 +00:00
Jonathan Cubides
8915177111
Update pre-commit (#1772)
Regular update
2023-01-27 14:24:10 +00: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
Jonathan Cubides
544bddba43
Add debugging builtin functions trace and fail (#1771)
- Closes #1731
2023-01-27 12:45:38 +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
Łukasz Czajka
acea6615a4
Lazy boolean operators (#1743)
Closes #1701
2023-01-25 18:57:47 +01:00
Jonathan Cubides
cd2af04601
Install wasmer binary from Github releases (#1765)
The current Github action responsible for installing Wasmer fails from
time to time, and it also is outdated, not following the new NodeJS 16
requirement by Github.

We could use https://github.com/jaxxstorm/action-install-gh-release
instead, but unfortunately, it does not have the proper support to
expose the binaries contained in an inner folder, as in the case with
the Wasmer release. In the meantime, let's use my
[fork](https://github.com/jonaprieto/action-install-gh-release) while I
open PR to the main repository.
2023-01-25 13:45:04 +00:00
Jonathan Cubides
444fdc4416
Run the new Juvix formatter for all the Juvix examples (#1764)
Juvix now provides an intial and functional formatting tool by calling
the command `juvix dev scope file --with-comments` .

This PR adds a new Makefile target `juvix-format` to format all the
Juvix programs we showcase in the documentation as Juvix-projects, i.e.,
files from the `examples` directory. Note the corresponding target in
the Makefile also calls the typechecker to ensure the programs do not
have type errors introduced by the formatter, considering also that all
the Juvix files in the `examples` directory type-checked before this PR.
Thus, we should preserve that state. Finally, I included `juvix-format`
as part of the `check` target, so we widen the testing of the compiler.

The formatter is not perfect yet, so we need to fix some formatting
issues manually.
For example, the end of the line is modified by the formatting. We can
fix this by calling after
`make pre-commit`.
2023-01-25 13:52:04 +01:00
janmasrovira
830afad187
Fix let expressions in the repl (#1763)
- Fixes #1739
2023-01-25 09:06:29 +00:00
Jonathan Cubides
01d6a7301f
Fix broken links and other improvements (#1761) 2023-01-24 17:21:35 +01:00
janmasrovira
c1020f9adb
Improve arity inference for repl expressions (#1762)
Closes #1721.

Now the arity checker does not add an unnecessary hole and so the repl
displays the type properly:

![image](https://user-images.githubusercontent.com/5511599/214322656-706d6bd7-5fbe-42dd-adf7-cc9170d001b0.png)
2023-01-24 15:49:37 +00:00
janmasrovira
88ab622353
Print comments when pretty printing concrete syntax (#1737) 2023-01-24 16:15:24 +01:00
Paul Cadman
dd4aab16b6
Translate Nat builtins to the correct Core Ops (#1760) 2023-01-24 13:37:12 +00:00
Jonathan Cubides
2094e5daea
Remove hlint from the CI and pre-commit config (#1759) 2023-01-24 13:55:12 +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
Paul Cadman
c66720d6d9
Fix demo example build (#1757)
The docs build was failing because it was trying to build the Demo
example from the wrong directory.
2023-01-23 19:33:55 +00:00
Jonathan Cubides
9de850df75
Move juvix-mode to a separate repository (#1744)
The new repo is https://github.com/anoma/juvix/mode
2023-01-23 17:09:58 +01:00
Łukasz Czajka
43d114f9b1
Adapt Juvix programs to the new pipeline (#1746)
Progress for #1742 

* Remove putStr and putStrLn
* Remove named Nats (one, two, ...)
2023-01-23 14:57:01 +01:00
Łukasz Czajka
83853f817b
Fix link in README for the new docs (#1745) 2023-01-23 12:56:56 +01:00
Paul Cadman
b00d4b2270
Fix macOS CI build (#1747)
We need to use the homebrew Clang/LLVM installation to build the Juvix
runtime because macOS ships with a version of Clang/LLVM that does not
support the wasi target.

The GitHub action runner agent has the homebrew packaged Clang/LLVM
installed but it is not on the shell PATH.

We were using `brew --prefix llvm@14` to point to the homebrew
Clang/LLVM installation. However this breaks when the runner image is
updated to a new version of llvm.

So we switch to using `brew --prefix llvm` which will resolve to the
latest (and in this case only) version of homebrew Clang/LLVM. This will
be stable when Clang/LLVM is updated to a new version.
2023-01-23 11:43:20 +01:00
Jonathan Cubides
48558dccd0 Bump up version to v0.2.9 2023-01-19 15:44:25 +01:00
Łukasz Czajka
b95abeaada
Restructure the documentation and add a tutorial (#1718)
* Closes #1597 
* Closes #1624 
* Closes #1633 

The tutorial uses syntax which has not been implemented yet: it depends
on
- #1637, 
- #1716, 
- #1639,
- #1638.

The tutorial also assumes the following issues are done: 
- #1720, and
- #1701.

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-01-19 13:28:21 +01:00
Łukasz Czajka
ecac5e07c7 Translate 'let' to Core (#1740)
Closes #1351
2023-01-19 12:56:37 +01:00
Łukasz Czajka
6499100d67 Add test for div and mod (#1741) 2023-01-19 12:52:51 +01:00
Jonathan Cubides
8be1fccfbd Add missing juvix.yaml to Demo 2023-01-18 11:53:27 +01:00
Jonathan Cubides
f2cc163998
Add initial setup for codespaces (#1713)
Once this PR is merged, Github codespaces will be available,
facilitating contributions from all kinds.

- Juvix Haskell Project CodeSpace

[![Open in GitHub
Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope)

- Juvix Standard Library CodeSpace

[![Open in GitHub
Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=455254004)

Note that the change here to REAMDE.org only adds a badge that opens the
Juvix Standard Lib Open Spaces. Such an environment quickly loads the
Juvix binary, examples from anoma/juvix/examples, and all the files from
the Standard library. One needs more than 15 GB of memory RAM and more
than 15 GB of storage to load the Juvix Haskell project properly. These
are requirements that are not included in the free plan offered with
GitHub Codespace.
2023-01-18 11:25:18 +01:00
Jonathan Cubides
ef310be94b
Update stack.yaml (#1734) 2023-01-18 10:23:14 +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
742a0e53dd
Add a new example Juvix Demo (#1736) 2023-01-17 17:45:26 +01:00
Łukasz Czajka
6bb3227ce0
Fix Nat builtins (#1733) 2023-01-17 17:11:31 +01:00
Łukasz Czajka
204113677f
Script to count LOC (#1732) 2023-01-17 15:32:05 +01:00
janmasrovira
0193a33d4c
Fix inference loop (#1726) 2023-01-17 13:28:38 +01:00
janmasrovira
f7205915a5
Typecheck let expressions (#1712) 2023-01-17 09:41:07 +01:00
Paul Cadman
d2a7b8e2b2
Give a proper type to literal Strings (#1730) 2023-01-16 18:15:25 +00:00
Paul Cadman
ff748b988e
Do not filter implicit args in internal to core translation (#1728)
The internal to core translation was removing implicit arguments from
function definitions and applications. This is incorrect as the implicit
bindings are required when translating the following (in `csuc`, the
binding of the implicit argument is required in an application on the
rhs):

```
Num : Type;
Num := {A : Type} → (A → A) → A → A;

csuc : Num → Num;
csuc n {_} f := f ∘ n {_} f;
```

Apart from removing this filter from function and application
translation, this required the following changes:

ConstructorInfo:
The _constructorArgsNum field must include the number of type parameters
of its inductive type.

PatternConstructorApp:
The pattern arguments must include wildcards for the implicit type
parameters passed to the constructor.

BuiltinIf:
The BuiltinIf expression is passed an implicit type argument that must
be removed when translating to Core if.

LitString:
A literal string is a function with an implcit type argument. So this
must be a translated to a lambda where the type argument is ignored.

Fixes https://github.com/anoma/juvix/issues/1714
2023-01-16 14:13:17 +00:00
Paul Cadman
0ac9eb1ab4
Fix de Brujin indexing of lambda arguments (#1727)
A lambda:

```
\ { v0 := b0 ; v1 := b1 ; ... ; vn := bn }
```

should be translated to:

```
λ? (λ? ... (λ? (match ?$0, ?$1, ... , ?$n with ...)))
```

i.e the de Brujin index of the values in the match always start from 0.

Fixes: https://github.com/anoma/juvix/issues/1695
2023-01-16 11:13:39 +00:00
janmasrovira
d5bd3d4fa1
Remove wildcard patterns from Internal (#1724)
This pr removes wildcard patterns from the Internal language.
Wildcards are translated to variables with generated names.
This should resolve the issue of having unbound names after inference
2023-01-13 18:00:07 +00:00
Łukasz Czajka
186f4f66ef
Tests for the new compilation pipeline (#1703)
Adds Juvix tests for the compilation pipeline - these are converted from
the JuvixCore tests (those that make sense). Currently, only the
translation from Juvix to JuvixCore is checked for the tests that can be
type-checked. Ultimately, the entire compilation pipeline down to native
code / WebAssembly should be checked on these tests.

Closes #1689
2023-01-12 11:22:32 +01:00
Łukasz Czajka
df4187a25f
Improve error message for confusing ':=' with '=' (#1715)
Closes #1483 

The error now points to the offending `=`, works correctly with
multi-line clauses, and explains exactly what's wrong. E.g. for
```agda
f : Nat → Nat → Nat;
f zero x = x;
```
we get
```
  |
6 | f zero x = x;
  |           ^
expected ":=" instead of "="
```
A minor disadvantage of the proposed solution is that now it's
impossible to use `=` without parentheses as a top variable name in a
pattern, e.g.
```
f zero = := =;
```
gives an error.

However, if one really wants to name a variable `=`, it is enough just
to enclose it in parentheses:
```agda
f : Nat → Nat → Nat;
f zero (=) := =;
f (suc n) (=) := f n =;
```

I believe this slight non-uniformity is well worth the increased
usability due to a better error message. Confusing `:=` with `=` is very
common. Using `=` as a variable name in a top pattern is rare.

Co-authored-by: janmasrovira <janmasrovira@gmail.com>
2023-01-11 16:43:16 +01:00
janmasrovira
f1ca889997
Fix #1704 (#1711) 2023-01-10 17:31:15 +01:00
Jonathan Cubides
8805a02eff
Use Smoke instead of shelltestrunner (#1710)
This PR adds smoke tests using [Smoke
tool](https://github.com/SamirTalwar/smoke) for all the shell tests we
have. One reason for adopting Smoke instead of the previous tool,
`shelltestrunner`, is that tests are declared cleanly and simply using
Smoke Yaml syntax compared to shelltestrunner's syntax.

To add a new smoke test, create a file with the suffix ".smoke.yaml" in
the `tests/smoke` folder. In such a folder, you can also find examples
of how to test the CLI.
2023-01-10 12:49:56 +01:00
janmasrovira
3b452e7d76
Fix #1693 (#1708) 2023-01-09 18:56:28 +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
janmasrovira
6a571e3d28
Automatized benchmarks (#1673) 2023-01-05 17:48:26 +01:00
Łukasz Czajka
638cd0ebb5
Nat builtins (#1686)
* Fixes #1678.
* Adds the `clean-juvix-build` Makefile target, which removes all
`.juvix-build` directories in the project (necessary to do after
changing the standard library).
* Depends on PR #1688. The tests go through without merging this PR, but
it's a bug. The present PR requires the possibility to use the
`terminating` keyword with the `div` built-in, which possibility is
provided by PR #1688.
2023-01-05 16:39:40 +01:00
Jonathan Cubides
d48e3bd16a
Allow optional pipe before the first constructor for inductive type declarations (#1699) 2023-01-05 11:28:54 +01:00
Paul Cadman
8ef970d3fd
Add printString and printBool support to legacy C backend (#1698)
This PR implements `printString` and `printBool` builtins for the legacy
C backend. Previously IO for strings was done using compile blocks with
included C code.

Fixes https://github.com/anoma/juvix/issues/1696
2023-01-04 18:02:02 +01:00