fix highlighting

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

@@ -29,10 +29,12 @@ data InfoTableBuilder m a where
 
 makeSem ''InfoTableBuilder
 
-registerDoc :: forall r. (Member (State InfoTable) r) => NameId -> Maybe (Judoc 'Scoped) -> Sem r ()
-registerDoc k md = modify (set (infoHighlightDoc . at k) md)
+registerDoc :: forall r. (Members '[HighlightBuilder, State InfoTable] r) => NameId -> Maybe (Judoc 'Scoped) -> Sem r ()
+registerDoc k md = do
+  modify (set (highlightDoc . at k) md)
+  modify (set (infoHighlightDoc . at k) md)
 
-toState :: Sem (InfoTableBuilder ': r) a -> Sem (State InfoTable ': r) a
+toState :: (Member HighlightBuilder r) => Sem (InfoTableBuilder ': r) a -> Sem (State InfoTable ': r) a
 toState = reinterpret $ \case
   RegisterAxiom d ->
     let j = d ^. axiomDoc
@@ -54,8 +56,12 @@ toState = reinterpret $ \case
      in do
           modify' (over infoFunctions (HashMap.insert (f ^. signName . nameId) f))
           registerDoc (f ^. signName . nameId) j
-  RegisterName n -> modify (over infoHighlightNames (cons (S.anameFromName n)))
-  RegisterScopedIden n -> modify (over infoHighlightNames (cons (anameFromScopedIden n)))
+  RegisterName n -> do
+    modify (over highlightNames (cons (S.anameFromName n)))
+    modify (over infoHighlightNames (cons (S.anameFromName n)))
+  RegisterScopedIden n -> do
+    modify (over highlightNames (cons (anameFromScopedIden n)))
+    modify (over infoHighlightNames (cons (anameFromScopedIden n)))
   RegisterModuleDoc uid doc -> do
     registerDoc uid doc
   RegisterFixity f -> do
@@ -84,10 +90,10 @@ toState = reinterpret $ \case
 runInfoTableBuilderRepl :: InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
 runInfoTableBuilderRepl tab = ignoreHighlightBuilder . runInfoTableBuilder tab . raiseUnder
 
-runInfoTableBuilder :: InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
+runInfoTableBuilder :: (Member HighlightBuilder r) => InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
 runInfoTableBuilder tab = runState tab . toState
 
-ignoreInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r a
+ignoreInfoTableBuilder :: (Member HighlightBuilder r) => Sem (InfoTableBuilder ': r) a -> Sem r a
 ignoreInfoTableBuilder = evalState mempty . toState
 
 anameFromScopedIden :: ScopedIden -> AName

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

@@ -5,6 +5,7 @@ module Juvix.Compiler.Concrete.Translation.FromParsed
   )
 where
 
+import Juvix.Compiler.Concrete.Data.Highlight
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context
@@ -15,7 +16,7 @@ import Juvix.Compiler.Store.Language
 import Juvix.Prelude
 
 fromParsed ::
-  (Members '[Reader EntryPoint, Reader ModuleTable, Reader Parsed.ParserResult, Error JuvixError, NameIdGen] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Reader ModuleTable, Reader Parsed.ParserResult, Error JuvixError, NameIdGen] r) =>
   Sem r ScoperResult
 fromParsed = do
   e <- ask

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -14,6 +14,7 @@ import Data.Text qualified as Text
 import Juvix.Compiler.Backend.Markdown.Data.Types (Mk (..))
 import Juvix.Compiler.Backend.Markdown.Data.Types qualified as MK
 import Juvix.Compiler.Backend.Markdown.Error
+import Juvix.Compiler.Concrete (HighlightBuilder, ignoreHighlightBuilder)
 import Juvix.Compiler.Concrete.Extra (takeWhile1P)
 import Juvix.Compiler.Concrete.Extra qualified as P
 import Juvix.Compiler.Concrete.Language
@@ -49,7 +50,7 @@ type JudocStash = State (Maybe (Judoc 'Parsed))
 type PragmasStash = State (Maybe ParsedPragmas)
 
 fromSource ::
-  (Members '[Files, PathResolver, Error JuvixError] r) =>
+  (Members '[HighlightBuilder, Files, PathResolver, Error JuvixError] r) =>
   EntryPoint ->
   Sem r ParserResult
 fromSource e = mapError (JuvixError @ParserError) $ do
@@ -269,9 +270,10 @@ runExpressionParser ::
   Sem r (Either ParserError (ExpressionAtoms 'Parsed))
 runExpressionParser fpath input = do
   m <-
-    runParserResultBuilder mempty
-      . evalState (Nothing @ParsedPragmas)
-      . evalState (Nothing @(Judoc 'Parsed))
+    ignoreHighlightBuilder
+      $ runParserResultBuilder mempty
+        . evalState (Nothing @ParsedPragmas)
+        . evalState (Nothing @(Judoc 'Parsed))
       $ P.runParserT parseExpressionAtoms (toFilePath fpath) input
   case m of
     (_, Left err) -> return (Left (ErrMegaparsec (MegaparsecError err)))

src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs

@@ -68,13 +68,15 @@ registerLiteral l =
 registerItem' :: (Member (State ParserState) r) => ParsedItem -> Sem r ()
 registerItem' i = modify' (over parserStateParsedItems (i :))
 
-runParserResultBuilder :: ParserState -> Sem (ParserResultBuilder ': r) a -> Sem r (ParserState, a)
+runParserResultBuilder :: (Member HighlightBuilder r) => ParserState -> Sem (ParserResultBuilder ': r) a -> Sem r (ParserState, a)
 runParserResultBuilder s =
   runState s
     . reinterpret
       ( \case
           RegisterImport i -> modify' (over parserStateImports (i :))
-          RegisterItem i -> registerItem' i
+          RegisterItem i -> do
+            modify' (over highlightParsed (i :))
+            registerItem' i
           RegisterSpaceSpan g -> do
             modify' (over parserStateComments (g :))
             forM_ (g ^.. spaceSpan . each . _SpaceComment) $ \c ->

src/Juvix/Compiler/Internal/Translation/FromInternal.hs

@@ -26,6 +26,7 @@ typeCheckExpressionType ::
   Expression ->
   Sem r TypedExpression
 typeCheckExpressionType exp = do
+  -- TODO: refactor: modules outside of REPL should not refer to Artifacts
   table <- extendedTableReplArtifacts exp
   runTypesTableArtifacts
     . runFunctionsTableArtifacts
@@ -52,7 +53,7 @@ typeCheckImport = return
 
 typeCheckingNew ::
   forall r.
-  (Members '[Reader EntryPoint, Error JuvixError, NameIdGen, Reader ModuleTable] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Error JuvixError, NameIdGen, Reader ModuleTable] r) =>
   Sem (Termination ': r) InternalResult ->
   Sem r InternalTypedResult
 typeCheckingNew a = do

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs

@@ -12,6 +12,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Builtins.Error (NotDefined (..))
+import Juvix.Compiler.Concrete.Data.Highlight
 import Juvix.Compiler.Internal.Data.Cast
 import Juvix.Compiler.Internal.Data.CoercionInfo
 import Juvix.Compiler.Internal.Data.InstanceInfo
@@ -103,14 +104,15 @@ instance HasExpressions AppBuilderArg where
           _appBuilderArgIsDefault
         }
 
-registerConstructor :: (Members '[State TypesTable, Reader InfoTable] r) => ConstructorDef -> Sem r ()
+registerConstructor :: (Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r) => ConstructorDef -> Sem r ()
 registerConstructor ctr = do
   ty <- lookupConstructorType (ctr ^. inductiveConstructorName)
   registerNameIdType (ctr ^. inductiveConstructorName . nameId) ty
 
-registerNameIdType :: (Members '[State TypesTable, Reader InfoTable] r) => NameId -> Expression -> Sem r ()
+registerNameIdType :: (Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r) => NameId -> Expression -> Sem r ()
 registerNameIdType uid ty = do
   modify (over typesTable (HashMap.insert uid ty))
+  modify (over (highlightTypes . typesTable) (HashMap.insert uid ty))
 
 checkTable ::
   (Members '[Reader InfoTable, Error TypeCheckerError] r) =>
@@ -124,7 +126,7 @@ checkTable = do
       . CoercionCycles
 
 checkModule ::
-  (Members '[Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Termination] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Termination] r) =>
   Module ->
   Sem r Module
 checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do
@@ -143,7 +145,7 @@ checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do
       }
 
 checkModuleBody ::
-  (Members '[Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Termination, Reader InsertedArgsStack] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Termination, Reader InsertedArgsStack] r) =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -159,14 +161,14 @@ checkImport :: Import -> Sem r Import
 checkImport = return
 
 checkMutualBlock ::
-  (Members '[Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Termination, Reader InsertedArgsStack] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Termination, Reader InsertedArgsStack] r) =>
   MutualBlock ->
   Sem r MutualBlock
 checkMutualBlock s = runReader emptyLocalVars (checkTopMutualBlock s)
 
 checkInductiveDef ::
   forall r.
-  (Members '[Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) =>
   InductiveDef ->
   Sem r InductiveDef
 checkInductiveDef InductiveDef {..} = runInferenceDef $ do
@@ -232,7 +234,7 @@ withEmptyVars :: Sem (Reader LocalVars ': r) a -> Sem r a
 withEmptyVars = runReader emptyLocalVars
 
 checkTopMutualBlock ::
-  (Members '[State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Termination, Reader InsertedArgsStack] r) =>
+  (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Termination, Reader InsertedArgsStack] r) =>
   MutualBlock ->
   Sem r MutualBlock
 checkTopMutualBlock (MutualBlock ds) =
@@ -269,7 +271,7 @@ resolveCastHoles s = do
     getNatTy = mkBuiltinInductive BuiltinNat
 
 checkMutualStatement ::
-  (Members '[State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Termination, Reader InsertedArgsStack] r) =>
+  (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Termination, Reader InsertedArgsStack] r) =>
   MutualStatement ->
   Sem r MutualStatement
 checkMutualStatement = \case

src/Juvix/Compiler/Pipeline.hs

@@ -53,7 +53,7 @@ type PipelineEff r = Reader Parser.ParserResult ': Reader Store.ModuleTable ': N
 --------------------------------------------------------------------------------
 
 upToParsing ::
-  (Members '[Reader EntryPoint, Error JuvixError, Files, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Error JuvixError, Files, PathResolver] r) =>
   Sem r Parser.ParserResult
 upToParsing = ask >>= Parser.fromSource
 
@@ -67,57 +67,57 @@ upToParsedSource ::
 upToParsedSource = ask
 
 upToScoping ::
-  (Members '[Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Error JuvixError, NameIdGen] r) =>
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Error JuvixError, NameIdGen] r) =>
   Sem r Scoper.ScoperResult
 upToScoping = Scoper.fromParsed
 
 upToInternal ::
-  (Members '[Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Error JuvixError, NameIdGen, Termination] r) =>
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Error JuvixError, NameIdGen, Termination] r) =>
   Sem r Internal.InternalResult
 upToInternal = upToScoping >>= Internal.fromConcrete
 
 upToInternalTyped ::
-  (Members '[Reader Parser.ParserResult, Error JuvixError, Reader EntryPoint, Reader Store.ModuleTable, NameIdGen] r) =>
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Error JuvixError, Reader EntryPoint, Reader Store.ModuleTable, NameIdGen] r) =>
   Sem r Internal.InternalTypedResult
 upToInternalTyped = Internal.typeCheckingNew upToInternal
 
 upToCore ::
-  (Members '[Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
   Sem r Core.CoreResult
 upToCore = upToInternalTyped >>= Core.fromInternal
 
 upToStoredCore ::
-  (Members '[Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
   Sem r Core.CoreResult
 upToStoredCore =
   upToCore >>= \r -> Core.toStored (r ^. Core.coreResultModule) >>= \md -> return r {Core._coreResultModule = md}
 
 upToAsm ::
-  (Members '[Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
   Sem r Asm.InfoTable
 upToAsm =
   upToStoredCore >>= \Core.CoreResult {..} -> storedCoreToAsm _coreResultModule
 
 upToMiniC ::
-  (Members '[Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
   Sem r C.MiniCResult
 upToMiniC = upToAsm >>= asmToMiniC
 
 upToVampIR ::
-  (Members '[Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
   Sem r VampIR.Result
 upToVampIR =
   upToStoredCore >>= \Core.CoreResult {..} -> storedCoreToVampIR _coreResultModule
 
 upToGeb ::
-  (Members '[Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
   Geb.ResultSpec ->
   Sem r Geb.Result
 upToGeb spec =
   upToStoredCore >>= \Core.CoreResult {..} -> storedCoreToGeb spec _coreResultModule
 
 upToCoreTypecheck ::
-  (Members '[Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
   Sem r Core.CoreResult
 upToCoreTypecheck =
   upToCore >>= \r -> Core.toTypechecked (r ^. Core.coreResultModule) >>= \md -> return r {Core._coreResultModule = md}

src/Juvix/Compiler/Pipeline/Driver.hs

@@ -9,6 +9,7 @@ where
 
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Concrete (ImportCycle (ImportCycle), ScoperError (ErrImportCycle))
+import Juvix.Compiler.Concrete.Data.Highlight
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
@@ -55,7 +56,7 @@ type MCache = Cache EntryIndex (PipelineResult Store.ModuleInfo)
 
 processFile ::
   forall r.
-  (Members '[Error JuvixError, Files, GitClone, PathResolver] r) =>
+  (Members '[HighlightBuilder, Error JuvixError, Files, GitClone, PathResolver] r) =>
   EntryPoint ->
   Sem r (PipelineResult Parser.ParserResult)
 processFile entry =
@@ -96,7 +97,7 @@ processFileToStoredCore entry =
 
 processFileUpTo ::
   forall r a.
-  (Members '[Reader EntryPoint, Error JuvixError, Files, GitClone, PathResolver] r) =>
+  (Members '[HighlightBuilder, Reader EntryPoint, Error JuvixError, Files, GitClone, PathResolver] r) =>
   Sem (Reader Parser.ParserResult ': Reader Store.ModuleTable ': NameIdGen ': r) a ->
   Sem r (PipelineResult a)
 processFileUpTo a = do
@@ -111,7 +112,7 @@ processFileUpTo a = do
 
 processFile' ::
   forall r.
-  (Members '[Reader ImportParents, Error JuvixError, Files, GitClone, PathResolver, MCache] r) =>
+  (Members '[HighlightBuilder, Reader ImportParents, Error JuvixError, Files, GitClone, PathResolver, MCache] r) =>
   EntryPoint ->
   Sem r (PipelineResult Parser.ParserResult)
 processFile' entry = do
@@ -165,7 +166,7 @@ processFileToStoredCore' ::
   (Members '[Reader ImportParents, Error JuvixError, Files, GitClone, PathResolver, MCache] r) =>
   EntryPoint ->
   Sem r (PipelineResult Core.CoreResult)
-processFileToStoredCore' entry = do
+processFileToStoredCore' entry = ignoreHighlightBuilder $ do
   res <- processFile' entry
   r <-
     evalTopNameIdGen

src/Juvix/Compiler/Pipeline/Repl.hs

@@ -1,5 +1,6 @@
 module Juvix.Compiler.Pipeline.Repl where
 
+import Juvix.Compiler.Concrete (ignoreHighlightBuilder)
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromParsed qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
@@ -79,9 +80,10 @@ parseReplInput ::
   Text ->
   Sem r Parser.ReplInput
 parseReplInput fp txt =
-  runNameIdGenArtifacts $
-    runStateLikeArtifacts runParserResultBuilder artifactParsing $
-      Parser.replInputFromTextSource fp txt
+  ignoreHighlightBuilder $
+    runNameIdGenArtifacts $
+      runStateLikeArtifacts runParserResultBuilder artifactParsing $
+        Parser.replInputFromTextSource fp txt
 
 expressionUpToTyped ::
   (Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r) =>