From c1d85c451e447dd8b1b82fe2fd4677d8ee9a117b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Fri, 10 Feb 2023 19:21:46 +0100 Subject: [PATCH] Give proper errors for incorrect application of lazy builtins (#1830) * Closes #1828 --- .../milestone/TicTacToe/Web/TicTacToe.juvix | 5 ++- .../Compiler/Core/Translation/FromInternal.hs | 22 ++-------- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 14 +++++++ .../Analysis/ArityChecking/Checker.hs | 41 +++++++++++++++++-- .../Analysis/ArityChecking/Error.hs | 2 + .../Analysis/ArityChecking/Error/Types.hs | 28 +++++++++++++ test/Arity/Negative.hs | 7 ++++ tests/negative/Internal/LazyBuiltin.juvix | 14 +++++++ 8 files changed, 110 insertions(+), 23 deletions(-) create mode 100644 tests/negative/Internal/LazyBuiltin.juvix diff --git a/examples/milestone/TicTacToe/Web/TicTacToe.juvix b/examples/milestone/TicTacToe/Web/TicTacToe.juvix index 52094edec..8711fbfdd 100644 --- a/examples/milestone/TicTacToe/Web/TicTacToe.juvix +++ b/examples/milestone/TicTacToe/Web/TicTacToe.juvix @@ -23,8 +23,11 @@ module Web.TicTacToe; IOUnit : IO; IOUnit := printString ""; + ioseq : IO → IO → IO; + ioseq x y := x >> y; + sequenceIO : List IO → IO; - sequenceIO := foldr (>>) IOUnit; + sequenceIO := foldr ioseq IOUnit; mapIO : {A : Type} → (A → IO) → List A → IO; mapIO f xs := sequenceIO (map f xs); diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 30dca2893..46ef7a957 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -624,7 +624,7 @@ goExpression' = \case varsNum <- asks (^. indexTableVarsNum) return (mkVar (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) (varsNum - k - 1)) Internal.IdenFunction n -> do - funInfoBuiltin <- getFunctionBuiltinInfo n + funInfoBuiltin <- Internal.getFunctionBuiltinInfo n case funInfoBuiltin of Just Internal.BuiltinBoolIf -> error "if must be called with 3 arguments" Just Internal.BuiltinBoolOr -> error "|| must be called with 2 arguments" @@ -655,7 +655,7 @@ goExpression' = \case Just _ -> error ("internal to core: not a constructor " <> txt) Nothing -> error ("internal to core: undeclared identifier: " <> txt) Internal.IdenAxiom n -> do - axiomInfoBuiltin <- getAxiomBuiltinInfo n + axiomInfoBuiltin <- Internal.getAxiomBuiltinInfo n case axiomInfoBuiltin of Just Internal.BuiltinIOSequence -> error ">> must be called with 2 arguments" Just Internal.BuiltinTrace -> error "trace must be called with 2 arguments" @@ -721,7 +721,7 @@ goApplication a = do case f of Internal.ExpressionIden (Internal.IdenAxiom n) -> do - axiomInfoBuiltin <- getAxiomBuiltinInfo n + axiomInfoBuiltin <- Internal.getAxiomBuiltinInfo n case axiomInfoBuiltin of Just Internal.BuiltinNatPrint -> app Just Internal.BuiltinStringPrint -> app @@ -748,7 +748,7 @@ goApplication a = do Just Internal.BuiltinFail -> app Nothing -> app Internal.ExpressionIden (Internal.IdenFunction n) -> do - funInfoBuiltin <- getFunctionBuiltinInfo n + funInfoBuiltin <- Internal.getFunctionBuiltinInfo n case funInfoBuiltin of Just Internal.BuiltinBoolIf -> do sym <- getBoolSymbol @@ -778,17 +778,3 @@ goLiteral intToNat l = case l ^. withLocParam of where mkLitConst :: ConstantValue -> Node mkLitConst = mkConstant (Info.singleton (LocationInfo (l ^. withLocInt))) - -getAxiomBuiltinInfo :: Member (Reader Internal.InfoTable) r => Name -> Sem r (Maybe BuiltinAxiom) -getAxiomBuiltinInfo n = do - maybeAxiomInfo <- HashMap.lookup n <$> asks (^. Internal.infoAxioms) - return $ case maybeAxiomInfo of - Just axiomInfo -> axiomInfo ^. Internal.axiomInfoBuiltin - Nothing -> Nothing - -getFunctionBuiltinInfo :: Member (Reader Internal.InfoTable) r => Name -> Sem r (Maybe BuiltinFunction) -getFunctionBuiltinInfo n = do - maybeFunInfo <- HashMap.lookup n <$> asks (^. Internal.infoFunctions) - return $ case maybeFunInfo of - Just funInfo -> funInfo ^. Internal.functionInfoDef . Internal.funDefBuiltin - Nothing -> Nothing diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index 8029e17d6..ceb546955 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -196,3 +196,17 @@ constructorReturnType c = do ind inductiveParams return saturatedTy + +getAxiomBuiltinInfo :: Member (Reader InfoTable) r => Name -> Sem r (Maybe BuiltinAxiom) +getAxiomBuiltinInfo n = do + maybeAxiomInfo <- HashMap.lookup n <$> asks (^. infoAxioms) + return $ case maybeAxiomInfo of + Just axiomInfo -> axiomInfo ^. axiomInfoBuiltin + Nothing -> Nothing + +getFunctionBuiltinInfo :: Member (Reader InfoTable) r => Name -> Sem r (Maybe BuiltinFunction) +getFunctionBuiltinInfo n = do + maybeFunInfo <- HashMap.lookup n <$> asks (^. infoFunctions) + return $ case maybeFunInfo of + Just funInfo -> funInfo ^. functionInfoDef . funDefBuiltin + Nothing -> Nothing diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs index fbb32fb41..acfa02506 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs @@ -477,8 +477,8 @@ checkExpression :: Expression -> Sem r Expression checkExpression hintArity expr = case expr of - ExpressionIden {} -> appHelper expr [] - ExpressionApplication a -> goApp a + ExpressionIden {} -> goApp expr [] + ExpressionApplication a -> uncurry goApp $ second toList (unfoldApplication' a) ExpressionLiteral {} -> appHelper expr [] ExpressionFunction {} -> return expr ExpressionUniverse {} -> return expr @@ -488,8 +488,41 @@ checkExpression hintArity expr = case expr of ExpressionLet l -> ExpressionLet <$> checkLet hintArity l ExpressionCase l -> ExpressionCase <$> checkCase hintArity l where - goApp :: Application -> Sem r Expression - goApp = uncurry appHelper . second toList . unfoldApplication' + goApp :: Expression -> [(IsImplicit, Expression)] -> Sem r Expression + goApp f args = do + case f of + ExpressionIden (IdenAxiom n) -> do + blt <- getAxiomBuiltinInfo n + case blt of + Just BuiltinIOSequence -> goBuiltinApp n 0 2 f args + Just BuiltinTrace -> goBuiltinApp n 2 2 f args + _ -> appHelper f args + ExpressionIden (IdenFunction n) -> do + blt <- getFunctionBuiltinInfo n + case blt of + Just BuiltinBoolIf -> goBuiltinApp n 1 3 f args + Just BuiltinBoolOr -> goBuiltinApp n 0 2 f args + Just BuiltinBoolAnd -> goBuiltinApp n 0 2 f args + _ -> appHelper f args + _ -> appHelper f args + + goBuiltinApp :: Name -> Int -> Int -> Expression -> [(IsImplicit, Expression)] -> Sem r Expression + goBuiltinApp n implArgsNum argsNum f args = do + args' <- goImplArgs implArgsNum args + if + | length args' >= argsNum -> appHelper f args + | otherwise -> + throw $ + ErrBuiltinNotFullyApplied + BuiltinNotFullyApplied + { _builtinNotFullyAppliedName = n, + _builtinNotFullyAplliedExpectedArgsNum = argsNum + } + where + goImplArgs :: Int -> [(IsImplicit, Expression)] -> Sem r [(IsImplicit, Expression)] + goImplArgs 0 as = return as + goImplArgs k ((Implicit, _) : as) = goImplArgs (k - 1) as + goImplArgs _ as = return as appHelper :: Expression -> [(IsImplicit, Expression)] -> Sem r Expression appHelper fun0 args = do diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error.hs index b0a3a948d..9e9c577bf 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error.hs @@ -15,6 +15,7 @@ data ArityCheckerError | ErrPatternFunction PatternFunction | ErrTooManyArguments TooManyArguments | ErrFunctionApplied FunctionApplied + | ErrBuiltinNotFullyApplied BuiltinNotFullyApplied instance ToGenericError ArityCheckerError where genericError :: (Member (Reader GenericOptions) r) => ArityCheckerError -> Sem r GenericError @@ -26,3 +27,4 @@ instance ToGenericError ArityCheckerError where ErrPatternFunction e -> genericError e ErrTooManyArguments e -> genericError e ErrFunctionApplied e -> genericError e + ErrBuiltinNotFullyApplied e -> genericError e diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error/Types.hs index 70fb4ee81..977244e67 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error/Types.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error/Types.hs @@ -232,3 +232,31 @@ instance ToGenericError FunctionApplied where <> softline <> "In the application" <+> ppApp opts' (fun, args) + +data BuiltinNotFullyApplied = BuiltinNotFullyApplied + { _builtinNotFullyAppliedName :: Name, + _builtinNotFullyAplliedExpectedArgsNum :: Int + } + +makeLenses ''BuiltinNotFullyApplied + +instance ToGenericError BuiltinNotFullyApplied where + genericError e = ask >>= generr + where + generr opts = + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = ppOutput msg, + _genericErrorIntervals = [i] + } + where + opts' = fromGenericOptions opts + i = getLoc (e ^. builtinNotFullyAppliedName) + argsNum = e ^. builtinNotFullyAplliedExpectedArgsNum + msg = + "The lazy builtin" + <+> ppCode opts' (e ^. builtinNotFullyAppliedName) + <+> "must be applied to exactly" + <+> pretty argsNum + <+> "arguments" diff --git a/test/Arity/Negative.hs b/test/Arity/Negative.hs index 0834e6d81..d3e2cb07a 100644 --- a/test/Arity/Negative.hs +++ b/test/Arity/Negative.hs @@ -92,5 +92,12 @@ tests = $(mkRelFile "WrongReturnTypeTooManyArguments.juvix") $ \case ErrTooManyArguments {} -> Nothing + _ -> wrongError, + NegTest + "Lazy builtin not fully applied" + $(mkRelDir "Internal") + $(mkRelFile "LazyBuiltin.juvix") + $ \case + ErrBuiltinNotFullyApplied {} -> Nothing _ -> wrongError ] diff --git a/tests/negative/Internal/LazyBuiltin.juvix b/tests/negative/Internal/LazyBuiltin.juvix new file mode 100644 index 000000000..b5782fb2b --- /dev/null +++ b/tests/negative/Internal/LazyBuiltin.juvix @@ -0,0 +1,14 @@ +module LazyBuiltin; + +builtin bool type Bool := + | true : Bool + | false : Bool; + +builtin bool-if if : {A : Type} -> Bool -> A -> A -> A; +if true x _ := x; +if false _ x := x; + +f : Bool -> Bool; +f x := if x; + +end;