cli and TypeCheckingMode

app/App.hs

@@ -223,11 +223,18 @@ runPipelineTermination ::
   (Members '[EmbedIO, App, Logger, TaggedLock] r) =>
   Maybe (AppPath File) ->
   Sem (Termination ': PipelineEff r) a ->
-  Sem r (PipelineResult a)
+  Sem r (PipelineResult (TerminationState, a))
 runPipelineTermination input_ p = silenceProgressLog $ do
-  r <- runPipelineEither () input_ (evalTermination iniTerminationState (inject p)) >>= fromRightJuvixError
+  r <- runPipelineEither () input_ (runTermination iniTerminationState (inject p)) >>= fromRightJuvixError
   return (snd r)
 
+evalPipelineTermination ::
+  (Members '[EmbedIO, App, Logger, TaggedLock] r) =>
+  Maybe (AppPath File) ->
+  Sem (Termination ': PipelineEff r) a ->
+  Sem r (PipelineResult a)
+evalPipelineTermination input_ p = fmap snd <$> runPipelineTermination input_ p
+
 runPipelineNoOptions ::
   (Members '[App, EmbedIO, Logger, TaggedLock] r) =>
   Maybe (AppPath File) ->

app/Commands/Dev.hs

@@ -12,6 +12,7 @@ import Commands.Dev.DevCompile qualified as DevCompile
 import Commands.Dev.DisplayRoot qualified as DisplayRoot
 import Commands.Dev.Highlight qualified as Highlight
 import Commands.Dev.ImportTree qualified as ImportTree
+import Commands.Dev.InstanceTermination qualified as InstanceTermination
 import Commands.Dev.Internal qualified as Internal
 import Commands.Dev.Latex qualified as Latex
 import Commands.Dev.MigrateJuvixYaml qualified as MigrateJuvixYaml
@@ -35,6 +36,7 @@ runCommand = \case
   Scope opts -> Scope.runCommand opts
   Internal opts -> Internal.runCommand opts
   Termination opts -> Termination.runCommand opts
+  InstanceTermination opts -> InstanceTermination.runCommand opts
   Core opts -> Core.runCommand opts
   Asm opts -> Asm.runCommand opts
   Reg opts -> Reg.runCommand opts

app/Commands/Dev/InstanceTermination.hs

@@ -4,6 +4,6 @@ import Commands.Base
 import Commands.Dev.InstanceTermination.Calls qualified as Calls
 import Commands.Dev.InstanceTermination.Options
 
-runCommand :: InstanceTerminationCommand -> Sem r ()
+runCommand :: (Members AppEffects r) => InstanceTerminationCommand -> Sem r ()
 runCommand = \case
   Calls opts -> Calls.runCommand opts

app/Commands/Dev/InstanceTermination/Calls.hs

@@ -2,6 +2,22 @@ module Commands.Dev.InstanceTermination.Calls where
 
 import Commands.Base
 import Commands.Dev.InstanceTermination.Calls.Options
+import Juvix.Compiler.Internal.Pretty
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Options
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 
-runCommand :: CallsOptions -> Sem r ()
-runCommand CallsOptions {} = return ()
+runCommand :: (Members AppEffects r) => CallsOptions -> Sem r ()
+runCommand localOpts@CallsOptions {..} = do
+  globalOpts <- askGlobalOptions
+  let tco =
+        TypeCheckingOptions
+          { _typeCheckingMode = TypeCheckingBuildCallMap
+          }
+  PipelineResult {..} <-
+    runReader tco $
+      runPipelineTermination (Just _callsInputFile) upToInternalTypedOptions
+  let res :: InstanceCallMaps = snd _pipelineResult ^. resultInstanceCallMaps
+  forM_ (res ^. instanceCallMaps) $
+    \(block :: InstanceCallMap) -> do
+      renderStdOut (ppOut (globalOpts, localOpts) (block ^. instanceCallMap))
+      newline

app/Commands/Dev/InstanceTermination/Options.hs

@@ -26,4 +26,4 @@ parseInstanceTerminationCommand =
         minfo =
           info
             (Calls <$> parseCalls)
-            (progDesc "Compute the calls table of a .juvix file")
+            (progDesc "Compute the instance constraints table of a .juvix file")

app/Commands/Dev/Internal/Pretty.hs

@@ -8,5 +8,5 @@ import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
 runCommand :: (Members AppEffects r) => InternalPrettyOptions -> Sem r ()
 runCommand opts = do
   globalOpts <- askGlobalOptions
-  intern <- (^. pipelineResult . Internal.resultModule) <$> runPipelineTermination (opts ^. internalPrettyInputFile) upToInternal
+  intern <- (^. pipelineResult . Internal.resultModule) <$> evalPipelineTermination (opts ^. internalPrettyInputFile) upToInternal
   renderStdOut (Internal.ppOut globalOpts intern)

app/Commands/Dev/Options.hs

@@ -19,6 +19,7 @@ import Commands.Dev.DevCompile.Options (DevCompileCommand, parseDevCompileComman
 import Commands.Dev.DisplayRoot.Options
 import Commands.Dev.Highlight.Options
 import Commands.Dev.ImportTree.Options
+import Commands.Dev.InstanceTermination.Options
 import Commands.Dev.Internal.Options
 import Commands.Dev.Latex.Options
 import Commands.Dev.MigrateJuvixYaml.Options
@@ -49,6 +50,7 @@ data DevCommand
   | Parse ParseOptions
   | Scope ScopeOptions
   | Termination TerminationCommand
+  | InstanceTermination InstanceTerminationCommand
   | JuvixDevRepl ReplOptions
   | MigrateJuvixYaml MigrateJuvixYamlOptions
   | Nockma NockmaCommand
@@ -72,6 +74,7 @@ parseDevCommand =
           commandScope,
           commandShowRoot,
           commandTermination,
+          commandInstanceTermination,
           commandJuvixDevRepl,
           commandMigrateJuvixYaml,
           commandLatex,
@@ -177,6 +180,13 @@ commandShowRoot =
       (DisplayRoot <$> parseRoot)
       (progDesc "Show the root path for a Juvix project")
 
+commandInstanceTermination :: Mod CommandFields DevCommand
+commandInstanceTermination =
+  command "instance-termination" $
+    info
+      (InstanceTermination <$> parseInstanceTerminationCommand)
+      (progDesc "Subcommands related to instance termination checking")
+
 commandTermination :: Mod CommandFields DevCommand
 commandTermination =
   command "termination" $

app/Commands/Dev/Termination/CallGraph.hs

@@ -11,7 +11,7 @@ import Juvix.Compiler.Store.Extra qualified as Stored
 runCommand :: (Members AppEffects r) => CallGraphOptions -> Sem r ()
 runCommand CallGraphOptions {..} = do
   globalOpts <- askGlobalOptions
-  PipelineResult {..} <- runPipelineTermination _graphInputFile upToInternalTyped
+  PipelineResult {..} <- evalPipelineTermination _graphInputFile upToInternalTyped
   let mainModule = _pipelineResult ^. Internal.resultModule
       toAnsiText' :: forall a. (HasAnsiBackend a, HasTextBackend a) => a -> Text
       toAnsiText' = toAnsiText (not (globalOpts ^. globalNoColors))

app/Commands/Dev/Termination/Calls.hs

@@ -9,7 +9,7 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination qua
 runCommand :: (Members AppEffects r) => CallsOptions -> Sem r ()
 runCommand localOpts@CallsOptions {..} = do
   globalOpts <- askGlobalOptions
-  PipelineResult {..} <- runPipelineTermination _callsInputFile upToInternal
+  PipelineResult {..} <- evalPipelineTermination _callsInputFile upToInternal
   let callMap0 = fst (Termination.buildCallMap (_pipelineResult ^. Internal.resultModule))
       callMap = case _callsFunctionNameFilter of
         Nothing -> callMap0

src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs

@@ -25,19 +25,6 @@ updateInstanceTable tab ii@InstanceInfo {..} =
 lookupInstanceTable :: InstanceTable -> Name -> Maybe [InstanceInfo]
 lookupInstanceTable tab name = HashMap.lookup name (tab ^. instanceTableMap)
 
-paramToExpression :: InstanceParam -> Expression
-paramToExpression = \case
-  InstanceParamVar v ->
-    ExpressionIden (IdenVar v)
-  InstanceParamApp InstanceApp {..} ->
-    _instanceAppExpression
-  InstanceParamFun InstanceFun {..} ->
-    _instanceFunExpression
-  InstanceParamHole h ->
-    ExpressionHole h
-  InstanceParamMeta v ->
-    ExpressionIden (IdenVar v)
-
 paramFromExpression :: HashSet VarName -> Expression -> Maybe InstanceParam
 paramFromExpression metaVars e = case e of
   ExpressionIden (IdenInductive n) ->

src/Juvix/Compiler/Internal/Pretty/Base.hs

@@ -13,7 +13,6 @@ import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Pretty.Options
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New
 import Juvix.Compiler.Store.Internal.Data.InfoTable
-import Juvix.Compiler.Store.Internal.Data.InstanceInfo
 import Juvix.Data.CodeAnn
 import Juvix.Data.Keyword.All qualified as Kw
 import Juvix.Prelude
@@ -404,9 +403,6 @@ instance (PrettyCode a, PrettyCode b) => PrettyCode (Either a b) where
       r' <- ppCode r
       return ("Right" <+> r')
 
-instance PrettyCode InstanceInfo where
-  ppCode = ppCode . (^. instanceInfoIden)
-
 instance PrettyCode LocalVars where
   ppCode LocalVars {..} = ppCode (HashMap.toList _localTypes)
 

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

@@ -1,5 +1,7 @@
 module Juvix.Compiler.Internal.Translation.FromInternal
   ( typeCheckingNew,
+    typeCheckingNewOptions,
+    computeImportContext,
   )
 where
 
@@ -18,13 +20,32 @@ import Juvix.Compiler.Store.Scoped.Language qualified as Scoped
 import Juvix.Data.Effect.NameIdGen
 import Juvix.Prelude hiding (fromEither)
 
+computeImportContext :: InternalModuleTable -> ImportContext
+computeImportContext itab =
+  ImportContext
+    { _importContextTypesTable = computeTypesTable itab,
+      _importContextFunctionsTable = computeFunctionsTable itab,
+      _importContextInstances = computeInstanceTable itab,
+      _importContextCoercions = computeCoercionTable itab
+    }
+
 typeCheckingNew ::
   forall r.
   (Members '[HighlightBuilder, Reader EntryPoint, Error JuvixError, NameIdGen, Reader ModuleTable] r) =>
   Sem (Termination ': r) InternalResult ->
   Sem r InternalTypedResult
-typeCheckingNew a = do
-  (termin, (res, (bst, checkedModule))) <- runTermination iniTerminationState $ do
+typeCheckingNew =
+  runReader defaultTypeCheckingOptions
+    . typeCheckingNewOptions
+    . inject
+
+typeCheckingNewOptions ::
+  forall r.
+  (Members '[Reader TypeCheckingOptions, HighlightBuilder, Reader EntryPoint, Error JuvixError, NameIdGen, Reader ModuleTable] r) =>
+  Sem (Termination ': r) InternalResult ->
+  Sem r InternalTypedResult
+typeCheckingNewOptions a = do
+  (termin, (res, (callmaps, (bst, checkedModule)))) <- runTermination iniTerminationState $ do
     res :: InternalResult <- a
     itab :: InternalModuleTable <- getInternalModuleTable <$> ask
     stab :: ScopedModuleTable <- getScopedModuleTable <$> ask
@@ -34,14 +55,9 @@ typeCheckingNew a = do
         stable =
           Scoped.computeCombinedInfoTable stab
             <> res ^. Internal.resultScoper . resultScopedModule . scopedModuleInfoTable
-        importCtx =
-          ImportContext
-            { _importContextTypesTable = computeTypesTable itab,
-              _importContextFunctionsTable = computeFunctionsTable itab,
-              _importContextInstances = computeInstanceTable itab,
-              _importContextCoercions = computeCoercionTable itab
-            }
+        importCtx = computeImportContext itab
     fmap (res,)
+      . runOutputList
       . runReader table
       . runReader (stable ^. Scoped.infoBuiltins)
       . runResultBuilder importCtx
@@ -58,6 +74,7 @@ typeCheckingNew a = do
     InternalTypedResult
       { _resultInternal = res,
         _resultModule = checkedModule,
+        _resultInstanceCallMaps = InstanceCallMaps callmaps,
         _resultInternalModule = md,
         _resultTermination = termin,
         _resultIdenTypes = bst ^. resultBuilderStateCombinedTypesTable,