diff --git a/src/Juvix/Compiler/Core/Data/InfoTable.hs b/src/Juvix/Compiler/Core/Data/InfoTable.hs index 79787ff5dc..3b89a9cac5 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTable.hs @@ -18,6 +18,7 @@ data InfoTable = InfoTable _infoInductives :: HashMap Symbol InductiveInfo, _infoConstructors :: HashMap Tag ConstructorInfo, _infoAxioms :: HashMap Text AxiomInfo, + _infoIntToNat :: Maybe Symbol, _infoNextSymbol :: Word, _infoNextTag :: Word } @@ -32,6 +33,7 @@ emptyInfoTable = _infoInductives = mempty, _infoConstructors = mempty, _infoAxioms = mempty, + _infoIntToNat = Nothing, _infoNextSymbol = 0, _infoNextTag = 0 } diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs index 8293f5aa33..0cfe5830a3 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs @@ -85,3 +85,82 @@ runInfoTableBuilder tab = return $ HashMap.lookup txt (s ^. identMap) GetInfoTable -> get + +-------------------------------------------- +-- Builtin declarations +-------------------------------------------- + +createBuiltinConstr :: + Symbol -> + Tag -> + Text -> + Type -> + Maybe BuiltinConstructor -> + Sem r ConstructorInfo +createBuiltinConstr sym tag nameTxt ty cblt = do + return $ + ConstructorInfo + { _constructorName = nameTxt, + _constructorLocation = Nothing, + _constructorTag = tag, + _constructorType = ty, + _constructorArgsNum = length (typeArgs ty), + _constructorInductive = sym, + _constructorBuiltin = cblt + } + +declareInductiveBuiltins :: + Member InfoTableBuilder r => + Text -> + Maybe BuiltinInductive -> + [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> + Sem r () +declareInductiveBuiltins indName blt ctrs = do + sym <- freshSymbol + let ty = mkIdent' sym + constrs <- mapM (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) cblt) ctrs + registerInductive + indName + ( InductiveInfo + { _inductiveName = indName, + _inductiveLocation = Nothing, + _inductiveSymbol = sym, + _inductiveKind = mkDynamic', + _inductiveConstructors = constrs, + _inductivePositive = True, + _inductiveParams = [], + _inductiveBuiltin = blt + } + ) + mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) constrs + +declareIOBuiltins :: Member InfoTableBuilder r => Sem r () +declareIOBuiltins = + declareInductiveBuiltins + "IO" + Nothing + [ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing), + (BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing), + (BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing), + (BuiltinTag TagReadLn, "readLn", id, Nothing) + ] + +declareBoolBuiltins :: Member InfoTableBuilder r => Sem r () +declareBoolBuiltins = + declareInductiveBuiltins + "bool" + (Just BuiltinBool) + [ (BuiltinTag TagTrue, "true", id, Just BuiltinBoolTrue), + (BuiltinTag TagFalse, "false", id, Just BuiltinBoolFalse) + ] + +declareNatBuiltins :: Member InfoTableBuilder r => Sem r () +declareNatBuiltins = do + tagZero <- freshTag + tagSuc <- freshTag + declareInductiveBuiltins + "nat" + (Just BuiltinNat) + [ (tagZero, "zero", id, Just BuiltinNatZero), + (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc) + ] diff --git a/src/Juvix/Compiler/Core/Transformation/NatToInt.hs b/src/Juvix/Compiler/Core/Transformation/NatToInt.hs index b2d9dff51b..c43ffc1dea 100644 --- a/src/Juvix/Compiler/Core/Transformation/NatToInt.hs +++ b/src/Juvix/Compiler/Core/Transformation/NatToInt.hs @@ -17,6 +17,9 @@ convertNode tab = convert [] 0 go levels bl node = case node of NVar (Var {..}) -> End' (mkVar _varInfo (_varIndex + length (filter (\x -> x >= bl - _varIndex) levels))) + NApp (App _ (NIdt (Ident {..})) l) + | Just _identSymbol == tab ^. infoIntToNat -> + End' (convert levels bl l) NApp (App _ (NApp (App _ (NIdt (Ident {..})) l)) r) -> Recur' (levels, convertIdentApp node (\op -> mkBuiltinApp _identInfo op [l, r]) _identSymbol) NApp (App _ (NIdt (Ident {..})) l) -> @@ -90,4 +93,11 @@ convertNode tab = convert [] 0 _ -> node natToInt :: InfoTable -> InfoTable -natToInt tab = mapT (const (convertNode tab)) tab +natToInt tab = mapT (const (convertNode tab')) tab' + where + tab' = + case tab ^. infoIntToNat of + Just sym -> + tab {_identContext = HashMap.insert sym (mkLambda' (mkVar' 0)) (tab ^. identContext)} + Nothing -> + tab diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index e973b008a7..216d7fb846 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -28,21 +28,69 @@ isExplicit = (== Internal.Explicit) . (^. Internal.patternArgIsImplicit) mkIdentIndex :: Name -> Text mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId) +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 = "intToNat", + _identifierLocation = Nothing, + _identifierArgsNum = 1, + _identifierArgsInfo = + [ ArgumentInfo + { _argumentName = "x", + _argumentLocation = Nothing, + _argumentType = mkTypePrim' (PrimInteger $ PrimIntegerInfo Nothing Nothing), + _argumentIsImplicit = Explicit + } + ], + _identifierType = mkDynamic', + _identifierIsExported = False, + _identifierBuiltin = Nothing + } + node = + case (tagZeroM, tagSucM, boolSymM) of + (Just tagZero, Just tagSuc, Just boolSym) -> + mkLambda' $ + 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' $ mkVar' 0 + tagZeroM = fmap ((^. constructorTag) . fst) $ uncons $ filter (\ci -> ci ^. constructorBuiltin == Just BuiltinNatZero) $ HashMap.elems (tab ^. infoConstructors) + tagSucM = fmap ((^. constructorTag) . fst) $ uncons $ filter (\ci -> ci ^. constructorBuiltin == Just BuiltinNatSuc) $ HashMap.elems (tab ^. infoConstructors) + boolSymM = fmap ((^. inductiveSymbol) . fst) $ uncons $ filter (\ind -> ind ^. inductiveBuiltin == Just BuiltinBool) $ HashMap.elems (tab ^. infoInductives) + fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult fromInternal i = do - (res, _) <- runInfoTableBuilder emptyInfoTable (runReader (i ^. InternalTyped.resultIdenTypes) f) + (res, _) <- runInfoTableBuilder tab0 (runReader (i ^. InternalTyped.resultIdenTypes) f) return $ CoreResult - { _coreResultTable = res, + { _coreResultTable = setupIntToNat intToNatSym res, _coreResultInternalTypedResult = i } where + tab0 :: InfoTable + tab0 = emptyInfoTable {_infoIntToNat = Just intToNatSym, _infoNextSymbol = intToNatSym + 1} + + intToNatSym :: Symbol + intToNatSym = 0 + f :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable] r => Sem r () f = do + declareIOBuiltins let resultModules = toList (i ^. InternalTyped.resultModules) - runNameIdGen (runReader (Internal.buildTable resultModules) (mapM_ coreModule resultModules)) + runReader (Internal.buildTable resultModules) (mapM_ coreModule resultModules) where - coreModule :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, NameIdGen] r => Internal.Module -> Sem r () + coreModule :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r => Internal.Module -> Sem r () coreModule m = do registerInductiveDefs m registerFunctionDefs m @@ -86,14 +134,14 @@ registerInductiveDefsBody body = mapM_ go (body ^. Internal.moduleStatements) registerFunctionDefs :: forall r. - Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, NameIdGen, Reader Internal.InfoTable] r => + Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r => Internal.Module -> Sem r () registerFunctionDefs m = registerFunctionDefsBody (m ^. Internal.moduleBody) registerFunctionDefsBody :: forall r. - Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, NameIdGen, Reader Internal.InfoTable] r => + Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r => Internal.ModuleBody -> Sem r () registerFunctionDefsBody body = mapM_ go (body ^. Internal.moduleStatements) @@ -173,7 +221,7 @@ goConstructor sym ctor = do goMutualBlock :: forall r. - Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, NameIdGen, Reader Internal.InfoTable] r => + Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r => Internal.MutualBlock -> Sem r () goMutualBlock m = do @@ -188,7 +236,7 @@ goMutualBlock m = do goFunctionDefIden :: forall r. - Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, NameIdGen] r => + Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable] r => (Internal.FunctionDef, Symbol) -> Sem r () goFunctionDefIden (f, sym) = do @@ -470,7 +518,9 @@ goExpression' :: Internal.Expression -> Sem r Node goExpression' = \case - Internal.ExpressionLiteral l -> return (goLiteral l) + Internal.ExpressionLiteral l -> do + tab <- getInfoTable + return (goLiteral (fromJust $ tab ^. infoIntToNat) l) Internal.ExpressionIden i -> case i of Internal.IdenVar n -> do k <- HashMap.lookupDefault impossible id_ <$> asks (^. indexTableVars) @@ -568,10 +618,10 @@ goApplication a = do _ -> app _ -> app -goLiteral :: LiteralLoc -> Node -goLiteral l = case l ^. withLocParam of +goLiteral :: Symbol -> LiteralLoc -> Node +goLiteral intToNat l = case l ^. withLocParam of Internal.LitString s -> mkLitConst (ConstString s) - Internal.LitInteger i -> mkLitConst (ConstInteger i) + Internal.LitInteger 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/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index de8b61808d..a4005dbad0 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -43,92 +43,13 @@ guardSymbolNotDefined sym err = do b <- lift $ checkSymbolDefined sym when b err -createBuiltinConstr :: - Symbol -> - Tag -> - Text -> - Type -> - Interval -> - Maybe BuiltinConstructor -> - Sem r ConstructorInfo -createBuiltinConstr sym tag nameTxt ty i cblt = do - return $ - ConstructorInfo - { _constructorName = nameTxt, - _constructorLocation = Just i, - _constructorTag = tag, - _constructorType = ty, - _constructorArgsNum = length (typeArgs ty), - _constructorInductive = sym, - _constructorBuiltin = cblt - } - -declareInductiveBuiltins :: - Member InfoTableBuilder r => - Text -> - Maybe BuiltinInductive -> - [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> - ParsecS r () -declareInductiveBuiltins indName blt ctrs = do - loc <- curLoc - let i = mkInterval loc loc - sym <- lift freshSymbol - let ty = mkIdent' sym - constrs <- lift $ mapM (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) i cblt) ctrs - lift $ - registerInductive - indName - ( InductiveInfo - { _inductiveName = indName, - _inductiveLocation = Just i, - _inductiveSymbol = sym, - _inductiveKind = mkDynamic', - _inductiveConstructors = constrs, - _inductivePositive = True, - _inductiveParams = [], - _inductiveBuiltin = blt - } - ) - lift $ mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) constrs - -declareIOBuiltins :: Member InfoTableBuilder r => ParsecS r () -declareIOBuiltins = - declareInductiveBuiltins - "IO" - Nothing - [ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing), - (BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing), - (BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing), - (BuiltinTag TagReadLn, "readLn", id, Nothing) - ] - -declareBoolBuiltins :: Member InfoTableBuilder r => ParsecS r () -declareBoolBuiltins = - declareInductiveBuiltins - "bool" - (Just BuiltinBool) - [ (BuiltinTag TagTrue, "true", id, Just BuiltinBoolTrue), - (BuiltinTag TagFalse, "false", id, Just BuiltinBoolFalse) - ] - -declareNatBuiltins :: Member InfoTableBuilder r => ParsecS r () -declareNatBuiltins = do - tagZero <- lift freshTag - tagSuc <- lift freshTag - declareInductiveBuiltins - "nat" - (Just BuiltinNat) - [ (tagZero, "zero", id, Just BuiltinNatZero), - (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc) - ] - parseToplevel :: Member InfoTableBuilder r => ParsecS r (Maybe Node) parseToplevel = do - declareIOBuiltins - declareBoolBuiltins - declareNatBuiltins + lift declareIOBuiltins + lift declareBoolBuiltins + lift declareNatBuiltins space P.endBy statement (kw kwSemicolon) r <- optional expression diff --git a/test/Internal/Eval/Positive.hs b/test/Internal/Eval/Positive.hs index f6994ad970..9a24774e79 100644 --- a/test/Internal/Eval/Positive.hs +++ b/test/Internal/Eval/Positive.hs @@ -100,12 +100,12 @@ tests = $(mkRelFile "NatMatch2.juvix") $(mkRelFile "out/NatMatch2.out"), PosTest - "Literal integer is Core integer" + "Literal Nat" $(mkRelDir ".") $(mkRelFile "LitInteger.juvix") $(mkRelFile "out/LitInteger.out"), PosTest - "Literal integer is Core string" + "Literal String" $(mkRelDir ".") $(mkRelFile "LitString.juvix") $(mkRelFile "out/LitString.out"), diff --git a/tests/CLI/Commands/repl.test b/tests/CLI/Commands/repl.test index 5ad1a36252..1527640fb3 100644 --- a/tests/CLI/Commands/repl.test +++ b/tests/CLI/Commands/repl.test @@ -90,3 +90,9 @@ $ juvix repl tests/Internal/positive/BuiltinBool.juvix $ juvix repl > /\// >= 0 + +< +1 + 2 +$ juvix repl +> /Stdlib.Prelude> suc \(suc \(suc zero\)\)/ +>= 0 \ No newline at end of file diff --git a/tests/Internal/positive/LitInteger.juvix b/tests/Internal/positive/LitInteger.juvix index 5b3cc87fed..7bcb282990 100644 --- a/tests/Internal/positive/LitInteger.juvix +++ b/tests/Internal/positive/LitInteger.juvix @@ -3,7 +3,7 @@ module LitInteger; open import Stdlib.Prelude public; main : Nat; -main := 1; +main := 1 + 2; nilNat : List Nat; nilNat := nil; diff --git a/tests/Internal/positive/out/LitInteger.out b/tests/Internal/positive/out/LitInteger.out index d00491fd7e..7574e3e74c 100644 --- a/tests/Internal/positive/out/LitInteger.out +++ b/tests/Internal/positive/out/LitInteger.out @@ -1 +1 @@ -1 +suc (suc (suc zero))