Add TopDef property for specs

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

@@ -44,12 +44,23 @@ buildProperties HighlightInput {..} =
           <> mapMaybe goFaceName _highlightNames
           <> map goFaceError _highlightErrors,
       _propertiesGoto = map goGotoProperty _highlightNames,
+      _propertiesTopDef = nubHashable (mapMaybe goDefProperty _highlightNames),
       _propertiesInfo = mapMaybe (goDocProperty _highlightDocTable _highlightTypes) _highlightNames
     }
 
 goFaceError :: Interval -> WithLoc PropertyFace
 goFaceError i = WithLoc i (PropertyFace FaceError)
 
+goDefProperty :: AName -> Maybe (WithLoc PropertyTopDef)
+goDefProperty n = do
+  guard (n ^. anameIsTop)
+  guard ((n ^. anameLoc) == (n ^. anameDefinedLoc))
+  return
+    WithLoc
+      { _withLocInt = n ^. anameLoc,
+        _withLocParam = PropertyTopDef (n ^. anameVerbatim)
+      }
+
 goFaceSemanticItem :: SemanticItem -> Maybe (WithLoc PropertyFace)
 goFaceSemanticItem i = WithLoc (getLoc i) . PropertyFace <$> f
   where

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

@@ -15,8 +15,8 @@ data InfoTableBuilder :: Effect where
   RegisterConstructor :: ConstructorDef 'Scoped -> InfoTableBuilder m ()
   RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m ()
   RegisterFunctionDef :: FunctionDef 'Scoped -> InfoTableBuilder m ()
