mirror of
https://github.com/anoma/juvix.git
synced 2024-12-12 14:28:08 +03:00
34719bbc4d
- Closes #2293. - Closes #2319 I've added an effect for termination. It keeps track of which functions failed the termination checker, which is run just after translating to Internal. During typechecking, non-terminating functions are not normalized. After typechecking, if there is at least one function which failed the termination checker, an error is reported. Additionally, we now properly check for termination of functions defined in a let expression in the repl.
13 lines
597 B
Haskell
13 lines
597 B
Haskell
module Commands.Dev.Internal.Arity where
|
|
|
|
import Commands.Base
|
|
import Commands.Dev.Internal.Arity.Options
|
|
import Juvix.Compiler.Internal.Pretty qualified as Internal
|
|
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as InternalArity
|
|
|
|
runCommand :: (Members '[Embed IO, App] r) => InternalArityOptions -> Sem r ()
|
|
runCommand opts = do
|
|
globalOpts <- askGlobalOptions
|
|
micro <- head . (^. InternalArity.resultModules) <$> runPipelineTermination (opts ^. internalArityInputFile) upToInternalArity
|
|
renderStdOut (Internal.ppOut globalOpts micro)
|