Improve instance termination checking

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

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

app/Commands/Dev/InstanceTermination/Calls.hs

@@ -0,0 +1,23 @@
+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 :: (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/Calls/Options.hs

@@ -0,0 +1,36 @@
+module Commands.Dev.InstanceTermination.Calls.Options where
+
+import CommonOptions
+import GlobalOptions
+import Juvix.Compiler.Internal.Pretty.Options qualified as Internal
+
+data CallsOptions = CallsOptions
+  { _callsShowDecreasingArgs :: Internal.ShowDecrArgs,
+    _callsInputFile :: AppPath File
+  }
+  deriving stock (Data)
+
+makeLenses ''CallsOptions
+
+parseCalls :: Parser CallsOptions
+parseCalls = do
+  _callsShowDecreasingArgs <-
+    option
+      decrArgsParser
+      ( long "show-decreasing-args"
+          <> short 'd'
+          <> value Internal.ArgRel
+          <> helpDoc (enumHelp Internal.showDecrArgsHelp)
+      )
+  _callsInputFile <- parseInputFile FileExtJuvix
+  pure CallsOptions {..}
+  where
+    decrArgsParser :: ReadM Internal.ShowDecrArgs
+    decrArgsParser = enumReader Proxy
+
+instance CanonicalProjection (GlobalOptions, CallsOptions) Internal.Options where
+  project (GlobalOptions {..}, CallsOptions {..}) =
+    Internal.defaultOptions
+      { Internal._optShowNameIds = _globalShowNameIds,
+        Internal._optShowDecreasingArgs = _callsShowDecreasingArgs
+      }

app/Commands/Dev/InstanceTermination/Options.hs

@@ -0,0 +1,29 @@
+module Commands.Dev.InstanceTermination.Options
+  ( module Commands.Dev.InstanceTermination.Options,
+    module Commands.Dev.InstanceTermination.Calls.Options,
+  )
+where
+
+import Commands.Dev.InstanceTermination.Calls.Options
+import Juvix.Prelude
+import Options.Applicative
+
+newtype InstanceTerminationCommand
+  = Calls CallsOptions
+  deriving stock (Data)
+
+parseInstanceTerminationCommand :: Parser InstanceTerminationCommand
+parseInstanceTerminationCommand =
+  hsubparser $
+    mconcat
+      [ commandCalls
+      ]
+  where
+    commandCalls :: Mod CommandFields InstanceTerminationCommand
+    commandCalls = command "calls" minfo
+      where
+        minfo :: ParserInfo InstanceTerminationCommand
+        minfo =
+          info
+            (Calls <$> parseCalls)
+            (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))
@@ -20,7 +20,7 @@ runCommand CallGraphOptions {..} = do
           <> _pipelineResult
             ^. Internal.resultInternalModule
               . Internal.internalModuleInfoTable
-      callMap = Termination.buildCallMap mainModule
+      callMap = fst (Termination.buildCallMap mainModule)
       completeGraph = Termination.completeCallGraph callMap
       filteredGraph =
         maybe

app/Commands/Dev/Termination/Calls.hs

@@ -9,8 +9,8 @@ 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
-  let callMap0 = Termination.buildCallMap (_pipelineResult ^. Internal.resultModule)
+  PipelineResult {..} <- evalPipelineTermination _callsInputFile upToInternal
+  let callMap0 = fst (Termination.buildCallMap (_pipelineResult ^. Internal.resultModule))
       callMap = case _callsFunctionNameFilter of
         Nothing -> callMap0
         Just f -> Termination.filterCallMap f callMap0

app/Commands/Dev/Termination/Calls/Options.hs

@@ -28,22 +28,14 @@ parseCalls = do
           )
   _callsShowDecreasingArgs <-
     option
-      decrArgsParser
+      (enumReader Proxy)
       ( long "show-decreasing-args"
           <> short 'd'
           <> value Internal.ArgRel
-          <> help "possible values: argument, relation, both"
+          <> helpDoc (enumHelp Internal.showDecrArgsHelp)
       )
   _callsInputFile <- optional (parseInputFile FileExtJuvix)
   pure CallsOptions {..}
-  where
-    decrArgsParser :: ReadM Internal.ShowDecrArgs
-    decrArgsParser = eitherReader $ \s ->
-      case map toLower s of
-        "argument" -> return Internal.OnlyArg
-        "relation" -> return Internal.OnlyRel
-        "both" -> return Internal.ArgRel
-        _ -> Left "bad argument"
 
 instance CanonicalProjection (GlobalOptions, CallsOptions) Internal.Options where
   project (GlobalOptions {..}, CallsOptions {..}) =

src/Juvix/Compiler/Internal/Data.hs

@@ -1,7 +1,7 @@
 module Juvix.Compiler.Internal.Data
   ( module Juvix.Compiler.Internal.Data.InfoTable,
     module Juvix.Compiler.Internal.Data.LocalVars,
-    module Juvix.Compiler.Internal.Data.TypedHole,
+    module Juvix.Compiler.Internal.Data.TypedInstanceHole,
     module Juvix.Compiler.Internal.Data.Name,
     module Juvix.Compiler.Internal.Data.NameDependencyInfo,
   )
