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..a63958966f 100644 --- a/app/Commands/Dev/InstanceTermination/Calls.hs +++ b/app/Commands/Dev/InstanceTermination/Calls.hs @@ -2,6 +2,15 @@ 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.Data.Context -runCommand :: CallsOptions -> Sem r () -runCommand CallsOptions {} = return () +runCommand :: (Members AppEffects r) => CallsOptions -> Sem r () +runCommand localOpts@CallsOptions {..} = do + globalOpts <- askGlobalOptions + PipelineResult {..} <- runPipelineTermination (Just _callsInputFile) upToInternalTyped + 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..58fd0d4e6b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs @@ -1,5 +1,6 @@ module Juvix.Compiler.Internal.Translation.FromInternal ( typeCheckingNew, + computeImportContext, ) where @@ -18,13 +19,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 +54,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 +73,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..4ee24e8c2c 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -3,6 +3,9 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Ch checkTopModule, withEmptyInsertedArgsStack, inferExpression, + TypeCheckingOptions (..), + defaultTypeCheckingOptions, + mutualBlockInstanceCallMap, ) where @@ -33,6 +36,29 @@ import Juvix.Compiler.Pipeline.EntryPoint import Juvix.Data.Effect.NameIdGen 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 + data FunctionDefaultInfo = FunctionDefaultInfo { _functionDefaultArgId :: ArgId, _functionDefaultValue :: Expression @@ -140,7 +166,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 +174,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 +191,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,7 +207,7 @@ 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) @@ -191,7 +217,7 @@ checkInductiveDef :: (Members '[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 +276,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) = @@ -578,12 +604,14 @@ checkResolveInstanceHoles :: forall r. ( Members '[ Reader InfoTable, + Reader TypeCheckingOptions, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, + Output InstanceCallMap, Reader InsertedArgsStack ] r @@ -592,9 +620,25 @@ 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, + 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 +647,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,6 +658,38 @@ 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, 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/Repl.hs b/src/Juvix/Compiler/Internal/Translation/Repl.hs index d4ab9aefa1..31b9ac9cf1 100644 --- a/src/Juvix/Compiler/Internal/Translation/Repl.hs +++ b/src/Juvix/Compiler/Internal/Translation/Repl.hs @@ -31,7 +31,7 @@ typeCheckExpressionType exp = do . withEmptyLocalVars . withEmptyInsertedArgsStack . mapError (JuvixError @TypeCheckerError) - . runInferenceDef + . runInferenceDefs $ inferExpression Nothing exp >>= traverseOf typedType strongNormalize_ 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