This pr simplifies parsing by removing `FunctionParameterUnnamed`. It
also removes ghost wildcards introduced during parsing.
It also introduces an error for double braced atoms `{{x}}` that are not
on the left of an arrow `->`
* Closes#1646
Implements a basic trait framework. A simple instance search mechanism
is included which fails if there is more than one matching instance at
any step.
Example usage:
```
import Stdlib.Prelude open hiding {Show; mkShow; show};
trait
type Show A :=
mkShow {
show : A → String
};
instance
showStringI : Show String := mkShow (show := id);
instance
showBoolI : Show Bool := mkShow (show := λ{x := if x "true" "false"});
instance
showNatI : Show Nat := mkShow (show := natToString);
showList {A} : {{Show A}} → List A → String
| nil := "nil"
| (h :: t) := Show.show h ++str " :: " ++str showList t;
instance
showListI {A} {{Show A}} : Show (List A) := mkShow (show := showList);
showMaybe {A} {{Show A}} : Maybe A → String
| (just x) := "just (" ++str Show.show x ++str ")"
| nothing := "nothing";
instance
showMaybeI {A} {{Show A}} : Show (Maybe A) := mkShow (show := showMaybe);
main : IO :=
printStringLn (Show.show true) >>
printStringLn (Show.show false) >>
printStringLn (Show.show 3) >>
printStringLn (Show.show [true; false]) >>
printStringLn (Show.show [1; 2; 3]) >>
printStringLn (Show.show [1; 2]) >>
printStringLn (Show.show [true; false]) >>
printStringLn (Show.show [just true; nothing; just false]) >>
printStringLn (Show.show [just [1]; nothing; just [2; 3]]) >>
printStringLn (Show.show "abba") >>
printStringLn (Show.show ["a"; "b"; "c"; "d"]);
```
It is possible to manually provide an instance and to match on implicit
instances:
```
f {A} : {{Show A}} -> A -> String
| {{mkShow s}} x -> s x;
f' {A} : {{Show A}} → A → String
| {{M}} x := Show.show {{M}} x;
```
The trait parameters in instance types are checked to be structurally
decreasing to avoid looping in the instance search. So the following is
rejected:
```
type Box A := box A;
trait
type T A := mkT { pp : A → A };
instance
boxT {A} : {{T (Box A)}} → T (Box A) := mkT (λ{x := x});
```
We check whether each parameter is a strict subterm of some trait
parameter in the target. This ordering is included in the finite
multiset extension of the subterm ordering, hence terminating.
- Closes#2331.
The rules implemented in this pr are as follows.
1. If a type definition has only one constructor, no pipe is added. The
constructor is printed in the same line if it fits.
2. If a constructor is a record with a single field, the field is
printed in the same line if it fits. If the constructor has multiple
fields, they are printed aligned and indented after a line break.
Examples:
```
type T := constructT : T;
type T-wrapper := mkWrapper {unwrap : T};
type EnumRecord :=
| --- doc for C1
C1 {
c1a : T;
c1b : T
}
| C2 {
c2a : T;
c2b : T
};
```
This PR introduces a global `--offline` flag.
## Doctor
This replaces the `--offline` flag on the doctor command.
## Juvix package builds
The flag applies to juvix build commands like `juvix compile`, `juvix
repl`. This is so that users can continue to build packages offline that
have external dependencies when there's no network connection (as long
as they built the same package online previously).
Specifically, when the `--offline` flag is used in a package that has
external git dependencies.
* No `git clone` or `git fetch` commands are used
* `git checkout` will continue to be used
* Clones from previous builds are reused
This means that you can update the `ref` field in a git dependency, as
long as the ref existed the last time that the project was built without
the `--offline` flag.
* Closes https://github.com/anoma/juvix/issues/2333
This PR adds external git dependency support to the Juvix package
format.
## New dependency Git item
You can now add a `git` block to the dependencies list:
```yaml
name: HelloWorld
main: HelloWorld.juvix
dependencies:
- .juvix-build/stdlib
- git:
url: https://my.git.repo
name: myGitRepo
ref: main
version: 0.1.0
```
Git block required fields:
* `url`: The URL of the git repository
* `ref`: The git reference that should be checked out
* `name`: The name for the dependency. This is used to name the
directory of the clone, it is required. Perhaps we could come up with a
way to automatically name the clone directory. Current ideas are to
somehow encode the URL / ref combination or use a UUID. However there's
some value in having the clone directory named in a friendly way.
NB:
* The values of the `name` fields must be unique among the git blocks in
the dependencies list.
## Behaviour
When dependencies for a package are registered, at the beginning of the
compiler pipeline, all remote dependencies are processed:
1. If it doesn't already exist, the remote dependency is cloned to
`.juvix-build/deps/$name`
2. `git fetch` is run in the clone
3. `git checkout` at the specified `ref` is run in the clone
The clone is then processed by the PathResolver in the same way as path
dependencies.
NB:
* Remote dependencies of transitive dependencies are also processed.
* The `git fetch` step is required for the case where the remote is
updated. In this case we want the user to be able to update the `ref`
field.
## Errors
1. Missing fields in the Git dependency block are YAML parse errors
2. Duplicate `name` values in the dependencies list is an error thrown
when the package file is processed
3. The `ref` doesn't exist in the clone or the clone directory is
otherwise corrupt. An error with a suggestion to `juvix clean` is given.
The package file path is used as the location in the error message.
4. Other `git` command errors (command not found, etc.), a more verbose
error is given with the arguments that were passed to the git command.
## Future work
1. Add an offline mode
2. Add a lock file mechanism that resolves branch/tag git refs to commit
hashes
* closes https://github.com/anoma/juvix/issues/2083
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- Closes#2293.
- Closes#2319
I've added an effect for termination. It keeps track of which functions
failed the termination checker, which is run just after translating to
Internal. During typechecking, non-terminating functions are not
normalized. After typechecking, if there is at least one function which
failed the termination checker, an error is reported.
Additionally, we now properly check for termination of functions defined
in a let expression in the repl.
- 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.
Avoid excessive backtracking in iterator and named arguments parsing.
This also improves error messages by committing to a parsing branch as
early as possible.
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
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
- 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;
```
