wip internal

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

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 ::

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

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

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

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

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

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))

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) =>