* Closes#2571
* It is reasonable to finish this PR before tackling #2562, because the
field element type is the primary data type in Cairo.
* Depends on #2653
Checklist
---------
- [x] Add field type and operations to intermediate representations
(JuvixCore, JuvixTree, JuvixAsm, JuvixReg).
- [x] Add CLI option to choose field size.
- [x] Add frontend field builtins.
- [x] Automatic conversion of integer literals to field elements.
- [x] Juvix standard library support for fields.
- [x] Check if field size matches when loading a stored module.
- [x] Update the Cairo Assembly (CASM) interpreter to use the field type
instead of integer type.
- [x] Add field type to VampIR backend.
- [x] Tests
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- ⚠️ Depends on #2644
The `effectful` library does not support the `Embed` effect out of the
box. However, it offers `IOE`, which is equivalent to `Embed IO` from
polysemy. In preparation to a possible migration to `effectful`, this pr
hides the general `Embed` effect from the prelude and it exports a
specialized `EmbedIO` in its place.
* Closes#2392
Changes checklist
-----------------
* [X] Abstract out data types for stored module representation
(`ModuleInfo` in `Juvix.Compiler.Store.Language`)
* [X] Adapt the parser to operate per-module
* [X] Adapt the scoper to operate per-module
* [X] Adapt the arity checker to operate per-module
* [X] Adapt the type checker to operate per-module
* [x] Adapt Core transformations to operate per-module
* [X] Adapt the pipeline functions in `Juvix.Compiler.Pipeline`
* [X] Add `Juvix.Compiler.Pipeline.Driver` which drives the per-module
compilation process
* [x] Implement module saving / loading in `Pipeline.Driver`
* [x] Detect cyclic module dependencies in `Pipeline.Driver`
* [x] Cache visited modules in memory in `Pipeline.Driver` to avoid
excessive disk operations and repeated hash re-computations
* [x] Recompile a module if one of its dependencies needs recompilation
and contains functions that are always inlined.
* [x] Fix identifier dependencies for mutual block creation in
`Internal.fromConcrete`
- Fixed by making textually later definitions depend on earlier ones.
- Now instances are used for resolution only after the textual point of
their definition.
- Similarly, type synonyms will be unfolded only after the textual point
of their definition.
* [x] Fix CLI
* [x] Fix REPL
* [x] Fix highlighting
* [x] Fix HTML generation
* [x] Adapt test suite
This patch dramatically increases the efficiency of `juvix dev root`,
which was unnecessarily parsing all dependencies included in the
`Package.juvix` file. Other commands that do not require the `Package`
will also be faster.
It also refactors some functions so that the `TaggedLock` effect is run
globally.
I've added `singletons-base` as a dependency so we can have `++` on the
type level. We've tried to define a type family ourselves but inference
was not working properly.
- Closes#2362
This pr implements a new typechecking algorithm. This algorithm can be
activated using the global flag `--new-typechecker`. This flag will only
take effect on the compilation pipeline but not the repl.
The main difference between the new and old algorithm is that the new
one inserts holes during typechecking. Thus, it does not require the
arity checker pass.
The new algorithm does not yet implement default arguments. The plan is
to make the change in the following steps:
1. Merge this pr.
2. Merge #2506.
3. Implement default arguments for the new algorithm.
4. Remove the arity checker and the old algorithm.
---------
Co-authored-by: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com>
This PR:
* Modifies entry point `_entryPointBuildDir` to use the `BuildDir` type
instead of `SomeBase Dir`. This allows delayed resolution of the default
build directory which was useful for the Package -> Concrete translation
point below.
* Modifies `juvix dev root` to render the current package as a
Package.juvix file.
* Modifies the Package -> Concrete translation to recognise default
arguments. So, for example, an empty `juvix.yaml` file will be
translated into the following (instead of the `name`, `version`, and
`dependencies` arguments being populated).
module Package;
import Stdlib.Prelude open;
import PackageDescription.V1 open;
package : Package := defaultPackage;
* Adds a temporary command (removed when juvix.yaml support is removed)
`juvix dev migrate-juvix-yaml` that translates `juvix.yaml` into an
equivalent `Package.juvix` in the current project.
* Adds a temporary script `migrate-juvix-yaml.sh` (removed when
juvix.yaml support is removed) which can be run in the project to
translate all Juvix projects in the repository.
* Actually translate all of the `juvix.yaml` files to `Package.juvix`
using the script.
* Part of https://github.com/anoma/juvix/issues/2487
This PR introduces a global `--offline` flag.
## Doctor
This replaces the `--offline` flag on the doctor command.
## Juvix package builds
The flag applies to juvix build commands like `juvix compile`, `juvix
repl`. This is so that users can continue to build packages offline that
have external dependencies when there's no network connection (as long
as they built the same package online previously).
Specifically, when the `--offline` flag is used in a package that has
external git dependencies.
* No `git clone` or `git fetch` commands are used
* `git checkout` will continue to be used
* Clones from previous builds are reused
This means that you can update the `ref` field in a git dependency, as
long as the ref existed the last time that the project was built without
the `--offline` flag.
* Closes https://github.com/anoma/juvix/issues/2333
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
* 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.
# 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>
- 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>
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
* 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
* w.i.p
* Added strict positivity condition for datatypes w.i.p
* Add negative test for str.postivity check
* Add some revisions
* the branch is back to feet
* w.i.p add lots of traces to check alg.
* Add more test and revisions
* Add negative and positive test to the new flag and the keyword
* Fix shell tests.
* Make pre-commit happy
* Fix rebase conflicts
* Make pre-commit happy
* Add shell test, rename keyword, fix error msg
* Revert change
* Necessary changes
* Remove wrong unless
* Move the positivity checker to its own folder
* Add missing juvix.yaml
* Add a negative test thanks to jan
* make some style changes
* Make ormolu happy
* Remove unnecessary instance of Show
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* 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
* Embed stdlib in minijuvix library
We add a new step at the beginning of the pipeline called Setup that
registers the modules in the standard library with the Files effect. The
standard library is then used when the Scoper queries the Files effect
for modules as it resolves import statements.
Use of the standard library can be disabled using the global
`--no-stdlib` command-line option.
* CI: Checkout submodules recursively for stdlib
* Add a new `--no-stdlib` option to shell check
* Poke CI
* CI: Checkout submodules in the test job
* Remove input file fields from command opts
* [cli] Make version and help commands
* Fix on reviews
* Fixes for dealing with global options inside subcmds
* Fix minijuvix emacs mode and add some instance to GlobalOpts
* Remove unrelated code
* Propagate globals opts in each cmd parser
* Add initial shell tests
* Add test-shell to makefile and CI
* Fix CI: adding .local/bin to PATH
* Fixing CI
* Installing shelltest just before running it
* Install app for shell testing
* Hide global flags after cmd. Fix shell tests accordingly.
* Fixing CI
* Shell test only run on ubuntu for now
* [WIP] EntryPoint now has options. --no-termination is a new global opt.
* Add TerminationChecking to the pipeline
* Add TerminationChecking to the pipeline
* Keep GlobalOptions in App
* Fix reviewer's comments
* delete unnecessary parens
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* add face and handling of not in scope symbol error
* small fix
* generic errors wip
* add App effect
* format
* add flycheck-minijuvix
* use absolute paths and refactor
* fix dir0
* add generic error instances and improve some errors
* format
* qualify strings
* use AnsiText
* add ToGenericError instances for the type checker errors
* improve error message
* improve handling of parsing errors
