diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index 95354db193..fd598e525c 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -1,6 +1,7 @@ module Juvix.Compiler.Internal.Data.InfoTable ( module Juvix.Compiler.Store.Internal.Language, buildTable, + buildInfoTable, extendWithReplExpression, lookupConstructor, lookupConstructorArgTypes, @@ -13,6 +14,8 @@ module Juvix.Compiler.Internal.Data.InfoTable getAxiomBuiltinInfo, getFunctionBuiltinInfo, mkConstructorEntries, + functionInfoFromFunctionDef, + inductiveInfoFromInductiveDef, ) where @@ -25,9 +28,6 @@ import Juvix.Compiler.Internal.Pretty (ppTrace) import Juvix.Compiler.Store.Internal.Language import Juvix.Prelude -buildTable :: (Foldable f) => StoredModuleTable -> f Module -> InfoTable -buildTable mtab = mconcatMap (computeTable mtab) - functionInfoFromFunctionDef :: FunctionDef -> FunctionInfo functionInfoFromFunctionDef FunctionDef {..} = FunctionInfo @@ -78,21 +78,29 @@ letFunctionDefs e = LetFunDef f -> pure f LetMutualBlock (MutualBlockLet fs) -> fs -computeTable :: StoredModuleTable -> Module -> InfoTable -computeTable mtab m = compute +buildInfoTable :: StoredModuleTable -> InfoTable +buildInfoTable = mconcatMap (^. storedModuleInfoTable) . HashMap.elems . (^. storedModuleTable) + +buildTable :: (Foldable f) => f Module -> StoredModuleTable +buildTable = foldr go mempty where - compute :: InfoTable - compute = - InfoTable {..} <> mconcatMap goImport imports + go :: Module -> StoredModuleTable -> StoredModuleTable + go m mtab = mtab' where - goImport :: Import -> InfoTable - goImport Import {..} = - let sm = lookupStoredModule mtab _importModuleName - in sm ^. storedModuleInfoTable <> mconcatMap goImport (sm ^. storedModuleImports) + sm = computeStoredModule m + mtab' = over storedModuleTable (HashMap.insert (sm ^. storedModuleName) sm) mtab - imports :: [Import] - imports = m ^. moduleBody . moduleImports +computeStoredModule :: Module -> StoredModule +computeStoredModule m@Module {..} = + StoredModule + { _storedModuleName = _moduleName, + _storedModuleImports = _moduleBody ^. moduleImports, + _storedModuleInfoTable = computeInfoTable m + } +computeInfoTable :: Module -> InfoTable +computeInfoTable m = InfoTable {..} + where mutuals :: [MutualStatement] mutuals = [ d diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 3c174da438..c131a7f095 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -30,6 +30,7 @@ import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context import Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker import Juvix.Compiler.Pipeline.EntryPoint +import Juvix.Compiler.Store.Scoped.Language qualified as S import Juvix.Data.NameKind import Juvix.Prelude import Safe (lastMay) @@ -61,7 +62,7 @@ fromConcrete _resultScoper = . runReader @DefaultArgsStack mempty . runCacheEmpty goModuleNoCache $ mapM goTopModule ms - let _resultTable = buildTable _resultModules + let _resultTable = buildTable _resultModules -- TODO: imports _resultDepInfo = buildDependencyInfo _resultModules exportTbl _resultModulesCache = ModulesCache modulesCache return InternalResult {..} @@ -138,13 +139,10 @@ fromConcreteImport :: Scoper.Import 'Scoped -> Sem r Internal.Import fromConcreteImport i = do - i' <- - mapError (JuvixError @ScoperError) - . runReader @Pragmas mempty - . goImport - $ i - checkTerminationShallow i' - return i' + mapError (JuvixError @ScoperError) + . runReader @Pragmas mempty + . goImport + $ i goLocalModule :: (Members '[Reader DefaultArgsStack, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader NameSignatures, Reader ConstructorNameSignatures] r) => @@ -177,11 +175,12 @@ goPragmas p = do return $ p' <> p ^. _Just . withLocParam . withSourceValue goScopedIden :: ScopedIden -> Internal.Name -goScopedIden iden = +goScopedIden iden = goName (iden ^. scopedIdenFinal) + +goName :: S.Name -> Internal.Name +goName name = set Internal.namePretty prettyStr (goSymbol (S.nameUnqualify name)) where - name :: S.Name - name = iden ^. scopedIdenFinal prettyStr :: Text prettyStr = prettyText name @@ -325,19 +324,14 @@ scanImports = mconcatMap go goImport :: forall r. - (Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r) => Import 'Scoped -> Sem r Internal.Import -goImport Import {..} = undefined - -{- let m = _importModule ^. moduleRefModule - m' <- goTopModule m +goImport Import {..} = return ( Internal.Import - { _importModuleName = undefined + { _importModuleName = goName (_importModule ^. S.scopedModuleName) } ) --} -- | Ignores functions goAxiomInductive :: diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs index 6f1c53d957..d633ff4b70 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs @@ -20,7 +20,7 @@ newtype ModulesCache = ModulesCache data InternalResult = InternalResult { _resultScoper :: Concrete.ScoperResult, - _resultTable :: InfoTable, + _resultTable :: StoredModuleTable, _resultModules :: NonEmpty Module, _resultDepInfo :: NameDependencyInfo, _resultModulesCache :: ModulesCache diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs index c29061f4cb..5bf39093be 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs @@ -1,6 +1,5 @@ module Juvix.Compiler.Internal.Translation.FromInternal - ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability, - arityChecking, + ( arityChecking, typeChecking, typeCheckExpression, typeCheckExpressionType, @@ -14,10 +13,8 @@ import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Builtins.Effect import Juvix.Compiler.Concrete.Data.Highlight.Input import Juvix.Compiler.Internal.Language -import Juvix.Compiler.Internal.Pretty import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as ArityChecking -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking import Juvix.Compiler.Pipeline.Artifacts @@ -38,11 +35,12 @@ arityChecking res@InternalResult {..} = return ArityChecking.InternalArityResult { _resultInternalResult = res, - _resultModules = r + _resultModules = r, + _resultTable = buildTable r } where table :: InfoTable - table = buildTable _resultModules + table = buildInfoTable _resultTable arityCheckExpression :: (Members '[Error JuvixError, State Artifacts] r) => @@ -56,17 +54,19 @@ arityCheckExpression exp = do $ ArityChecking.inferReplExpression exp arityCheckImport :: - (Members '[Error JuvixError, State Artifacts] r) => + -- (Members '[Error JuvixError, State Artifacts] r) => Import -> Sem r Import -arityCheckImport i = do - artiTable <- gets (^. artifactInternalTypedTable) - let table = buildTable [i ^. importModule . moduleIxModule] <> artiTable +arityCheckImport = return + +{- artiTable <- gets (^. artifactInternalTypedTable) + let table = buildTable <> artiTable mapError (JuvixError @ArityChecking.ArityCheckerError) . runReader table . runNameIdGenArtifacts . evalCacheEmpty ArityChecking.checkModuleIndexNoCache $ ArityChecking.checkImport i +-} typeCheckExpressionType :: forall r. @@ -95,12 +95,13 @@ typeCheckExpression :: typeCheckExpression exp = (^. typedExpression) <$> typeCheckExpressionType exp typeCheckImport :: - (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) => + -- (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) => Import -> Sem r Import -typeCheckImport i = do - artiTable <- gets (^. artifactInternalTypedTable) - let table = buildTable [i ^. importModule . moduleIxModule] <> artiTable +typeCheckImport = return + +{- artiTable <- gets (^. artifactInternalTypedTable) + let table = buildTable mempty [i ^. importModule . moduleIxModule] <> artiTable modify (set artifactInternalTypedTable table) mapError (JuvixError @TypeCheckerError) . runTypesTableArtifacts @@ -114,6 +115,7 @@ typeCheckImport i = do -- TODO Store cache in Artifacts and use it here . evalCacheEmpty checkModuleNoCache $ checkTable >> checkImport i +-} typeChecking :: forall r. @@ -124,7 +126,7 @@ typeChecking a = do (termin, (res, table, (normalized, (idens, (funs, r))))) <- runTermination iniTerminationState $ do res <- a let table :: InfoTable - table = buildTable (res ^. ArityChecking.resultModules) + table = buildInfoTable (res ^. ArityChecking.resultTable) entryPoint :: EntryPoint entryPoint = res ^. ArityChecking.internalArityResultEntryPoint diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs index 66157fff2e..f33e810390 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs @@ -53,11 +53,8 @@ checkModuleIndex :: Sem r ModuleIndex checkModuleIndex (ModuleIndex m) = ModuleIndex <$> checkModule m -checkImport :: - (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) => - Import -> - Sem r Import -checkImport = undefined +checkImport :: Import -> Sem r Import +checkImport = return checkInductive :: forall r. (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => InductiveDef -> Sem r InductiveDef checkInductive d = do diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Context.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Context.hs index b4180489fe..557c6a7d37 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Context.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Context.hs @@ -4,11 +4,13 @@ import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Cont import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal import Juvix.Compiler.Pipeline.EntryPoint qualified as E +import Juvix.Compiler.Store.Internal.Language import Juvix.Prelude data InternalArityResult = InternalArityResult { _resultInternalResult :: Internal.InternalResult, - _resultModules :: NonEmpty Module + _resultModules :: NonEmpty Module, + _resultTable :: StoredModuleTable } makeLenses ''InternalArityResult diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs deleted file mode 100644 index 0d314d7609..0000000000 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs +++ /dev/null @@ -1,64 +0,0 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability (filterUnreachable) where - -import Juvix.Compiler.Internal.Data.NameDependencyInfo -import Juvix.Compiler.Internal.Language -import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as Arity -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Typed -import Juvix.Compiler.Pipeline.EntryPoint -import Juvix.Prelude - -type MCache = Cache ModuleIndex Module - -filterUnreachable :: (Members '[Reader EntryPoint] r) => Typed.InternalTypedResult -> Sem r Typed.InternalTypedResult -filterUnreachable r = do - asks (^. entryPointSymbolPruningMode) >>= \case - KeepAll -> return r - FilterUnreachable -> return (set Typed.resultModules modules' r) - where - depInfo = r ^. Typed.resultInternalArityResult . Arity.resultInternalResult . resultDepInfo - modules = r ^. Typed.resultModules - modules' = - run - . runReader depInfo - . evalCacheEmpty goModuleNoCache - $ mapM goModule modules - -askIsReachable :: (Member (Reader NameDependencyInfo) r) => Name -> Sem r Bool -askIsReachable n = do - depInfo <- ask - return (isReachable depInfo n) - -returnIfReachable :: (Member (Reader NameDependencyInfo) r) => Name -> a -> Sem r (Maybe a) -returnIfReachable n a = do - r <- askIsReachable n - return (guard r $> a) - -goModuleNoCache :: forall r. (Members '[Reader NameDependencyInfo, MCache] r) => ModuleIndex -> Sem r Module -goModuleNoCache (ModuleIndex m) = do - body' <- goBody (m ^. moduleBody) - return (set moduleBody body' m) - where - goBody :: ModuleBody -> Sem r ModuleBody - goBody body = do - _moduleStatements <- mapMaybeM goMutual (body ^. moduleStatements) - _moduleImports <- mapM goImport (body ^. moduleImports) - return ModuleBody {..} - -goModule :: (Members '[Reader NameDependencyInfo, MCache] r) => Module -> Sem r Module -goModule = cacheGet . ModuleIndex - -goModuleIndex :: (Members '[Reader NameDependencyInfo, MCache] r) => ModuleIndex -> Sem r ModuleIndex -goModuleIndex = fmap ModuleIndex . cacheGet - --- note that the first mutual statement is reachable iff all are reachable -goMutual :: forall r. (Member (Reader NameDependencyInfo) r) => MutualBlock -> Sem r (Maybe MutualBlock) -goMutual b@(MutualBlock (m :| _)) = case m of - StatementFunction f -> returnIfReachable (f ^. funDefName) b - StatementInductive f -> returnIfReachable (f ^. inductiveName) b - StatementAxiom ax -> returnIfReachable (ax ^. axiomName) b - -goImport :: forall r. (Members '[Reader NameDependencyInfo, MCache] r) => Import -> Sem r Import -goImport i = do - _importModule <- goModuleIndex (i ^. importModule) - return Import {..} diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs index e26557764f..77750bedfe 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs @@ -53,9 +53,6 @@ evalTermination s = fmap snd . runTermination s execTermination :: (Members '[Error JuvixError] r) => TerminationState -> Sem (Termination ': r) a -> Sem r TerminationState execTermination s = fmap fst . runTermination s -instance Scannable Import where - buildCallMap = buildCallMap . (^. importModule . moduleIxModule) - instance Scannable Module where buildCallMap = run diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index a86b072361..91c761062f 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -92,11 +92,8 @@ checkModuleBody ModuleBody {..} = do _moduleImports = _moduleImports' } -checkImport :: - (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination] r) => - Import -> - Sem r Import -checkImport = traverseOf importModule checkModuleIndex +checkImport :: Import -> Sem r Import +checkImport = return checkMutualBlock :: (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) => @@ -127,7 +124,7 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do _inductiveTrait, _inductivePragmas } - checkPositivity d + checkPositivity (inductiveInfoFromInductiveDef d) return d where paramLocals :: LocalVars @@ -643,7 +640,7 @@ checkPattern = go Left hole -> return (Left hole) Right (ind, args) -> do params :: [InductiveParameter] <- - (^. inductiveInfoDef . inductiveParameters) + (^. inductiveInfoParameters) <$> lookupInductive ind let numArgs = length args numParams = length params @@ -879,7 +876,7 @@ inferExpression' hint e = case e of goIden i = case i of IdenFunction fun -> do info <- lookupFunction fun - return (TypedExpression (info ^. functionInfoDef . funDefType) (ExpressionIden i)) + return (TypedExpression (info ^. functionInfoType) (ExpressionIden i)) IdenConstructor c -> do ty <- lookupConstructorType c return (TypedExpression ty (ExpressionIden i)) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs index e0563f0934..0421a67ef0 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs @@ -24,7 +24,7 @@ subsIToE = fmap paramToExpression type CoercionChain = [(CoercionInfo, SubsI)] isTrait :: InfoTable -> Name -> Bool -isTrait tab name = maybe False (^. inductiveInfoDef . inductiveTrait) (HashMap.lookup name (tab ^. infoInductives)) +isTrait tab name = maybe False (^. inductiveInfoTrait) (HashMap.lookup name (tab ^. infoInductives)) resolveTraitInstance :: (Members '[Error TypeCheckerError, NameIdGen, Inference, Reader InfoTable] r) => diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs index 2bfc1ab534..0e6c2e7e09 100644 --- a/src/Juvix/Compiler/Pipeline.hs +++ b/src/Juvix/Compiler/Pipeline.hs @@ -78,16 +78,10 @@ upToInternalTyped :: Sem r Internal.InternalTypedResult upToInternalTyped = Internal.typeChecking upToInternalArity -upToInternalReachability :: - (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, GitClone, PathResolver] r) => - Sem r Internal.InternalTypedResult -upToInternalReachability = - upToInternalTyped >>= Internal.filterUnreachable - upToCore :: (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, GitClone, PathResolver] r) => Sem r Core.CoreResult -upToCore = upToInternalReachability >>= Core.fromInternal +upToCore = upToInternalTyped >>= Core.fromInternal upToAsm :: (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, GitClone, PathResolver] r) => diff --git a/src/Juvix/Compiler/Store/Internal/Language.hs b/src/Juvix/Compiler/Store/Internal/Language.hs index 6e955459bb..157ea4618b 100644 --- a/src/Juvix/Compiler/Store/Internal/Language.hs +++ b/src/Juvix/Compiler/Store/Internal/Language.hs @@ -23,6 +23,7 @@ newtype StoredModuleTable = StoredModuleTable { _storedModuleTable :: HashMap Name StoredModule } deriving stock (Generic) + deriving newtype (Semigroup, Monoid) instance Serialize StoredModuleTable