0 | ||| Messages exchanged during the IDE protocol
  1 | module Protocol.IDE
  2 |
  3 | import public Libraries.Data.Span
  4 |
  5 | import public Protocol.IDE.Command     as Protocol.IDE
  6 | import public Protocol.IDE.Decoration  as Protocol.IDE
  7 | import public Protocol.IDE.Formatting  as Protocol.IDE
  8 | import public Protocol.IDE.FileContext as Protocol.IDE
  9 | import public Protocol.IDE.Holes       as Protocol.IDE
 10 | import public Protocol.IDE.Result      as Protocol.IDE
 11 | import public Protocol.IDE.Highlight   as Protocol.IDE
 12 |
 13 | import Protocol.SExp
 14 | import Protocol.SExp.Parser
 15 |
 16 | %default total
 17 | ------------------------------------------------------------------------
 18 |
 19 | public export
 20 | Highlighting : Type
 21 | Highlighting = List (Span Properties)
 22 |
 23 | export
 24 | SExpable a => SExpable (Span a) where
 25 |   toSExp (MkSpan start width ann)
 26 |     = SExpList [ IntegerAtom (cast start)
 27 |                , IntegerAtom (cast width)
 28 |                , toSExp ann
 29 |                ]
 30 |
 31 | export
 32 | FromSExpable a => FromSExpable (Span a) where
 33 |   fromSExp (SExpList [ start
 34 |                      , width
 35 |                      , ann
 36 |                      ]) = do pure $ MkSpan { start = !(fromSExp start)
 37 |                                            , length = !(fromSExp width)
 38 |                                            , property  = !(fromSExp ann)}
 39 |   fromSExp _ = Nothing
 40 |
 41 | ------------------------------------------------------------------------
 42 |
 43 | public export
 44 | data ReplyPayload =
 45 |     OK    Result Highlighting
 46 |   | HighlightSource (List SourceHighlight)
 47 |   | Error String Highlighting
 48 |
 49 | export
 50 | SExpable ReplyPayload where
 51 |   toSExp (OK    result hl) = SExpList (SymbolAtom "ok" :: toSExp result ::
 52 |     case hl of
 53 |       [] => []
 54 |       _ => [SExpList (map toSExp hl)])
 55 |   toSExp (HighlightSource hls) = SExpList
 56 |     [ SymbolAtom "ok"
 57 |     , SExpList
 58 |       [ SymbolAtom "highlight-source"
 59 |       , toSExp hls]
 60 |     ]
 61 |   toSExp (Error msg    hl) = SExpList (SymbolAtom "error" :: toSExp msg ::
 62 |     case hl of
 63 |       [] => []
 64 |       _  => [SExpList (map toSExp hl)])
 65 |
 66 | -- Again, not the most efficient. Probably better to index by the
 67 | -- expected return type in the future
 68 | export
 69 | FromSExpable ReplyPayload where
 70 |   fromSExp (SExpList
 71 |     [ SymbolAtom "ok"
 72 |     , SExpList
 73 |       [ SymbolAtom "highlight-source"
 74 |       , hls]
 75 |     ]) = do pure $ HighlightSource !(fromSExp hls)
 76 |   fromSExp (SExpList [SymbolAtom "ok", result])
 77 |     = do pure $ OK !(fromSExp result) []
 78 |   fromSExp (SExpList [SymbolAtom "ok", result, hl])
 79 |     = do pure $ OK !(fromSExp result) !(fromSExp hl)
 80 |   fromSExp (SExpList [SymbolAtom "error", msg])
 81 |     = do pure $ Error !(fromSExp msg) []
 82 |   fromSExp (SExpList [SymbolAtom "error", msg, hl])
 83 |     = do pure $ Error !(fromSExp msg) !(fromSExp hl)
 84 |   fromSExp _ = Nothing
 85 |
 86 | public export
 87 | data Reply =
 88 |     ProtocolVersion Int Int
 89 |   | Immediate    ReplyPayload Integer
 90 |   | Intermediate ReplyPayload Integer
 91 |   | WriteString String Integer
 92 |   | SetPrompt   String Integer
 93 |   | Warning FileContext String Highlighting Integer
 94 |
 95 | export
 96 | SExpable Reply where
 97 |   toSExp (ProtocolVersion maj min) =  toSExp (SymbolAtom "protocol-version", maj, min)
 98 |   toSExp (   Immediate payload id) = SExpList [SymbolAtom "return",
 99 |                                                       toSExp payload, toSExp id]
