[highlight] add basic support for highlighting symbols

app/Main.hs

@@ -14,6 +14,8 @@ import qualified MiniJuvix.Syntax.Abstract.Pretty.Ansi as A
 import qualified MiniJuvix.Syntax.Concrete.Language as M
 import qualified MiniJuvix.Syntax.Concrete.Parser as M
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as M
+import qualified MiniJuvix.Syntax.Concrete.Scoped.InfoTable as Scoped
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Highlight as Scoped
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (defaultOptions)
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as M
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html
@@ -43,6 +45,7 @@ data Command
   | MiniHaskell MiniHaskellOptions
   | MicroJuvix MicroJuvixCommand
   | DisplayVersion
+  | Highlight HighlightOptions
 
 data ScopeOptions = ScopeOptions
   { _scopeRootDir :: FilePath,
@@ -57,6 +60,10 @@ data ParseOptions = ParseOptions
     _parseNoPrettyShow :: Bool
   }
 
+data HighlightOptions = HighlightOptions
+  { _highlightInputFile :: FilePath
+  }
+
 data HtmlOptions = HtmlOptions
   { _htmlInputFile :: FilePath,
     _htmlRecursive :: Bool,
@@ -88,6 +95,11 @@ parseHtml = do
       "ayu" -> Right Ayu
       _ -> Left $ "unrecognised theme: " <> s
 
+parseHighlight :: Parser HighlightOptions
+parseHighlight = do
+  _highlightInputFile <- parseInputFile
+  pure HighlightOptions {..}
+
 parseParse :: Parser ParseOptions
 parseParse = do
   _parseInputFile <- parseInputFile
@@ -165,7 +177,8 @@ parseCommand =
                 commandHtml,
                 commandTermination,
                 commandMicroJuvix,
-                commandMiniHaskell
+                commandMiniHaskell,
+                commandHighlight
               ]
         )
   where
@@ -187,6 +200,15 @@ parseCommand =
             (MiniHaskell <$> parseMiniHaskell)
             (progDesc "Translate a MiniJuvix file to MiniHaskell")
 
+    commandHighlight :: Mod CommandFields Command
+    commandHighlight = command "highlight" minfo
+      where
+        minfo :: ParserInfo Command
+        minfo =
+          info
+            (Highlight <$> parseHighlight)
+            (progDesc "Highlight a MiniJuvix file")
+
     commandParse :: Mod CommandFields Command
     commandParse = command "parse" minfo
       where
@@ -248,6 +270,10 @@ go c = do
         printer
           | not _scopeNoColors = M.printPrettyCode
           | otherwise = T.printPrettyCode
+    Highlight HighlightOptions {..} -> do
+        m <- parseModuleIO _highlightInputFile
+        (i , _) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+        putStrLn (Scoped.go (i ^. Scoped.infoNames))
     Parse ParseOptions {..} -> do
       m <- parseModuleIO _parseInputFile
       if _parseNoPrettyShow then print m else pPrint m

src/MiniJuvix/Syntax/Concrete/Lexer.hs

@@ -62,17 +62,21 @@ bracedString =
 string :: MonadParsec e Text m => m Text
 string = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
 
-mkLoc :: SourcePos -> Loc
-mkLoc SourcePos {..} = Loc {..}
+mkLoc :: Int -> SourcePos -> Loc
+mkLoc offset SourcePos {..} = Loc {..}
   where
     _locFile = sourceName
+    _locOffset = Pos (fromIntegral offset)
     _locFileLoc = FileLoc {..}
       where
         _locLine = fromPos sourceLine
         _locCol = fromPos sourceColumn
 
 curLoc :: MonadParsec e Text m => m Loc
-curLoc = mkLoc <$> getSourcePos
+curLoc = do
+  sp <- getSourcePos
+  offset <- stateOffset <$> getParserState
+  return (mkLoc offset sp)
 
 withLoc :: MonadParsec e Text m => (Loc -> m a) -> m a
 withLoc ma = curLoc >>= ma

src/MiniJuvix/Syntax/Concrete/Loc.hs

@@ -3,7 +3,7 @@ module MiniJuvix.Syntax.Concrete.Loc where
 import MiniJuvix.Prelude
 import Prettyprinter
 
