[termination] add termination subcommands

app/Commands/Extra.hs

@@ -0,0 +1,17 @@
+module Commands.Extra where
+
+import qualified MiniJuvix.Translation.ScopedToAbstract as A
+import qualified Data.Text as Text
+import Control.Monad.Extra
+import Options.Applicative
+import Options.Applicative.Help.Pretty
+import qualified MiniJuvix.Syntax.Abstract.Pretty.Base as A
+import MiniJuvix.Prelude hiding (Doc)
+
+parseInputFile :: Parser FilePath
+parseInputFile =
+ argument
+      str
+      ( metavar "MINIJUVIX_FILE"
+          <> help "Path to a .mjuvix file"
+      )

app/Commands/Termination.hs

@@ -0,0 +1,101 @@
+{-# LANGUAGE ApplicativeDo #-}
+module Commands.Termination where
+
+import Commands.Extra
+import qualified Data.Text as Text
+import Control.Monad.Extra
+import Options.Applicative
+import qualified MiniJuvix.Syntax.Abstract.Pretty.Base as A
+import MiniJuvix.Prelude hiding (Doc)
+
+data TerminationCommand =
+  Calls CallsOptions
+  | CallGraph CallGraphOptions
+
+data CallsOptions = CallsOptions
+  { _callsInputFile :: FilePath,
+    _callsShowIds :: Bool,
+    _callsFunctionNameFilter :: Maybe (NonEmpty Text),
+    _callsShowDecreasingArgs :: A.ShowDecrArgs
+  }
+
+data CallGraphOptions = CallGraphOptions
+  { _graphInputFile :: FilePath,
+    _graphFunctionNameFilter :: Maybe (NonEmpty Text)
+  }
+
+parseCalls :: Parser CallsOptions
+parseCalls = do
+  _callsInputFile <- parseInputFile
+  _callsShowIds <-
+    switch
+      ( long "show-name-ids"
+          <> help "Show the unique number of each identifier"
+      )
+  _callsFunctionNameFilter <-
+    fmap msum . optional $ nonEmpty . Text.words <$> option str
+      ( long "function"
+          <> short 'f'
+          <> metavar "fun1 fun2 ..."
+          <> help "Only shows the specified functions"
+      )
+  _callsShowDecreasingArgs <-
+    option decrArgsParser
+      ( long "show-decreasing-args"
+          <> short 'd'
+          <> value A.ArgRel
+          <> help "possible values: argument, relation, both"
+      )
+  pure CallsOptions {..}
+  where
+  decrArgsParser :: ReadM A.ShowDecrArgs
+  decrArgsParser = eitherReader $ \s ->
+    case map toLower s of
+      "argument" -> return A.OnlyArg
+      "relation" -> return A.OnlyRel
+      "both" -> return A.ArgRel
+      _ -> Left "bad argument"
+
+
+parseCallGraph :: Parser CallGraphOptions
+parseCallGraph = do
+  _graphInputFile <- parseInputFile
+  _graphFunctionNameFilter <-
+    fmap msum . optional $ nonEmpty . Text.words <$> option str
+      ( long "function"
+          <> short 'f'
+          <> help "Only shows the specified function"
+      )
+  pure CallGraphOptions {..}
+
+parseTerminationCommand :: Parser TerminationCommand
+parseTerminationCommand =
+  hsubparser $
+    mconcat
+      [ commandCalls,
+        commandGraph
+      ]
+  where
+    commandCalls :: Mod CommandFields TerminationCommand
+    commandCalls = command "calls" minfo
+      where
+        minfo :: ParserInfo TerminationCommand
+        minfo =
+          info
+            (Calls <$> parseCalls)
+            (progDesc "Compute the calls table of a .mjuvix file")
+    commandGraph :: Mod CommandFields TerminationCommand
+    commandGraph = command "graph" minfo
+      where
+        minfo :: ParserInfo TerminationCommand
+        minfo =
+          info
+            (CallGraph <$> parseCallGraph)
+            (progDesc "Compute the complete call graph of a .mjuvix file")
+
+callsPrettyOptions :: CallsOptions -> A.Options
+callsPrettyOptions CallsOptions {..} =
+  A.defaultOptions
+    { A._optShowNameId = _callsShowIds,
+      A._optShowDecreasingArgs = _callsShowDecreasingArgs
+    }

app/Main.hs

@@ -18,16 +18,14 @@ import Text.Show.Pretty hiding (Html)
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (defaultOptions)
 import qualified MiniJuvix.Syntax.Abstract.Pretty.Ansi as A
-import qualified MiniJuvix.Termination.CallGraph as T
-import qualified Data.Text as Text
-import qualified MiniJuvix.Termination.CallGraph as T
+import Commands.Extra
+import Commands.Termination as T
 
 data Command
   = Scope ScopeOptions
   | Parse ParseOptions
   | Html HtmlOptions
-  | Calls CallsOptions
-  | CallGraph CallGraphOptions
+  | Termination TerminationCommand
 
 data ScopeOptions = ScopeOptions
   { _scopeRootDir :: FilePath,
@@ -47,18 +45,6 @@ data HtmlOptions = HtmlOptions
     _htmlTheme :: Theme
   }
 
-data CallsOptions = CallsOptions
-  { _callsInputFile :: FilePath,
-    _callsShowIds :: Bool,
-    _callsFunctionNameFilter :: Maybe [Text],
-    _callsShowDecreasingArgs :: A.ShowDecrArgs
-  }
-
-data CallGraphOptions = CallGraphOptions
-  { _graphInputFile :: FilePath,
-    _graphFunctionNameFilter :: Maybe [Text]
-  }
-
 parseHtml :: Parser HtmlOptions
 parseHtml = do
   _htmlInputFile <- parseInputFile
@@ -82,58 +68,8 @@ parseHtml = do
     "ayu" -> Right Ayu
     _ -> Left $ "unrecognised theme: " <> s
 
-parseCalls :: Parser CallsOptions
-parseCalls = do
-  _callsInputFile <- parseInputFile
-  _callsShowIds <-
-    switch
-      ( long "show-name-ids"
-          <> help "Show the unique number of each identifier"
-      )
-  _callsFunctionNameFilter <-
-    optional $ Text.words <$> option str
-      ( long "function"
-          <> short 'f'
-          <> metavar "fun1 fun2 ..."
-          <> help "Only shows the specified functions"
-      )
-  _callsShowDecreasingArgs <-
-    option decrArgsParser
-      ( long "show-decreasing-args"
-          <> short 'd'
-          <> value A.ArgRel
-          <> help "possible values: argument, relation, both"
-      )
-  pure CallsOptions {..}
-  where
-  decrArgsParser :: ReadM A.ShowDecrArgs
-  decrArgsParser = eitherReader $ \s ->
-    case map toLower s of
-      "argument" -> return A.OnlyArg
-      "relation" -> return A.OnlyRel
-      "both" -> return A.ArgRel
-      _ -> Left "bad argument"
 
 
-parseCallGraph :: Parser CallGraphOptions
-parseCallGraph = do
-  _graphInputFile <- parseInputFile
-  _graphFunctionNameFilter <-
-    optional $ Text.words <$> option str
-      ( long "function"
-          <> short 'f'
-          <> help "Only shows the specified function"
-      )
-  pure CallGraphOptions {..}
-
-parseInputFile :: Parser FilePath
-parseInputFile =
- argument
-      str
-      ( metavar "MINIJUVIX_FILE"
-          <> help "Path to a .mjuvix file"
-      )
-
 parseParse :: Parser ParseOptions
 parseParse = do
   _parseInputFile <- parseInputFile
@@ -195,8 +131,7 @@ parseCommand =
       [ commandParse,
         commandScope,
         commandHtml,
-        commandCalls,
-        commandGraph
+        commandTermination
       ]
   where
     commandParse :: Mod CommandFields Command
@@ -224,22 +159,14 @@ parseCommand =
           info
             (Scope <$> parseScope)
             (progDesc "Parse and scope a .mjuvix file")
-    commandCalls :: Mod CommandFields Command
-    commandCalls = command "calls" minfo
+    commandTermination :: Mod CommandFields Command
+    commandTermination = command "termination" minfo
       where
         minfo :: ParserInfo Command
         minfo =
           info
-            (Calls <$> parseCalls)
-            (progDesc "Compute the calls table of a .mjuvix file")
-    commandGraph :: Mod CommandFields Command
-    commandGraph = command "graph" minfo
-      where
-        minfo :: ParserInfo Command
-        minfo =
-          info
-            (CallGraph <$> parseCallGraph)
-            (progDesc "Compute the complete call graph of a .mjuvix file")
+            (Termination <$> parseTerminationCommand)
+            (progDesc "Subcommands related to termination checking")
 
 
 mkScopePrettyOptions :: ScopeOptions -> M.Options
@@ -249,13 +176,6 @@ mkScopePrettyOptions ScopeOptions {..} =
       M._optInlineImports = _scopeInlineImports
     }
 
