1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-13 19:49:20 +03:00
Commit Graph

1282 Commits

Author SHA1 Message Date
Paul Cadman
fa4c92c7a5
Propogate formatter results when traversing subdirs (#2207)
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.
2023-06-19 18:42:28 +01:00
Paul Cadman
7840f9fa79
Always print source of formatted file unless --check is specified (#2205)
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
2023-06-19 15:14:59 +01:00
Łukasz Czajka
dd16274a24
Restrict permutative conversions on cases to non-booleans (#2201)
* 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.
2023-06-19 11:57:12 +02:00
Łukasz Czajka
f421e87963
Update to the new version of VampIR (#2138)
* Closes #2131 

It remains to update the VampIR version in the CI.
2023-06-16 16:34:58 +01:00
Jonathan Cubides
812edea6a8
Update vamp-ir CI installation (#2199)
- Leveraging https://github.com/anoma/vamp-ir/pull/108
2023-06-16 14:29:31 +01:00
Łukasz Czajka
a3a2454733
More tests for the VampIR compilation pipeline (#2197) 2023-06-16 12:58:37 +02:00
Paul Cadman
82a6f8c891
Fix runtime C maybe benchmark example (#2195)
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.
2023-06-16 09:54:13 +01:00
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