Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Group tables related to typechecking #3056

Merged
merged 1 commit into from
Sep 25, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 10 additions & 5 deletions src/Juvix/Compiler/Core/Translation/FromInternal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,10 @@ computeImplicitArgs = \case
False : computeImplicitArgs _functionRight
_ -> []

fromInternal :: (Members '[NameIdGen, Reader Store.ModuleTable, Error JuvixError] k) => Internal.InternalTypedResult -> Sem k CoreResult
fromInternal ::
(Members '[NameIdGen, Reader Store.ModuleTable, Error JuvixError] k) =>
InternalTyped.InternalTypedResult ->
Sem k CoreResult
fromInternal i = mapError (JuvixError . ErrBadScope) $ do
importTab <- asks Store.getInternalModuleTable
coreImportsTab <- asks Store.computeCombinedCoreInfoTable
Expand All @@ -65,10 +68,11 @@ fromInternal i = mapError (JuvixError . ErrBadScope) $ do
_moduleInfoTable = mempty,
_moduleImportsTable = coreImportsTab
}
tabs = i ^. InternalTyped.resultTypeCheckingTables
res <-
execInfoTableBuilder md
. runReader (i ^. InternalTyped.resultFunctions)
. runReader (i ^. InternalTyped.resultIdenTypes)
. runReader (tabs ^. InternalTyped.typeCheckingTablesFunctionsTable)
. runReader (tabs ^. InternalTyped.typeCheckingTablesTypesTable)
$ do
when
(isNothing (coreImportsTab ^. infoLiteralIntToNat))
Expand Down Expand Up @@ -101,11 +105,12 @@ fromInternalExpression importTab res exp = do
let mtab =
res ^. coreResultInternalTypedResult . InternalTyped.resultInternalModule . Internal.internalModuleInfoTable
<> Internal.computeCombinedInfoTable importTab
tabs = res ^. coreResultInternalTypedResult . InternalTyped.resultTypeCheckingTables
fmap snd
. runReader mtab
. runInfoTableBuilder (res ^. coreResultModule)
. runReader (res ^. coreResultInternalTypedResult . InternalTyped.resultFunctions)
. runReader (res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes)
. runReader (tabs ^. InternalTyped.typeCheckingTablesFunctionsTable)
. runReader (tabs ^. InternalTyped.typeCheckingTablesTypesTable)
$ fromTopIndex (goExpression exp)

goModule ::
Expand Down
9 changes: 3 additions & 6 deletions src/Juvix/Compiler/Internal/Data/InfoTable.hs
Original file line number Diff line number Diff line change
Expand Up @@ -80,17 +80,14 @@ letFunctionDefs e =
LetFunDef f -> pure f
LetMutualBlock (MutualBlockLet fs) -> fs

computeInternalModule :: InstanceTable -> CoercionTable -> TypesTable -> FunctionsTable -> Module -> InternalModule
computeInternalModule instTab coeTab tysTab funsTab m@Module {..} =
computeInternalModule :: TypeCheckingTables -> Module -> InternalModule
computeInternalModule tabs m@Module {..} =
InternalModule
{ _internalModuleId = _moduleId,
_internalModuleName = _moduleName,
_internalModuleImports = _moduleBody ^. moduleImports,
_internalModuleInfoTable = computeInternalModuleInfoTable m,
_internalModuleTypesTable = tysTab,
_internalModuleFunctionsTable = funsTab,
_internalModuleInstanceTable = instTab,
_internalModuleCoercionTable = coeTab
_internalModuleTypeCheckingTables = tabs
}

computeInternalModuleInfoTable :: Module -> InfoTable
Expand Down
1 change: 0 additions & 1 deletion src/Juvix/Compiler/Internal/Translation/Extra.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ where
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Translation
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
import Juvix.Prelude

unfoldPolyApplication :: (Member (Reader TypesTable) r) => Application -> Sem r (Expression, [Expression])
Expand Down
21 changes: 3 additions & 18 deletions src/Juvix/Compiler/Internal/Translation/FromInternal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -34,34 +34,19 @@ 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 = ImportContext (computeTypeCheckingTables itab)
fmap (res,)
. runReader table
. runReader (stable ^. Scoped.infoBuiltins)
. runResultBuilder importCtx
. mapError (JuvixError @TypeCheckerError)
$ checkTopModule (res ^. Internal.resultModule)
let md =
computeInternalModule
(bst ^. resultBuilderStateInstanceTable)
(bst ^. resultBuilderStateCoercionTable)
(bst ^. resultBuilderStateTypesTable)
(bst ^. resultBuilderStateFunctionsTable)
checkedModule
let md = computeInternalModule (bst ^. resultBuilderStateTables) checkedModule
return
InternalTypedResult
{ _resultInternal = res,
_resultModule = checkedModule,
_resultInternalModule = md,
_resultTermination = termin,
_resultIdenTypes = bst ^. resultBuilderStateCombinedTypesTable,
_resultFunctions = bst ^. resultBuilderStateCombinedFunctionsTable,
_resultInstances = bst ^. resultBuilderStateCombinedInstanceTable,
_resultCoercions = bst ^. resultBuilderStateCombinedCoercionTable
_resultTypeCheckingTables = bst ^. resultBuilderStateCombinedTables
}
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context,
module Juvix.Compiler.Store.Internal.Data.FunctionsTable,
module Juvix.Compiler.Store.Internal.Data.TypesTable,
module Juvix.Compiler.Store.Internal.Data.TypeCheckingTables,
module Juvix.Compiler.Internal.Data.InfoTable,
)
where
Expand All @@ -10,28 +9,19 @@ 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.Store.Internal.Data.CoercionInfo
import Juvix.Compiler.Store.Internal.Data.FunctionsTable
import Juvix.Compiler.Store.Internal.Data.InstanceInfo
import Juvix.Compiler.Store.Internal.Data.TypesTable
import Juvix.Compiler.Store.Internal.Data.TypeCheckingTables
import Juvix.Prelude

