cli calls skeleton

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 :: InstanceTerminationCommand -> Sem r ()
+runCommand = \case
+  Calls opts -> Calls.runCommand opts

app/Commands/Dev/InstanceTermination/Calls.hs

@@ -0,0 +1,7 @@
+module Commands.Dev.InstanceTermination.Calls where
+
+import Commands.Base
+import Commands.Dev.InstanceTermination.Calls.Options
+
+runCommand :: CallsOptions -> Sem r ()
+runCommand CallsOptions {} = return ()

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 calls table of a .juvix file")

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/Pretty/Base.hs

@@ -13,6 +13,7 @@ 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
@@ -397,6 +398,9 @@ 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/Pretty/Options.hs

@@ -1,12 +1,25 @@
 module Juvix.Compiler.Internal.Pretty.Options where
 
 import Juvix.Prelude
+import Prelude qualified
 
 data ShowDecrArgs
   = OnlyArg
   | OnlyRel
   | ArgRel
-  deriving stock (Data)
+  deriving stock (Enum, Bounded, Data)
+
+instance Show ShowDecrArgs where
+  show = \case
+    OnlyArg -> "arg"
+    OnlyRel -> "rel"
+    ArgRel -> "both"
+
+showDecrArgsHelp :: (IsString str) => ShowDecrArgs -> str
+showDecrArgsHelp = \case
+  OnlyRel -> "Show only the size relation"
+  OnlyArg -> "Show only the argument"
+  ArgRel -> "Show both the argument and the size relation"
 
 defaultOptions :: Options
 defaultOptions =

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/Base.hs

@@ -44,6 +44,7 @@ data Call = Call
 newtype LexOrder = LexOrder (NonEmpty Int)
 
 data CallMapBuilder' expr :: Effect where
+  -- | The first argument is the name of the caller
   AddCall :: FunctionName -> FunCall' expr -> CallMapBuilder' expr m ()
 
 makeEffect ''CallMapBuilder'

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs

@@ -20,7 +20,8 @@ import Juvix.Compiler.Internal.Extra.InstanceInfo
 import Juvix.Compiler.Internal.Pretty
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (Termination)
--- import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.LexOrder
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference
@@ -403,12 +404,6 @@ getInstanceInfoHelper funName funTy = do
   let err = throw (ErrInvalidInstanceType (InvalidInstanceType funTy))
   maybe err return (mkInstanceInfo (TypedIden (IdenFunction funName) funTy))
 
