Skip to content

Commit

Permalink
Group tables related to typechecking (#3056)
Browse files Browse the repository at this point in the history
I've grouped tables related to typechecking:
```
data TypeCheckingTables = TypeCheckingTables
  { _typeCheckingTablesTypesTable :: TypesTable,
    _typeCheckingTablesFunctionsTable :: FunctionsTable,
    _typeCheckingTablesInstanceTable :: InstanceTable,
    _typeCheckingTablesCoercionTable :: CoercionTable
  }
```
  • Loading branch information
janmasrovira authored Sep 25, 2024
1 parent 49e8c9d commit 7ae42a1
Show file tree
Hide file tree
Showing 14 changed files with 172 additions and 164 deletions.
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

0 comments on commit 7ae42a1

Please sign in to comment.