From 20966688a6c36720063764439d1b344c8d55233c Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 18 Dec 2024 12:44:15 +0100 Subject: [PATCH 1/2] Make all top-level definitions mutually recursive --- .../FromParsed/Analysis/Scoping.hs | 20 +++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 077216e433..8d9212699a 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1262,9 +1262,10 @@ checkTypeSig TypeSig {..} = do checkFunctionDef :: forall r. (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) => + Bool -> FunctionDef 'Parsed -> Sem r (FunctionDef 'Scoped) -checkFunctionDef fdef@FunctionDef {..} = do +checkFunctionDef isTop fdef@FunctionDef {..} = do let FunctionLhs {..} = _functionDefLhs sigDoc' <- mapM checkJudoc _functionDefDoc (sig', sigBody') <- withLocalScope $ do @@ -1276,7 +1277,7 @@ checkFunctionDef fdef@FunctionDef {..} = do FunctionDefName name -> do name' <- if - | P.isFunctionLike fdef -> getReservedDefinitionSymbol name + | isTop || P.isFunctionLike fdef -> getReservedDefinitionSymbol name | otherwise -> reserveFunctionSymbol (fdef ^. functionDefLhs) return FunctionDefNameScoped @@ -1634,7 +1635,7 @@ checkModuleBody body = do body' <- fmap flattenSections . syntaxBlock - $ checkSections (mkSections body) + $ checkSections True (mkSections body) exported <- get >>= exportScope return (exported, body') where @@ -1672,9 +1673,10 @@ checkModuleBody body = do checkSections :: forall r. (Members '[HighlightBuilder, Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, State ScoperSyntax, Reader PackageId] r) => + Bool -> StatementSections 'Parsed -> Sem r (StatementSections 'Scoped) -checkSections sec = topBindings helper +checkSections isTop sec = topBindings helper where helper :: forall r'. @@ -1780,7 +1782,9 @@ checkSections sec = topBindings helper reserveDefinition :: Definition 'Parsed -> Sem r' (Maybe (Module 'Parsed 'ModuleLocal)) reserveDefinition = \case DefinitionSyntax s -> resolveSyntaxDef s $> Nothing - DefinitionFunctionDef d -> reserveFunctionLikeSymbol d >> return Nothing + DefinitionFunctionDef d + | isTop -> reserveFunctionSymbol (d ^. functionDefLhs) >> return Nothing + | otherwise -> reserveFunctionLikeSymbol d >> return Nothing DefinitionDeriving d -> reserveDerivingSymbol d >> return Nothing DefinitionAxiom d -> reserveAxiomSymbol d >> return Nothing DefinitionProjectionDef d -> reserveProjectionSymbol d >> return Nothing @@ -1836,7 +1840,7 @@ checkSections sec = topBindings helper goDefinition :: Definition 'Parsed -> Sem r' (Definition 'Scoped) goDefinition = \case DefinitionSyntax s -> DefinitionSyntax <$> checkSyntaxDef s - DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef d + DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef isTop d DefinitionDeriving d -> DefinitionDeriving <$> checkDeriving d DefinitionAxiom d -> DefinitionAxiom <$> checkAxiomDef d DefinitionInductive d -> DefinitionInductive <$> checkInductiveDef d @@ -2344,7 +2348,7 @@ checkLetStatements :: checkLetStatements = ignoreSyntax . fmap fromSections - . checkSections + . checkSections False . mkLetSections . toList where @@ -3034,7 +3038,7 @@ checkNamedArgumentFunctionDef :: NamedArgumentFunctionDef 'Parsed -> Sem r (NamedArgumentFunctionDef 'Scoped) checkNamedArgumentFunctionDef NamedArgumentFunctionDef {..} = do - def <- localBindings . ignoreSyntax $ checkFunctionDef _namedArgumentFunctionDef + def <- localBindings . ignoreSyntax $ checkFunctionDef False _namedArgumentFunctionDef return NamedArgumentFunctionDef { _namedArgumentFunctionDef = def From eca5c18ddcb8169d828953db9723cf1193ebc704 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 18 Dec 2024 17:40:13 +0100 Subject: [PATCH 2/2] fix recursive detection --- 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 | 26 ++++++++----------- .../Concrete/Translation/FromSource.hs | 24 +++++++++++------ src/Juvix/Compiler/Pipeline/Package/Loader.hs | 3 ++- tests/Compilation/positive/test090.juvix | 5 ++-- 7 files changed, 59 insertions(+), 28 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 8d9212699a..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 @@ -1262,10 +1262,9 @@ checkTypeSig TypeSig {..} = do checkFunctionDef :: forall r. (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) => - Bool -> FunctionDef 'Parsed -> Sem r (FunctionDef 'Scoped) -checkFunctionDef isTop fdef@FunctionDef {..} = do +checkFunctionDef fdef@FunctionDef {..} = do let FunctionLhs {..} = _functionDefLhs sigDoc' <- mapM checkJudoc _functionDefDoc (sig', sigBody') <- withLocalScope $ do @@ -1277,7 +1276,7 @@ checkFunctionDef isTop fdef@FunctionDef {..} = do FunctionDefName name -> do name' <- if - | isTop || P.isFunctionLike fdef -> getReservedDefinitionSymbol name + | P.isFunctionRecursive fdef -> getReservedDefinitionSymbol name | otherwise -> reserveFunctionSymbol (fdef ^. functionDefLhs) return FunctionDefNameScoped @@ -1635,7 +1634,7 @@ checkModuleBody body = do body' <- fmap flattenSections . syntaxBlock - $ checkSections True (mkSections body) + $ checkSections (mkSections body) exported <- get >>= exportScope return (exported, body') where @@ -1673,10 +1672,9 @@ checkModuleBody body = do checkSections :: forall r. (Members '[HighlightBuilder, Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, State ScoperSyntax, Reader PackageId] r) => - Bool -> StatementSections 'Parsed -> Sem r (StatementSections 'Scoped) -checkSections isTop sec = topBindings helper +checkSections sec = topBindings helper where helper :: forall r'. @@ -1782,9 +1780,7 @@ checkSections isTop sec = topBindings helper reserveDefinition :: Definition 'Parsed -> Sem r' (Maybe (Module 'Parsed 'ModuleLocal)) reserveDefinition = \case DefinitionSyntax s -> resolveSyntaxDef s $> Nothing - DefinitionFunctionDef d - | isTop -> reserveFunctionSymbol (d ^. functionDefLhs) >> return Nothing - | otherwise -> reserveFunctionLikeSymbol d >> return Nothing + DefinitionFunctionDef d -> reserveFunctionLikeSymbol d >> return Nothing DefinitionDeriving d -> reserveDerivingSymbol d >> return Nothing DefinitionAxiom d -> reserveAxiomSymbol d >> return Nothing DefinitionProjectionDef d -> reserveProjectionSymbol d >> return Nothing @@ -1840,7 +1836,7 @@ checkSections isTop sec = topBindings helper goDefinition :: Definition 'Parsed -> Sem r' (Definition 'Scoped) goDefinition = \case DefinitionSyntax s -> DefinitionSyntax <$> checkSyntaxDef s - DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef isTop d + DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef d DefinitionDeriving d -> DefinitionDeriving <$> checkDeriving d DefinitionAxiom d -> DefinitionAxiom <$> checkAxiomDef d DefinitionInductive d -> DefinitionInductive <$> checkInductiveDef d @@ -2348,7 +2344,7 @@ checkLetStatements :: checkLetStatements = ignoreSyntax . fmap fromSections - . checkSections False + . checkSections . mkLetSections . toList where @@ -3038,7 +3034,7 @@ checkNamedArgumentFunctionDef :: NamedArgumentFunctionDef 'Parsed -> Sem r (NamedArgumentFunctionDef 'Scoped) checkNamedArgumentFunctionDef NamedArgumentFunctionDef {..} = do - def <- localBindings . ignoreSyntax $ checkFunctionDef False _namedArgumentFunctionDef + def <- localBindings . ignoreSyntax $ checkFunctionDef _namedArgumentFunctionDef return NamedArgumentFunctionDef { _namedArgumentFunctionDef = def 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;