1
1
mirror of https://github.com/anoma/juvix.git synced 2025-01-08 16:51:53 +03:00
Commit Graph

9 Commits

Author SHA1 Message Date
janmasrovira
5de0026d83
Add juvix global project under xdg directory and other improvements (#1963)
Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-04-13 11:27:39 +02:00
Paul Cadman
ea09ec3068
Add builtin integer type to the surface language (#1948)
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>
2023-04-13 08:16:49 +01:00
janmasrovira
90a7a5e7e0
Fix REPL state to include enough information to rerun the pipeline (#1911)
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>
2023-03-30 13:39:27 +02:00
janmasrovira
0193a33d4c
Fix inference loop (#1726) 2023-01-17 13:28:38 +01:00
janmasrovira
f7205915a5
Typecheck let expressions (#1712) 2023-01-17 09:41:07 +01:00
janmasrovira
3b452e7d76
Fix #1693 (#1708) 2023-01-09 18:56:28 +01:00
janmasrovira
af63c36574
Support basic dependencies (#1622) 2022-12-20 13:05:40 +01:00
Paul Cadman
a3b2aa6940
Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
janmasrovira
41ef5f6219
Add lambda expressions to internal and add typechecking support (#1538) 2022-09-23 15:43:18 +02:00