- Closes#2269
Example:
```
type Sum (A B : Type) :=
| inj1 {
fst : A;
snd : B
}
| inj2 {
fst : A;
snd2 : B
};
sumSwap {A B : Type} : Sum A B -> Sum B A
| inj1@{fst; snd := y} := inj2 y fst
| inj2@{snd2 := y; fst := fst} := inj1 y fst;
```
- Closes#1642.
This pr introduces syntax for convenient record updates.
Example:
```
type Triple (A B C : Type) :=
| mkTriple {
fst : A;
snd : B;
thd : C;
};
main : Triple Nat Nat Nat;
main :=
let
p : Triple Nat Nat Nat := mkTriple 2 2 2;
p' :
Triple Nat Nat Nat :=
p @Triple{
fst := fst + 1;
snd := snd * 3
};
f : Triple Nat Nat Nat -> Triple Nat Nat Nat := (@Triple{fst := fst * 10});
in f p';
```
We write `@InductiveType{..}` to update the contents of a record. The
`@` is used for parsing. The `InductiveType` symbol indicates the type
of the record update. Inside the braces we have a list of `fieldName :=
newValue` items separated by semicolon. The `fieldName` is bound in
`newValue` with the old value of the field. Thus, we can write something
like `p @Triple{fst := fst + 1;}`.
Record updates `X@{..}` are parsed as postfix operators with higher
priority than application, so `f x y @X{q := 1}` is equivalent to `f x
(y @X{q := 1})`.
It is possible the use a record update with no argument by wrapping the
update in parentheses. See `f` in the above example.
- 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));
```
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.
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.
- Closes#2162
This pr improves formatting of source files with comments.
The concrete ast now stores location information of almost all keywords.
We do not store location information of parentheses. Comments will be
pushed out of parentheses by the formatter.
E.g.
```
( -- comment
f x)
```
will become
```
-- comment
(f x)
```
This only occurs if the comment appears just after the `(`. So the
following will be respected
```
(f --comment
x)
```
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
`format` command now returns code `0` most of the time.
It will return `1` when:
* some error occur, so can not format
* file is unformatted and `--check` option is used
* One or more files are not formatted in a Juvix project.
- Fixes#2171
Say we have a module that import/open the Prelude:
Test.juvix
```
module Test;
import Stdlib.Prelude open;
```
When the module is compiled, we have a step in the compiler pipeline
which filters out unreachable symbols. For this module all symbols are
filtered because the module contains no definitions.
So if the module is loaded in the REPL, no symbols will be available to
process through the evaluator. The REPL is a place to explore the
symbols in the module so (like with Haskell's GHCi) it would be useful
if all symbols were available in the REPL session. That's what this PR
implements.
* Closes https://github.com/anoma/juvix/issues/2159
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- Closes#2128
- Closes#2161
This pr fully implements the monadic pretty printer based on
`ExactPrint`, which respects comments. Until now, comments inside
expressions were printed after the current statement. Now they are
printed in the correct place, except when a comment occurs before
something that we don't store its location. E.g. parentheses,
semicolons, braces, colons, etc. I proposed that we irone out this issue
in a separate pr.
Since the old non-monadic algorithm is no longer necessary, I removed
it.
This does not change any examples or documentation. The interface of the
standard library remains unchanged (except the addition of new
iterators), so this PR can be merged without side effects.
* Closes#2146
* Closes#2134
Adds the `argnames` pragma which specifies function argument names.
These will be the names used in Core and subsequently in VampIR for the
`main` function.
```
{-# argnames: [x, y] -#}
main : Nat -> Nat -> Nat;
```
If set, `JUVIX_LLVM_DIST_PATH` should point to the root of a LLVM
installation, i.e clang should be present
in`$JUVIX_LLVM_DIST_PATH`/bin/clang.
If `JUVIX_LLVM_DIST_PATH` is not set, or `clang` is not available there
then the system PATH is used instead, (this is the current behaviour).
The `juvix doctor` clang checks use the same logic as `juvix compile` to
find and check the `clang` executable.
To help with debugging the clang location, this PR also adds `juvix
doctor --verbose` which prints the location of the `clang` executable
and whether it was found using the system PATH or the
JUVIX_LLVM_DIST_PATH environment variable:
```
juvix doctor --verbose
> Checking for clang...
| Found clang at "/Users/paul/.local/share/juvix/llvmbox/bin/clang" using JUVIX_LLVM_DIST_PATH environment variable
```
or
```
juvix doctor --verbose
> Checking for clang...
| Found clang at "/Users/paul/.local/bin/clang" using system PATH
```
* Closes https://github.com/anoma/juvix/issues/2133