-  RegisterName :: (HasLoc c) => S.Name' c -> InfoTableBuilder m ()
-  RegisterScopedIden :: ScopedIden -> InfoTableBuilder m ()
+  RegisterName :: (HasLoc c) => Bool -> S.Name' c -> InfoTableBuilder m ()
+  RegisterScopedIden :: Bool -> ScopedIden -> InfoTableBuilder m ()
   RegisterModuleDoc :: S.NameId -> Maybe (Judoc 'Scoped) -> InfoTableBuilder m ()
   RegisterFixity :: FixityDef -> InfoTableBuilder m ()
   RegisterPrecedence :: S.NameId -> S.NameId -> InfoTableBuilder m ()
@@ -65,8 +65,8 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case
         fid = f ^. functionDefName . functionDefNameScoped . nameId
     modify' (over infoFunctions (HashMap.insert fid f))
     highlightDoc fid j
-  RegisterName n -> highlightName (S.anameFromName n)
-  RegisterScopedIden n -> highlightName (anameFromScopedIden n)
+  RegisterName isTop n -> highlightName (S.anameFromName isTop n)
+  RegisterScopedIden isTop n -> highlightName (anameFromScopedIden isTop n)
   RegisterModuleDoc uid doc -> highlightDoc uid doc
   RegisterFixity f -> do
     let sid = f ^. fixityDefSymbol . S.nameId
@@ -143,10 +143,11 @@ runInfoTableBuilderRepl tab = ignoreHighlightBuilder . runInfoTableBuilder tab .
 ignoreInfoTableBuilder :: (Members '[Error ScoperError, HighlightBuilder] r) => Sem (InfoTableBuilder ': r) a -> Sem r a
 ignoreInfoTableBuilder = fmap snd . runInfoTableBuilder mempty
 
-anameFromScopedIden :: ScopedIden -> AName
-anameFromScopedIden s =
+anameFromScopedIden :: Bool -> ScopedIden -> AName
+anameFromScopedIden isTop s =
   AName
     { _anameLoc = getLoc s,
+      _anameIsTop = isTop,
       _anameKindPretty = getNameKindPretty s,
       _anameDocId = s ^. scopedIdenFinal . nameId,
       _anameDefinedLoc = s ^. scopedIdenSrcName . nameDefined,

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

@@ -106,6 +106,7 @@ data AName = AName
   { _anameLoc :: Interval,
     _anameDefinedLoc :: Interval,
     _anameKindPretty :: NameKind,
+    _anameIsTop :: Bool,
     _anameDocId :: NameId,
     _anameVerbatim :: Text
   }
@@ -118,13 +119,14 @@ instance NFData AName
 makeLenses ''Name'
 makeLenses ''AName
 
-anameFromName :: (HasLoc c) => Name' c -> AName
-anameFromName n =
+anameFromName :: (HasLoc c) => Bool -> Name' c -> AName
+anameFromName isTop n =
   AName
     { _anameLoc = getLoc n,
       _anameDefinedLoc = n ^. nameDefined,
       _anameKindPretty = getNameKindPretty n,
       _anameDocId = n ^. nameId,
+      _anameIsTop = isTop,
       _anameVerbatim = n ^. nameVerbatim
     }
 

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -283,7 +283,10 @@ reserveSymbolOfNameSpace ns kind kindPretty nameSig builtin s = do
   whenJust nameSig (modify' . set (scoperNameSignatures . at (s' ^. S.nameId)) . Just)
   whenJust nameSig (registerParsedNameSig (s' ^. S.nameId))
   modify (set (scopeNameSpaceLocal sns . at s) (Just s'))
-  registerName s'
+  let isTop = case strat of
+        BindingLocal -> False
+        BindingTop -> True
+  registerName isTop s'
   let u = S.unqualifiedSymbol s'
       entry :: NameSpaceEntryType ns
       entry =
@@ -643,8 +646,8 @@ checkImportNoPublic import_@Import {..} = do
       qual' = do
         asName <- _importAsName
         return (set S.nameConcrete asName sname')
-  registerName importName
-  whenJust synonymName registerName
+  registerName False importName
+  whenJust synonymName (registerName False)
   registerScoperModules scopedModule
   importOpen' <- mapM (checkOpenModuleShort scopedModule) _importOpen
   usingHiding' <- mapM (checkUsingHiding importName exportInfoOriginal) _importUsingHiding
@@ -851,7 +854,7 @@ entryToScopedIden name e = do
           { _scopedIdenAlias = Just scopedName',
             _scopedIdenFinal = helper (e' ^. symbolEntry)
           }
-  registerScopedIden si
+  registerScopedIden False si
   return si
 
 -- | We gather all symbols which have been defined or marked to be public in the given scope.
@@ -1490,7 +1493,7 @@ checkTopModule m@Module {..} = checkedModule
           _nameIterator :: Maybe IteratorInfo
           _nameIterator = Nothing
           moduleName = S.Name' {..}
-      registerName moduleName
+      registerName True moduleName
       return moduleName
 
     iniScope :: Scope
@@ -2005,7 +2008,7 @@ checkLocalModule md@Module {..} = do
           }
   modify (over scoperModules (HashMap.insert mid smod))
   registerLocalModule smod
-  registerName _modulePath'
+  registerName True _modulePath'
   return m
   where
     inheritScope :: (Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, Reader BindingStrategy] r') => Sem r' ()
@@ -2109,7 +2112,7 @@ checkUsingHiding modulepath exportInfo = \case
                 }
       entry <- maybe err return mentry
       let scopedSym = entryToSymbol entry s
-      registerName scopedSym
+      registerName False scopedSym
       return scopedSym
 
     checkHidingList :: HidingList 'Parsed -> Sem r (HidingList 'Scoped)
@@ -2155,7 +2158,7 @@ checkUsingHiding modulepath exportInfo = \case
       let scopedAs = do
             c <- i ^. usingAs
             return (set S.nameConcrete c scopedSym)
-      mapM_ registerName scopedAs
+      mapM_ (registerName False) scopedAs
       return
         UsingItem
           { _usingSymbol = scopedSym,
@@ -2172,7 +2175,7 @@ checkOpenModuleHelper ::
   Sem r (OpenModule 'Scoped short)
 checkOpenModuleHelper openedModule OpenModule {..} = do
   let exportInfo = openedModule ^. scopedModuleExportInfo
-  registerName (openedModule ^. scopedModuleName)
+  registerName False (openedModule ^. scopedModuleName)
   usingHiding' <- mapM (checkUsingHiding (openedModule ^. scopedModulePath) exportInfo) _openModuleUsingHiding
   mergeScope (filterExportInfo _openModulePublic usingHiding' exportInfo)
   let openName :: OpenModuleNameType 'Scoped short = case sing :: SIsOpenShort short of
@@ -2709,7 +2712,7 @@ checkFixitySymbol s = do
     [] -> throw (ErrSymNotInScope (NotInScope s scope))
     [x] -> do
       let res = entryToSymbol x s
-      registerName res
+      registerName False res
       return res
     es -> throw (ErrAmbiguousSym (AmbiguousSym n (map (PreSymbolFinal . SymbolEntry . (^. fixityEntry)) es)))
   where

src/Juvix/Compiler/Nockma/Highlight.hs

@@ -25,6 +25,7 @@ buildProperties HighlightInput {..} =
         mapMaybe goFaceSemanticItem _highlightSemanticItems
           <> map goFaceError _highlightErrors,
       _propertiesGoto = [],
+      _propertiesTopDef = [],
       _propertiesInfo = map goInfoNockOp _highlightNockOps <> map goInfoPath _highlightPaths
     }
 

src/Juvix/Emacs/Properties.hs

@@ -88,6 +88,14 @@ data PropertyGoto = PropertyGoto
     _gotoPos :: FileLoc
   }
 
+-- | Location where a top symbol is defined
+newtype PropertyTopDef = PropertyTopDef
+  { _topDef :: Text
+  }
+  deriving stock (Eq, Generic)
+
+instance Hashable PropertyTopDef
+
 newtype PropertyFace = PropertyFace
   { _faceFace :: Face
   }
@@ -100,13 +108,15 @@ data PropertyInfo = PropertyInfo
 data LocProperties = LocProperties
   { _propertiesGoto :: [WithLoc PropertyGoto],
     _propertiesFace :: [WithLoc PropertyFace],
+    _propertiesTopDef :: [WithLoc PropertyTopDef],
     _propertiesInfo :: [WithLoc PropertyInfo]
   }
 
 data RawProperties = RawProperties
   { _rawPropertiesFace :: [RawWithLoc RawFace],
     _rawPropertiesGoto :: [RawWithLoc RawGoto],
-    _rawPropertiesDoc :: [RawWithLoc RawType]
+    _rawPropertiesDoc :: [RawWithLoc RawType],
+    _rawPropertiesTopDef :: [RawWithLoc RawTopDef]
   }
 
 -- | (File, Start Row, Start Col, Length, End Row, End Col)
@@ -119,6 +129,8 @@ type RawFace = Face
 -- | (TargetFile, TargetLine, TargetColumn)
 type RawGoto = (Path Abs File, Int, Int)
 
+type RawTopDef = Text
+
 -- | (Type)
 type RawType = Text
 
@@ -135,6 +147,7 @@ rawProperties LocProperties {..} =
   RawProperties
     { _rawPropertiesGoto = map (rawWithLoc rawGoto) _propertiesGoto,
       _rawPropertiesFace = map (rawWithLoc rawFace) _propertiesFace,
+      _rawPropertiesTopDef = map (rawWithLoc rawTopDef) _propertiesTopDef,
       _rawPropertiesDoc = map (rawWithLoc rawType) _propertiesInfo
     }
   where
@@ -160,6 +173,9 @@ rawProperties LocProperties {..} =
     rawFace :: PropertyFace -> RawFace
     rawFace PropertyFace {..} = _faceFace
 
+    rawTopDef :: PropertyTopDef -> RawTopDef
+    rawTopDef PropertyTopDef {..} = _topDef
+
     rawGoto :: PropertyGoto -> RawGoto
     rawGoto PropertyGoto {..} =
       ( _gotoFile,