Report termination errors after typechecking (#2318)

- Closes #2293.
- Closes #2319 

I've added an effect for termination. It keeps track of which functions
failed the termination checker, which is run just after translating to
Internal. During typechecking, non-terminating functions are not
normalized. After typechecking, if there is at least one function which
failed the termination checker, an error is reported.
Additionally, we now properly check for termination of functions defined
in a let expression in the repl.

app/App.hs

@@ -4,6 +4,7 @@ import CommonOptions
 import Data.ByteString qualified as ByteString
 import GlobalOptions
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Pipeline
 import Juvix.Data.Error qualified as Error
 import Juvix.Extra.Paths.Base
@@ -146,6 +147,13 @@ getEntryPoint inputFile = do
   _runAppIOArgsRoots <- askRoots
   embed (getEntryPoint' (RunAppIOArgs {..}) inputFile)
 
+runPipelineTermination :: (Member App r) => AppPath File -> Sem (Termination ': PipelineEff) a -> Sem r a
+runPipelineTermination input p = do
+  r <- runPipelineEither input (evalTermination iniTerminationState p)
+  case r of
+    Left err -> exitJuvixError err
+    Right res -> return (snd res)
+
 runPipeline :: (Member App r) => AppPath File -> Sem PipelineEff a -> Sem r a
 runPipeline input p = do
   r <- runPipelineEither input p

app/Commands/Dev/Internal/Arity.hs

@@ -8,5 +8,5 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.D
 runCommand :: (Members '[Embed IO, App] r) => InternalArityOptions -> Sem r ()
 runCommand opts = do
   globalOpts <- askGlobalOptions
-  micro <- head . (^. InternalArity.resultModules) <$> runPipeline (opts ^. internalArityInputFile) upToInternalArity
+  micro <- head . (^. InternalArity.resultModules) <$> runPipelineTermination (opts ^. internalArityInputFile) upToInternalArity
   renderStdOut (Internal.ppOut globalOpts micro)

app/Commands/Dev/Internal/Pretty.hs

@@ -8,5 +8,5 @@ import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
 runCommand :: (Members '[Embed IO, App] r) => InternalPrettyOptions -> Sem r ()
 runCommand opts = do
   globalOpts <- askGlobalOptions
-  intern <- head . (^. Internal.resultModules) <$> runPipeline (opts ^. internalPrettyInputFile) upToInternal
+  intern <- head . (^. Internal.resultModules) <$> runPipelineTermination (opts ^. internalPrettyInputFile) upToInternal
   renderStdOut (Internal.ppOut globalOpts intern)

app/Commands/Dev/Internal/Reachability.hs

@@ -8,5 +8,5 @@ import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
 runCommand :: (Members '[Embed IO, App] r) => InternalReachabilityOptions -> Sem r ()
 runCommand opts = do
   globalOpts <- askGlobalOptions
-  depInfo <- (^. Internal.resultDepInfo) <$> runPipeline (opts ^. internalReachabilityInputFile) upToInternal
+  depInfo <- (^. Internal.resultDepInfo) <$> runPipelineTermination (opts ^. internalReachabilityInputFile) upToInternal
   renderStdOut (Internal.ppOut globalOpts depInfo)

app/Commands/Dev/Termination/CallGraph.hs

@@ -12,13 +12,13 @@ import Juvix.Prelude.Pretty
 runCommand :: (Members '[Embed IO, App] r) => CallGraphOptions -> Sem r ()
 runCommand CallGraphOptions {..} = do
   globalOpts <- askGlobalOptions
-  results <- runPipeline _graphInputFile upToInternal
+  results <- runPipelineTermination _graphInputFile upToInternal
   let topModules = results ^. Internal.resultModules
       mainModule = head topModules
       toAnsiText' :: forall a. (HasAnsiBackend a, HasTextBackend a) => a -> Text
       toAnsiText' = toAnsiText (not (globalOpts ^. globalNoColors))
       infotable = Internal.buildTable topModules
-      callMap = Termination.buildCallMap infotable mainModule
+      callMap = Termination.buildCallMap mainModule
       completeGraph = Termination.completeCallGraph callMap
       filteredGraph =
         maybe

app/Commands/Dev/Termination/Calls.hs

@@ -2,7 +2,6 @@ module Commands.Dev.Termination.Calls where
 
 import Commands.Base
 import Commands.Dev.Termination.Calls.Options
-import Juvix.Compiler.Internal.Data.InfoTable qualified as Internal
 import Juvix.Compiler.Internal.Pretty qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination qualified as Termination
@@ -10,10 +9,9 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination qua
 runCommand :: (Members '[Embed IO, App] r) => CallsOptions -> Sem r ()
 runCommand localOpts@CallsOptions {..} = do
   globalOpts <- askGlobalOptions
-  results <- runPipeline _callsInputFile upToInternal
+  results <- runPipelineTermination _callsInputFile upToInternal
   let topModules = results ^. Internal.resultModules
-      infotable = Internal.buildTable topModules
+      callMap0 = Termination.buildCallMap (head topModules)
-      callMap0 = Termination.buildCallMap infotable (head topModules)
       callMap = case _callsFunctionNameFilter of
         Nothing -> callMap0
         Just f -> Termination.filterCallMap f callMap0

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -1,6 +1,12 @@
 module Juvix.Compiler.Internal.Translation.FromConcrete
-  ( module Juvix.Compiler.Internal.Translation.FromConcrete,
+  ( module Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context,
-    module Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context,
+    fromConcrete,
+    MCache,
+    ConstructorInfos,
+    goModuleNoCache,
+    fromConcreteExpression,
+    fromConcreteImport,
+    fromConcreteOpenImport,
   )
 where
 
@@ -35,7 +41,7 @@ unsupported :: Text -> a
 unsupported msg = error $ msg <> "Scoped to Internal: not yet supported"
 
 fromConcrete ::
-  (Members '[Reader EntryPoint, Error JuvixError, Builtins, NameIdGen] r) =>
+  (Members '[Reader EntryPoint, Error JuvixError, Builtins, NameIdGen, Termination] r) =>
   Scoper.ScoperResult ->
   Sem r InternalResult
 fromConcrete _resultScoper =
@@ -127,23 +133,41 @@ buildLetMutualBlocks ss = nonEmpty' . mapMaybe nameToPreStatement $ scomponents
           AcyclicSCC a -> AcyclicSCC <$> a
           CyclicSCC p -> CyclicSCC . toList <$> nonEmpty (catMaybes p)
 
-fromConcreteExpression :: (Members '[Builtins, Error JuvixError, NameIdGen] r) => Scoper.Expression -> Sem r Internal.Expression
+fromConcreteExpression :: (Members '[Builtins, Error JuvixError, NameIdGen, Termination] r) => Scoper.Expression -> Sem r Internal.Expression
-fromConcreteExpression = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goExpression
+fromConcreteExpression e = do
+  e' <-
+    mapError (JuvixError @ScoperError)
+      . runReader @Pragmas mempty
+      . goExpression
+      $ e
+  checkTerminationShallow e'
+  return e'
 
 fromConcreteImport ::
-  (Members '[Reader ExportsTable, Error JuvixError, NameIdGen, Builtins, MCache] r) =>
+  (Members '[Reader ExportsTable, Error JuvixError, NameIdGen, Builtins, MCache, Termination] r) =>
   Scoper.Import 'Scoped ->
   Sem r Internal.Import
-fromConcreteImport =
+fromConcreteImport i = do
-  mapError (JuvixError @ScoperError)
+  i' <-
-    . runReader @Pragmas mempty
+    mapError (JuvixError @ScoperError)
-    . goImport
+      . runReader @Pragmas mempty
+      . goImport
+      $ i
+  checkTerminationShallow i'
+  return i'
 
 fromConcreteOpenImport ::
-  (Members '[Reader ExportsTable, Error JuvixError, NameIdGen, Builtins, MCache] r) =>
+  (Members '[Reader ExportsTable, Error JuvixError, NameIdGen, Builtins, MCache, Termination] r) =>
   Scoper.OpenModule 'Scoped ->
   Sem r (Maybe Internal.Import)
-fromConcreteOpenImport = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goOpenModule'
+fromConcreteOpenImport i = do
+  i' <-
+    mapError (JuvixError @ScoperError)
+      . runReader @Pragmas mempty
+      . goOpenModule
+      $ i
+  whenJust i' checkTerminationShallow
+  return i'
 
 goLocalModule ::
   (Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ConstructorInfos] r) =>
@@ -158,7 +182,7 @@ goTopModule ::
 goTopModule = cacheGet . ModuleIndex
 
 goModuleNoCache ::
-  (Members '[Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos] r) =>
+  (Members '[Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos, Termination] r) =>
   ModuleIndex ->
   Sem r Internal.Module
 goModuleNoCache (ModuleIndex m) = do
@@ -167,14 +191,7 @@ goModuleNoCache (ModuleIndex m) = do
   let depInfo = buildDependencyInfoPreModule p tbl
   r <- runReader depInfo (fromPreModule p)
   noTerminationOption <- asks (^. entryPointNoTermination)
-  -- TODO we should reuse this table
+  unless noTerminationOption (checkTerminationShallow r)
-  let itbl = buildTableShallow r
-  unless
-    noTerminationOption
-    ( mapError
-        (JuvixError @TerminationError)
-        (checkTermination itbl r)
-    )
   return r
 
 goPragmas :: (Member (Reader Pragmas) r) => Maybe ParsedPragmas -> Sem r Pragmas
@@ -356,11 +373,6 @@ goImport Import {..} = do
         }
     )
 
-guardNotCached :: (Bool, Internal.Module) -> Maybe Internal.Module
-guardNotCached (hit, m) = do
-  guard (not hit)
-  return m
-
 -- | Ignores functions
 goAxiomInductive ::
   forall r.
@@ -377,32 +389,24 @@ goAxiomInductive = \case
   StatementOpenModule {} -> return []
   StatementProjectionDef {} -> return []
 
-goOpenModule' ::
-  forall r.
-  (Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r) =>
-  OpenModule 'Scoped ->
-  Sem r (Maybe Internal.Import)
-goOpenModule' o =
-  case o ^. openModuleImportKw of
-    Just kw ->
-      case o ^. openModuleName of
-        ModuleRef' (SModuleTop :&: m) ->
-          Just
-            <$> goImport
-              Import
-                { _importKw = kw,
-                  _importModule = m,
-                  _importAsName = o ^. openImportAsName
-                }
-        _ -> impossible
-    Nothing -> return Nothing
-
 goOpenModule ::
   forall r.
   (Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r) =>
   OpenModule 'Scoped ->
   Sem r (Maybe Internal.Import)
-goOpenModule o = goOpenModule' o
+goOpenModule o = runFail $ do
+  case o ^. openModuleImportKw of
+    Nothing -> fail
+    Just kw ->
+      case o ^. openModuleName of
+        ModuleRef' (SModuleTop :&: m) ->
+          goImport
+            Import
+              { _importKw = kw,
+                _importModule = m,
+                _importAsName = o ^. openImportAsName
+              }
+        _ -> impossible
 
 goProjectionDef ::
   forall r.
@@ -977,8 +981,12 @@ goFunctionParameters FunctionParameters {..} = do
             Internal._paramImplicit = _paramImplicit,
             Internal._paramName = goSymbol <$> param
           }
-  return . fromMaybe (pure (mkParam Nothing)) . nonEmpty $
+  return
-    mkParam . goFunctionParameter <$> _paramNames
+    . fromMaybe (pure (mkParam Nothing))
+    . nonEmpty
+    $ mkParam
+      . goFunctionParameter
+      <$> _paramNames
   where
     goFunctionParameter :: FunctionParameter 'Scoped -> Maybe (SymbolType 'Scoped)
     goFunctionParameter = \case

src/Juvix/Compiler/Internal/Translation/FromInternal.hs

@@ -17,6 +17,7 @@ import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as ArityChecking
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking
 import Juvix.Compiler.Pipeline.Artifacts
 import Juvix.Compiler.Pipeline.EntryPoint
@@ -68,13 +69,12 @@ arityCheckImport i = do
 
 typeCheckExpressionType ::
   forall r.
-  (Members '[Error JuvixError, State Artifacts] r) =>
+  (Members '[Error JuvixError, State Artifacts, Termination] r) =>
   Expression ->
   Sem r TypedExpression
 typeCheckExpressionType exp = do
   table <- extendedTableReplArtifacts exp
-  mapError (JuvixError @TypeCheckerError)
+  runTypesTableArtifacts
-    . runTypesTableArtifacts
     . ignoreHighlightBuilder
     . runFunctionsTableArtifacts
     . runBuiltinsArtifacts
@@ -82,17 +82,19 @@ typeCheckExpressionType exp = do
     . runReader table
     . ignoreOutput @Example
     . withEmptyVars
+    . mapError (JuvixError @TypeCheckerError)
     . runInferenceDef
-    $ inferExpression' Nothing exp >>= traverseOf typedType strongNormalize
+    $ inferExpression' Nothing exp
+      >>= traverseOf typedType strongNormalize
 
 typeCheckExpression ::
-  (Members '[Error JuvixError, State Artifacts] r) =>
+  (Members '[Error JuvixError, State Artifacts, Termination] r) =>
   Expression ->
   Sem r Expression
 typeCheckExpression exp = (^. typedExpression) <$> typeCheckExpressionType exp
 
 typeCheckImport ::
-  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r) =>
+  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) =>
   Import ->
   Sem r Import
 typeCheckImport i = do
@@ -113,31 +115,34 @@ typeCheckImport i = do
     $ checkImport i
 
 typeChecking ::
+  forall r.
   (Members '[HighlightBuilder, Error JuvixError, Builtins, NameIdGen] r) =>
-  ArityChecking.InternalArityResult ->
+  Sem (Termination ': r) ArityChecking.InternalArityResult ->
   Sem r InternalTypedResult
-typeChecking res@ArityChecking.InternalArityResult {..} =
+typeChecking a = do
-  mapError (JuvixError @TypeCheckerError) $ do
+  (termin, (res, (normalized, (idens, (funs, r))))) <- runTermination iniTerminationState $ do
-    (normalized, (idens, (funs, r))) <-
+    res <- a
-      runOutputList
+    let table :: InfoTable
-        . runReader entryPoint
+        table = buildTable (res ^. ArityChecking.resultModules)
-        . runState (mempty :: TypesTable)
-        . runState (mempty :: FunctionsTable)
-        . runReader table
-        . evalCacheEmpty checkModuleNoCache
-        $ mapM checkModule _resultModules
-    return
-      InternalTypedResult
-        { _resultInternalArityResult = res,
-          _resultModules = r,
-          _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized],
-          _resultIdenTypes = idens,
-          _resultFunctions = funs,
-          _resultInfoTable = buildTable r
-        }
-  where
-    table :: InfoTable
-    table = buildTable _resultModules
 
-    entryPoint :: EntryPoint
+        entryPoint :: EntryPoint
-    entryPoint = res ^. ArityChecking.internalArityResultEntryPoint
+        entryPoint = res ^. ArityChecking.internalArityResultEntryPoint
+    fmap (res,)
+      . runOutputList
+      . runReader entryPoint
+      . runState (mempty :: TypesTable)
+      . runState (mempty :: FunctionsTable)
+      . runReader table
+      . mapError (JuvixError @TypeCheckerError)
+      . evalCacheEmpty checkModuleNoCache
+      $ mapM checkModule (res ^. ArityChecking.resultModules)
+  return
+    InternalTypedResult
+      { _resultInternalArityResult = res,
+        _resultModules = r,
+        _resultTermination = termin,
+        _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized],
+        _resultIdenTypes = idens,
+        _resultFunctions = funs,
+        _resultInfoTable = buildTable r
+      }

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/FunctionCall.hs

@@ -70,6 +70,12 @@ addCall fun c = over callMap (HashMap.alter (Just . insertCall c) fun)
       HashMap FunctionRef [FunCall]
     addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callRef) [fc]
 
+registerFunctionDef ::
+  (Members '[State CallMap] r) =>
+  FunctionDef ->
+  Sem r ()
+registerFunctionDef f = modify' (set ((callMapScanned . at (f ^. funDefName))) (Just f))
+
 registerCall ::
   (Members '[State CallMap, Reader FunctionRef] r) =>
   FunCall ->

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs

@@ -1,45 +1,110 @@
 module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
-  ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker,
+  ( Termination,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.FunctionCall,
+    buildCallMap,
-    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Error,
+    checkTerminationShallow,
+    runTermination,
+    evalTermination,
+    execTermination,
+    functionIsTerminating,
+    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.TerminationState,
   )
 where
 
 import Data.HashMap.Internal.Strict qualified as HashMap
-import Juvix.Compiler.Internal.Data.InfoTable as Internal
 import Juvix.Compiler.Internal.Language as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.FunctionCall
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.TerminationState
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Error
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.LexOrder
 import Juvix.Prelude
 
-checkTermination ::
+class Scannable a where
-  (Members '[Error TerminationError] r) =>
+  buildCallMap :: a -> CallMap
-  InfoTable ->
+
-  Module ->
+data Termination m a where
+  CheckTerminationShallow :: (Scannable a) => a -> Termination m ()
+  FunctionTermination :: FunctionRef -> Termination m IsTerminating
+
+makeSem ''Termination
+
+functionIsTerminating :: (Members '[Termination] r) => FunctionRef -> Sem r Bool
+functionIsTerminating = fmap terminates . functionTermination
+  where
+    terminates :: IsTerminating -> Bool
+    terminates = \case
+      TerminatingCheckedOrMarked -> True
+      TerminatingFailed -> False
+
+runTermination :: forall r a. (Members '[Error JuvixError] r) => TerminationState -> Sem (Termination ': r) a -> Sem r (TerminationState, a)
+runTermination ini m = do
+  res <- runState ini (re m)
+  checkNonTerminating (fst res)
+  return res
+  where
+    checkNonTerminating :: TerminationState -> Sem r ()
+    checkNonTerminating i =
+      whenJust (i ^. terminationFailedSet . to (nonEmpty . toList)) $
+        throw . JuvixError . ErrNoLexOrder . NoLexOrder
+
+evalTermination :: (Members '[Error JuvixError] r) => TerminationState -> Sem (Termination ': r) a -> Sem r a
+evalTermination s = fmap snd . runTermination s
+
+execTermination :: (Members '[Error JuvixError] r) => TerminationState -> Sem (Termination ': r) a -> Sem r TerminationState
+execTermination s = fmap fst . runTermination s
+
+instance Scannable Import where
+  buildCallMap = buildCallMap . (^. importModule . moduleIxModule)
+
+instance Scannable Module where
+  buildCallMap =
+    run
+      . execState emptyCallMap
+      . scanModule
+
+instance Scannable Expression where
+  buildCallMap =
+    run
+      . execState emptyCallMap
+      . scanTopExpression
+
+re :: Sem (Termination ': r) a -> Sem (State TerminationState ': r) a
+re = reinterpret $ \case
+  CheckTerminationShallow m -> checkTerminationShallow' m
+  FunctionTermination m -> functionTermination' m
+
+-- | If the function is missing, can we assume that it is not recursive
+functionTermination' ::
+  forall r.
+  (Members '[State TerminationState] r) =>
+  FunctionName ->
+  Sem r IsTerminating
+functionTermination' f = fromMaybe TerminatingCheckedOrMarked <$> gets (^. terminationTable . at f)
+
+-- | Returns the set of non-terminating functions. Does not go into imports.
+checkTerminationShallow' ::
+  forall r m.
+  (Members '[State TerminationState] r, Scannable m) =>
+  m ->
   Sem r ()
-checkTermination infotable topModule = do
+checkTerminationShallow' topModule = do
-  let callmap = buildCallMap infotable topModule
+  let callmap = buildCallMap topModule
       completeGraph = completeCallGraph callmap
       rEdges = reflexiveEdges completeGraph
       recBehav = map recursiveBehaviour rEdges
-  forM_ recBehav $ \r -> do
+  forM_ recBehav $ \rb -> do
-    let funName = r ^. recursiveBehaviourFun
+    let funName = rb ^. recursiveBehaviourFun
-        markedTerminating :: Bool = funInfo ^. (Internal.functionInfoDef . Internal.funDefTerminating)
+        markedTerminating :: Bool = funInfo ^. Internal.funDefTerminating
-        funInfo :: FunctionInfo
+        funInfo :: FunctionDef
-        funInfo = HashMap.lookupDefault err funName (infotable ^. Internal.infoFunctions)
+        funInfo = HashMap.lookupDefault err funName (callmap ^. callMapScanned)
           where
             err = error ("Impossible: function not found: " <> funName ^. nameText)
-    if
+        order = findOrder rb
-        | markedTerminating -> return ()
+    addTerminating funName $
-        | otherwise ->
+      if
-            case findOrder r of
+          | markedTerminating -> TerminatingCheckedOrMarked
-              Nothing -> throw (ErrNoLexOrder (NoLexOrder funName))
+          | Nothing <- order -> TerminatingFailed
-              Just _ -> return ()
+          | Just {} <- order -> TerminatingCheckedOrMarked
-
-buildCallMap :: InfoTable -> Module -> CallMap
-buildCallMap infotable = run . execState mempty . runReader infotable . scanModule
 
 scanModule ::
   (Members '[State CallMap] r) =>
@@ -48,31 +113,51 @@ scanModule ::
 scanModule m = scanModuleBody (m ^. moduleBody)
 
 scanModuleBody :: (Members '[State CallMap] r) => ModuleBody -> Sem r ()
-scanModuleBody body =
+scanModuleBody body = mapM_ scanStatement (body ^. moduleStatements)
-  mapM_ scanFunctionDef moduleFunctions
+
+scanStatement :: (Members '[State CallMap] r) => Statement -> Sem r ()
+scanStatement = \case
+  StatementAxiom a -> scanAxiom a
+  StatementMutual m -> scanMutual m
+
+scanMutual :: (Members '[State CallMap] r) => MutualBlock -> Sem r ()
+scanMutual (MutualBlock ss) = mapM_ scanMutualStatement ss
+
+scanInductive :: forall r. (Members '[State CallMap] r) => InductiveDef -> Sem r ()
+scanInductive i = do
+  scanTopExpression (i ^. inductiveType)
+  mapM_ scanConstructor (i ^. inductiveConstructors)
   where
-    moduleFunctions =
+    scanConstructor :: ConstructorDef -> Sem r ()
-      [ f | StatementMutual (MutualBlock m) <- body ^. moduleStatements, StatementFunction f <- toList m
+    scanConstructor c = scanTopExpression (c ^. inductiveConstructorType)
-      ]
+
+scanMutualStatement :: (Members '[State CallMap] r) => MutualStatement -> Sem r ()
+scanMutualStatement = \case
+  StatementInductive i -> scanInductive i
+  StatementFunction i -> scanFunctionDef i
+
+scanAxiom :: (Members '[State CallMap] r) => AxiomDef -> Sem r ()
+scanAxiom = scanTopExpression . (^. axiomType)
 
 scanFunctionDef ::
   (Members '[State CallMap] r) =>
   FunctionDef ->
   Sem r ()
-scanFunctionDef FunctionDef {..} =
+scanFunctionDef f@FunctionDef {..} = do
-  runReader _funDefName $ do
+  registerFunctionDef f
+  runReader (Just _funDefName) $ do
     scanTypeSignature _funDefType
     mapM_ scanFunctionClause _funDefClauses
 
 scanTypeSignature ::
-  (Members '[State CallMap, Reader FunctionRef] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef)] r) =>
   Expression ->
   Sem r ()
 scanTypeSignature = runReader emptySizeInfo . scanExpression
 
 scanFunctionClause ::
   forall r.
-  (Members '[State CallMap, Reader FunctionRef] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef)] r) =>
   FunctionClause ->
   Sem r ()
 scanFunctionClause FunctionClause {..} = go (reverse _clausePatterns) _clauseBody
@@ -86,7 +171,7 @@ scanFunctionClause FunctionClause {..} = go (reverse _clausePatterns) _clauseBod
         goClause (LambdaClause pats clBody) = go (reverse (toList pats) ++ revArgs) clBody
 
 scanCase ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Case ->
   Sem r ()
 scanCase c = do
@@ -94,13 +179,13 @@ scanCase c = do
   scanExpression (c ^. caseExpression)
 
 scanCaseBranch ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   CaseBranch ->
   Sem r ()
 scanCaseBranch = scanExpression . (^. caseBranchExpression)
 
 scanLet ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Let ->
   Sem r ()
 scanLet l = do
@@ -116,14 +201,20 @@ scanLetClause = \case
 scanMutualBlockLet :: (Members '[State CallMap] r) => MutualBlockLet -> Sem r ()
 scanMutualBlockLet MutualBlockLet {..} = mapM_ scanFunctionDef _mutualLet
 
+scanTopExpression ::
+  (Members '[State CallMap] r) =>
+  Expression ->
+  Sem r ()
+scanTopExpression = runReader (Nothing @FunctionRef) . runReader emptySizeInfo . scanExpression
+
 scanExpression ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Expression ->
   Sem r ()
 scanExpression e =
   viewCall e >>= \case
     Just c -> do
-      registerCall c
+      whenJustM (ask @(Maybe FunctionRef)) (\caller -> runReader caller (registerCall c))
       mapM_ (scanExpression . snd) (c ^. callArgs)
     Nothing -> case e of
       ExpressionApplication a -> scanApplication a
@@ -139,14 +230,14 @@ scanExpression e =
 
 scanSimpleLambda ::
   forall r.
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   SimpleLambda ->
   Sem r ()
 scanSimpleLambda SimpleLambda {..} = scanExpression _slambdaBody
 
 scanLambda ::
   forall r.
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Lambda ->
   Sem r ()
 scanLambda Lambda {..} = mapM_ scanClause _lambdaClauses
@@ -155,7 +246,7 @@ scanLambda Lambda {..} = mapM_ scanClause _lambdaClauses
     scanClause LambdaClause {..} = scanExpression _lambdaBody
 
 scanApplication ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Application ->
   Sem r ()
 scanApplication (Application l r _) = do
@@ -163,7 +254,7 @@ scanApplication (Application l r _) = do
   scanExpression r
 
 scanFunction ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   Function ->
   Sem r ()
 scanFunction (Function l r) = do
@@ -171,7 +262,7 @@ scanFunction (Function l r) = do
   scanExpression r
 
 scanFunctionParameter ::
-  (Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r) =>
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
   FunctionParameter ->
   Sem r ()
 scanFunctionParameter p = scanExpression (p ^. paramType)

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/FunctionCall.hs

@@ -9,10 +9,10 @@ import Juvix.Prelude
 
 type FunctionRef = FunctionName
 
-newtype CallMap = CallMap
+data CallMap = CallMap
-  { _callMap :: HashMap FunctionRef (HashMap FunctionRef [FunCall])
+  { _callMap :: HashMap FunctionRef (HashMap FunctionRef [FunCall]),
+    _callMapScanned :: HashMap FunctionRef FunctionDef
   }
-  deriving newtype (Semigroup, Monoid)
 
 data FunCall = FunCall
   { _callRef :: FunctionRef,
@@ -91,7 +91,7 @@ instance PrettyCode CallMap where
     (Members '[Reader Options] r) =>
     CallMap ->
     Sem r (Doc Ann)
-  ppCode (CallMap m) = vsep <$> mapM ppEntry (HashMap.toList m)
+  ppCode (CallMap m _) = vsep <$> mapM ppEntry (HashMap.toList m)
     where
       ppEntry :: (FunctionRef, HashMap FunctionRef [FunCall]) -> Sem r (Doc Ann)
       ppEntry (fun, mcalls) = do
@@ -115,3 +115,10 @@ kwQuestion = keyword Str.questionMark
 
 kwWaveArrow :: Doc Ann
 kwWaveArrow = keyword Str.waveArrow
+
+emptyCallMap :: CallMap
+emptyCallMap =
+  CallMap
+    { _callMap = mempty,
+      _callMapScanned = mempty
+    }

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/TerminationState.hs

@@ -0,0 +1,49 @@
+module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.TerminationState
+  ( IsTerminating (..),
+    TerminationState,
+    iniTerminationState,
+    addTerminating,
+    terminationTable,
+    terminationFailedSet,
+  )
+where
+
+import Data.HashSet qualified as HashSet
+import Juvix.Compiler.Internal.Language
+import Juvix.Prelude
+
+data IsTerminating
+  = -- | Has been checked or marked for termination.
+    TerminatingCheckedOrMarked
+  | -- | Has been checked for termination but failed.
+    TerminatingFailed
+
+data TerminationState = TerminationState
+  { _iterminationTable :: HashMap FunctionName IsTerminating,
+    _iterminationFailed :: HashSet FunctionName
+  }
+
+makeLenses ''TerminationState
+
+iniTerminationState :: TerminationState
+iniTerminationState =
+  TerminationState
+    { _iterminationTable = mempty,
+      _iterminationFailed = mempty
+    }
+
+addTerminating :: (Members '[State TerminationState] r) => FunctionName -> IsTerminating -> Sem r ()
+addTerminating f i = do
+  modify' (set (iterminationTable . at f) (Just i))
+  when isFailed (modify' (over iterminationFailed (HashSet.insert f)))
+  where
+    isFailed :: Bool
+    isFailed = case i of
+      TerminatingFailed -> True
+      TerminatingCheckedOrMarked -> False
+
+terminationTable :: SimpleGetter TerminationState (HashMap FunctionName IsTerminating)
+terminationTable = iterminationTable
+
+terminationFailedSet :: SimpleGetter TerminationState (HashSet FunctionName)
+terminationFailedSet = iterminationFailed

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Error/Types.hs

@@ -5,7 +5,7 @@ import Juvix.Data.PPOutput
 import Juvix.Prelude
 
 newtype NoLexOrder = NoLexOrder
-  { _noLexOrderFun :: Name
+  { _noLexOrderFun :: NonEmpty Name
   }
   deriving stock (Show)
 
@@ -20,11 +20,26 @@ instance ToGenericError NoLexOrder where
           _genericErrorIntervals = [i]
         }
     where
-      name = _noLexOrderFun
+      names = _noLexOrderFun
-      i = getLoc name
+      i = getLocSpan names
 
+      single = case names of
+        _ :| [] -> True
+        _ -> False
       msg :: Doc Ann
       msg = do
-        "The function"
+        "The following"
-          <+> code (pretty name)
+          <+> function
-          <+> "fails the termination checker."
+          <+> fails
+          <+> "the termination checker:"
+            <> line
+            <> itemize (fmap (code . pretty) names)
+        where
+          function :: Doc Ann
+          function
+            | single = "function"
+            | otherwise = "functions"
+          fails :: Doc Ann
+          fails
+            | single = "fails"
+            | otherwise = "fail"

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs

@@ -11,6 +11,7 @@ import Juvix.Compiler.Internal.Data.LocalVars
 import Juvix.Compiler.Internal.Extra
 import Juvix.Compiler.Internal.Pretty
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (Termination)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
@@ -43,7 +44,7 @@ checkModuleIndex ::
 checkModuleIndex = fmap ModuleIndex . cacheGet
 
 checkModuleNoCache ::
-  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination] r) =>
   ModuleIndex ->
   Sem r Module
 checkModuleNoCache (ModuleIndex Module {..}) = do
@@ -61,7 +62,7 @@ checkModuleNoCache (ModuleIndex Module {..}) = do
       }
 
 checkModuleBody ::
-  (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination] r) =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -74,13 +75,13 @@ checkModuleBody ModuleBody {..} = do
       }
 
 checkImport ::
-  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination] r) =>
   Import ->
   Sem r Import
 checkImport = traverseOf importModule checkModuleIndex
 
 checkStatement ::
-  (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) =>
   Statement ->
   Sem r Statement
 checkStatement s = case s of
@@ -91,7 +92,7 @@ checkStatement s = case s of
 
 checkInductiveDef ::
   forall r.
-  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Builtins] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Builtins, Termination] r) =>
   InductiveDef ->
   Sem r InductiveDef
 checkInductiveDef InductiveDef {..} = runInferenceDef $ do
@@ -155,14 +156,14 @@ withEmptyVars = runReader emptyLocalVars
 
 -- TODO should we register functions (type synonyms) first?
 checkTopMutualBlock ::
-  (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
+  (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) =>
   MutualBlock ->
   Sem r MutualBlock
 checkTopMutualBlock (MutualBlock ds) =
   MutualBlock <$> runInferenceDefs (mapM checkMutualStatement ds)
 
 checkMutualStatement ::
-  (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
+  (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) =>
   MutualStatement ->
   Sem r MutualStatement
 checkMutualStatement = \case
@@ -170,7 +171,7 @@ checkMutualStatement = \case
   StatementInductive f -> StatementInductive <$> checkInductiveDef f
 
 checkFunctionDef ::
-  (Members '[HighlightBuilder, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference] r) =>
+  (Members '[HighlightBuilder, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference, Termination] r) =>
   FunctionDef ->
   Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
@@ -188,7 +189,7 @@ checkFunctionDef FunctionDef {..} = do
   traverseOf funDefExamples (mapM checkExample) funDef
 
 checkIsType ::
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination] r) =>
   Interval ->
   Expression ->
   Sem r Expression
@@ -196,7 +197,7 @@ checkIsType = checkExpression . smallUniverseE
 
 checkDefType ::
   forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination] r) =>
   Expression ->
   Sem r Expression
 checkDefType ty = checkIsType loc ty
@@ -204,7 +205,7 @@ checkDefType ty = checkIsType loc ty
     loc = getLoc ty
 
 checkExample ::
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Output Example, State TypesTable, Termination] r) =>
   Example ->
   Sem r Example
 checkExample e = do
@@ -214,7 +215,7 @@ checkExample e = do
 
 checkExpression ::
   forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference, Output Example, State TypesTable, Termination] r) =>
   Expression ->
   Expression ->
   Sem r Expression
@@ -238,7 +239,7 @@ checkExpression expectedTy e = do
           )
 
 checkFunctionParameter ::
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination] r) =>
   FunctionParameter ->
   Sem r FunctionParameter
 checkFunctionParameter (FunctionParameter mv i e) = do
@@ -287,7 +288,7 @@ checkConstructorReturnType indType ctor = do
     )
 
 inferExpression ::
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination] r) =>
   Maybe Expression -> -- type hint
   Expression ->
   Sem r Expression
@@ -300,7 +301,7 @@ lookupVar v = HashMap.lookupDefault err v <$> asks (^. localTypes)
 
 checkFunctionClause ::
   forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Inference, Builtins, State TypesTable, Output Example, Reader LocalVars] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Inference, Builtins, State TypesTable, Output Example, Reader LocalVars, Termination] r) =>
   Expression ->
   FunctionClause ->
   Sem r FunctionClause
@@ -316,7 +317,7 @@ checkFunctionClause clauseType FunctionClause {..} = do
 -- | helper function for function clauses and lambda functions
 checkClause ::
   forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins, Output Example, State TypesTable, Termination] r) =>
   -- | Type
   Expression ->
   -- | Arguments
@@ -508,7 +509,7 @@ checkPattern = go
 
 inferExpression' ::
   forall r.
-  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Builtins] r) =>
+  (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Builtins, Termination] r) =>
   Maybe Expression ->
   Expression ->
   Sem r TypedExpression

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs

@@ -10,6 +10,7 @@ import Juvix.Compiler.Internal.Data.InfoTable
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context (InternalArityResult)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as Arity
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (TerminationState)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.FunctionsTable
 import Juvix.Compiler.Pipeline.EntryPoint qualified as E
 import Juvix.Prelude
@@ -21,6 +22,7 @@ type NormalizedTable = HashMap NameId Expression
 data InternalTypedResult = InternalTypedResult
   { _resultInternalArityResult :: InternalArityResult,
     _resultModules :: NonEmpty Module,
+    _resultTermination :: TerminationState,
     _resultNormalized :: NormalizedTable,
     _resultIdenTypes :: TypesTable,
     _resultFunctions :: FunctionsTable,

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs

@@ -8,6 +8,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Concrete.Data.Highlight.Input
 import Juvix.Compiler.Internal.Extra
 import Juvix.Compiler.Internal.Pretty
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.FunctionsTable
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
@@ -417,10 +418,16 @@ addIdens idens = do
   modify (HashMap.union idens)
   modify (over highlightTypes (HashMap.union idens))
 
--- | Assumes the given function has been type checked.
+-- | Assumes the given function has been type checked. Does *not* register the
--- Does *not* register the function.
+-- function.
--- Throws an error if the return type is Type and returns Nothing.
+-- Conditons:
-functionDefEval :: forall r'. (Members '[State FunctionsTable, Error TypeCheckerError] r') => FunctionDef -> Sem r' (Maybe Expression)
+-- 1. Only one clause.
+-- 2. No pattern matching.
+-- 3. Terminates.
+--
+-- Throws an error if the return type is Type and it does not satisfy the
+-- some condition.
+functionDefEval :: forall r'. (Members '[State FunctionsTable, Termination, Error TypeCheckerError] r') => FunctionDef -> Sem r' (Maybe Expression)
 functionDefEval f = do
   r <- runFail goTop
   retTy <- returnsType
@@ -439,12 +446,16 @@ functionDefEval f = do
     returnsType :: (Members '[State FunctionsTable] r) => Sem r Bool
     returnsType = isUniverse ret
 
-    goTop :: forall r. (Members '[Fail, State FunctionsTable, Error TypeCheckerError] r) => Sem r Expression
+    goTop :: forall r. (Members '[Fail, State FunctionsTable, Error TypeCheckerError, Termination] r) => Sem r Expression
-    goTop =
+    goTop = do
+      checkTerminating
       case f ^. funDefClauses of
         c :| [] -> goClause c
         _ -> fail
       where
+        checkTerminating :: Sem r ()
+        checkTerminating = unlessM (functionIsTerminating (f ^. funDefName)) fail
+
         goClause :: FunctionClause -> Sem r Expression
         goClause c = do
           let pats = c ^. clausePatterns
@@ -472,6 +483,6 @@ functionDefEval f = do
                 | Implicit <- p ^. patternArgIsImplicit -> fail
                 | otherwise -> go ps >>= goPattern (p ^. patternArgPattern, ty)
 
-registerFunctionDef :: (Members '[State FunctionsTable, Error TypeCheckerError] r) => FunctionDef -> Sem r ()
+registerFunctionDef :: (Members '[State FunctionsTable, Error TypeCheckerError, Termination] r) => FunctionDef -> Sem r ()
 registerFunctionDef f = whenJustM (functionDefEval f) $ \e ->
   modify (over functionsTable (HashMap.insert (f ^. funDefName) e))

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs

@@ -335,7 +335,7 @@ instance ToGenericError UnsupportedTypeFunction where
             <+> ppCode opts (_unsupportedTypeFunction ^. funDefName)
               <> "."
               <> line
-              <> "Only functions with a single clause and no pattern matching are supported."
+              <> "Only terminating functions with a single clause and no pattern matching are supported."
     return
       GenericError
         { _genericErrorLoc = i,

src/Juvix/Compiler/Pipeline.hs

@@ -29,6 +29,7 @@ import Juvix.Compiler.Core qualified as Core
 import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped
 import Juvix.Compiler.Internal qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as Arity
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Typed
 import Juvix.Compiler.Pipeline.Artifacts
 import Juvix.Compiler.Pipeline.EntryPoint
@@ -57,19 +58,19 @@ upToScoping ::
 upToScoping = upToParsing >>= Scoper.fromParsed
 
 upToInternal ::
-  (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver, Termination] r) =>
   Sem r Internal.InternalResult
 upToInternal = upToScoping >>= Internal.fromConcrete
 
 upToInternalArity ::
-  (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver, Termination] r) =>
   Sem r Internal.InternalArityResult
 upToInternalArity = upToInternal >>= Internal.arityChecking
 
 upToInternalTyped ::
   (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
   Sem r Internal.InternalTypedResult
-upToInternalTyped = upToInternalArity >>= Internal.typeChecking
+upToInternalTyped = Internal.typeChecking upToInternalArity
 
 upToInternalReachability ::
   (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
@@ -162,6 +163,9 @@ coreToVampIR' = Core.toVampIR' >=> return . VampIR.toResult . VampIR.fromCore
 runIOEither :: forall a. EntryPoint -> Sem PipelineEff a -> IO (Either JuvixError (ResolverState, a))
 runIOEither entry = fmap snd . runIOEitherHelper entry
 
+runIOEitherTermination :: forall a. EntryPoint -> Sem (Termination ': PipelineEff) a -> IO (Either JuvixError (ResolverState, a))
+runIOEitherTermination entry = fmap snd . runIOEitherHelper entry . evalTermination iniTerminationState
+
 runPipelineHighlight :: forall a. EntryPoint -> Sem PipelineEff a -> IO HighlightInput
 runPipelineHighlight entry = fmap fst . runIOEitherHelper entry
 
@@ -253,20 +257,22 @@ corePipelineIOEither entry = do
           mainModuleScope_ :: Scope
           mainModuleScope_ = Scoped.mainModuleSope scopedResult
        in Right $
-            foldl'
+            Artifacts
-              (flip ($))
+              { _artifactMainModuleScope = Just mainModuleScope_,
-              art
+                _artifactParsing = parserResult ^. P.resultBuilderState,
-              [ set artifactMainModuleScope (Just mainModuleScope_),
+                _artifactInternalModuleCache = internalResult ^. Internal.resultModulesCache,
-                set artifactParsing (parserResult ^. P.resultBuilderState),
+                _artifactInternalTypedTable = typedTable,
-                set artifactInternalModuleCache (internalResult ^. Internal.resultModulesCache),
+                _artifactTerminationState = typedResult ^. Typed.resultTermination,
-                set artifactInternalTypedTable typedTable,
+                _artifactCoreTable = coreTable,
-                set artifactCoreTable coreTable,
+                _artifactScopeTable = resultScoperTable,
-                set artifactScopeTable resultScoperTable,
+                _artifactScopeExports = scopedResult ^. Scoped.resultExports,
-                set artifactScopeExports (scopedResult ^. Scoped.resultExports),
+                _artifactTypes = typesTable,
-                set artifactTypes typesTable,
+                _artifactFunctions = functionsTable,
-                set artifactFunctions functionsTable,
+                _artifactScoperState = scopedResult ^. Scoped.resultScoperState,
-                set artifactScoperState (scopedResult ^. Scoped.resultScoperState)
+                _artifactResolver = art ^. artifactResolver,
-              ]
+                _artifactBuiltins = art ^. artifactBuiltins,
+                _artifactNameIdState = art ^. artifactNameIdState
+              }
   where
     initialArtifacts :: Artifacts
     initialArtifacts =
@@ -275,6 +281,7 @@ corePipelineIOEither entry = do
           _artifactMainModuleScope = Nothing,
           _artifactInternalTypedTable = mempty,
           _artifactTypes = mempty,
+          _artifactTerminationState = iniTerminationState,
           _artifactResolver = PathResolver.iniResolverState,
           _artifactNameIdState = allNameIds,
           _artifactFunctions = mempty,

src/Juvix/Compiler/Pipeline/Artifacts.hs

@@ -19,6 +19,7 @@ import Juvix.Compiler.Core.Data.InfoTableBuilder qualified as Core
 import Juvix.Compiler.Internal.Extra.DependencyBuilder (ExportsTable)
 import Juvix.Compiler.Internal.Language qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Prelude
@@ -37,6 +38,7 @@ data Artifacts = Artifacts
     _artifactScoperState :: Scoped.ScoperState,
     -- Concrete -> Internal
     _artifactInternalModuleCache :: Internal.ModulesCache,
+    _artifactTerminationState :: TerminationState,
     -- Typechecking
     _artifactTypes :: TypesTable,
     _artifactFunctions :: FunctionsTable,
@@ -93,6 +95,9 @@ runFunctionsTableArtifacts = runStateArtifacts artifactFunctions
 readerTypesTableArtifacts :: (Members '[State Artifacts] r) => Sem (Reader TypesTable ': r) a -> Sem r a
 readerTypesTableArtifacts = runReaderArtifacts artifactTypes
 
+runTerminationArtifacts :: (Members '[Error JuvixError, State Artifacts] r) => Sem (Termination ': r) a -> Sem r a
+runTerminationArtifacts = runStateLikeArtifacts runTermination artifactTerminationState
+
 runTypesTableArtifacts :: (Members '[State Artifacts] r) => Sem (State TypesTable ': r) a -> Sem r a
 runTypesTableArtifacts = runStateArtifacts artifactTypes
 
@@ -131,8 +136,8 @@ runFromConcreteCache ::
 runFromConcreteCache =
   runCacheArtifacts
     (artifactInternalModuleCache . Internal.cachedModules)
-    ( mapError (JuvixError @ScoperError)
+    $ mapError (JuvixError @ScoperError)
-        . runReader (mempty :: Pragmas)
+      . runReader (mempty :: Pragmas)
-        . evalState (mempty :: Internal.ConstructorInfos)
+      . evalState (mempty :: Internal.ConstructorInfos)
-        . Internal.goModuleNoCache
+      . runTerminationArtifacts
-    )
+      . Internal.goModuleNoCache

src/Juvix/Compiler/Pipeline/Repl.hs

@@ -11,12 +11,13 @@ import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
 import Juvix.Compiler.Core qualified as Core
 import Juvix.Compiler.Internal qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromConcrete qualified as FromConcrete
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Pipeline.Artifacts
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Prelude
 
 arityCheckExpression ::
-  (Members '[Error JuvixError, State Artifacts] r) =>
+  (Members '[Error JuvixError, State Artifacts, Termination] r) =>
   ExpressionAtoms 'Parsed ->
   Sem r Internal.Expression
 arityCheckExpression p = do
@@ -93,7 +94,7 @@ runToInternal m = do
     $ m
 
 openImportToInternal ::
-  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r) =>
+  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) =>
   OpenModule 'Parsed ->
   Sem r (Maybe Internal.Import)
 openImportToInternal o = runToInternal $ do
@@ -101,18 +102,18 @@ openImportToInternal o = runToInternal $ do
     >>= Internal.fromConcreteOpenImport
 
 importToInternal ::
-  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r) =>
+  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) =>
   Import 'Parsed ->
   Sem r Internal.Import
 importToInternal i = runToInternal $ do
   Scoper.scopeCheckImport i
     >>= Internal.fromConcreteImport
 
-importToInternal' ::
+importToInternalTyped ::
-  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r) =>
+  (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) =>
   Internal.Import ->
   Sem r Internal.Import
-importToInternal' = Internal.arityCheckImport >=> Internal.typeCheckImport
+importToInternalTyped = Internal.arityCheckImport >=> Internal.typeCheckImport
 
 parseReplInput ::
   (Members '[PathResolver, Files, State Artifacts, Error JuvixError] r) =>
@@ -132,32 +133,40 @@ expressionUpToTyped ::
   Sem r Internal.TypedExpression
 expressionUpToTyped fp txt = do
   p <- expressionUpToAtomsParsed fp txt
-  arityCheckExpression p
+  runTerminationArtifacts
-    >>= Internal.typeCheckExpressionType
+    ( arityCheckExpression p
+        >>= Internal.typeCheckExpressionType
+    )
 
 compileExpression ::
   (Members '[Error JuvixError, State Artifacts] r) =>
   ExpressionAtoms 'Parsed ->
   Sem r Core.Node
 compileExpression p = do
-  arityCheckExpression p
+  runTerminationArtifacts
-    >>= Internal.typeCheckExpression
+    ( arityCheckExpression p
+        >>= Internal.typeCheckExpression
+    )
     >>= fromInternalExpression
 
 registerImport ::
   (Members '[Error JuvixError, State Artifacts, Reader EntryPoint] r) =>
   Import 'Parsed ->
   Sem r ()
-registerImport =
+registerImport p =
-  importToInternal >=> importToInternal' >=> fromInternalImport
+  runTerminationArtifacts
+    ( importToInternal p
+        >>= importToInternalTyped
+    )
+    >>= fromInternalImport
 
 registerOpenImport ::
   (Members '[Error JuvixError, State Artifacts, Reader EntryPoint] r) =>
   OpenModule 'Parsed ->
   Sem r ()
-registerOpenImport o = do
+registerOpenImport o = ignoreFail $ do
-  mImport <- openImportToInternal o
+  mImport <- runTerminationArtifacts (openImportToInternal o >>= failMaybe >>= importToInternalTyped)
-  whenJust mImport (importToInternal' >=> fromInternalImport)
+  fromInternalImport mImport
 
 fromInternalImport :: (Members '[State Artifacts] r) => Internal.Import -> Sem r ()
 fromInternalImport i = do

test/Arity/Negative.hs

@@ -21,7 +21,7 @@ testDescr NegTest {..} =
           _testRoot = tRoot,
           _testAssertion = Single $ do
             entryPoint <- defaultEntryPointCwdIO file'
-            result <- runIOEither entryPoint upToInternalArity
+            result <- runIOEitherTermination entryPoint upToInternalArity
             case mapLeft fromJuvixError result of
               Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure
               Left Nothing -> assertFailure "The arity checker did not find an error."
@@ -97,5 +97,12 @@ tests =
       $(mkRelFile "LazyBuiltin.juvix")
       $ \case
         ErrBuiltinNotFullyApplied {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "issue 2293: Non-terminating function with arity error"
+      $(mkRelDir "Internal")
+      $(mkRelFile "issue2293.juvix")
+      $ \case
+        ErrWrongConstructorAppLength {} -> Nothing
         _ -> wrongError
   ]

test/Scope/Negative.hs

@@ -24,7 +24,7 @@ testDescr NegTest {..} =
           _testRoot = tRoot,
           _testAssertion = Single $ do
             entryPoint <- defaultEntryPointCwdIO file'
-            res <- runIOEither entryPoint upToInternal
+            res <- runIOEitherTermination entryPoint upToInternal
             case mapLeft fromJuvixError res of
               Left (Just err) -> whenJust (_checkErr err) assertFailure
               Left Nothing -> assertFailure "An error ocurred but it was not in the scoper."

test/Termination/Negative.hs

@@ -21,7 +21,7 @@ testDescr NegTest {..} =
           _testRoot = tRoot,
           _testAssertion = Single $ do
             entryPoint <- set entryPointNoStdlib True <$> defaultEntryPointCwdIO file'
-            result <- runIOEither entryPoint upToInternal
+            result <- runIOEither entryPoint upToInternalTyped
             case mapLeft fromJuvixError result of
               Left (Just lexError) -> whenJust (_checkErr lexError) assertFailure
               Left Nothing -> assertFailure "The termination checker did not find an error."
@@ -73,6 +73,12 @@ tests =
       "Quicksort is not terminating"
       $(mkRelDir ".")
       $(mkRelFile "Data/QuickSort.juvix")
+      $ \case
+        ErrNoLexOrder {} -> Nothing,
+    NegTest
+      "Loop in axiom type"
+      $(mkRelDir ".")
+      $(mkRelFile "Axiom.juvix")
       $ \case
         ErrNoLexOrder {} -> Nothing
   ]

test/Termination/Positive.hs

@@ -21,7 +21,7 @@ testDescr PosTest {..} =
           _testRoot = tRoot,
           _testAssertion = Single $ do
             entryPoint <- set entryPointNoStdlib True <$> defaultEntryPointCwdIO file'
-            (void . runIO' entryPoint) upToInternal
+            (void . runIO' entryPoint) upToInternalTyped
         }
 
 --------------------------------------------------------------------------------
@@ -43,7 +43,7 @@ testDescrFlag N.NegTest {..} =
               set entryPointNoTermination True
                 . set entryPointNoStdlib True
                 <$> defaultEntryPointCwdIO file'
-            (void . runIO' entryPoint) upToInternal
+            (void . runIO' entryPoint) upToInternalTyped
         }
 
 tests :: [PosTest]

test/Typecheck/Positive.hs

@@ -47,7 +47,7 @@ testNoPositivityFlag N.NegTest {..} =
             entryPoint <-
               set entryPointNoPositivity True
                 <$> defaultEntryPointCwdIO file'
-            (void . runIO' entryPoint) upToInternal
+            (void . runIO' entryPoint) upToInternalTyped
         }
 
 negPositivityTests :: [N.NegTest]

tests/negative/Internal/issue2293.juvix

@@ -0,0 +1,7 @@
+module issue2293;
+
+type List A := nil | cons A (List A);
+
+map {A B} (f : A → B) : List A → List B
+  | nil := nil
+  | cons h t := cons (f h) (map f t);

tests/negative/Termination/Axiom.juvix

@@ -0,0 +1,5 @@
+module Axiom;
+
+axiom A : let
+    x : Type := x;
+  in x;

tests/negative/Termination/Data/Bool.juvix

@@ -18,9 +18,9 @@ syntax operator && logical;
   | false _ := false
   | true a := a;
 
-ite : (a : Type) → Bool → a → a → a
+ite : {a : Type} → Bool → a → a → a
-  | _ true a _ := a
+  | true a _ := a
-  | _ false _ b := b;
+  | false _ b := b;
 
 not : Bool → Bool
   | true := false

tests/negative/Termination/Data/QuickSort.juvix

@@ -10,33 +10,30 @@ type List (A : Type) :=
   | nil : List A
   | cons : A → List A → List A;
 
-filter : (A : Type) → (A → Bool) → List A → List A
+filter : {A : Type} → (A → Bool) → List A → List A
-  | A f nil := nil A
+  | f nil := nil
-  | A f (cons h hs) :=
+  | f (cons h hs) :=
     ite
-      (List A)
       (f h)
-      (cons A h (filter A f hs))
+      (cons h (filter f hs))
-      (filter A f hs);
+      (filter f hs);
 
-concat : (A : Type) → List A → List A → List A
+concat : {A : Type} → List A → List A → List A
-  | A nil ys := ys
+  | nil ys := ys
-  | A (cons x xs) ys := cons A x (concat A xs ys);
+  | (cons x xs) ys := cons x (concat xs ys);
 
-ltx : (A : Type) → (A → A → Bool) → A → A → Bool
+ltx : {A : Type} → (A → A → Bool) → A → A → Bool
-  | A lessThan x y := lessThan y x;
+  | lessThan x y := lessThan y x;
 
-gex : (A : Type) → (A → A → Bool) → A → A → Bool
+gex : {A : Type} → (A → A → Bool) → A → A → Bool
-  | A lessThan x y := not (ltx A lessThan x y);
+  | lessThan x y := not (ltx lessThan x y);
 
-quicksort : (A : Type) → (A → A → Bool) → List A → List A
+quicksort : {A : Type} → (A → A → Bool) → List A → List A
-  | A _ nil := nil A
+  | _ nil := nil
-  | A _ (cons x nil) := cons A x (nil A)
+  | _ (cons x nil) := cons x nil
-  | A lessThan (cons x ys) :=
+  | lessThan (cons x ys) :=
     concat
-      A
+      (quicksort lessThan (filter (ltx lessThan x) ys))
-      (quicksort A lessThan (filter A (ltx A lessThan x) ys))
       (concat
-        A
+        (cons x nil)
-        (cons A x (nil A))
+        (quicksort lessThan (filter (gex lessThan x) ys)));
-        (quicksort A lessThan (filter A (gex A lessThan x)) ys));

tests/negative/Termination/Ord.juvix

@@ -17,4 +17,3 @@ addord : Ord -> Ord -> Ord
 aux-addord : (ℕ -> Ord) -> Ord -> ℕ -> Ord
   
   | f y z := addord (f z) y;
-

tests/smoke/Commands/repl.smoke.yaml

@@ -1,6 +1,20 @@
 working-directory: ./../../../tests/
 
 tests:
+  - name: repl-non-terminating
+    command:
+      - juvix
+      - repl
+    stdin: "let x : Bool := x in x"
+    stdout:
+      matches: |
+        .*
+    stderr:
+      contains: |
+        The following function fails the termination checker:
+        • x
+    exit-status: 0
+
   - name: repl-doc
     command:
       - juvix