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>
2025-01-05 22:46:08 +03:00 · 2023-04-13 08:16:49 +01:00 · 2023-04-13 08:16:49 +01:00 · ea09ec3068
commit ea09ec3068
parent 34b0969141
36 changed files with 1186 additions and 137 deletions
--- a/2
+++ b/2
@ -1 +1 @@
-Subproject commit dd5fa12156468a97deb96228b2c754fadef5ce92
+Subproject commit ce3623ffb0e8a0aa6c79cbb9a08eb14de5aef27f
--- a/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs
+++ b/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs
@ -78,6 +78,7 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
    go = \case
      BuiltinNat -> addInductiveStartNode
      BuiltinBool -> addInductiveStartNode
+      BuiltinInt -> addInductiveStartNode

    addInductiveStartNode :: Sem r ()
    addInductiveStartNode = addStartNode (i ^. inductiveName)
--- a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs
@ -268,6 +268,7 @@ registerBuiltinInductive ::
 registerBuiltinInductive d = \case
  BuiltinNat -> registerNatDef d
  BuiltinBool -> registerBoolDef d
+  BuiltinInt -> registerIntDef d

 registerBuiltinFunction ::
  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) =>
@ -287,6 +288,18 @@ registerBuiltinFunction d = \case
  BuiltinBoolIf -> registerIf d
  BuiltinBoolOr -> registerOr d
  BuiltinBoolAnd -> registerAnd d
+  BuiltinIntEq -> registerIntEq d
+  BuiltinIntSubNat -> registerIntSubNat d
+  BuiltinIntPlus -> registerIntPlus d
+  BuiltinIntNegNat -> registerIntNegNat d
+  BuiltinIntNeg -> registerIntNeg d
+  BuiltinIntMul -> registerIntMul d
+  BuiltinIntDiv -> registerIntDiv d
+  BuiltinIntMod -> registerIntMod d
+  BuiltinIntSub -> registerIntSub d
+  BuiltinIntNonNeg -> registerIntNonNeg d
+  BuiltinIntLe -> registerIntLe d
+  BuiltinIntLt -> registerIntLt d

 registerBuiltinAxiom ::
  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) =>
@ -307,6 +320,8 @@ registerBuiltinAxiom d = \case
  BuiltinBoolPrint -> registerBoolPrint d
  BuiltinTrace -> registerTrace d
  BuiltinFail -> registerFail d
