Simplifies arithmetic expressions in the Core optimization phase,
changing e.g. `(x - 1) + 1` to `x`. Such expressions appear as a result
of compiling pattern matching on natural numbers.
* Closes#2154
* Evaluates closed applications with value arguments when the result
type is zero-order. For example, `3 + 4` is evaluated to `7`, and `id 3`
is evaluated to `3`, but `id id` is not evaluated because the target
type is not zero-order (it's a function type).
* 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";
```
* Introduces the `inline: case` pragma which causes an identifier to be
inlined if it is matched on. This is necessary to support GEB without
compromising optimization for other targets.
* Adapts to the new commits in
https://github.com/anoma/juvix-stdlib/pull/86
* Adapts to https://github.com/anoma/juvix-stdlib/pull/86
* Adds a pass in `toEvalTransformations` to automatically inline all
record projection functions, regardless of the optimization level. This
is necessary to ensure that arithmetic operations and comparisons on
`Nat` or `Int` are always represented directly with the corresponding
built-in Core functions. This is generally highly desirable and required
for the Geb target.
* Adds the `inline: always` pragma which indicates that a function
should always be inlined during the mandatory inlining phase, regardless
of optimization level.
* Closes#2416
* Closes#2401
* Avoids generating identical specialisations by keeping a
specialisation signature for each specialised function application.
* Allows to specialise on a per-trait or per-instance basis:
```
{-# specialize: true #-}
trait
type Natural N := mkNatural {
+ : N -> N -> N;
* : N -> N -> N;
fromNat : Nat -> N;
};
```
or
```
{-# specialize: true #-}
instance
naturalNatI : Natural Nat := ...
```
* The above `specialize: bool` pragma actually works with any type or
function. To be able to simultaneously specify the boolean
specialisation flag and specialisation arguments, one can use
`specialize-args: [arg1, .., argn]` which works like `specialize: [arg1,
.., argn]`.
Adds a Partial trait to the standard library, similar to the one in
PureScript:
https://book.purescript.org/chapter6.html#nullary-type-classes
This enables using partial functions in an encapsulated manner and
without depending on the Debug module.
Adds a trait:
```
trait
type Partial := mkPartial {
fail : {A : Type} -> String -> A
};
runPartial {A} (f : {{Partial}} -> A) : A := f {{mkPartial Debug.failwith}};
```
* Closes#2280
* Record creation syntax uses normal function definition syntax like at
the top-level or in lets.
* It is now allowed to omit the result type annotation in function
definitions (the `: ResultType` part) with `_` inserted by default. This
is allowed only for simple definitions of the form `x := value` in lets
and record creation, but not at the top level.
- Closes#2330
- Closes#2329
This pr implements the syntax changes described in #2330. It drops
support for the old yaml-based syntax.
Some valid examples:
```
syntax iterator for {init := 1; range := 1};
syntax fixity cons := binary {assoc := right};
syntax fixity cmp := binary;
syntax fixity cmp := binary {}; -- debatable whether we want to accept empty {} or not. I think we should
```
# Future work
This pr creates an asymmetry between iterators and operators
definitions. Iterators definition do not require a constructor. We could
add it to make it homogeneous, but it looks a bit redundant:
```
syntax iterator for := mkIterator {init := 1; range := 1};
```
We could consider merging iterator and fixity declarations with this
alternative syntax.
```
syntax XXX for := iterator {init := 1; range := 1};
syntax XXX cons := binary {assoc := right};
```
where `XXX` is a common keyword. Suggestion by @lukaszcz XXX = declare
---------
Co-authored-by: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
* 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#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.
- Closes#2060
- Closes#2189
- This pr adds support for the syntax described in #2189. It does not
drop support for the old syntax.
It is possible to automatically translate juvix files to the new syntax
by using the formatter with the `--new-function-syntax` flag. E.g.
```
juvix format --in-place --new-function-syntax
```
# Syntax changes
Type signatures follow this pattern:
```
f (a1 : Expr) .. (an : Expr) : Expr
```
where each `ai` is a non-empty list of symbols. Braces are used instead
of parentheses when the argument is implicit.
Then, we have these variants:
1. Simple body. After the signature we have `:= Expr;`.
2. Clauses. The function signature is followed by a non-empty sequence
of clauses. Each clause has the form:
```
| atomPat .. atomPat := Expr
```
# Mutual recursion
Now identifiers **do not need to be defined before they are used**,
making it possible to define mutually recursive functions/types without
any special syntax.
There are some exceptions to this. We cannot forward reference a symbol
`f` in some statement `s` if between `s` and the definition of `f` there
is one of the following statements:
1. Local module
2. Import statement
3. Open statement
I think it should be possible to drop the restriction for local modules
and import statements
- Depends on #2219
- Closes#1643
This pr introduces a `list` as a new builtin so that we can use syntax
sugar both in expressions and patterns. E.g. it is now possible to write
`[1; 2; 3;]`.
* Fixes the indices in `inline` and `specialize` for local lambda-lifted
identifiers.
* Adds the `specialize-by` pragma which allows to specialize a local
function by some of its free variables, or specialize arguments by name.
For example:
```
funa : {A : Type} -> (A -> A) -> A -> A;
funa {A} f a :=
let
{-# specialize-by: [f] #-}
go : Nat -> A;
go zero := a;
go (suc n) := f (go n);
in go 10;
```
If `funa` is inlined, then `go` will be specialized by the actual
argument substituted for `f`.
* 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));
```
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#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.
* Closes#1989
* Adds optimization phases to the pipline (specified by
`opt-phase-eval`, `opt-phase-exec` and `opt-phase-geb` transformations).
* Adds the `-O` option to the `compile` command to specify the
optimization level.
* Functions can be declared for inlining with the `inline` pragma:
```
{-# inline: true #-}
const : {A B : Type} -> A -> B -> A;
const x _ := x;
```
By default, the function is inlined only if it's fully applied. One can
specify that a function (partially) applied to at least `n` explicit
arguments should be inlined.
```
{-# inline: 2 #-}
compose : {A B C : Type} -> (B -> C) -> (A -> B) -> A -> C;
compose f g x := f (g x);
```
Then `compose f g` will be inlined, even though it's not fully applied.
But `compose f` won't be inlined.
* Non-recursive fully applied functions are automatically inlined if the
height of the body term does not exceed the inlining depth limit, which
can be specified with the `--inline` option to the `compile` command.
* The pragma `inline: false` disables automatic inlining on a
per-function basis.
- Closes#2039
- Closes#2055
- Depends on #2053
Changes in this pr:
- Local modules are removed (flattened) in the translation abstract ->
internal.
- In the translation abstract -> internal we group definitions in
mutually recursive blocks. These blocks can contain function definitions
and type definitions. Previously we only handled functions.
- The translation of Internal has been enhanced to handle these mutually
recursive blocks.
- Some improvements the pretty printer for internal (e.g. we now print
builtin tags properly).
- A "hack" that puts the builtin bool definition at the beginning of a
module if present. This was the easiest way to handle the implicit
dependency of the builtin stringToNat with bool in the internal-to-core
translation.
- A moderately sized test defining a simple lambda calculus involving
and an evaluator for it. This example showcases mutually recursive types
in juvix.
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
- Closes#2006
During lambda lifting, we now substitute the calls to the lifted
functions before recursively applying lambda lifting. This will slightly
increase the amount of captured variables. However, I think this is the
only way since we need all identifiers to have a type when recursing.
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>
This implements a basic version of the algorithm from: Luc Maranget,
[Compiling pattern matching to good decision
trees](http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf). No
heuristics are used - the first column is always chosen.
* Closes#1798
* Closes#1225
* Closes#1926
* Adds a global `--no-coverage` option which turns off coverage checking
in favour of generating runtime failures
* Changes the representation of Match patterns in JuvixCore to achieve a
more streamlined implementation
* Adds options to the Core pipeline
