From 4c7e8a74a02b1a838b9672e5b5511b27d5d5fe6b Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 5 Sep 2024 10:56:52 +0200 Subject: [PATCH] cli and TypeCheckingMode --- app/App.hs | 11 +- app/Commands/Dev.hs | 2 + app/Commands/Dev/InstanceTermination.hs | 2 +- app/Commands/Dev/InstanceTermination/Calls.hs | 20 ++- .../Dev/InstanceTermination/Options.hs | 2 +- app/Commands/Dev/Internal/Pretty.hs | 2 +- app/Commands/Dev/Options.hs | 10 ++ app/Commands/Dev/Termination/CallGraph.hs | 2 +- app/Commands/Dev/Termination/Calls.hs | 2 +- .../Compiler/Internal/Extra/InstanceInfo.hs | 13 -- src/Juvix/Compiler/Internal/Pretty/Base.hs | 4 - .../Internal/Translation/FromInternal.hs | 35 +++-- .../Analysis/TypeChecking/CheckerNew.hs | 134 +++++++++++------- .../TypeChecking/CheckerNew/Options.hs | 26 ++++ .../Analysis/TypeChecking/Data/Context.hs | 16 +++ .../Analysis/TypeChecking/Data/Inference.hs | 13 +- .../TypeChecking/Data/ResultBuilder.hs | 3 + .../TypeChecking/Traits/Termination.hs | 10 +- .../Compiler/Internal/Translation/Repl.hs | 3 +- src/Juvix/Compiler/Pipeline.hs | 6 + src/Juvix/Compiler/Pipeline/Result.hs | 3 + .../Store/Internal/Data/InstanceInfo.hs | 34 +++++ src/Juvix/Data/Hole.hs | 4 + 23 files changed, 258 insertions(+), 99 deletions(-) create mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Options.hs diff --git a/app/App.hs b/app/App.hs index 0f61308be5..0b37b13020 100644 --- a/app/App.hs +++ b/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) -> diff --git a/app/Commands/Dev.hs b/app/Commands/Dev.hs index c9910635c0..55a5f05925 100644 --- a/app/Commands/Dev.hs +++ b/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 diff --git a/app/Commands/Dev/InstanceTermination.hs b/app/Commands/Dev/InstanceTermination.hs index bc82594d61..15d3ee9ac7 100644 --- a/app/Commands/Dev/InstanceTermination.hs +++ b/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 diff --git a/app/Commands/Dev/InstanceTermination/Calls.hs b/app/Commands/Dev/InstanceTermination/Calls.hs index 16117d88c0..824c88224e 100644 --- a/app/Commands/Dev/InstanceTermination/Calls.hs +++ b/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 diff --git a/app/Commands/Dev/InstanceTermination/Options.hs b/app/Commands/Dev/InstanceTermination/Options.hs index f2adbd6996..c1b7eab7d6 100644 --- a/app/Commands/Dev/InstanceTermination/Options.hs +++ b/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") diff --git a/app/Commands/Dev/Internal/Pretty.hs b/app/Commands/Dev/Internal/Pretty.hs index b8c1c3f962..9737eaa06b 100644 --- a/app/Commands/Dev/Internal/Pretty.hs +++ b/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) diff --git a/app/Commands/Dev/Options.hs b/app/Commands/Dev/Options.hs index f68a579789..9b849c514d 100644 --- a/app/Commands/Dev/Options.hs +++ b/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" $ diff --git a/app/Commands/Dev/Termination/CallGraph.hs b/app/Commands/Dev/Termination/CallGraph.hs index aba5641d5d..1d518a9abc 100644 --- a/app/Commands/Dev/Termination/CallGraph.hs +++ b/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)) diff --git a/app/Commands/Dev/Termination/Calls.hs b/app/Commands/Dev/Termination/Calls.hs index 521e8d524c..2b3b32ad99 100644 --- a/app/Commands/Dev/Termination/Calls.hs +++ b/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 diff --git a/src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs b/src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs index 899354d61e..4363456e31 100644 --- a/src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs +++ b/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) -> diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index ff89ed70b4..915fcc069b 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/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) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs index f1e8d9d1b1..aea1f9a901 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs +++ b/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, diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index 72d267cdb2..d4d0a0c66e 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -1,8 +1,10 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error, + module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Options, checkTopModule, withEmptyInsertedArgsStack, inferExpression, + mutualBlockInstanceCallMap, ) where @@ -23,6 +25,7 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Che 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.CheckerNew.Options import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder @@ -140,7 +143,7 @@ checkCoercionCycles = do . CoercionCycles checkTopModule :: - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader TypeCheckingOptions, Output InstanceCallMap] r) => Module -> Sem r Module checkTopModule md = do @@ -148,7 +151,7 @@ checkTopModule md = do checkModule md checkModule :: - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader TypeCheckingOptions, Output InstanceCallMap] r) => Module -> Sem r Module checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do @@ -165,7 +168,7 @@ checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do } checkModuleBody :: - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack, Reader TypeCheckingOptions, Output InstanceCallMap] r) => ModuleBody -> Sem r ModuleBody checkModuleBody ModuleBody {..} = do @@ -181,17 +184,17 @@ checkImport :: Import -> Sem r Import checkImport = return checkMutualBlock :: - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack, Reader TypeCheckingOptions, Output InstanceCallMap] r) => MutualBlock -> Sem r MutualBlock checkMutualBlock s = runReader emptyLocalVars (checkTopMutualBlock s) checkInductiveDef :: forall r. - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, State NegativeTypeParameters, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => + (Members '[Reader TypeCheckingOptions, HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, State NegativeTypeParameters, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => InductiveDef -> Sem r InductiveDef -checkInductiveDef InductiveDef {..} = runInferenceDef $ do +checkInductiveDef InductiveDef {..} = runInferenceDefs $ do params <- checkParams withLocalTypes params $ do constrs' <- mapM goConstructor _inductiveConstructors @@ -250,7 +253,7 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do ) checkTopMutualBlock :: - (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack, Reader TypeCheckingOptions, Output InstanceCallMap] r) => MutualBlock -> Sem r MutualBlock checkTopMutualBlock (MutualBlock ds) = @@ -290,6 +293,7 @@ checkMutualStatement :: ( Members '[ HighlightBuilder, Reader BuiltinsTable, + Reader TypeCheckingOptions, State NegativeTypeParameters, Reader EntryPoint, Inference, @@ -331,7 +335,7 @@ unfoldFunType' e = do checkFunctionDef :: forall r. - (Members '[Reader LocalVars, Reader BuiltinsTable, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader LocalVars, Reader BuiltinsTable, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => FunctionDef -> Sem r FunctionDef checkFunctionDef FunctionDef {..} = do @@ -379,7 +383,7 @@ checkFunctionDef FunctionDef {..} = do withLocalTypeMaybe (p ^. paramName) (p ^. paramType) (go rest) checkIsType :: - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> Expression -> Sem r Expression @@ -387,7 +391,7 @@ checkIsType = checkExpression . smallUniverseE checkDefType :: forall r. - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Sem r Expression checkDefType ty = checkIsType loc ty @@ -406,7 +410,7 @@ getInstanceInfoHelper funName funTy = do checkInstanceType :: forall r. - (Members '[Error TypeCheckerError, Reader InfoTable, Inference, NameIdGen, ResultBuilder] r) => + (Members '[Reader TypeCheckingOptions, Error TypeCheckerError, Reader InfoTable, Inference, NameIdGen, ResultBuilder] r) => FunctionDef -> Sem r () checkInstanceType def@FunctionDef {..} = do @@ -423,7 +427,7 @@ checkInstanceType def@FunctionDef {..} = do checkInstanceConstraints :: forall r. - (Members '[Reader InfoTable, Error TypeCheckerError] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Error TypeCheckerError] r) => InstanceInfo -> Sem r [InstanceApp] checkInstanceConstraints ii = mapMaybeM checkInstanceConstraint (ii ^. instanceInfoArgs) @@ -487,7 +491,7 @@ checkCoercionType FunctionDef {..} = do checkCaseBranchRhs :: forall r. - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> CaseBranchRhs -> Sem r CaseBranchRhs @@ -508,6 +512,7 @@ checkSideIfs :: Termination, Reader BuiltinsTable, Output CastHole, + Reader TypeCheckingOptions, Reader InsertedArgsStack ] r @@ -526,7 +531,7 @@ checkSideIfs expectedTy SideIfs {..} = do checkSideIfBranch :: forall r. - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> SideIfBranch -> Sem r SideIfBranch @@ -545,7 +550,7 @@ getBoolType loc = toExpression <$> getBuiltinNameTypeChecker loc BuiltinBool checkExpression :: forall r. - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Expression -> Sem r Expression @@ -578,12 +583,14 @@ checkResolveInstanceHoles :: forall r. ( Members '[ Reader InfoTable, + Reader TypeCheckingOptions, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, + Output InstanceCallMap, Reader InsertedArgsStack ] r @@ -592,9 +599,26 @@ checkResolveInstanceHoles :: Sem r (NonEmpty MutualStatement) checkResolveInstanceHoles s = do (holes, stmts :: NonEmpty MutualStatement) <- runOutputList s - infos <- mapM getInstanceInfo (stmts ^.. each . _StatementFunction . filtered isInstance) - checkInstanceTermination infos - resolveInstanceHoles holes stmts + checkInstanceTermination (MutualBlock stmts) + mode <- asks (^. typeCheckingMode) + case mode of + TypeCheckingBuildCallMap -> return stmts + TypeCheckingNormal -> resolveInstanceHoles holes stmts + +mutualBlockInstanceCallMap :: + ( Members + '[ Reader InfoTable, + Error TypeCheckerError, + Reader TypeCheckingOptions, + Inference + ] + r + ) => + MutualBlock -> + Sem r ([InstanceInfo], CallMap' InstanceParam) +mutualBlockInstanceCallMap stmts = do + instances <- mapM getInstanceInfo (stmts ^.. mutualStatements . each . _StatementFunction . filtered isInstance) + (instances,) . mkInstanceCallMap <$> mapWithM checkInstanceConstraints instances where isInstance :: FunctionDef -> Bool isInstance f = case f ^. funDefIsInstanceCoercion of @@ -603,28 +627,6 @@ checkResolveInstanceHoles s = do 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 - 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 @@ -636,10 +638,42 @@ checkInstanceTermination instances = do let c :: FunCall' InstanceParam = mkFunCall cmpInstanceParam _instanceAppHead _instanceInfoParams _instanceAppArgs addCall _instanceInfoInductive c +checkInstanceTermination :: + ( Members + '[ Reader InfoTable, + Error TypeCheckerError, + Output InstanceCallMap, + Reader TypeCheckingOptions, + Inference + ] + r + ) => + MutualBlock -> + Sem r () +checkInstanceTermination stmts = do + -- TODO remove later calls to checkInstanceConstraints + (instances, cm :: CallMap' InstanceParam) <- mutualBlockInstanceCallMap stmts + output + ( InstanceCallMap + { _instanceCallMap = cm, + _instanceCallMapBlock = stmts + } + ) + forM_ (mapWith findOrder (callMapRecursiveBehaviour cm)) $ \(recBehav, morder) -> case morder of + Just {} -> return () + Nothing -> do + mode <- asks (^. typeCheckingMode) + unless (mode == TypeCheckingBuildCallMap) $ + throw $ + ErrTraitNotTerminatingNew + TraitNotTerminatingNew + { _traitNotTerminatingNew = nonEmpty' [i | i <- instances, i ^. instanceInfoInductive == recBehav ^. recursiveBehaviourFun] + } + resolveInstanceHoles :: forall a r. ( HasExpressions a, - Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r + Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r ) => [TypedInstanceHole] -> a -> @@ -660,7 +694,7 @@ resolveInstanceHoles hs e = do runResolveInstanceHoles :: forall a r. ( HasExpressions a, - Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r + Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r ) => Sem (Output TypedInstanceHole ': r) a -> Sem r a @@ -669,7 +703,7 @@ runResolveInstanceHoles s = do resolveInstanceHoles hs e checkFunctionParameter :: - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => FunctionParameter -> Sem r FunctionParameter checkFunctionParameter FunctionParameter {..} = do @@ -686,7 +720,7 @@ checkFunctionParameter FunctionParameter {..} = do } inferExpression :: - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Reader InsertedArgsStack] r) => -- | type hint Maybe Expression -> Expression -> @@ -701,7 +735,7 @@ lookupVar v = do err = error $ "internal error: could not find var " <> ppTrace v <> " at " <> ppTrace (getLoc v) checkFunctionBody :: - (Members '[Reader LocalVars, Reader BuiltinsTable, Reader InfoTable, NameIdGen, Error TypeCheckerError, Output TypedInstanceHole, ResultBuilder, Inference, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader LocalVars, Reader BuiltinsTable, Reader InfoTable, NameIdGen, Error TypeCheckerError, Output TypedInstanceHole, ResultBuilder, Inference, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Expression -> Sem r Expression @@ -726,7 +760,7 @@ checkFunctionBody expectedTy body = checkClauseExpression :: forall r. - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> -- | Type Expression -> @@ -744,7 +778,7 @@ checkClauseExpression clauseLoc clauseType clausePats body = do -- | helper function for lambda functions and case branches checkClause :: forall r. - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedInstanceHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> -- | Type Expression -> @@ -1014,7 +1048,7 @@ checkPattern = go inferExpression' :: forall r. - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression @@ -1023,7 +1057,7 @@ inferExpression' = holesHelper -- | Checks anything but an Application. Does not insert holes inferLeftAppExpression :: forall r. - (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression @@ -1255,7 +1289,7 @@ inferLeftAppExpression mhint e = case e of return (TypedExpression kind (ExpressionIden i)) -- | The hint is used for trailing holes only -holesHelper :: forall r. (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression +holesHelper :: forall r. (Members '[Reader TypeCheckingOptions, Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedInstanceHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression holesHelper mhint expr = do let (f, args) = unfoldExpressionApp expr hint diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Options.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Options.hs new file mode 100644 index 0000000000..f6db6e45ed --- /dev/null +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Options.hs @@ -0,0 +1,26 @@ +module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Options where + +import Juvix.Prelude hiding (fromEither) + +data TypeCheckingMode + = -- | The default mode with the normal behavious + TypeCheckingNormal + | -- | Used in `juvix dev instance-termination calls`. + -- + -- 1. Does not attempt to resolve instane holes. + -- + -- 2. Does not throw an error if instance-termination cannot be proved + TypeCheckingBuildCallMap + deriving stock (Eq, Show) + +newtype TypeCheckingOptions = TypeCheckingOptions + { _typeCheckingMode :: TypeCheckingMode + } + +defaultTypeCheckingOptions :: TypeCheckingOptions +defaultTypeCheckingOptions = + TypeCheckingOptions + { _typeCheckingMode = TypeCheckingNormal + } + +makeLenses ''TypeCheckingOptions diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs index 51a491592e..395772a6ab 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs @@ -3,6 +3,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Da module Juvix.Compiler.Store.Internal.Data.FunctionsTable, module Juvix.Compiler.Store.Internal.Data.TypesTable, module Juvix.Compiler.Internal.Data.InfoTable, + module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.Base, ) where @@ -10,6 +11,7 @@ import Juvix.Compiler.Internal.Data.InfoTable import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (TerminationState) +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.Base import Juvix.Compiler.Store.Internal.Data.CoercionInfo import Juvix.Compiler.Store.Internal.Data.FunctionsTable import Juvix.Compiler.Store.Internal.Data.InstanceInfo @@ -21,12 +23,24 @@ data InternalTypedResult = InternalTypedResult _resultModule :: Module, _resultInternalModule :: InternalModule, _resultTermination :: TerminationState, + -- | Used only in `juvix dev instance-termination calls` + _resultInstanceCallMaps :: InstanceCallMaps, _resultIdenTypes :: TypesTable, _resultFunctions :: FunctionsTable, _resultInstances :: InstanceTable, _resultCoercions :: CoercionTable } +data InstanceCallMap = InstanceCallMap + { _instanceCallMapBlock :: MutualBlock, + _instanceCallMap :: CallMap' InstanceParam + } + +newtype InstanceCallMaps = InstanceCallMaps + { _instanceCallMaps :: [InstanceCallMap] + } + deriving newtype (Semigroup, Monoid) + data ImportContext = ImportContext { _importContextTypesTable :: TypesTable, _importContextFunctionsTable :: FunctionsTable, @@ -36,6 +50,8 @@ data ImportContext = ImportContext makeLenses ''InternalTypedResult makeLenses ''ImportContext +makeLenses ''InstanceCallMaps +makeLenses ''InstanceCallMap getInternalTypedResultComments :: InternalTypedResult -> Comments getInternalTypedResultComments = Internal.getInternalResultComments . (^. resultInternal) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs index 070063751b..c5f8c33ca3 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs @@ -13,7 +13,6 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Da strongNormalize, weakNormalize, runInferenceDefs, - runInferenceDef, rememberFunctionDef, matchTypes, queryMetavarFinal, @@ -513,8 +512,8 @@ matchPatterns (PatternArg impl1 name1 pat1) (PatternArg impl2 name2 pat2) = runInferenceDefs :: (Members '[Termination, Error TypeCheckerError, ResultBuilder, NameIdGen] r, HasExpressions funDef) => - Sem (Inference ': r) (NonEmpty funDef) -> - Sem r (NonEmpty funDef) + Sem (Inference ': r) funDef -> + Sem r funDef runInferenceDefs a = do (finalState, expr) <- runInferenceState iniState a (subs, idens) <- closeState finalState @@ -522,13 +521,7 @@ runInferenceDefs a = do stash' <- mapM (subsHoles subs) (finalState ^. inferenceFunctionsStash) forM_ stash' registerFunctionDef addIdenTypes (TypesTable idens') - mapM (subsHoles subs) expr - -runInferenceDef :: - (Members '[Termination, Error TypeCheckerError, ResultBuilder, NameIdGen] r, HasExpressions funDef) => - Sem (Inference ': r) funDef -> - Sem r funDef -runInferenceDef = fmap head . runInferenceDefs . fmap pure + subsHoles subs expr -- | Assumes the given function has been type checked. Does *not* register the -- function. diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs index 42b50a6bbb..b717189745 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs @@ -48,6 +48,9 @@ initResultBuilderState ctx = _resultBuilderStateCombinedCoercionTable = ctx ^. importContextCoercions } +evalResultBuilder :: ImportContext -> Sem (ResultBuilder ': r) a -> Sem r a +evalResultBuilder ctx = fmap snd . runResultBuilder ctx + runResultBuilder' :: ResultBuilderState -> Sem (ResultBuilder ': r) a -> diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs index bdf1b01433..f6feb6370b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs @@ -6,17 +6,21 @@ 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.CheckerNew.Options import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error import Juvix.Prelude checkTraitTermination :: forall r. - (Member (Error TypeCheckerError) r) => + (Members '[Reader TypeCheckingOptions, Error TypeCheckerError] r) => InstanceApp -> InstanceInfo -> Sem r () -checkTraitTermination InstanceApp {..} InstanceInfo {..} = - mapM_ checkArg _instanceAppArgs +checkTraitTermination InstanceApp {..} InstanceInfo {..} = do + mode <- asks (^. typeCheckingMode) + case mode of + TypeCheckingNormal -> mapM_ checkArg _instanceAppArgs + TypeCheckingBuildCallMap -> return () where checkArg :: InstanceParam -> Sem r () checkArg arg = diff --git a/src/Juvix/Compiler/Internal/Translation/Repl.hs b/src/Juvix/Compiler/Internal/Translation/Repl.hs index d4ab9aefa1..ae24df0fd3 100644 --- a/src/Juvix/Compiler/Internal/Translation/Repl.hs +++ b/src/Juvix/Compiler/Internal/Translation/Repl.hs @@ -23,6 +23,7 @@ typeCheckExpressionType exp = do table <- extendedTableReplArtifacts exp stable <- gets (^. artifactScopeTable) runResultBuilderArtifacts + . runReader defaultTypeCheckingOptions . runNameIdGenArtifacts . ignoreHighlightBuilder . runReader table @@ -31,7 +32,7 @@ typeCheckExpressionType exp = do . withEmptyLocalVars . withEmptyInsertedArgsStack . mapError (JuvixError @TypeCheckerError) - . runInferenceDef + . runInferenceDefs $ inferExpression Nothing exp >>= traverseOf typedType strongNormalize_ diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs index 2f6ac71cf6..f33a08ee6a 100644 --- a/src/Juvix/Compiler/Pipeline.hs +++ b/src/Juvix/Compiler/Pipeline.hs @@ -33,6 +33,7 @@ import Juvix.Compiler.Core.Transformation import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped import Juvix.Compiler.Internal qualified as Internal import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Options import Juvix.Compiler.Nockma.Translation.FromTree qualified as NockmaTree import Juvix.Compiler.Pipeline.Artifacts import Juvix.Compiler.Pipeline.EntryPoint @@ -132,6 +133,11 @@ upToInternal = do pkg <- asks (^. entryPointPackage) runReader pkg upToScoping >>= Internal.fromConcrete +upToInternalTypedOptions :: + (Members '[Reader TypeCheckingOptions, HighlightBuilder, Reader Parser.ParserResult, Error JuvixError, Reader EntryPoint, Reader Store.ModuleTable, NameIdGen] r) => + Sem r Internal.InternalTypedResult +upToInternalTypedOptions = Internal.typeCheckingNewOptions upToInternal + upToInternalTyped :: (Members '[HighlightBuilder, Reader Parser.ParserResult, Error JuvixError, Reader EntryPoint, Reader Store.ModuleTable, NameIdGen] r) => Sem r Internal.InternalTypedResult diff --git a/src/Juvix/Compiler/Pipeline/Result.hs b/src/Juvix/Compiler/Pipeline/Result.hs index 4e143287b4..5666184644 100644 --- a/src/Juvix/Compiler/Pipeline/Result.hs +++ b/src/Juvix/Compiler/Pipeline/Result.hs @@ -19,3 +19,6 @@ data PipelineResult a = PipelineResult makeLenses ''PipelineResult instance (NFData a) => NFData (PipelineResult a) + +instance Functor PipelineResult where + fmap f = over pipelineResult f diff --git a/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs b/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs index e85366ac45..629a2f4411 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs @@ -2,6 +2,7 @@ module Juvix.Compiler.Store.Internal.Data.InstanceInfo where import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Internal.Language +import Juvix.Compiler.Internal.Pretty.Base import Juvix.Extra.Serialize import Juvix.Prelude @@ -17,6 +18,14 @@ instance Serialize InstanceParam instance NFData InstanceParam +instance HasAtomicity InstanceParam where + atomicity = \case + InstanceParamVar v -> atomicity v + InstanceParamMeta v -> atomicity v + InstanceParamHole h -> atomicity h + InstanceParamApp h -> atomicity h + InstanceParamFun h -> atomicity h + data InstanceApp = InstanceApp { _instanceAppHead :: Name, _instanceAppArgs :: [InstanceParam], @@ -25,6 +34,9 @@ data InstanceApp = InstanceApp } deriving stock (Eq, Generic) +instance HasAtomicity InstanceApp where + atomicity = const (Aggregate appFixity) + instance Serialize InstanceApp instance NFData InstanceApp @@ -37,6 +49,9 @@ data InstanceFun = InstanceFun } deriving stock (Eq, Generic) +instance HasAtomicity InstanceFun where + atomicity = const (Aggregate funFixity) + instance Serialize InstanceFun instance NFData InstanceFun @@ -74,6 +89,9 @@ makeLenses ''InstanceFun makeLenses ''InstanceInfo makeLenses ''InstanceTable +instance PrettyCode InstanceInfo where + ppCode = ppCode . (^. instanceInfoIden) + instance Semigroup InstanceTable where t1 <> t2 = InstanceTable $ @@ -84,3 +102,19 @@ instance Semigroup InstanceTable where instance Monoid InstanceTable where mempty = InstanceTable mempty + +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) + +instance PrettyCode InstanceParam where + ppCode = ppCode . paramToExpression diff --git a/src/Juvix/Data/Hole.hs b/src/Juvix/Data/Hole.hs index 692d99ff1c..5f617c83cf 100644 --- a/src/Juvix/Data/Hole.hs +++ b/src/Juvix/Data/Hole.hs @@ -1,5 +1,6 @@ module Juvix.Data.Hole where +import Juvix.Data.Fixity import Juvix.Data.Keyword import Juvix.Data.Keyword.All (kwWildcard) import Juvix.Data.Loc @@ -14,6 +15,9 @@ data Hole = Hole } deriving stock (Show, Data, Generic) +instance HasAtomicity Hole where + atomicity = const Atom + mkHole :: Interval -> NameId -> Hole mkHole loc uid = Hole