data InternalTypedResult = InternalTypedResult
{ _resultInternal :: Internal.InternalResult,
_resultModule :: Module,
_resultInternalModule :: InternalModule,
_resultTermination :: TerminationState,
_resultIdenTypes :: TypesTable,
_resultFunctions :: FunctionsTable,
_resultInstances :: InstanceTable,
_resultCoercions :: CoercionTable
_resultTypeCheckingTables :: TypeCheckingTables
}

data ImportContext = ImportContext
{ _importContextTypesTable :: TypesTable,
_importContextFunctionsTable :: FunctionsTable,
_importContextInstances :: InstanceTable,
_importContextCoercions :: CoercionTable
newtype ImportContext = ImportContext
{ _importContextTables :: TypeCheckingTables
}

makeLenses ''InternalTypedResult
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -617,10 +617,13 @@ strongNormalize'' ty = do
ftab <- ask
let importCtx =
ImportContext
{ _importContextCoercions = mempty,
_importContextInstances = mempty,
_importContextTypesTable = mempty,
_importContextFunctionsTable = ftab
{ _importContextTables =
TypeCheckingTables
{ _typeCheckingTablesCoercionTable = mempty,
_typeCheckingTablesInstanceTable = mempty,
_typeCheckingTablesTypesTable = mempty,
_typeCheckingTablesFunctionsTable = ftab
}
}
fmap snd
. runResultBuilder importCtx
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,73 +15,68 @@ data ResultBuilder :: Effect where
AddCoercionInfo :: CoercionInfo -> ResultBuilder m ()
LookupFunctionDef :: FunctionName -> ResultBuilder m (Maybe Expression)
LookupIdenType :: NameId -> ResultBuilder m (Maybe Expression)
LookupInstanceInfo :: Name -> ResultBuilder m (Maybe [InstanceInfo])
LookupCoercionInfo :: Name -> ResultBuilder m (Maybe [CoercionInfo])
GetCombinedInstanceTable :: ResultBuilder m InstanceTable
GetCombinedCoercionTable :: ResultBuilder m CoercionTable

makeSem ''ResultBuilder

typeCheckingTablesFromImportContext :: ImportContext -> TypeCheckingTables
typeCheckingTablesFromImportContext = (^. importContextTables)

data ResultBuilderState = ResultBuilderState
{ _resultBuilderStateTypesTable :: TypesTable,
_resultBuilderStateFunctionsTable :: FunctionsTable,
_resultBuilderStateInstanceTable :: InstanceTable,
_resultBuilderStateCoercionTable :: CoercionTable,
_resultBuilderStateCombinedTypesTable :: TypesTable,
_resultBuilderStateCombinedFunctionsTable :: FunctionsTable,
_resultBuilderStateCombinedInstanceTable :: InstanceTable,
_resultBuilderStateCombinedCoercionTable :: CoercionTable
{ _resultBuilderStateTables :: TypeCheckingTables,
_resultBuilderStateCombinedTables :: TypeCheckingTables
}

makeLenses ''ResultBuilderState

initResultBuilderState :: ImportContext -> ResultBuilderState
initResultBuilderState ctx =
ResultBuilderState
{ _resultBuilderStateFunctionsTable = mempty,
_resultBuilderStateTypesTable = mempty,
_resultBuilderStateInstanceTable = mempty,
_resultBuilderStateCoercionTable = mempty,
_resultBuilderStateCombinedFunctionsTable = ctx ^. importContextFunctionsTable,
_resultBuilderStateCombinedTypesTable = ctx ^. importContextTypesTable,
_resultBuilderStateCombinedInstanceTable = ctx ^. importContextInstances,
_resultBuilderStateCombinedCoercionTable = ctx ^. importContextCoercions
{ _resultBuilderStateTables = mempty,
_resultBuilderStateCombinedTables = typeCheckingTablesFromImportContext ctx
}

runResultBuilder' ::
ResultBuilderState ->
Sem (ResultBuilder ': r) a ->
Sem r (ResultBuilderState, a)
runResultBuilder' inis = reinterpret (runState inis) $ \case
AddFunctionDef name def -> do
modify' (over (resultBuilderStateFunctionsTable . functionsTable) (HashMap.insert name def))
modify' (over (resultBuilderStateCombinedFunctionsTable . functionsTable) (HashMap.insert name def))
AddIdenType nid ty -> do
modify' (over (resultBuilderStateTypesTable . typesTable) (HashMap.insert nid ty))
modify' (over (resultBuilderStateCombinedTypesTable . typesTable) (HashMap.insert nid ty))
AddIdenTypes itab -> do
modify' (over (resultBuilderStateTypesTable . typesTable) (HashMap.union (itab ^. typesTable)))
modify' (over (resultBuilderStateCombinedTypesTable . typesTable) (HashMap.union (itab ^. typesTable)))
AddFunctionDef name def ->
overBothTables (set (typeCheckingTablesFunctionsTable . functionsTable . at name) (Just def))
AddIdenType nid ty ->
overBothTables (set (typeCheckingTablesTypesTable . typesTable . at nid) (Just ty))
AddIdenTypes itab ->
overBothTables (over (typeCheckingTablesTypesTable . typesTable) (HashMap.union (itab ^. typesTable)))
AddInstanceInfo ii -> do
modify' (over (resultBuilderStateInstanceTable) (flip updateInstanceTable ii))
modify' (over (resultBuilderStateCombinedInstanceTable) (flip updateInstanceTable ii))
AddCoercionInfo ii -> do
modify' (over (resultBuilderStateCoercionTable) (flip updateCoercionTable ii))
modify' (over (resultBuilderStateCombinedCoercionTable) (flip updateCoercionTable ii))
overBothTables (over typeCheckingTablesInstanceTable (`updateInstanceTable` ii))
AddCoercionInfo ii ->
overBothTables (over typeCheckingTablesCoercionTable (`updateCoercionTable` ii))
LookupFunctionDef name ->
gets (^. resultBuilderStateCombinedFunctionsTable . functionsTable . at name)
gets (^. resultBuilderStateCombinedTables . typeCheckingTablesFunctionsTable . functionsTable . at name)
LookupIdenType nid ->
gets (^. resultBuilderStateCombinedTypesTable . typesTable . at nid)
LookupInstanceInfo name -> do
tab <- gets (^. resultBuilderStateCombinedInstanceTable)
return $ lookupInstanceTable tab name
LookupCoercionInfo name -> do
tab <- gets (^. resultBuilderStateCombinedCoercionTable)
return $ lookupCoercionTable tab name
gets (^. resultBuilderStateCombinedTables . typeCheckingTablesTypesTable . typesTable . at nid)
GetCombinedInstanceTable ->
gets (^. resultBuilderStateCombinedInstanceTable)
gets (^. resultBuilderStateCombinedTables . typeCheckingTablesInstanceTable)
GetCombinedCoercionTable ->
gets (^. resultBuilderStateCombinedCoercionTable)
gets (^. resultBuilderStateCombinedTables . typeCheckingTablesCoercionTable)
where
overBothTables :: (Members '[State ResultBuilderState] r') => (TypeCheckingTables -> TypeCheckingTables) -> Sem r' ()
overBothTables f = modify $ \res ->
res
{ _resultBuilderStateTables = f (res ^. resultBuilderStateTables),
_resultBuilderStateCombinedTables = f (res ^. resultBuilderStateCombinedTables)
}

lookupInstanceInfo :: (Members '[ResultBuilder] r) => Name -> Sem r (Maybe [InstanceInfo])
lookupInstanceInfo name = do
tab <- getCombinedInstanceTable
return $ lookupInstanceTable tab name

lookupCoercionInfo :: (Members '[ResultBuilder] r) => Name -> Sem r (Maybe [CoercionInfo])
lookupCoercionInfo name = do
tab <- getCombinedCoercionTable
return $ lookupCoercionTable tab name

runResultBuilder :: ImportContext -> Sem (ResultBuilder ': r) a -> Sem r (ResultBuilderState, a)
runResultBuilder ctx a =
Expand Down
22 changes: 5 additions & 17 deletions src/Juvix/Compiler/Pipeline/Artifacts.hs
Original file line number Diff line number Diff line change
Expand Up @@ -69,10 +69,10 @@ runNameIdGenArtifacts ::
runNameIdGenArtifacts = runStateLikeArtifacts runNameIdGen artifactNameIdState

readerFunctionsTableArtifacts :: (Members '[State Artifacts] r) => Sem (Reader FunctionsTable ': r) a -> Sem r a
readerFunctionsTableArtifacts = runReaderArtifacts artifactFunctions
readerFunctionsTableArtifacts = runReaderArtifacts (artifactTypeCheckingTables . typeCheckingTablesFunctionsTable)

readerTypesTableArtifacts :: (Members '[State Artifacts] r) => Sem (Reader TypesTable ': r) a -> Sem r a
readerTypesTableArtifacts = runReaderArtifacts artifactTypes
readerTypesTableArtifacts = runReaderArtifacts (artifactTypeCheckingTables . typeCheckingTablesTypesTable)

runTerminationArtifacts :: (Members '[Error JuvixError, State Artifacts] r) => Sem (Termination ': r) a -> Sem r a
runTerminationArtifacts = runStateLikeArtifacts runTermination artifactTerminationState
Expand All @@ -99,20 +99,8 @@ runStateLikeArtifacts runner l m = do

runResultBuilderArtifacts :: forall r a. (Members '[State Artifacts] r) => Sem (ResultBuilder ': r) a -> Sem r a
runResultBuilderArtifacts m = do
ftab <- gets (^. artifactFunctions)
ttab <- gets (^. artifactTypes)
itab <- gets (^. artifactInstances)
ctab <- gets (^. artifactCoercions)
let importCtx =
ImportContext
{ _importContextCoercions = ctab,
_importContextInstances = itab,
_importContextFunctionsTable = ftab,
_importContextTypesTable = ttab
}
tabs <- gets (^. artifactTypeCheckingTables)
let importCtx = ImportContext tabs
(s, a) <- runResultBuilder importCtx m
modify' (set artifactFunctions (s ^. resultBuilderStateCombinedFunctionsTable))
modify' (set artifactTypes (s ^. resultBuilderStateCombinedTypesTable))
modify' (set artifactInstances (s ^. resultBuilderStateCombinedInstanceTable))
modify' (set artifactCoercions (s ^. resultBuilderStateCombinedCoercionTable))
modify' (set artifactTypeCheckingTables (s ^. resultBuilderStateCombinedTables))
return a
9 changes: 2 additions & 7 deletions src/Juvix/Compiler/Pipeline/Artifacts/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,8 @@ import Juvix.Compiler.Concrete.Translation.FromSource.Data.ParserState
import Juvix.Compiler.Core.Data.Module qualified as Core
import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
import Juvix.Compiler.Pipeline.Loader.PathResolver.Data
import Juvix.Compiler.Store.Internal.Data.CoercionInfo
import Juvix.Compiler.Store.Internal.Data.InstanceInfo
import Juvix.Compiler.Store.Internal.Data.TypeCheckingTables
import Juvix.Compiler.Store.Language qualified as Store
import Juvix.Prelude

Expand All @@ -27,10 +25,7 @@ data Artifacts = Artifacts
-- Concrete -> Internal
_artifactTerminationState :: TerminationState,
-- Typechecking
_artifactTypes :: TypesTable,
_artifactFunctions :: FunctionsTable,
_artifactInstances :: InstanceTable,
_artifactCoercions :: CoercionTable,
_artifactTypeCheckingTables :: TypeCheckingTables,
-- | This includes the InfoTable from all type checked modules
_artifactInternalTypedTable :: Internal.InfoTable,
-- Core
Expand Down
23 changes: 4 additions & 19 deletions src/Juvix/Compiler/Pipeline/Run.hs
Original file line number Diff line number Diff line change
Expand Up @@ -246,17 +246,8 @@ runReplPipelineIOEither' lockMode entry = do
_pipelineResult
^. Core.coreResultInternalTypedResult

typesTable :: Typed.TypesTable
typesTable = typedResult ^. Typed.resultIdenTypes

functionsTable :: Typed.FunctionsTable
functionsTable = typedResult ^. Typed.resultFunctions

instanceTable :: Typed.InstanceTable
instanceTable = typedResult ^. Typed.resultInstances

coercionTable :: Typed.CoercionTable
coercionTable = typedResult ^. Typed.resultCoercions
typesTable :: Typed.TypeCheckingTables
typesTable = typedResult ^. Typed.resultTypeCheckingTables

typedTable :: Internal.InfoTable
typedTable = typedResult ^. Typed.resultInternalModule . Typed.internalModuleInfoTable
Expand Down Expand Up @@ -289,10 +280,7 @@ runReplPipelineIOEither' lockMode entry = do
_artifactCoreModule = coreModule,
_artifactScopeTable = resultScoperTable,
_artifactScopeExports = scopedResult ^. Scoped.resultExports,
_artifactTypes = typesTable,
_artifactFunctions = functionsTable,
_artifactInstances = instanceTable,
_artifactCoercions = coercionTable,
_artifactTypeCheckingTables = typesTable,
_artifactScoperState = scopedResult ^. Scoped.resultScoperState,
_artifactResolver = art ^. artifactResolver,
_artifactNameIdState = art ^. artifactNameIdState,
Expand All @@ -308,10 +296,7 @@ runReplPipelineIOEither' lockMode entry = do
_artifactTerminationState = iniTerminationState,
_artifactResolver = iniResolverState,
_artifactNameIdState = genNameIdState defaultModuleId,
_artifactTypes = mempty,
_artifactFunctions = mempty,
_artifactInstances = mempty,
_artifactCoercions = mempty,
_artifactTypeCheckingTables = mempty,
_artifactCoreModule = Core.emptyModule,
_artifactScopeTable = mempty,
_artifactScopeExports = mempty,
Expand Down
Loading
Loading