detect cycles in arity checker

anoma · Oct 25, 2023 · 7378c4c · 7378c4c
1 parent da7eed1
commit 7378c4c
Show file tree

Hide file tree

Showing 6 changed files with 95 additions and 33 deletions.
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
@@ -4,6 +4,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.C
   )
 where
 
+import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Internal.Extra
 import Juvix.Compiler.Internal.Extra qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
@@ -26,15 +27,15 @@ checkModuleIndexNoCache ::
   ModuleIndex ->
   Sem r Module
 checkModuleIndexNoCache (ModuleIndex Module {..}) = do
-  _moduleBody' <- checkModuleBody _moduleBody
+  _moduleBody' <- runReader @InsertedArgsStack mempty (checkModuleBody _moduleBody)
   return
     Module
       { _moduleBody = _moduleBody',
         ..
       }
 
 checkModuleBody ::
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) =>
+  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -58,7 +59,7 @@ checkImport ::
   Sem r Import
 checkImport = traverseOf importModule checkModuleIndex
 
-checkInductive :: forall r. (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => InductiveDef -> Sem r InductiveDef
+checkInductive :: forall r. (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => InductiveDef -> Sem r InductiveDef
 checkInductive d = do
   let _inductiveName = d ^. inductiveName
       _inductiveBuiltin = d ^. inductiveBuiltin
@@ -77,7 +78,7 @@ checkInductive d = do
         checkParam :: InductiveParameter -> Sem (State LocalVars ': r) InductiveParameter
         checkParam = return
 
-checkConstructor :: (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => ConstructorDef -> Sem r ConstructorDef
+checkConstructor :: (Members '[Reader InsertedArgsStack, Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => ConstructorDef -> Sem r ConstructorDef
 checkConstructor c = do
   let _inductiveConstructorName = c ^. inductiveConstructorName
       _inductiveConstructorPragmas = c ^. inductiveConstructorPragmas
@@ -86,10 +87,10 @@ checkConstructor c = do
   return ConstructorDef {..}
 
 -- | check the arity of some ty : Type
-checkType :: (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => Expression -> Sem r Expression
+checkType :: (Members '[Reader InsertedArgsStack, Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => Expression -> Sem r Expression
 checkType = checkExpression ArityUnit
 
-checkAxiom :: (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => AxiomDef -> Sem r AxiomDef
+checkAxiom :: (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => AxiomDef -> Sem r AxiomDef
 checkAxiom a = do
   let _axiomName = a ^. axiomName
       _axiomBuiltin = a ^. axiomBuiltin
@@ -98,7 +99,7 @@ checkAxiom a = do
   return AxiomDef {..}
 
 checkMutualStatement ::
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
+  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
   MutualStatement ->
   Sem r MutualStatement
 checkMutualStatement = \case
@@ -107,20 +108,20 @@ checkMutualStatement = \case
   StatementAxiom a -> StatementAxiom <$> checkAxiom a
 
 checkMutualBlockLet ::
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
+  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
   MutualBlockLet ->
   Sem r MutualBlockLet
 checkMutualBlockLet (MutualBlockLet funs) = MutualBlockLet <$> mapM checkFunctionDef funs
 
 checkMutualBlock ::
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
+  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
   MutualBlock ->
   Sem r MutualBlock
 checkMutualBlock (MutualBlock funs) = MutualBlock <$> mapM checkMutualStatement funs
 
 checkFunctionDef ::
   forall r.
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
+  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
   FunctionDef ->
   Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
@@ -146,7 +147,7 @@ checkFunctionDef FunctionDef {..} = do
 
 checkArgsInfo ::
   forall r.
-  (Members '[NameIdGen, Reader LocalVars, Error ArityCheckerError, Reader InfoTable] r) =>
+  (Members '[Reader InsertedArgsStack, NameIdGen, Reader LocalVars, Error ArityCheckerError, Reader InfoTable] r) =>
   [ArgInfo] ->
   [FunctionParameter] ->
   Sem r [ArgInfo]
@@ -170,7 +171,7 @@ checkArgsInfo defaults =
           withLocalVarMaybe ari (p ^. paramName) (go ds' ps')
 
 checkFunctionBody ::
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
+  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
   Arity ->
   Expression ->
   Sem r Expression
@@ -216,7 +217,9 @@ arityLet l = guessArity (l ^. letExpression)
 inferReplExpression :: (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => Expression -> Sem r Expression
 inferReplExpression e = do
   ari <- guessArity e
-  withEmptyLocalVars (checkExpression ari e)
+  withEmptyLocalVars
+    . runReader @InsertedArgsStack mempty
+    $ checkExpression ari e
 
 guessArity ::
   forall r.
@@ -481,7 +484,7 @@ checkConstructorApp ca = do
 
 checkCase ::
   forall r.
-  (Members '[Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) =>
+  (Members '[Reader InsertedArgsStack, Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) =>
   Arity ->
   Case ->
   Sem r Case
@@ -498,7 +501,7 @@ checkCase ari l = do
 
 checkLet ::
   forall r.
-  (Members '[Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) =>
+  (Members '[Reader InsertedArgsStack, Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) =>
   Arity ->
   Let ->
   Sem r Let
@@ -514,7 +517,7 @@ checkLet ari l = do
 
 checkLambda ::
   forall r.
-  (Members '[Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) =>
+  (Members '[Reader InsertedArgsStack, Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) =>
   Arity ->
   Lambda ->
   Sem r Lambda
@@ -624,14 +627,14 @@ typeArity = go
 
 checkExample ::
   forall r.
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, Reader LocalVars] r) =>
+  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError, Reader LocalVars] r) =>
   Example ->
   Sem r Example
 checkExample = traverseOf exampleExpression (checkExpression ArityUnknown)
 
 checkExpression ::
   forall r.
-  (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, Reader LocalVars] r) =>
+  (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError, Reader LocalVars] r) =>
   Arity ->
   Expression ->
   Sem r Expression
@@ -784,9 +787,20 @@ checkExpression hintArity expr = case expr of
           let argsWithAris :: [(InsertedArg, Arity)]
               argsWithAris = zip argsWithHoles (argsAris ++ repeat ArityUnknown)
           forM argsWithAris $ \(ia, argAri) -> do
-            -- TODO put context
-            let adjustCtx = case isa of
-            traverseOf (insertedArg . appArg) (checkExpression argAri) ia
+            checkDefaultArgCycle ia
+            let adjustCtx
+                  | ia ^. insertedArgDefault = over insertedArgsStack ((ia ^. insertedArgName) :)
+                  | otherwise = id
+            local adjustCtx (traverseOf (insertedArg . appArg) (checkExpression argAri) ia)
+          where
+            checkDefaultArgCycle :: InsertedArg -> Sem r ()
+            checkDefaultArgCycle ia = do
+              st <- asks (^. insertedArgsStack)
+              case span (/= (ia ^. insertedArgName)) st of
+                (_, []) -> return ()
+                (c, _) ->
+                  let cyc = NonEmpty.reverse (ia ^. insertedArgName :| c)
+                   in throw (ErrDefaultArgCycle (DefaultArgCycle cyc))
 
         addHoles ::
           Interval ->
@@ -818,11 +832,12 @@ checkExpression hintArity expr = case expr of
                     emitWithParameter isDef p (ApplicationArg Implicit h)
                   emit :: Bool -> Name -> ApplicationArg -> Sem (Output InsertedArg ': State Int ': r) ()
                   emit isDef n x = do
-                    output InsertedArg {
-                      _insertedArg = x,
-                      _insertedDefault = isDef,
-                      _insertedArgName = n
-                                       }
+                    output
+                      InsertedArg
+                        { _insertedArg = x,
+                          _insertedArgDefault = isDef,
+                          _insertedArgName = n
+                        }
                     modify' @Int succ
               case (ari, goargs) of
                 (ArityFunction (FunctionArity (p@ArityParameter {_arityParameterImplicit = Implicit}) r), (ApplicationArg Implicit e) : rest) -> do

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs
@@ -1,18 +1,24 @@
 module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types where
 
+import Juvix.Compiler.Internal.Extra
 import Juvix.Compiler.Internal.Language
 import Juvix.Prelude
 import Juvix.Prelude.Pretty
-import Juvix.Compiler.Internal.Extra
+
+-- | Used to detect of cycles of default arguments in the arity checker.
+newtype InsertedArgsStack = InsertedArgsStack
+  { _insertedArgsStack :: [Name]
+  }
+  deriving newtype (Monoid, Semigroup)
 
 -- | Helper type used during insertion of default arguments in the arity
 -- checker.
-data InsertedArg = InsertedArg {
-  _insertedArgName :: Name,
-  _insertedArg :: ApplicationArg,
-  -- | True if this corresponds to an automatically inserted default argument.
-  -- False if it is an inserted hole or an argument present in the source code.
-  _insertedDefault :: Bool
+data InsertedArg = InsertedArg
+  { _insertedArgName :: Name,
+    _insertedArg :: ApplicationArg,
+    -- | True if this corresponds to an automatically inserted default argument.
+    -- False if it is an inserted hole or an argument present in the source code.
+    _insertedArgDefault :: Bool
   }
 
 data Arity
@@ -51,6 +57,7 @@ instance Eq ArityParameter where
 makeLenses ''UnfoldedArity
 makeLenses ''InsertedArg
 makeLenses ''ArityParameter
+makeLenses ''InsertedArgsStack
 
 arityParameterName :: Lens' ArityParameter (Maybe Name)
 arityParameterName = arityParameterInfo . argInfoName

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error.hs
@@ -16,6 +16,7 @@ data ArityCheckerError
   | ErrTooManyArguments TooManyArguments
   | ErrFunctionApplied FunctionApplied
   | ErrBuiltinNotFullyApplied BuiltinNotFullyApplied
+  | ErrDefaultArgCycle DefaultArgCycle
 
 instance ToGenericError ArityCheckerError where
   genericError :: (Member (Reader GenericOptions) r) => ArityCheckerError -> Sem r GenericError
@@ -28,3 +29,4 @@ instance ToGenericError ArityCheckerError where
     ErrTooManyArguments e -> genericError e
     ErrFunctionApplied e -> genericError e
     ErrBuiltinNotFullyApplied e -> genericError e
+    ErrDefaultArgCycle 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
@@ -262,3 +262,28 @@ instance ToGenericError BuiltinNotFullyApplied where
               <+> "must be applied to exactly"
               <+> pretty argsNum
               <+> "arguments"
+
+newtype DefaultArgCycle = DefaultArgCycle
+  { _defaultArgCycle :: NonEmpty Name
+  }
+
+makeLenses ''DefaultArgCycle
+
+instance ToGenericError DefaultArgCycle where
+  genericError DefaultArgCycle {..} = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = i,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = map getLoc (toList _defaultArgCycle)
+            }
+        where
+          opts' = fromGenericOptions opts
+          i = getLoc (head _defaultArgCycle)
+          ss = ppCode opts' <$> _defaultArgCycle
+          msg =
+            "Arity checker: There is a cyclic dependency between some default arguments:"
+              <> line
+              <> itemize ss
diff --git a/test/Arity/Negative.hs b/test/Arity/Negative.hs
@@ -104,5 +104,12 @@ tests =
       $(mkRelFile "issue2293.juvix")
       $ \case
         ErrWrongConstructorAppLength {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Detect default argument cycle in the arity checker"
+      $(mkRelDir "Internal")
+      $(mkRelFile "DefaultArgCycleArity.juvix")
+      $ \case
+        ErrDefaultArgCycle {} -> Nothing
         _ -> wrongError
   ]
diff --git a/tests/negative/Internal/DefaultArgCycleArity.juvix b/tests/negative/Internal/DefaultArgCycleArity.juvix
@@ -0,0 +1,6 @@
+module DefaultArgCycleArity;
+
+import Stdlib.Data.Nat.Base open;
+
+fun {a : Nat := 1} {b : Nat := fun + a + 1} {c : Nat := b + a + 1}
+  : Nat := a * b + c;