From ea09ec30686b6c09514afa8d3acc8e0a11c505cb Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 13 Apr 2023 08:16:49 +0100 Subject: [PATCH] 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 --- juvix-stdlib | 2 +- .../Abstract/Extra/DependencyBuilder.hs | 1 + .../Abstract/Translation/FromConcrete.hs | 15 + src/Juvix/Compiler/Builtins.hs | 2 + src/Juvix/Compiler/Builtins/Int.hs | 390 ++++++++++++++++++ src/Juvix/Compiler/Concrete/Data/Builtins.hs | 51 ++- src/Juvix/Compiler/Core/Data/InfoTable.hs | 6 +- .../Compiler/Core/Data/InfoTableBuilder.hs | 96 ++++- .../Compiler/Core/Data/TransformationId.hs | 5 +- .../Core/Data/TransformationId/Parser.hs | 10 +- src/Juvix/Compiler/Core/Transformation.hs | 6 +- .../Transformation/ConvertBuiltinTypes.hs | 1 + .../Core/Transformation/IntToPrimInt.hs | 188 +++++++++ .../{NatToInt.hs => NatToPrimInt.hs} | 12 +- .../Compiler/Core/Translation/FromInternal.hs | 165 ++++---- .../Translation/FromInternal/Builtins/Int.hs | 39 ++ .../Translation/FromInternal/Builtins/Nat.hs | 25 ++ src/Juvix/Compiler/Internal/Language.hs | 18 +- src/Juvix/Compiler/Internal/Pretty/Base.hs | 9 +- .../Internal/Translation/FromAbstract.hs | 10 +- .../Analysis/TypeChecking/Checker.hs | 85 +++- src/Juvix/Extra/Strings.hs | 45 ++ test/Compilation/Positive.hs | 12 +- test/Reachability/Positive.hs | 2 +- test/Typecheck/Negative.hs | 14 + tests/Compilation/positive/out/test049.out | 31 ++ tests/Compilation/positive/out/test050.out | 1 + tests/Compilation/positive/test027.juvix | 2 +- tests/Compilation/positive/test049.juvix | 43 ++ tests/Compilation/positive/test050.juvix | 14 + tests/Internal/positive/Church.juvix | 2 +- .../Internal/positive/MatchConstructor.juvix | 2 +- tests/negative/Internal/LiteralInteger.juvix | 6 + .../Internal/LiteralIntegerString.juvix | 9 + tests/positive/Reachability/O.juvix | 2 +- tests/smoke/Commands/dev/core.smoke.yaml | 2 +- 36 files changed, 1186 insertions(+), 137 deletions(-) create mode 100644 src/Juvix/Compiler/Builtins/Int.hs create mode 100644 src/Juvix/Compiler/Core/Transformation/IntToPrimInt.hs rename src/Juvix/Compiler/Core/Transformation/{NatToInt.hs => NatToPrimInt.hs} (94%) create mode 100644 src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Int.hs create mode 100644 src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Nat.hs create mode 100644 tests/Compilation/positive/out/test049.out create mode 100644 tests/Compilation/positive/out/test050.out create mode 100644 tests/Compilation/positive/test049.juvix create mode 100644 tests/Compilation/positive/test050.juvix create mode 100644 tests/negative/Internal/LiteralInteger.juvix create mode 100644 tests/negative/Internal/LiteralIntegerString.juvix diff --git a/juvix-stdlib b/juvix-stdlib index dd5fa1215..ce3623ffb 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit dd5fa12156468a97deb96228b2c754fadef5ce92 +Subproject commit ce3623ffb0e8a0aa6c79cbb9a08eb14de5aef27f diff --git a/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs index fe0596586..e04059169 100644 --- 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) diff --git a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs index 68aa8a2f3..b9281b82f 100644 --- 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) => diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs index 6b6224ef3..d3cadac94 100644 --- 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 diff --git a/src/Juvix/Compiler/Builtins/Int.hs b/src/Juvix/Compiler/Builtins/Int.hs new file mode 100644 index 000000000..da1715275 --- /dev/null +++ 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) diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 6b03669bd..c5090b9e3 100644 --- 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) diff --git a/src/Juvix/Compiler/Core/Data/InfoTable.hs b/src/Juvix/Compiler/Core/Data/InfoTable.hs index ea27369b1..921072f76 100644 --- 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 diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs index a85780362..181b909b5 100644 --- 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) diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs index 495775540..b2f92e349 100644 --- 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 = diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs index c07f9e9b9..8c41e4402 100644 --- 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" diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs index cae40f315..95fbbaa47 100644 --- 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 diff --git a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs index f3c554ec6..58b947f5b 100644 --- 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 diff --git a/src/Juvix/Compiler/Core/Transformation/IntToPrimInt.hs b/src/Juvix/Compiler/Core/Transformation/IntToPrimInt.hs new file mode 100644 index 000000000..7f99bf58c --- /dev/null +++ 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 diff --git a/src/Juvix/Compiler/Core/Transformation/NatToInt.hs b/src/Juvix/Compiler/Core/Transformation/NatToPrimInt.hs similarity index 94% rename from src/Juvix/Compiler/Core/Transformation/NatToInt.hs rename to src/Juvix/Compiler/Core/Transformation/NatToPrimInt.hs index 9c8351f61..7cbfc92bf 100644 --- a/src/Juvix/Compiler/Core/Transformation/NatToInt.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 -> diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index b518191ca..97977d014 100644 --- 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))) diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Int.hs b/src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Int.hs new file mode 100644 index 000000000..d552c162c --- /dev/null +++ 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 diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Nat.hs b/src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Nat.hs new file mode 100644 index 000000000..8d492e873 --- /dev/null +++ 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 diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index 759c9965f..c6e974924 100644 --- 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 diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 698f68f07..f16f5b631 100644 --- 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 diff --git a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs index c49b4248b..d976b936d 100644 --- 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) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index d96695abd..478c24e43 100644 --- 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 diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index d1d3304de..759cbeee5 100644 --- 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" diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 1398e5904..8ce3dd365 100644 --- 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") ] diff --git a/test/Reachability/Positive.hs b/test/Reachability/Positive.hs index 0497f60bd..272e79694 100644 --- 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" diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index f7cec3edf..8bddc0ef5 100644 --- 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 ] diff --git a/tests/Compilation/positive/out/test049.out b/tests/Compilation/positive/out/test049.out new file mode 100644 index 000000000..8edfdbac3 --- /dev/null +++ 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 diff --git a/tests/Compilation/positive/out/test050.out b/tests/Compilation/positive/out/test050.out new file mode 100644 index 000000000..b4de39476 --- /dev/null +++ b/tests/Compilation/positive/out/test050.out @@ -0,0 +1 @@ +11 diff --git a/tests/Compilation/positive/test027.juvix b/tests/Compilation/positive/test027.juvix index 124c9a266..8b9184426 100644 --- 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; diff --git a/tests/Compilation/positive/test049.juvix b/tests/Compilation/positive/test049.juvix new file mode 100644 index 000000000..e88bd8b9b --- /dev/null +++ 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); diff --git a/tests/Compilation/positive/test050.juvix b/tests/Compilation/positive/test050.juvix new file mode 100644 index 000000000..0127d8654 --- /dev/null +++ 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; diff --git a/tests/Internal/positive/Church.juvix b/tests/Internal/positive/Church.juvix index a761a20f7..13a84f47b 100644 --- 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; diff --git a/tests/Internal/positive/MatchConstructor.juvix b/tests/Internal/positive/MatchConstructor.juvix index 40dd42395..08a111de4 100644 --- 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 | diff --git a/tests/negative/Internal/LiteralInteger.juvix b/tests/negative/Internal/LiteralInteger.juvix new file mode 100644 index 000000000..c8aba7553 --- /dev/null +++ b/tests/negative/Internal/LiteralInteger.juvix @@ -0,0 +1,6 @@ +module LiteralInteger; + +open import Stdlib.Prelude; + +h : Nat; +h := div 1 -2; diff --git a/tests/negative/Internal/LiteralIntegerString.juvix b/tests/negative/Internal/LiteralIntegerString.juvix new file mode 100644 index 000000000..b38876aec --- /dev/null +++ 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; diff --git a/tests/positive/Reachability/O.juvix b/tests/positive/Reachability/O.juvix index de008d68b..ff84590a0 100644 --- 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; diff --git a/tests/smoke/Commands/dev/core.smoke.yaml b/tests/smoke/Commands/dev/core.smoke.yaml index 05bcb4479..69b899a88 100644 --- 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: |