From 9708dd3fe3b7b67604ea2356a08cadd81aff466e Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 1 Apr 2022 00:39:53 +0200 Subject: [PATCH] [highlight] add basic support for highlighting symbols --- app/Main.hs | 28 +++++- src/MiniJuvix/Syntax/Concrete/Lexer.hs | 10 ++- src/MiniJuvix/Syntax/Concrete/Loc.hs | 10 ++- .../Syntax/Concrete/Scoped/Highlight.hs | 85 +++++++++++++++++++ .../Syntax/Concrete/Scoped/InfoTable.hs | 6 +- .../Syntax/Concrete/Scoped/Scoper.hs | 66 ++++++++------ .../Scoped/Scoper/InfoTableBuilder.hs | 22 +++-- tests/positive/StdlibList/Data/Bool.mjuvix | 18 ++-- 8 files changed, 187 insertions(+), 58 deletions(-) create mode 100644 src/MiniJuvix/Syntax/Concrete/Scoped/Highlight.hs diff --git a/app/Main.hs b/app/Main.hs index c5727efea..fca3f2f0c 100644 --- a/app/Main.hs +++ b/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 diff --git a/src/MiniJuvix/Syntax/Concrete/Lexer.hs b/src/MiniJuvix/Syntax/Concrete/Lexer.hs index 5180087d1..1833a0960 100644 --- a/src/MiniJuvix/Syntax/Concrete/Lexer.hs +++ b/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 diff --git a/src/MiniJuvix/Syntax/Concrete/Loc.hs b/src/MiniJuvix/Syntax/Concrete/Loc.hs index bb0c5f956..29dcfb152 100644 --- a/src/MiniJuvix/Syntax/Concrete/Loc.hs +++ b/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 diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Highlight.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Highlight.hs new file mode 100644 index 000000000..128792b3f --- /dev/null +++ b/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 diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/InfoTable.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/InfoTable.hs index 3b22ad1ad..00809ead2 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/InfoTable.hs +++ b/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 diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs index b7075b1f1..5557dc942 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs +++ b/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 diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs index 43b3cb1e1..96859732a 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs +++ b/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 diff --git a/tests/positive/StdlibList/Data/Bool.mjuvix b/tests/positive/StdlibList/Data/Bool.mjuvix index f4e666011..a10e90af5 100644 --- a/tests/positive/StdlibList/Data/Bool.mjuvix +++ b/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; \ No newline at end of file +end;