Separate modules namespace (#2257)

app/Commands/Repl.hs

@@ -251,12 +251,15 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers
 
         printIdentifier :: Concrete.ScopedIden -> Repl ()
         printIdentifier s = do
-          mdoc <- case s of
-            Concrete.ScopedAxiom a -> getDocAxiom (a ^. Scoped.nameId)
-            Concrete.ScopedInductive a -> getDocInductive (a ^. Scoped.nameId)
-            Concrete.ScopedVar {} -> return Nothing
-            Concrete.ScopedFunction f -> getDocFunction (f ^. Scoped.nameId)
-            Concrete.ScopedConstructor c -> getDocConstructor (c ^. Scoped.nameId)
+          let n = s ^. Concrete.scopedIden . Scoped.nameId
+          mdoc <- case getNameKind s of
+            KNameAxiom -> getDocAxiom n
+            KNameInductive -> getDocInductive n
+            KNameLocal -> return Nothing
+            KNameFunction -> getDocFunction n
+            KNameConstructor -> getDocConstructor n
+            KNameLocalModule -> impossible
+            KNameTopModule -> impossible
           printDoc mdoc
           where
             printDoc :: Maybe (Concrete.Judoc 'Concrete.Scoped) -> Repl ()
@@ -303,13 +306,16 @@ printDefinition = replParseIdentifiers >=> printIdentifiers
         getInfoTable = (^. replContextArtifacts . artifactScopeTable) <$> replGetContext
 
         printIdentifier :: Concrete.ScopedIden -> Repl ()
-        printIdentifier s = do
-          case s of
-            Concrete.ScopedAxiom a -> printAxiom (a ^. Scoped.nameId)
-            Concrete.ScopedInductive a -> printInductive (a ^. Scoped.nameId)
-            Concrete.ScopedVar {} -> return ()
-            Concrete.ScopedFunction f -> printFunction (f ^. Scoped.nameId)
-            Concrete.ScopedConstructor c -> printConstructor (c ^. Scoped.nameId)
+        printIdentifier s =
+          let n = s ^. Concrete.scopedIden . Scoped.nameId
+           in case getNameKind s of
+                KNameAxiom -> printAxiom n
+                KNameInductive -> printInductive n
+                KNameLocal -> return ()
+                KNameFunction -> printFunction n
+                KNameConstructor -> printConstructor n
+                KNameLocalModule -> impossible
+                KNameTopModule -> impossible
           where
             printLocation :: HasLoc s => s -> Repl ()
             printLocation def = do

src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs

@@ -15,7 +15,7 @@ data InfoTableBuilder m a where
   RegisterTypeSignature :: TypeSignature 'Scoped -> InfoTableBuilder m ()
   RegisterFunctionDef :: FunctionDef 'Scoped -> InfoTableBuilder m ()
   RegisterFunctionClause :: FunctionClause 'Scoped -> InfoTableBuilder m ()
-  RegisterName :: (HasLoc c) => S.Name' c -> InfoTableBuilder m ()
+  RegisterName :: HasLoc c => S.Name' c -> InfoTableBuilder m ()
   RegisterModule :: Module 'Scoped 'ModuleTop -> InfoTableBuilder m ()
 
 makeSem ''InfoTableBuilder

src/Juvix/Compiler/Concrete/Data/NameSpace.hs

@@ -0,0 +1,27 @@
+module Juvix.Compiler.Concrete.Data.NameSpace where
+
+import Data.Kind qualified as GHC
+import Juvix.Data.NameKind
+import Juvix.Prelude
+
+data NameSpace
+  = NameSpaceSymbols
+  | NameSpaceModules
+  deriving stock (Eq, Generic, Enum, Bounded, Show, Ord)
+
+instance Hashable NameSpace
+
+type AnyNameSpace (k :: NameSpace -> GHC.Type) =
+  Σ NameSpace (TyCon1 k)
+
+$(genSingletons [''NameSpace])
+
+type NameKindNameSpace :: NameKind -> NameSpace
+type family NameKindNameSpace s = res where
+  NameKindNameSpace 'KNameLocal = 'NameSpaceSymbols
+  NameKindNameSpace 'KNameConstructor = 'NameSpaceSymbols
+  NameKindNameSpace 'KNameInductive = 'NameSpaceSymbols
+  NameKindNameSpace 'KNameFunction = 'NameSpaceSymbols
+  NameKindNameSpace 'KNameAxiom = 'NameSpaceSymbols
+  NameKindNameSpace 'KNameLocalModule = 'NameSpaceModules
+  NameKindNameSpace 'KNameTopModule = 'NameSpaceModules

src/Juvix/Compiler/Concrete/Data/Scope.hs

@@ -1,24 +1,31 @@
 module Juvix.Compiler.Concrete.Data.Scope
   ( module Juvix.Compiler.Concrete.Data.Scope,
     module Juvix.Compiler.Concrete.Data.InfoTable,
+    module Juvix.Compiler.Concrete.Data.NameSpace,
   )
 where
 
 import Juvix.Compiler.Concrete.Data.InfoTable
 import Juvix.Compiler.Concrete.Data.NameSignature.Base
+import Juvix.Compiler.Concrete.Data.NameSpace
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language
 import Juvix.Prelude
 
 type LocalVariable = S.Symbol
 
-newtype SymbolInfo = SymbolInfo
+newtype SymbolInfo (n :: NameSpace) = SymbolInfo
   { -- | This map must have at least one entry. If there are more than one
     -- entry, it means that the same symbol has been brought into scope from two
     -- different places
-    _symbolInfo :: HashMap S.AbsModulePath SymbolEntry
+    _symbolInfo :: HashMap S.AbsModulePath (NameSpaceEntryType n)
   }
-  deriving newtype (Show, Semigroup, Monoid)
+  deriving newtype (Semigroup, Monoid)
+
+nsEntry :: forall ns. SingI ns => Lens' (NameSpaceEntryType ns) (S.Name' ())
+nsEntry = case sing :: SNameSpace ns of
+  SNameSpaceModules -> moduleEntry
+  SNameSpaceSymbols -> symbolEntry
 
 mkModuleRef' :: SingI t => ModuleRef'' 'S.NotConcrete t -> ModuleRef' 'S.NotConcrete
 mkModuleRef' m = ModuleRef' (sing :&: m)
@@ -31,7 +38,8 @@ data BindingStrategy
 
 data Scope = Scope
   { _scopePath :: S.AbsModulePath,
-    _scopeSymbols :: HashMap Symbol SymbolInfo,
+    _scopeSymbols :: HashMap Symbol (SymbolInfo 'NameSpaceSymbols),
+    _scopeModuleSymbols :: HashMap Symbol (SymbolInfo 'NameSpaceModules),
     -- | The map from S.NameId to Modules is needed because we support merging
     -- several imports under the same name. E.g.
     -- import A as X;
@@ -41,14 +49,23 @@ data Scope = Scope
     -- should map to itself. This is needed because we may query it with a
     -- symbol with a different location but we may want the location of the
     -- original symbol
-    _scopeLocalSymbols :: HashMap Symbol S.Symbol
+    _scopeLocalSymbols :: HashMap Symbol S.Symbol,
+    _scopeLocalModuleSymbols :: HashMap Symbol S.Symbol
   }
-  deriving stock (Show)
 
-makeLenses ''ExportInfo
 makeLenses ''SymbolInfo
 makeLenses ''Scope
 
+scopeNameSpace :: forall (ns :: NameSpace). SingI ns => Lens' Scope (HashMap Symbol (SymbolInfo ns))
+scopeNameSpace = case sing :: SNameSpace ns of
+  SNameSpaceSymbols -> scopeSymbols
+  SNameSpaceModules -> scopeModuleSymbols
+
+scopeNameSpaceLocal :: forall (ns :: NameSpace). Sing ns -> Lens' Scope (HashMap Symbol S.Symbol)
+scopeNameSpaceLocal s = case s of
+  SNameSpaceSymbols -> scopeLocalSymbols
+  SNameSpaceModules -> scopeLocalModuleSymbols
+
 newtype ModulesCache = ModulesCache
   { _cachedModules :: HashMap TopModulePath (ModuleRef'' 'S.NotConcrete 'ModuleTop)
   }
@@ -65,6 +82,7 @@ makeLenses ''ScopeParameters
 
 data ScoperState = ScoperState
   { _scoperModulesCache :: ModulesCache,
+    -- | Local and top modules
     _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete),
     _scoperScope :: HashMap TopModulePath Scope,
     _scoperSignatures :: HashMap S.NameId NameSignature
@@ -104,6 +122,8 @@ emptyScope absPath =
   Scope
     { _scopePath = absPath,
       _scopeSymbols = mempty,
+      _scopeModuleSymbols = mempty,
       _scopeTopModules = mempty,
-      _scopeLocalSymbols = mempty
+      _scopeLocalSymbols = mempty,
+      _scopeLocalModuleSymbols = mempty
     }

src/Juvix/Compiler/Concrete/Data/ScopedName.hs

@@ -112,8 +112,11 @@ isConstructor n = case n ^. nameKind of
 fromQualifiedName :: C.QualifiedName -> C.Symbol
 fromQualifiedName (C.QualifiedName _ s) = s
 
-topModulePathName :: TopModulePath -> Symbol
-topModulePathName = over nameConcrete (^. C.modulePathName)
+topModulePathSymbol :: TopModulePath -> Symbol
+topModulePathSymbol = over nameConcrete (^. C.modulePathName)
+
+topModulePathName :: TopModulePath -> Name
+topModulePathName = over nameConcrete C.topModulePathToName
 
 unConcrete :: Name' a -> Name' ()
 unConcrete = set nameConcrete ()