* 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.
- 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
`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>