--- | Does not normalize the type. TODO should we completely forbid type synonyms in instance declarations?
--- getInstanceInfoTermination ::
---   (Members '[Error TypeCheckerError] r) =>
---   FunctionDef ->
---   Sem r InstanceInfo
--- getInstanceInfoTermination FunctionDef {..} = getInstanceInfoHelper _funDefName _funDefType
 checkInstanceType ::
   forall r.
   (Members '[Error TypeCheckerError, Reader InfoTable, Inference, NameIdGen, ResultBuilder] r) =>
@@ -581,60 +576,65 @@ checkExpression expectedTy e = do
 
 checkResolveInstanceHoles ::
   forall r.
-  ( Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r
+  ( Members
+      '[ Reader InfoTable,
+         Reader BuiltinsTable,
+         ResultBuilder,
+         Error TypeCheckerError,
+         NameIdGen,
+         Inference,
+         Termination,
+         Reader InsertedArgsStack
+       ]
+      r
   ) =>
   Sem (Output TypedInstanceHole ': r) (NonEmpty MutualStatement) ->
   Sem r (NonEmpty MutualStatement)
 checkResolveInstanceHoles s = do
   (holes, stmts :: NonEmpty MutualStatement) <- runOutputList s
-  -- infos <- mapM getInstanceInfo (stmts ^.. each . _StatementFunction . filtered isInstance)
-  -- checkInstanceTermination infos
+  infos <- mapM getInstanceInfo (stmts ^.. each . _StatementFunction . filtered isInstance)
+  checkInstanceTermination infos
   resolveInstanceHoles holes stmts
   where
-
--- isInstance :: FunctionDef -> Bool
--- isInstance f = case f ^. funDefIsInstanceCoercion of
---   Nothing -> False
---   Just k -> case k of
---     IsInstanceCoercionInstance -> True
---     IsInstanceCoercionCoercion -> False
+    isInstance :: FunctionDef -> Bool
+    isInstance f = case f ^. funDefIsInstanceCoercion of
+      Nothing -> False
+      Just k -> case k of
+        IsInstanceCoercionInstance -> True
+        IsInstanceCoercionCoercion -> False
 
 -- {Show a} : Show (List a)
--- checkInstanceTermination ::
---   ( Members
---       '[ Reader InfoTable,
---          Error TypeCheckerError
---        ]
---       r
---   ) =>
---   [InstanceInfo] ->
---   Sem r ()
--- checkInstanceTermination instances = do
---   -- TODO remove later calls to checkInstanceConstraints
---   x :: [(InstanceInfo, [InstanceApp])] <- mapWithM checkInstanceConstraints instances
---   undefined
---   where
---     cmpInstanceParam :: InstanceParam -> InstanceParam -> SizeRel'
---     cmpInstanceParam = undefined
-
---     instanceCallMap :: [(InstanceInfo, [InstanceApp])] -> CallMap' InstanceParam
---     instanceCallMap l = run . execCallMapBuilder . forM l $ \(ii, calls) ->
---       forM calls $ \(call :: InstanceApp) -> do
---         let arsg :: [FunCallArg' InstanceParam] =
---               [ FunCallArg
---                   { _argExpression = x
---                   }
---                 | x :: InstanceParam <- call ^. instanceAppArgs
---               ]
---         let r :: CallRow =
---               CallRow
---                 {
---                 }
---         let c :: FunCall' InstanceParam =
---               FunCall
---                 {
---                 }
---         undefined
+checkInstanceTermination ::
+  ( Members
+      '[ Reader InfoTable,
+         Error TypeCheckerError
+       ]
+      r
+  ) =>
+  [InstanceInfo] ->
+  Sem r ()
+checkInstanceTermination instances = do
+  -- TODO remove later calls to checkInstanceConstraints
+  cm :: CallMap' InstanceParam <- mkInstanceCallMap <$> mapWithM checkInstanceConstraints instances
+  forM_ (mapWith findOrder (callMapRecursiveBehaviour cm)) $ \(recBehav, morder) -> case morder of
+    Just {} -> return ()
+    Nothing ->
+      throw $
+        ErrTraitNotTerminatingNew
+          TraitNotTerminatingNew
+            { _traitNotTerminatingNew = nonEmpty' [i | i <- instances, i ^. instanceInfoInductive == recBehav ^. recursiveBehaviourFun]
+            }
+  where
+    mkInstanceCallMap :: [(InstanceInfo, [InstanceApp])] -> CallMap' InstanceParam
+    mkInstanceCallMap l = run (execCallMapBuilder (forM l (uncurry addInstance)))
+      where
+        addInstance :: (Members '[CallMapBuilder' InstanceParam] r) => InstanceInfo -> [InstanceApp] -> Sem r ()
+        addInstance i = mapM_ (addConstraint i)
+
+        addConstraint :: (Members '[CallMapBuilder' InstanceParam] r) => InstanceInfo -> InstanceApp -> Sem r ()
+        addConstraint InstanceInfo {..} InstanceApp {..} = do
+          let c :: FunCall' InstanceParam = mkFunCall cmpInstanceParam _instanceAppHead _instanceInfoParams _instanceAppArgs
+          addCall _instanceInfoInductive c
 
 resolveInstanceHoles ::
   forall a r.
@@ -1002,16 +1002,14 @@ checkPattern = go
                       _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
                     }
             )
