- merge #2260 first
Allows constructors to be defined using Haskell-like Adt syntax.
E.g.
```
module Adt;
type Bool :=
| true
| false;
type Pair (A B : Type) :=
| mkPair A B;
type Nat :=
| zero
| suc Nat;
```
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
- Closes#2258
# Overview
When we define a type with a single constructor and one ore more fields,
a local module is generated with the same name as the inductive type.
This module contains a projection for every field. Projections can be
used as any other function.
E.g. If we have
```
type Pair (A B : Type) := mkPair {
fst : A;
snd : B;
};
```
Then we generate
```
module Pair;
fst {A B : Type} : Pair A B -> A
| (mkPair a b) := a;
snd : {A B : Type} : Pair A B -> B
| (mkPair a b) := b;
end;
```
- Closes#1641
This pr adds the option to declare constructors with fields. E.g.
```
type Pair (A B : Type) :=
| mkPair {
fst : A;
snd : B
};
```
Which is desugared to
```
type Pair (A B : Type) :=
| mkPair : (fst : A) -> (snd : B) -> Pair A B;
```
making it possible to write ` mkPair (fst := 1; snd := 2)`.
Mutli-constructor types are also allowed to have fields.
- closes#1991
This pr implements named arguments as described in #1991. It does not
yet implement optional arguments, which should be added in a later pr as
they are not required for record syntax.
# Syntax Overview
Named arguments are a convenient mehcanism to provide arguments, where
we give the arguments by name instead of by position. Anything with a
type signature can have named arguments, i.e. functions, types,
constructors and axioms.
For instance, if we have (note that named arguments can also appear on
the rhs of the `:`):
```
fun : {A B : Type} (f : A -> B) : (x : A) -> B := ... ;
```
With the traditional positional application, we would write
```
fun suc zero
```
With named arguments we can write the following:
1. `fun (f := suc) (x := zero)`.
2. We can change the order: `fun (x := zero) (f := suc)`.
3. We can group the arguments: `fun (x := zero; f := suc)`.
4. We can partially apply functions with named arguments: `fun (f :=
suc) zero`.
5. We can provide implicit arguments analogously (with braces): `fun {A
:= Nat; B := Nat} (f := suc; x := zero)`.
6. We can skip implicit arguments: `fun {B := Nat} (f := suc; x :=
zero)`.
What we cannot do:
1. Skip explicit arguments. E.g. `fun (x := zero)`.
2. Mix explicit and implicit arguments in the same group. E.g. `fun (A
:= Nat; f := suc)`
3. Provide explicit and implicit arguments in different order. E.g. `fun
(f := suc; x := zero) {A := Nat}`.
GEB 0.3.2 introduces the following changes.
* The STLC frontend no longer requires full type information in terms.
The syntax of the terms changed.
* An error node has been introduced which allows to compile Juvix `fail`
nodes.
The following features required for compilation from Juvix are still
missing in GEB.
* Modular arithmetic types ([GEB issue
#61](https://github.com/anoma/geb/issues/61)).
* Functor/algebra iteration to implement bounded inductive types ([GEB
issue #62](https://github.com/anoma/geb/issues/62)).
- Closes#2060
- Closes#2189
- This pr adds support for the syntax described in #2189. It does not
drop support for the old syntax.
It is possible to automatically translate juvix files to the new syntax
by using the formatter with the `--new-function-syntax` flag. E.g.
```
juvix format --in-place --new-function-syntax
```
# Syntax changes
Type signatures follow this pattern:
```
f (a1 : Expr) .. (an : Expr) : Expr
```
where each `ai` is a non-empty list of symbols. Braces are used instead
of parentheses when the argument is implicit.
Then, we have these variants:
1. Simple body. After the signature we have `:= Expr;`.
2. Clauses. The function signature is followed by a non-empty sequence
of clauses. Each clause has the form:
```
| atomPat .. atomPat := Expr
```
# Mutual recursion
Now identifiers **do not need to be defined before they are used**,
making it possible to define mutually recursive functions/types without
any special syntax.
There are some exceptions to this. We cannot forward reference a symbol
`f` in some statement `s` if between `s` and the definition of `f` there
is one of the following statements:
1. Local module
2. Import statement
3. Open statement
I think it should be possible to drop the restriction for local modules
and import statements
- Depends on #2219
- Closes#1643
This pr introduces a `list` as a new builtin so that we can use syntax
sugar both in expressions and patterns. E.g. it is now possible to write
`[1; 2; 3;]`.
* Fixes the indices in `inline` and `specialize` for local lambda-lifted
identifiers.
* Adds the `specialize-by` pragma which allows to specialize a local
function by some of its free variables, or specialize arguments by name.
For example:
```
funa : {A : Type} -> (A -> A) -> A -> A;
funa {A} f a :=
let
{-# specialize-by: [f] #-}
go : Nat -> A;
go zero := a;
go (suc n) := f (go n);
in go 10;
```
If `funa` is inlined, then `go` will be specialized by the actual
argument substituted for `f`.
* Closes#2147
Adds a `specialize` pragma which allows to specify (explicit) arguments
considered for specialization. Whenever a function is applied to a
constant known value for the specialized argument, a new version of the
function will be created with the argument pasted in. For example, the
code
```juvix
{-# specialize: [1] #-}
mymap : {A B : Type} -> (A -> B) -> List A -> List B;
mymap f nil := nil;
mymap f (x :: xs) := f x :: mymap f xs;
main : Nat;
main := length (mymap λ{x := x + 3} (1 :: 2 :: 3 :: 4 :: nil));
```
will be transformed into code equivalent to
```juvix
mymap' : (Nat -> Nat) -> List Nat -> List Nat;
mymap' f nil := nil;
mymap' f (x :: xs) := λ{x := x + 3} x :: mymap' xs;
main : Nat;
main := length (mymap' (1 :: 2 :: 3 :: 4 :: nil));
```
* Closes#2226
For the program
```juvix
module letrec;
import Stdlib.Prelude open;
myfun : {A : Type} -> (A -> A) -> A -> A;
myfun {A} f a :=
let
go : Nat -> A -> A;
go' : Nat -> A -> A;
go zero a := a;
go (suc n) a := f (go' n a);
go' zero a := a;
go' (suc n) a := f (go n a);
in
go 5 a;
main : Nat;
main := myfun ((+) 1) 7;
```
after translating to Core and lambda-lifting we got the incorrect
indices in types of the let-bindings.
```
def myfun : Π A : Type, (A$0 → A$1) → A$1 → A$2 :=
λ(A : Type)
λ(f : A$0 → A$1)
λ(a : A$1)
let go' : Int → a$1 → a$2 := go'_9 A$2 f$1 in
let go : Int → a$2 → a$3 := go_10 A$3 f$2 in
go$0 5 a$2;
```
The indices have been corrected in this PR.
This PR prepares the 0.4.1 release.
* Bump version in package.yaml
* Update version smoke test
* Updates CHANGELOG
NB: The links in the changelog will not work until we create the release
tag.
* Closes#2200
For example,
```
def power' : Int → Int → Int → Int :=
λ(acc : Int)
λ(a : Int)
λ(b : Int)
if = b 0 then acc else if = (% b 2) 0 then power' acc (* a a) (/ b 2) else power' (* acc a) (* a a) (/ b 2);
```
is transformed into
```
def power' : Int → Int → Int → Int :=
λ(acc : Int)
λ(a : Int)
λ(b : Int)
if = b 0 then acc else let _X : Bool := = (% b 2) 0 in
power' (if _X then acc else * acc a) (* a a) (/ b 2);
```
This PR replaces fetching a precompiled binary of smoke with a
build/cache for macOS smoke tests on CI.
smoke dynamically links to icu4c, so a cached binary of smoke will break
when brew bumps the icu4c version. In this PR we use the icu4c version
in the cache key of the smoke build to avoid this issue.
NB: The smoke build cannot be done as a separate job because the smoke
binary must be built using exactly the same version of the macos-12
runner image as the smoke testing step to make sure that the icu4c
versions match.
Motivation for doing this is this failure:
https://github.com/anoma/juvix/actions/runs/5325094406/jobs/9645334642
which uses this release of the runner image
https://github.com/actions/runner-images/releases/tag/macOS-12%2F20230618.1
which contains the updated brew version of icu4c.
20230618.1 is currently a prerelease, but will start to run on more jobs
shortly.
```
2023-06-20T17:10:13.2222310Z Copied executables to /Users/runner/.local/bin:
2023-06-20T17:10:13.2223440Z - juvix
2023-06-20T17:10:13.5312790Z dyld[90256]: Library not loaded: '/usr/local/opt/icu4c/lib/libicuuc.72.dylib'
2023-06-20T17:10:13.5331930Z Referenced from: '/Users/runner/hostedtoolcache/jonaprieto/smoke/latest/darwin-x64/smoke'
2023-06-20T17:10:13.5333610Z Reason: tried: '/usr/local/opt/icu4c/lib/libicuuc.72.dylib' (no such file), '/usr/local/lib/libicuuc.72.dylib' (no such file), '/usr/lib/libicuuc.72.dylib' (no such file), '/usr/local/Cellar/icu4c/73.2/lib/libicuuc.72.dylib' (no such file), '/usr/local/lib/libicuuc.72.dylib' (no such file), '/usr/lib/libicuuc.72.dylib' (no such file)
2023-06-20T17:10:13.5334690Z make[1]: *** [smoke-only] Abort trap: 6
2023-06-20T17:10:13.5335310Z make: *** [smoke] Error 2
2023-06-20T17:10:13.5363170Z ##[error]Process completed with exit code 2.
```
When `juvix format` is invoked from some directory within a juvix
project then the formatter is run on all the files contained in the
project.
If `juvix format` is run from some directory outside of a Juvix project
then an error is reported. The user gets the same error as they would
get if
`juvix format` was run with a directory argument that is not within a
Juvix project.
* Closes https://github.com/anoma/juvix/issues/2087
Previously if a project looked like (where `Unformatted.juvix` contains
unformatted code, and `Formatted.juvix` is fully formatted):
```
Dir
|- juvix.yaml
|- Unformatted.juvix
|- Subdir
|- Formatted.juvix
```
and the user ran `juvix format Dir/` then the command would return exit
code 0 instead of exit code 1. This is because only the result from
formatting files within `Subdir` was used, the result from `Dir` was
discarded.
This PR fixes this, the results of formatting all subdirectories in a
project are combined appropriately.
This PR was already merged in https://github.com/anoma/juvix/pull/2173,
but main was subsequently forced pushed as part of the 0.4.0 release and
these changes were erased by mistake.
This PR changes the behaviour of the formatter when run on files that
are already formatted. Previously the source of a file that was already
formatted was not output by the formatter.
After this PR, the formatter always outputs the contents of a formatted
file (when used on a single file, and if the --check option is not
specified).
If the `format: false` pragma is set then the source is echoed verbatim,
without highlighting (because it's not possible to get the highlighting
without the formatting).
This probably helps implementing the formatter in the vscode extension,
see https://github.com/anoma/vscode-juvix/issues/98
* 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.
The constr_info_t struct has changed, so this example must be changed
accordingly.
The benchmark builds are still broken because I missed this file in
https://github.com/anoma/juvix/pull/2192
I've removed the unsupported wasm target from the `compile.sh` script in
the benchmark directory to make it easier to spot errors.