-mkAbstractPrettyOptions :: CallsOptions -> A.Options
-mkAbstractPrettyOptions CallsOptions {..} =
-  A.defaultOptions
-    { A._optShowNameId = _callsShowIds,
-      A._optShowDecreasingArgs = _callsShowDecreasingArgs
-    }
-
 parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop)
 parseModuleIO = fromRightIO id . M.runModuleParserIO
 
@@ -284,7 +204,7 @@ go c = do
       m <- parseModuleIO _htmlInputFile
       s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       genHtml defaultOptions _htmlRecursive _htmlTheme s
-    Calls opts@CallsOptions {..} -> do
+    Termination (Calls opts@CallsOptions {..}) -> do
       m <- parseModuleIO _callsInputFile
       s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       a <- fromRightIO' putStrLn (return $ A.translateModule s)
@@ -292,10 +212,10 @@ go c = do
           callMap = case _callsFunctionNameFilter of
             Nothing -> callMap0
             Just f -> T.filterCallMap f callMap0
-          opts' = mkAbstractPrettyOptions opts
+          opts' = T.callsPrettyOptions opts
       A.printPrettyCode opts' callMap
       putStrLn ""
-    CallGraph CallGraphOptions {..} -> do
+    Termination (CallGraph CallGraphOptions {..}) -> do
       m <- parseModuleIO _graphInputFile
       s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       a <- fromRightIO' putStrLn (return $ A.translateModule s)

