This PR adds the `PackageDescription.Basic` module, available to
Package.juvix files.
```
module Package;
import PackageDescription.Basic open;
package : Package := basicPackage;
```
The `PackageDescription.Basic` module provides a Package type that is
translated to a Juvix Package with all default arguments. It is not
possible to customize a basic package.
A basic package does not depend on the standard library, so loads much
more quickly.
Additionally this PR:
* Adds `juvix init --basic/-b` option to generate a basic Package.juvix.
* Migrates Package.juvix files that only use default arguments, or only
customise the name field, to basic Package files.
* Closes https://github.com/anoma/juvix/issues/2508
- 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 adds an initial support for Literate Juvix Markdown files, files
with the extension `.juvix.md`.
Here is a small example of such a file: `Test.juvix.md`.
<pre>
# This is a heading
Lorem ...
```juvix
module Test;
type A := a;
fun : A -> A
| _ := a;
```
Other text
</pre>
This initial support enables users to execute common commands such as
typechecking, compilation, and HTML generation. Additionally, a new
command called `markdown` has been introduced. This command replaces
code blocks marked with the juvix attribute with their respective HTML
output, much like the output we obtain when running `juvix html`. In
this version, comments are ignored in the output, including judoc
blocks.
- We intend to use this new feature in combination with this Python
plugin (https://github.com/anoma/juvix-mkdocs) to enhance our
documentation site.
https://github.com/anoma/juvix/assets/1428088/a0c17f36-3d76-42cc-a571-91f885866874
## Future work
Open as issues once this PR is merged, we can work on the following:
- Support imports of Juvix Markdown modules (update the path resolver to
support imports of Literate Markdown files)
- Support (Judoc) comments in md Juvix blocks
- Support Markdown in Judoc blocks
- Update Text editor support, vscode extension and emacs mode (the
highlighting info is a few characters off in the current state)
- Closes#1839
- Closes#1719
* Closes#2365
* Implements the syntax `f@{x1 := def1; ...; xn := defn}` and `f@?{x1 :=
def1; ..; xn := defn}`. Each definition inside the `@{..}` is an
ordinary function definition. The `@?` version allows partial
application (not all explicit named arguments need to be provided). This
subsumes the old record creation syntax.
* Closes#2453
* Closes#2432
* Any nonnegative literal `n` is replaced with `fromNat {_} {{_}} n`
where `fromNat` is the builtin conversion function defined in the
`Natural` trait in `Stdlib.Trait.Natural`.
* Any negative literal `-n` is replaced with `fromInt {_} {{_}} -n`
where `fromInt` is the builtin conversion function defined in the
`Integral` trait in `Stdlib.Trait.Integral`.
* Before resolving instance holes, it is checked whether the type holes
introduced for `fromNat` and `fromInt` have been inferred. If not, an
attempt is made to unify them with `Nat` or `Int`. This allows to
type-check e.g. `1 == 1` (there is no hint in the context as to what the
type of `1` should be, so it is decided to be `Nat` after inferring the
hole fails).
Depends on:
* ~~https://github.com/anoma/juvix/pull/2459~~
* https://github.com/anoma/juvix/pull/2462
This PR is part of a series implementing:
* https://github.com/anoma/juvix/issues/2336
This PR adds the package file loading function, including a file
evaluation effect. It integrates this with the existing `readPackage`
function and adds tests / smoke tests.
## Package.juvix format
Instead of `juvix.yaml` (which is still supported currently) users can
now place a `Package.juvix` file in the root of their project. The
simplest `Package.juvix` file you can write is:
```
module Package;
import PackageDescription open;
package : Package := defaultPackage;
```
The
[PackageDescription](35b2f618f0/include/package/PackageDescription.juvix)
module defines the `Package` type. Users can use "go-to definition" in
their IDE from the Package file to see the documentation and
definitions.
Users may also import `Stdlib.Prelude` in their Package file. This is
loaded from the global project. No other module imports are supported.
Notes:
* If a directory contains both `Package.juvix` and `juvix.yaml` then
`Package.juvix` is used in preference.
## Default stdlib dependency
The `Dependency` type has a constructor called `defaultStdlib`. This
means that any project can use the compiler builtin standard library
dependency. With `juvix.yaml` this dependency is only available when the
`dependencies` field is unspecified.
```
module Package;
import PackageDescription open;
package : Package := defaultPackage { dependencies := [defaultStdlib] };
```
## Validation
As well as the standard type checking validation that the Juvix compiler
provides additional validation is made on the file.
* The Package module must contain the identifier `package` and it must
have type `Package` that's obtained from the global `PackageDescription`
module.
* Every dependency specified in the Package.juvix must be unique.
* Closes https://github.com/anoma/juvix/issues/2336
## Examples
### Package with name and version
```
module Package;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0};
```
### Package with GitHub dependency
```
module Package;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0;
dependencies := [defaultStdlib;
github (org := "anoma";
repo := "juvix-containers";
ref := "v0.7.1")]};
```
## Package with main and buildDir fields
```
module Package;
import Stdlib.Prelude open;
import PackageDescription open;
package : Package :=
defaultPackage {name := "a-package";
version := mkVersion 0 1 0;
dependencies := [defaultStdlib;
github (org := "anoma";
repo := "juvix-containers";
ref := "v0.7.1")];
buildDir := just "/tmp/build";
main := just "HelloWorld.juvix"
};
```
Simplifies arithmetic expressions in the Core optimization phase,
changing e.g. `(x - 1) + 1` to `x`. Such expressions appear as a result
of compiling pattern matching on natural numbers.
The special PathResolver puts files from the global package stdlib and
files from the global package description files in scope of the
$root/Package.juvix module.
Currently this means that PackageDescription module is in scope for the
module so that the user can write:
```
module Package;
import Stdlib.Prelude open;
import PackageDescription open;
package : Package :=
mkPackageDefault
(name := "foo")
{ version := mkVersion 0 1 0
; dependencies :=
[ github "anoma" "juvix-stdlib" "adf58a7180b361a022fb53c22ad9e5274ebf6f66"
; github "anoma" "juvix-containers" "v0.7.1"]};
```
* Closes#2154
* Evaluates closed applications with value arguments when the result
type is zero-order. For example, `3 + 4` is evaluated to `7`, and `id 3`
is evaluated to `3`, but `id id` is not evaluated because the target
type is not zero-order (it's a function type).
* Closes#2426
A coercion from trait `T` to `T'` can be declared with the syntax
```
coercion instance
coeName {A} {{T A}} : T' A := ...
```
Coercions can be seen as instances with special resolution rules.
Coercion resolution rules
-------------------------
* If a non-coercion instance can be applied in a single instance
resolution step, no coercions are considered. No ambiguity results if
there exists some coercion which could be applied, but a non-coercion
instance exists - the non-coercion instances have priority.
* If no non-coercion instance can be applied in a single resolution
step, all minimal coercion paths which lead to an applicable
non-coercion instance are considered. If there is more than one,
ambiguity is reported.
Examples
----------
The following type-checks because:
1. There is no non-coercion instance found for `U String`.
2. There are two minimal coercion paths `U` <- `U1` and `U` <- `U2`, but
only one of them (`U` <- `U2`) ends in an applicable non-coercion
instance (`instU2` for `U2 String`).
```
trait
type U A := mkU {pp : A -> A};
trait
type U1 A := mkU1 {pp : A -> A};
trait
type U2 A := mkU2 {pp : A -> A};
coercion instance
fromU1toU {A} {{U1 A}} : U A :=
mkU@{
pp := U1.pp
};
coercion instance
fromU2toU {A} {{U2 A}} : U A :=
mkU@{
pp := U2.pp
};
instance
instU2 : U2 String := mkU2 id;
main : IO := printStringLn (U.pp "X")
```
The following results in an ambiguity error because:
1. There is no non-coercion instance found for `T Unit`.
2. There are two minimal coercion paths `T` <- `T1` and `T` <- `T2`,
both of which end in applicable non-coercion instances.
```
trait
type T A := mkT { pp : A → A };
trait
type T1 A := mkT1 { pp : A → A };
trait
type T2 A := mkT2 { pp : A → A };
instance
unitT1 : T1 Unit := mkT1 (pp := λ{_ := unit});
instance
unitT2 : T2 Unit := mkT2 (pp := λ{_ := unit});
coercion instance
fromT1toT {A} {{T1 A}} : T A := mkT@{
pp := T1.pp
};
coercion instance
fromT2toT {A} {{T2 A}} : T A := mkT@{
pp := T2.pp
};
main : Unit := T.pp unit;
```
The following type-checks, because there exists a non-coercion instance
for `T2 String`, so the coercion `fromT1toT2` is ignored during instance
resolution.
```
trait
type T1 A := mkT1 {pp : A -> A};
trait
type T2 A := mkT2 {pp : A -> A};
instance
instT1 {A} : T1 A :=
mkT1@{
pp := id
};
coercion instance
fromT1toT2 {A} {{M : T1 A}} : T2 A :=
mkT2@{
pp := T1.pp {{M}}
};
instance
instT2 : T2 String :=
mkT2@{
pp (s : String) : String := s ++str "!"
};
main : String := T2.pp "a";
```
* 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.
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>
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
* 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.
- 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
};
```
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
This PR adds external git dependency support to the Juvix package
format.
## New dependency Git item
You can now add a `git` block to the dependencies list:
```yaml
name: HelloWorld
main: HelloWorld.juvix
dependencies:
- .juvix-build/stdlib
- git:
url: https://my.git.repo
name: myGitRepo
ref: main
version: 0.1.0
```
Git block required fields:
* `url`: The URL of the git repository
* `ref`: The git reference that should be checked out
* `name`: The name for the dependency. This is used to name the
directory of the clone, it is required. Perhaps we could come up with a
way to automatically name the clone directory. Current ideas are to
somehow encode the URL / ref combination or use a UUID. However there's
some value in having the clone directory named in a friendly way.
NB:
* The values of the `name` fields must be unique among the git blocks in
the dependencies list.
## Behaviour
When dependencies for a package are registered, at the beginning of the
compiler pipeline, all remote dependencies are processed:
1. If it doesn't already exist, the remote dependency is cloned to
`.juvix-build/deps/$name`
2. `git fetch` is run in the clone
3. `git checkout` at the specified `ref` is run in the clone
The clone is then processed by the PathResolver in the same way as path
dependencies.
NB:
* Remote dependencies of transitive dependencies are also processed.
* The `git fetch` step is required for the case where the remote is
updated. In this case we want the user to be able to update the `ref`
field.
## Errors
1. Missing fields in the Git dependency block are YAML parse errors
2. Duplicate `name` values in the dependencies list is an error thrown
when the package file is processed
3. The `ref` doesn't exist in the clone or the clone directory is
otherwise corrupt. An error with a suggestion to `juvix clean` is given.
The package file path is used as the location in the error message.
4. Other `git` command errors (command not found, etc.), a more verbose
error is given with the arguments that were passed to the git command.
## Future work
1. Add an offline mode
2. Add a lock file mechanism that resolves branch/tag git refs to commit
hashes
* closes https://github.com/anoma/juvix/issues/2083
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- Closes#2293.
- Closes#2319
I've added an effect for termination. It keeps track of which functions
failed the termination checker, which is run just after translating to
Internal. During typechecking, non-terminating functions are not
normalized. After typechecking, if there is at least one function which
failed the termination checker, an error is reported.
Additionally, we now properly check for termination of functions defined
in a let expression in the repl.
- Closes#2188.
This pr introduces a new syntactical statement for defining aliases:
```
syntax alias newName := oldName;
```
where `oldName` can be any name in the expression namespace. Fixity and
module aliases are not supported at the moment.
- The `newName` does not inherit the fixity of `oldName`. We have agreed
that the goal is to inherit the fixity of `oldName` except if `newName`
has a fixity statement, but this will be done in a separate pr as it
requires #2310.
