* Closes#2392
Changes checklist
-----------------
* [X] Abstract out data types for stored module representation
(`ModuleInfo` in `Juvix.Compiler.Store.Language`)
* [X] Adapt the parser to operate per-module
* [X] Adapt the scoper to operate per-module
* [X] Adapt the arity checker to operate per-module
* [X] Adapt the type checker to operate per-module
* [x] Adapt Core transformations to operate per-module
* [X] Adapt the pipeline functions in `Juvix.Compiler.Pipeline`
* [X] Add `Juvix.Compiler.Pipeline.Driver` which drives the per-module
compilation process
* [x] Implement module saving / loading in `Pipeline.Driver`
* [x] Detect cyclic module dependencies in `Pipeline.Driver`
* [x] Cache visited modules in memory in `Pipeline.Driver` to avoid
excessive disk operations and repeated hash re-computations
* [x] Recompile a module if one of its dependencies needs recompilation
and contains functions that are always inlined.
* [x] Fix identifier dependencies for mutual block creation in
`Internal.fromConcrete`
- Fixed by making textually later definitions depend on earlier ones.
- Now instances are used for resolution only after the textual point of
their definition.
- Similarly, type synonyms will be unfolded only after the textual point
of their definition.
* [x] Fix CLI
* [x] Fix REPL
* [x] Fix highlighting
* [x] Fix HTML generation
* [x] Adapt test suite
This patch dramatically increases the efficiency of `juvix dev root`,
which was unnecessarily parsing all dependencies included in the
`Package.juvix` file. Other commands that do not require the `Package`
will also be faster.
It also refactors some functions so that the `TaggedLock` effect is run
globally.
I've added `singletons-base` as a dependency so we can have `++` on the
type level. We've tried to define a type family ourselves but inference
was not working properly.
This PR fixes our positivity checker to support inductive definitions
with type families as type parameters. This kind of ind. type is
type-checked using the global flag `--new-type checker.`
For example, the following definition is not allowed:
```
module Evil;
type Evil (f : Type -> Type) :=
magic : f (Evil f) -> Evil f;
```
- Closes#2540
## Overview
This PR makes the compiler pipeline thread-safe so that the test suite
can be run in parallel.
This is achieved by:
* Removing use of `{get, set, with}CurrentDir` functions.
* Adding locking around shared file resources like the the
global-project and internal build directory.
NB: **Locking is disabled for the main compiler target**, as it is
single threaded they are not required.
## Run test suite in parallel
To run the test suite in parallel you must add `--ta '+RTS -N -RTS'` to
your stack test arguments. For example:
```
stack test --fast --ta '+RTS -N -RTS'
```
The `-N` instructs the Haskell runtime to choose the number of threads
to use based on how many processors there are on your machine. You can
use `-Nn` to see the number of threads to `n`.
These flags are already [set in the
Makefile](e6dca22cfd/Makefile (L26))
when you or CI uses `stack test`.
## Locking
The Haskell package
[filelock](https://hackage.haskell.org/package/filelock) is used for
locking. File locks are used instead of MVars because Juvix code does
not control when new threads are created, they are created by the test
suite. This means that MVars created by Juvix code will have no effect,
because they are created independently on each test-suite thread.
Additionally the resources we're locking live on the filesystem and so
can be conveniently tagged by path.
### FileLock
The filelock library is wrapped in a FileLock effect:
e6dca22cfd/src/Juvix/Data/Effect/FileLock/Base.hs (L6-L8)
There is an [IO
interpreter](e6dca22cfd/src/Juvix/Data/Effect/FileLock/IO.hs (L8))
that uses filelock and an [no-op
interpreter](e6dca22cfd/src/Juvix/Data/Effect/FileLock/Permissive.hs (L7))
that just runs actions unconditionally.
### TaggedLock
To make the file locks simpler to use a TaggedLock effect is introduced:
e6dca22cfd/src/Juvix/Data/Effect/TaggedLock/Base.hs (L5-L11)
And convenience function:
e6dca22cfd/src/Juvix/Data/Effect/TaggedLock.hs (L28)
This allows an action to be locked, tagged by a directory that may or
may not exist. For example in the following code, an action is performed
on a directory `root` that may delete the directory before repopulating
the files. So the lockfile cannot be stored in the `root` itself.
e6dca22cfd/src/Juvix/Extra/Files.hs (L55-L60)
## Pipeline
As noted above, we only use locking in the test suite. The main app
target pipeline is single threaded and so locking is unnecessary. So the
interpretation of locks is parameterised so that locking can be disabled
e6dca22cfd/src/Juvix/Compiler/Pipeline/Run.hs (L64)
* Closes#2453
* Closes#2432
* Any nonnegative literal `n` is replaced with `fromNat {_} {{_}} n`
where `fromNat` is the builtin conversion function defined in the
`Natural` trait in `Stdlib.Trait.Natural`.
* Any negative literal `-n` is replaced with `fromInt {_} {{_}} -n`
where `fromInt` is the builtin conversion function defined in the
`Integral` trait in `Stdlib.Trait.Integral`.
* Before resolving instance holes, it is checked whether the type holes
introduced for `fromNat` and `fromInt` have been inferred. If not, an
attempt is made to unify them with `Nat` or `Int`. This allows to
type-check e.g. `1 == 1` (there is no hint in the context as to what the
type of `1` should be, so it is decided to be `Nat` after inferring the
hole fails).
* Closes#2426
A coercion from trait `T` to `T'` can be declared with the syntax
```
coercion instance
coeName {A} {{T A}} : T' A := ...
```
Coercions can be seen as instances with special resolution rules.
Coercion resolution rules
-------------------------
* If a non-coercion instance can be applied in a single instance
resolution step, no coercions are considered. No ambiguity results if
there exists some coercion which could be applied, but a non-coercion
instance exists - the non-coercion instances have priority.
* If no non-coercion instance can be applied in a single resolution
step, all minimal coercion paths which lead to an applicable
non-coercion instance are considered. If there is more than one,
ambiguity is reported.
Examples
----------
The following type-checks because:
1. There is no non-coercion instance found for `U String`.
2. There are two minimal coercion paths `U` <- `U1` and `U` <- `U2`, but
only one of them (`U` <- `U2`) ends in an applicable non-coercion
instance (`instU2` for `U2 String`).
```
trait
type U A := mkU {pp : A -> A};
trait
type U1 A := mkU1 {pp : A -> A};
trait
type U2 A := mkU2 {pp : A -> A};
coercion instance
fromU1toU {A} {{U1 A}} : U A :=
mkU@{
pp := U1.pp
};
coercion instance
fromU2toU {A} {{U2 A}} : U A :=
mkU@{
pp := U2.pp
};
instance
instU2 : U2 String := mkU2 id;
main : IO := printStringLn (U.pp "X")
```
The following results in an ambiguity error because:
1. There is no non-coercion instance found for `T Unit`.
2. There are two minimal coercion paths `T` <- `T1` and `T` <- `T2`,
both of which end in applicable non-coercion instances.
```
trait
type T A := mkT { pp : A → A };
trait
type T1 A := mkT1 { pp : A → A };
trait
type T2 A := mkT2 { pp : A → A };
instance
unitT1 : T1 Unit := mkT1 (pp := λ{_ := unit});
instance
unitT2 : T2 Unit := mkT2 (pp := λ{_ := unit});
coercion instance
fromT1toT {A} {{T1 A}} : T A := mkT@{
pp := T1.pp
};
coercion instance
fromT2toT {A} {{T2 A}} : T A := mkT@{
pp := T2.pp
};
main : Unit := T.pp unit;
```
The following type-checks, because there exists a non-coercion instance
for `T2 String`, so the coercion `fromT1toT2` is ignored during instance
resolution.
```
trait
type T1 A := mkT1 {pp : A -> A};
trait
type T2 A := mkT2 {pp : A -> A};
instance
instT1 {A} : T1 A :=
mkT1@{
pp := id
};
coercion instance
fromT1toT2 {A} {{M : T1 A}} : T2 A :=
mkT2@{
pp := T1.pp {{M}}
};
instance
instT2 : T2 String :=
mkT2@{
pp (s : String) : String := s ++str "!"
};
main : String := T2.pp "a";
```
This PR removes the CaseBranchImplicit error from the scoper. This error
is already handled in the arity/typechecker with a good error message:
The arity checker error message for
```
case b of {
| {{true}} := false
```
is
```
Expected an explicit pattern but found an implicit instance pattern: {{true}}
```
* Closes https://github.com/anoma/juvix/issues/2356
* 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.
This PR adds a builtin integer type to the surface language that is
compiled to the backend integer type.
## Inductive definition
The `Int` type is defined in the standard library as:
```
builtin int
type Int :=
| --- ofNat n represents the integer n
ofNat : Nat -> Int
| --- negSuc n represents the integer -(n + 1)
negSuc : Nat -> Int;
```
## New builtin functions defined in the standard library
```
intToString : Int -> String;
+ : Int -> Int -> Int;
neg : Int -> Int;
* : Int -> Int -> Int;
- : Int -> Int -> Int;
div : Int -> Int -> Int;
mod : Int -> Int -> Int;
== : Int -> Int -> Bool;
<= : Int -> Int -> Bool;
< : Int -> Int -> Bool;
```
Additional builtins required in the definition of the other builtins:
```
negNat : Nat -> Int;
intSubNat : Nat -> Nat -> Int;
nonNeg : Int -> Bool;
```
## REPL types of literals
In the REPL, non-negative integer literals have the inferred type `Nat`,
negative integer literals have the inferred type `Int`.
```
Stdlib.Prelude> :t 1
Nat
Stdlib.Prelude> :t -1
Int
:t let x : Int := 1 in x
Int
```
## The standard library Prelude
The definitions of `*`, `+`, `div` and `mod` are not exported from the
standard library prelude as these would conflict with the definitions
from `Stdlib.Data.Nat`.
Stdlib.Prelude
```
open import Stdlib.Data.Int hiding {+;*;div;mod} public;
```
* Closes https://github.com/anoma/juvix/issues/1679
* Closes https://github.com/anoma/juvix/issues/1984
---------
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
Previously we were:
* discarding the types table
* discarding the name ids state
after processing an expression in the REPL.
For example evaluating:
```
let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10
```
would loop in the REPL.
We noticed that the `n` in `suc n` was being given type `Type` instead
of `Nat`. This was because the name id given to n was incorrect, the
REPL started using name ids from 0 again.
We fixed this issue by storing information, including the types table
and name ids state in the Artifacts data structure that is returned when
we run the pipeline for the first time. This information is then used
when we call functions to compile / type check REPL expressions.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