+  BuiltinIntToString -> registerIntToString d
+  BuiltinIntPrint -> registerIntPrint d

 goInductive ::
  (Members '[InfoTableBuilder, Builtins, Error ScoperError] r) =>
--- a/src/Juvix/Compiler/Builtins.hs
+++ b/src/Juvix/Compiler/Builtins.hs
@ -2,6 +2,7 @@ module Juvix.Compiler.Builtins
  ( module Juvix.Compiler.Builtins.Effect,
    module Juvix.Compiler.Builtins.Nat,
    module Juvix.Compiler.Builtins.IO,
+    module Juvix.Compiler.Builtins.Int,
    module Juvix.Compiler.Builtins.Bool,
    module Juvix.Compiler.Builtins.String,
    module Juvix.Compiler.Builtins.Debug,
@ -12,5 +13,6 @@ import Juvix.Compiler.Builtins.Bool
 import Juvix.Compiler.Builtins.Debug
 import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Builtins.IO
+import Juvix.Compiler.Builtins.Int
 import Juvix.Compiler.Builtins.Nat
 import Juvix.Compiler.Builtins.String
--- a/src/Juvix/Compiler/Builtins/Int.hs
+++ b/src/Juvix/Compiler/Builtins/Int.hs
@ -0,0 +1,390 @@
+module Juvix.Compiler.Builtins.Int where
+
+import Juvix.Compiler.Abstract.Extra
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Prelude
+
+registerIntDef :: Member Builtins r => InductiveDef -> Sem r ()
+registerIntDef d = do
+  unless (null (d ^. inductiveParameters)) (error "Int should have no type parameters")
+  unless (isSmallUniverse' (d ^. inductiveType)) (error "Int should be in the small universe")
+  registerBuiltin BuiltinInt (d ^. inductiveName)
+  case d ^. inductiveConstructors of
+    [c1, c2] -> registerIntCtor BuiltinIntOfNat c1 >> registerIntCtor BuiltinIntNegSuc c2
+    _ -> error "Int should have exactly two constructors"
+
+registerIntCtor :: (Member Builtins r) => BuiltinConstructor -> InductiveConstructorDef -> Sem r ()
+registerIntCtor ctor d@InductiveConstructorDef {..} = do
+  let ctorName = _constructorName
+      ty = _constructorType
+      loc = getLoc d
+  int <- getBuiltinName loc BuiltinInt
+  nat <- getBuiltinName loc BuiltinNat
+  unless (ty === (nat --> int)) (error (ctorName ^. nameText <> " has the wrong type"))
+  registerBuiltin ctor ctorName
+
+registerIntToString :: Member Builtins r => AxiomDef -> Sem r ()
+registerIntToString f = do
+  string_ <- getBuiltinName (getLoc f) BuiltinString
+  int <- getBuiltinName (getLoc f) BuiltinInt
+  unless (f ^. axiomType === (int --> string_)) (error "intToString has the wrong type signature")
+  registerBuiltin BuiltinIntToString (f ^. axiomName)
+
+registerIntEq :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntEq f = do
+  int <- builtinName BuiltinInt
+  ofNat <- toExpression <$> builtinName BuiltinIntOfNat
+  negSuc <- toExpression <$> builtinName BuiltinIntNegSuc
+  tybool <- builtinName BuiltinBool
+  false <- toExpression <$> builtinName BuiltinBoolFalse
+  natEq <- toExpression <$> builtinName BuiltinNatEq
+  varm <- freshVar "m"
+  varn <- freshVar "n"
+  h1 <- freshHole
+  h2 <- freshHole
+  let eq = f ^. funDefName
+      m = toExpression varm
+      n = toExpression varn
+      (.==.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+      x .==. y = eq @@ x @@ y
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ ((ofNat @@ m) .==. (ofNat @@ n), (natEq @@ m @@ n)),
+          ((negSuc @@ m) .==. (negSuc @@ n), (natEq @@ m @@ n)),
+          (h1 .==. h2, false)
+        ]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntEq,
+        _funInfoSignature = int --> int --> tybool,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varn, varm],
+        _funInfoFreeTypeVars = []
+      }
+  where
+    builtinName :: IsBuiltin a => a -> Sem r Name
+    builtinName = getBuiltinName (getLoc f)
+
+registerIntSubNat :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntSubNat f = do
+  let loc = getLoc f
+  int <- getBuiltinName loc BuiltinInt
+  nat <- getBuiltinName loc BuiltinNat
+  unless (f ^. funDefTypeSig === (nat --> nat --> int)) (error "int-sub-nat has the wrong type signature")
+  registerBuiltin BuiltinIntSubNat (f ^. funDefName)
+
+registerIntPlus :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntPlus f = do
+  let loc = getLoc f
+  int <- getBuiltinName loc BuiltinInt
+  ofNat <- toExpression <$> getBuiltinName loc BuiltinIntOfNat
+  negSuc <- toExpression <$> getBuiltinName loc BuiltinIntNegSuc
+  suc <- toExpression <$> getBuiltinName loc BuiltinNatSuc
+  natPlus <- toExpression <$> getBuiltinName loc BuiltinNatPlus
+  intSubNat <- toExpression <$> getBuiltinName loc BuiltinIntSubNat
+  let plus = f ^. funDefName
+  varn <- freshVar "m"
+  varm <- freshVar "n"
+  let m = toExpression varm
+      n = toExpression varn
+      (.+.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+      x .+. y = plus @@ x @@ y
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ ((ofNat @@ m) .+. (ofNat @@ n), ofNat @@ (natPlus @@ m @@ n)),
+          ((ofNat @@ m) .+. (negSuc @@ n), intSubNat @@ m @@ (suc @@ n)),
+          ((negSuc @@ m) .+. (ofNat @@ n), intSubNat @@ n @@ (suc @@ m)),
+          ((negSuc @@ m) .+. (negSuc @@ n), negSuc @@ (suc @@ (natPlus @@ m @@ n)))
+        ]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntPlus,
+        _funInfoSignature = int --> int --> int,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varm, varn],
+        _funInfoFreeTypeVars = []
+      }
+
+registerIntNegNat :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntNegNat f = do
+  int <- builtinName BuiltinInt
+  nat <- builtinName BuiltinNat
+  ofNat <- toExpression <$> builtinName BuiltinIntOfNat
+  negSuc <- toExpression <$> builtinName BuiltinIntNegSuc
+  zero <- toExpression <$> builtinName BuiltinNatZero
+  suc <- toExpression <$> builtinName BuiltinNatSuc
+  varn <- freshVar "n"
+  let negNat = f ^. funDefName
+      n = toExpression varn
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ (negNat @@ zero, ofNat @@ zero),
+          (negNat @@ (suc @@ n), negSuc @@ n)
+        ]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntNegNat,
+        _funInfoSignature = nat --> int,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varn],
+        _funInfoFreeTypeVars = []
+      }
+  where
+    builtinName :: IsBuiltin a => a -> Sem r Name
+    builtinName = getBuiltinName (getLoc f)
+
+registerIntNeg :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntNeg f = do
+  int <- builtinName BuiltinInt
+  ofNat <- toExpression <$> builtinName BuiltinIntOfNat
+  negSuc <- toExpression <$> builtinName BuiltinIntNegSuc
+  negNat <- toExpression <$> builtinName BuiltinIntNegNat
+  suc <- toExpression <$> builtinName BuiltinNatSuc
+  varn <- freshVar "n"
+  let neg = f ^. funDefName
+      n = toExpression varn
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ (neg @@ (ofNat @@ n), negNat @@ n),
+          (neg @@ (negSuc @@ n), ofNat @@ (suc @@ n))
+        ]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntNeg,
+        _funInfoSignature = int --> int,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varn],
+        _funInfoFreeTypeVars = []
+      }
+  where
+    builtinName :: IsBuiltin a => a -> Sem r Name
+    builtinName = getBuiltinName (getLoc f)
+
+registerIntMul :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntMul f = do
+  int <- builtinName BuiltinInt
+  ofNat <- toExpression <$> builtinName BuiltinIntOfNat
+  negSuc <- toExpression <$> builtinName BuiltinIntNegSuc
+  negNat <- toExpression <$> builtinName BuiltinIntNegNat
+  natMul <- toExpression <$> builtinName BuiltinNatMul
+  natSuc <- toExpression <$> builtinName BuiltinNatSuc
+  varm <- freshVar "m"
+  varn <- freshVar "n"
+  let mul = f ^. funDefName
+      m = toExpression varm
+      n = toExpression varn
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ (mul @@ (ofNat @@ m) @@ (ofNat @@ n), ofNat @@ (natMul @@ m @@ n)),
+          (mul @@ (ofNat @@ m) @@ (negSuc @@ n), negNat @@ (natMul @@ m @@ (natSuc @@ n))),
+          (mul @@ (negSuc @@ m) @@ (ofNat @@ n), negNat @@ (natMul @@ (natSuc @@ m) @@ n)),
+          (mul @@ (negSuc @@ m) @@ (negSuc @@ n), ofNat @@ (natMul @@ (natSuc @@ m) @@ (natSuc @@ n)))
+        ]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntMul,
+        _funInfoSignature = int --> int --> int,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varm, varn],
+        _funInfoFreeTypeVars = []
+      }
+  where
+    builtinName :: IsBuiltin a => a -> Sem r Name
+    builtinName = getBuiltinName (getLoc f)
+
+registerIntDiv :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntDiv f = do
+  int <- builtinName BuiltinInt
+  ofNat <- toExpression <$> builtinName BuiltinIntOfNat
+  negSuc <- toExpression <$> builtinName BuiltinIntNegSuc
+  negNat <- toExpression <$> builtinName BuiltinIntNegNat
+  natDiv <- toExpression <$> builtinName BuiltinNatDiv
+  natSuc <- toExpression <$> builtinName BuiltinNatSuc
+  varm <- freshVar "m"
+  varn <- freshVar "n"
+  let intDiv = f ^. funDefName
+      m = toExpression varm
+      n = toExpression varn
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ (intDiv @@ (ofNat @@ m) @@ (ofNat @@ n), ofNat @@ (natDiv @@ m @@ n)),
+          (intDiv @@ (ofNat @@ m) @@ (negSuc @@ n), negNat @@ (natDiv @@ m @@ (natSuc @@ n))),
+          (intDiv @@ (negSuc @@ m) @@ (ofNat @@ n), negNat @@ (natDiv @@ (natSuc @@ m) @@ n)),
+          (intDiv @@ (negSuc @@ m) @@ (negSuc @@ n), ofNat @@ (natDiv @@ (natSuc @@ m) @@ (natSuc @@ n)))
+        ]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntDiv,
+        _funInfoSignature = int --> int --> int,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varm, varn],
+        _funInfoFreeTypeVars = []
+      }
+  where
+    builtinName :: IsBuiltin a => a -> Sem r Name
+    builtinName = getBuiltinName (getLoc f)
+
+registerIntMod :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntMod f = do
+  int <- builtinName BuiltinInt
+  ofNat <- toExpression <$> builtinName BuiltinIntOfNat
+  negSuc <- toExpression <$> builtinName BuiltinIntNegSuc
+  negNat <- toExpression <$> builtinName BuiltinIntNegNat
+  natMod <- toExpression <$> builtinName BuiltinNatMod
+  natSuc <- toExpression <$> builtinName BuiltinNatSuc
+  varm <- freshVar "m"
+  varn <- freshVar "n"
+  let intMod = f ^. funDefName
+      m = toExpression varm
+      n = toExpression varn
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ (intMod @@ (ofNat @@ m) @@ (ofNat @@ n), ofNat @@ (natMod @@ m @@ n)),
+          (intMod @@ (ofNat @@ m) @@ (negSuc @@ n), ofNat @@ (natMod @@ m @@ (natSuc @@ n))),
+          (intMod @@ (negSuc @@ m) @@ (ofNat @@ n), negNat @@ (natMod @@ (natSuc @@ m) @@ n)),
+          (intMod @@ (negSuc @@ m) @@ (negSuc @@ n), negNat @@ (natMod @@ (natSuc @@ m) @@ (natSuc @@ n)))
+        ]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntMod,
+        _funInfoSignature = int --> int --> int,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varm, varn],
+        _funInfoFreeTypeVars = []
+      }
+  where
+    builtinName :: IsBuiltin a => a -> Sem r Name
+    builtinName = getBuiltinName (getLoc f)
+
+registerIntSub :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntSub f = do
+  int <- builtinName BuiltinInt
+  neg <- toExpression <$> builtinName BuiltinIntNeg
+  intPlus <- toExpression <$> builtinName BuiltinIntPlus
+  varm <- freshVar "m"
+  varn <- freshVar "n"
+  let intSub = f ^. funDefName
+      m = toExpression varm
+      n = toExpression varn
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ (intSub @@ m @@ n, intPlus @@ m @@ (neg @@ n))
+        ]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntSub,
+        _funInfoSignature = int --> int --> int,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varm, varn],
+        _funInfoFreeTypeVars = []
+      }
+  where
+    builtinName :: IsBuiltin a => a -> Sem r Name
+    builtinName = getBuiltinName (getLoc f)
+
+registerIntNonNeg :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntNonNeg f = do
+  int <- builtinName BuiltinInt
+  bool_ <- builtinName BuiltinBool
+  ofNat <- toExpression <$> builtinName BuiltinIntOfNat
+  negSuc <- toExpression <$> builtinName BuiltinIntNegSuc
+  true <- toExpression <$> builtinName BuiltinBoolTrue
+  false <- toExpression <$> builtinName BuiltinBoolFalse
+  varn <- freshVar "n"
+  h <- freshHole
+  let intNonNeg = f ^. funDefName
+      n = toExpression varn
+
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ (intNonNeg @@ (ofNat @@ n), true),
+          (intNonNeg @@ (negSuc @@ h), false)
+        ]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntNonNeg,
+        _funInfoSignature = int --> bool_,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varn],
+        _funInfoFreeTypeVars = []
+      }
+  where
+    builtinName :: IsBuiltin a => a -> Sem r Name
+    builtinName = getBuiltinName (getLoc f)
+
+registerIntPrint :: Members '[Builtins] r => AxiomDef -> Sem r ()
+registerIntPrint f = do
+  int <- getBuiltinName (getLoc f) BuiltinInt
+  io <- getBuiltinName (getLoc f) BuiltinIO
+  unless (f ^. axiomType === (int --> io)) (error "Int print has the wrong type signature")
+  registerBuiltin BuiltinIntPrint (f ^. axiomName)
+
+registerIntLe :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntLe f = do
+  int <- builtinName BuiltinInt
+  bool_ <- builtinName BuiltinBool
+  nonNeg <- toExpression <$> builtinName BuiltinIntNonNeg
+  intSub <- toExpression <$> builtinName BuiltinIntSub
+  varm <- freshVar "m"
+  varn <- freshVar "n"
+  let intLe = f ^. funDefName
+      (.-.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+      x .-. y = intSub @@ x @@ y
+      m = toExpression varm
+      n = toExpression varn
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [(intLe @@ m @@ n, nonNeg @@ (n .-. m))]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntLe,
+        _funInfoSignature = int --> int --> bool_,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varm, varn],
+        _funInfoFreeTypeVars = []
+      }
+  where
+    builtinName :: IsBuiltin a => a -> Sem r Name
+    builtinName = getBuiltinName (getLoc f)
+
+registerIntLt :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerIntLt f = do
+  int <- builtinName BuiltinInt
+  bool_ <- builtinName BuiltinBool
+  intLe <- toExpression <$> builtinName BuiltinIntLe
+  intPlus <- toExpression <$> builtinName BuiltinIntPlus
+  varm <- freshVar "m"
+  varn <- freshVar "n"
+  let intLt = f ^. funDefName
+      (.+.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+      x .+. y = intPlus @@ x @@ y
+      (.<=.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+      lit1 = ExpressionLiteral (WithLoc (getLoc f) (LitInteger 1))
+      x .<=. y = intLe @@ x @@ y
+      m = toExpression varm
+      n = toExpression varn
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [(intLt @@ m @@ n, (m .+. lit1) .<=. n)]
+  registerFun
+    FunInfo
+      { _funInfoDef = f,
+        _funInfoBuiltin = BuiltinIntLt,
+        _funInfoSignature = int --> int --> bool_,
+        _funInfoClauses = exClauses,
+        _funInfoFreeVars = [varm, varn],
+        _funInfoFreeTypeVars = []
+      }
+  where
+    builtinName :: IsBuiltin a => a -> Sem r Name
+    builtinName = getBuiltinName (getLoc f)
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@ -39,10 +39,12 @@ builtinConstructors :: BuiltinInductive -> [BuiltinConstructor]
 builtinConstructors = \case
  BuiltinNat -> [BuiltinNatZero, BuiltinNatSuc]
  BuiltinBool -> [BuiltinBoolTrue, BuiltinBoolFalse]
+  BuiltinInt -> [BuiltinIntOfNat, BuiltinIntNegSuc]

 data BuiltinInductive
  = BuiltinNat
  | BuiltinBool
+  | BuiltinInt
  deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)

 instance Hashable BuiltinInductive
@ -51,12 +53,15 @@ instance Pretty BuiltinInductive where
  pretty = \case
    BuiltinNat -> Str.nat
    BuiltinBool -> Str.bool_
+    BuiltinInt -> Str.int_

 data BuiltinConstructor
  = BuiltinNatZero
  | BuiltinNatSuc
  | BuiltinBoolTrue
  | BuiltinBoolFalse
+  | BuiltinIntOfNat
+  | BuiltinIntNegSuc
  deriving stock (Show, Eq, Ord, Generic, Data)

 instance Hashable BuiltinConstructor
@ -74,6 +79,18 @@ data BuiltinFunction
  | BuiltinBoolIf
  | BuiltinBoolOr
  | BuiltinBoolAnd
+  | BuiltinIntEq
+  | BuiltinIntPlus
+  | BuiltinIntSubNat
+  | BuiltinIntNegNat
+  | BuiltinIntNeg
+  | BuiltinIntMul
+  | BuiltinIntDiv
+  | BuiltinIntMod
+  | BuiltinIntSub
+  | BuiltinIntNonNeg
+  | BuiltinIntLe
+  | BuiltinIntLt
  deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)

 instance Hashable BuiltinFunction
