* 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>
This PR removes the CaseBranchImplicit error from the scoper. This error
is already handled in the arity/typechecker with a good error message:
The arity checker error message for
```
case b of {
| {{true}} := false
```
is
```
Expected an explicit pattern but found an implicit instance pattern: {{true}}
```
* Closes https://github.com/anoma/juvix/issues/2356
This pr simplifies parsing by removing `FunctionParameterUnnamed`. It
also removes ghost wildcards introduced during parsing.
It also introduces an error for double braced atoms `{{x}}` that are not
on the left of an arrow `->`
* Closes#1646
Implements a basic trait framework. A simple instance search mechanism
is included which fails if there is more than one matching instance at
any step.
Example usage:
```
import Stdlib.Prelude open hiding {Show; mkShow; show};
trait
type Show A :=
mkShow {
show : A → String
};
instance
showStringI : Show String := mkShow (show := id);
instance
showBoolI : Show Bool := mkShow (show := λ{x := if x "true" "false"});
instance
showNatI : Show Nat := mkShow (show := natToString);
showList {A} : {{Show A}} → List A → String
| nil := "nil"
| (h :: t) := Show.show h ++str " :: " ++str showList t;
instance
showListI {A} {{Show A}} : Show (List A) := mkShow (show := showList);
showMaybe {A} {{Show A}} : Maybe A → String
| (just x) := "just (" ++str Show.show x ++str ")"
| nothing := "nothing";
instance
showMaybeI {A} {{Show A}} : Show (Maybe A) := mkShow (show := showMaybe);
main : IO :=
printStringLn (Show.show true) >>
printStringLn (Show.show false) >>
printStringLn (Show.show 3) >>
printStringLn (Show.show [true; false]) >>
printStringLn (Show.show [1; 2; 3]) >>
printStringLn (Show.show [1; 2]) >>
printStringLn (Show.show [true; false]) >>
printStringLn (Show.show [just true; nothing; just false]) >>
printStringLn (Show.show [just [1]; nothing; just [2; 3]]) >>
printStringLn (Show.show "abba") >>
printStringLn (Show.show ["a"; "b"; "c"; "d"]);
```
It is possible to manually provide an instance and to match on implicit
instances:
```
f {A} : {{Show A}} -> A -> String
| {{mkShow s}} x -> s x;
f' {A} : {{Show A}} → A → String
| {{M}} x := Show.show {{M}} x;
```
The trait parameters in instance types are checked to be structurally
decreasing to avoid looping in the instance search. So the following is
rejected:
```
type Box A := box A;
trait
type T A := mkT { pp : A → A };
instance
boxT {A} : {{T (Box A)}} → T (Box A) := mkT (λ{x := x});
```
We check whether each parameter is a strict subterm of some trait
parameter in the target. This ordering is included in the finite
multiset extension of the subterm ordering, hence terminating.
- Closes#2331.
The rules implemented in this pr are as follows.
1. If a type definition has only one constructor, no pipe is added. The
constructor is printed in the same line if it fits.
2. If a constructor is a record with a single field, the field is
printed in the same line if it fits. If the constructor has multiple
fields, they are printed aligned and indented after a line break.
Examples:
```
type T := constructT : T;
type T-wrapper := mkWrapper {unwrap : T};
type EnumRecord :=
| --- doc for C1
C1 {
c1a : T;
c1b : T
}
| C2 {
c2a : T;
c2b : T
};
```
