* Adapts to https://github.com/anoma/juvix-stdlib/pull/86
* Adds a pass in `toEvalTransformations` to automatically inline all
record projection functions, regardless of the optimization level. This
is necessary to ensure that arithmetic operations and comparisons on
`Nat` or `Int` are always represented directly with the corresponding
built-in Core functions. This is generally highly desirable and required
for the Geb target.
* Adds the `inline: always` pragma which indicates that a function
should always be inlined during the mandatory inlining phase, regardless
of optimization level.
- Closes#2402.
Changes:
1. Allow the definition of empty record types.
2. Introduce the _constructor wildcard_ pattern. That is, a pattern of
the form `constr@{}` that matches the constructor `constr` regardless of
its number of arguments.
Changes in the printing of Lambda terms necessary for the use of the Juvix
Geb backend, changing the names of binary operations, adding a
constructor for natural numbers. Appropriately changes tests when
necessary.
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
* Closes#2416
* Closes#2401
* Avoids generating identical specialisations by keeping a
specialisation signature for each specialised function application.
* Allows to specialise on a per-trait or per-instance basis:
```
{-# specialize: true #-}
trait
type Natural N := mkNatural {
+ : N -> N -> N;
* : N -> N -> N;
fromNat : Nat -> N;
};
```
or
```
{-# specialize: true #-}
instance
naturalNatI : Natural Nat := ...
```
* The above `specialize: bool` pragma actually works with any type or
function. To be able to simultaneously specify the boolean
specialisation flag and specialisation arguments, one can use
`specialize-args: [arg1, .., argn]` which works like `specialize: [arg1,
.., argn]`.
This PR adds a new command `juvix dependencies update` that fetches all
dependencies in a project and updates the project lock file.
Currently the only way to update the lock file is to delete it and
generate a new one.
## CLI Docs
```
juvix dependencies --help
Usage: juvix dependencies COMMAND
Subcommands related to dependencies
Available options:
-h,--help Show this help text
Available commands:
update Fetch package dependencies and update the lock file
```
## Example
A project containing the following `juvix.yaml`
```yaml
dependencies:
- .juvix-build/stdlib/
- git:
url: https://github.com/anoma/juvix-test
ref: v0.6.0
name: test
main: Example.juvix
name: example
version: 1.0.0
```
compile to generate the lockfile: `juvix compile`
```yaml
# This file was autogenerated by Juvix version 0.5.1.
# Do not edit this file manually.
dependencies:
- path: .juvix-build/stdlib/
dependencies: []
- git:
name: test
ref: a94c61749678ff57556ee6e4cb1f8fbbddbc4ab1
url: https://github.com/anoma/juvix-test
dependencies:
- git:
name: stdlib
ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45
url: https://github.com/anoma/juvix-stdlib
dependencies: []
```
Now update the test dependency version:
```yaml
- .juvix-build/stdlib/
- git:
url: https://github.com/anoma/juvix-test
ref: v0.6.1
name: test
main: Example.juvix
name: example
version: 1.0.0
```
And run `juvix dependencies update`
Now the lockfile has updated to the hash of v0.6.1:
```yaml
# This file was autogenerated by Juvix version 0.5.1.
# Do not edit this file manually.
dependencies:
- path: .juvix-build/stdlib/
dependencies: []
- git:
name: test
ref: a7ac74cac0db92e0b5e349f279d797c3788cdfdd
url: https://github.com/anoma/juvix-test
dependencies:
- git:
name: stdlib
ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45
url: https://github.com/anoma/juvix-stdlib
dependencies: []
```
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
.hlint.yaml was removed in:
* https://github.com/anoma/juvix/pull/2398
however it's useful to keep it because it is used by Haskell tooling
(emacs haskell-mode and vscode haskell extension).
This PR adds lock file support to the compiler pipeline. The lock file
is generated whenever a compiler pipeline command (`juvix {compile,
typecheck, repl}`) is run.
The lock file contains all the information necessary to reproduce the
whole dependency source tree. In particular for git dependencies,
branch/tag references are resolved to git hash references.
## Lock file format
The lock file is a YAML `juvix.lock.yaml` file written by the compiler
alongside the package's `juvix.yaml` file.
```
LOCKFILE_SPEC: { dependencies: { DEPENDENCY_SPEC, dependencies: LOCKFILE_SPEC }
DEPENDENCY_SPEC: PATH_SPEC | GIT_SPEC
PATH_SPEC: { path: String }
GIT_SPEC: { git: {url: String, ref: String, name: String } }
```
## Example
Consider a project containing the following `juvix.yaml`:
```yaml
dependencies:
- .juvix-build/stdlib/
- git:
url: https://github.com/anoma/juvix-containers
ref: v0.7.1
name: containers
name: example
version: 1.0.0
```
After running `juvix compile` the following lockfile `juvix.lock.yaml`
is generated.
```yaml
# This file was autogenerated by Juvix version 0.5.1.
# Do not edit this file manually.
dependencies:
- path: .juvix-build/stdlib/
dependencies: []
- git:
name: containers
ref: 3debbc7f5776924eb9652731b3c1982a2ee0ff24
url: https://github.com/anoma/juvix-containers
dependencies:
- git:
name: stdlib
ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45
url: https://github.com/anoma/juvix-stdlib
dependencies: []
- git:
name: test
ref: a7ac74cac0db92e0b5e349f279d797c3788cdfdd
url: https://github.com/anoma/juvix-test
dependencies:
- git:
name: stdlib
ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45
url: https://github.com/anoma/juvix-stdlib
dependencies: []
```
For subsequent runs of the juvix compile pipeline, the lock file
dependency information is used.
## Behaviour when package file and lock file are out of sync
If a dependency is specified in `juvix.yaml` that is not present in the
lock file, an error is raised.
Continuing the example above, say we add an additional dependency:
```
dependencies:
- .juvix-build/stdlib/
- git:
url: https://github.com/anoma/juvix-containers
ref: v0.7.1
name: containers
- git:
url: https://github.com/anoma/juvix-test
ref: v0.6.1
name: test
name: example
version: 1.0.0
```
`juvix compile` will throw an error:
```
/Users/paul/tmp/lockfile/dep/juvix.yaml:1:1: error:
The dependency test is declared in the package's juvix.yaml but is not declared in the lockfile: /Users/paul/tmp/lockfile/dep/juvix.lock.json
Try removing /Users/paul/tmp/lockfile/dep/juvix.lock.yaml and then run Juvix again.
```
Closes:
* https://github.com/anoma/juvix/issues/2334
Adds a Partial trait to the standard library, similar to the one in
PureScript:
https://book.purescript.org/chapter6.html#nullary-type-classes
This enables using partial functions in an encapsulated manner and
without depending on the Debug module.
Adds a trait:
```
trait
type Partial := mkPartial {
fail : {A : Type} -> String -> A
};
runPartial {A} (f : {{Partial}} -> A) : A := f {{mkPartial Debug.failwith}};
```
* Small style improvements
* Update `mapfun.juvix` to use `Int` instead of `Nat` so that it is
semantically equivalent to the other implementations.
* Adapt to #2396
* Closes#2280
* Record creation syntax uses normal function definition syntax like at
the top-level or in lets.
* It is now allowed to omit the result type annotation in function
definitions (the `: ResultType` part) with `_` inserted by default. This
is allowed only for simple definitions of the form `x := value` in lets
and record creation, but not at the top level.
- Closes#2373
Consider this:
```
let
x : _ := 0
in ...
```
When translating the let to internal, we build the dependency graph and
then use that to group definitions in mutually recursive blocks. Since
`x` has no edge, it was not being added to the dependency graph, so it
was not being translated to Internal, thus crashing later during
inference.
The _packageFile field of the Package record is used internally to track
the package file path and is used in error messages. It is not intended
to be present in the juvix.yaml file.
To express this the PackageFileType family with the Raw index is set to
`()`. However `()` is serialized to an empty array by Aeson, so the
`file: []` field was added to juvix.yaml.
NB: From aeson 2.2, fields with type `()` are ommitted when the
`omitNothingFields` flag is set to True, as it is for the package ToJSON
instance.
The solution in this PR is to set `PackageFileType 'Raw` to `Maybe ()`.
The
`omitNothingFields` flag then omits this field from the serialized
package object.
* Closes https://github.com/anoma/juvix/issues/2380
During path resolution, `git fetch` is called on every git dependency
clone. It's desirable to reduce the number of `git fetch` calls because
it makes a network call.
This PR changes the git dependency resolution to only call `git fetch`
if the existing clone does not already contain the specified ref.
With `-Os` ill-typed code is generated for the following:
```
module wasmcrash.juvix;
import Stdlib.Prelude open;
{-# inline: false #-}
I {A} (x : A) : A := x;
{-# inline: false #-}
I' {A} (x : A) : A := x;
main : Nat := I' (I I 1);
```
Running the generated WASM file with `wasmer` or `wasmtime` gives an
error:
```
Validation error: type mismatch: expected i32 but nothing on stack (at offset 740)
```
The issue occurs with clang version 16.0.5 but not 16.0.0. The issue
does not occur with any other optimization option (`-O1`, `-O2`, `-O3`).
There is no issue with `-Os` used with the native target.
This is thus likely a bug in a specific version of LLVM. It could be
theoretically some very subtle non-conformance to the C standard in our
generated code, but this seems less likely. Creating a minimum C file
exposing the bug would be very time-consuming, so I propose to just
avoid using the `-Os` option for now.
- Closes#2330
- Closes#2329
This pr implements the syntax changes described in #2330. It drops
support for the old yaml-based syntax.
Some valid examples:
```
syntax iterator for {init := 1; range := 1};
syntax fixity cons := binary {assoc := right};
syntax fixity cmp := binary;
syntax fixity cmp := binary {}; -- debatable whether we want to accept empty {} or not. I think we should
```
# Future work
This pr creates an asymmetry between iterators and operators
definitions. Iterators definition do not require a constructor. We could
add it to make it homogeneous, but it looks a bit redundant:
```
syntax iterator for := mkIterator {init := 1; range := 1};
```
We could consider merging iterator and fixity declarations with this
alternative syntax.
```
syntax XXX for := iterator {init := 1; range := 1};
syntax XXX cons := binary {assoc := right};
```
where `XXX` is a common keyword. Suggestion by @lukaszcz XXX = declare
---------
Co-authored-by: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
