Add typecheck and internal command (#270)

* Closes #269

* Add internal command

* w.i.p

* Fix shell tests.

* Rename check command and add shell-tests

app/Command.hs

@@ -2,38 +2,24 @@ module Command
   ( module Command,
     module Commands.Extra,
     module Commands.Html,
-    module Commands.MicroJuvix,
-    module Commands.Parse,
-    module Commands.Scope,
-    module Commands.Termination,
     module Commands.Compile,
+    module Commands.Internal,
   )
 where
 
 import Commands.Compile
 import Commands.Extra
 import Commands.Html
-import Commands.MicroJuvix
-import Commands.Parse
-import Commands.Scope
-import Commands.Termination
+import Commands.Internal
 import GlobalOptions
 import Juvix.Prelude hiding (Doc)
-import Juvix.Syntax.Concrete.Scoped.Pretty qualified as Scoper
 import Options.Applicative
 
 data Command
-  = Compile CompileOptions
-  | DisplayRoot
-  | Highlight
+  = Check
+  | Compile CompileOptions
   | Html HtmlOptions
-  | MicroJuvix MicroJuvixCommand
-  | MiniC
-  | MiniHaskell
-  | MonoJuvix
-  | Parse ParseOptions
-  | Scope ScopeOptions
-  | Termination TerminationCommand
+  | Internal InternalCommand
 
 data CommandGlobalOptions = CommandGlobalOptions
   { _cliCommand :: Command,
@@ -48,21 +34,21 @@ parseCommandGlobalOptions = do
   cmd <-
     hsubparser
       ( mconcat
-          [ commandCompile,
-            commandHighlight,
+          [ commandCheck,
+            commandCompile,
             commandHtml,
-            commandMicroJuvix,
-            commandMiniC,
-            commandMonoJuvix,
-            commandParse,
-            commandScope,
-            commandShowRoot,
-            commandTermination
+            commandInternal
           ]
       )
-      <|> hsubparser (commandMiniHaskell <> internal)
   return (cmd {_cliGlobalOptions = opts <> cmd ^. cliGlobalOptions})
 
+commandCheck :: Mod CommandFields CommandGlobalOptions
+commandCheck =
+  command "typecheck" $
+    info
+      (addGlobalOptions (pure Check))
+      (progDesc "Type check a Juvix file")
+
 commandCompile :: Mod CommandFields CommandGlobalOptions
 commandCompile =
   command "compile" $
@@ -70,13 +56,6 @@ commandCompile =
       (addGlobalOptions (Compile <$> parseCompile))
       (progDesc "Compile a Juvix file")
 
-commandHighlight :: Mod CommandFields CommandGlobalOptions
-commandHighlight =
-  command "highlight" $
-    info
-      (addGlobalOptions (pure Highlight))
-      (progDesc "Highlight a Juvix file")
-
 commandHtml :: Mod CommandFields CommandGlobalOptions
 commandHtml =
   command "html" $
@@ -84,61 +63,12 @@ commandHtml =
       (addGlobalOptions (Html <$> parseHtml))
       (progDesc "Generate HTML for a Juvix file")
 
-commandMiniC :: Mod CommandFields CommandGlobalOptions
-commandMiniC =
-  command "minic" $
+commandInternal :: Mod CommandFields CommandGlobalOptions
+commandInternal =
+  command "internal" $
     info
-      (addGlobalOptions (pure MiniC))
-      (progDesc "Translate a Juvix file to MiniC")
-
-commandMicroJuvix :: Mod CommandFields CommandGlobalOptions
-commandMicroJuvix =
-  command "microjuvix" $
-    info
-      (addGlobalOptions (MicroJuvix <$> parseMicroJuvixCommand))
-      (progDesc "Subcommands related to MicroJuvix")
-
-commandMiniHaskell :: Mod CommandFields CommandGlobalOptions
-commandMiniHaskell =
-  command "minihaskell" $
-    info
-      (addGlobalOptions (pure MiniHaskell))
-      (progDesc "Translate a Juvix file to MiniHaskell")
-
-commandMonoJuvix :: Mod CommandFields CommandGlobalOptions
-commandMonoJuvix =
-  command "monojuvix" $
-    info
-      (addGlobalOptions (pure MonoJuvix))
-      (progDesc "Translate a Juvix file to MonoJuvix")
-
-commandParse :: Mod CommandFields CommandGlobalOptions
-commandParse =
-  command "parse" $
-    info
-      (addGlobalOptions (Parse <$> parseParse))
-      (progDesc "Parse a Juvix file")
-
-commandScope :: Mod CommandFields CommandGlobalOptions
-commandScope =
-  command "scope" $
-    info
-      (addGlobalOptions (Scope <$> parseScope))
-      (progDesc "Parse and scope a Juvix file")
-
-commandShowRoot :: Mod CommandFields CommandGlobalOptions
-commandShowRoot =
-  command "root" $
-    info
-      (liftParserCmd (pure DisplayRoot))
-      (progDesc "Show the root path for a Juvix project")
-
-commandTermination :: Mod CommandFields CommandGlobalOptions
-commandTermination =
-  command "termination" $
-    info
-      (addGlobalOptions $ Termination <$> parseTerminationCommand)
-      (progDesc "Subcommands related to termination checking")
+      (addGlobalOptions (Internal <$> parseInternalCommand))
+      (progDesc "Internal subcommands")
 
 --------------------------------------------------------------------------------
 -- Misc
@@ -154,17 +84,10 @@ liftParserCmd cmd = cmdDefaultOptions <$> cmd
 addGlobalOptions :: Parser Command -> Parser CommandGlobalOptions
 addGlobalOptions parser = do
   flags1 <- parseGlobalFlags True
-  ~(opts2, _cliCommand) <- addParser (parseGlobalOptions True) parser
+  ~(opts2, _cliCommand) <- addParser (parseGlobalFlags True) parser
   fs <- parserInputFiles
   return
     CommandGlobalOptions
       { _cliGlobalOptions = flags1 <> opts2 <> mempty {_globalInputFiles = fs},
         ..
       }
-
-mkScopePrettyOptions :: GlobalOptions -> ScopeOptions -> Scoper.Options
-mkScopePrettyOptions g ScopeOptions {..} =
-  Scoper.defaultOptions
-    { Scoper._optShowNameIds = g ^. globalShowNameIds,
-      Scoper._optInlineImports = _scopeInlineImports
-    }

app/Commands/Extra.hs

@@ -1,10 +1,16 @@
 module Commands.Extra where
 
 import Juvix.Prelude hiding (Doc)
-import Options.Applicative
+import Options.Applicative hiding (hidden)
 import Options.Applicative.Builder.Internal
 import Options.Applicative.Types
 
+hidden :: Bool -> Mod f a
+hidden sure = optionMod $ \p ->
+  if
+      | not sure -> p
+      | otherwise -> p {propVisibility = min Hidden (propVisibility p)}
+
 parserInputFile :: Parser FilePath
 parserInputFile =
   argument
@@ -39,9 +45,3 @@ addParser parser = \case
   (BindP p k) -> BindP (addParser parser p) $ \(g1, x) ->
     BindP (addParser parser $ k x) $ \(g2, x') ->
       pure (g1 <> g2, x')
-
-hidden :: Bool -> Mod f a
-hidden sure = optionMod $ \p ->
-  if
-      | not sure -> p
-      | otherwise -> p {propVisibility = min Hidden (propVisibility p)}

app/Commands/Internal.hs

@@ -0,0 +1,105 @@
+module Commands.Internal
+  ( module Commands.Internal,
+    module Commands.Internal.MicroJuvix,
+    module Commands.Internal.Parse,
+    module Commands.Internal.Scope,
+    module Commands.Internal.Termination,
+  )
+where
+
+import Commands.Internal.MicroJuvix
+import Commands.Internal.Parse
+import Commands.Internal.Scope
+import Commands.Internal.Termination
+import Juvix.Prelude
+import Options.Applicative
+
+data InternalCommand
+  = DisplayRoot
+  | Highlight
+  | MicroJuvix MicroJuvixCommand
+  | MiniC
+  | MiniHaskell
+  | MonoJuvix
+  | Parse ParseOptions
+  | Scope ScopeOptions
+  | Termination TerminationCommand
+
+parseInternalCommand :: Parser InternalCommand
+parseInternalCommand =
+  hsubparser
+    ( mconcat
+        [ commandHighlight,
+          commandMicroJuvix,
+          commandMiniC,
+          commandMiniHaskell,
+          commandMonoJuvix,
+          commandParse,
+          commandScope,
+          commandShowRoot,
+          commandTermination
+        ]
+    )
+
+commandHighlight :: Mod CommandFields InternalCommand
+commandHighlight =
+  command "highlight" $
+    info
+      (pure Highlight)
+      (progDesc "Highlight a Juvix file")
+
+commandMiniC :: Mod CommandFields InternalCommand
+commandMiniC =
+  command "minic" $
+    info
+      (pure MiniC)
+      (progDesc "Translate a Juvix file to MiniC")
+
+commandMicroJuvix :: Mod CommandFields InternalCommand
+commandMicroJuvix =
+  command "microjuvix" $
+    info
+      (MicroJuvix <$> parseMicroJuvixCommand)
+      (progDesc "Subcommands related to MicroJuvix")
+
+commandMiniHaskell :: Mod CommandFields InternalCommand
+commandMiniHaskell =
+  command "minihaskell" $
+    info
+      (pure MiniHaskell)
+      (progDesc "Translate a Juvix file to MiniHaskell")
+
+commandMonoJuvix :: Mod CommandFields InternalCommand
+commandMonoJuvix =
+  command "monojuvix" $
+    info
+      (pure MonoJuvix)
+      (progDesc "Translate a Juvix file to MonoJuvix")
+
+commandParse :: Mod CommandFields InternalCommand
+commandParse =
+  command "parse" $
+    info
+      (Parse <$> parseParse)
+      (progDesc "Parse a Juvix file")
+
+commandScope :: Mod CommandFields InternalCommand
+commandScope =
+  command "scope" $
+    info
+      (Scope <$> parseScope)
+      (progDesc "Parse and scope a Juvix file")
+
+commandShowRoot :: Mod CommandFields InternalCommand
+commandShowRoot =
+  command "root" $
+    info
+      (pure DisplayRoot)
+      (progDesc "Show the root path for a Juvix project")
+
+commandTermination :: Mod CommandFields InternalCommand
+commandTermination =
+  command "termination" $
+    info
+      (Termination <$> parseTerminationCommand)
+      (progDesc "Subcommands related to termination checking")

app/Commands/Internal/MicroJuvix.hs

@@ -1,4 +1,4 @@
-module Commands.MicroJuvix where
+module Commands.Internal.MicroJuvix where
 
 import Juvix.Prelude hiding (Doc)
 import Options.Applicative
@@ -14,6 +14,22 @@ newtype MicroJuvixTypeOptions = MicroJuvixTypeOptions
 
 makeLenses ''MicroJuvixTypeOptions
 
+defaultMicroJuvixTypeOptions :: MicroJuvixTypeOptions
+defaultMicroJuvixTypeOptions =
+  MicroJuvixTypeOptions
+    { _microJuvixTypePrint = False
+    }
+
+instance Semigroup MicroJuvixTypeOptions where
+  o1 <> o2 =
+    MicroJuvixTypeOptions
+      { _microJuvixTypePrint = (o1 ^. microJuvixTypePrint) || (o2 ^. microJuvixTypePrint)
+      }
+
+instance Monoid MicroJuvixTypeOptions where
+  mempty = defaultMicroJuvixTypeOptions
+  mappend = (<>)
+
 parseMicroJuvixCommand :: Parser MicroJuvixCommand
 parseMicroJuvixCommand =
   hsubparser $

app/Commands/Internal/Parse.hs

@@ -1,6 +1,4 @@
-{-# LANGUAGE ApplicativeDo #-}
-
-module Commands.Parse where
+module Commands.Internal.Parse where
 
 import Juvix.Prelude hiding (Doc)
 import Options.Applicative

app/Commands/Internal/Scope.hs

@@ -1,6 +1,8 @@
-module Commands.Scope where
+module Commands.Internal.Scope where
 
+import GlobalOptions
 import Juvix.Prelude hiding (Doc)
+import Juvix.Syntax.Concrete.Scoped.Pretty qualified as Scoper
 import Options.Applicative
 
 newtype ScopeOptions = ScopeOptions
@@ -17,3 +19,10 @@ parseScope = do
           <> help "Show the code of imported modules next to the import statement"
       )
   pure ScopeOptions {..}
+
+mkScopePrettyOptions :: GlobalOptions -> ScopeOptions -> Scoper.Options
+mkScopePrettyOptions g ScopeOptions {..} =
+  Scoper.defaultOptions
+    { Scoper._optShowNameIds = g ^. globalShowNameIds,
+      Scoper._optInlineImports = _scopeInlineImports
+    }

app/Commands/Internal/Termination.hs

@@ -1,4 +1,4 @@
-module Commands.Termination where
+module Commands.Internal.Termination where
 
 import Control.Monad.Extra
 import Data.Text qualified as Text

app/Main.hs

@@ -2,7 +2,7 @@ module Main (main) where
 
 import App
 import CLI
-import Commands.Termination as Termination
+import Commands.Internal.Termination as Termination
 import Control.Exception qualified as IO
 import Control.Monad.Extra
 import Data.HashMap.Strict qualified as HashMap
@@ -85,151 +85,156 @@ runCommand cmdWithOpts = do
       toAnsiText' = toAnsiText (not (globalOpts ^. globalNoColors))
   root <- embed (findRoot cmdWithOpts)
   case cmd of
-    DisplayRoot -> say (pack root)
+    (Internal DisplayRoot) -> say (pack root)
     _ -> do
       -- Other commands require an entry point:
       case getEntryPoint root globalOpts of
         Nothing -> printFailureExit "Provide a Juvix file to run this command\nUse --help to see all the options"
-        Just entryPoint -> do
-          case cmd of
-            Highlight -> do
-              res <- runPipelineEither (upToScoping entryPoint)
-              case res of
-                Left err -> say (Highlight.goError (errorIntervals err))
-                Right r -> do
-                  let tbl = r ^. Scoper.resultParserTable
-                      items = tbl ^. Parser.infoParsedItems
-                      names = r ^. (Scoper.resultScoperTable . Scoper.infoNames)
-                      inputFile = entryPoint ^. mainModulePath
-                      hinput =
-                        Highlight.filterInput
-                          inputFile
-                          Highlight.HighlightInput
-                            { _highlightNames = names,
-                              _highlightParsed = items
+        Just entryPoint -> commandHelper cmd
+          where
+            commandHelper = \case
+              -- Visible commands
+              Check -> commandHelper (Internal (MicroJuvix (TypeCheck mempty)))
+              Compile localOpts -> do
+                miniC <- (^. MiniC.resultCCode) <$> runPipeline (upToMiniC entryPoint)
+                let inputFile = entryPoint ^. mainModulePath
+                result <- embed (runCompile root inputFile localOpts miniC)
+                case result of
+                  Left err -> printFailureExit err
+                  _ -> return ()
+              Html HtmlOptions {..} -> do
+                res <- runPipeline (upToScoping entryPoint)
+                let m = head (res ^. Scoper.resultModules)
+                embed (genHtml Scoper.defaultOptions _htmlRecursive _htmlTheme _htmlOutputDir _htmlPrintMetadata m)
+              (Internal cmd') -> case cmd' of
+                Highlight -> do
+                  res <- runPipelineEither (upToScoping entryPoint)
+                  case res of
+                    Left err -> say (Highlight.goError (errorIntervals err))
+                    Right r -> do
+                      let tbl = r ^. Scoper.resultParserTable
+                          items = tbl ^. Parser.infoParsedItems
+                          names = r ^. (Scoper.resultScoperTable . Scoper.infoNames)
+                          inputFile = entryPoint ^. mainModulePath
+                          hinput =
+                            Highlight.filterInput
+                              inputFile
+                              Highlight.HighlightInput
+                                { _highlightNames = names,
+                                  _highlightParsed = items
+                                }
+                      say (Highlight.go hinput)
+                Parse localOpts -> do
+                  m <-
+                    head . (^. Parser.resultModules)
+                      <$> runPipeline (upToParsing entryPoint)
+                  if localOpts ^. parseNoPrettyShow then say (show m) else say (pack (ppShow m))
+                Scope localOpts -> do
+                  l <-
+                    (^. Scoper.resultModules)
+                      <$> runPipeline
+                        (upToScoping entryPoint)
+                  forM_ l $ \s -> do
+                    renderStdOut (Scoper.ppOut (mkScopePrettyOptions globalOpts localOpts) s)
+                MicroJuvix Pretty -> do
+                  micro <-
+                    head . (^. Micro.resultModules)
+                      <$> runPipeline (upToMicroJuvix entryPoint)
+                  let ppOpts =
+                        Micro.defaultOptions
+                          { Micro._optShowNameIds = globalOpts ^. globalShowNameIds
+                          }
+                  App.renderStdOut (Micro.ppOut ppOpts micro)
+                MicroJuvix Arity -> do
+                  micro <- head . (^. MicroArity.resultModules) <$> runPipeline (upToMicroJuvixArity entryPoint)
+                  App.renderStdOut (Micro.ppOut Micro.defaultOptions micro)
+                MicroJuvix (TypeCheck localOpts) -> do
+                  res <- runPipeline (upToMicroJuvixTyped entryPoint)
+                  say "Well done! It type checks"
+                  when (localOpts ^. microJuvixTypePrint) $ do
+                    let ppOpts =
+                          Micro.defaultOptions
+                            { Micro._optShowNameIds = globalOpts ^. globalShowNameIds
                             }
-                  say (Highlight.go hinput)
-            Parse localOpts -> do
-              m <-
-                head . (^. Parser.resultModules)
-                  <$> runPipeline (upToParsing entryPoint)
-              if localOpts ^. parseNoPrettyShow then say (show m) else say (pack (ppShow m))
-            Scope localOpts -> do
-              l <-
-                (^. Scoper.resultModules)
-                  <$> runPipeline
-                    (upToScoping entryPoint)
-              forM_ l $ \s -> do
-                renderStdOut (Scoper.ppOut (mkScopePrettyOptions globalOpts localOpts) s)
-            Html HtmlOptions {..} -> do
-              res <- runPipeline (upToScoping entryPoint)
-              let m = head (res ^. Scoper.resultModules)
-              embed (genHtml Scoper.defaultOptions _htmlRecursive _htmlTheme _htmlOutputDir _htmlPrintMetadata m)
-            MicroJuvix Pretty -> do
-              micro <-
-                head . (^. Micro.resultModules)
-                  <$> runPipeline (upToMicroJuvix entryPoint)
-              let ppOpts =
-                    Micro.defaultOptions
-                      { Micro._optShowNameIds = globalOpts ^. globalShowNameIds
-                      }
-              App.renderStdOut (Micro.ppOut ppOpts micro)
-            MicroJuvix Arity -> do
-              micro <- head . (^. MicroArity.resultModules) <$> runPipeline (upToMicroJuvixArity entryPoint)
-              App.renderStdOut (Micro.ppOut Micro.defaultOptions micro)
-            MicroJuvix (TypeCheck localOpts) -> do
-              res <- runPipeline (upToMicroJuvixTyped entryPoint)
-              say "Well done! It type checks"
-              when (localOpts ^. microJuvixTypePrint) $ do
-                let ppOpts =
-                      Micro.defaultOptions
-                        { Micro._optShowNameIds = globalOpts ^. globalShowNameIds
-                        }
-                    checkedModule = head (res ^. MicroTyped.resultModules)
-                renderStdOut (Micro.ppOut ppOpts checkedModule)
-                newline
-                let typeCalls = Mono.buildTypeCallMap res
-                renderStdOut (Micro.ppOut ppOpts typeCalls)
-                newline
-                let concreteTypeCalls = Mono.collectTypeCalls res
-                renderStdOut (Micro.ppOut ppOpts concreteTypeCalls)
-            MonoJuvix -> do
-              let ppOpts =
-                    Mono.defaultOptions
-                      { Mono._optShowNameIds = globalOpts ^. globalShowNameIds
-                      }
-              monojuvix <- head . (^. Mono.resultModules) <$> runPipeline (upToMonoJuvix entryPoint)
-              renderStdOut (Mono.ppOut ppOpts monojuvix)
-            MiniHaskell -> do
-              minihaskell <-
-                head . (^. MiniHaskell.resultModules)
-                  <$> runPipeline (upToMiniHaskell entryPoint)
-              renderStdOut (MiniHaskell.ppOutDefault minihaskell)
-            MiniC -> do
-              miniC <- (^. MiniC.resultCCode) <$> runPipeline (upToMiniC entryPoint)
-              say miniC
-            Compile localOpts -> do
-              miniC <- (^. MiniC.resultCCode) <$> runPipeline (upToMiniC entryPoint)
-              let inputFile = entryPoint ^. mainModulePath
-              result <- embed (runCompile root inputFile localOpts miniC)
-              case result of
-                Left err -> printFailureExit err
-                _ -> return ()
-            Termination (Calls localOpts@CallsOptions {..}) -> do
-              results <- runPipeline (upToAbstract entryPoint)
-              let topModule = head (results ^. Abstract.resultModules)
-                  infotable = results ^. Abstract.resultTable
-                  callMap0 = Termination.buildCallMap infotable topModule
-                  callMap = case _callsFunctionNameFilter of
-                    Nothing -> callMap0
-                    Just f -> Termination.filterCallMap f callMap0
-                  localOpts' = Termination.callsPrettyOptions globalOpts localOpts
-              renderStdOut (Abstract.ppOut localOpts' callMap)
-              newline
-            Termination (CallGraph CallGraphOptions {..}) -> do
-              results <- runPipeline (upToAbstract entryPoint)
-              let topModule = head (results ^. Abstract.resultModules)
-                  infotable = results ^. Abstract.resultTable
-                  callMap = Termination.buildCallMap infotable topModule
-                  localOpts' =
-                    Abstract.defaultOptions
-                      { Abstract._optShowNameIds = globalOpts ^. globalShowNameIds
-                      }
-                  completeGraph = Termination.completeCallGraph callMap
-                  filteredGraph =
-                    maybe
-                      completeGraph
-                      (`Termination.unsafeFilterGraph` completeGraph)
-                      _graphFunctionNameFilter
-                  rEdges = Termination.reflexiveEdges filteredGraph
-                  recBehav = map Termination.recursiveBehaviour rEdges
-              App.renderStdOut (Abstract.ppOut localOpts' filteredGraph)
-              newline
-              forM_ recBehav $ \r -> do
-                let funName = r ^. Termination.recursiveBehaviourFun
-                    funRef = Abstract.FunctionRef funName
-                    funInfo =
-                      HashMap.lookupDefault
-                        impossible
-                        funRef
-                        (infotable ^. Abstract.infoFunctions)
-                    markedTerminating = funInfo ^. (Abstract.functionInfoDef . Abstract.funDefTerminating)
-                    ppOpts =
-                      Abstract.defaultOptions
-                        { Abstract._optShowNameIds = globalOpts ^. globalShowNameIds
-                        }
-                    n = toAnsiText' (Abstract.ppOut ppOpts funName)
-                App.renderStdOut (Abstract.ppOut localOpts' r)
-                newline
-                if
-                    | markedTerminating ->
-                        printSuccessExit (n <> " Terminates by assumption")
-                    | otherwise ->
-                        case Termination.findOrder r of
-                          Nothing ->
-                            printFailureExit (n <> " Fails the termination checking")
-                          Just (Termination.LexOrder k) ->
-                            printSuccessExit (n <> " Terminates with order " <> show (toList k))
+                        checkedModule = head (res ^. MicroTyped.resultModules)
+                    renderStdOut (Micro.ppOut ppOpts checkedModule)
+                    newline
+                    let typeCalls = Mono.buildTypeCallMap res
+                    renderStdOut (Micro.ppOut ppOpts typeCalls)
+                    newline
+                    let concreteTypeCalls = Mono.collectTypeCalls res
+                    renderStdOut (Micro.ppOut ppOpts concreteTypeCalls)
+                MonoJuvix -> do
+                  let ppOpts =
+                        Mono.defaultOptions
+                          { Mono._optShowNameIds = globalOpts ^. globalShowNameIds
+                          }
+                  monojuvix <- head . (^. Mono.resultModules) <$> runPipeline (upToMonoJuvix entryPoint)
+                  renderStdOut (Mono.ppOut ppOpts monojuvix)
+                MiniHaskell -> do
+                  minihaskell <-
+                    head . (^. MiniHaskell.resultModules)
+                      <$> runPipeline (upToMiniHaskell entryPoint)
+                  renderStdOut (MiniHaskell.ppOutDefault minihaskell)
+                MiniC -> do
+                  miniC <- (^. MiniC.resultCCode) <$> runPipeline (upToMiniC entryPoint)
+                  say miniC
+                Termination (Calls localOpts@CallsOptions {..}) -> do
+                  results <- runPipeline (upToAbstract entryPoint)
+                  let topModule = head (results ^. Abstract.resultModules)
+                      infotable = results ^. Abstract.resultTable
+                      callMap0 = Termination.buildCallMap infotable topModule
+                      callMap = case _callsFunctionNameFilter of
+                        Nothing -> callMap0
+                        Just f -> Termination.filterCallMap f callMap0
+                      localOpts' = Termination.callsPrettyOptions globalOpts localOpts
+                  renderStdOut (Abstract.ppOut localOpts' callMap)
+                  newline
+                Termination (CallGraph CallGraphOptions {..}) -> do
+                  results <- runPipeline (upToAbstract entryPoint)
+                  let topModule = head (results ^. Abstract.resultModules)
+                      infotable = results ^. Abstract.resultTable
+                      callMap = Termination.buildCallMap infotable topModule
+                      localOpts' =
+                        Abstract.defaultOptions
+                          { Abstract._optShowNameIds = globalOpts ^. globalShowNameIds
+                          }
+                      completeGraph = Termination.completeCallGraph callMap
+                      filteredGraph =
+                        maybe
+                          completeGraph
+                          (`Termination.unsafeFilterGraph` completeGraph)
+                          _graphFunctionNameFilter
+                      rEdges = Termination.reflexiveEdges filteredGraph
+                      recBehav = map Termination.recursiveBehaviour rEdges
+                  App.renderStdOut (Abstract.ppOut localOpts' filteredGraph)
+                  newline
+                  forM_ recBehav $ \r -> do
+                    let funName = r ^. Termination.recursiveBehaviourFun
+                        funRef = Abstract.FunctionRef funName
+                        funInfo =
+                          HashMap.lookupDefault
+                            impossible
+                            funRef
+                            (infotable ^. Abstract.infoFunctions)
+                        markedTerminating = funInfo ^. (Abstract.functionInfoDef . Abstract.funDefTerminating)
+                        ppOpts =
+                          Abstract.defaultOptions
+                            { Abstract._optShowNameIds = globalOpts ^. globalShowNameIds
+                            }
+                        n = toAnsiText' (Abstract.ppOut ppOpts funName)
+                    App.renderStdOut (Abstract.ppOut localOpts' r)
+                    newline
+                    if
+                        | markedTerminating ->
+                            printSuccessExit (n <> " Terminates by assumption")
+                        | otherwise ->
+                            case Termination.findOrder r of
+                              Nothing ->
+                                printFailureExit (n <> " Fails the termination checking")
+                              Just (Termination.LexOrder k) ->
+                                printSuccessExit (n <> " Terminates with order " <> show (toList k))
+                _ -> impossible
 
 showHelpText :: ParserPrefs -> IO ()
 showHelpText p = do

juvix-mode/flycheck-juvix.el

@@ -9,7 +9,7 @@
 
 (flycheck-define-checker juvix
   "A Juvix syntax checker."
-  :command ("juvix" "microjuvix" "typecheck" "--only-errors" "--no-colors"
+  :command ("juvix" "internal" "microjuvix" "typecheck" "--only-errors" "--no-colors"
             (option-flag "--no-stdlib" juvix-disable-embedded-stdlib)
             source-original)
   :error-patterns

juvix-mode/juvix-input.el

@@ -1,5 +1,5 @@
 ;;; -*- lexical-binding: t; -*-
-;;; juvix-input.el --- The juvix input method
+;;; juvix-input.el --- The Juvix input method
 
 ;; Copyright (c) 2005-2021 remains with the authors.
 ;; Agda 2 was originally written by Ulf Norell,

juvix-mode/juvix-mode.el

@@ -16,7 +16,7 @@
   "Keymap for Juvix mode.")
 
 ;;;###autoload
-(add-to-list 'auto-mode-alist '("\\.m?juvix\\'" . juvix-mode))
+(add-to-list 'auto-mode-alist '("\\.juvix\\'" . juvix-mode))
 
 (define-derived-mode juvix-mode prog-mode "Juvix-v0.2.1"
 
@@ -48,7 +48,7 @@
   (interactive)
   (save-buffer)
   (juvix-clear-annotations)
-  (eval (read (shell-command-to-string (concat "juvix highlight " (if juvix-disable-embedded-stdlib "--no-stdlib " "") (buffer-file-name)))))
+  (eval (read (shell-command-to-string (concat "juvix internal highlight " (if juvix-disable-embedded-stdlib "--no-stdlib " "") (buffer-file-name)))))
   (save-buffer)
   )
 

tests/CLI/Commands/internals/microjuvix.test

@@ -0,0 +1,37 @@
+$ juvix internal microjuvix
+>2 /Usage: juvix internal microjuvix.*/
+>= 1
+
+$ juvix internal microjuvix --help
+> /Usage: juvix internal microjuvix COMMAND.*/
+>= 0
+
+$ juvix internal microjuvix pretty
+> /Provide.*/
+>= 1
+
+$ juvix internal microjuvix typecheck
+> /Provide.*/
+>= 1
+
+$ juvix internal microjuvix typecheck tests/positive/MicroJuvix/Simple.juvix
+>
+Well done! It type checks
+>= 0
+
+$ juvix internal --only-errors microjuvix typecheck tests/positive/MicroJuvix/Simple.juvix
+>
+>= 0
+
+$ juvix internal microjuvix typecheck --only-errors tests/positive/MicroJuvix/Simple.juvix
+>
+>= 0
+
+$ juvix internal microjuvix typecheck tests/positive/MicroJuvix/Simple.juvix --only-errors
+>
+>= 0
+
+$ juvix internal microjuvix typecheck tests/negative/MicroJuvix/MultiWrongType.juvix --no-colors
+>2 /(.+)\/([^\/]+)\.juvix\:11\:7\-8\: error.*
+.*/
+>= 1

tests/CLI/Commands/internals/minic.test

@@ -0,0 +1,3 @@
+$ juvix internal minic
+> /Provide.*/
+>= 1

tests/CLI/Commands/internals/minihaskell.test

@@ -0,0 +1,3 @@
+$ juvix internal minihaskell
+> /Provide.*/
+>= 1

tests/CLI/Commands/internals/monojuvix.test

@@ -0,0 +1,3 @@
+$ juvix internal monojuvix
+> /Provide.*/
+>= 1

tests/CLI/Commands/internals/parse.test

@@ -0,0 +1,14 @@
+$ juvix internal parse
+> /Provide.*/
+>= 1
+
+$ juvix internal parse tests/positive/Axiom.juvix
+> /Module
+*/
+>2
+>= 0
+
+$ juvix internal parse --no-pretty-show tests/positive/Axiom.juvix
+> /Module \{.*/
+>2
+>= 0

tests/CLI/Commands/internals/root.test

@@ -1,3 +1,3 @@
-$ juvix root
+$ juvix internal root
 > /(.+)\/([^\/]+)/
 >= 0

tests/CLI/Commands/internals/scope.test

@@ -0,0 +1,3 @@
+$ juvix internal scope
+> /Provide.*/
+>= 1

tests/CLI/Commands/internals/termination.test

@@ -0,0 +1,23 @@
+$ juvix internal termination
+>2 /Usage: juvix internal termination COMMAND.*/
+>= 1
+
+$ juvix internal termination calls
+> /Provide.*/
+>2
+>=1
+
+$ juvix internal termination graph
+> /Provide.*/
+>2
+>= 1
+
+
+$ juvix internal termination calls --help
+> /Usage: juvix internal termination calls 
+         \[\-f|\-\-function fun1 fun2 ...] \[\-d|\-\-show\-decreasing\-args ARG].*/
+>= 0
+
+$ juvix internal termination graph --help
+> /Usage: juvix internal termination graph \[\-f\|\-\-function ARG\].*/
+>= 0

tests/CLI/Commands/microjuvix.test

@@ -1,37 +0,0 @@
-$ juvix microjuvix
->2 /Usage: juvix microjuvix .*/
->= 1
-
-$ juvix microjuvix --help
-> /Usage: juvix microjuvix COMMAND \[JUVIX_FILE\].*/
->= 0
-
-$ juvix microjuvix pretty
-> /Provide.*/
->= 1
-
-$ juvix microjuvix typecheck
-> /Provide.*/
->= 1
-
-$ juvix microjuvix typecheck tests/positive/MicroJuvix/Simple.juvix
->
-Well done! It type checks
->= 0
-
-$ juvix --only-errors microjuvix typecheck tests/positive/MicroJuvix/Simple.juvix
->
->= 0
-
-$ juvix microjuvix typecheck --only-errors tests/positive/MicroJuvix/Simple.juvix
->
->= 0
-
-$ juvix microjuvix typecheck tests/positive/MicroJuvix/Simple.juvix --only-errors
->
->= 0
-
-$ juvix microjuvix typecheck tests/negative/MicroJuvix/MultiWrongType.juvix --no-colors
->2 /(.+)\/([^\/]+)\.juvix\:11\:7\-8\: error.*
-.*/
->= 1

tests/CLI/Commands/minic.test

@@ -1,3 +0,0 @@
-$ juvix minic
-> /Provide.*/
->= 1

tests/CLI/Commands/minihaskell.test

@@ -1,3 +0,0 @@
-$ juvix minihaskell
-> /Provide.*/
->= 1

tests/CLI/Commands/monojuvix.test

@@ -1,3 +0,0 @@
-$ juvix monojuvix
-> /Provide.*/
->= 1

tests/CLI/Commands/parse.test

@@ -1,14 +0,0 @@
-$ juvix parse
-> /Provide.*/
->= 1
-
-$ juvix parse tests/positive/Axiom.juvix
-> /Module
-*/
->2
->= 0
-
-$ juvix parse tests/positive/Axiom.juvix --no-pretty-show
-> /Module \{.*/
->2
->= 0

tests/CLI/Commands/scope.test

@@ -1,3 +0,0 @@
-$ juvix scope
-> /Provide.*/
->= 1

tests/CLI/Commands/termination.test

@@ -1,23 +0,0 @@
-$ juvix termination
->2 /Usage\: juvix termination COMMAND \[JUVIX_FILE\].*/
->= 1
-
-$ juvix termination calls
-> /Provide.*/
->2
->=1
-
-$ juvix termination graph
-> /Provide.*/
->2
->= 1
-
-
-$ juvix termination calls --help
-> /Usage\: juvix termination calls \[JUVIX_FILE\] \[\-f\|\-\-function fun1 fun2 ...\] 
-                               \[\-d\|\-\-show\-decreasing\-args ARG\].*/
->= 0
-
-$ juvix termination graph --help
-> /Usage\: juvix termination graph \[JUVIX_FILE\] \[\-f\|\-\-function ARG\].*/
->= 0

tests/CLI/Commands/typecheck.test

@@ -0,0 +1,29 @@
+$ juvix typecheck
+> /Provide.*/
+>= 1
+
+$ juvix typecheck --help
+> /Usage: juvix typecheck \[JUVIX\_FILE\].*/
+>= 0
+
+$ juvix typecheck tests/positive/MicroJuvix/Simple.juvix
+>
+Well done! It type checks
+>= 0
+
+$ juvix --only-errors typecheck tests/positive/MicroJuvix/Simple.juvix
+>
+>= 0
+
+$ juvix typecheck --only-errors tests/positive/MicroJuvix/Simple.juvix
+>
+>= 0
+
+$ juvix typecheck tests/positive/MicroJuvix/Simple.juvix --only-errors
+>
+>= 0
+
+$ juvix typecheck tests/negative/MicroJuvix/MultiWrongType.juvix --no-colors
+>2 /(.+)\/([^\/]+)\.juvix\:11\:7\-8\: error.*
+.*/
+>= 1