mirror of
https://github.com/anoma/juvix.git
synced 2025-01-08 08:39:26 +03:00
ea09ec3068
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>
|
||
|---|---|---|
| .. | ||
| out | ||
| test001.juvix | ||
| test002.juvix | ||
| test003.juvix | ||
| test004.juvix | ||
| test005.juvix | ||
| test006.juvix | ||
| test007.juvix | ||
| test008.juvix | ||
| test009.juvix | ||
| test010.juvix | ||
| test011.juvix | ||
| test012.juvix | ||
| test013.juvix | ||
| test014.juvix | ||
| test015.juvix | ||
| test016.juvix | ||
| test017.juvix | ||
| test018.juvix | ||
| test019.juvix | ||
| test020.juvix | ||
| test021.juvix | ||
| test022.juvix | ||
| test023.juvix | ||
| test024.juvix | ||
| test025.juvix | ||
| test026.juvix | ||
| test027.juvix | ||
| test028.juvix | ||
| test029.juvix | ||
| test030.juvix | ||
| test031.juvix | ||
| test032.juvix | ||
| test033.juvix | ||
| test034.juvix | ||
| test035.juvix | ||
| test036.juvix | ||
| test037.juvix | ||
| test038.juvix | ||
| test039.juvix | ||
| test040.juvix | ||
| test041.juvix | ||
| test042.juvix | ||
| test043.juvix | ||
| test044.juvix | ||
| test045.juvix | ||
| test046.juvix | ||
| test047.juvix | ||
| test048.juvix | ||
| test049.juvix | ||
| test050.juvix | ||