-newtype Pos = Pos Word64
+newtype Pos = Pos {_unPos :: Word64 }
   deriving stock (Show, Eq, Ord)
 
 instance Semigroup Pos where
@@ -16,12 +16,14 @@ data FileLoc = FileLoc
   { -- | Line number
     _locLine :: !Pos,
     -- | Column number
-    _locCol :: !Pos
+    _locCol :: !Pos,
+    -- | Offset wrt the start of the input. Used for syntax highlighting.
+    _locOffset :: !Pos
   }
   deriving stock (Show, Eq)
 
 instance Ord FileLoc where
-  compare (FileLoc l c) (FileLoc l' c') = compare (l, c) (l', c')
+  compare (FileLoc l c o) (FileLoc l' c' o') = compare (l, c, o) (l', c', o')
 
 data Loc = Loc
   { -- | Name of source file
@@ -79,4 +81,6 @@ instance Pretty Interval where
         | otherwise = pretty s <> hyphen <> pretty e
 
 makeLenses ''Interval
+makeLenses ''FileLoc
 makeLenses ''Loc
+makeLenses ''Pos

src/MiniJuvix/Syntax/Concrete/Scoped/Highlight.hs

@@ -0,0 +1,85 @@
+module MiniJuvix.Syntax.Concrete.Scoped.Highlight where
+
+import MiniJuvix.Syntax.Concrete.Scoped.Name
+import MiniJuvix.Syntax.Concrete.Loc
+import qualified MiniJuvix.Internal.Strings as Str
+import MiniJuvix.Prelude
+import Prettyprinter
+import Prettyprinter.Render.Text
+
+data Face =
+  FaceConstructor
+  | FaceInductive
+  | FaceFunction
+  | FaceModule
+  | FaceAxiom
+
+data Property =
+  PropertyFace Face
+
+data Instruction =
+  SetProperty {
+  _setPropertyInterval :: Interval,
+  _setPropertyProperty :: Property
+  }
+
+data SExp =
+  Symbol Text
+  | List [SExp]
+  | Quote SExp
+  | Int Word64
+
+makeLenses ''Instruction
+
+go :: [Name] -> Text
+go = renderSExp . progn . mapMaybe goName
+
+progn :: [SExp] -> SExp
+progn l = List (Symbol "progn" : l)
+
+nameKindFace :: NameKind -> Maybe Face
+nameKindFace = \case
+  KNameConstructor -> Just FaceConstructor
+  KNameInductive -> Just FaceInductive
+  KNameFunction -> Just FaceFunction
+  KNameTopModule -> Just FaceModule
+  KNameLocalModule -> Just FaceModule
+  KNameAxiom -> Just FaceAxiom
+  KNameLocal -> Nothing
+
+-- | Example instruction:
+-- (add-text-properties 20 28
+--  '(face minijuvix-highlight-constructor-face))
+instr :: Interval -> Face -> SExp
+instr i f =
+  List [Symbol "add-text-properties", start , end, face]
+  where
+  pos l = Int (succ (l ^. locOffset . unPos))
+  start = pos (i ^. intStart)
+  end = pos (i ^. intEnd)
+  face = Quote (List [Symbol "face", faceSymbol ])
+  faceSymbol = Symbol ("minijuvix-highlight-" <> faceSymbolStr <> "-face")
+  faceSymbolStr = case f of
+    FaceAxiom -> Str.axiom
+    FaceInductive -> Str.inductive
+    FaceConstructor -> Str.constructor
+    FaceModule -> Str.module_
+    FaceFunction -> Str.function
+
+goName :: Name -> Maybe SExp
+goName n = do
+  f <- nameKindFace (n ^. nameKind)
+  return (instr (getLoc n) f)
+
+renderSExp :: SExp -> Text
+renderSExp =
+  renderStrict
+  . layoutPretty defaultLayoutOptions
+  . pretty
+
+instance Pretty SExp where
+  pretty = \case
+    Symbol s -> pretty s
+    Int s -> pretty s
+    List l -> parens (sep (map pretty l))
+    Quote l -> pretty '`' <> pretty l

src/MiniJuvix/Syntax/Concrete/Scoped/InfoTable.hs

@@ -27,7 +27,8 @@ data InfoTable = InfoTable {
   _infoAxioms :: HashMap AxiomRef AxiomInfo,
   _infoInductives :: HashMap InductiveRef InductiveInfo,
   _infoFunctions :: HashMap FunctionRef FunctionInfo,
-  _infoFunctionClauses :: HashMap S.Symbol (FunctionClause 'Scoped)
+  _infoFunctionClauses :: HashMap S.Symbol (FunctionClause 'Scoped),
+  _infoNames :: [S.Name]
   }
 
 emptyInfoTable :: InfoTable
@@ -36,7 +37,8 @@ emptyInfoTable = InfoTable {
   _infoAxioms = mempty,
   _infoInductives = mempty,
   _infoFunctions = mempty,
-  _infoFunctionClauses = mempty
+  _infoFunctionClauses = mempty,
+  _infoNames = mempty
   }
 
 makeLenses ''InfoTable

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -138,7 +138,7 @@ bindReservedSymbol s' entry = do
       Just SymbolInfo {..} -> SymbolInfo (HashMap.insert path entry _symbolInfo)
 
 bindSymbolOf ::
-  Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r =>
   S.NameKind ->
   (S.Name' () -> SymbolEntry) ->
   Symbol ->
@@ -146,10 +146,11 @@ bindSymbolOf ::
 bindSymbolOf k e s = do
   s' <- reserveSymbolOf k s
   bindReservedSymbol s' (e (set S.nameConcrete () s'))
+  registerName (S.unqualifiedSymbol s')
   return s'
 
 bindFunctionSymbol ::
-  Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r =>
   Symbol ->
   Sem r S.Symbol
 bindFunctionSymbol =
@@ -158,7 +159,7 @@ bindFunctionSymbol =
     (\s' -> EntryFunction (FunctionRef' s'))
 
 bindInductiveSymbol ::
-  Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r =>
   Symbol ->
   Sem r S.Symbol
 bindInductiveSymbol =
@@ -167,7 +168,7 @@ bindInductiveSymbol =
     (\s' -> EntryInductive (InductiveRef' s'))
 
 bindAxiomSymbol ::
-  Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r =>
   Symbol ->
   Sem r S.Symbol
 bindAxiomSymbol =
@@ -176,7 +177,7 @@ bindAxiomSymbol =
     (\s' -> EntryAxiom (AxiomRef' s'))
 
 bindConstructorSymbol ::
-  Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r =>
   Symbol ->
   Sem r S.Symbol
 bindConstructorSymbol =
@@ -185,7 +186,7 @@ bindConstructorSymbol =
     (\s' -> EntryConstructor (ConstructorRef' s'))
 
 bindLocalModuleSymbol ::
-  Members '[Error ScopeError, State ScoperState, State Scope] r =>
+  Members '[Error ScopeError, State ScoperState, State Scope, InfoTableBuilder] r =>
   ExportInfo ->
   Module 'Scoped 'ModuleLocal ->
   Symbol ->
@@ -307,29 +308,33 @@ lookupQualifiedSymbol (path, sym) = do
           ((fmap (^. moduleExportInfo) . HashMap.lookup topPath) >=> lookInExport sym remaining) <$> gets _scopeTopModules
 
 checkQualifiedExpr ::
-  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r =>
   QualifiedName ->
   Sem r ScopedIden
 checkQualifiedExpr q@(QualifiedName (Path p) sym) = do
   es <- lookupQualifiedSymbol (toList p, sym)
   case es of
     [] -> notInScope
-    [e] -> return (entryToScopedIden q' e)
+    [e] -> entryToScopedIden q' e
     _ -> throw (ErrAmbiguousSym (AmbiguousSym q' es))
   where
     q' = NameQualified q
     notInScope = throw (ErrQualSymNotInScope q)
 
-entryToScopedIden :: Name -> SymbolEntry -> ScopedIden
-entryToScopedIden name = \case
-  EntryAxiom ref -> ScopedAxiom (set (axiomRefName . S.nameConcrete) name ref)
-  EntryInductive ref ->
-    ScopedInductive (set (inductiveRefName . S.nameConcrete) name ref)
-  EntryConstructor ref ->
-    ScopedConstructor (set (constructorRefName . S.nameConcrete) name ref)
-  EntryFunction ref ->
-    ScopedFunction (set (functionRefName . S.nameConcrete) name ref)
-  EntryModule {} -> impossible
+entryToScopedIden :: Members '[InfoTableBuilder] r => Name -> SymbolEntry -> Sem r ScopedIden
+entryToScopedIden name e = do
+  let scopedName :: S.Name
+      scopedName = set S.nameConcrete name (entryName e)
+  registerName scopedName
+  return $ case e of
+    EntryAxiom ref -> ScopedAxiom (set (axiomRefName . S.nameConcrete) name ref)
+    EntryInductive ref ->
+      ScopedInductive (set (inductiveRefName . S.nameConcrete) name ref)
+    EntryConstructor ref ->
+      ScopedConstructor (set (constructorRefName . S.nameConcrete) name ref)
+    EntryFunction ref ->
+      ScopedFunction (set (functionRefName . S.nameConcrete) name ref)
+    EntryModule {} -> impossible
 
 -- | We gather all symbols which have been defined or marked to be public in the given scope.
 exportScope :: forall r. Members '[State Scope, Error ScopeError] r => Scope -> Sem r ExportInfo
@@ -502,7 +507,9 @@ checkTopModule m@(Module path params body) = do
           _nameVisibilityAnn = VisPublic
           _nameWhyInScope = S.BecauseDefined
           _nameVerbatim = N.topModulePathToDottedPath path
-      return S.Name' {..}
+          moduleName = S.Name' {..}
+      -- registerName moduleName
+      return moduleName
     iniScope :: Scope
     iniScope = emptyScope (getTopModulePath m)
     checkedModule :: Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
@@ -712,6 +719,7 @@ checkFunctionClause ::
   Sem r (FunctionClause 'Scoped)
 checkFunctionClause clause@FunctionClause {..} = do
   clauseOwnerFunction' <- checkTypeSigInScope
+  registerName (S.unqualifiedSymbol clauseOwnerFunction')
   (clausePatterns', clauseWhere', clauseBody') <- do
     clp <- mapM checkParsePatternAtom _clausePatterns
     withBindCurrentGroup $ do
@@ -851,7 +859,7 @@ checkLambdaClause LambdaClause {..} = do
       }
 
 checkUnqualified ::
-  Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState, InfoTableBuilder] r =>
   Symbol ->
   Sem r ScopedIden
 checkUnqualified s = do
@@ -869,20 +877,22 @@ checkUnqualified s = do
           <$> lookupQualifiedSymbol ([], s)
       case entries of
         [] -> err
-        [x] -> return (entryToScopedIden n x)
+        [x] -> entryToScopedIden n x
         es -> throw (ErrAmbiguousSym (AmbiguousSym n es))
       where
         n = NameUnqualified s
 
 checkPatternName ::
   forall r.
-  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r =>
   Name ->
   Sem r PatternScopedIden
 checkPatternName n = do
   c <- getConstructorRef
   case c of
-    Just constr -> return (PatternScopedConstructor constr) -- the symbol is a constructor
+    Just constr -> do
+      registerName (constr ^. constructorRefName)
+      return (PatternScopedConstructor constr) -- the symbol is a constructor
     Nothing -> PatternScopedVar <$> groupBindLocalVariable sym -- the symbol is a variable
   where
     (path, sym) = case n of
@@ -954,13 +964,13 @@ groupBindLocalVariable s = do
       return n
 
 checkPatternAtoms ::
-  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r =>
   PatternAtoms 'Parsed ->
   Sem r (PatternAtoms 'Scoped)
 checkPatternAtoms (PatternAtoms s) = PatternAtoms <$> mapM checkPatternAtom s
 
 checkPatternAtom ::
-  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r =>
   PatternAtom 'Parsed ->
   Sem r (PatternAtom 'Scoped)
 checkPatternAtom p = case p of
@@ -970,7 +980,7 @@ checkPatternAtom p = case p of
   PatternAtomIden n -> PatternAtomIden <$> checkPatternName n
 
 checkName ::
-  Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, Reader LocalVars, State ScoperState, InfoTableBuilder] r =>
   Name ->
   Sem r ScopedIden
 checkName n = case n of
@@ -1036,13 +1046,13 @@ checkExpressionAtoms ::
 checkExpressionAtoms (ExpressionAtoms l) = ExpressionAtoms <$> mapM checkExpressionAtom l
 
 checkParseExpressionAtoms ::
-  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder ] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder] r =>
   ExpressionAtoms 'Parsed ->
   Sem r Expression
 checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms
 
 checkParsePatternAtom ::
-  Members '[Error ScopeError, State Scope, State ScoperState] r =>
+  Members '[Error ScopeError, State Scope, State ScoperState, InfoTableBuilder] r =>
   PatternAtom 'Parsed ->
   Sem r Pattern
 checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs

@@ -3,7 +3,7 @@ module MiniJuvix.Syntax.Concrete.Scoped.Scoper.InfoTableBuilder where
 import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Language
-import MiniJuvix.Syntax.Concrete.Scoped.Name
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import MiniJuvix.Syntax.Concrete.Scoped.Scope
 
 data InfoTableBuilder m a where
@@ -12,6 +12,7 @@ data InfoTableBuilder m a where
   RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m ()
   RegisterFunction :: TypeSignature 'Scoped -> InfoTableBuilder m ()
   RegisterFunctionClause :: FunctionClause 'Scoped -> InfoTableBuilder m ()
+  RegisterName :: S.Name -> InfoTableBuilder m ()
 
 makeSem ''InfoTableBuilder
 
@@ -36,41 +37,38 @@ registerFunctionClause' :: Member InfoTableBuilder r =>
   FunctionClause 'Scoped -> Sem r (FunctionClause 'Scoped)
 registerFunctionClause' a = registerFunctionClause a $> a
 
-
 toState :: Sem (InfoTableBuilder ': r) a -> Sem (State InfoTable ': r) a
 toState = reinterpret $ \case
   RegisterAxiom d ->
-    let ref = AxiomRef' (unqualifiedSymbol (d ^. axiomName))
+    let ref = AxiomRef' (S.unqualifiedSymbol (d ^. axiomName))
         info = AxiomInfo {
           _axiomInfoType = d ^. axiomType,
           _axiomInfoBackends = d ^. axiomBackendItems
           }
     in modify (over infoAxioms (HashMap.insert ref info))
   RegisterConstructor c -> let
-      ref = ConstructorRef' (unqualifiedSymbol (c ^. constructorName))
+      ref = ConstructorRef' (S.unqualifiedSymbol (c ^. constructorName))
       info = ConstructorInfo {
         _constructorInfoType = c ^. constructorType
       }
-      in modify (over infoConstructors  (HashMap.insert ref info)
-   )
+      in modify (over infoConstructors  (HashMap.insert ref info))
   RegisterInductive ity -> let
-        ref = InductiveRef' (unqualifiedSymbol (ity ^. inductiveName))
+        ref = InductiveRef' (S.unqualifiedSymbol (ity ^. inductiveName))
         info = InductiveInfo {
           _inductiveInfoDef = ity
         }
-      in modify (over infoInductives  (HashMap.insert ref info)
-   )
+      in modify (over infoInductives  (HashMap.insert ref info))
   RegisterFunction f -> let
-      ref = FunctionRef' (unqualifiedSymbol (f ^. sigName))
+      ref = FunctionRef' (S.unqualifiedSymbol (f ^. sigName))
       info = FunctionInfo {
         _functionInfoType = f ^. sigType
       }
-      in modify (over infoFunctions  (HashMap.insert ref info)
-   )
+      in modify (over infoFunctions  (HashMap.insert ref info))
   RegisterFunctionClause c -> let
     key = c ^. clauseOwnerFunction
     value = c
     in modify (over infoFunctionClauses (HashMap.insert key value))
+  RegisterName n -> modify (over infoNames (cons n))
 
 runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
 runInfoTableBuilder = runState emptyInfoTable . toState

tests/positive/StdlibList/Data/Bool.mjuvix

@@ -8,14 +8,14 @@ module Data.Bool;
   not true ≔ false;
   not false ≔ true;
 
-  infixr 2 ||;
-  || : Bool → Bool → Bool;
-  || false a ≔ a;
-  || true _ ≔ true;
+  -- infixr 2 ||;
+  -- || : Bool → Bool → Bool;
+  -- || false a ≔ a;
+  -- || true _ ≔ true;
 
-  infixr 2 &&;
-  && : Bool → Bool → Bool;
-  && false _ ≔ false;
-  && true a ≔ a;
+  -- infixr 2 &&;
+  -- && : Bool → Bool → Bool;
+  -- && false _ ≔ false;
+  -- && true a ≔ a;
 
-end;
+end;