@@ -11,4 +11,4 @@ import Juvix.Compiler.Internal.Data.InfoTable
 import Juvix.Compiler.Internal.Data.LocalVars
 import Juvix.Compiler.Internal.Data.Name
 import Juvix.Compiler.Internal.Data.NameDependencyInfo
-import Juvix.Compiler.Internal.Data.TypedHole
+import Juvix.Compiler.Internal.Data.TypedInstanceHole

src/Juvix/Compiler/Internal/Data/Cast.hs

@@ -3,7 +3,9 @@ module Juvix.Compiler.Internal.Data.Cast where
 import Juvix.Compiler.Internal.Language
 import Juvix.Prelude
 
-data CastType = CastInt | CastNat
+data CastType
+  = CastInt
+  | CastNat
 
 data CastHole = CastHole
   { _castHoleHole :: Hole,

src/Juvix/Compiler/Internal/Data/TypedHole.hs → src/Juvix/Compiler/Internal/Data/TypedInstanceHole.hs

@@ -1,13 +1,13 @@
-module Juvix.Compiler.Internal.Data.TypedHole where
+module Juvix.Compiler.Internal.Data.TypedInstanceHole where
 
 import Juvix.Compiler.Internal.Data.LocalVars
 import Juvix.Compiler.Internal.Language
 import Juvix.Prelude
 
-data TypedHole = TypedHole
+data TypedInstanceHole = TypedInstanceHole
   { _typedHoleHole :: InstanceHole,
     _typedHoleType :: Expression,
     _typedHoleLocalVars :: LocalVars
   }
 
-makeLenses ''TypedHole
+makeLenses ''TypedInstanceHole

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

@@ -2,6 +2,7 @@
 
 module Juvix.Compiler.Internal.Extra.Base where
 
+import Control.Lens.Combinators (cosmos)
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Internal.Data.LocalVars
@@ -54,6 +55,13 @@ instance Plated Expression where
     ExpressionHole {} -> pure e
     ExpressionInstanceHole {} -> pure e
 
+subExpressions :: Expression -> [Expression]
+subExpressions e = e ^.. subCosmos
+
+-- | Fold over all transitive descendants, excluding self
+subCosmos :: (Plated a) => Fold a a
+subCosmos = dropping 1 cosmos
+
 class HasExpressions a where
   -- | Traverses itself if `a` is an Expression. Otherwise traverses children `Expression`s (not transitive).
   directExpressions :: Traversal' a Expression
@@ -340,17 +348,6 @@ subsKind uids k =
     [ (s, toExpression s') | s <- uids, let s' = toExpression (set nameKind k s)
     ]
 
-data Expr
-  = Val Int
-  | Neg Expr
-  | Add Expr Expr
-  deriving stock (Eq, Ord, Show, Data)
-
-instance Plated Expr where
-  plate f (Neg e) = Neg <$> f e
-  plate f (Add a b) = Add <$> f a <*> f b
-  plate _ a = pure a
-
 -- | A Fold over all subexressions, including self
 allExpressions :: (HasExpressions expr) => Fold expr Expression
 allExpressions = cosmosOn directExpressions

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) ->
@@ -101,19 +88,18 @@ traitFromExpression metaVars e = case paramFromExpression metaVars e of
   Just (InstanceParamApp app) -> Just app
   _ -> Nothing
 
-instanceFromTypedIden :: TypedIden -> Maybe InstanceInfo
-instanceFromTypedIden TypedIden {..} = do
-  InstanceApp {..} <- traitFromExpression metaVars e
+mkInstanceInfo :: TypedIden -> Maybe InstanceInfo
+mkInstanceInfo TypedIden {..} = do
+  let (args, ret) = unfoldFunType _typedIdenType
+      metaVars = hashSet (mapMaybe (^. paramName) args)
+  InstanceApp {..} <- traitFromExpression metaVars ret
   return $
     InstanceInfo
       { _instanceInfoInductive = _instanceAppHead,
         _instanceInfoParams = _instanceAppArgs,
-        _instanceInfoResult = _typedIden,
+        _instanceInfoIden = _typedIden,
         _instanceInfoArgs = args
       }
-  where
-    (args, e) = unfoldFunType _typedIdenType
-    metaVars = HashSet.fromList $ mapMaybe (^. paramName) args
 
 checkNoMeta :: InstanceParam -> Bool
 checkNoMeta = \case

src/Juvix/Compiler/Internal/Language.hs

@@ -484,6 +484,8 @@ data NormalizedExpression = NormalizedExpression
   }
 
 makePrisms ''Expression
+makePrisms ''MutualStatement
+
 makeLenses ''SideIfBranch
 makeLenses ''SideIfs
 makeLenses ''CaseBranchRhs
@@ -582,7 +584,7 @@ instance HasAtomicity Pattern where
     PatternWildcardConstructor {} -> Atom
 
 instance HasLoc Module where
-  getLoc m = getLoc (m ^. moduleName) <>? maybe Nothing (Just . getLocSpan) (nonEmpty (m ^. moduleBody . moduleStatements))
+  getLoc m = getLoc (m ^. moduleName) <>? fmap getLocSpan (nonEmpty (m ^. moduleBody . moduleStatements))
 
 instance HasLoc MutualBlock where
   getLoc = getLocSpan . (^. mutualStatements)