[ refactor ] More IDE protocol (#2238)

CHANGELOG.md

@@ -55,6 +55,24 @@
   `prim__void`.
 * Adds `%deprecate` pragma that can be used to warn when deprecated functions are used.
 
+### IDE protocol changes
+
+* The IDE protocol and its serialisation to S-Expressions are factored
+  into a separate module hierarchy Protocol.{Hex, SExp, IDE}.
+
+* File context ranges sent in the IDE protocol follow the same
+  convention as Bounds values in the parser:
+  + all offsets (line and column) are 0-based.
+  + Lines: start and end are within the bounds
+  + Column:
+    + start column is within the bounds;
+    + end   column is after the bounds.
+
+  This changes behaviour from previous versions of the protocol.
+  Matching PRs in the emacs modes:
+  + idris2-mode [PR#11](https://github.com/idris-community/idris2-mode/pull/11)
+  + idris-mode [PR#547](https://github.com/idris-hackers/idris-mode/pull/547)
+
 ### Library changes
 
 #### Base

docs/source/implementation/ide-protocol.rst

@@ -7,6 +7,8 @@ The Idris REPL has two modes of interaction: a human-readable syntax designed fo
 The IDE-Protocol is versioned separately from the Idris compiler.
 The first version of Idris (written in Haskell and is at v1.3.3) implements version one of the IDE Protocol, and Idris2 (self-hosting and is at v.0.3.0) implements version two of the IDE Protocol.
 
+The protocol and its serialisation/deserialisation routines are part of the `Protocol` submodule hierarchy and are packaged in the `idris2protocols.ipkg` package.
+
 
 Protocol Overview
 -----------------
@@ -173,21 +175,23 @@ Possible Replies
 
 Possible replies include a normal final reply:::
 
- (:return (:ok SEXP [HIGHLIGHTING]))
- (:return (:error String [HIGHLIGHTING]))
+ (:return (:ok SEXP [HIGHLIGHTING]) ID)
+ (:return (:error String [HIGHLIGHTING]) ID)
 
 A normal intermediate reply:::
 
- (:output (:ok SEXP [HIGHLIGHTING]))
- (:output (:error String [HIGHLIGHTING]))
+ (:output (:ok SEXP [HIGHLIGHTING]) ID)
+ (:output (:error String [HIGHLIGHTING]) ID)
 
 Informational and/or abnormal replies:::
 
-  (:write-string String)
-  (:set-prompt String)
-  (:warning (FilePath (LINE COL) (LINE COL) String [HIGHLIGHTING]))
+  (:write-string String ID)
+  (:set-prompt String ID)
+  (:warning (FilePath (LINE COL) (LINE COL) String [HIGHLIGHTING]) ID)
 
 
+Warnings include compiler errors that don't cause the compiler to stop.
+
 Output Highlighting
 -------------------
 
@@ -257,6 +261,6 @@ When elaborating source code or REPL input, Idris will locate regions of the sou
 These messages will arrive as replies to the command that caused elaboration to occur, such as ``:load-file`` or ``:interpret``.
 They have the format:::
 
-  (:output (:ok (:highlight-source POSNS)))
+  (:output (:ok (:highlight-source POSNS)) ID)
 
 where ``POSNS`` is a list of positions to highlight. Each of these is a two-element list whose first element is a position (encoded as for the ``source-loc`` property above) and whose second element is highlighting metadata in the same format used for output.

idris2api.ipkg

@@ -221,6 +221,7 @@ modules =
     Protocol.IDE.Highlight,
     Protocol.Hex,
     Protocol.SExp,
+    Protocol.SExp.Parser,
 
     TTImp.BindImplicits,
     TTImp.Elab,

idris2protocols.ipkg.hide

@@ -3,18 +3,34 @@ version = 0.0.1
 
 modules
   = Protocol.Hex
-  , Protocol.IDE
+  -- , Protocol.IDE
   , Protocol.IDE.Command
   , Protocol.IDE.Decoration
   , Protocol.SExp
+  -- TODO: want to add this module, but the parser library introduces
+  -- dependencies on core idris
+  -- , Protocol.SExp.Parser
   , Libraries.Data.Span
-  , Protocol.IDE.FileContext
-  , Protocol.IDE.Formatting
-  , Protocol.IDE.Holes
-  , Protocol.IDE.Result
-  , Protocol.IDE.Highlight
-
+  , Libraries.Text.Lexer
+  , Libraries.Control.Delayed
+  , Libraries.Text.Bounded
+  , Libraries.Text.Lexer.Core
+  , Libraries.Text.Quantity
+  , Libraries.Text.Token
+  , Libraries.Text.Lexer.Tokenizer
+  , Libraries.Data.String.Extra
+  , Libraries.Text.PrettyPrint.Prettyprinter.Doc
+  , Libraries.Text.PrettyPrint.Prettyprinter.Symbols
+  , Libraries.Text.PrettyPrint.Prettyprinter
+  , Libraries.Text.Parser.Core
+  , Libraries.Text.Parser
+  , Parser.Rule.Source
+  -- , Protocol.IDE.FileContext
+  -- , Protocol.IDE.Formatting
+  -- , Protocol.IDE.Holes
+  -- , Protocol.IDE.Result
+  -- , Protocol.IDE.Highlight
 
 --depends =
 
-sourcedir = "src"
+sourcedir = "../src"

src/Idris/IDEMode/Parser.idr

@@ -3,85 +3,20 @@
 ||| we can reuse the standard stuff
 module Idris.IDEMode.Parser
 
-import Idris.IDEMode.Commands
+import Protocol.SExp
+import Protocol.SExp.Parser
+
+import Parser.Source
+
 import Core.Core
 import Core.FC
 
-import Data.List
-import Parser.Lexer.Source
-import Parser.Source
-import Parser.Support
-import Libraries.Text.Lexer
-import Libraries.Text.Lexer.Tokenizer
-import Libraries.Text.Parser
-
-%default total
-
-%hide Text.Lexer.symbols
-%hide Parser.Lexer.Source.symbols
-
-symbols : List String
-symbols = ["(", ":", ")"]
-
-stringTokens : Tokenizer Token
-stringTokens
-    = match (someUntil (is '"') (escape (is '\\') any <|> any)) $ StringLit 0
-
-ideTokens : Tokenizer Token
-ideTokens =
-      match (choice $ exact <$> symbols) Symbol
-  <|> match digits (IntegerLit . cast)
-  <|> compose (is '"')
-              (const $ StringBegin Single)
-              (const ())
-              (const stringTokens)
-              (const $ is '"')
-              (const StringEnd)
-  <|> match identAllowDashes Ident
-  <|> match space (const Comment)
-
-idelex : String -> Either (StopReason, Int, Int, String) (List (WithBounds Token))
-idelex str
-    = case lex ideTokens str of
-           -- Add the EndInput token so that we'll have a line and column
-           -- number to read when storing spans in the file
-           (tok, (EndInput, l, c, _)) => Right (filter notComment tok ++
-                                               [MkBounded EndInput False (MkBounds l c l c)])
-           (_, fail) => Left fail
-    where
-      notComment : WithBounds Token -> Bool
-      notComment t = case t.val of
-                          Comment => False
-                          _ => True
-
-covering
-sexp : Rule SExp
-sexp
-    = do symbol ":"; exactIdent "True"
-         pure (BoolAtom True)
-  <|> do symbol ":"; exactIdent "False"
-         pure (BoolAtom False)
-  <|> do i <- intLit
-         pure (IntegerAtom i)
-  <|> do str <- simpleStr
-         pure (StringAtom str)
-  <|> do symbol ":"; x <- unqualifiedName
-         pure (SymbolAtom x)
-  <|> do symbol "("
-         xs <- many sexp
-         symbol ")"
-         pure (SExpList xs)
-
-ideParser : {e : _} ->
-            String -> Grammar State Token e ty -> Either Error ty
-ideParser str p
-    = do toks   <- mapFst (fromLexError (Virtual Interactive)) $ idelex str
-         (_, _, (parsed, _)) <- mapFst (fromParsingErrors (Virtual Interactive)) $ parseWith p toks
-         Right parsed
-
+Cast SExpError Error where
+  cast (LexError    err) = fromLexError      (Virtual Interactive) err
+  cast (ParseErrors err) = fromParsingErrors (Virtual Interactive) err
 
 export
 covering
 parseSExp : String -> Either Error SExp
 parseSExp inp
-    = ideParser inp (do c <- sexp; eoi; pure c)
+    = mapFst cast $ Protocol.SExp.Parser.parseSExp inp

src/Protocol/SExp/Parser.idr

@@ -0,0 +1,99 @@
+module Protocol.SExp.Parser
+
+import Idris.IDEMode.Commands
+
+import Data.List
+
+import Libraries.Text.Lexer
+import Parser.Lexer.Common
+import Parser.Source
+import Parser.Lexer.Source
+import Libraries.Text.Token
+import Libraries.Text.Lexer.Tokenizer
+import Libraries.Text.Parser
+
+import Core.Metadata
+
+%default total
+
+%hide Text.Lexer.symbols
+%hide Parser.Lexer.Source.symbols
+%hide Parser.Rule.Source.symbol
+
+symbols : List String
+symbols = ["(", ":", ")"]
+
+symbol : String -> Rule ()
+symbol req
+    = terminal ("Expected '" ++ req ++ "'") $
+               \case
+                 Symbol s => guard (s == req)
+                 _ => Nothing
+
+
+stringTokens : Tokenizer Token
+stringTokens
+    = match (someUntil (is '"') (escape (is '\\') any <|> any)) $ StringLit 0
+
+ideTokens : Tokenizer Token
+ideTokens =
+      match (choice $ exact <$> symbols) Symbol
+  <|> match digits (IntegerLit . cast)
+  <|> compose (is '"')
+              (const $ StringBegin Single)
+              (const ())
+              (const stringTokens)
+              (const $ is '"')
+              (const StringEnd)
+  <|> match identAllowDashes Ident
+  <|> match space (const Comment)
+
+idelex : String -> Either (StopReason, Int, Int, String) (List (WithBounds Token))
+idelex str
+    = case lex ideTokens str of
+           -- Add the EndInput token so that we'll have a line and column
+           -- number to read when storing spans in the file
+           (tok, (EndInput, l, c, _)) => Right (filter notComment tok ++
+                                               [MkBounded EndInput False (MkBounds l c l c)])
+           (_, fail) => Left fail
+    where
+      notComment : WithBounds Token -> Bool
+      notComment t = case t.val of
+                          Comment => False
+                          _ => True
+
+covering
+sexp : Rule SExp
+sexp
+    = do symbol ":"; exactIdent "True"
+         pure (BoolAtom True)
+  <|> do symbol ":"; exactIdent "False"
+         pure (BoolAtom False)
+  <|> do i <- intLit
+         pure (IntegerAtom i)
+  <|> do str <- simpleStr
+         pure (StringAtom str)
+  <|> do symbol ":"; x <- unqualifiedName
+         pure (SymbolAtom x)
+  <|> do Parser.symbol "("
+         xs <- Parser.many sexp
+         symbol ")"
+         pure (SExpList xs)
+
+public export
+data SExpError =
+    LexError (StopReason, Int, Int, String)
+  | ParseErrors (List1 $ ParsingError Token)
+
+ideParser : {e : _} ->
+            String -> Grammar State Token e ty -> Either SExpError ty
+ideParser str p
+    = do toks   <- mapFst LexError $ idelex str
+         (_, _, (parsed, _)) <- mapFst ParseErrors $ parseWith p toks
+         Right parsed
+
+export
+covering
+parseSExp : String -> Either SExpError SExp
+parseSExp inp
+    = ideParser inp (do c <- sexp; eoi; pure c)