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

1025 Commits

Author SHA1 Message Date
Jonathan Cubides
56cde347d3
Refactor isValidChar (#2194)
Move common functions to Prelude
2023-06-16 09:43:15 +02:00
Łukasz Czajka
31627a0ce5
Check valid argument names in YAML (#2193)
* Closes #2191
2023-06-15 16:42:58 +02:00
Paul Cadman
121e883a49
Fix benchmark runtime C examples (#2192)
The constr_info_t struct has changed, so these examples must be changed
accordingly.

This should fix the failing benchmark builds
https://github.com/anoma/juvix-nightly-builds/actions/runs/5274325536/jobs/9538974076
2023-06-15 14:38:42 +01:00
Jonathan Cubides
925d7cb749 Bump to version 0.4.0 🎉 2023-06-09 18:44:39 +02:00
Jan Mas Rovira
b7b0e1039e
Store source location of (almost) everything (#2174)
- 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>
2023-06-07 19:57:51 +02:00
Veronika Romashkina
216c1cd0e8
Change terminal colours to be more align with the scheme (#2183)
Colouring in the REPL now is a bit closer to the scheme we have for
Juvix.
Because of the allowed colors in the `prettyprinter-ansi-terminal` we
can use one of the standard colours only:
<img width="896" alt="Screenshot 2023-06-07 at 07 05 34"
src="https://github.com/anoma/juvix/assets/8126674/c0077c7c-edba-4ed8-9824-f9b9e773e943">

- Fixes https://github.com/anoma/vscode-juvix/issues/107
2023-06-07 18:21:17 +02:00
Łukasz Czajka
4c2aa499af
Use stderr for errors in the runtime (#2184)
* Closes #1902
2023-06-07 14:38:28 +02:00
Veronika Romashkina
8e59624ff5
Format returns 0 when file is not formatted (#2181)
`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
2023-06-07 13:53:10 +02:00
Łukasz Czajka
4c0e0b13c8
Respect fixity in runtime printer (#2182)
* Closes #2180
2023-06-07 11:44:41 +02:00
Łukasz Czajka
9db16ca87f
Fix 'function not found' error in juvix eval (#2178)
* Closes #2176

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-06-06 13:26:43 +02:00
Łukasz Czajka
5d85cb44f2
Print values in juvix eval (#2179)
* Closes #2177
2023-06-06 12:35:01 +02:00
Paul Cadman
108ccf7dcf
Do not filter unreachable symbols when compiling for REPL (#2172)
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>
2023-06-05 16:52:52 +01:00
Łukasz Czajka
68b4b38f98
Improve parsing error messages (#2170)
* Closes #2160 
* Closes #2167 
* Closes #2168
2023-06-05 12:06:05 +02:00
Jonathan Cubides
d869ce4dd6 Bump version to v0.3.5 🎉 2023-06-02 17:28:07 +02:00
Jan Mas Rovira
f4aa70b13d
Finish the new pretty printing algorithm and delete the old one (#2151)
- 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.
2023-06-02 13:02:35 +02:00
Jan Mas Rovira
02e9f89e5e
Properly scan imports inside local modules (#2165)
- Closes #2163 

Nested imports where not scanned properly when building the Internal
InfoTable. That is no fixed
2023-06-02 12:12:02 +02:00
Łukasz Czajka
e0689801cf
Update standard library for better readability, efficiency and iterator use (#2153)
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
2023-06-01 18:21:03 +02:00
Łukasz Czajka
c4c92d5fcf
Allow to specify VampIR variable names (#2141)
* 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;
```
2023-06-01 17:36:47 +02:00
Paul Cadman
7e1a641908
Support new import ... open syntax in REPL (#2156)
Similar to https://github.com/anoma/juvix/pull/2098 which introduced the
new `import ... open` syntax the old syntax is still supported.

The `try` must be removed when the old `open import ...` syntax is
removed.

* Closes https://github.com/anoma/juvix/issues/2155
2023-06-01 16:44:08 +02:00
Jan Mas Rovira
c66213e06a
Add extra git dependencies to cabal.project (#2158)
- Closes #2157
2023-06-01 13:32:34 +01:00
Paul Cadman
40e6648ae1
Use theJUVIX_LLVM_DIST_PATH environment variable to search for the clang executable (#2152)
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
2023-06-01 12:18:31 +02:00
Łukasz Czajka
757b4ed180
VampIR pipeline: handle booleans in the type of main (#2137)
* Closes #2132

---------

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-06-01 11:42:35 +02:00
Łukasz Czajka
d08d8ce7eb
Add the format pragma (#2150)
* Closes #2117
2023-05-31 23:30:59 +02:00
Łukasz Czajka
b293e19ac9
Remove code for Eval and Print statements (#2149)
* Closes #2052
2023-05-31 10:19:58 +02:00
Jan Mas Rovira
88c5dabb6d
Add Semigroup instance for AnsiText (#2140)
`AnsiText` is a type that represents some text that can be printed with
`Ansi` formatting annotations, or as plain text. It is expected that it
should have a `Semigroup` instance. This pr adds that.

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-05-31 08:53:08 +01:00
Jan Mas Rovira
f56110b87e
Add :doc command to the repl (#2142) 2023-05-30 18:19:39 +02:00
Łukasz Czajka
649d905b85
Fix printing of infix constructor values (#2144)
To print e.g.
```agda
(::) :: nil
```
instead of
```agda
:: :: nil
```
2023-05-30 17:11:18 +02:00
Łukasz Czajka
e9284b3ef6
Iterator syntax (#2126)
* Closes #1992 

A function identifier `fun` can be declared as an iterator with
```
syntax iterator fun;
```
For example:
```haskell
syntax iterator for;
for : {A B : Type} -> (A -> B -> A) -> A -> List B -> List A;
for f acc nil := acc;
for f acc (x :: xs) := for (f acc x) xs;
```
Iterator application syntax allows for a finite number of initializers
`acc := a` followed by a finite number of ranges `x in xs`. For example:
```
for (acc := 0) (x in lst) acc + x
```
The number of initializers plus the number of ranges must be non-zero.

An iterator application
```
fun (acc1 := a1; ..; accn := an) (x1 in b1; ..; xk in bk) body
```
gets desugared to
```
fun \{acc1 .. accn x1 .. xk := body} a1 .. an b1 .. bk
```
The `acc1`, ..., `accn`, `x1`, ..., `xk` can be patterns.

The desugaring works on a purely syntactic level. Without further
restrictions, it is not checked if the number of initializers/ranges
matches the type of the identifier. The restrictions on the number of
initializers/ranges can be specified in iterator declaration:
```
syntax iterator fun {init: n, range: k};
syntax iterator for {init: 1, range: 1};
syntax iterator map {init: 0, range: 1};
```
The attributes (`init`, `range`) in between braces are parsed as YAML to
avoid inventing and parsing a new attribute language. Both attributes
are optional.
2023-05-30 15:30:11 +02:00
Jan Mas Rovira
b4154f70a4
Add ValueType (#2143)
- Closes #2136
2023-05-30 11:51:28 +02:00
Jan Mas Rovira
e944f85074
Add :def command to the repl (#2119)
This pr adds a new command, `:def` to the repl. This command expects a
single identifier that must be in scope and then prints its definition.
For constructors, the whole type definition is printed.

It also applies some refactors to the code for repl command.
1. Before there was a mega `where` block of definitions. I have hoisted
most of the definitions there to the top level. I feel like now it is
easier to navigate and read.
2. Use `ExceptT` instead of local `case` expressions for errors.
3. Use forks of `haskeline` and `repline`. These forks are necessary
because these libraries do not export the constructors `HaskelineT` and
`InputT` respectively, thus, making it impossible to catch errors in
their underlying monad.
2023-05-30 10:19:09 +02:00
Jan Mas Rovira
121063cf0b
Show unicode characters without escaping (#2127)
- Closes #2064
2023-05-24 21:35:07 +02:00
Jan Mas Rovira
4fcb881ebc
Add main field to juvix.yaml (#2120)
- Closes #2067

This pr adds the field `main` to `juvix.yaml`. This field is optional
and should contain a path to a juvix file that is meant to be used for
the `compile` (and `dev compile`) command when no file is given as an
argument in the CLI. This makes it possible to simply run `juvix
compile` if the `main` is specified in the `jvuix.yaml`.

I have updated the `juvix.yaml` of the milestone examples.

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-05-24 15:42:20 +02:00
Jonathan Cubides
68ed1461ab
Add gnu-sed to the macOS build in the CI (#2123)
This PR installs the `gnu-sed` for the macOS build.
It can be called with the name `sed`, no `gsed`.

NB: The environmental variables set in one step are only reflected in
the subsequent steps.
2023-05-24 13:32:08 +01:00
Łukasz Czajka
9765686b97
Fix spurious messages from Makefile.generic (#2125)
* Closes #2124
2023-05-24 12:50:02 +02:00
Veronika Romashkina
acb8b0c773
Fix baseUrl for juvix docs in Doctor command (#2122)
Currently generated links for fixing errors in the `juvix doctor`
command are broken.
Fixing that by updating the base Url link.

Also fixed the link to the installation of juvix in the contributing
guide.
2023-05-24 12:14:30 +02:00
Veronika Romashkina
b4e7dbc7fd
Remove --no-format option (#2121)
Instead, always act as `--no-format` option is set to `False` as
previous default.

The change seem to not affect any current formatting, so I assume it
passes the checks on testing.

Fixes #2084 

# Checklist:

- [x] My code follows the style guidelines of this project
- [ ] I have made corresponding changes to the documentation
- [x] My changes generate no new warnings
2023-05-24 10:46:18 +02:00
Jan Mas Rovira
39b797ecfa
Add Bottom node (#2112)
- Closes #2056 
- Depends on #2103 

I am not sure about the implementation of `isType` for `NBot`. (solved).

The `Eq` instance returns `True` for every two `Bottom` terms,
regardless of their type.

---------

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
2023-05-23 18:31:28 +02:00
Łukasz Czajka
d576111241
VampIR integration (#2103)
* Closes #2035 
* Depends on #2086 
* Depends on #2096 
* Adds end-to-end tests for the Juvix-to-VampIR compilation pipeline.

---------

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-05-22 20:18:18 +02:00
Jonathan Cubides
2148d174f5
Add VampIR to the CI (#2096)
This PR:

- Makes `vamp-ir` available in the CI (pre-release 0.1.2)
- [Use a setup-wasmer action to install
`wasmer`](https://github.com/marketplace/actions/setup-wasmer)
- Fixes cache option value for `jaxxstorm/action-install-gh-release`'s
usages

Adds support for:

- #2103 


Related: 

- https://github.com/anoma/vamp-ir/issues/90

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-05-22 19:49:36 +02:00
Jonathan Cubides
3ec54b7189 Bump version to v0.3.4 🎉 2023-05-22 18:51:42 +02:00
Łukasz Czajka
6bfe727a0e
Add syntax keyword (#2107)
* Closes #2007
2023-05-22 12:50:07 +02:00
Jan Mas Rovira
b25873ac6a
Allow symbol renaming inside using {..} (#2109)
- Closes #2090 
- Depends on #2108
2023-05-22 12:24:29 +02:00
Jan Mas Rovira
ab83749a86
Scope check symbols inside using {..} and hiding {..} (#2108)
- Closes #2089 

Now the symbols inside `using {..}` and `hiding {..}` are properly
scoped, which means that they will be properly colored and will have
goto information. If the referenced module does not contain a symbol in
the list, an error will be thrown.
2023-05-22 11:41:13 +02:00
Jonathan Cubides
e2f2d0a2f4
Fix Makefile target bugs for formatting and type Checking Juvix files (#2057)
This PR resolves a few bugs in the Makefile targets for formatting and
type checking Juvix files, which were preventing the capture of type
checking errors for our examples and bad formatting for all the Juvix
files in the repository. With this PR, our code should now be clean, and
we can expect every file to be properly formatted and type checked.

Changes made:

- [x] Updated `make format-juvix-files`
- [x] Updated `make check-format-juvix-files`
- [x] Formatted all Juvix files
- [x] Comment a fragment in `examples/milestone/Bank/Bank.juvix`

In the future, we will drastically simplify the Makefile once we improve
the `format` and the `type check` command for example posted here:

- #2066 
- #2087 

Related:

- #2063 
- #2040 (due to some typechecking errors we're not capturing before)
- #2105
- https://github.com/anoma/juvix/issues/2059
2023-05-19 17:33:56 +02:00
Paul Cadman
4a1c7a101e
Pass through compile optimization flag to C compiler and disable optimization for --debug (#2106)
In this PR we pass through the `juvix compile` optimization flag to the
C compiler in the native compilation.

NB: Clang supports -On for any positive n. -O4 and higher is equivalent
to -O3

Also we disable optimizations when the `-g` / `--debug` option is
specified.

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

---------

Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
2023-05-19 15:29:52 +01:00
Łukasz Czajka
fe78ff451c
Direct translation from normalized JuvixCore to VampIR (#2086)
* Closes #2034.
* Adds the `vampir` target to the `compile` command.
* Adds two tests which are not yet enabled because `vamp-ir` is not
available in the CI (these and more tests will be enabled in #2103).
2023-05-19 14:43:45 +02:00
Jan Mas Rovira
9b1011b8ad
Add syntax for Judoc blocks (#2102)
- Closes #2050 

This pr adds the possibility to give judoc documentation in blocks
delimited by `{--` and `--}`.
- Inside these blocks, normal comments are disabled.
- It is allowed to have multiple blocks associated with the same
identifier, e.g.
```
{-- an axiom --}
{-- of type ;Type; --}
axiom a : Type;
```
- Nested blocks are *not* allowed.
- Blocks can be empty: `{-- --}`.
- The formatter respects line breaks inside blocks.
- The formatter normalizes whitespace at both ends of the block to a
single whitespace.
2023-05-19 14:05:32 +02:00
Jan Mas Rovira
d9d72f98eb
Simplify formatting of lambdas with a single clause (#2105)
After this pr, lambdas with a single clause will be printed in one line,
without a preceding `|`. I.e. `\ {x := x}`.
2023-05-19 13:24:02 +02:00
Paul Cadman
ad3607f104
Fix extra whitespace in text rendering of indented empty lines (#2101)
The prettyprinter library takes care avoid adding whitespace to empty
lines when it is rendering indented text.

See:

7e32c010ec/prettyprinter/src/Prettyprinter/Internal.hs (L1999)

However it only does this for unannotated text.

In our code we were stripping annotations from renderings within
`toTextStream` but we must remove the annotations before calling
`layoutPretty` to get the proper handling of whitespace with
indentations. That's what this PR does.
2023-05-19 11:41:28 +02:00
Jan Mas Rovira
a164083b70
Modify open import syntax (#2098) 2023-05-17 11:08:48 +02:00