1
1
mirror of https://github.com/anoma/juvix.git synced 2024-11-09 22:11:27 +03:00
Commit Graph

19 Commits

Author SHA1 Message Date
Jan Mas Rovira
e0ae356cd7
Use prettyString instead of show . pretty (#2711)
Use `prettyString` instead of relying on `Show` instance for `Doc a` so
that it is more consistent with `prettyText`.
2024-04-12 10:26:54 +02:00
Paul Cadman
be24abb0ca
Support compilation to Anoma compatible functions (#2652)
This PR adds a `anoma` target to the `juvix compile`. This target
compiles a Juvix `main` function to a Nockma/Anoma "function". Unlike
the native, wasm, and nockma targets the main function may have any type
signature.

## Anoma calling convention

[Anoma calls
functions](6a4e15fe9c/lib/anoma/resource.ex (L122))
by evaluating the formula `[call L replace [RL args] @ S]` against a
subject equal to the function. Here `args` is a Nockma term that
evaluates to a tuple of arguments that should be passed to the function.

The anoma target compiles the `main` function to Nockma in the same way
as the nockma target. The main function is then
[wrapped](9a658465ae/src/Juvix/Compiler/Nockma/Translation/FromTree.hs (L627))
to make it compatible with the Anoma calling convention.

## Testing

The anoma calling convention is [unit
tested](9a658465ae/test/Nockma/Eval/Positive.hs (L117))
and [smoke
tested](9a658465ae/tests/smoke/Commands/compile.smoke.yaml (L159)).

This PR also adds versions of the end-to-end compilation tests. Most
tests are included, tests for builtin IO operations and string builtins
are omitted. Other tests that use Strings have been adapted to use other
types that are compatible with this backend.

## Nockma REPL

To facilitate testing the Nockma REPL can now load a nockma file as an
initial subject.

---------

Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
2024-02-23 12:54:22 +00:00
Jan Mas Rovira
a825f41507
Refactor readFile and some parsers to use Path instead of FilePath (#2649)
Now the prelude exports this function:
```
readFile :: (MonadIO m) => Path Abs File -> m Text
readFile = liftIO . Utf8.readFile . toFilePath
```
It is more convenient to use because it uses typed `Path` and works in
any `MonadIO`.
2024-02-19 17:33:58 +01:00
Jan Mas Rovira
84b0e5605f
Use writeFileEnsureLn in place of writeFile (#2604)
Now we guarantee that whenever we write a file there is a newline
character at the end, which is a [Unix
convention](https://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap03.html#tag_03_205).

The juvix prelude now exports `writeFileEnsureLn` and it no longer
exports `writeFile`. If at some point we need the behaviour of
`writeFile` I'd suggest that we export it renamed as `writeFileVerbatim`
or something similar.
2024-01-31 11:15:17 +01:00
Paul Cadman
517897930f
Nockma compile refactor (#2582)
This PR contains refactors split out from the Nockma compile PR
https://github.com/anoma/juvix/pull/2570. Each refactor is associated
with a separate commit in this PR.
2024-01-16 16:22:10 +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
Paul Cadman
2f4a3f809b
Run test suite in parallel (#2507)
## Overview

This PR makes the compiler pipeline thread-safe so that the test suite
can be run in parallel.

This is achieved by:
* Removing use of `{get, set, with}CurrentDir` functions.
* Adding locking around shared file resources like the the
global-project and internal build directory.

NB: **Locking is disabled for the main compiler target**, as it is
single threaded they are not required.

## Run test suite in parallel

To run the test suite in parallel you must add `--ta '+RTS -N -RTS'` to
your stack test arguments. For example:

```
stack test --fast --ta '+RTS -N -RTS'
```

The `-N` instructs the Haskell runtime to choose the number of threads
to use based on how many processors there are on your machine. You can
use `-Nn` to see the number of threads to `n`.

These flags are already [set in the
Makefile](e6dca22cfd/Makefile (L26))
when you or CI uses `stack test`.

## Locking

The Haskell package
[filelock](https://hackage.haskell.org/package/filelock) is used for
locking. File locks are used instead of MVars because Juvix code does
not control when new threads are created, they are created by the test
suite. This means that MVars created by Juvix code will have no effect,
because they are created independently on each test-suite thread.
Additionally the resources we're locking live on the filesystem and so
can be conveniently tagged by path.

### FileLock

The filelock library is wrapped in a FileLock effect:


e6dca22cfd/src/Juvix/Data/Effect/FileLock/Base.hs (L6-L8)

There is an [IO
interpreter](e6dca22cfd/src/Juvix/Data/Effect/FileLock/IO.hs (L8))
that uses filelock and an [no-op
interpreter](e6dca22cfd/src/Juvix/Data/Effect/FileLock/Permissive.hs (L7))
that just runs actions unconditionally.

### TaggedLock

To make the file locks simpler to use a TaggedLock effect is introduced:


e6dca22cfd/src/Juvix/Data/Effect/TaggedLock/Base.hs (L5-L11)

And convenience function:


e6dca22cfd/src/Juvix/Data/Effect/TaggedLock.hs (L28)

This allows an action to be locked, tagged by a directory that may or
may not exist. For example in the following code, an action is performed
on a directory `root` that may delete the directory before repopulating
the files. So the lockfile cannot be stored in the `root` itself.


e6dca22cfd/src/Juvix/Extra/Files.hs (L55-L60)

## Pipeline

As noted above, we only use locking in the test suite. The main app
target pipeline is single threaded and so locking is unnecessary. So the
interpretation of locks is parameterised so that locking can be disabled
e6dca22cfd/src/Juvix/Compiler/Pipeline/Run.hs (L64)
2023-11-16 16:19:52 +01:00
Łukasz Czajka
1710615fb0
VampIR range checks and error handling (#2344)
* Adds range checks and proper error handling to the Juvix-to-VampIR
pipeline.
* Adds the `--unsafe` option which disables the checks.
2023-09-12 19:56:28 +02:00
Łukasz Czajka
5f35178575
Switch to Halo2 for VampIR backend tests (#2216)
* Closes #2214
2023-06-21 13:08:19 +02:00
Łukasz Czajka
c47320bb13
Use equality instead of less-equal when translating matching on Nats (#2215)
* Closes #2211
2023-06-20 15:39:53 +01:00
Łukasz Czajka
afbee7f14d
Fix isNegative in the VampIR runtime (#2212)
* Closes #2206
2023-06-20 15:34:50 +02:00
Łukasz Czajka
dd16274a24
Restrict permutative conversions on cases to non-booleans (#2201)
* Restricts permutative conversions for case-expressions to
non-booleans. This reduces the blow-up a bit.

  Permutative conversions rewrite
  ```
  case (case M | C1 -> A1 | C2 -> A2)
  | D1 -> B1
  | D2 -> B2
  ```
  to
  ```
  case M
  | C1 -> case A1
              | D1 -> B1
              | D2 -> B2
  | C2 -> case A2
              | D1 -> B1
              | D2 -> B2
  ```

It is necessary to perform them for non-boolean A1/A2 to obtain the
right kind of normal forms.

* Adds a test demonstrating the necessity of permutative conversions for
non-booleans.
2023-06-19 11:57:12 +02:00
Łukasz Czajka
f421e87963
Update to the new version of VampIR (#2138)
* Closes #2131 

It remains to update the VampIR version in the CI.
2023-06-16 16:34:58 +01:00
Łukasz Czajka
a3a2454733
More tests for the VampIR compilation pipeline (#2197) 2023-06-16 12:58:37 +02:00
Łukasz Czajka
31627a0ce5
Check valid argument names in YAML (#2193)
* Closes #2191
2023-06-15 16:42:58 +02:00
Łukasz Czajka
757b4ed180
VampIR pipeline: handle booleans in the type of main (#2137)
* Closes #2132

---------

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-06-01 11:42:35 +02:00
Łukasz Czajka
d576111241
VampIR integration (#2103)
* Closes #2035 
* Depends on #2086 
* Depends on #2096 
* Adds end-to-end tests for the Juvix-to-VampIR compilation pipeline.

---------

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-05-22 20:18:18 +02:00
Łukasz Czajka
fe78ff451c
Direct translation from normalized JuvixCore to VampIR (#2086)
* Closes #2034.
* Adds the `vampir` target to the `compile` command.
* Adds two tests which are not yet enabled because `vamp-ir` is not
available in the CI (these and more tests will be enabled in #2103).
2023-05-19 14:43:45 +02:00