Add builtin integer type to the surface language

[paulcadman]

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 Add an integer (Int) type in the surface language #1679
• Closes Negative number literals should not be typed as Nat #1984

[lukaszcz]

In the REPL:

Stdlib.Prelude> :type div 4 -2
Nat

The operations on Nats can somehow be used with integers. It shouldn't be possible or the result should have type Int.

[paulcadman]

In the REPL:

Stdlib.Prelude> :type div 4 -2
Nat

The operations on Nats can somehow be used with integers. It shouldn't be possible or the result should have type Int.

Thanks for catching this. I've now fixed it and added a negative type checking test.

The REPL now reports:

Stdlib.Prelude> div 1 -2
/<repl>:1:8-9: error:
The expression -2 has type:
  Int
but is expected to have type:
  Nat

[lukaszcz]

In the REPL:

Stdlib.Prelude> :type div 4 -2
Nat

The operations on Nats can somehow be used with integers. It shouldn't be possible or the result should have type Int.

Thanks for catching this. I've now fixed it and added a negative type checking test.

The REPL now reports:

Stdlib.Prelude> div 1 -2
/<repl>:1:8-9: error:
The expression -2 has type:
  Int
but is expected to have type:
  Nat

This doesn't solve the problem completely:

Stdlib.Prelude> let f : String -> Nat := \{_ := 0} in f 2
0

Should give an error that 2 is expected to have type String. I guess one also needs to check if the inferred type is actually a subtype of the hint type in src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs:626.

[paulcadman]

This doesn't solve the problem completely:

Stdlib.Prelude> let f : String -> Nat := \{_ := 0} in f 2
0

Should give an error that 2 is expected to have type String. I guess one also needs to check if the inferred type is actually a subtype of the hint type in src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs:626.

Thank you - I've tried to solve the problem again.