summaryrefslogtreecommitdiff
path: root/src/lsp.sml
blob: c99a6f2ef61ec887e1aeb507de01f3a2d7820c5f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
structure Lsp :> LSP = struct 

structure C = Compiler
structure P = Print

val debug = LspSpec.debug

structure SK = struct
  type ord_key = string
  val compare = String.compare
end
structure SM = BinaryMapFn(SK)

type fileState =
     { envBeforeThisModule: ElabEnv.env
     , decls: Elab.decl list
     , text: string}
type state =
     { urpPath : string
     , fileStates : fileState SM.map
     }

(* Wrapping this in structure as an attempt to not get concurrency bugs *)
structure State :
          sig
              val init: state -> unit
              val insertText: string -> string -> unit
              val insertElabRes: string -> ElabEnv.env -> Elab.decl list -> unit
              val removeFile: string -> unit
              val withState: (state -> 'a) -> 'a
          end = struct
val stateRef = ref (NONE: state option)
fun init (s: state) = 
    stateRef := SOME s
fun withState (f: state -> 'a): 'a =
    case !stateRef of
        NONE => raise LspSpec.LspError LspSpec.ServerNotInitialized
      | SOME s => f s

fun insertText (fileName: string) (text: string) = 
    withState (fn oldS =>
                  stateRef := SOME { urpPath = #urpPath oldS
                                   , fileStates =
                                     case SM.find (#fileStates oldS, fileName) of
                                         NONE => SM.insert ( #fileStates oldS
                                                           , fileName
                                                           , { text = text
                                                             , decls = []
                                                             , envBeforeThisModule = ElabEnv.empty })
                                       | SOME oldfs => 
                                         SM.insert ( #fileStates oldS
                                                   , fileName
                                                   , { text = text
                                                     , decls = #decls oldfs
                                                     , envBeforeThisModule = #envBeforeThisModule oldfs })
                                   }
              )

fun insertElabRes (fileName: string) (env: ElabEnv.env) decls =
    withState (fn oldS =>
                  stateRef := SOME { urpPath = #urpPath oldS
                                   , fileStates =
                                     case SM.find (#fileStates oldS, fileName) of
                                         NONE => raise Fail ("No text found for file " ^ fileName)
                                       | SOME oldfs => 
                                         SM.insert ( #fileStates oldS
                                                   , fileName
                                                   , { text = #text oldfs
                                                     , decls = decls
                                                     , envBeforeThisModule = env })
                                   }
              )

fun removeFile (fileName: string) =
    withState (fn oldS =>
                  stateRef := SOME { urpPath = #urpPath oldS
                                   , fileStates = #1 (SM.remove (#fileStates oldS, fileName))
                                   }
              )

end



fun scanDir (f: string -> bool) (path: string) =
    let
        val dir = OS.FileSys.openDir path
        fun doScanDir acc =
            case OS.FileSys.readDir dir of 
                NONE => (OS.FileSys.closeDir dir; acc)
             |  SOME fname =>
                (if f fname
                 then doScanDir (fname :: acc)
                 else doScanDir acc)
    in
        doScanDir []
    end

(* Throws Fail if can't init *)
fun initState (initParams: LspSpec.initializeParams): state = 
    let 
        val rootPath = case #rootUri initParams of 
                           NONE => raise Fail "No rootdir found"
                         | SOME a => #path a
        val optsUrpFile =
            (SOME (FromJson.asString (FromJson.get "urpfile" (FromJson.get "project" (FromJson.get "urweb" (#initializationOptions initParams))))))
            handle ex => NONE
        val foundUrps = scanDir (fn fname => OS.Path.ext fname = SOME "urp") rootPath
    in 
        { urpPath = case foundUrps of
                        [] => raise Fail ("No .urp files found in path " ^ rootPath)
                      | one :: [] => OS.Path.base (OS.Path.file one)
                      | many => case List.find (fn m => SOME (OS.Path.base (OS.Path.file m)) = optsUrpFile) many of
                                    NONE => raise Fail ("Found multiple .urp files in path " ^ rootPath)
                                  | SOME f => OS.Path.base (OS.Path.file f)
        , fileStates = SM.empty
        }
    end

fun addSgnToEnv (env: ElabEnv.env) (sgn: Source.sgn_item list) (fileName: string) (addUnprefixed: bool): ElabEnv.env =
    let
        val moduleName = C.moduleOf fileName
        val (sgn, gs) = Elaborate.elabSgn (env, Disjoint.empty) (Source.SgnConst sgn, { file = fileName
                                                                                      , first = ErrorMsg.dummyPos
                                                                                      , last = ErrorMsg.dummyPos })
        val () = case gs of
                     [] => ()
                   | _ => (app (fn (_, env, _, c1, c2) =>
                                   Print.prefaces "Unresolved"
                                                  [("c1", ElabPrint.p_con env c1),
                                                   ("c2", ElabPrint.p_con env c2)]) gs;
                           raise Fail ("Unresolved disjointness constraints in " ^ moduleName ^ " at " ^ fileName)) (* TODO Not sure if this is needed for all signatures or only for Basis *)
        val (env', n) = ElabEnv.pushStrNamed env moduleName sgn
        val (_, env') = if addUnprefixed
                        then Elaborate.dopen env' {str = n, strs = [], sgn = sgn}
                        else ([], env')
    in
        env'
    end

fun errorToDiagnostic (err: { span: ErrorMsg.span , message: string }): LspSpec.diagnostic = 
    { range = { start = { line = #line (#first (#span err)) - 1
                        , character = #char (#first (#span err))
                        }
              , end_ = { line = #line (#last (#span err)) - 1
                       , character = #char (#last (#span err))
                       }
              }
    , severity = 1
    , source = "UrWeb"
    , message = #message err
    }

(* TODO FFI modules ? Check compiler.sml -> parse -> parseFfi *)
(* TODO Optim: cache parsed urp file? *)
fun elabFile (state: state) (fileName: string): ({ decls: Elab.decl list, envBeforeThisModule: ElabEnv.env} option * LspSpec.diagnostic list) =
    let
        val () = if (OS.Path.ext fileName = SOME "ur")
                 then ()
                 else raise Fail ("Can only handle .ur files for now")
        (* val () = Elaborate.unifyMore := true *)
        (* To reuse Basis and Top *)
        val () = Elaborate.incremental := true
        (* Parsing .urp *)
        val job = case C.run (C.transform C.parseUrp "parseUrp") (#urpPath state) of
                      NONE => raise LspSpec.LspError (LspSpec.InternalError ("Couldn't parse .urp file at " ^ (#urpPath state)))
                    | SOME a => a
        val moduleSearchRes =
            List.foldl
                (fn (entry, acc) => if #2 acc
                                    then acc
                                    else
                                        if entry ^ ".ur" = fileName
                                        then (List.rev (#1 acc), true)
                                        else (entry :: #1 acc, false))
                ([] (* modules before *), false (* module found *))
                (#ffi job @ #sources job)
        val modulesBeforeThisFile = #1 moduleSearchRes 
        val () = if #2 moduleSearchRes
                 then ()
                 else raise LspSpec.LspError (LspSpec.InternalError ("Couldn't find file " ^ fileName ^ " referenced in .urp file at " ^ (#urpPath state)))
        (* Parsing .urs files of previous modules *)
        val parsedUrss = List.map (fn entry =>
                                      if OS.FileSys.access (entry ^ ".urs", [])
                                      then case C.run (C.transform C.parseUrs "parseUrs") (entry ^ ".urs") of
                                                NONE => raise LspSpec.LspError (LspSpec.InternalError ("Failed to parse .urs file at " ^ entry))
                                              | SOME a => { fileName = entry ^ ".urs", parsed = a}
                                      else
                                          if OS.FileSys.access (entry ^ ".ur", [])
                                          then case C.run (C.transform C.parseUrs "parseUrs") (entry ^ ".ur") of
                                                   NONE => raise LspSpec.LspError (LspSpec.InternalError ("No .urs file found for " ^ entry ^ " and couldn't parse .ur as .urs file"))
                                                 | SOME a => { fileName = entry ^ ".ur" , parsed = a}
                                          else raise LspSpec.LspError (LspSpec.InternalError ("Couldn't find an .ur or .urs file for " ^ entry)))
                                  modulesBeforeThisFile
        (* Parsing Basis and Top *)
        val basisF = Settings.libFile "basis.urs"
        val topF = Settings.libFile "top.urs"
        val topF' = Settings.libFile "top.ur"

        val tm1 = OS.FileSys.modTime topF
        val tm2 = OS.FileSys.modTime topF'

        val parsedBasisUrs =
            case C.run (C.transform C.parseUrs "parseUrs") basisF of
                NONE => raise LspSpec.LspError (LspSpec.InternalError ("Failed to parse basis.urs file at " ^ basisF))
              | SOME a => a
        val parsedTopUrs =
            case C.run (C.transform C.parseUrs "parseUrs") topF of
                NONE => raise LspSpec.LspError (LspSpec.InternalError ("Failed to parse top.urs file at " ^ topF))
              | SOME a => a
        val parsedTopUr =
            case C.run (C.transform C.parseUr "parseUr") topF' of
                NONE => raise LspSpec.LspError (LspSpec.InternalError ("Failed to parse top.ur file at " ^ topF'))
              | SOME a => a

        (* Parsing .ur and .urs of current file *)
        val (parsedUrs: Source.sgn option) =
            (if OS.FileSys.access (fileName ^ "s", [])
             then
                 case C.run (C.transform C.parseUrs "parseUrs") (fileName ^ "s") of
                     NONE => NONE
                   | SOME a => SOME ( Source.SgnConst a
                                    , {file = fileName ^ "s", first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos})
             else
                 NONE) handle ex => NONE
        val () = ErrorMsg.resetErrors ()
        val (parsedUrO: (Source.decl list) option) =
            C.run (C.transform C.parseUr "parseUr") fileName
    in
        case parsedUrO of
            NONE => (* Parse error *) (NONE, List.map errorToDiagnostic (ErrorMsg.readErrorLog ()))
          | SOME parsedUr => 
            (* Parsing of .ur succeeded *)
            let 
                val loc = {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}
                val envBeforeThisModule = ref ElabEnv.empty
                val res = Elaborate.elabFile
                              parsedBasisUrs tm1 parsedTopUr parsedTopUrs tm2 ElabEnv.empty
                              (* Adding urs's of previous modules to env *)
                              (fn envB =>
                                  let 
                                      val newEnv = List.foldl (fn (sgn, env) => addSgnToEnv env (#parsed sgn) (#fileName sgn) false) envB parsedUrss
                                  in
                                      (envBeforeThisModule := newEnv; newEnv)
                                  end
                              )
                              [( Source.DStr (C.moduleOf fileName, parsedUrs, NONE, (Source.StrConst parsedUr, loc), false)
                               , loc )]
                (* report back errors (as Diagnostics) *)
                val errors = ErrorMsg.readErrorLog ()
                val decls = case List.last res of
                                (Elab.DStr (_, _, _, (Elab.StrConst decls, _)), _) => decls
                              | _ => raise Fail ("Impossible: Source.StrConst did not become Elab.StrConst after elaboration")
            in 
                (SOME { envBeforeThisModule = !envBeforeThisModule, decls = decls },
                 List.map errorToDiagnostic errors)
            end
    end

fun uniq (eq: 'b -> 'b -> bool) (bs: 'b list) =
    case bs of
        [] => []
      | (l as b :: bs') => b :: uniq eq (List.filter (fn a => not (eq a b)) bs')

fun elabFileAndSendDiags (state: state) (toclient: LspSpec.toclient) (documentUri: LspSpec.documentUri): unit =
    let 
        val fileName = #path documentUri
        val res = elabFile state fileName
        fun eq_diag (d1: LspSpec.diagnostic) (d2: LspSpec.diagnostic) = #range d1 = #range d2 andalso #message d1 = #message d2
        val diags = uniq eq_diag (#2 res)
    in
        (case #1 res of
             NONE => ()
           | SOME fs =>
             (State.insertElabRes fileName (#envBeforeThisModule fs) (#decls fs));
         #publishDiagnostics toclient { uri = documentUri , diagnostics = diags})
    end

fun scanDir (f: string -> bool) (path: string) =
    let
        val dir = OS.FileSys.openDir path
        fun doScanDir acc =
            case OS.FileSys.readDir dir of 
                NONE => (OS.FileSys.closeDir dir; acc)
             |  SOME fname =>
                (if f fname
                 then doScanDir (fname :: acc)
                 else doScanDir acc)
    in
        doScanDir []
    end

fun readFile (fileName: string): string =
    let 
        val stream = TextIO.openIn fileName
        fun doReadFile acc = 
            case TextIO.inputLine stream of
                NONE => acc
              | SOME str => (if acc = ""
                             then doReadFile str
                             else doReadFile (acc ^ str))
        val res = doReadFile ""
    in 
        (TextIO.closeIn stream; res)
    end
        

(* TODO PERF BIG I couldn't figure out how to print just to a string, so writing to a temp file, then reading it, then deleting it, ... *)
fun ppToString (pp: Print.PD.pp_desc) (width: int): string =
    let
        val tempfile = OS.FileSys.tmpName ()
        val outStr = TextIO.openOut tempfile
        val outDev = TextIOPP.openOut {dst = outStr, wid = width}
        val () = Print.fprint outDev pp
        val res = readFile tempfile
        val () = TextIO.closeOut outStr
    in
        res
    end

fun getStringAtCursor
    (stopAtCursor: bool)
    (text: string)
    (pos: LspSpec.position)
    : string
    = 
    let
        val line = List.nth (Substring.fields (fn c => c = #"\n") (Substring.full text), #line pos)
        val chars = [ (* #".", *) #"(", #")", #"{", #"}", #"[", #"]", #"<", #">", #"-", #"=", #":", #"@"
                      , #" ", #"\n", #"#", #",", #"*", #"\"", #"|", #"&", #"$", #"^", #"+", #";"]
        val lineUntilCursor = Substring.slice (line, 0, SOME (#character pos))
        val beforeCursor = Substring.string (Substring.taker (fn c => not (List.exists (fn c' => c = c') chars)) lineUntilCursor)
        val afterCursor = if stopAtCursor
                          then ""
                          else let
                              val lineAfterCursor = Substring.slice (line, #character pos, NONE)
                          in
                              Substring.string (Substring.takel (fn c => not (List.exists (fn c' => c = c') (#"." :: chars))) lineAfterCursor)
                          end
    in
        beforeCursor ^ afterCursor
    end

fun formatTypeBox (a: P.PD.pp_desc, b: P.PD.pp_desc) =
    P.PD.hvBox (P.PD.PPS.Rel 0, [a,
                                 P.PD.string ": ",
                                 P.PD.break {nsp = 0, offset = 2},
                                 b])

fun handleHover (state: state) (p: LspSpec.hoverReq): LspSpec.hoverResp LspSpec.result =
    let
        val fileName = #path (#uri (#textDocument p))
        val s = SM.find (#fileStates state, fileName)
    in
        case s of
            NONE => LspSpec.Success NONE
          | SOME s =>
            let 
                val searchString = getStringAtCursor false (#text s) (#position p)
                val env = #envBeforeThisModule s
                val decls = #decls s
                val loc = #position p
                val (env, prefix, found) = GetInfo.findStringInEnv env (Elab.StrConst decls) fileName { line = #line loc + 1
                                                                                                      , char = #character loc + 1} searchString
            in
                case found of
                    NONE => LspSpec.Success NONE
                  | SOME f =>
                    let
                        val desc = case f of
                                       GetInfo.FoundStr (x, (_, sgn)) => formatTypeBox (P.PD.string (prefix ^ x), P.PD.string "module")
                                     | GetInfo.FoundKind (x, kind) => formatTypeBox (P.PD.string (prefix ^ x), ElabPrint.p_kind env kind)
                                     | GetInfo.FoundCon (x, con) => formatTypeBox (P.PD.string (prefix ^ x), ElabPrint.p_con env con)
                    in
                        LspSpec.Success (SOME {contents = ppToString desc 50})
                    end
            end
    end

(* TODO IDEA can we use the real parser to figure out what we're typing (exp, con, field, etc) to predict better? *)
fun handleCompletion (state: state) (p: LspSpec.completionReq) =
    let
        val fileName = #path (#uri (#textDocument p))
        val s = SM.find (#fileStates state, fileName)
    in
        case s of
            NONE => LspSpec.Success { isIncomplete = false, items = []}
          | SOME s =>
            let 
                val pos = #position p
                val searchStr = getStringAtCursor true (#text s) pos
                val env = #envBeforeThisModule s
                val decls = #decls s
                val (env, prefix, foundItems) = GetInfo.matchStringInEnv env (Elab.StrConst decls) fileName { line = #line pos + 1, char = #character pos + 1} searchStr
                val completions = List.map
                                    (fn f => case f of
                                                GetInfo.FoundStr (x, _) => {label = prefix ^ x, kind = LspSpec.Module, detail = ""}
                                              | GetInfo.FoundKind (x, k) => {label = prefix ^ x, kind = LspSpec.Constructor, detail = ppToString (ElabPrint.p_kind env k) 200}
                                              | GetInfo.FoundCon (x, c) => {label = prefix ^ x, kind = LspSpec.Value, detail = ppToString (ElabPrint.p_con env c) 200}
                                    )
                                    foundItems
            in
                LspSpec.Success { isIncomplete = false
                                , items = completions }
            end
    end

fun applyContentChange ((c, s): LspSpec.contentChange * string): string =
    case (#range c, #rangeLength c) of
        (SOME range, SOME _) =>
        let
            val lines = Substring.fields (fn c => c = #"\n") (Substring.full s)
            val linesBefore = List.take (lines, #line (#start range))
            val linesAfter = List.drop (lines, #line (#end_ range) + 1)
            val startLine = List.nth (lines, #line (#start range))
            val startText = Substring.slice (startLine, 0, SOME (#character (#start range))) 
            val endLine = List.nth (lines, #line (#end_ range))
            val endText = Substring.triml (#character (#end_ range)) endLine 
        in
            Substring.concatWith "\n" (linesBefore
                                       @ [Substring.full (Substring.concat [startText, Substring.full (#text c), endText])]
                                       @ linesAfter)
        end
      | _ =>
        #text c

fun handleDocumentDidChange (state: state) (toclient: LspSpec.toclient) (p: LspSpec.didChangeParams): unit =
    let
        val fileName = #path (#uri (#textDocument p))
        val s = SM.find (#fileStates state, fileName)
    in
        case s of
            NONE =>
            (debug ("Got change event for file that isn't open: " ^ fileName);
             (#showMessage toclient) ("Got change event for file that isn't open: " ^ fileName) 1)
          | SOME s =>
            State.insertText fileName (List.foldl applyContentChange (#text s) (#contentChanges p))
    end

fun runInBackground (toclient: LspSpec.toclient) (fileName: string) (f: unit -> unit): unit =
    BgThread.queueBgTask
        fileName
        ((fn () => (f ()
                    handle LspSpec.LspError (LspSpec.InternalError str) => (#showMessage toclient) str 1
                         | LspSpec.LspError LspSpec.ServerNotInitialized => (#showMessage toclient) "Server not initialized" 1
                         | ex => (#showMessage toclient) (General.exnMessage ex) 1
                   ; (#showMessage toclient) ("Done running BG job for " ^ fileName) 3
                   )))

fun handleRequest (requestMessage: LspSpec.message) =
    case requestMessage of
        LspSpec.Notification n =>
        LspSpec.matchNotification
            n
            { initialized = fn () => ()
            , textDocument_didOpen =
              fn (p, toclient) =>
                 (State.insertText (#path (#uri (#textDocument p))) (#text (#textDocument p));
                  runInBackground
                      toclient
                      (#path (#uri (#textDocument p)))
                      (fn () => State.withState (fn state => elabFileAndSendDiags state toclient (#uri (#textDocument p)))))
            , textDocument_didChange =
              fn (p, toclient) =>
                 State.withState (fn state => handleDocumentDidChange state toclient p)
            , textDocument_didSave =
              fn (p, toclient) =>
                 runInBackground
                     toclient
                     (#path (#uri (#textDocument p)))
                     (fn () => State.withState (fn state => elabFileAndSendDiags state toclient (#uri (#textDocument p))))
            , textDocument_didClose =
              fn (p, toclient) =>
                 State.removeFile (#path (#uri (#textDocument p)))
            }
      | LspSpec.RequestMessage m => 
        (* TODO should error handling here be inside handleMessage? *)
        LspSpec.matchMessage
            m
            { initialize = fn p => 
                              (let val st = initState p
                               in
                                   State.init st;
                                   LspSpec.Success
                                       { capabilities =
                                         { hoverProvider = true
                                         , completionProvider = SOME { triggerCharacters = ["."]}
                                         , textDocumentSync = { openClose = true
                                                              , change = 2
                                                              , save = SOME { includeText = false }
                                         }}
                                       }
                               end)
            , shutdown = fn () => LspSpec.Success ()
            , textDocument_hover = fn toclient => State.withState handleHover
            , textDocument_completion = fn p => State.withState (fn s => handleCompletion s p)
        }

fun serverLoop () =            
    if not (Option.isSome (TextIO.canInput (TextIO.stdIn, 1))) andalso BgThread.hasBgTasks ()
    then 
        (* no input waiting -> give control to lower prio thread *)
        BgThread.runBgTaskForABit ()
    else
        let 
            val requestMessage =
                LspSpec.readRequestFromStdIO ()
                handle ex => (debug ("Error in reading from stdIn: " ^ General.exnMessage ex) ; raise ex)
        in
            handleRequest requestMessage
        end

fun startServer () = while true do serverLoop ()
end