-          when
-            (numArgs > numParams)
-            ( throw $
-                ErrTooManyArgumentsIndType
-                  WrongNumberArgumentsIndType
-                    { _wrongNumberArgumentsIndTypeActualType = ty,
-                      _wrongNumberArgumentsIndTypeActualNumArgs = numArgs,
-                      _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
-                    }
-            )
+          when (numArgs > numParams)
+            . throw
+            $ ErrTooManyArgumentsIndType
+              WrongNumberArgumentsIndType
+                { _wrongNumberArgumentsIndTypeActualType = ty,
+                  _wrongNumberArgumentsIndTypeActualNumArgs = numArgs,
+                  _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
+                }
           return (Right (ind, zipExact params args))
 
 inferExpression' ::

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs

@@ -36,6 +36,7 @@ data TypeCheckerError
   | ErrSubsumedInstance SubsumedInstance
   | ErrExplicitInstanceArgument ExplicitInstanceArgument
   | ErrTraitNotTerminating TraitNotTerminating
+  | ErrTraitNotTerminatingNew TraitNotTerminatingNew
   | ErrBuiltinNotDefined BuiltinNotDefined
   | ErrArityCheckerError ArityCheckerError
   | ErrDefaultArgLoop DefaultArgLoop
@@ -65,6 +66,7 @@ instance ToGenericError TypeCheckerError where
     ErrSubsumedInstance e -> genericError e
     ErrExplicitInstanceArgument e -> genericError e
     ErrTraitNotTerminating e -> genericError e
+    ErrTraitNotTerminatingNew e -> genericError e
     ErrBuiltinNotDefined e -> genericError e
     ErrArityCheckerError e -> genericError e
     ErrDefaultArgLoop e -> genericError e
@@ -93,6 +95,7 @@ instance Show TypeCheckerError where
     ErrSubsumedInstance {} -> "ErrSubsumedInstance"
     ErrExplicitInstanceArgument {} -> "ErrExplicitInstanceArgument"
     ErrTraitNotTerminating {} -> "ErrTraitNotTerminating"
+    ErrTraitNotTerminatingNew {} -> "ErrTraitNotTerminatingNew"
     ErrArityCheckerError {} -> "ErrArityCheckerError"
     ErrDefaultArgLoop {} -> "ErrDefaultArgLoop"
     ErrBuiltinNotDefined {} -> "ErrBuiltinNotDefined"

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs

@@ -586,6 +586,31 @@ instance ToGenericError ExplicitInstanceArgument where
         where
           i = getLoc (e ^. explicitInstanceArgumentParameter)
 
+newtype TraitNotTerminatingNew = TraitNotTerminatingNew
+  { _traitNotTerminatingNew :: NonEmpty InstanceInfo
+  }
+
+makeLenses ''TraitNotTerminatingNew
+
+instance ToGenericError TraitNotTerminatingNew where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = i,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = [i]
+            }
+        where
+          opts' = fromGenericOptions opts
+          i = getLoc (head (e ^. traitNotTerminatingNew))
+          msg :: Doc CodeAnn =
+            "Unable to prove instance-termination."
+              <+> "Make sure that the constraints are decreasing on the following instances:"
+                <> line
+                <> itemize (ppCode opts' <$> (e ^. traitNotTerminatingNew))
+
 newtype TraitNotTerminating = TraitNotTerminating
   { _traitNotTerminating :: Expression
   }

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs

@@ -1,9 +1,11 @@
 module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Traits.Termination
   ( checkTraitTermination,
+    cmpInstanceParam,
   )
 where
 
 import Juvix.Compiler.Internal.Extra.InstanceInfo
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.SizeRelation
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
 import Juvix.Prelude
 
@@ -33,3 +35,9 @@ checkStrictSubterm p1 p2 = case p2 of
 
 checkSubterm :: InstanceParam -> InstanceParam -> Bool
 checkSubterm p1 p2 = p1 == p2 || checkStrictSubterm p1 p2
+
+cmpInstanceParam :: InstanceParam -> InstanceParam -> Maybe SizeRel'
+cmpInstanceParam l r
+  | checkStrictSubterm l r = Just RLe
+  | l == r = Just REq
+  | otherwise = Nothing