1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-13 11:16:48 +03:00
Commit Graph

808 Commits

Author SHA1 Message Date
Łukasz Czajka
45aa415b71
Short syntax for sequences of function and datatype parameters (#1809) 2023-02-06 19:01:54 +01:00
janmasrovira
929a8658ac
Special syntax for case (#1800)
- Closes #1716

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-02-06 14:53:35 +01:00
Łukasz Czajka
e5a9853998
Remove the usage annotation syntax (#1805) 2023-02-03 19:16:06 +01:00
Łukasz Czajka
14d1e5d614
Mid-square hashing implemented in JuvixCore (#1804)
- Can be compiled to GEB after merging #1778.
2023-02-03 13:09:41 +01:00
Łukasz Czajka
5e06441f48
Support integers in the GEB backend (#1778)
* Depends on PR #1748 
* Closes #1753
2023-02-03 12:45:57 +01:00
janmasrovira
50aca6f74c
Autocompletion for dev core compilation --target (#1803) 2023-02-02 18:09:22 +01:00
janmasrovira
fab40c6c99
Support letrec lifting without lambda lifting (#1794)
- Closes #1756
2023-02-02 11:10:12 +01:00
janmasrovira
3c33916034
Remove braces from let expressions (#1790) 2023-02-01 19:22:43 +01:00
Łukasz Czajka
5ec80641cb
Adapt benchmarks to the new pipeline (#1795)
Closes #1742
2023-02-01 15:44:09 +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
janmasrovira
f0e493f86f
Use the reader effect in the Core to GEB translation (#1791) 2023-02-01 12:53:57 +01: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
Jonathan Cubides
a5623c54ae
Use restore/save github action to speed up the CI testing (#1783)
This PR addresses a caching issue in our CI by streamlining each
operating system's build and test processes, reducing CI time. 🤞 Also,
our caching strategy has been updated with the new restore/save actions.
For example, we aim to cache the .stack folder, and if the stack build
is successful, the .stack-build. The building documentation job
continues depending on the Linux build. Upon merging this PR, we get
back to the point where the CI maintain a cache for each OS to be shared
among all PRs, significantly reducing CI testing time. The expected
scenario is as follows. The CI can take, on average, 35' in Linux to
build and test everything. Using caching, that time is reduced to less
than 10'. macOS is a different story. It can easily take one hour, and
even more, the first time to build and test the project. After that, it
might take an average of 20'.

- Caching strategies
[descriptions](https://github.com/actions/cache/blob/main/caching-strategies.md#saving-cache-even-if-the-build-fails)
- Closes #1776
2023-01-31 19:34:05 +01:00
Łukasz Czajka
4be4d58d30
String builtins (#1784)
- Progress for #1742 
* Adds builtin primitives for operations on strings and removes the
corresponding foreign & compile blocks.
2023-01-31 18:31:04 +01:00
janmasrovira
e3860aef9f
Fix termination with as-patterns (#1787) 2023-01-31 17:54:18 +01:00
Paul Cadman
feff86d576
Translate as-pattern binders to Core PatternBinders (#1789)
Before this change, nested as-patterns (i.e as-patterns binding
arguments to constructors) were not translated to Core pattern binders.

This meant that the following function would crash the compiler:

```
f : List Nat -> List Nat;
f  (x :: a@(x' :: xs)) := a;
f _ := nil;
```

i.e the nested as-pattern `a` was ignored in the internal to core
translation.

This commit translates each as-pattern to a Core `PatternBinder`.

* Fixes https://github.com/anoma/juvix/issues/1788
* Fixes https://github.com/anoma/juvix/issues/1738
2023-01-31 14:32:50 +00:00
janmasrovira
38622b28d1
Allow type signatures to have a body (#1785)
- Closes #1637.

A function type signature is now allowed to have a body. This is valid
for both top level and let definitions.
```
not : Bool -> Bool := λ {
 | true := false
 | false := true
};
```
2023-01-31 08:46:53 +00:00
Paul Cadman
0d18b136c4
Track builtins in the Core InfoTable (#1782)
This PR adds a new field `infoBuiltins : HashMap BuiltinPrim IdentKind`
to the Core InfoTable. This is used to register builtin inductive,
constructors and functions against their corresponding Core
symbols/tags.

The point of doing this is to make it easier to lookup the Infos for
builtins during the internal to core translation:
d91241a685/src/Juvix/Compiler/Core/Translation/FromInternal.hs (L65)

This is one proposed approach, I think Jan mentioned using the Builtins
effect for this but it doesn't seem appropriate to expose the
registration function from the Builtins effect at this part of the code.
Perhaps I misunderstood, if so I'm happy to revisit this refactor.
2023-01-30 17:19:44 +01:00
janmasrovira
d8ba7ca36f
Pipes for lambda clauses (#1781)
- Closes #1639
2023-01-30 12:06:18 +01:00
Jonathan Cubides
6d49c9c9f1
Fix minor issue with ==% for type equality (#1780) 2023-01-27 19:34:25 +01:00
Jonathan Cubides
384653f630 No run jobs after pr is closed/merged, docs only on pushes to main (#1779) 2023-01-27 19:01:25 +01:00
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