src/MiniJuvix/Prelude/Base.hs

@@ -80,7 +80,7 @@ import Data.HashSet (HashSet)
 import Data.Hashable
 import Data.Int
 import Data.List.Extra hiding (head, last)
-import Data.List.NonEmpty.Extra (NonEmpty (..), head, last, nonEmpty, minimum1, minimumOn1, maximum1, maximumOn1)
+import Data.List.NonEmpty.Extra (NonEmpty (..), head, last, nonEmpty, minimum1, minimumOn1, maximum1, maximumOn1, some1)
 import qualified Data.List.NonEmpty as NonEmpty
 import Data.Maybe
 import Data.Singletons.Sigma

src/MiniJuvix/Termination/CallGraph.hs

@@ -72,7 +72,7 @@ fromFunCall caller fc =
 
 -- | IMPORTANT: the resulting call graph is not complete. Use this function
 -- only to filter the pretty printed graph
-unsafeFilterGraph :: [Text] -> CompleteCallGraph -> CompleteCallGraph
+unsafeFilterGraph :: Foldable f => f Text -> CompleteCallGraph -> CompleteCallGraph
 unsafeFilterGraph funNames (CompleteCallGraph g) =
   CompleteCallGraph (HashMap.filterWithKey  (\(f , _) _ -> S.symbolText f `elem`funNames) g)
 

src/MiniJuvix/Termination/Types.hs

@@ -7,7 +7,6 @@ module MiniJuvix.Termination.Types (
 
 import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Abstract.Language as A
-import qualified MiniJuvix.Syntax.Concrete.Name as C
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import qualified Data.HashMap.Strict as HashMap
 import Prettyprinter as PP
@@ -99,5 +98,5 @@ instance PrettyCode CallRow where
 instance PrettyCode CallMatrix where
   ppCode l = vsep <$> mapM ppCode l
 
-filterCallMap :: [Text] -> CallMap -> CallMap
+filterCallMap :: Foldable f => f Text -> CallMap -> CallMap
 filterCallMap funNames = over callMap (HashMap.filterWithKey (\k _ -> S.symbolText k `elem` funNames))