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.
anoma · Dec 19, 2024 · 58d1f43 · 58d1f43
1 parent cb10fe3
commit 58d1f43
Show file tree

Hide file tree

Showing 7 changed files with 52 additions and 17 deletions.
diff --git 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
@@ -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
@@ -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
@@ -432,15 +432,15 @@ reserveDerivingSymbol ::
   Sem r ()
 reserveDerivingSymbol f = do
   let lhs = f ^. derivingFunLhs
-  when (P.isLhsFunctionLike lhs) $
+  when (P.isLhsFunctionRecursive lhs) $
     void (reserveFunctionSymbol lhs)
 
 reserveFunctionLikeSymbol ::
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
   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
@@ -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 "<top level statement>" $ 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 "<function definition>" $ 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
@@ -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
@@ -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;