@ -92,6 +109,18 @@ instance Pretty BuiltinFunction where
    BuiltinBoolIf -> Str.boolIf
    BuiltinBoolOr -> Str.boolOr
    BuiltinBoolAnd -> Str.boolAnd
+    BuiltinIntEq -> Str.intEq
+    BuiltinIntPlus -> Str.intPlus
+    BuiltinIntSubNat -> Str.intSubNat
+    BuiltinIntNegNat -> Str.intNegNat
+    BuiltinIntNeg -> Str.intNeg
+    BuiltinIntMul -> Str.intMul
+    BuiltinIntDiv -> Str.intDiv
+    BuiltinIntMod -> Str.intMod
+    BuiltinIntSub -> Str.intSub
+    BuiltinIntNonNeg -> Str.intNonNeg
+    BuiltinIntLe -> Str.intLe
+    BuiltinIntLt -> Str.intLt

 data BuiltinAxiom
  = BuiltinNatPrint
@ -107,6 +136,8 @@ data BuiltinAxiom
  | BuiltinIOReadline
  | BuiltinTrace
  | BuiltinFail
+  | BuiltinIntToString
+  | BuiltinIntPrint
  deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)

 instance Hashable BuiltinAxiom
@ -126,6 +157,8 @@ instance Pretty BuiltinAxiom where
    BuiltinIOReadline -> Str.ioReadline
    BuiltinTrace -> Str.trace_
    BuiltinFail -> Str.fail_
+    BuiltinIntToString -> Str.intToString
+    BuiltinIntPrint -> Str.intPrint

 data BuiltinType
  = BuiltinTypeInductive BuiltinInductive
@ -157,5 +190,21 @@ isNatBuiltin = \case
  BuiltinNatEq -> True
  _ -> False

+isIntBuiltin :: BuiltinFunction -> Bool
+isIntBuiltin = \case
+  BuiltinIntEq -> True
+  BuiltinIntPlus -> True
+  BuiltinIntSubNat -> True
+  BuiltinIntNegNat -> True
+  BuiltinIntNeg -> True
+  BuiltinIntMul -> True
+  BuiltinIntDiv -> True
+  BuiltinIntMod -> True
+  BuiltinIntSub -> True
+  BuiltinIntNonNeg -> True
+  BuiltinIntLe -> True
+  BuiltinIntLt -> True
+  _ -> False
+
 isIgnoredBuiltin :: BuiltinFunction -> Bool
-isIgnoredBuiltin = not . isNatBuiltin
+isIgnoredBuiltin f = not (isNatBuiltin f) && not (isIntBuiltin f)
--- a/src/Juvix/Compiler/Core/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTable.hs
@ -19,7 +19,8 @@ data InfoTable = InfoTable
    _infoInductives :: HashMap Symbol InductiveInfo,
    _infoConstructors :: HashMap Tag ConstructorInfo,
    _infoAxioms :: HashMap Text AxiomInfo,
-    _infoIntToNat :: Maybe Symbol,
+    _infoLiteralIntToNat :: Maybe Symbol,
+    _infoLiteralIntToInt :: Maybe Symbol,
    _infoNextSymbol :: Word,
    _infoNextTag :: Word,
    _infoBuiltins :: HashMap BuiltinPrim IdentKind
@ -35,7 +36,8 @@ emptyInfoTable =
      _infoInductives = mempty,
      _infoConstructors = mempty,
      _infoAxioms = mempty,
-      _infoIntToNat = Nothing,
+      _infoLiteralIntToNat = Nothing,
+      _infoLiteralIntToInt = Nothing,
      _infoNextSymbol = 1,
      _infoNextTag = 0,
      _infoBuiltins = mempty
--- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
@ -18,6 +18,8 @@ data InfoTableBuilder m a where
  RegisterInductive :: Text -> InductiveInfo -> InfoTableBuilder m ()
  RegisterIdentNode :: Symbol -> Node -> InfoTableBuilder m ()
  RegisterMain :: Symbol -> InfoTableBuilder m ()
+  RegisterLiteralIntToNat :: Symbol -> InfoTableBuilder m ()
+  RegisterLiteralIntToInt :: Symbol -> InfoTableBuilder m ()
  RemoveSymbol :: Symbol -> InfoTableBuilder m ()
  OverIdentArgs :: Symbol -> ([Binder] -> [Binder]) -> InfoTableBuilder m ()
  GetIdent :: Text -> InfoTableBuilder m (Maybe IdentKind)
@ -32,6 +34,11 @@ getConstructorInfo tag = flip lookupConstructorInfo tag <$> getInfoTable
 getInductiveInfo :: (Member InfoTableBuilder r) => Symbol -> Sem r InductiveInfo
 getInductiveInfo sym = flip lookupInductiveInfo sym <$> getInfoTable

+getBuiltinInductiveInfo :: Member InfoTableBuilder r => BuiltinInductive -> Sem r InductiveInfo
+getBuiltinInductiveInfo b = do
+  tab <- getInfoTable
+  return $ fromJust (lookupBuiltinInductive tab b)
+
 getIdentifierInfo :: (Member InfoTableBuilder r) => Symbol -> Sem r IdentifierInfo
 getIdentifierInfo sym = flip lookupIdentifierInfo sym <$> getInfoTable

@ -46,9 +53,10 @@ getIOSymbol = do
  return $ ci ^. constructorInductive

 getNatSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
-getNatSymbol = do
-  tab <- getInfoTable
-  return $ fromJust (lookupBuiltinInductive tab BuiltinNat) ^. inductiveSymbol
+getNatSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinNat
+
+getIntSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
+getIntSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinInt

 checkSymbolDefined :: (Member InfoTableBuilder r) => Symbol -> Sem r Bool
 checkSymbolDefined sym = do
@ -101,6 +109,10 @@ runInfoTableBuilder tab =
        modify' (over identContext (HashMap.insert sym node))
      RegisterMain sym -> do
        modify' (set infoMain (Just sym))
+      RegisterLiteralIntToInt sym -> do
+        modify' (set infoLiteralIntToInt (Just sym))
+      RegisterLiteralIntToNat sym -> do
+        modify' (set infoLiteralIntToNat (Just sym))
      RemoveSymbol sym -> do
        modify' (over infoMain (maybe Nothing (\sym' -> if sym' == sym then Nothing else Just sym')))
        modify' (over infoIdentifiers (HashMap.delete sym))
@ -210,3 +222,81 @@ declareNatBuiltins = do
    [ (tagZero, "zero", id, Just BuiltinNatZero),
      (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc)
    ]
