Skip to content

Commit

Permalink
wip internal
Browse files Browse the repository at this point in the history
  • Loading branch information
lukaszcz committed Nov 8, 2023
1 parent bee4360 commit fd74b94
Show file tree
Hide file tree
Showing 12 changed files with 65 additions and 137 deletions.
36 changes: 22 additions & 14 deletions src/Juvix/Compiler/Internal/Data/InfoTable.hs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module Juvix.Compiler.Internal.Data.InfoTable
( module Juvix.Compiler.Store.Internal.Language,
buildTable,
buildInfoTable,
extendWithReplExpression,
lookupConstructor,
lookupConstructorArgTypes,
Expand All @@ -13,6 +14,8 @@ module Juvix.Compiler.Internal.Data.InfoTable
getAxiomBuiltinInfo,
getFunctionBuiltinInfo,
mkConstructorEntries,
functionInfoFromFunctionDef,
inductiveInfoFromInductiveDef,
)
where

Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
30 changes: 12 additions & 18 deletions src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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 {..}
Expand Down Expand Up @@ -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) =>
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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 ::
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ newtype ModulesCache = ModulesCache

data InternalResult = InternalResult
{ _resultScoper :: Concrete.ScoperResult,
_resultTable :: InfoTable,
_resultTable :: StoredModuleTable,
_resultModules :: NonEmpty Module,
_resultDepInfo :: NameDependencyInfo,
_resultModulesCache :: ModulesCache
Expand Down
32 changes: 17 additions & 15 deletions src/Juvix/Compiler/Internal/Translation/FromInternal.hs
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
module Juvix.Compiler.Internal.Translation.FromInternal
( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability,
arityChecking,
( arityChecking,
typeChecking,
typeCheckExpression,
typeCheckExpressionType,
Expand All @@ -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
Expand All @@ -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) =>
Expand All @@ -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.
Expand Down Expand Up @@ -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
Expand All @@ -114,6 +115,7 @@ typeCheckImport i = do
-- TODO Store cache in Artifacts and use it here
. evalCacheEmpty checkModuleNoCache
$ checkTable >> checkImport i
-}

typeChecking ::
forall r.
Expand All @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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) =>
Expand Down Expand Up @@ -127,7 +124,7 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
_inductiveTrait,
_inductivePragmas
}
checkPositivity d
checkPositivity (inductiveInfoFromInductiveDef d)
return d
where
paramLocals :: LocalVars
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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))
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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) =>
Expand Down
Loading

0 comments on commit fd74b94

Please sign in to comment.