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

351 Commits

Author SHA1 Message Date
Dimitris Apostolou
d6d21a22e3
Fix typos (#2573) 2024-01-08 13:27:18 +01: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
Łukasz Czajka
758d1cd949
Implement the dynamic dispatch loop in JuvixAsm (#2556)
* Closes #2555 
* Depends on #2554
2023-12-15 19:08:40 +01:00
Jan Mas Rovira
4fa17359a6
Implement wildcard constructor (#2550)
- Closes #2549 

The implementation of wildcard constructors was previously done in the
arity checker. I did not realise I was missing it because there was not
tests for it that included typechecking (we were only checking
formatting).
2023-12-07 10:12:36 +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
Paul Cadman
77b29c6963
Update to the latest juvix-stdlib (#2546)
This PR updates the juvix-stdlib submodule ref to the current
juvix-stdlib/main.

NB: The Markdown test is not stable after changes to the stdlib - the
ids (deriving from internal name ids?) will change and so the expected
file must be regenerated.
2023-12-01 15:12:54 +01:00
Jan Mas Rovira
c237f292a7
Add dependent defaults for the new typechecker (#2541)
This pr adds support for default values that depend on previous
arguments. For instance, see
[test071](ca7d0fa06d/tests/Compilation/positive/test071.juvix).
- After #2540 is implemented, we'll be able to remove the old type
checker (including the aritychecker).
2023-11-30 19:17:00 +01:00
Paul Cadman
20a95ec42d
Extract builtin definitions for loading a Package into bundled package-base package (#2535)
This PR creates a new package that's bundled with the compiler in a
similar way to the stdlib and the package description package.

## The `package-base` Package

This package is called
[package-base](ab4376cf9e/include/package-base)
and contains the minimal set of definitions required to load a Package
file.

The
[`Juvix.Builtin`](ab4376cf9e/include/package-base/Juvix/Builtin/V1.juvix)
module contains:

```
module Juvix.Builtin.V1;

import Juvix.Builtin.V1.Nat open public;
import Juvix.Builtin.V1.Trait.Natural open public;
import Juvix.Builtin.V1.String open public;
import Juvix.Builtin.V1.Bool open public;
import Juvix.Builtin.V1.Maybe open public;
import Juvix.Builtin.V1.List open public;
import Juvix.Builtin.V1.Fixity open public;
```

`Juvix.Builtin.V1.Bool` is required to support backend primitive
integers `Juvix.Builtin.V1.Trait.Natural` is required to support numeric
literals.

## The `PackageDescription.V2` module

This PR also adds a new
[`PackageDescription.V2`](ab4376cf9e/include/package/PackageDescription/V2.juvix)
type that uses the `package-base`. This is to avoid breaking existing
Package files. The Packages files in the repo (except those that test
`PackageDescription.V1`) have also been updated.

## Updating the stdlib

The standard library will be updated to use `Juvix.Builtin.*` modules in
a subsequent PR.

* Part of https://github.com/anoma/juvix/issues/2511
2023-11-30 16:22:18 +00:00
Jonathan Cubides
7de9f2f0f3
Add new case for positivity checker: type cannot occur as arg of bound var (#2542)
This PR fixes our positivity checker to support inductive definitions
with type families as type parameters. This kind of ind. type is
type-checked using the global flag `--new-type checker.`

For example, the following definition is not allowed:

```
module Evil;

type Evil (f : Type -> Type) :=
  magic : f (Evil f) -> Evil f;
```

- Closes #2540
2023-11-30 15:03:54 +01:00
Jan Mas Rovira
ca7d0fa06d
Negative tests for --new-typechecker (#2532)
Adds all existing negative tests for the new typechecker.
- Depends on #2524
2023-11-28 17:24:03 +00:00
Jan Mas Rovira
d6c1a74cec
Improve inference for --new-typechecker (#2524)
This pr applies a number of fixes to the new typechecker.
The fixes implemented are:
1. When guessing the arity of the body, we properly use the type
information of the variables in the patterns.
2. When generating wildcards, we name them properly so that they align
with the name in the type signature.
3. When compiling named applications, we inline all clauses of the form
`fun : _ := body`. This is a workaround to
https://github.com/anoma/juvix/issues/2247 and
https://github.com/anoma/juvix/issues/2517
4. I've had to ignore test027 (Church numerals). While the typechecker
passes and one can see that the types are correct, there is a lambda
where its clauses have different number of patterns. Our goal is to
support that in the near future
(https://github.com/anoma/juvix/issues/1706). This is the conflicting
lambda:
    ```
    mutual num : Nat → Num
      := λ : Nat → Num {| (zero : Nat) := czero
      | ((suc n : Nat)) {A} := csuc (num n) {A}}
    ```
5. I've added non-trivial a compilation test involving monad
transformers.
2023-11-28 16:43:14 +01:00
Jan Mas Rovira
f610518449
Add non-dependent default values to the new typechecking algorithm (#2516)
This pr adds default values (that don't depend on previous default
values) under the new `--new-typechecker` flag.
2023-11-23 11:42:58 +01:00
Paul Cadman
1c1a5b7117
Update the Juvix lock file when the Package file changes (#2522)
Adds a new version of the lock file that stores the hash (sha256 digest)
of the package file (Package.juvix, juvix.yaml) it was generated from as
a field:

```
# This file was autogenerated by Juvix version 0.5.4.
# Do not edit this file manually.

version: 2
checksum: d05940a4d3dc0e15451d02e1294819c875ba486ee54e26865ba8d190ac7c27c3
dependencies:
- git:
    name: stdlib
    ref: f68b0614ad695eaa13ead42f3466e0a78219f826
    url: https://github.com/anoma/juvix-stdlib.git
  dependencies: []
```

The lock file is regenerated when the hash of the package file doesn't
match the value of the `checksum` field, i.e when the user updates the
package file.

Existing lock files are automatically migrated to version 2.

* Closes https://github.com/anoma/juvix/issues/2464
2023-11-22 23:21:29 +01:00
Jonathan Cubides
dd43f07905
Fix #2510 (#2512)
- Close #2510 
- Close #2518 
- Progress for #2520
2023-11-17 16:10:38 +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
Jonathan Cubides
8616370fb2
Add MarkdownInfo entry in Module Concrete Decl and proper errors (#2515)
Remove TODO added by @janmasrovira in 
- https://github.com/anoma/juvix/pull/2513
2023-11-16 11:20:34 +01:00
Jan Mas Rovira
90200ab6de
General inductive parameters (#2506)
- Depends on #2481 

This pr allows inductive type parameters to be any type. Until now, they
had to be exactly `Type`. This allows us to define more general traits
such as the `Monad` and `Functor`, as shown in the new test.
This is only supported under the temporary `--new-typechecker` flag.

Pending work:

Update the positivity checker if necessary (@jonaprieto).
Update the necessary compilation steps in Core (@lukaszcz).
Add compilation tests.
2023-11-15 10:24:54 +01:00
Paul Cadman
7b5211664e
Add PackageDescription.Basic module Package variant (#2509)
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
2023-11-13 17:36:18 +00: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
Jonathan Cubides
bd16d3ef2a
Add support for Literate Juvix Markdown (#2448)
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
2023-11-10 13:55:36 +01:00
Łukasz Czajka
5948a38a54
Named arguments syntax with function definitions (#2494)
* 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.
2023-11-07 12:02:22 +01:00
Jonathan Cubides
47c8df11f1
Fix remove unexpected whitespaces introduced by formatting (#2489)
- Closes #2059
2023-11-03 12:51:45 +01:00
Łukasz Czajka
485f6e7920
Literal casting (#2457)
* 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).
2023-11-03 10:01:03 +01: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
0a8799a344
Use a Juvix source file to define a package (#2434)
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"
                };

```
2023-10-27 12:35:20 +01:00
Jan Mas Rovira
0943a4ab92
Dependent default values (#2446)
- Closes #2445
2023-10-27 10:19:07 +02:00
Łukasz Czajka
ef1148beaa
Fix precedence inconsistency bug (#2470)
Precedence inconsistency was not always correctly detected.
2023-10-25 16:13:27 +02:00
Paul Cadman
27aaf9d9f9
Add dependency on expressions in function default arguments (#2462)
Closes:
* https://github.com/anoma/juvix/issues/2461
2023-10-24 11:02:24 +02:00
Paul Cadman
8e6c1c8f07
Use JuvixError instead of Text for errors in Package file loading (#2459)
Depends on:
*  https://github.com/anoma/juvix/pull/2458

This PR is part of a series implementing:
* https://github.com/anoma/juvix/issues/2336

In attempt to make the main PR:
* https://github.com/anoma/juvix/pull/2434
easier to review.

This PR introduces standard JuvixError handling for errors related to
the loading of the juvix.yaml file. Before this PR errors were thrown as
Text and then communicated to the user using the `error` function.
2023-10-23 19:01:36 +01:00
Paul Cadman
37de293c3d
Refactor EntryPoint, Package, Pipeline, Root packages (#2458)
Depends on:
*  https://github.com/anoma/juvix/pull/2451

This PR is part of a series implementing:
* https://github.com/anoma/juvix/issues/2336

In attempt to make the main PR:
* https://github.com/anoma/juvix/pull/2434
easier to review.

Changes in this PR refactor EntryPoint, Package, Pipeline, Root,
splitting out the types into Base modules so that they can be imported
and used in subsequent PRs with fewer dependencies to avoid package
cycles.
2023-10-23 12:38:52 +01:00
Łukasz Czajka
cdfb35aaac
Arithmetic simplification (#2454)
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.
2023-10-23 11:47:17 +02:00
Paul Cadman
c1c2a06922
Process $root/Package.juvix using a special PathResolver (#2451)
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"]};
```
2023-10-23 10:08:44 +02:00
Łukasz Czajka
272b93e595
Constant folding (#2450)
* 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).
2023-10-20 12:03:56 +02:00
Łukasz Czajka
cbd8253afd
Instance coercions (#2444)
* 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";
```
2023-10-19 16:00:31 +02:00
Jan Mas Rovira
a5516a5a08
Add default arguments (#2408) 2023-10-10 23:28:06 +02:00
Łukasz Czajka
407a74004c
Fix instance axiom bug (#2439)
* Closes #2438
2023-10-10 15:55:17 +02:00
Łukasz Czajka
60a191b786
Numeric, ordering and equality traits (#2433)
* 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.
2023-10-09 18:25:01 +02:00
Jan Mas Rovira
28c404348a
Ignore instance arguments in the termination checker (#2435)
- Fixes #2414
2023-10-06 12:09:15 +02:00
Paul Cadman
76d69b5ef3
Add juvix dependencies update command (#2419)
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>
2023-10-03 18:09:13 +02:00
Jan Mas Rovira
9d9631aa26
Allow open statements in let expressions (#2395)
- Closes #2185
2023-10-02 23:13:45 +02:00
Jan Mas Rovira
76b58f090f
Fix for crash with wildcard used in type definition (#2405)
- Closes #2292.

Holes are now allowed in the type of inductive parameters.
If the type is unsupported, a user error is thrown.
2023-10-02 18:58:21 +02:00
Paul Cadman
dad3963c00
Add package lockfile support (#2388)
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
2023-10-02 17:51:14 +02:00
Łukasz Czajka
1260853583
Improve closure calls in the runtime (#2396)
* Closes #1653 

The running time improvement is 20-30% on benchmarks dominated by
closure calls.
2023-09-29 14:20:00 +02:00
Łukasz Czajka
e4a5ca7399
Record creation syntax with function definitions (#2369)
* 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.
2023-09-28 17:07:38 +02:00
Jan Mas Rovira
27df3949f5
Add nodes with no edges to the dependency graph (#2390)
- 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.
2023-09-26 13:17:50 +02:00
Łukasz Czajka
e4558975b1
Improve inlining (#2377)
Small improvement of the inlining optimization - types are not counted
toward inlining depth limit
2023-09-21 19:12:39 +01:00
Łukasz Czajka
fe90da58ed
Error for an instance subsumed by other instances (#2375)
* Closes #2372
2023-09-21 11:12:49 +01:00
Łukasz Czajka
c5d8641142
Error on local instances (#2376)
* Closes #2374

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-09-21 10:34:28 +01:00
Jan Mas Rovira
8daca2ba0a
New fixity/iterator syntax (#2332)
- 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>
2023-09-14 10:57:38 +02:00