+
+reserveLiteralIntToNatSymbol :: Member InfoTableBuilder r => Sem r ()
+reserveLiteralIntToNatSymbol = do
+  sym <- freshSymbol
+  registerLiteralIntToNat sym
+
+reserveLiteralIntToIntSymbol :: Member InfoTableBuilder r => Sem r ()
+reserveLiteralIntToIntSymbol = do
+  sym <- freshSymbol
+  registerLiteralIntToInt sym
+
+-- | Register a function Int -> Nat used to transform literal integers to builtin Nat
+setupLiteralIntToNat :: forall r. Member InfoTableBuilder r => (Symbol -> Sem r Node) -> Sem r ()
+setupLiteralIntToNat mkNode = do
+  tab <- getInfoTable
+  whenJust (tab ^. infoLiteralIntToNat) go
+  where
+    go :: Symbol -> Sem r ()
+    go sym = do
+      ii <- info sym
+      registerIdent (ii ^. identifierName) ii
+      n <- mkNode sym
+      registerIdentNode sym n
+      where
+        info :: Symbol -> Sem r IdentifierInfo
+        info s = do
+          tab <- getInfoTable
+          ty <- targetType
+          return $
+            IdentifierInfo
+              { _identifierSymbol = s,
+                _identifierName = freshIdentName tab "intToNat",
+                _identifierLocation = Nothing,
+                _identifierArgsNum = 1,
+                _identifierType = mkPi mempty (Binder "x" Nothing mkTypeInteger') ty,
+                _identifierIsExported = False,
+                _identifierBuiltin = Nothing
+              }
+
+        targetType :: Sem r Node
+        targetType = do
+          tab <- getInfoTable
+          let natSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinNat
+          return (maybe mkTypeInteger' (\s -> mkTypeConstr (setInfoName "Nat" mempty) s []) natSymM)
+
+-- | Register a function Int -> Int used to transform literal integers to builtin Int
+setupLiteralIntToInt :: forall r. Member InfoTableBuilder r => Sem r Node -> Sem r ()
+setupLiteralIntToInt node = do
+  tab <- getInfoTable
+  whenJust (tab ^. infoLiteralIntToInt) go
+  where
+    go :: Symbol -> Sem r ()
+    go sym = do
+      ii <- info sym
+      registerIdent (ii ^. identifierName) ii
+      n <- node
+      registerIdentNode sym n
+      where
+        info :: Symbol -> Sem r IdentifierInfo
+        info s = do
+          tab <- getInfoTable
+          ty <- targetType
+          return $
+            IdentifierInfo
+              { _identifierSymbol = s,
+                _identifierName = freshIdentName tab "literalIntToInt",
+                _identifierLocation = Nothing,
+                _identifierArgsNum = 1,
+                _identifierType = mkPi mempty (Binder "x" Nothing mkTypeInteger') ty,
+                _identifierIsExported = False,
+                _identifierBuiltin = Nothing
+              }
+
+        targetType :: Sem r Node
+        targetType = do
+          tab <- getInfoTable
+          let intSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinInt
+          return (maybe mkTypeInteger' (\s -> mkTypeConstr (setInfoName "Int" mempty) s []) intSymM)
--- a/src/Juvix/Compiler/Core/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs
@ -8,7 +8,8 @@ data TransformationId
  | TopEtaExpand
  | RemoveTypeArgs
  | MoveApps
-  | NatToInt
+  | NatToPrimInt
+  | IntToPrimInt
  | ConvertBuiltinTypes
  | Identity
  | UnrollRecursion
@ -51,7 +52,7 @@ toTypecheckTransformations :: [TransformationId]
 toTypecheckTransformations = [MatchToCase]

 toEvalTransformations :: [TransformationId]
-toEvalTransformations = [EtaExpandApps, MatchToCase, NatToInt, ConvertBuiltinTypes, LetFolding]
+toEvalTransformations = [EtaExpandApps, MatchToCase, NatToPrimInt, IntToPrimInt, ConvertBuiltinTypes, LetFolding]

 toStrippedTransformations :: [TransformationId]
 toStrippedTransformations =
--- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
@ -76,7 +76,8 @@ transformationText = \case
  Identity -> strIdentity
  RemoveTypeArgs -> strRemoveTypeArgs
  MoveApps -> strMoveApps
-  NatToInt -> strNatToInt
+  NatToPrimInt -> strNatToPrimInt
+  IntToPrimInt -> strIntToPrimInt
  ConvertBuiltinTypes -> strConvertBuiltinTypes
  ComputeTypeInfo -> strComputeTypeInfo
  UnrollRecursion -> strUnrollRecursion
@ -131,8 +132,11 @@ strRemoveTypeArgs = "remove-type-args"
 strMoveApps :: Text
 strMoveApps = "move-apps"

-strNatToInt :: Text
-strNatToInt = "nat-to-int"
+strNatToPrimInt :: Text
+strNatToPrimInt = "nat-to-primint"
+
+strIntToPrimInt :: Text
+strIntToPrimInt = "int-to-primint"

 strConvertBuiltinTypes :: Text
 strConvertBuiltinTypes = "convert-builtin-types"
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@ -20,11 +20,12 @@ import Juvix.Compiler.Core.Transformation.DisambiguateNames
 import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Transformation.FoldTypeSynonyms
 import Juvix.Compiler.Core.Transformation.Identity
+import Juvix.Compiler.Core.Transformation.IntToPrimInt
 import Juvix.Compiler.Core.Transformation.LambdaLetRecLifting
 import Juvix.Compiler.Core.Transformation.MatchToCase
 import Juvix.Compiler.Core.Transformation.MoveApps
 import Juvix.Compiler.Core.Transformation.NaiveMatchToCase qualified as Naive
-import Juvix.Compiler.Core.Transformation.NatToInt
+import Juvix.Compiler.Core.Transformation.NatToPrimInt
 import Juvix.Compiler.Core.Transformation.Optimize.LetFolding
 import Juvix.Compiler.Core.Transformation.RemoveTypeArgs
 import Juvix.Compiler.Core.Transformation.TopEtaExpand
@ -41,7 +42,8 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts
      TopEtaExpand -> return . topEtaExpand
      RemoveTypeArgs -> return . removeTypeArgs
      MoveApps -> return . moveApps
-      NatToInt -> return . natToInt
+      NatToPrimInt -> return . natToPrimInt
+      IntToPrimInt -> return . intToPrimInt
      ConvertBuiltinTypes -> return . convertBuiltinTypes
      ComputeTypeInfo -> return . computeTypeInfo
      UnrollRecursion -> unrollRecursion
--- a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs
+++ b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs
@ -16,6 +16,7 @@ convertNode tab = umap go
        case ii ^. inductiveBuiltin of
          Just (BuiltinTypeInductive BuiltinBool) -> mkTypeBool'
          Just (BuiltinTypeInductive BuiltinNat) -> mkTypeInteger'
+          Just (BuiltinTypeInductive BuiltinInt) -> mkTypeInteger'
          Just (BuiltinTypeAxiom BuiltinString) -> mkTypeString'
          _ -> node
        where
--- a/src/Juvix/Compiler/Core/Transformation/IntToPrimInt.hs
+++ b/src/Juvix/Compiler/Core/Transformation/IntToPrimInt.hs
@ -0,0 +1,188 @@
+module Juvix.Compiler.Core.Transformation.IntToPrimInt where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Transformation.Base
+import Safe (headMay)
+
+data BuiltinIntCtor
+  = BuiltinIntCtorOfNat
+  | BuiltinIntCtorNegSuc
+
+convertNode :: InfoTable -> Node -> Node
+convertNode tab = rmap go
+  where
+    go :: ([BinderChange] -> Node -> Node) -> Node -> Node
+    go recur node = case node of
+      NApp (App _ (NIdt (Ident {..})) l)
+        | Just _identSymbol == tab ^. infoLiteralIntToInt -> go recur l
+      NApp (App _ (NApp (App _ (NIdt (Ident {..})) l)) r) ->
+        recur [] $ convertIdentApp node (\g -> g _identInfo l r) _identSymbol
+      NApp (App _ (NIdt (Ident {..})) l) ->
+        recur [] $ convertSingleArgIdentApp node l _identInfo _identSymbol
+      NIdt (Ident {..})
+        | Just _identSymbol == tab ^. infoLiteralIntToInt ->
+            mkLambda' mkTypeInteger' (mkVar' 0)
+      NIdt (Ident {..}) ->
+        recur [] $ convertSingleArgIdent node _identInfo _identSymbol
+      NCtr (Constr {..}) ->
+        let ci = lookupConstructorInfo tab _constrTag
+         in case ci ^. constructorBuiltin of
+              Just BuiltinIntOfNat -> recur [] (fromJust (headMay _constrArgs))
+              Just BuiltinIntNegSuc -> recur [] (negSucConv (fromJust (headMay _constrArgs)))
+              _ -> recur [] node
+      NCase (Case {..}) ->
+        let ii = lookupInductiveInfo tab _caseInductive
+         in case ii ^. inductiveBuiltin of
+              Just (BuiltinTypeInductive BuiltinInt) ->
+                case _caseBranches of
+                  [br] -> makeIf' br (maybeBranch _caseDefault)
+                  [br1, br2] -> case (builtinCtor br1, builtinCtor br2) of
+                    (BuiltinIntCtorOfNat, BuiltinIntCtorNegSuc) -> makeIf br1 br2
+                    (BuiltinIntCtorNegSuc, BuiltinIntCtorOfNat) -> makeIf br2 br1
+                    _ -> impossible
+                  [] -> recur [] $ fromJust _caseDefault
+                  _ -> impossible
+              _ -> recur [] node
+        where
+          makeIf' :: CaseBranch -> Node -> Node
+          makeIf' caseBranch defaultNode =
+            let boolSym = lookupConstructorInfo tab (BuiltinTag TagTrue) ^. constructorInductive
+                cv = go recur _caseValue
+                binder = fromJust (headMay (caseBranch ^. caseBranchBinders))
+                binder' = over binderType (go recur) binder
+                mkBody n = go (recur . (BCKeep binder :)) n
+             in case builtinCtor caseBranch of
+                  BuiltinIntCtorOfNat ->
+                    mkIf
+                      _caseInfo
+                      boolSym
+                      (mkBuiltinApp' OpIntLe [mkConstant' (ConstInteger 0), cv])
+                      (mkLet mempty binder' cv (mkBody (caseBranch ^. caseBranchBody)))
+                      (go recur defaultNode)
+                  BuiltinIntCtorNegSuc ->
+                    mkIf
+                      _caseInfo
+                      boolSym
+                      (mkBuiltinApp' OpIntLt [cv, mkConstant' (ConstInteger 0)])
+                      (mkLet mempty binder' (negSucConv cv) (mkBody (caseBranch ^. caseBranchBody)))
+                      (go recur defaultNode)
+
+          makeIf :: CaseBranch -> CaseBranch -> Node
+          makeIf ofNatBranch negSucBranch =
+            let boolSym = lookupConstructorInfo tab (BuiltinTag TagTrue) ^. constructorInductive
+                cv = go recur _caseValue
+                binder :: CaseBranch -> Binder
+                binder br = fromJust (headMay (br ^. caseBranchBinders))
+                binder' br = over binderType (go recur) (binder br)
+                mkBody br = go (recur . (BCKeep (binder br) :)) (br ^. caseBranchBody)
+             in mkIf
+                  _caseInfo
+                  boolSym
+                  (mkBuiltinApp' OpIntLe [mkConstant' (ConstInteger 0), cv])
+                  (mkLet mempty (binder' ofNatBranch) cv (mkBody ofNatBranch))
+                  (mkLet mempty (binder' negSucBranch) (negSucConv cv) (mkBody negSucBranch))
+
+          builtinCtor :: CaseBranch -> BuiltinIntCtor
+          builtinCtor CaseBranch {..} =
+            let ci = lookupConstructorInfo tab _caseBranchTag
+             in case ci ^. constructorBuiltin of
+                  Just BuiltinIntOfNat -> BuiltinIntCtorOfNat
+                  Just BuiltinIntNegSuc -> BuiltinIntCtorNegSuc
+                  _ -> impossible
+
+          maybeBranch :: Maybe Node -> Node
+          maybeBranch = fromMaybe (mkBuiltinApp' OpFail [mkConstant' (ConstString "no matching branch")])
+      NTyp TypeConstr {..} ->
+        case ii ^. inductiveBuiltin of
+          Just (BuiltinTypeInductive BuiltinInt) -> mkTypeInteger'
+          _ -> recur [] node
+        where
+          ii = fromJust $ tab ^. infoInductives . at _typeConstrSymbol
+      _ -> recur [] node
+
+    -- Transforms n to -(n+1)
+    negSucConv :: Node -> Node
+    negSucConv n =
+      mkBuiltinApp'
+        OpIntSub
+        [ mkConstant' (ConstInteger 0),
+          mkBuiltinApp' OpIntAdd [n, mkConstant' (ConstInteger 1)]
+        ]
+
+    convertIdentApp :: Node -> ((Info -> Node -> Node -> Node) -> Node) -> Symbol -> Node
+    convertIdentApp node f sym =
+      let ii = lookupIdentifierInfo tab sym
+       in case ii ^. identifierBuiltin of
+            Just BuiltinIntEq -> f (\info x y -> mkBuiltinApp info OpEq [x, y])
+            Just BuiltinIntPlus -> f (\info x y -> mkBuiltinApp info OpIntAdd [x, y])
+            Just BuiltinIntSubNat -> f (\info x y -> mkBuiltinApp info OpIntSub [x, y])
+            Just BuiltinIntMul -> f (\info x y -> mkBuiltinApp info OpIntMul [x, y])
+            Just BuiltinIntDiv -> f (\info x y -> mkBuiltinApp info OpIntDiv [x, y])
+            Just BuiltinIntMod -> f (\info x y -> mkBuiltinApp info OpIntMod [x, y])
+            Just BuiltinIntSub -> f (\info x y -> mkBuiltinApp info OpIntSub [x, y])
+            Just BuiltinIntLe -> f (\info x y -> mkBuiltinApp info OpIntLe [x, y])
+            Just BuiltinIntLt -> f (\info x y -> mkBuiltinApp info OpIntLt [x, y])
+            _ -> node
+
+    convertSingleArgIdentApp :: Node -> Node -> Info -> Symbol -> Node
+    convertSingleArgIdentApp node l info sym =
+      let ii = lookupIdentifierInfo tab sym
+          negNode = negNatBody info l
+       in case ii ^. identifierBuiltin of
+            Just BuiltinIntNegNat -> negNode
+            Just BuiltinIntNeg -> negNode
+            Just BuiltinIntNonNeg -> mkBuiltinApp info OpIntLe [mkConstant' (ConstInteger 0), l]
+            _ ->
+              convertIdentApp
+                node
+                ( \g ->
+                    mkLet' mkTypeInteger' l $
+                      mkLambda' mkTypeInteger' $
+                        g info (mkVar' 1) (mkVar' 0)
+                )
+                sym
+
+    convertSingleArgIdent :: Node -> Info -> Symbol -> Node
+    convertSingleArgIdent node info sym =
+      let ii = lookupIdentifierInfo tab sym
+          negNode = mkLambda' mkTypeInteger' $ negNatBody info (mkVar' 0)
+       in case ii ^. identifierBuiltin of
+            Just BuiltinIntNegNat -> negNode
+            Just BuiltinIntNeg -> negNode
+            _ ->
+              convertIdentApp
+                node
+                ( \g ->
+                    mkLambda' mkTypeInteger' $
+                      mkLambda' mkTypeInteger' $
+                        g info (mkVar' 1) (mkVar' 0)
+                )
+                sym
+
+    negNatBody :: Info -> Node -> Node
+    negNatBody info n = mkBuiltinApp info OpIntSub [mkConstant' (ConstInteger 0), n]
+
+filterIntBuiltins :: InfoTable -> InfoTable
+filterIntBuiltins tab =
+  let tab' =
+        over
+          infoIdentifiers
+          (HashMap.filter (isNotIntBuiltin . (^. identifierBuiltin)))
+          tab
+   in pruneInfoTable tab'
+  where
+    isNotIntBuiltin :: Maybe BuiltinFunction -> Bool
+    isNotIntBuiltin = \case
+      Just b -> not (isIntBuiltin b)
+      Nothing -> True
+
+intToPrimInt :: InfoTable -> InfoTable
+intToPrimInt tab = filterIntBuiltins $ mapAllNodes (convertNode tab') tab'
+  where
+    tab' =
+      case tab ^. infoLiteralIntToInt of
+        Just sym ->
+          tab {_identContext = HashMap.insert sym (mkLambda' mkTypeInteger' (mkVar' 0)) (tab ^. identContext)}
+        Nothing ->
+          tab
--- a/src/Juvix/Compiler/Core/Transformation/NatToPrimInt.hs
+++ b/src/Juvix/Compiler/Core/Transformation/NatToPrimInt.hs
@ -1,4 +1,4 @@
-module Juvix.Compiler.Core.Transformation.NatToInt (natToInt) where
+module Juvix.Compiler.Core.Transformation.NatToPrimInt (natToPrimInt) where

 import Data.HashMap.Strict qualified as HashMap
 import Data.List qualified as List
@ -13,7 +13,7 @@ convertNode tab = rmap go
    go :: ([BinderChange] -> Node -> Node) -> Node -> Node
    go recur node = case node of
      NApp (App _ (NIdt (Ident {..})) l)
-        | Just _identSymbol == tab ^. infoIntToNat ->
+        | Just _identSymbol == tab ^. infoLiteralIntToNat ->
            go recur l
      NApp (App _ (NApp (App _ (NIdt (Ident {..})) l)) r) ->
        recur [] $ convertIdentApp node (\g -> g _identInfo l r) _identSymbol
@ -28,7 +28,7 @@ convertNode tab = rmap go
            )
            _identSymbol
      NIdt (Ident {..})
-        | Just _identSymbol == tab ^. infoIntToNat ->
+        | Just _identSymbol == tab ^. infoLiteralIntToNat ->
            mkLambda' mkTypeInteger' (mkVar' 0)
      NIdt (Ident {..}) ->
        recur [] $
@ -141,11 +141,11 @@ filterNatBuiltins tab =
      Just b -> not (isNatBuiltin b)
      Nothing -> True

-natToInt :: InfoTable -> InfoTable
-natToInt tab = filterNatBuiltins $ mapAllNodes (convertNode tab') tab'
+natToPrimInt :: InfoTable -> InfoTable
+natToPrimInt tab = filterNatBuiltins $ mapAllNodes (convertNode tab') tab'
  where
    tab' =
-      case tab ^. infoIntToNat of
+      case tab ^. infoLiteralIntToNat of
        Just sym ->
          tab {_identContext = HashMap.insert sym (mkLambda' mkTypeInteger' (mkVar' 0)) (tab ^. identContext)}
        Nothing ->
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@ -4,13 +4,14 @@ import Data.HashMap.Strict qualified as HashMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Text qualified as Text
 import Juvix.Compiler.Abstract.Data.Name
-import Juvix.Compiler.Concrete.Data.Literal (LiteralLoc)
 import Juvix.Compiler.Core.Data
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.LocationInfo
 import Juvix.Compiler.Core.Info.NameInfo
 import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Translation.FromInternal.Builtins.Int
+import Juvix.Compiler.Core.Translation.FromInternal.Builtins.Nat
 import Juvix.Compiler.Core.Translation.FromInternal.Data
 import Juvix.Compiler.Internal.Extra qualified as Internal
 import Juvix.Compiler.Internal.Translation.Extra qualified as Internal
@ -30,62 +31,25 @@ mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId)

 fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
 fromInternal i = do
-  (res, _) <- runInfoTableBuilder tab0 (evalState (i ^. InternalTyped.resultFunctions) (runReader (i ^. InternalTyped.resultIdenTypes) f))
+  (res, _) <- runInfoTableBuilder emptyInfoTable (evalState (i ^. InternalTyped.resultFunctions) (runReader (i ^. InternalTyped.resultIdenTypes) f))
  return $
    CoreResult
-      { _coreResultTable = setupIntToNat intToNatSym res,
+      { _coreResultTable = res,
        _coreResultInternalTypedResult = i
      }
  where
-    tab0 :: InfoTable
-    tab0 = emptyInfoTable {_infoIntToNat = Just intToNatSym, _infoNextSymbol = intToNatSym + 1}
-
-    intToNatSym :: Symbol
-    intToNatSym = 0
-
    f :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, State InternalTyped.FunctionsTable] r => Sem r ()
    f = do
+      reserveLiteralIntToNatSymbol
+      reserveLiteralIntToIntSymbol
      let resultModules = toList (i ^. InternalTyped.resultModules)
      runReader (Internal.buildTable resultModules) (mapM_ goTopModule resultModules)
      tab <- getInfoTable
      when
        (isNothing (lookupBuiltinInductive tab BuiltinBool))
        declareBoolBuiltins
-
-    setupIntToNat :: Symbol -> InfoTable -> InfoTable
-    setupIntToNat sym tab =
-      tab
-        { _infoIdentifiers = HashMap.insert sym ii (tab ^. infoIdentifiers),
-          _identContext = HashMap.insert sym node (tab ^. identContext),
-          _infoIntToNat = Just sym
-        }
-      where
-        ii =
-          IdentifierInfo
-            { _identifierSymbol = sym,
-              _identifierName = freshIdentName tab "intToNat",
-              _identifierLocation = Nothing,
-              _identifierArgsNum = 1,
-              _identifierType = mkPi mempty (Binder "x" Nothing mkTypeInteger') targetType,
-              _identifierIsExported = False,
-              _identifierBuiltin = Nothing
-            }
-        node =
-          case (tagZeroM, tagSucM, boolSymM) of
-            (Just tagZero, Just tagSuc, Just boolSym) ->
-              mkLambda' mkTypeInteger' $
-                mkIf'
-                  boolSym
-                  (mkBuiltinApp' OpEq [mkVar' 0, mkConstant' (ConstInteger 0)])
-                  (mkConstr (setInfoName "zero" mempty) tagZero [])
-                  (mkConstr (setInfoName "suc" mempty) tagSuc [mkApp' (mkIdent' sym) (mkBuiltinApp' OpIntSub [mkVar' 0, mkConstant' (ConstInteger 1)])])
-            _ ->
-              mkLambda' mkTypeInteger' $ mkVar' 0
-        targetType = maybe mkTypeInteger' (\s -> mkTypeConstr (setInfoName "Nat" mempty) s []) natSymM
-        tagZeroM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatZero
-        tagSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatSuc
-        boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
-        natSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinNat
+      setupLiteralIntToNat literalIntToNatNode
+      setupLiteralIntToInt literalIntToIntNode

 fromInternalExpression :: CoreResult -> Internal.Expression -> Sem r Node
 fromInternalExpression res exp = do
@ -213,6 +177,8 @@ goConstructor sym ctor = do
      Just Internal.BuiltinBoolFalse -> return (BuiltinTag TagFalse)
      Just Internal.BuiltinNatZero -> freshTag
      Just Internal.BuiltinNatSuc -> freshTag
+      Just Internal.BuiltinIntOfNat -> freshTag
+      Just Internal.BuiltinIntNegSuc -> freshTag
      Nothing -> freshTag

    ctorType :: Sem r Type
@ -504,6 +470,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
      Internal.BuiltinStringEq -> return ()
      Internal.BuiltinStringToNat -> return ()
      Internal.BuiltinNatToString -> return ()
+      Internal.BuiltinIntToString -> return ()
+      Internal.BuiltinIntPrint -> return ()

    registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r ()
    registerInductiveAxiom ax ctrs = do
@ -532,39 +500,19 @@ goAxiomDef ::
  Internal.AxiomDef ->
  Sem r ()
 goAxiomDef a = do
-  boolSym <- getBoolSymbol
-  natSym <- getNatSymbol
-  tab <- getInfoTable
-  let natName = fromJust (HashMap.lookup natSym (tab ^. infoInductives)) ^. inductiveName
-  case a ^. Internal.axiomBuiltin >>= builtinBody boolSym natSym natName of
-    Just body -> do
-      sym <- freshSymbol
-      ty <- axiomType'
-      _identifierName <- topName (a ^. Internal.axiomName)
-      let info =
-            IdentifierInfo
-              { _identifierLocation = Just $ a ^. Internal.axiomName . nameLoc,
-                _identifierSymbol = sym,
-                _identifierType = ty,
-                _identifierArgsNum = 0,
-                _identifierIsExported = False,
-                _identifierBuiltin = Nothing,
-                _identifierName
-              }
-      registerIdent (mkIdentIndex (a ^. Internal.axiomName)) info
-      registerIdentNode sym body
-      let (is, _) = unfoldLambdas body
-      setIdentArgs sym (map (^. lambdaLhsBinder) is)
-    Nothing -> return ()
+  mapM_ builtinBody (a ^. Internal.axiomBuiltin)
  where
-    builtinBody :: Symbol -> Symbol -> Text -> Internal.BuiltinAxiom -> Maybe Node
-    builtinBody boolSym natSym natName = \case
-      Internal.BuiltinNatPrint -> Just $ writeLambda (mkTypeConstr (setInfoName natName mempty) natSym [])
-      Internal.BuiltinStringPrint -> Just $ writeLambda mkTypeString'
-      Internal.BuiltinBoolPrint -> Just $ writeLambda mkTypeBool'
-      Internal.BuiltinIOSequence -> Nothing
+    builtinBody :: Internal.BuiltinAxiom -> Sem r ()
+    builtinBody = \case
+      Internal.BuiltinNatPrint -> do
+        natName <- getNatName
+        natSym <- getNatSymbol
+        registerAxiomDef $ writeLambda (mkTypeConstr (setInfoName natName mempty) natSym [])
+      Internal.BuiltinStringPrint -> registerAxiomDef $ writeLambda mkTypeString'
+      Internal.BuiltinBoolPrint -> registerAxiomDef $ writeLambda mkTypeBool'
+      Internal.BuiltinIOSequence -> return ()
      Internal.BuiltinIOReadline ->
-        Just
+        registerAxiomDef
          ( mkLambda'
              mkTypeString'
              ( mkConstr'
@ -575,11 +523,12 @@ goAxiomDef a = do
              )
          )
      Internal.BuiltinStringConcat ->
-        Just (mkLambda' mkTypeString' (mkLambda' mkTypeString' (mkBuiltinApp' OpStrConcat [mkVar' 1, mkVar' 0])))
+        registerAxiomDef (mkLambda' mkTypeString' (mkLambda' mkTypeString' (mkBuiltinApp' OpStrConcat [mkVar' 1, mkVar' 0])))
      Internal.BuiltinStringEq ->
-        Just (mkLambda' mkTypeString' (mkLambda' mkTypeString' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0])))
+        registerAxiomDef (mkLambda' mkTypeString' (mkLambda' mkTypeString' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0])))
      Internal.BuiltinStringToNat -> do
-        Just
+        boolSym <- getBoolSymbol
+        registerAxiomDef
          ( mkLambda'
              mkTypeString'
              ( mkLet'
@ -593,13 +542,23 @@ goAxiomDef a = do
                  )
              )
          )
-      Internal.BuiltinNatToString ->
-        Just (mkLambda' (mkTypeConstr (setInfoName natName mempty) natSym []) (mkBuiltinApp' OpShow [mkVar' 0]))
-      Internal.BuiltinString -> Nothing
-      Internal.BuiltinIO -> Nothing
-      Internal.BuiltinTrace -> Nothing
+      Internal.BuiltinNatToString -> do
+        natName <- getNatName
+        natSym <- getNatSymbol
+        registerAxiomDef (mkLambda' (mkTypeConstr (setInfoName natName mempty) natSym []) (mkBuiltinApp' OpShow [mkVar' 0]))
+      Internal.BuiltinString -> return ()
+      Internal.BuiltinIO -> return ()
+      Internal.BuiltinTrace -> return ()
      Internal.BuiltinFail ->
-        Just (mkLambda' mkSmallUniv (mkLambda' (mkVar' 0) (mkBuiltinApp' OpFail [mkVar' 0])))
+        registerAxiomDef (mkLambda' mkSmallUniv (mkLambda' (mkVar' 0) (mkBuiltinApp' OpFail [mkVar' 0])))
+      Internal.BuiltinIntToString -> do
+        intName <- getIntName
+        intSym <- getIntSymbol
+        registerAxiomDef (mkLambda' (mkTypeConstr (setInfoName intName mempty) intSym []) (mkBuiltinApp' OpShow [mkVar' 0]))
+      Internal.BuiltinIntPrint -> do
+        intName <- getIntName
+        intSym <- getIntSymbol
+        registerAxiomDef $ writeLambda (mkTypeConstr (setInfoName intName mempty) intSym [])

    axiomType' :: Sem r Type
    axiomType' = runReader initIndexTable (goType (a ^. Internal.axiomType))
@ -607,6 +566,33 @@ goAxiomDef a = do
    writeLambda :: Type -> Node
    writeLambda ty = mkLambda' ty (mkConstr' (BuiltinTag TagWrite) [mkVar' 0])

+    getNatName :: Sem r Text
+    getNatName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinNat
+
+    getIntName :: Sem r Text
+    getIntName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinInt
+
+    registerAxiomDef :: Node -> Sem r ()
+    registerAxiomDef body = do
+      let name = a ^. Internal.axiomName
+      sym <- freshSymbol
+      ty <- axiomType'
+      _identifierName <- topName name
+      let info =
+            IdentifierInfo
+              { _identifierLocation = Just $ name ^. nameLoc,
+                _identifierSymbol = sym,
+                _identifierType = ty,
+                _identifierArgsNum = 0,
+                _identifierIsExported = False,
+                _identifierBuiltin = Nothing,
+                _identifierName
+              }
+      registerIdent (mkIdentIndex name) info
+      registerIdentNode sym body
+      let (is, _) = unfoldLambdas body
+      setIdentArgs sym (map (^. lambdaLhsBinder) is)
+
 fromPatternArg ::
  forall r.
  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, State IndexTable] r) =>
@ -756,7 +742,7 @@ goExpression = \case
  Internal.ExpressionLet l -> goLet l
  Internal.ExpressionLiteral l -> do
    tab <- getInfoTable
-    return (goLiteral (fromJust $ tab ^. infoIntToNat) l)
+    return (goLiteral (fromJust $ tab ^. infoLiteralIntToNat) (fromJust $ tab ^. infoLiteralIntToInt) l)
  Internal.ExpressionIden i -> case i of
    Internal.IdenVar n -> do
      k <- HashMap.lookupDefault impossible id_ <$> asks (^. indexTableVars)
@ -905,6 +891,8 @@ goApplication a = do
              return (mkApps' (mkBuiltinApp' OpTrace [arg1, arg2]) xs)
            _ -> error "internal to core: trace must be called with 2 arguments"
        Just Internal.BuiltinFail -> app
+        Just Internal.BuiltinIntToString -> app
+        Just Internal.BuiltinIntPrint -> app
        Nothing -> app
    Internal.ExpressionIden (Internal.IdenFunction n) -> do
      funInfoBuiltin <- Internal.getFunctionBuiltinInfo n
@ -930,10 +918,11 @@ goApplication a = do
        _ -> app
    _ -> app

-goLiteral :: Symbol -> LiteralLoc -> Node
-goLiteral intToNat l = case l ^. withLocParam of
+goLiteral :: Symbol -> Symbol -> Internal.LiteralLoc -> Node
+goLiteral intToNat intToInt l = case l ^. withLocParam of
  Internal.LitString s -> mkLitConst (ConstString s)
-  Internal.LitInteger i -> mkApp' (mkIdent' intToNat) (mkLitConst (ConstInteger i))
+  Internal.LitInteger i -> mkApp' (mkIdent' intToInt) (mkLitConst (ConstInteger i))
+  Internal.LitNatural i -> mkApp' (mkIdent' intToNat) (mkLitConst (ConstInteger i))
  where
    mkLitConst :: ConstantValue -> Node
    mkLitConst = mkConstant (Info.singleton (LocationInfo (l ^. withLocInt)))
--- a/src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Int.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Int.hs
@ -0,0 +1,39 @@
+module Juvix.Compiler.Core.Translation.FromInternal.Builtins.Int where
+
+import Juvix.Compiler.Core.Data
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info.NameInfo
+import Juvix.Compiler.Core.Language
+
+-- | Returns the node representing a function Int -> Int that transforms literal
+-- integers to builtin Int.
+literalIntToIntNode :: Member InfoTableBuilder r => Sem r Node
+literalIntToIntNode = do
+  tab <- getInfoTable
+  let intToNatSymM = tab ^. infoLiteralIntToNat
+      tagOfNatM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinIntOfNat
+      tagNegSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinIntNegSuc
+      boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
+  return $
+    case (tagOfNatM, tagNegSucM, boolSymM, intToNatSymM) of
+      (Just tagOfNat, Just tagNegSuc, Just boolSym, Just intToNatSym) ->
+        mkLambda' mkTypeInteger' $
+          mkIf'
+            boolSym
+            (mkBuiltinApp' OpIntLt [mkVar' 0, mkConstant' (ConstInteger 0)])
+            ( mkConstr
+                (setInfoName "negSuc" mempty)
+                tagNegSuc
+                [ mkBuiltinApp'
+                    OpIntSub
+                    [ mkConstant' (ConstInteger 0),
+                      mkBuiltinApp' OpIntAdd [mkVar' 0, mkConstant' (ConstInteger 1)]
+                    ]
+                ]
+            )
+            ( mkConstr
+                (setInfoName "ofNat" mempty)
+                tagOfNat
+                [mkApp' (mkIdent' intToNatSym) (mkVar' 0)]
+            )
+      _ -> mkLambda' mkTypeInteger' $ mkVar' 0
--- a/src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Nat.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Nat.hs
@ -0,0 +1,25 @@
+module Juvix.Compiler.Core.Translation.FromInternal.Builtins.Nat where
+
+import Juvix.Compiler.Core.Data
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info.NameInfo
+import Juvix.Compiler.Core.Language
+
+-- | Returns the node representing a function Int -> Nat that is used to transform
+-- literal integers to builtin Nat. The symbol representing the literalIntToNat function is passed
+-- so that it can be called recusively.
+literalIntToNatNode :: Member InfoTableBuilder r => Symbol -> Sem r Node
+literalIntToNatNode sym = do
+  tab <- getInfoTable
+  let tagZeroM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatZero
+      tagSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatSuc
+      boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
+  return $ case (tagZeroM, tagSucM, boolSymM) of
+    (Just tagZero, Just tagSuc, Just boolSym) ->
+      mkLambda' mkTypeInteger' $
+        mkIf'
+          boolSym
+          (mkBuiltinApp' OpEq [mkVar' 0, mkConstant' (ConstInteger 0)])
+          (mkConstr (setInfoName "zero" mempty) tagZero [])
+          (mkConstr (setInfoName "suc" mempty) tagSuc [mkApp' (mkIdent' sym) (mkBuiltinApp' OpIntSub [mkVar' 0, mkConstant' (ConstInteger 1)])])
+    _ -> mkLambda' mkTypeInteger' $ mkVar' 0
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@ -3,7 +3,6 @@ module Juvix.Compiler.Internal.Language
    module Juvix.Compiler.Abstract.Data.Name,
    module Juvix.Data.WithLoc,
    module Juvix.Data.IsImplicit,
-    module Juvix.Compiler.Concrete.Data.Literal,
    module Juvix.Data.Universe,
    module Juvix.Data.Hole,
    module Juvix.Compiler.Concrete.Data.Builtins,
@ -12,7 +11,6 @@ where

 import Juvix.Compiler.Abstract.Data.Name
 import Juvix.Compiler.Concrete.Data.Builtins
-import Juvix.Compiler.Concrete.Data.Literal
 import Juvix.Data.Hole
 import Juvix.Data.IsImplicit
 import Juvix.Data.Universe hiding (smallUniverse)
@ -117,6 +115,16 @@ data Let = Let

 instance Hashable Let

+type LiteralLoc = WithLoc Literal
+
+data Literal
+  = LitString Text
+  | LitInteger Integer
+  | LitNatural Integer
+  deriving stock (Show, Eq, Ord, Generic, Data)
+
+instance Hashable Literal
+
 data Expression
  = ExpressionIden Iden
  | ExpressionApplication Application
@ -306,6 +314,12 @@ instance HasAtomicity SimpleLambda where
 instance HasAtomicity Let where
  atomicity l = atomicity (l ^. letExpression)

+instance HasAtomicity Literal where
+  atomicity = \case
+    LitNatural {} -> Atom
+    LitInteger {} -> Atom
+    LitString {} -> Atom
+
 instance HasAtomicity Lambda where
  atomicity = const Atom

--- a/src/Juvix/Compiler/Internal/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs
@ -69,7 +69,7 @@ instance PrettyCode Expression where
    ExpressionApplication a -> ppCode a
    ExpressionFunction f -> ppCode f
    ExpressionUniverse u -> ppCode u
-    ExpressionLiteral l -> return (pretty l)
+    ExpressionLiteral l -> ppCode l
    ExpressionSimpleLambda l -> ppCode l
    ExpressionLambda l -> ppCode l
    ExpressionLet l -> ppCode l
@ -106,6 +106,13 @@ instance PrettyCode LetClause where
            b' <- ppCode m
            return (kwMutual <+> braces (line <> indent' b' <> line))

+instance PrettyCode Literal where
+  ppCode =
+    return . \case
+      LitNatural n -> pretty n
+      LitInteger n -> pretty n
+      LitString s -> ppStringLit s
+
 ppPipeBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
 ppPipeBlock items = vsep <$> mapM (fmap (kwPipe <+>) . ppCode) items

--- a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs
@ -341,11 +341,19 @@ goExpression e = case e of
  Abstract.ExpressionFunction f -> ExpressionFunction <$> goExpressionFunction f
  Abstract.ExpressionApplication a -> ExpressionApplication <$> goApplication a
  Abstract.ExpressionLambda l -> ExpressionLambda <$> goLambda l
-  Abstract.ExpressionLiteral l -> return (ExpressionLiteral l)
+  Abstract.ExpressionLiteral l -> return (ExpressionLiteral (goLiteral l))
  Abstract.ExpressionHole h -> return (ExpressionHole h)
  Abstract.ExpressionLet l -> ExpressionLet <$> goLet l
  Abstract.ExpressionCase c -> ExpressionCase <$> goCase c

+goLiteral :: Abstract.LiteralLoc -> LiteralLoc
+goLiteral = fmap go
+  where
+    go :: Abstract.Literal -> Literal
+    go = \case
+      Abstract.LitString s -> LitString s
+      Abstract.LitInteger i -> LitInteger i
+
 goCase :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Case -> Sem r Case
 goCase c = do
  _caseExpression <- goExpression (c ^. Abstract.caseExpression)
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@ -475,23 +475,6 @@ freshHole l = do
  uid <- freshNameId
  return (Hole uid l)

-literalType :: (Members '[NameIdGen, Builtins] r) => LiteralLoc -> Sem r TypedExpression
-literalType lit@(WithLoc i l) = case l of
-  LitInteger {} -> do
-    nat <- getBuiltinName i BuiltinNat
-    return
-      TypedExpression
-        { _typedExpression = ExpressionLiteral lit,
-          _typedType = ExpressionIden (IdenInductive nat)
-        }
-  LitString {} -> do
-    str <- getBuiltinName i BuiltinString
-    return
-      TypedExpression
-        { _typedExpression = ExpressionLiteral lit,
-          _typedType = ExpressionIden (IdenAxiom str)
-        }
-
 inferExpression' ::
  forall r.
  (Members '[Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Builtins] r) =>
@ -620,7 +603,73 @@ inferExpression' hint e = case e of
      return (TypedExpression uni (ExpressionFunction (Function l' r')))

    goLiteral :: LiteralLoc -> Sem r TypedExpression
-    goLiteral = literalType
+    goLiteral lit@(WithLoc i l) = case l of
+      LitInteger v -> typedLitInteger v
+      LitNatural v -> typedLitInteger v
+      LitString {} -> do
+        str <- getBuiltinName i BuiltinString
+        return
+          TypedExpression
+            { _typedExpression = ExpressionLiteral lit,
+              _typedType = ExpressionIden (IdenAxiom str)
+            }
+      where
+        typedLitInteger :: Integer -> Sem r TypedExpression
+        typedLitInteger v = do
+          inferredTy <- inferLitTypeFromValue
+          ty <- case hint of
+            Nothing -> return inferredTy
+            Just ExpressionHole {} -> return inferredTy
+            Just hintTy -> checkHint inferredTy hintTy
+          lit' <- WithLoc i <$> valueFromType ty
+          return
+            TypedExpression
+              { _typedExpression = ExpressionLiteral lit',
+                _typedType = ty
+              }
+          where
+            mkBuiltinInductive :: BuiltinInductive -> Sem r Expression
+            mkBuiltinInductive = fmap (ExpressionIden . IdenInductive) . getBuiltinName i
+
+            getIntTy :: Sem r Expression
+            getIntTy = mkBuiltinInductive BuiltinInt
+
+            getNatTy :: Sem r Expression
+            getNatTy = mkBuiltinInductive BuiltinNat
+
+            inferLitTypeFromValue :: Sem r Expression
+            inferLitTypeFromValue
+              | v < 0 = getIntTy
+              | otherwise = getNatTy
+
+            valueFromType :: Expression -> Sem r Literal
+            valueFromType exp = do
+              natTy <- getNatTy
+              if
+                  | exp == natTy -> return $ LitNatural v
+                  | otherwise -> do
+                      -- Avoid looking up Int type when negative literals are not used.
+                      intTy <- getIntTy
+                      return $
+                        if
+                            | exp == intTy -> LitInteger v
+                            | otherwise -> l
+
+            checkHint :: Expression -> Expression -> Sem r Expression
+            checkHint inferredTy hintTy = do
+              natTy <- getNatTy
+              if
+                  -- Avoid looking up Int type when only Nat type is used.
+                  | inferredTy == natTy, hintTy == natTy -> return natTy
+                  | inferredTy == natTy -> checkHintWithInt
+                  | otherwise -> return inferredTy
+              where
+                checkHintWithInt :: Sem r Expression
+                checkHintWithInt = do
+                  intTy <- getIntTy
+                  if
+                      | hintTy == intTy -> return intTy
+                      | otherwise -> return inferredTy

    goIden :: Iden -> Sem r TypedExpression
    goIden i = case i of
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@ -104,6 +104,9 @@ stringToNat = "string-to-nat"
 bool_ :: (IsString s) => s
 bool_ = "bool"

+int_ :: (IsString s) => s
+int_ = "int"
+
 boolPrint :: (IsString s) => s
 boolPrint = "bool-print"

@ -164,6 +167,48 @@ boolOr = "bool-or"
 boolAnd :: IsString s => s
 boolAnd = "bool-and"

+intToString :: (IsString s) => s
+intToString = "int-to-string"
+
+intEq :: (IsString s) => s
+intEq = "int-eq"
+
+intPlus :: (IsString s) => s
+intPlus = "int-plus"
+
+intSubNat :: (IsString s) => s
+intSubNat = "int-sub-nat"
+
+intNegNat :: (IsString s) => s
+intNegNat = "int-neg-nat"
+
+intNeg :: (IsString s) => s
+intNeg = "int-neg"
+
+intMul :: (IsString s) => s
+intMul = "int-mul"
+
+intDiv :: (IsString s) => s
+intDiv = "int-div"
+
+intMod :: (IsString s) => s
+intMod = "int-mod"
+
+intSub :: (IsString s) => s
+intSub = "int-sub"
+
+intNonNeg :: (IsString s) => s
+intNonNeg = "int-nonneg"
+
+intLe :: IsString s => s
+intLe = "int-le"
+
+intLt :: IsString s => s
+intLt = "int-lt"
+
+intPrint :: (IsString s) => s
+intPrint = "int-print"
+
 builtin :: IsString s => s
 builtin = "builtin"

--- a/test/Compilation/Positive.hs
+++ b/test/Compilation/Positive.hs
@ -299,5 +299,15 @@ tests =
      "Test048: String quoting"
      $(mkRelDir ".")
      $(mkRelFile "test048.juvix")
-      $(mkRelFile "out/test048.out")
+      $(mkRelFile "out/test048.out"),
+    posTest
+      "Test049: Builtin Int"
+      $(mkRelDir ".")
+      $(mkRelFile "test049.juvix")
+      $(mkRelFile "out/test049.out"),
+    posTest
+      "Test050: Pattern matching with integers"
+      $(mkRelDir ".")
+      $(mkRelFile "test050.juvix")
+      $(mkRelFile "out/test050.out")
  ]
--- a/test/Reachability/Positive.hs
+++ b/test/Reachability/Positive.hs
@ -77,7 +77,7 @@ tests =
      StdlibInclude
      $(mkRelFile "N.juvix")
      ( HashSet.fromList
-          ["test", "Unit", "Bool", "Nat"]
+          ["test", "Unit", "Bool", "Nat", "Int"]
      ),
    PosTest
      "Reachability with public imports"
--- a/test/Typecheck/Negative.hs
+++ b/test/Typecheck/Negative.hs
@ -125,6 +125,20 @@ tests =
      $(mkRelFile "SelfApplication.juvix")
      $ \case
        ErrUnsolvedMeta {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Negative integer literal cannot be used as a Nat"
+      $(mkRelDir "Internal")
+      $(mkRelFile "LiteralInteger.juvix")
+      $ \case
+        ErrWrongType {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Integer literal cannot be used as a String"
+      $(mkRelDir "Internal")
+      $(mkRelFile "LiteralIntegerString.juvix")
+      $ \case
+        ErrWrongType {} -> Nothing
        _ -> wrongError
  ]

--- a/tests/Compilation/positive/out/test049.out
+++ b/tests/Compilation/positive/out/test049.out
@ -0,0 +1,31 @@
+1
+-1
+1
+-1
+1
+-1
+1
+0
+1
+1
+false
+true
+true
+false
+0
+-1
+-1
+1
+1
+-4
+-2
+0
+true
+false
+-1
+false
+true
+true
+false
+2
+-1
--- a/tests/Compilation/positive/out/test050.out
+++ b/tests/Compilation/positive/out/test050.out
@ -0,0 +1 @@
+11
--- a/tests/Compilation/positive/test027.juvix
+++ b/tests/Compilation/positive/test027.juvix
@ -1,7 +1,7 @@
 -- Church numerals
 module test027;

-open import Stdlib.Prelude;
+open import Stdlib.Prelude hiding {toNat};

 Num : Type;
 Num := {A : Type} → (A → A) → A → A;
--- a/tests/Compilation/positive/test049.juvix
+++ b/tests/Compilation/positive/test049.juvix
@ -0,0 +1,43 @@
+-- Builtin Int
+module test049;
+
+open import Stdlib.Prelude hiding {+;*;div;mod};
+open import Stdlib.Data.Int.Ord;
+open import Stdlib.Data.Int;
+
+f : Int -> Nat;
+f (negSuc n) := n;
+f (ofNat n) := n;
+
+main : IO;
+main := printStringLn (intToString 1)
+   >> printStringLn (intToString -1)
+   >> printIntLn (ofNat 1)
+   >> printIntLn (negSuc 0)
+   >> printIntLn (ofNat (suc zero))
+   >> printIntLn (negSuc zero)
+   >> printStringLn (natToString (f 1))
+   >> printNatLn (f (-1))
+   >> printNatLn (f (ofNat (suc zero)))
+   >> printNatLn (f (negSuc (suc zero)))
+   >> printBoolLn (-1 == -2)
+   >> printBoolLn (-1 == -1)
+   >> printBoolLn (1 == 1)
+   >> printBoolLn (-1 == 1)
+   >> printIntLn (-1 + 1)
+   >> printIntLn (negNat (suc zero))
+   >> printIntLn (let g : Nat -> Int := negNat in g (suc zero))
+   >> printIntLn (neg -1)
+   >> printIntLn (let g : Int -> Int := neg in g -1)
+   >> printIntLn (-2 * 2)
+   >> printIntLn (div 4 -2)
+   >> printIntLn (2 - 2)
+   >> printBoolLn (nonNeg 0)
+   >> printBoolLn (nonNeg -1)
+   >> printIntLn (mod -5 -2)
+   >> printBoolLn (0 < 0)
+   >> printBoolLn (0 <= 0)
+   >> printBoolLn (0 < 1)
+   >> printBoolLn (1 <= 0)
+   >> printIntLn (mod 5 -3)
+   >> printIntLn (div 5 -3);
--- a/tests/Compilation/positive/test050.juvix
+++ b/tests/Compilation/positive/test050.juvix
@ -0,0 +1,14 @@
+-- Pattern matching with integers
+module test050;
+
+open import Stdlib.Prelude hiding {+;*;div;mod};
+open import Stdlib.Data.Int.Ord;
+open import Stdlib.Data.Int;
+
+f : Int -> Int;
+f (negSuc zero) := ofNat 0;
+f (negSuc m@(suc n)) := ofNat n + ofNat m;
+f (ofNat n) := neg (ofNat n - 7);
+
+main : Int;
+main := f -10 - f 1 + f -1;
--- a/tests/Internal/positive/Church.juvix
+++ b/tests/Internal/positive/Church.juvix
@ -1,6 +1,6 @@
 module Church;

-open import Stdlib.Prelude;
+open import Stdlib.Prelude hiding {toNat};

 Num : Type;
 Num := {A : Type} → (A → A) → A → A;
--- a/tests/Internal/positive/MatchConstructor.juvix
+++ b/tests/Internal/positive/MatchConstructor.juvix
@ -1,6 +1,6 @@
 module MatchConstructor;

-open import Stdlib.Prelude;
+open import Stdlib.Prelude hiding {toNat};

 type Foo :=
  foo1 : Nat → Foo |
--- a/tests/negative/Internal/LiteralInteger.juvix
+++ b/tests/negative/Internal/LiteralInteger.juvix
@ -0,0 +1,6 @@
+module LiteralInteger;
+
+open import Stdlib.Prelude;
+
+h : Nat;
+h := div 1 -2;
--- a/tests/negative/Internal/LiteralIntegerString.juvix
+++ b/tests/negative/Internal/LiteralIntegerString.juvix
@ -0,0 +1,9 @@
+module LiteralIntegerString;
+
+open import Stdlib.Prelude;
+
+f : String -> Nat;
+f _ := 0;
+
+g : Nat;
+g := f 2;
--- a/tests/positive/Reachability/O.juvix
+++ b/tests/positive/Reachability/O.juvix
@ -1,7 +1,7 @@
 module O;

 open import M public;
-open import Stdlib.Prelude;
+open import Stdlib.Data.Bool;

 k : Bool;
 k := true;
--- a/tests/smoke/Commands/dev/core.smoke.yaml
+++ b/tests/smoke/Commands/dev/core.smoke.yaml
@ -22,7 +22,7 @@ tests:
      - from-concrete
      - --eval
      - --transforms
-      - nat-to-int
+      - nat-to-primint
    args:
      - positive/Internal/LiteralInt.juvix
    stdout: |