Add the termination checker to the pipeline (#111)

* [WIP] EntryPoint now has options. --no-termination is a new global opt.

* Add TerminationChecking to the pipeline

* Add TerminationChecking to the pipeline

* Keep GlobalOptions in App

* Fix reviewer's comments

* delete unnecessary parens

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>

app/GlobalOptions.hs

@@ -1,6 +1,9 @@
 {-# LANGUAGE ApplicativeDo #-}
 
-module GlobalOptions where
+module GlobalOptions
+  ( module GlobalOptions,
+  )
+where
 
 import MiniJuvix.Prelude
 import Options.Applicative
@@ -8,8 +11,10 @@ import Options.Applicative
 data GlobalOptions = GlobalOptions
   { _globalNoColors :: Bool,
     _globalShowNameIds :: Bool,
-    _globalOnlyErrors :: Bool
+    _globalOnlyErrors :: Bool,
+    _globalNoTermination :: Bool
   }
+  deriving stock (Eq, Show)
 
 makeLenses ''GlobalOptions
 
@@ -30,4 +35,9 @@ parseGlobalOptions = do
       ( long "only-errors"
           <> help "Only print errors in a uniform format (used by minijuvix-mode)"
       )
+  _globalNoTermination <-
+    switch
+      ( long "no-termination"
+          <> help "Disable the termination checker"
+      )
   pure GlobalOptions {..}

app/Main.hs

@@ -66,40 +66,62 @@ findRoot cli = do
     dir0 = takeDirectory <$> cliMainFile cli
 
 class HasEntryPoint a where
-  getEntryPoint :: FilePath -> a -> EntryPoint
+  getEntryPoint :: FilePath -> GlobalOptions -> a -> EntryPoint
 
 instance HasEntryPoint ScopeOptions where
-  getEntryPoint root = EntryPoint root . (^. scopeInputFiles)
+  getEntryPoint r opts = EntryPoint r nT . (^. scopeInputFiles)
+    where
+      nT = opts ^. globalNoTermination
 
 instance HasEntryPoint ParseOptions where
-  getEntryPoint root = EntryPoint root . pure . (^. parseInputFile)
+  getEntryPoint r opts = EntryPoint r nT . pure . (^. parseInputFile)
+    where
+      nT = opts ^. globalNoTermination
 
 instance HasEntryPoint HighlightOptions where
-  getEntryPoint root = EntryPoint root . pure . (^. highlightInputFile)
+  getEntryPoint r opts = EntryPoint r nT . pure . (^. highlightInputFile)
+    where
+      nT = opts ^. globalNoTermination
 
 instance HasEntryPoint HtmlOptions where
-  getEntryPoint root = EntryPoint root . pure . (^. htmlInputFile)
+  getEntryPoint r opts = EntryPoint r nT . pure . (^. htmlInputFile)
+    where
+      nT = opts ^. globalNoTermination
 
 instance HasEntryPoint MicroJuvixTypeOptions where
-  getEntryPoint root = EntryPoint root . pure . (^. microJuvixTypeInputFile)
+  getEntryPoint r opts = EntryPoint r nT . pure . (^. microJuvixTypeInputFile)
+    where
+      nT = opts ^. globalNoTermination
 
 instance HasEntryPoint MicroJuvixPrettyOptions where
-  getEntryPoint root = EntryPoint root . pure . (^. microJuvixPrettyInputFile)
+  getEntryPoint r opts = EntryPoint r nT . pure . (^. microJuvixPrettyInputFile)
+    where
+      nT = opts ^. globalNoTermination
 
 instance HasEntryPoint MonoJuvixOptions where
-  getEntryPoint root = EntryPoint root . pure . (^. monoJuvixInputFile)
+  getEntryPoint r opts = EntryPoint r nT . pure . (^. monoJuvixInputFile)
+    where
+      nT = opts ^. globalNoTermination
 
 instance HasEntryPoint MiniHaskellOptions where
-  getEntryPoint root = EntryPoint root . pure . (^. miniHaskellInputFile)
+  getEntryPoint r opts = EntryPoint r nT . pure . (^. miniHaskellInputFile)
+    where
+      nT = opts ^. globalNoTermination
 
 instance HasEntryPoint MiniCOptions where
-  getEntryPoint root = EntryPoint root . pure . (^. miniCInputFile)
+  getEntryPoint r opts = EntryPoint r nT . pure . (^. miniCInputFile)
+    where
+      nT = opts ^. globalNoTermination
 
 instance HasEntryPoint CallsOptions where
-  getEntryPoint root = EntryPoint root . pure . (^. callsInputFile)
+  getEntryPoint r opts = EntryPoint r nT . pure . (^. callsInputFile)
+    where
+      nT = opts ^. globalNoTermination
 
 instance HasEntryPoint CallGraphOptions where
-  getEntryPoint root = EntryPoint root . pure . (^. graphInputFile)
+  getEntryPoint r opts = EntryPoint r nT . pure . (^. graphInputFile)
+    where
+      nT = opts ^. globalNoTermination
 
 runCLI :: Members '[Embed IO, App] r => CLI -> Sem r ()
 runCLI cli = do
@@ -111,7 +133,7 @@ runCLI cli = do
     DisplayVersion -> embed runDisplayVersion
     DisplayRoot -> say (pack root)
     Highlight o -> do
-      res <- runPipelineEither (upToScoping (getEntryPoint root o))
+      res <- runPipelineEither (upToScoping (getEntryPoint root globalOptions o))
       absP <- embed (makeAbsolute (o ^. highlightInputFile))
       case res of
         Left err -> say (Highlight.goError (errorIntervals err))
@@ -128,25 +150,27 @@ runCLI cli = do
                     }
           say (Highlight.go hinput)
     Parse opts -> do
-      m <- head . (^. Parser.resultModules) <$> runPipeline (upToParsing (getEntryPoint root opts))
+      m <-
+        head . (^. Parser.resultModules)
+          <$> runPipeline (upToParsing (getEntryPoint root globalOptions opts))
       if opts ^. parseNoPrettyShow then say (show m) else say (pack (ppShow m))
     Scope opts -> do
-      l <- (^. Scoper.resultModules) <$> runPipeline (upToScoping (getEntryPoint root opts))
+      l <- (^. Scoper.resultModules) <$> runPipeline (upToScoping (getEntryPoint root globalOptions opts))
       forM_ l $ \s -> do
         renderStdOut (Scoper.ppOut (mkScopePrettyOptions globalOptions opts) s)
     Html o@HtmlOptions {..} -> do
-      res <- runPipeline (upToScoping (getEntryPoint root o))
+      res <- runPipeline (upToScoping (getEntryPoint root globalOptions o))
       let m = head (res ^. Scoper.resultModules)
       embed (genHtml Scoper.defaultOptions _htmlRecursive _htmlTheme m)
     MicroJuvix (Pretty opts) -> do
-      micro <- head . (^. Micro.resultModules) <$> runPipeline (upToMicroJuvix (getEntryPoint root opts))
+      micro <- head . (^. Micro.resultModules) <$> runPipeline (upToMicroJuvix (getEntryPoint root globalOptions opts))
       let ppOpts =
             Micro.defaultOptions
               { Micro._optShowNameId = globalOptions ^. globalShowNameIds
               }
       App.renderStdOut (Micro.ppOut ppOpts micro)
     MicroJuvix (TypeCheck opts) -> do
-      res <- runPipeline (upToMicroJuvixTyped (getEntryPoint root opts))
+      res <- runPipeline (upToMicroJuvixTyped (getEntryPoint root globalOptions opts))
       say "Well done! It type checks"
       when (opts ^. microJuvixTypePrint) $ do
         let ppOpts =
@@ -166,16 +190,16 @@ runCLI cli = do
             Mono.defaultOptions
               { Mono._optShowNameIds = globalOptions ^. globalShowNameIds
               }
-      monojuvix <- head . (^. Mono.resultModules) <$> runPipeline (upToMonoJuvix (getEntryPoint root o))
+      monojuvix <- head . (^. Mono.resultModules) <$> runPipeline (upToMonoJuvix (getEntryPoint root globalOptions o))
       renderStdOut (Mono.ppOut ppOpts monojuvix)
     MiniHaskell o -> do
-      minihaskell <- head . (^. MiniHaskell.resultModules) <$> runPipeline (upToMiniHaskell (getEntryPoint root o))
+      minihaskell <- head . (^. MiniHaskell.resultModules) <$> runPipeline (upToMiniHaskell (getEntryPoint root globalOptions o))
       renderStdOut (MiniHaskell.ppOutDefault minihaskell)
     MiniC o -> do
-      miniC <- (^. MiniC.resultCCode) <$> runPipeline (upToMiniC (getEntryPoint root o))
+      miniC <- (^. MiniC.resultCCode) <$> runPipeline (upToMiniC (getEntryPoint root globalOptions o))
       say miniC
     Termination (Calls opts@CallsOptions {..}) -> do
-      results <- runPipeline (upToAbstract (getEntryPoint root opts))
+      results <- runPipeline (upToAbstract (getEntryPoint root globalOptions opts))
       let topModule = head (results ^. Abstract.resultModules)
           infotable = results ^. Abstract.resultTable
           callMap0 = Termination.buildCallMap infotable topModule
@@ -186,7 +210,7 @@ runCLI cli = do
       renderStdOut (Abstract.ppOut opts' callMap)
       newline
     Termination (CallGraph opts@CallGraphOptions {..}) -> do
-      results <- runPipeline (upToAbstract (getEntryPoint root opts))
+      results <- runPipeline (upToAbstract (getEntryPoint root globalOptions opts))
       let topModule = head (results ^. Abstract.resultModules)
           infotable = results ^. Abstract.resultTable
           callMap = Termination.buildCallMap infotable topModule

src/MiniJuvix/Pipeline.hs

@@ -121,9 +121,10 @@ pipelineAbstract ::
 pipelineAbstract = Abstract.entryAbstract
 
 pipelineMicroJuvix ::
+  Members '[Error MiniJuvixError] r =>
   Abstract.AbstractResult ->
   Sem r MicroJuvix.MicroJuvixResult
-pipelineMicroJuvix = MicroJuvix.entryMicroJuvix
+pipelineMicroJuvix = mapError (MiniJuvixError @MicroJuvix.TerminationError) . MicroJuvix.entryMicroJuvix
 
 pipelineMicroJuvixTyped ::
   Members '[Files, NameIdGen, Error MiniJuvixError] r =>

src/MiniJuvix/Pipeline/EntryPoint.hs

@@ -1,15 +1,27 @@
-module MiniJuvix.Pipeline.EntryPoint where
+module MiniJuvix.Pipeline.EntryPoint
+  ( module MiniJuvix.Pipeline.EntryPoint,
+  )
+where
 
 import MiniJuvix.Prelude
 
--- | The head of _entryModulePaths is assumed to be the Main module.
+-- | The head of _entryModulePaths is assumed to be the Main module
 data EntryPoint = EntryPoint
-  { _entryRoot :: FilePath,
-    _entryModulePaths :: NonEmpty FilePath
+  { _entryPointRoot :: FilePath,
+    _entryPointNoTermination :: Bool,
+    _entryPointModulePaths :: NonEmpty FilePath
   }
   deriving stock (Eq, Show)
 
+defaultEntryPoint :: FilePath -> EntryPoint
+defaultEntryPoint mainFile =
+  EntryPoint
+    { _entryPointRoot = ".",
+      _entryPointNoTermination = False,
+      _entryPointModulePaths = pure mainFile
+    }
+
 makeLenses ''EntryPoint
 
 mainModulePath :: Lens' EntryPoint FilePath
-mainModulePath = entryModulePaths . _head
+mainModulePath = entryPointModulePaths . _head

src/MiniJuvix/Prelude/Base.hs

@@ -213,8 +213,15 @@ mconcatMap f = List.mconcatMap f . toList
 -- HashMap
 --------------------------------------------------------------------------------
 
-tableInsert :: Hashable k => (a -> v) -> (a -> v -> v) -> k -> a -> HashMap k v -> HashMap k v
-tableInsert s f k a m = over (at k) (Just . aux) m
+tableInsert ::
+  Hashable k =>
+  (a -> v) ->
+  (a -> v -> v) ->
+  k ->
+  a ->
+  HashMap k v ->
+  HashMap k v
+tableInsert s f k a = over (at k) (Just . aux)
   where
     aux = \case
       Just v -> f a v

src/MiniJuvix/Syntax/Abstract/AbstractResult.hs

@@ -4,9 +4,11 @@ module MiniJuvix.Syntax.Abstract.AbstractResult
   )
 where
 
+import MiniJuvix.Pipeline.EntryPoint qualified as E
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.InfoTable
 import MiniJuvix.Syntax.Abstract.Language
+import MiniJuvix.Syntax.Concrete.Parser.ParserResult
 import MiniJuvix.Syntax.Concrete.Scoped.Scoper.ScoperResult
 
 data AbstractResult = AbstractResult
@@ -16,3 +18,6 @@ data AbstractResult = AbstractResult
   }
 
 makeLenses ''AbstractResult
+
+abstractResultEntryPoint :: Lens' AbstractResult E.EntryPoint
+abstractResultEntryPoint = resultScoper . resultParserResult . resultEntry

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -27,7 +27,7 @@ entryParser ::
   EntryPoint ->
   Sem r ParserResult
 entryParser e = do
-  (_resultTable, _resultModules) <- runInfoTableBuilder (runReader e (mapM goFile (e ^. entryModulePaths)))
+  (_resultTable, _resultModules) <- runInfoTableBuilder (runReader e (mapM goFile (e ^. entryPointModulePaths)))
   let _resultEntry = e
   return ParserResult {..}
   where
@@ -37,7 +37,7 @@ entryParser e = do
       Sem r (Module 'Parsed 'ModuleTop)
     goFile fileName = do
       input <- readFile' fileName
-      case runModuleParser (e ^. entryRoot) fileName input of
+      case runModuleParser (e ^. entryPointRoot) fileName input of
         Left er -> throw er
         Right (tbl, m) -> mergeTable tbl $> m
 

src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs

@@ -247,7 +247,7 @@ makeLenses ''NotInScope
 instance ToGenericError NotInScope where
   genericError e@NotInScope {..} =
     GenericError
-      { _genericErrorLoc = (e ^. notInScopeSymbol . symbolLoc),
+      { _genericErrorLoc = e ^. notInScopeSymbol . symbolLoc,
         _genericErrorMessage = prettyError msg,
         _genericErrorIntervals = [e ^. notInScopeSymbol . symbolLoc]
       }

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -34,7 +34,7 @@ entryScoper ::
   ParserResult ->
   Sem r ScoperResult
 entryScoper pr = do
-  let root = pr ^. Parser.resultEntry . entryRoot
+  let root = pr ^. Parser.resultEntry . entryPointRoot
       modules = pr ^. Parser.resultModules
   scopeCheck pr root modules
 

src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -252,7 +252,7 @@ checkPattern ::
   FunctionArgType ->
   Pattern ->
   Sem r ()
-checkPattern funName type_ pat = go type_ pat
+checkPattern funName = go
   where
     go :: FunctionArgType -> Pattern -> Sem r ()
     go argTy p = do

src/MiniJuvix/Termination/Checker.hs

@@ -1,16 +1,44 @@
 module MiniJuvix.Termination.Checker
   ( module MiniJuvix.Termination.Checker,
     module MiniJuvix.Termination.FunctionCall,
+    module MiniJuvix.Termination.Error,
   )
 where
 
+import Data.HashMap.Internal.Strict qualified as HashMap
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Abstract.InfoTable
-import MiniJuvix.Syntax.Abstract.Language.Extra
+import MiniJuvix.Syntax.Abstract.InfoTable as Abstract
+import MiniJuvix.Syntax.Abstract.Language as Abstract
 import MiniJuvix.Syntax.Concrete.Scoped.Name (unqualifiedSymbol)
+import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as Scoper
+import MiniJuvix.Termination.Error
 import MiniJuvix.Termination.FunctionCall
+import MiniJuvix.Termination.LexOrder
 import MiniJuvix.Termination.Types
 
+checkTermination ::
+  Members '[Error TerminationError] r =>
+  Abstract.TopModule ->
+  Abstract.InfoTable ->
+  Sem r ()
+checkTermination topModule infotable = do
+  let callmap = buildCallMap infotable topModule
+      completeGraph = completeCallGraph callmap
+      rEdges = reflexiveEdges completeGraph
+      recBehav = map recursiveBehaviour rEdges
+  forM_ recBehav $ \r -> do
+    let funSym = r ^. recursiveBehaviourFun
+        funName = Scoper.unqualifiedSymbol funSym
+        funRef = Abstract.FunctionRef funName
+        funInfo = HashMap.lookupDefault impossible funRef (infotable ^. Abstract.infoFunctions)
+        markedTerminating = funInfo ^. (Abstract.functionInfoDef . Abstract.funDefTerminating)
+    if
+        | markedTerminating -> return ()
+        | otherwise ->
+            case findOrder r of
+              Nothing -> throw (ErrNoLexOrder (NoLexOrder funName))
+              Just _ -> return ()
+
 buildCallMap :: InfoTable -> TopModule -> CallMap
 buildCallMap infotable = run . execState mempty . runReader infotable . checkModule
 

src/MiniJuvix/Termination/Error/Types.hs

@@ -26,5 +26,5 @@ instance ToGenericError NoLexOrder where
 
       msg :: Doc Eann
       msg =
-        "The function" <+> pretty (Scoped.nameUnqualifiedText name)
+        "The function" <+> highlight (pretty (Scoped.nameUnqualifiedText name))
           <+> "fails the termination checker."

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -1,23 +1,26 @@
 module MiniJuvix.Translation.AbstractToMicroJuvix
   ( module MiniJuvix.Translation.AbstractToMicroJuvix,
     module MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult,
+    module MiniJuvix.Termination.Checker,
   )
 where
 
 import Data.HashSet qualified as HashSet
+import MiniJuvix.Pipeline.EntryPoint qualified as E
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract
-import MiniJuvix.Syntax.Abstract.Language.Extra qualified as A
+import MiniJuvix.Syntax.Abstract.Language qualified as Abstract
 import MiniJuvix.Syntax.Concrete.Name (symbolLoc)
-import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
+import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as Scoper
 import MiniJuvix.Syntax.MicroJuvix.Language
 import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult
 import MiniJuvix.Syntax.Universe
-import MiniJuvix.Syntax.Usage qualified as A
+import MiniJuvix.Syntax.Usage
+import MiniJuvix.Termination.Checker
 
 newtype TranslationState = TranslationState
   { -- | Top modules are supposed to be included at most once.
-    _translationStateIncluded :: HashSet A.TopModuleName
+    _translationStateIncluded :: HashSet Abstract.TopModuleName
   }
 
 iniState :: TranslationState
@@ -29,57 +32,68 @@ iniState =
 makeLenses ''TranslationState
 
 entryMicroJuvix ::
+  Members '[Error TerminationError] r =>
   Abstract.AbstractResult ->
   Sem r MicroJuvixResult
-entryMicroJuvix ares = do
+entryMicroJuvix abstractResults = do
+  unless noTerminationOption (checkTermination topModule infoTable)
   _resultModules' <-
     evalState
       iniState
-      (mapM goModule (ares ^. Abstract.resultModules))
+      (mapM goModule (abstractResults ^. Abstract.resultModules))
   return
     MicroJuvixResult
-      { _resultAbstract = ares,
+      { _resultAbstract = abstractResults,
         _resultModules = _resultModules'
       }
+  where
+    topModule = head (abstractResults ^. Abstract.resultModules)
+    infoTable = abstractResults ^. Abstract.resultTable
+    noTerminationOption =
+      abstractResults
+        ^. Abstract.abstractResultEntryPoint . E.entryPointNoTermination
 
-goModule :: Member (State TranslationState) r => A.TopModule -> Sem r Module
+goModule ::
+  Member (State TranslationState) r =>
+  Abstract.TopModule ->
+  Sem r Module
 goModule m = do
-  _moduleBody' <- goModuleBody (m ^. A.moduleBody)
+  _moduleBody' <- goModuleBody (m ^. Abstract.moduleBody)
   return
     Module
-      { _moduleName = goTopModuleName (m ^. A.moduleName),
+      { _moduleName = goTopModuleName (m ^. Abstract.moduleName),
         _moduleBody = _moduleBody'
       }
 
-goTopModuleName :: A.TopModuleName -> Name
-goTopModuleName = goSymbol . S.topModulePathName
+goTopModuleName :: Abstract.TopModuleName -> Name
+goTopModuleName = goSymbol . Scoper.topModulePathName
 
-goName :: S.Name -> Name
-goName = goSymbol . S.nameUnqualify
+goName :: Scoper.Name -> Name
+goName = goSymbol . Scoper.nameUnqualify
 
-goSymbol :: S.Symbol -> Name
+goSymbol :: Scoper.Symbol -> Name
 goSymbol s =
   Name
-    { _nameText = S.symbolText s,
-      _nameId = s ^. S.nameId,
+    { _nameText = Scoper.symbolText s,
+      _nameId = s ^. Scoper.nameId,
       _nameKind = getNameKind s,
-      _nameDefined = s ^. S.nameDefined,
-      _nameLoc = s ^. S.nameConcrete . symbolLoc
+      _nameDefined = s ^. Scoper.nameDefined,
+      _nameLoc = s ^. Scoper.nameConcrete . symbolLoc
     }
 
 unsupported :: Text -> a
 unsupported thing = error ("Abstract to MicroJuvix: Not yet supported: " <> thing)
 
-goModuleBody :: Member (State TranslationState) r => A.ModuleBody -> Sem r ModuleBody
-goModuleBody b = ModuleBody <$> mapMaybeM goStatement (b ^. A.moduleStatements)
+goModuleBody :: Member (State TranslationState) r => Abstract.ModuleBody -> Sem r ModuleBody
+goModuleBody b = ModuleBody <$> mapMaybeM goStatement (b ^. Abstract.moduleStatements)
 
-goImport :: Member (State TranslationState) r => A.TopModule -> Sem r (Maybe Include)
+goImport :: Member (State TranslationState) r => Abstract.TopModule -> Sem r (Maybe Include)
 goImport m = do
-  inc <- gets (HashSet.member (m ^. A.moduleName) . (^. translationStateIncluded))
+  inc <- gets (HashSet.member (m ^. Abstract.moduleName) . (^. translationStateIncluded))
   if
       | inc -> return Nothing
       | otherwise -> do
-          modify (over translationStateIncluded (HashSet.insert (m ^. A.moduleName)))
+          modify (over translationStateIncluded (HashSet.insert (m ^. Abstract.moduleName)))
           m' <- goModule m
           return
             ( Just
@@ -88,58 +102,62 @@ goImport m = do
                   }
             )
 
-goStatement :: Member (State TranslationState) r => A.Statement -> Sem r (Maybe Statement)
+goStatement ::
+  Member (State TranslationState) r =>
+  Abstract.Statement ->
+  Sem r (Maybe Statement)
 goStatement = \case
-  A.StatementAxiom d -> Just . StatementAxiom <$> goAxiomDef d
-  A.StatementForeign f -> return (Just (StatementForeign f))
-  A.StatementFunction f -> Just . StatementFunction <$> goFunctionDef f
-  A.StatementImport i -> fmap StatementInclude <$> goImport i
-  A.StatementLocalModule {} -> unsupported "local modules"
-  A.StatementInductive i -> Just . StatementInductive <$> goInductiveDef i
+  Abstract.StatementAxiom d -> Just . StatementAxiom <$> goAxiomDef d
+  Abstract.StatementForeign f -> return (Just (StatementForeign f))
+  Abstract.StatementFunction f -> Just . StatementFunction <$> goFunctionDef f
+  Abstract.StatementImport i -> fmap StatementInclude <$> goImport i
+  Abstract.StatementLocalModule {} -> unsupported "local modules"
+  Abstract.StatementInductive i -> Just . StatementInductive <$> goInductiveDef i
 
-goTypeIden :: A.Iden -> TypeIden
+goTypeIden :: Abstract.Iden -> TypeIden
 goTypeIden i = case i of
-  A.IdenFunction {} -> unsupported "functions in types"
-  A.IdenConstructor {} -> unsupported "constructors in types"
-  A.IdenVar v -> TypeIdenVariable (goSymbol v)
-  A.IdenInductive d -> TypeIdenInductive (goName (d ^. A.inductiveRefName))
-  A.IdenAxiom a -> TypeIdenAxiom (goName (a ^. A.axiomRefName))
+  Abstract.IdenFunction {} -> unsupported "functions in types"
+  Abstract.IdenConstructor {} -> unsupported "constructors in types"
+  Abstract.IdenVar v -> TypeIdenVariable (goSymbol v)
+  Abstract.IdenInductive d -> TypeIdenInductive (goName (d ^. Abstract.inductiveRefName))
+  Abstract.IdenAxiom a -> TypeIdenAxiom (goName (a ^. Abstract.axiomRefName))
 
-goAxiomDef :: A.AxiomDef -> Sem r AxiomDef
+goAxiomDef :: Abstract.AxiomDef -> Sem r AxiomDef
 goAxiomDef a = do
-  _axiomType' <- goType (a ^. A.axiomType)
+  _axiomType' <- goType (a ^. Abstract.axiomType)
   return
     AxiomDef
-      { _axiomName = goSymbol (a ^. A.axiomName),
+      { _axiomName = goSymbol (a ^. Abstract.axiomName),
         _axiomType = _axiomType'
       }
 
-goFunctionParameter :: A.FunctionParameter -> Sem r (Either VarName Type)
-goFunctionParameter f = case f ^. A.paramName of
+goFunctionParameter :: Abstract.FunctionParameter -> Sem r (Either VarName Type)
+goFunctionParameter f = case f ^. Abstract.paramName of
   Just var
-    | isSmallType (f ^. A.paramType) && isOmegaUsage (f ^. A.paramUsage) -> return (Left (goSymbol var))
+    | isSmallType (f ^. Abstract.paramType) && isOmegaUsage (f ^. Abstract.paramUsage) ->
+        return (Left (goSymbol var))
     | otherwise -> unsupported "named function arguments only for small types without usages"
   Nothing
-    | isOmegaUsage (f ^. A.paramUsage) -> Right <$> goType (f ^. A.paramType)
+    | isOmegaUsage (f ^. Abstract.paramUsage) -> Right <$> goType (f ^. Abstract.paramType)
     | otherwise -> unsupported "usages"
 
-isOmegaUsage :: A.Usage -> Bool
+isOmegaUsage :: Usage -> Bool
 isOmegaUsage u = case u of
-  A.UsageOmega -> True
+  UsageOmega -> True
   _ -> False
 
-goFunction :: A.Function -> Sem r Type
-goFunction (A.Function l r) = do
+goFunction :: Abstract.Function -> Sem r Type
+goFunction (Abstract.Function l r) = do
   l' <- goFunctionParameter l
   r' <- goType r
   return $ case l' of
     Left tyvar -> TypeAbs (TypeAbstraction tyvar r')
     Right ty -> TypeFunction (Function ty r')
 
-goFunctionDef :: A.FunctionDef -> Sem r FunctionDef
+goFunctionDef :: Abstract.FunctionDef -> Sem r FunctionDef
 goFunctionDef f = do
-  _funDefClauses' <- mapM (goFunctionClause _funDefName') (f ^. A.funDefClauses)
-  _funDefType' <- goType (f ^. A.funDefTypeSig)
+  _funDefClauses' <- mapM (goFunctionClause _funDefName') (f ^. Abstract.funDefClauses)
+  _funDefType' <- goType (f ^. Abstract.funDefTypeSig)
   return
     FunctionDef
       { _funDefName = _funDefName',
@@ -148,12 +166,12 @@ goFunctionDef f = do
       }
   where
     _funDefName' :: Name
-    _funDefName' = goSymbol (f ^. A.funDefName)
+    _funDefName' = goSymbol (f ^. Abstract.funDefName)
 
-goFunctionClause :: Name -> A.FunctionClause -> Sem r FunctionClause
+goFunctionClause :: Name -> Abstract.FunctionClause -> Sem r FunctionClause
 goFunctionClause n c = do
-  _clauseBody' <- goExpression (c ^. A.clauseBody)
-  _clausePatterns' <- mapM goPattern (c ^. A.clausePatterns)
+  _clauseBody' <- goExpression (c ^. Abstract.clauseBody)
+  _clausePatterns' <- mapM goPattern (c ^. Abstract.clausePatterns)
   return
     FunctionClause
       { _clauseName = n,
@@ -161,25 +179,25 @@ goFunctionClause n c = do
         _clauseBody = _clauseBody'
       }
 
-goPattern :: A.Pattern -> Sem r Pattern
+goPattern :: Abstract.Pattern -> Sem r Pattern
 goPattern p = case p of
-  A.PatternVariable v -> return (PatternVariable (goSymbol v))
-  A.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c
-  A.PatternWildcard -> return PatternWildcard
-  A.PatternEmpty -> unsupported "pattern empty"
+  Abstract.PatternVariable v -> return (PatternVariable (goSymbol v))
+  Abstract.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c
+  Abstract.PatternWildcard -> return PatternWildcard
+  Abstract.PatternEmpty -> unsupported "pattern empty"
 
-goConstructorApp :: A.ConstructorApp -> Sem r ConstructorApp
+goConstructorApp :: Abstract.ConstructorApp -> Sem r ConstructorApp
 goConstructorApp c = do
-  _constrAppParameters' <- mapM goPattern (c ^. A.constrAppParameters)
+  _constrAppParameters' <- mapM goPattern (c ^. Abstract.constrAppParameters)
   return
     ConstructorApp
-      { _constrAppConstructor = goName (c ^. A.constrAppConstructor . A.constructorRefName),
+      { _constrAppConstructor = goName (c ^. Abstract.constrAppConstructor . Abstract.constructorRefName),
         _constrAppParameters = _constrAppParameters'
       }
 
-isSmallType :: A.Expression -> Bool
+isSmallType :: Abstract.Expression -> Bool
 isSmallType e = case e of
-  A.ExpressionUniverse u -> isSmallUni u
+  Abstract.ExpressionUniverse u -> isSmallUni u
   _ -> False
 
 isSmallUni :: Universe -> Bool
@@ -190,52 +208,52 @@ goTypeUniverse u
   | isSmallUni u = TypeUniverse
   | otherwise = unsupported "big universes"
 
-goType :: A.Expression -> Sem r Type
+goType :: Abstract.Expression -> Sem r Type
 goType e = case e of
-  A.ExpressionIden i -> return (TypeIden (goTypeIden i))
-  A.ExpressionUniverse u -> return (goTypeUniverse u)
-  A.ExpressionApplication a -> TypeApp <$> goTypeApplication a
-  A.ExpressionFunction f -> goFunction f
-  A.ExpressionLiteral {} -> unsupported "literals in types"
+  Abstract.ExpressionIden i -> return (TypeIden (goTypeIden i))
+  Abstract.ExpressionUniverse u -> return (goTypeUniverse u)
+  Abstract.ExpressionApplication a -> TypeApp <$> goTypeApplication a
+  Abstract.ExpressionFunction f -> goFunction f
+  Abstract.ExpressionLiteral {} -> unsupported "literals in types"
 
-goApplication :: A.Application -> Sem r Application
-goApplication (A.Application f x) = do
+goApplication :: Abstract.Application -> Sem r Application
+goApplication (Abstract.Application f x) = do
   f' <- goExpression f
   x' <- goExpression x
   return (Application f' x')
 
-goIden :: A.Iden -> Iden
+goIden :: Abstract.Iden -> Iden
 goIden i = case i of
-  A.IdenFunction n -> IdenFunction (goName (n ^. A.functionRefName))
-  A.IdenConstructor c -> IdenConstructor (goName (c ^. A.constructorRefName))
-  A.IdenVar v -> IdenVar (goSymbol v)
-  A.IdenAxiom a -> IdenAxiom (goName (a ^. A.axiomRefName))
-  A.IdenInductive a -> IdenInductive (goName (a ^. A.inductiveRefName))
+  Abstract.IdenFunction n -> IdenFunction (goName (n ^. Abstract.functionRefName))
+  Abstract.IdenConstructor c -> IdenConstructor (goName (c ^. Abstract.constructorRefName))
+  Abstract.IdenVar v -> IdenVar (goSymbol v)
+  Abstract.IdenAxiom a -> IdenAxiom (goName (a ^. Abstract.axiomRefName))
+  Abstract.IdenInductive a -> IdenInductive (goName (a ^. Abstract.inductiveRefName))
 
-goExpressionFunction :: forall r. A.Function -> Sem r FunctionExpression
+goExpressionFunction :: forall r. Abstract.Function -> Sem r FunctionExpression
 goExpressionFunction f = do
-  l' <- goParam (f ^. A.funParameter)
-  r' <- goExpression (f ^. A.funReturn)
+  l' <- goParam (f ^. Abstract.funParameter)
+  r' <- goExpression (f ^. Abstract.funReturn)
   return (FunctionExpression l' r')
   where
-    goParam :: A.FunctionParameter -> Sem r Expression
+    goParam :: Abstract.FunctionParameter -> Sem r Expression
     goParam p
-      | isJust (p ^. A.paramName) = unsupported "named type parameters"
-      | isOmegaUsage (p ^. A.paramUsage) = goExpression (p ^. A.paramType)
+      | isJust (p ^. Abstract.paramName) = unsupported "named type parameters"
+      | isOmegaUsage (p ^. Abstract.paramUsage) = goExpression (p ^. Abstract.paramType)
       | otherwise = unsupported "usages"
 
-goExpression :: A.Expression -> Sem r Expression
+goExpression :: Abstract.Expression -> Sem r Expression
 goExpression e = case e of
-  A.ExpressionIden i -> return (ExpressionIden (goIden i))
-  A.ExpressionUniverse {} -> unsupported "universes in expression"
-  A.ExpressionFunction f -> ExpressionFunction <$> goExpressionFunction f
-  A.ExpressionApplication a -> ExpressionApplication <$> goApplication a
-  A.ExpressionLiteral l -> return (ExpressionLiteral l)
+  Abstract.ExpressionIden i -> return (ExpressionIden (goIden i))
+  Abstract.ExpressionUniverse {} -> unsupported "universes in expression"
+  Abstract.ExpressionFunction f -> ExpressionFunction <$> goExpressionFunction f
+  Abstract.ExpressionApplication a -> ExpressionApplication <$> goApplication a
+  Abstract.ExpressionLiteral l -> return (ExpressionLiteral l)
 
-goInductiveParameter :: A.FunctionParameter -> Sem r InductiveParameter
+goInductiveParameter :: Abstract.FunctionParameter -> Sem r InductiveParameter
 goInductiveParameter f =
-  case (f ^. A.paramName, f ^. A.paramUsage, f ^. A.paramType) of
-    (Just var, A.UsageOmega, A.ExpressionUniverse u)
+  case (f ^. Abstract.paramName, f ^. Abstract.paramUsage, f ^. Abstract.paramType) of
+    (Just var, UsageOmega, Abstract.ExpressionUniverse u)
       | isSmallUni u ->
           return
             InductiveParameter
@@ -244,12 +262,12 @@ goInductiveParameter f =
     (Just {}, _, _) -> unsupported "only type variables of small types are allowed"
     (Nothing, _, _) -> unsupported "unnamed inductive parameters"
 
-goInductiveDef :: forall r. A.InductiveDef -> Sem r InductiveDef
-goInductiveDef i = case i ^. A.inductiveType of
+goInductiveDef :: forall r. Abstract.InductiveDef -> Sem r InductiveDef
+goInductiveDef i = case i ^. Abstract.inductiveType of
   Just {} -> unsupported "inductive indices"
   _ -> do
-    _inductiveParameters' <- mapM goInductiveParameter (i ^. A.inductiveParameters)
-    _inductiveConstructors' <- mapM goConstructorDef (i ^. A.inductiveConstructors)
+    _inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
+    _inductiveConstructors' <- mapM goConstructorDef (i ^. Abstract.inductiveConstructors)
     return
       InductiveDef
         { _inductiveName = indName,
@@ -257,21 +275,21 @@ goInductiveDef i = case i ^. A.inductiveType of
           _inductiveConstructors = _inductiveConstructors'
         }
   where
-    indName = goSymbol (i ^. A.inductiveName)
-    goConstructorDef :: A.InductiveConstructorDef -> Sem r InductiveConstructorDef
+    indName = goSymbol (i ^. Abstract.inductiveName)
+    goConstructorDef :: Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
     goConstructorDef c = do
-      _constructorParameters' <- goConstructorType (c ^. A.constructorType)
+      _constructorParameters' <- goConstructorType (c ^. Abstract.constructorType)
       return
         InductiveConstructorDef
-          { _constructorName = goSymbol (c ^. A.constructorName),
+          { _constructorName = goSymbol (c ^. Abstract.constructorName),
             _constructorParameters = _constructorParameters'
           }
     -- TODO check that the return type corresponds with the inductive type
-    goConstructorType :: A.Expression -> Sem r [Type]
+    goConstructorType :: Abstract.Expression -> Sem r [Type]
     goConstructorType = fmap fst . viewConstructorType
 
-goTypeApplication :: A.Application -> Sem r TypeApplication
-goTypeApplication (A.Application l r) = do
+goTypeApplication :: Abstract.Application -> Sem r TypeApplication
+goTypeApplication (Abstract.Application l r) = do
   l' <- goType l
   r' <- goType r
   return
@@ -280,18 +298,18 @@ goTypeApplication (A.Application l r) = do
         _typeAppRight = r'
       }
 
-viewConstructorType :: A.Expression -> Sem r ([Type], Type)
+viewConstructorType :: Abstract.Expression -> Sem r ([Type], Type)
 viewConstructorType e = case e of
-  A.ExpressionFunction f -> first toList <$> viewFunctionType f
-  A.ExpressionIden i -> return ([], TypeIden (goTypeIden i))
-  A.ExpressionApplication a -> do
+  Abstract.ExpressionFunction f -> first toList <$> viewFunctionType f
+  Abstract.ExpressionIden i -> return ([], TypeIden (goTypeIden i))
+  Abstract.ExpressionApplication a -> do
     a' <- goTypeApplication a
     return ([], TypeApp a')
-  A.ExpressionUniverse {} -> return ([], TypeUniverse)
-  A.ExpressionLiteral {} -> unsupported "literal in a type"
+  Abstract.ExpressionUniverse {} -> return ([], TypeUniverse)
+  Abstract.ExpressionLiteral {} -> unsupported "literal in a type"
   where
-    viewFunctionType :: A.Function -> Sem r (NonEmpty Type, Type)
-    viewFunctionType (A.Function p r) = do
+    viewFunctionType :: Abstract.Function -> Sem r (NonEmpty Type, Type)
+    viewFunctionType (Abstract.Function p r) = do
       (args, ret) <- viewConstructorType r
       p' <- goFunctionParameter p
       return $ case p' of

src/MiniJuvix/Translation/ScopedToAbstract.hs

@@ -20,10 +20,7 @@ unsupported msg = error $ msg <> "Scoped to Abstract: not yet supported"
 entryAbstract :: Scoper.ScoperResult -> Sem r AbstractResult
 entryAbstract _resultScoper = do
   (_resultTable, _resultModules) <- runInfoTableBuilder (mapM goTopModule ms)
-  return
-    AbstractResult
-      { ..
-      }
+  return AbstractResult {..}
   where
     ms = _resultScoper ^. Scoper.resultModules
 

test/BackendC/Positive.hs

@@ -44,7 +44,7 @@ testDescr PosTest {..} =
                 "WASI_SYSROOT_PATH"
 
             step "C Generation"
-            let entryPoint = EntryPoint "." (pure mainFile)
+            let entryPoint = defaultEntryPoint mainFile
             p :: MiniC.MiniCResult <- runIO (upToMiniC entryPoint)
 
             expected <- TIO.readFile expectedFile

test/Base.hs

@@ -44,7 +44,10 @@ assertEqDiff msg a b
     pb = lines $ ppShow b
 
 assertCmdExists :: FilePath -> Assertion
-assertCmdExists cmd = assertBool ("Command: " <> cmd <> " is not present on $PATH") . isJust =<< findExecutable cmd
+assertCmdExists cmd =
+  assertBool ("Command: " <> cmd <> " is not present on $PATH")
+    . isJust
+    =<< findExecutable cmd
 
 assertEnvVar :: String -> String -> IO String
 assertEnvVar msg varName = fromMaybeM (assertFailure msg) (lookupEnv varName)

test/Main.hs

@@ -4,6 +4,7 @@ import BackendC qualified
 import Base
 import MonoJuvix qualified
 import Scope qualified
+import Termination qualified
 import TypeCheck qualified
 
 slowTests :: TestTree
@@ -17,6 +18,7 @@ fastTests =
   testGroup
     "MiniJuvix fast tests"
     [ Scope.allTests,
+      Termination.allTests,
       TypeCheck.allTests,
       MonoJuvix.allTests
     ]

test/MonoJuvix/Positive.hs

@@ -19,7 +19,7 @@ testDescr PosTest {..} =
         { _testName = _name,
           _testRoot = tRoot,
           _testAssertion = Single $ do
-            let entryPoint = EntryPoint "." (pure _file)
+            let entryPoint = defaultEntryPoint _file
             (void . runIO) (upToMonoJuvix entryPoint)
         }
 

test/Scope/Negative.hs

@@ -23,7 +23,7 @@ testDescr NegTest {..} =
         { _testName = _name,
           _testRoot = tRoot,
           _testAssertion = Single $ do
-            let entryPoint = EntryPoint "." (pure _file)
+            let entryPoint = defaultEntryPoint _file
             res <- runIOEither (upToScoping entryPoint)
             case mapLeft fromMiniJuvixError res of
               Left (Just err) -> whenJust (_checkErr err) assertFailure

test/Scope/Positive.hs

@@ -33,7 +33,7 @@ testDescr PosTest {..} =
           _testAssertion = Steps $ \step -> do
             cwd <- getCurrentDirectory
             entryFile <- makeAbsolute _file
-            let entryPoint = EntryPoint cwd (pure entryFile)
+            let entryPoint = EntryPoint cwd False (pure entryFile)
 
             step "Parsing"
             p :: Parser.ParserResult <- runIO (upToParsing entryPoint)
@@ -57,14 +57,20 @@ testDescr PosTest {..} =
 
             step "Parsing pretty scoped"
             let fs2 = HashMap.singleton entryFile scopedPretty
-            p' :: Parser.ParserResult <- (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs2) (upToParsing entryPoint)
+            p' :: Parser.ParserResult <-
+              (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs2)
+                (upToParsing entryPoint)
 
             step "Parsing pretty parsed"
             let fs3 = HashMap.singleton entryFile parsedPretty
-            parsedPretty' :: Parser.ParserResult <- (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs3) (upToParsing entryPoint)
+            parsedPretty' :: Parser.ParserResult <-
+              (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs3)
+                (upToParsing entryPoint)
 
             step "Scoping the scoped"
-            s' :: Scoper.ScoperResult <- (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs) (upToScoping entryPoint)
+            s' :: Scoper.ScoperResult <-
+              (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs)
+                (upToScoping entryPoint)
 
             step "Checks"
             let smodules = s ^. Scoper.resultModules

test/Termination.hs

@@ -0,0 +1,8 @@
+module Termination (allTests) where
+
+import Base
+import Termination.Negative qualified as N
+import Termination.Positive qualified as P
+
+allTests :: TestTree
+allTests = testGroup "Termination checker tests" [P.allTests, N.allTests]

test/Termination/Negative.hs

@@ -0,0 +1,84 @@
+module Termination.Negative (module Termination.Negative) where
+
+import Base
+import MiniJuvix.Pipeline
+import MiniJuvix.Termination
+
+type FailMsg = String
+
+data NegTest = NegTest
+  { _name :: String,
+    _relDir :: FilePath,
+    _file :: FilePath,
+    _checkErr :: TerminationError -> Maybe FailMsg
+  }
+
+testDescr :: NegTest -> TestDescr
+testDescr NegTest {..} =
+  let tRoot = root </> _relDir
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Single $ do
+            let entryPoint = defaultEntryPoint _file
+            result <- runIOEither (upToMicroJuvix entryPoint)
+            case mapLeft fromMiniJuvixError result of
+              Left (Just lexError) -> whenJust (_checkErr lexError) assertFailure
+              Left Nothing -> assertFailure "The termination checker did not find an error."
+              Right _ -> assertFailure "An error ocurred but it was not by the termination checker."
+        }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Termination negative tests"
+    (map (mkTest . testDescr) tests)
+
+root :: FilePath
+root = "tests/negative/Termination"
+
+tests :: [NegTest]
+tests =
+  [ NegTest
+      "Mutual recursive functions non terminating"
+      "."
+      "Mutual.mjuvix"
+      $ \case
+        ErrNoLexOrder {} -> Nothing,
+    NegTest
+      "Another mutual block non terminating"
+      "."
+      "Ord.mjuvix"
+      $ \case
+        ErrNoLexOrder {} -> Nothing,
+    NegTest
+      "Only one function, f, marked terminating in a mutual block"
+      "."
+      "TerminatingF.mjuvix"
+      $ \case
+        ErrNoLexOrder {} -> Nothing,
+    NegTest
+      "Only one function, g, marked terminating in a mutual block"
+      "."
+      "TerminatingG.mjuvix"
+      $ \case
+        ErrNoLexOrder {} -> Nothing,
+    NegTest
+      "f x := f x is not terminating"
+      "."
+      "ToEmpty.mjuvix"
+      $ \case
+        ErrNoLexOrder {} -> Nothing,
+    NegTest
+      "Tree"
+      "."
+      "Data/Tree.mjuvix"
+      $ \case
+        ErrNoLexOrder {} -> Nothing,
+    NegTest
+      "Quicksort is not terminating"
+      "."
+      "Data/QuickSort.mjuvix"
+      $ \case
+        ErrNoLexOrder {} -> Nothing
+  ]

test/Termination/Positive.hs

@@ -0,0 +1,78 @@
+module Termination.Positive where
+
+import Base
+import MiniJuvix.Pipeline
+import Termination.Negative qualified as N
+
+data PosTest = PosTest
+  { _name :: String,
+    _relDir :: FilePath,
+    _file :: FilePath
+  }
+
+root :: FilePath
+root = "tests/positive/Termination"
+
+testDescr :: PosTest -> TestDescr
+testDescr PosTest {..} =
+  let tRoot = root </> _relDir
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Single $ do
+            let entryPoint = defaultEntryPoint _file
+            (void . runIO) (upToMicroJuvix entryPoint)
+        }
+
+--------------------------------------------------------------------------------
+-- Testing --no-termination flag with all termination negative tests
+--------------------------------------------------------------------------------
+
+rootNegTests :: FilePath
+rootNegTests = "tests/negative/Termination"
+
+testDescrFlag :: N.NegTest -> TestDescr
+testDescrFlag N.NegTest {..} =
+  let tRoot = rootNegTests </> _relDir
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Single $ do
+            let entryPoint = EntryPoint "." True (pure _file)
+            (void . runIO) (upToMicroJuvix entryPoint)
+        }
+
+--------------------------------------------------------------------------------
+
+tests :: [PosTest]
+tests =
+  [ PosTest "Ackerman nice def. is terminating" "." "Ack.mjuvix",
+    PosTest "Recursive functions on Lists" "." "Data/List.mjuvix"
+  ]
+
+testsWithKeyword :: [PosTest]
+testsWithKeyword =
+  [ PosTest "terminating added to fx:=fx" "." "ToEmpty.mjuvix",
+    PosTest "terminating for all functions in the mutual block" "." "Mutual.mjuvix",
+    PosTest "Undefined is terminating by assumption" "." "Undefined.mjuvix"
+  ]
+
+negTests :: [N.NegTest]
+negTests = N.tests
+
+--------------------------------------------------------------------------------
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "Positive tests"
+    [ testGroup
+        "Well-known terminating functions"
+        (map (mkTest . testDescr) tests),
+      testGroup
+        "Bypass checking using --non-termination flag on negative tests"
+        (map (mkTest . testDescrFlag) negTests),
+      testGroup
+        "Terminating keyword"
+        (map (mkTest . testDescr) testsWithKeyword)
+    ]

test/TypeCheck/Negative.hs

@@ -20,7 +20,7 @@ testDescr NegTest {..} =
         { _testName = _name,
           _testRoot = tRoot,
           _testAssertion = Single $ do
-            let entryPoint = EntryPoint "." (pure _file)
+            let entryPoint = defaultEntryPoint _file
             result <- runIOEither (upToMicroJuvixTyped entryPoint)
             case mapLeft fromMiniJuvixError result of
               Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure

test/TypeCheck/Positive.hs

@@ -19,7 +19,7 @@ testDescr PosTest {..} =
         { _testName = _name,
           _testRoot = tRoot,
           _testAssertion = Single $ do
-            let entryPoint = EntryPoint "." (pure _file)
+            let entryPoint = defaultEntryPoint _file
             (void . runIO) (upToMicroJuvixTyped entryPoint)
         }
 

tests/negative/Termination/Data/Bool.mjuvix

@@ -0,0 +1,25 @@
+module Data.Bool;
+  inductive Bool {
+    true : Bool;
+    false : Bool;
+  };
+
+  not : Bool → Bool;
+  not true ≔ false;
+  not false ≔ true;
+
+  infixr 2 ||;
+  || : Bool → Bool → Bool;
+  || false a ≔ a;
+  || true _ ≔ true;
+
+  infixr 2 &&;
+  && : Bool → Bool → Bool;
+  && false _ ≔ false;
+  && true a ≔ a;
+
+  ite : (a : Type) → Bool → a → a → a;
+  ite _ true a _ ≔ a;
+  ite _ false _ b ≔ b;
+
+end;

tests/negative/Termination/Data/Nat.mjuvix

@@ -0,0 +1,28 @@
+module Data.Nat;
+  inductive ℕ  {
+    zero : ℕ;
+    suc : ℕ → ℕ;
+  };
+
+  infixl 6 +;
+  + : ℕ → ℕ → ℕ;
+  + zero b ≔ b;
+  + (suc a) b ≔ suc (a + b);
+
+  infixl 7 *;
+  * : ℕ → ℕ → ℕ;
+  * zero b ≔ zero;
+  * (suc a) b ≔ b + a * b;
+
+  import Data.Bool;
+  open Data.Bool;
+
+  even : ℕ → Bool;
+  odd : ℕ → Bool;
+
+  even zero ≔ true;
+  even (suc n) ≔ odd n;
+
+  odd zero ≔ false;
+  odd (suc n) ≔ even n;
+end;

tests/negative/Termination/Data/QuickSort.mjuvix

@@ -0,0 +1,38 @@
+module Data.QuickSort;
+
+import Data.Bool;
+open Data.Bool;
+
+import Data.Nat;
+open Data.Nat;
+
+inductive List (A : Type) {
+  nil  : List A;
+  cons : A → List A → List A;
+};
+
+filter : (A : Type) → (A → Bool) → List A → List A;
+filter A f nil         ≔ nil A;
+filter A f (cons h hs) ≔ ite (List A) (f h)
+  (cons A h (filter A f hs))
+  (filter A f hs);
+
+concat : (A : Type) → List A → List A → List A;
+concat A nil ys         ≔ ys;
+concat A (cons x xs) ys ≔ cons A x (concat A xs ys);
+
+ltx : (A : Type) → (A → A → Bool) → A → A → Bool;
+ltx A lessThan x y ≔ lessThan y x;
+
+gex : (A : Type) → (A → A → Bool) → A → A → Bool;
+gex A lessThan x y ≔ not (ltx A lessThan x y) ;
+
+quicksort : (A : Type) → (A → A → Bool) → List A → List A;
+quicksort A _ nil ≔ nil A;
+quicksort A _ (cons x nil) ≔ cons A x (nil A);
+quicksort A lessThan (cons x ys) ≔
+  concat A (quicksort A lessThan (filter A (ltx A lessThan x) ys))
+           (concat A
+           (cons A x (nil A))
+           (quicksort A lessThan (filter A (gex A lessThan x)) ys));
+end;

tests/negative/Termination/Mutual.mjuvix

@@ -1,4 +1,4 @@
-module Loop;
+module Mutual;
 
 axiom A : Type;
 

tests/negative/Termination/Ord.mjuvix

@@ -0,0 +1,20 @@
+module Ord;
+
+import Data.Nat;
+open Data.Nat;
+
+inductive Ord {
+  ZOrd : Ord;
+  SOrd : Ord -> Ord;
+  Lim  : (ℕ -> Ord) -> Ord;
+};
+
+addord : Ord -> Ord -> Ord;
+aux-addord : (ℕ -> Ord) -> Ord -> (ℕ -> Ord);
+
+addord (Zord)   y := y;
+addord (SOrd x) y := SOrd (addord x y);
+addord (Lim f)  y := Lim (aux-addord f y);
+aux-addord f y z := addord (f z) y;
+
+end;

tests/positive/Polymorphism.mjuvix

@@ -23,6 +23,7 @@ inductive Bool {
 id : (A : Type) → A → A;
 id _ a ≔ a;
 
+terminating
 undefined : (A : Type) → A;
 undefined A ≔ undefined A;
 

tests/positive/Termination/Data/List.mjuvix

@@ -7,100 +7,49 @@ import Data.Nat;
 open Data.Nat;
 
 inductive List (A : Type) {
-  nil  : List A;
+  nil : List A;
   cons : A → List A → List A;
 };
 
 foldr : (A : Type) → (B : Type) → (A → B → B) → B → List A → B;
-foldr _ _ _ z (nil _) ≔ z;
-foldr A B f z (cons _ h hs) ≔ f h (foldr A B f z hs);
+foldr _ _ _ z nil ≔ z;
+foldr A B f z (cons h hs) ≔ f h (foldr A B f z hs);
 
 foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B;
-foldl A B f z (nil _) ≔ z ;
-foldl A B f z (cons _ h hs) ≔ foldl A B f (f z h) hs;
+foldl A B f z nil ≔ z ;
+foldl A B f z (cons h hs) ≔ foldl A B f (f z h) hs;
 
 map : (A : Type) → (B : Type) → (A → B) → List A → List B;
-map _ B f (nil _) ≔ nil B;
-map A B f (cons _ h hs) ≔ cons A (f h) (map A B f hs);
+map _ B f nil ≔ nil B;
+map A B f (cons h hs) ≔ cons B (f h) (map A B f hs);
 
 filter : (A : Type) → (A → Bool) → List A → List A;
-filter A f (nil _) ≔ nil A;
-filter A f (cons _ h hs) ≔ ite (List A) (f h)
+filter A f nil ≔ nil A;
+filter A f (cons h hs) ≔ ite (List A) (f h)
   (cons A h (filter A f hs))
   (filter A f hs);
 
 length : (A : Type) → List A → ℕ;
-length _ (nil _)      ≔ zero;
-length A (cons _ _ l) ≔ suc (length A l);
+length _ nil ≔ zero;
+length A (cons _ l) ≔ suc (length A l);
 
 rev : (A : Type) → List A → List A → List A;
-rev _ (nil _)       l ≔ l;
-rev A (cons _ x xs) l ≔ rev A xs (cons A x l);
+rev _ nil l ≔ l;
+rev A (cons x xs) l ≔ rev A xs (cons A x l);
 
 reverse : (A : Type) → List A → List A;
-reverse A l ≔ rev l (nil A);
+reverse A l ≔ rev A l (nil A);
 
 replicate : (A : Type) → ℕ → A → List A;
-replicate A zero _    ≔ nil A;
+replicate A zero _ ≔ nil A;
 replicate A (suc n) x ≔ cons A x (replicate A n x);
 
 take : (A : Type) → ℕ → List A → List A;
-take A (suc n) (cons _ x xs) ≔ cons A x (take A n xs);
-take A _ _                   ≔ nil A;
-
-alternate : (A : Type) → List A → List A → List A;
-alternate A (nil _)      b ≔ b;
-alternate A (cons _ h t) b ≔ cons A h (alternate A b t);
-
-merge : (A : Type) → (A → A → Bool) → List A → List A → List A;
-merge _ _ (nil _) ys ≔ ys;
-merge _ _ xs (nil _) ≔ xs;
-merge A lessThan (cons _ x xs) (cons _ y ys) ≔
-  ite (List A) (lessThan x y)
-          (cons A x (merge A lessThan xs (cons A y ys)))
-          (cons A y (merge A lessThan ys (cons A x xs)));
+take A (suc n) (cons x xs) ≔ cons A x (take A n xs);
+take A _ _ ≔ nil A;
 
 concat : (A : Type) → List A → List A → List A;
-concat A (nil _) ys       ≔ ys;
-concat A (cons _ x xs) ys ≔ cons A x (concat A xs ys);
-
-ltx : (A : Type) → (A → A → Bool) → A → A → Bool;
-ltx A lessThan x y ≔ lessThan y x;
-
-gex : (A : Type) → (A → A → Bool) → A → A → Bool;
-gex A lessThan x y ≔ not (ltx A lessThan x y) ;
-
-quickSort : (A : Type) → (A → A → Bool) → List A → List A;
-quickSort A _ (nil _)              ≔ nil A;
-quickSort A _ (cons _ x (nil _))   ≔ cons A x (nil A);
-quickSort A lessThan (cons _ x ys) ≔
-  concat A (quickSort A (filter A ltx) ys)
-           (concat A (cons A x (nil A)) (quickSort A (filter A gex) ys));
-
--- Mutual recursive function example
-
-aux  : (A : Type) → A → List A → List A;
-flat : (A : Type) → List A → List A;
-
-aux A (nil _) ls       := flat A ls;
-aux A (cons _ x xs) ls := cons A x (aux A xs ls);
-
-flat A (nil _)       := nil A;
-flat A (cons _ x xs) := aux A x xs;
-
-inductive Ord {
-  ZOrd : Ord;
-  SOrd : Ord -> Ord;
-  Lim  : (ℕ -> Ord) -> Ord;
-};
-
-addord : Ord -> Ord -> Ord;
-aux-addord : (ℕ -> Ord) -> Ord -> (ℕ -> Ord);
-
-addord (Zord)   y := y;
-addord (SOrd x) y := SOrd (addord x y);
-addord (Lim f)  y := Lim (aux-addord f y);
--- where
-aux-addord f y z := addord (f z) y;
+concat A nil ys ≔ ys;
+concat A (cons x xs) ys ≔ cons A x (concat A xs ys);
 
 end;

tests/positive/Termination/Data/Maybe.mjuvix

@@ -1,8 +0,0 @@
-module Data.Maybe;
-
-  inductive Maybe (a : Type) {
-     nothing : Maybe a;
-     just : a → Maybe a;
-  }
-
-end;

tests/positive/Termination/Data/Ord.mjuvix

@@ -1,7 +0,0 @@
-module Data.Ord;
-    inductive Ordering {
-      LT : Ordering;
-      EQ : Ordering;
-      GT : Ordering;
-    };
-end;

tests/positive/Termination/Data/Product.mjuvix

@@ -1,9 +0,0 @@
-module Data.Product;
-
-infixr 2 ×;
--- infixr 4 ,; waiting for implicit arguments
-inductive × (a : Type) (b : Type) {
-  , : a → b → a × b;
-};
-
-end;