From 58d1f434bca3b3c07e9927d0152825c48764d4fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Thu, 19 Dec 2024 09:37:17 +0100 Subject: [PATCH] Make top-level definitions mutually recursive (#3250) All top-level definitions are now back to being recursive, except definitions with pattern-matching on the left-hand side, e.g., ``` (x, y) := ...; ``` is not recursive on the top level. --- src/Juvix/Compiler/Concrete/Extra.hs | 14 +++++++++++ src/Juvix/Compiler/Concrete/Gen.hs | 3 ++- src/Juvix/Compiler/Concrete/Language/Base.hs | 12 +++++++++- .../FromParsed/Analysis/Scoping.hs | 8 +++---- .../Concrete/Translation/FromSource.hs | 24 ++++++++++++------- src/Juvix/Compiler/Pipeline/Package/Loader.hs | 3 ++- tests/Compilation/positive/test090.juvix | 5 ++-- 7 files changed, 52 insertions(+), 17 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index 42859b64a3..a6c48347d9 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -10,6 +10,8 @@ module Juvix.Compiler.Concrete.Extra isBodyExpression, isFunctionLike, isLhsFunctionLike, + isFunctionRecursive, + isLhsFunctionRecursive, symbolParsed, ) where @@ -116,3 +118,15 @@ isLhsFunctionLike FunctionLhs {..} = notNull (_funLhsTypeSig ^. typeSigArgs) isFunctionLike :: FunctionDef 'Parsed -> Bool isFunctionLike d@FunctionDef {..} = isLhsFunctionLike (d ^. functionDefLhs) || (not . isBodyExpression) _functionDefBody + +isFunctionRecursive :: FunctionDef 'Parsed -> Bool +isFunctionRecursive d = case d ^. functionDefLhs . funLhsIsTop of + FunctionTop -> isLhsFunctionRecursive (d ^. functionDefLhs) + FunctionNotTop -> isFunctionLike d + +isLhsFunctionRecursive :: FunctionLhs 'Parsed -> Bool +isLhsFunctionRecursive d = case d ^. funLhsIsTop of + FunctionTop -> case d ^. funLhsName of + FunctionDefNamePattern {} -> False + FunctionDefName {} -> True + FunctionNotTop -> isLhsFunctionLike d diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs index 0c145247cb..1d34245e40 100644 --- a/src/Juvix/Compiler/Concrete/Gen.hs +++ b/src/Juvix/Compiler/Concrete/Gen.hs @@ -38,7 +38,8 @@ simplestFunctionDef funName funBody = _funLhsBuiltin = Nothing, _funLhsTerminating = Nothing, _funLhsInstance = Nothing, - _funLhsCoercion = Nothing + _funLhsCoercion = Nothing, + _funLhsIsTop = FunctionNotTop } in FunctionDef { _functionDefBody = SigBodyExpression funBody, diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index c61e9c583a..c4b5336c0f 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -760,6 +760,15 @@ instance Serialize FunctionDefNameScoped instance NFData FunctionDefNameScoped +data FunctionIsTop + = FunctionTop + | FunctionNotTop + deriving stock (Eq, Ord, Show, Generic) + +instance Serialize FunctionIsTop + +instance NFData FunctionIsTop + data FunctionDef (s :: Stage) = FunctionDef { _functionDefDoc :: Maybe (Judoc s), _functionDefPragmas :: Maybe ParsedPragmas, @@ -2957,7 +2966,8 @@ data FunctionLhs (s :: Stage) = FunctionLhs _funLhsInstance :: Maybe KeywordRef, _funLhsCoercion :: Maybe KeywordRef, _funLhsName :: FunctionSymbolType s, - _funLhsTypeSig :: TypeSig s + _funLhsTypeSig :: TypeSig s, + _funLhsIsTop :: FunctionIsTop } deriving stock (Generic) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 077216e433..cdbeb9468b 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -432,7 +432,7 @@ reserveDerivingSymbol :: Sem r () reserveDerivingSymbol f = do let lhs = f ^. derivingFunLhs - when (P.isLhsFunctionLike lhs) $ + when (P.isLhsFunctionRecursive lhs) $ void (reserveFunctionSymbol lhs) reserveFunctionLikeSymbol :: @@ -440,7 +440,7 @@ reserveFunctionLikeSymbol :: FunctionDef 'Parsed -> Sem r () reserveFunctionLikeSymbol f = - when (P.isFunctionLike f) $ + when (P.isFunctionRecursive f) $ void (reserveFunctionSymbol (f ^. functionDefLhs)) bindFixitySymbol :: @@ -1198,7 +1198,7 @@ checkDeriving Deriving {..} = do typeSig' <- withLocalScope (checkTypeSig _funLhsTypeSig) name' <- if - | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol name + | P.isLhsFunctionRecursive lhs -> getReservedDefinitionSymbol name | otherwise -> reserveFunctionSymbol lhs let defname' = FunctionDefNameScoped @@ -1276,7 +1276,7 @@ checkFunctionDef fdef@FunctionDef {..} = do FunctionDefName name -> do name' <- if - | P.isFunctionLike fdef -> getReservedDefinitionSymbol name + | P.isFunctionRecursive fdef -> getReservedDefinitionSymbol name | otherwise -> reserveFunctionSymbol (fdef ^. functionDefLhs) return FunctionDefNameScoped diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index df062611b7..dcf835ddde 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -40,7 +40,8 @@ import Juvix.Prelude.Pretty data FunctionSyntaxOptions = FunctionSyntaxOptions { _funAllowOmitType :: Bool, - _funAllowInstance :: Bool + _funAllowInstance :: Bool, + _funIsTop :: FunctionIsTop } data SigOptions = SigOptions @@ -475,7 +476,8 @@ derivingInstance = do let opts = FunctionSyntaxOptions { _funAllowOmitType = False, - _funAllowInstance = True + _funAllowInstance = True, + _funIsTop = FunctionTop } off <- P.getOffset _derivingFunLhs <- functionDefinitionLhs opts Nothing @@ -492,7 +494,8 @@ statement = P.label "" $ do let funSyntax = FunctionSyntaxOptions { _funAllowInstance = True, - _funAllowOmitType = False + _funAllowOmitType = False, + _funIsTop = FunctionTop } ms <- optional @@ -678,7 +681,8 @@ builtinFunctionDef = functionDefinition funSyntax . Just funSyntax = FunctionSyntaxOptions { _funAllowInstance = True, - _funAllowOmitType = False + _funAllowOmitType = False, + _funIsTop = FunctionTop } builtinStatement :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Statement 'Parsed) @@ -1019,7 +1023,8 @@ pnamedArgumentFunctionDef = do let funSyntax = FunctionSyntaxOptions { _funAllowOmitType = True, - _funAllowInstance = False + _funAllowInstance = False, + _funIsTop = FunctionNotTop } fun <- functionDefinition funSyntax Nothing return @@ -1130,7 +1135,8 @@ letFunDef = do funSyntax = FunctionSyntaxOptions { _funAllowOmitType = True, - _funAllowInstance = False + _funAllowInstance = False, + _funIsTop = FunctionNotTop } letStatement :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (LetStatement 'Parsed) @@ -1368,7 +1374,8 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "" $ do _funLhsCoercion, _funLhsName, _funLhsTypeSig, - _funLhsTerminating + _funLhsTerminating, + _funLhsIsTop = opts ^. funIsTop } parseArg :: forall r. (Members '[ParserResultBuilder, JudocStash, PragmasStash, Error ParserError] r) => SigOptions -> ParsecS r (SigArg 'Parsed) @@ -1674,7 +1681,8 @@ checkNoNamedApplicationMissingAt = recoverStashes $ do let funSyntax = FunctionSyntaxOptions { _funAllowOmitType = True, - _funAllowInstance = False + _funAllowInstance = False, + _funIsTop = FunctionNotTop } x <- P.observing diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs index 41ef36dc1b..44c60871f0 100644 --- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs +++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs @@ -97,7 +97,8 @@ toConcrete t p = run . runReader l $ do _funLhsBuiltin = Nothing, _funLhsName = FunctionDefName name', _funLhsInstance = Nothing, - _funLhsTypeSig + _funLhsTypeSig, + _funLhsIsTop = FunctionTop } return ( StatementFunctionDef diff --git a/tests/Compilation/positive/test090.juvix b/tests/Compilation/positive/test090.juvix index 0acf05b6f0..ec2894cbea 100644 --- a/tests/Compilation/positive/test090.juvix +++ b/tests/Compilation/positive/test090.juvix @@ -21,12 +21,13 @@ module Resource; x : Delta.Nat := Resource.x + Resource0.x; a : Delta.Nat := x * Resource.Gamma.x + test090.x; + b : Delta.Nat := 1900; end; open Resource.Delta; - a : Delta.Nat := a; + b : Delta.Nat := a; end; -- result: 31 -main : Delta.Nat := Resource.a; +main : Delta.Nat := Resource.b;