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

38 Commits

Author SHA1 Message Date
Jan Mas Rovira
138d9e545d
Logger (#2908)
1. Adds the `--log-level LOG_LEVEL` flag to the CLI. This flag can be
given `error`, `warn`, `info`, `progress`, `debug` as argument to filter
the logged messages.
2. Removes the `--only-errors` flag.
3. Adds the `--ide-end-error-char CHAR`, which receives a character as
an argument, which is appended to the end of error messages. This is
handy to facilitate parsing of errors messages from the ide. This
functionality was previously embeded in the old `--only-errors` flag.
2024-07-22 17:14:37 +02:00
Jan Mas Rovira
6fcc9f21d2
Improve performance of formatting a project (#2863)
Currently formatting a project is equivalent to running `juvix format`
on each individual file. Hence, the performance is quadratic wrt the
number of modules in the project. This pr fixes that and we now we only
process each module once.

# Benchmark (1236% faster 🚀)
Checking the standard library
```
hyperfine --warmup 1 'juvix format --check' 'juvix-main format --check'
Benchmark 1: juvix format --check
  Time (mean ± σ):     450.6 ms ±  33.7 ms    [User: 707.2 ms, System: 178.7 ms]
  Range (min … max):   396.0 ms … 497.0 ms    10 runs

Benchmark 2: juvix-main format --check
  Time (mean ± σ):      6.019 s ±  0.267 s    [User: 9.333 s, System: 1.512 s]
  Range (min … max):    5.598 s …  6.524 s    10 runs

Summary
  juvix format --check ran
   13.36 ± 1.16 times faster than juvix-main format --check
```

# Other changes:
1. The `EntryPoint` field `entryPointModulePath` is now optional.
2. I've introduced a new type `TopModulePathKey` which is analogous to
`TopModulePath` but wihout location information. It is used in hashmap
keys where the location in the key is never used. This is useful as we
can now get a `TopModulePathKey` from a `Path Rel File`.
3. I've refactored the `_formatInput` field in `FormatOptions` so that
it doesn't need to be a special case anymore.
4. I've introduced a new effect `Forcing` that allows to individually
force fields of a record type with a convenient syntax.
5. I've refactored some of the constraints in scoping so that they only
require `Reader Package` instead of `Reader EntryPoint`.
6. I've introduced a new type family so that local modules are no longer
required to have `ModuleId` from their type. Before, they were assigned
one, but it was never used.


# Future work:
1. For project-wise formatting, the compilation is done in parallel, but
the formatting is still done sequentially. That should be improved.
2024-07-01 18:05:24 +02:00
Jan Mas Rovira
e9afdad82a
Parallel pipeline (#2779)
This pr introduces parallelism in the pipeline to gain performance. I've
included benchmarks at the end.

- Closes #2750.

# Flags:
There are two new global flags:
1. `-N / --threads`. It is used to set the number of capabilities.
According to [GHC
documentation](https://hackage.haskell.org/package/base-4.20.0.0/docs/GHC-Conc.html#v:setNumCapabilities):
_Set the number of Haskell threads that can run truly simultaneously (on
separate physical processors) at any given time_. When compiling in
parallel, we create this many worker threads. The default value is `-N
auto`, which sets `-N` to half the number of logical cores, capped at 8.
2. `--dev-show-thread-ids`. When given, the thread id is printed in the
compilation progress log. E.g.

![image](https://github.com/anoma/juvix/assets/5511599/9359fae2-0be1-43e5-8d74-faa82cba4034)

# Parallel compilation
1. I've added `src/Parallel/ParallelTemplate.hs` which contains all the
concurrency related code. I think it is good to keep this code separated
from the actual compiler code.
2. I've added a progress log (only for the parallel driver) that outputs
a log of the compilation progress, similar to what stack/cabal do.

# Code changes:
1. I've removed the `setup` stage where we were registering
dependencies. Instead, the dependencies are registered when the
`pathResolver` is run for the first time. This way it is safer.
1. Now the `ImportTree` is needed to run the pipeline. Cycles are
detected during the construction of this tree, so I've removed `Reader
ImportParents` from the pipeline.
3. For the package pathresolver, we do not support parallelism yet (we
could add support for it in the future, but the gains will be small).
4. When `-N1`, the pipeline remains unchanged, so performance should be
the same as in the main branch (except there is a small performance
degradation due to adding the `-threaded` flag).
5. I've introduced `PipelineOptions`, which are options that are used to
pass options to the effects in the pipeline.
6. `PathResolver` constraint has been removed from the `upTo*` functions
in the pipeline due to being redundant.
7. I've added a lot of `NFData` instances. They are needed to force the
full evaluation of `Stored.ModuleInfo` in each of the threads.
2. The `Cache` effect uses
[`SharedState`](https://hackage.haskell.org/package/effectful-core-2.3.0.1/docs/Effectful-State-Static-Shared.html)
as opposed to
[`LocalState`](https://hackage.haskell.org/package/effectful-core-2.3.0.1/docs/Effectful-Writer-Static-Local.html).
Perhaps we should provide different versions.
3. I've added a `Cache` handler that accepts a setup function. The setup
is triggered when a miss is detected. It is used to lazily compile the
modules in parallel.

# Tests
1. I've adapted the smoke test suite to ignore the progress log in the
stderr.
5. I've had to adapt `tests/positive/Internal/Lambda.juvix`. Due to
laziness, a crash happening in this file was not being caught. The
problem is that in this file we have a lambda function with different
number of patterns in their clauses, which we currently do not support
(https://github.com/anoma/juvix/issues/1706).
6. I've had to comment out the definition
   ```
   x : Box ((A : Type) → A → A) := box λ {A a := a};
   ```
From the test as it was causing a crash
(https://github.com/anoma/juvix/issues/2247).
# Future Work
1. It should be investigated how much performance we lose by fully
evaluating the `Stored.ModuleInfo`, since some information in it will be
discarded. It may be possible to be more fine-grained when forcing
evaluation.
8. The scanning of imports to build the import tree is sequential. Now,
we build the import tree from the entry point module and only the
modules that are imported from it are in the tree. However, we have
discussed that at some point we should make a distinction between
`juvix` _the compiler_ and `juvix` _the build tool_. When using `juvix`
as a build tool it makes sense to typecheck/compile (to stored core) all
modules in the project. When/if we do this, scanning imports in all
modules in parallel becomes trivial.
9. The implementation of the `ParallelTemplate` uses low level
primitives such as
[forkIO](https://hackage.haskell.org/package/base-4.20.0.0/docs/Control-Concurrent.html#v:forkIO).
At some point it should be refactored to use safer functions from the
[`Effectful.Concurrent.Async`](https://hackage.haskell.org/package/effectful-2.3.0.0/docs/Effectful-Concurrent-Async.html)
module.
10. The number of cores and worker threads that we spawn is determined
by the command line. Ideally, we could use to import tree to compute an
upper bound to the ideal number of cores to use.
11. We could add an animation that displays which modules are being
compiled in parallel and which have finished being compiled.

# Benchmarks

On some benchmarks, I include the GHC runtime option
[`-A`](https://downloads.haskell.org/ghc/latest/docs/users_guide/runtime_control.html#rts-flag--A%20%E2%9F%A8size%E2%9F%A9),
which sometimes makes a good impact on performance. Thanks to
@paulcadman for pointing this out. I've figured a good combination of
`-N` and `-A` through trial and error (but this oviously depends on the
cpu and juvix projects).

## Typecheck the standard library
   
### Clean run (88% faster than main):
```
 hyperfine --warmup 1 --prepare 'juvix clean' 'juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432'  'juvix -N 4 typecheck Stdlib/Prelude.juvix' 'juvix-main typecheck Stdlib/Prelude.juvix'
Benchmark 1: juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432
  Time (mean ± σ):     444.1 ms ±   6.5 ms    [User: 1018.0 ms, System: 77.7 ms]
  Range (min … max):   432.6 ms … 455.9 ms    10 runs

Benchmark 2: juvix -N 4 typecheck Stdlib/Prelude.juvix
  Time (mean ± σ):     628.3 ms ±  23.9 ms    [User: 1227.6 ms, System: 69.5 ms]
  Range (min … max):   584.7 ms … 670.6 ms    10 runs

Benchmark 3: juvix-main typecheck Stdlib/Prelude.juvix
  Time (mean ± σ):     835.9 ms ±  12.3 ms    [User: 788.5 ms, System: 31.9 ms]
  Range (min … max):   816.0 ms … 853.6 ms    10 runs

Summary
  juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432 ran
    1.41 ± 0.06 times faster than juvix -N 4 typecheck Stdlib/Prelude.juvix
    1.88 ± 0.04 times faster than juvix-main typecheck Stdlib/Prelude.juvix
```
   
### Cached run (43% faster than main):
```
hyperfine --warmup 1 'juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432'  'juvix -N 4 typecheck Stdlib/Prelude.juvix' 'juvix-main typecheck Stdlib/Prelude.juvix'
Benchmark 1: juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432
  Time (mean ± σ):     241.3 ms ±   7.3 ms    [User: 538.6 ms, System: 101.3 ms]
  Range (min … max):   231.5 ms … 251.3 ms    11 runs

Benchmark 2: juvix -N 4 typecheck Stdlib/Prelude.juvix
  Time (mean ± σ):     235.1 ms ±  12.0 ms    [User: 405.3 ms, System: 87.7 ms]
  Range (min … max):   216.1 ms … 253.1 ms    12 runs

Benchmark 3: juvix-main typecheck Stdlib/Prelude.juvix
  Time (mean ± σ):     336.7 ms ±  13.3 ms    [User: 269.5 ms, System: 67.1 ms]
  Range (min … max):   316.9 ms … 351.8 ms    10 runs

Summary
  juvix -N 4 typecheck Stdlib/Prelude.juvix ran
    1.03 ± 0.06 times faster than juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432
    1.43 ± 0.09 times faster than juvix-main typecheck Stdlib/Prelude.juvix
```
## Typecheck the test suite of the containers library
At the moment this is the biggest juvix project that we have.

### Clean run (105% faster than main)
```
hyperfine --warmup 1 --prepare 'juvix clean' 'juvix -N 6 typecheck Main.juvix +RTS -A67108864' 'juvix -N 4 typecheck Main.juvix' 'juvix-main typecheck Main.juvix'
Benchmark 1: juvix -N 6 typecheck Main.juvix +RTS -A67108864
  Time (mean ± σ):      1.006 s ±  0.011 s    [User: 2.171 s, System: 0.162 s]
  Range (min … max):    0.991 s …  1.023 s    10 runs

Benchmark 2: juvix -N 4 typecheck Main.juvix
  Time (mean ± σ):      1.584 s ±  0.046 s    [User: 2.934 s, System: 0.149 s]
  Range (min … max):    1.535 s …  1.660 s    10 runs

Benchmark 3: juvix-main typecheck Main.juvix
  Time (mean ± σ):      2.066 s ±  0.010 s    [User: 1.939 s, System: 0.089 s]
  Range (min … max):    2.048 s …  2.077 s    10 runs

Summary
  juvix -N 6 typecheck Main.juvix +RTS -A67108864 ran
    1.57 ± 0.05 times faster than juvix -N 4 typecheck Main.juvix
    2.05 ± 0.03 times faster than juvix-main typecheck Main.juvix
```

### Cached run (54% faster than main)
```
hyperfine --warmup 1 'juvix -N 6 typecheck Main.juvix +RTS -A33554432'  'juvix -N 4 typecheck Main.juvix' 'juvix-main typecheck Main.juvix'
Benchmark 1: juvix -N 6 typecheck Main.juvix +RTS -A33554432
  Time (mean ± σ):     551.8 ms ±  13.2 ms    [User: 1419.8 ms, System: 199.4 ms]
  Range (min … max):   535.2 ms … 570.6 ms    10 runs

Benchmark 2: juvix -N 4 typecheck Main.juvix
  Time (mean ± σ):     636.7 ms ±  17.3 ms    [User: 1006.3 ms, System: 196.3 ms]
  Range (min … max):   601.6 ms … 655.3 ms    10 runs

Benchmark 3: juvix-main typecheck Main.juvix
  Time (mean ± σ):     847.2 ms ±  58.9 ms    [User: 710.1 ms, System: 126.5 ms]
  Range (min … max):   731.1 ms … 890.0 ms    10 runs

Summary
  juvix -N 6 typecheck Main.juvix +RTS -A33554432 ran
    1.15 ± 0.04 times faster than juvix -N 4 typecheck Main.juvix
    1.54 ± 0.11 times faster than juvix-main typecheck Main.juvix
```
2024-05-31 12:41:30 +01:00
Jan Mas Rovira
2d36a65324
Make compile targets a subcommand instead of a flag (#2700)
# Changes
The main goal of this pr is to remove the `--target` flag for `juvix
compile` and use subcommands instead. The targets that are relevant to
normal users are found in `juvix compile --help`. Targets that are
relevant only to developers are found in `juvix dev compile --help`.

Below I list some of the changes in more detail.
## Compile targets for user-facing languages
- `juvix compile native`
- `juvix compile wasi`. I wasn't sure how to call this: `wasm`,
`wasm32-wasi`, etc. In the end I thought `wasi` was short and accurate,
but we can change it.
- `juvix compile vampir`
- `juvix compile anoma`
- `juvix compile cairo`
## *New* compile targets for internal languages
See `juvix dev compile --help`.

1. `dev compile core` has the same behaviour as `dev core
from-concrete`. The `dev core from-concrete` is redundant at the moment.
2. `dev compile tree` compiles to Tree and prints the InfoTable to the
output file wihout any additional checks.
3. `dev compile reg` compiles to Reg and prints the InfoTable to the
output file wihout any additional checks.
4. `dev compile asm` compiles to Asm and prints the InfoTable to the
output file wihout any additional checks.
5. 4. `dev compile casm` compiles to Asm and prints the Result to the
output file wihout any additional checks. TODO: should the Result be
printed or something else? At the moment the Result lacks a pretty
instance.
6. 
## Optional input file
1. The input file for commands that expect a .juvix file as input is now
optional. If the argument is ommited, he main file given in the
package.yaml will be used. This applies to the following commands:
   1. `juvix compile [native|wasi|geb|vampir|anoma|cairo]`
   8.  `juvix dev compile [core|reg|tree|casm|asm]`
   1. `juvix html`
   3. `juvix markdown`.
   4. `juvix dev internal [typecheck|pretty]`.
   5. `juvix dev [parse|scope]`
   7. `juvix compile [native|wasi|geb|vampir|anoma|cairo]`
   9. note that `juvix format` has not changed its behaviour.

## Refactor some C-like compiler flags
Both `juvix compile native` and `juvix compile wasi` support `--only-c`
(`-C`), `--only-preprocess` (`-E`), `--only-assemble` (`-S`). I propose
to deviate from the `gcc` style and instead use a flag with a single
argument:
- `--cstage [source|preprocess|assembly|exec(default)]`. I'm open to
suggestions. For now, I've kept the legacy flags but marked them as
deprecated in the help message.

## Remove code duplication
I've tried to reduce code duplication. This is sometimes in tension with
code readability so I've tried to find a good balance. I've tried to
make it so we don't have to jump to many different files to understand
what a single command is doing. I'm sure there is still room for
improvement.

## Other refactors
I've implemented other small refactors that I considered improved the
quality of the code.

## TODO/Future work
We should refactor commands (under `compile dev`) which still use
`module Commands.Extra.Compile` and remove it.
2024-04-09 13:29:07 +02:00
Łukasz Czajka
dcea0bbecb
Add field element type (#2659)
* 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>
2024-02-27 14:54:43 +01:00
Jan Mas Rovira
97030f8cb4
Use EmbedIO instead of Embed IO (#2645)
- ⚠️ 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.
2024-02-13 18:00:01 +00:00
Łukasz Czajka
75bce8f665
Per-module compilation (#2468)
* 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
2023-12-30 20:15:35 +01:00
Jan Mas Rovira
69594edc7b
Read Package on demand and cache it (#2548)
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.
2023-12-06 18:24:59 +01:00
Jan Mas Rovira
c8e7ce8afd
Remove old typechecker (#2545) 2023-12-01 16:50:37 +01:00
Jan Mas Rovira
a05586e44f
Interleave arity and typechecking (#2481)
- 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>
2023-11-12 16:23:33 +01:00
Paul Cadman
68d4314c78
Migrate all Juvix projects from juvix.yaml to Package.juvix in the repository (#2503)
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
2023-11-07 18:11:02 +00:00
Paul Cadman
cbee146bd7
Rename Roots type to Root (#2480)
This was suggested by @jonaprieto in
https://github.com/anoma/juvix/pull/2458#discussion_r1368476371 - but we
deferred it until the Package file PR sequence was merged.
2023-10-30 14:05:52 +01:00
Paul Cadman
382a4d3cef
Global offline flag (#2335)
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
2023-09-05 17:11:17 +02:00
Jan Mas Rovira
d69d8c6eca
Remove abstract (#2219)
- Closes #2002 
- Closes #1690 
- Closes #2224
- Closes #2237
2023-06-30 15:01:46 +02:00
Jan Mas Rovira
6fb7bbff2d
Move termination checker to Internal (#2209)
- Closes #2203
2023-06-20 11:02:37 +02:00
Veronika Romashkina
b4e7dbc7fd
Remove --no-format option (#2121)
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
2023-05-24 10:46:18 +02:00
Łukasz Czajka
8aa54ecc28
Inlining (#2036)
* 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.
2023-05-15 17:27:05 +02:00
Veronika Romashkina
8ab4ccd73b
Make format command's filepath optional (#2028)
# 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>
2023-04-27 17:33:08 +02:00
janmasrovira
3d012cc8fb
Support more paths (#2000)
- 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>
2023-04-19 15:56:48 +01:00
janmasrovira
5de0026d83
Add juvix global project under xdg directory and other improvements (#1963)
Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-04-13 11:27:39 +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
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
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
af63c36574
Support basic dependencies (#1622) 2022-12-20 13:05:40 +01: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
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
Łukasz Czajka
708a4032c6
Add an option to show name ids in errors (#1486) 2022-09-01 13:22:32 +02:00
janmasrovira
bcaf319b90
Add --stdin flag (#1459) 2022-08-19 16:57:07 +02:00
Jonathan Cubides
423ccec70a
Add positivity check for inductive types (#1393)
* 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>
2022-07-23 09:27:12 +02:00
Jonathan Cubides
3b3ea45da9
Rename MiniJuvix to Juvix (#259)
* 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
2022-07-08 13:59:45 +02:00
Paul Cadman
ed78f2636b
Embed standard library in the minijuvix binary (#210)
* 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
2022-06-30 11:31:08 +02:00
Jonathan Cubides
3b0cde27bb
Add CLI improvements and shell testing (#131)
* 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
2022-06-09 16:36:07 +02:00
Jonathan Cubides
29c526833d
Revision for package.yaml and minor deletions (#135) 2022-06-01 11:53:06 +02:00
Jonathan Cubides
f16570e546
Add the termination checker to the pipeline (#111)
* [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>
2022-05-30 13:40:52 +02:00
janmasrovira
50ea7373ee
Improve error generation and handling (#108)
* 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
2022-05-18 17:10:10 +02:00