This PR updates the juvix-stdlib submodule. In particular the update
contains the new traits implemented in
https://github.com/anoma/juvix-stdlib/pull/54.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
# 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>
This PR adds testing for the core-to-geb translation.
It works as follows:
1. Parse the Juvix Core file.
2. Prepare the Juvix Core node for translation to Geb.
3. Translate the Juvix Core node to Geb.
5. Perform type checking on the translated Geb node to ensure that the
types
from the core node make sense in the Geb context and avoid any Geb
runtime
errors.
6. Evaluate the Juvix Core node to see if it produces the expected
result.
7. Translate the result of the evaluated Juvix Core node to Geb for
comparison
with the expected output later.
8. Compare the result of the evaluation of the Geb term produced in step
3
with the result of the evaluation of the Geb term produced in step 6 to
ensure consistency.
9. If step 8 succeeds, then compare the output of step 6 (the evaluation
of the core
node) with the expected output (given in Geb format) to ensure that
the program is functioning as intended.
This PR goes after:
- https://github.com/anoma/juvix/pull/1863
and
https://github.com/anoma/juvix/pull/1832
This implements a basic version of the algorithm from: Luc Maranget,
[Compiling pattern matching to good decision
trees](http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf). No
heuristics are used - the first column is always chosen.
* Closes#1798
* Closes#1225
* Closes#1926
* Adds a global `--no-coverage` option which turns off coverage checking
in favour of generating runtime failures
* Changes the representation of Match patterns in JuvixCore to achieve a
more streamlined implementation
* Adds options to the Core pipeline
* Depends on PR #1909
* Closes#1750
* Adds recursion unrolling tests on JuvixCore
* Adds a version of the mid-square hash example without the recursion
manually unrolled
For now, the recursion is always unrolled to a fixed depth (140). In the
future, we want to add a global option to override this depth, as well
as a mechanism to specify it on a per-function basis. In a more distant
future, we might want to try deriving the unrolling depth heuristically
for each function.
In this PR I will add tests for the example programs in
`examples/milestone`.
There's currently an runtime assertion error generated by the Hanoi
example https://github.com/anoma/juvix/issues/1919, so it'd be good to
test these programs in the future.
This PR goes after:
- #1797
Included in this PR:
- Add Clang formatting (v.15) as part of the pre-commits.
- Add new pre-commits:
- forbid binary files
- check toml files for mdbook
- detect-private-key
- format-juvix-examples: check all the Juvix programs in the `examples`
folder type-check for local runs.
- Remove .pre-commit-hooks and add ormolu for local pre-commit runs
instead.
In this PR, I have updated the README file to reflect the new goals of
the project and highlight related products to Juvix. The ORG files have
been replaced with Markdown for better readability and maintainability.
Additionally, I have added a couple of files to fine-tune the mdbook
settings. These changes, I believe, will make it easier for users to
understand and contribute to the project.🤞
- Closes#1878
- New pre-commit hook to format md, yaml, js, CSS files.
To check the website generation, I have deployed the result here:
Work in progress.
- https://jonaprieto.github.io/juvix
- https://github.com/jonaprieto/juvix
---------
Co-authored-by: Paul Cadman <pcadman@gmail.com>
Co-authored-by: Christopher Goes <cwgoes@pluranimity.org>
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Depends on PR #1832
* Closes#1799
* Removes Backend.C.Translation.FromInternal
* Removes `foreign` and `compile` blocks
* Removes unused test files
* Removes the old C runtime
* Removes other dead code
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`.
* 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>
* 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.
* remove ≔ from the language and replace it by :=
* revert accidental changes in juvix input mode
* update stdlib submodule
* rename ℕ by Nat in the tests and examples
* fix shell tests
Now that integer literals have the builtin int type we need an actual
IOUnit value to use in the IO sequence implementation.
This commit also adds the TicTacToe web example to the test suite. It is
a typecheck / C generation only test because it uses the Wasm browser APIs.
* Add a Web version of TicTacToe
The web version demonstrates injecting host functions into the WASM
import table and call exported Juvix functions from JS.
The web version and the CLI version of the TicTacToe game use the same
game logic backend Juvix module.
* Build and publish web apps in documentation
* Add a link to the TicTacToe web app in example documentation
* Update Makefile to match the new format
* Update SimpleFungibleToken to use stdlib
We do not want to put an Int type into the standard library before we
have builtin support for arbitrary precision integers. So we include the
Int type locally in the project for now.
* Update reference to stdlib
* Fix shell-tests for SimpleFungibleToken
* Renaming MiniJuvix to Juvix
* Make Ormolu happy
* Make Hlint happy
* Remove redundant imports
* Fix shell tests and add target ci to our Makefile
* Make pre-commit happy
* Add support for parital application eval/apply
* include string.h in libc runtime
* Add wasm SimpleFungibleTokenImplicit to tests
* Update VP example to new syntax
* propagate types from all reachable modules
* Change prelude import ordering to workaround minic issue
* Pre-declare inductive typedefs in C backend
This generates the typedefs corresponding to each inductive type.
e.g
```
inductive Bool { .. }
```
is translated to:
```
typedef struct Bool_3_s Bool_3_t;
```
This means that C code can reference these typedefs before they have
been fully defined. (all references to inductive types go through these typedefs
names).
This fixes an issue with the ordering of delcarations when modules are included.
* Use common Lib for MiniC tests
* libc runtime: flush stdout after writing to it
* Adds MiniTicTacToe example using common example lib
In MonoJuvixToMiniC we emit the inductive type typedefs before anything
else to support includes ordering
* Adds tests for mutually recrusive functions
* Add golden tests for milestone examples
* Example: Remove commented out code
* Test error handling behaviour in MiniTicTacToe
* Fail clang compilation on warnings
* Add test for Nested list types
* Add PrettyCode instances for NonEmpty and ConcreteType
* Ignore IsImplicit field in Eq and Hashable of TypeApplication
This is to workaround a crash in Micro->Mono translation when looking up
a concrete type
* Fix formatting
* hlint fixes
* Formatting fixes not reported by local pre-commit
* Refactor MonoJuvixToMiniC
* Fix shelltest
NB: We cannot check the order of the 'Writing' lines because this
depends on the order of files returned by the FS which is
non-deterministic between systems
* Refactor Base to CBuilder
* Refactor using applyOnFunStatement
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Update VP example to new syntax
* Ignore html folders and include assets for html rendering
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