100 |   toSExp (Intermediate payload id) = SExpList [SymbolAtom "output",
101 |                                                       toSExp payload, toSExp id]
102 |   toSExp (WriteString str id) = SExpList [SymbolAtom "write-string", toSExp str, toSExp id]
103 |   toSExp (SetPrompt   str id) = SExpList [SymbolAtom "set-prompt"  , toSExp str, toSExp id]
104 |   toSExp (Warning fc str spans id) = SExpList [SymbolAtom "warning",
105 |     SExpList $ toSExp fc.file :: toSExp (fc.range.startLine, fc.range.startCol)
106 |                               :: toSExp (fc.range.endLine  , fc.range.endCol  )
107 |                               :: toSExp str :: case spans of
108 |       [] => []
109 |       _  => [SExpList (map toSExp spans)]
110 |       , toSExp id]
111 |
112 | export
113 | FromSExpable Reply where
114 |   fromSExp (SExpList [SymbolAtom "protocol-version", major, minor]) =
115 |      do Just $ ProtocolVersion !(fromSExp major) !(fromSExp minor)
116 |   fromSExp (SExpList [SymbolAtom "return", payload, iden]) =
117 |      do Just $ Immediate !(fromSExp payload) !(fromSExp iden)
118 |   fromSExp (SExpList [SymbolAtom "output", payload, iden]) =
119 |      do Just $ Intermediate !(fromSExp payload) !(fromSExp iden)
120 |   fromSExp (SExpList [SymbolAtom "write-string", str, iden]) =
121 |      do Just $ WriteString !(fromSExp str) !(fromSExp iden)
122 |   fromSExp (SExpList [SymbolAtom "set-prompt", str, iden]) =
123 |      do Just $ SetPrompt !(fromSExp str) !(fromSExp iden)
124 |   fromSExp (SExpList [SymbolAtom "warning"
125 |     , SExpList [filename, SExpList [startLine, startCol]
126 |                         , SExpList [endLine  , endCol  ]
127 |                         , str]
128 |     , iden]) = do
129 |       pure $ Warning (MkFileContext
130 |            { file = !(fromSExp filename)
131 |            , range = MkBounds { startLine = !(fromSExp startLine)
132 |                               , startCol  = !(fromSExp startCol)
133 |                               , endLine   = !(fromSExp endLine)
134 |                               , endCol    = !(fromSExp endCol)}
135 |            })
136 |            !(fromSExp str)
137 |            []
138 |            !(fromSExp iden)
139 |   fromSExp (SExpList [SymbolAtom "warning"
140 |     , SExpList [filename, SExpList [startLine, startCol]
141 |                       , SExpList [endLine  , endCol  ]
142 |                       , str, hl]
143 |     , iden]) = do
144 |       pure $ Warning (MkFileContext
145 |            { file = !(fromSExp filename)
146 |            , range = MkBounds { startLine = !(fromSExp startLine)
147 |                               , startCol  = !(fromSExp startCol)
148 |                               , endLine   = !(fromSExp endLine)
149 |                               , endCol    = !(fromSExp endCol)}
150 |            })
151 |            !(fromSExp str)
152 |            !(fromSExp hl)
153 |            !(fromSExp iden)
154 |   fromSExp _ = Nothing
155 |
156 | public export
157 | data Request =
158 |     Cmd IDECommand
159 |
160 | export
161 | SExpable Request where
162 |   toSExp (Cmd cmd) = toSExp cmd
163 |
164 | export
165 | FromSExpable Request where
166 |   fromSExp cmd = do pure $ Cmd !(fromSExp cmd)
167 |