1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-14 08:27:03 +03:00
Commit Graph

1094 Commits

Author SHA1 Message Date
Jan Mas Rovira
ef16b45ca6
Aliasing (#2301)
- 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.
2023-08-25 15:28:58 +02:00
Łukasz Czajka
2baad15a41 Remove old function syntax (#2305)
* Enables new function syntax in local let-declarations
* Closes #2251
2023-08-24 16:24:47 +02:00
Jonathan Cubides
56871a204c Bump version to v0.4.3 2023-08-24 16:24:40 +02:00
Paul Cadman
a167fee9d8
Fix shell variables in linux static build stack install (#2309) 2023-08-23 23:36:26 +01:00
Paul Cadman
06346d18de
Replace gitrev with githash for obtaining build-time git info (#2308)
This PR replaces [gitrev](https://hackage.haskell.org/package/gitrev)
with [githash](https://hackage.haskell.org/package/githash) which
provides more reliable git information about the current git info, it
seems to work as expected. githash originated as a fork of gitrev
containing fixes https://github.com/snoyberg/githash/issues/11

This PR also fixes the issue with git info detection in the linux static
build. There was a permission issue in the build container that caused
git cli calls to fail.

Closes:
* https://github.com/anoma/juvix/issues/2294
* https://github.com/anoma/juvix/issues/2130
2023-08-23 15:53:23 +01:00
Jan Mas Rovira
5194e7c2cd
Check that type functions are supported (#2306)
- Closes #2297 

When the type of function definition is of the form `... -> Type` it has
to have only one clause and no pattern matching.
2023-08-23 13:18:57 +02:00
Łukasz Czajka
fa7489a9cb
Minor comment updates (#2303) 2023-08-22 15:26:45 +02:00
Paul Cadman
da9e511bab
Update stdlib to use new ADT and record syntax (#2302)
The associated stdliib PR is:

* https://github.com/anoma/juvix-stdlib/pull/76
2023-08-22 13:50:14 +02:00
Jan Mas Rovira
d57f1a3d64
Fix bug in arity checker with pi types (#2300)
All variables bound in a pi type were assumed to be of arity unit. This
pr fixes that.

- Closes #2296
2023-08-22 11:40:12 +02:00
Łukasz Czajka
63a94bb976
Allow omitting : Type in implicit function argument definitions and in type definitions (#2291)
* Closes #2281

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-08-22 10:32:26 +02:00
Łukasz Czajka
4b29f551b4
Allow wildcard arguments in new function definition syntax (#2295)
* Closes #2288
2023-08-16 17:51:09 +02:00
Łukasz Czajka
8095e52c21
Check for incomparable precedences (#2289)
Give an error when there are two operators with incomparable precedences
instead of linearising the ordering arbitrarily.
2023-08-16 16:33:29 +02:00
Łukasz Czajka
1abeeb96b9
Improve iterator and named arguments parsing (#2278)
Avoid excessive backtracking in iterator and named arguments parsing.
This also improves error messages by committing to a parsing branch as
early as possible.
2023-08-15 15:28:10 +02:00
Paul Cadman
46ab163ca7
Update stackage resolver to LTS 21.6 (#2275)
Stack LTS 21.6 uses GHC 9.4.5, binaries for HLS are available via ghcup.

Changes required:

1. Fix warnings about type level `:` and `[]` used without backticks.
2. Fix warnings about deprecation of builtin `~` - replaced with `import
Data.Type.Equality ( type (~) )` in the Prelude
3. SemVer is no longer a monoid
4. `path-io` now contains the `AnyPath` instances we were defining
(thanks to Jan) so they can be removed.
5. Added `aeson-better-errors-0.9.1.1` as an extra-dep. The reason it is
not part of the resolver is only because it has a strict bound on base
which is not compatible with ghc 9.4.5. To work around this I've set:

    ```
    allow-newer: true
    allow-newer-deps:
      - aeson-better-errors
    ```
which relaxed the upper constraint bounds for `aeson-better-errors`
only. When the base constraints have been updated we can remove this
workaround.

6. Use stack2cabal to generate the cabal.project file and to freeze
dependency versions.

    https://www.stackage.org/lts-21.6/cabal.config now contains the
constraint `haskeline installed`, which means that the version of
haskeline that is globally installed with GHC 9.4.5 will be used, see:
    * https://github.com/commercialhaskell/stackage/issues/7002
GHC 9.4.5 comes with haskeline 0.8.2 preinstalled but our configuration
contains the source-repository-package for haskeline 0.8.2.1 (required
because we're using a fork) so if you try to run` cabal build` you get a
conflict.

Constraints from cabal imports cannot yet be overridden so it's not
possible to get rid of this conflict using the import method. So we need
to use stack2cabal with an explicit freeze file instead.

7. Remove `runTempFilePure` as this is unused and depends on
`Polysemy.Fresh` in `polysemy-zoo` which is not available in the
resolver. It turns out that it's not possible to use the `Fresh` effect
in a pure context anyway, so it was not possible to use
`runTempFilePure` for its original purpose.

8. We now use https://github.com/benz0li/ghc-musl as the base container
for static linux builds, this means we don't need to maintain our own
Docker container for this purpose.

9. The PR for the nightly builds is ready
https://github.com/anoma/juvix-nightly-builds/pull/2, it should be
merged as soon as this PR is merged.

Thanks to @benz0li for maintaining https://github.com/benz0li/ghc-musl
and (along with @TravisCardwell) for help with building the static
binary.

* Closes https://github.com/anoma/juvix/issues/2166
2023-08-11 11:49:33 +02:00
Łukasz Czajka
b5a3b0088e
Error on duplicate keys in YAML (#2290)
* Closes #2285
2023-08-11 09:22:22 +01:00
Łukasz Czajka
eebe961321
User-friendly operator declaration syntax (#2270)
* Closes #1964 

Adds the possibility to define operator fixities. They live in a
separate namespace. Standard library defines a few in
`Stdlib.Data.Fixity`:
```

syntax fixity rapp {arity: binary, assoc: right};
syntax fixity lapp {arity: binary, assoc: left, same: rapp};
syntax fixity seq {arity: binary, assoc: left, above: [lapp]};

syntax fixity functor {arity: binary, assoc: right};

syntax fixity logical {arity: binary, assoc: right, above: [seq]};
syntax fixity comparison {arity: binary, assoc: none, above: [logical]};

syntax fixity pair {arity: binary, assoc: right};
syntax fixity cons {arity: binary, assoc: right, above: [pair]};

syntax fixity step {arity: binary, assoc: right};
syntax fixity range {arity: binary, assoc: right, above: [step]};

syntax fixity additive {arity: binary, assoc: left, above: [comparison, range, cons]};
syntax fixity multiplicative {arity: binary, assoc: left, above: [additive]};

syntax fixity composition {arity: binary, assoc: right, above: [multiplicative]};
```

The fixities are identifiers in a separate namespace (different from
symbol and module namespaces). They can be exported/imported and then
used in operator declarations:
```
import Stdlib.Data.Fixity open;

syntax operator && logical;
syntax operator || logical;
syntax operator + additive;
syntax operator * multiplicative;
```
2023-08-09 18:15:51 +02:00
Paul Cadman
7b000eba0c
Fixes behaviour of default stdlib when internal-build-flag is set (#2283)
The mechanism for using `--internal-build-flag` to set the build
directory for the default stdlib location already existed, it was just
unused (Nothing always passed in, instead of the entry point):


11ebc4acde/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/PathResolver.hs (L128)

This PR fixes that issue, adds some smoke tests to check the behaviour
of the stdlib dependency.

* Closes https://github.com/anoma/juvix/issues/2273

The issue with what to do with relative stdlib dependency paths when
`--internal-build-flag` is set remains open:
https://github.com/anoma/juvix/issues/2274
2023-08-09 16:12:44 +01:00
Paul Cadman
e0aadef298
Prettyprint aggregate ADT constructor types with parentheses (#2284)
This PR fixes an issue with formatting ADT definitions.

Previously the pretty printer would remove required parentheses from
aggregate constructor arguments: `type t (A : Type) := c A (t A) ` ->
`type t (A : Type) := c A t A`.

We now handle this in the same way as patterns.

* https://github.com/anoma/juvix/issues/2277
2023-08-09 09:48:58 +01:00
Łukasz Czajka
9718433a89
Enable builtin list syntax in the standard library (#2282) 2023-08-08 17:33:43 +02:00
Jan Mas Rovira
98b3621ae1
Record patterns (#2271)
- 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;
```
2023-08-08 16:01:20 +02:00
Jan Mas Rovira
f7382caeac
Record updates (#2263)
- 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.
2023-08-07 12:35:36 +02:00
Paul Cadman
18b664aa53
Fix benchmark wasmer command (#2268)
The benchmark run has been failing since the latest release of wasmer.


https://github.com/anoma/juvix-nightly-builds/actions/runs/5746121923/job/15575622923

wasmer no longer supports the --disable-cache option and there's no
equivalent that I can find in the new CLI.
2023-08-03 13:44:36 +01:00
Łukasz Czajka
22de9d0233
Disallow iterators with zero ranges (#2267)
* Closes #2265
2023-08-03 11:43:59 +02:00
Jan Mas Rovira
f38123c550
Adt syntax (#2262)
- 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>
2023-08-01 13:39:43 +01:00
Jan Mas Rovira
4a6a7e6540
Add field projections for records (#2260)
- 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;
```
2023-08-01 09:46:22 +01:00
Łukasz Czajka
3c5cc744ec
Don't print pragmas in documentation (#2266)
* Fixes #2187
2023-07-31 14:33:05 +02:00
Łukasz Czajka
70dea79181
Minor refactor and script update (#2261)
* Updates the `cntlines.sh` script to take into account the removal of
Abstract.
* Moves the VampIR runtime to `runtime/src/vampir`.
2023-07-27 17:57:20 +02:00
Jan Mas Rovira
65b000999d
Separate modules namespace (#2257) 2023-07-26 09:59:50 +02:00
Jonathan Cubides
d27da6f17c
Bump version to v0.4.2 🎉 (#2259)
This PR updates:

- package version 
- smoke test 
- changelog

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-07-25 10:35:26 +02:00
Jan Mas Rovira
e79159b21e
Add record declaration syntax (#2254)
- 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.
2023-07-24 16:56:13 +02:00
Jan Mas Rovira
ea652e5279
Refactor deriving statements in Concrete.Language (#2256)
Deriving instances was a pita because of the extensive use of type
families. I have refactored the code to make it easier to work with
2023-07-19 15:39:23 +01:00
Jan Mas Rovira
49a0bc0496
Rename inductive constructor (#2255)
Rename `InductiveConstructorDef` -> `ConstructorDef` in `Concrete` so
that it is consistent with `Internal` and its field names
2023-07-18 12:50:30 +01:00
Jan Mas Rovira
2d666fd82c
Named arguments (#2250)
- 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}`.
2023-07-18 10:32:34 +01:00
Jan Mas Rovira
9ad2d71001
Format juvix files using new function syntax (#2245) 2023-07-11 17:22:07 +02:00
Jan Mas Rovira
9fdf848e3e
Typcheck imports before statements (#2253)
- closes #2248
2023-07-11 12:26:52 +02:00
Jan Mas Rovira
366afb5dad
Parse many consecutive - as a comment (#2240)
- Closes #2190
2023-07-11 11:35:33 +02:00
Łukasz Czajka
bf6603eb33
Update to GEB version 0.3.2 (#2244)
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)).
2023-07-11 11:02:48 +02:00
Jan Mas Rovira
2c8a364143
New syntax for function definitions (#2243)
- 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
2023-07-10 19:57:55 +02:00
Jan Mas Rovira
0cc689a2ef
Add syntax for builtin list (#2239)
- 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;]`.
2023-07-03 13:24:56 +02:00
Łukasz Czajka
ff940b427e
Local pragmas improvements (#2236)
* 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`.
2023-06-30 16:59:29 +02:00
Jan Mas Rovira
d69d8c6eca
Remove abstract (#2219)
- Closes #2002 
- Closes #1690 
- Closes #2224
- Closes #2237
2023-06-30 15:01:46 +02:00
Jan Mas Rovira
38028d2dff
Fix bug in aritychecker (#2238)
When inserting wildcards on the LHS of a clause, we were reusing the
same variable, which is wrong. Now fresh variables are generated.

- Closes #2235
2023-06-29 17:25:30 +02:00
Łukasz Czajka
39ef069bfc
Fold lets when the bound variable occurs at most once (#2231)
For example, convert
```
let x := f a b c in
g x
```
to
```
g (f a b c)
```
2023-06-29 13:02:10 +02:00
Łukasz Czajka
b4347bdd23
Numeric range types (#2232)
* Closes #2145
2023-06-28 17:24:08 +02:00
Łukasz Czajka
755f02ab4c
Fix bug in computeTypeInfo (#2234)
* Closes #2233
2023-06-28 16:08:12 +02:00
Łukasz Czajka
5b44b2e654
Use specialization pragmas in the standard library (#2230)
* Adds `specialize` pragmas for folds, maps, etc.
* Fixes two bugs in `specializeArgs`
2023-06-27 15:37:11 +02:00
Łukasz Czajka
2fff65030b
Case folding (#2229)
Fold constant cases, i.e., convert
```
case C a b
| A := ..
| B x := ..
| C x y := M
```
to
```
let x := a;
     y := b;
in
M
```
2023-06-27 12:29:26 +02:00
Łukasz Czajka
7c039d687b
Specialization optimisation (#2164)
* 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));
```
2023-06-26 16:49:19 +02:00
Łukasz Czajka
82a86ace45
Fix de Bruijn indices in LetRecs (#2227)
* 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.
2023-06-26 12:05:51 +02:00
Paul Cadman
4ab201f1ac
Bump version to 0.4.1 and update CHANGELOG (#2225)
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.
2023-06-23 12:39:27 +01:00