From a0efdaf11337df1fb1a5478f9a193a2737b2665b Mon Sep 17 00:00:00 2001 From: Simon Van Casteren Date: Wed, 11 Dec 2019 12:31:50 +0100 Subject: Fixed parsing errors and loading of interfaces --- src/json.sml | 4 +- src/lsp.sml | 262 ++++++++++++++++++++++++++++++++++++----------------------- 2 files changed, 163 insertions(+), 103 deletions(-) diff --git a/src/json.sml b/src/json.sml index cc9ea6ae..656d28ff 100644 --- a/src/json.sml +++ b/src/json.sml @@ -271,7 +271,9 @@ fun print (ast: json): string = s ^ "\"" | Bool b => if b then "true" else "false" - | Int i => Int.toString i + | Int i => if i >= 0 + then (Int.toString i) + else "-" ^ (Int.toString (Int.abs i)) (* default printing uses ~ instead of - *) | Obj l => "{" ^ List.foldl (fn ((k, v), acc) => acc ^ (if acc = "" then "" else ", ") ^ "\"" ^ k ^ "\": " ^ print v ) "" l ^ "}" diff --git a/src/lsp.sml b/src/lsp.sml index 658ca7a6..34209231 100644 --- a/src/lsp.sml +++ b/src/lsp.sml @@ -294,8 +294,7 @@ structure LspSpec (* :> LSPSPEC *) = struct ])) val toPrint = "Content-Length:" ^ Int.toString (String.size jsonToPrint) ^ "\r\n\r\n" ^ jsonToPrint in - (debug ("Sending diagnostics: " ^ toPrint); - TextIO.print toPrint) + TextIO.print toPrint end val toclient: toclient = {showMessage = showMessage, publishDiagnostics = publishDiagnostics} @@ -375,6 +374,42 @@ end structure Lsp :> LSP = struct + +datatype lspError = InternalError of string +exception LspError of lspError +fun handleLspErrorInNotification (e: lspError) : unit = + let + fun print (message: string) = + let + val jsonStr = Json.print (Json.Obj [ ("jsonrpc", Json.String "2.0") + , ("method", Json.String "window/showMessage") + , ("params", Json.Obj [ ("type", Json.Int 1 (* Error*)) + , ("message", Json.String message)]) + ]) + in + TextIO.print ("Content-Length:" ^ Int.toString (String.size jsonStr) ^ "\r\n\r\n" ^ jsonStr) + end + in + case e of + InternalError str => print str + end +fun handleLspErrorInRequest (id: Json.json) (e: lspError): unit = + let + fun print (code: int) (message: string) = + let + val jsonStr = Json.print (Json.Obj [ ("jsonrpc", Json.String "2.0") + , ("id", id) + , ("error", Json.Obj [ ("code", Json.Int code (* Error*)) + , ("message", Json.String message)]) + ]) + in + TextIO.print ("Content-Length:" ^ Int.toString (String.size jsonStr) ^ "\r\n\r\n" ^ jsonStr) + end + in + case e of + InternalError str => print (~32603) str + end + structure SK = struct type ord_key = string val compare = String.compare @@ -411,7 +446,6 @@ fun initState (initParams: LspSpec.initializeParams): state = val rootPath = case #rootUri initParams of NONE => raise Fail "No rootdir found" | SOME a => #path a - (* val () = debug ("Scanning dir: " ^ rootPath) *) val foundUrps = scanDir (fn fname => OS.Path.ext fname = SOME "urp") rootPath in { urpPath = case foundUrps of @@ -438,110 +472,126 @@ fun addSgnToEnv (env: ElabEnv.env) (sgn: Source.sgn_item list) (fileName: string val (env', n) = ElabEnv.pushStrNamed env moduleName sgn val (_, env') = if addUnprefixed then Elaborate.dopen env' {str = n, strs = [], sgn = sgn} - else ([], env) + else ([], env') in env' end -(* TODO: Any parse error -> valOf fails, throws and server crashes *) -fun calculateFileState (state: state) (fileName: string): (fileState * LspSpec.diagnostic list) = +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 calculateFileState (state: state) (fileName: string): (fileState option * LspSpec.diagnostic list) = let - (* TODO Optim: cache parsed urp file? *) val () = if (OS.Path.ext fileName = SOME "ur") then () else raise Fail ("Can only handle .ur files for now") val () = Elaborate.unifyMore := true - val job = valOf (C.run (C.transform C.parseUrp "parseUrp") (#urpPath state)) - fun entryInUrpToFileName (entry: string) (ext: string) = (#urpPath state) ^ "/" ^ entry ^ ext - val modulesBeforeAndAfterThisFile = - List.partition (fn entry => entryInUrpToFileName entry ".ur" = fileName) (#sources job) - val () = case #2 modulesBeforeAndAfterThisFile of - [] => - (* Module we're handling should always be in here *) - raise Fail ("Couldn't find file " ^ fileName ^ " referenced in .urp file at " ^ (#urpPath state)) - | _ => () + (* Parsing .urp *) + val job = case C.run (C.transform C.parseUrp "parseUrp") (#urpPath state) of + NONE => raise LspError (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 *)) + (#sources job) + val modulesBeforeThisFile = #1 moduleSearchRes + val () = if #2 moduleSearchRes + then () + else raise LspError (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 => let - val fileName = entryInUrpToFileName entry ".urs" + val fileName = entry ^ ".urs" in { fileName = fileName , parsed = if OS.FileSys.access (fileName, []) - then raise (Fail ("Couldn't find an .urs file for " ^ fileName)) - else valOf (C.run (C.transform C.parseUrs "parseUrs") fileName)} + then case C.run (C.transform C.parseUrs "parseUrs") fileName of + NONE => raise LspError (InternalError ("Failed to parse .urs file at " ^ fileName)) + | SOME a => a + else raise LspError (InternalError ("Couldn't find an .urs file for " ^ fileName)) + } end) - (#1 modulesBeforeAndAfterThisFile) - val parsedBasisUrs = valOf (C.run (C.transform C.parseUrs "parseUrs") (Settings.libFile "basis.urs")) - val parsedTopUrs = valOf (C.run (C.transform C.parseUrs "parseUrs") (Settings.libFile "top.urs")) + modulesBeforeThisFile + (* Parsing Basis and Top .urs *) + val parsedBasisUrs = + case C.run (C.transform C.parseUrs "parseUrs") (Settings.libFile "basis.urs") of + NONE => raise LspError (InternalError ("Failed to parse basis.urs file at " ^ (Settings.libFile "basis.urs"))) + | SOME a => a + val parsedTopUrs = + case C.run (C.transform C.parseUrs "parseUrs") (Settings.libFile "top.urs") of + NONE => raise LspError (InternalError ("Failed to parse top.urs file at " ^ (Settings.libFile "top.urs"))) + | SOME a => a + (* Building env with previous .urs files *) val envWithStdLib = addSgnToEnv (addSgnToEnv ElabEnv.empty parsedBasisUrs (Settings.libFile "basis.urs") true) parsedTopUrs (Settings.libFile "top.urs") true val envBeforeThisFile = List.foldl (fn (sgn, env) => addSgnToEnv env (#parsed sgn) (#fileName sgn) false) envWithStdLib parsedUrss - val (parsedUr: Source.decl list) = - valOf (C.run (C.transform C.parseUr "parseUr") fileName) + (* Parsing .ur and .urs of current file *) val (parsedUrs: (Source.sgn_item list) option) = - if OS.FileSys.access (fileName ^ "s", []) then - SOME (valOf (C.run (C.transform C.parseUrs "parseUrs") (fileName ^ "s"))) - else - NONE + (if OS.FileSys.access (fileName ^ "s", []) + then + case C.run (C.transform C.parseUrs "parseUrs") (fileName ^ "s") of + NONE => NONE + | SOME a => SOME a + else + NONE) handle ex => NONE val () = ErrorMsg.resetErrors () - val (str, sgn', gs) = - Elaborate.elabStr - (envBeforeThisFile, Disjoint.empty) - (Source.StrConst parsedUr, {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}) - - (* TODO definitely not sure about this one, just copied from "top" processing *) - (* val () = case gs of *) - (* [] => () *) - (* | _ => app (fn Elaborate.Disjoint (loc, env, denv, c1, c2) => *) - (* (case Disjoint.prove env denv (c1, c2, loc) of *) - (* [] => () *) - (* | _ => *) - (* (Print.prefaces "Unresolved constraint in top.ur" *) - (* [("loc", Print.PD.string (ErrorMsg.spanToString loc)), *) - (* ("c1", ElabPrint.p_con env c1), *) - (* ("c2", ElabPrint.p_con env c2)]; *) - (* raise Fail "Unresolved constraint in top.ur")) *) - (* | Elaborate.TypeClass (env, c, r, loc) => *) - (* let *) - (* val c = normClassKey env c *) - (* in *) - (* case resolveClass env c of *) - (* SOME e => r := SOME e *) - (* | NONE => expError env (Unresolvable (loc, c)) *) - (* end *) - (* ) gs *) - val (sgn, gs) = Elaborate.elabSgn - (envBeforeThisFile, Disjoint.empty) - ( Source.SgnConst (case parsedUrs of NONE => [] | SOME a => a) - , {file = fileName ^ "s", first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}) - val () = case gs of [] => () | _ => raise Fail ("Unresolved disjointness constraints in " ^ fileName) (* TODO not sure? *) - val () = Elaborate.subSgn envBeforeThisFile ErrorMsg.dummySpan sgn' sgn - val errors = ErrorMsg.readErrorLog () - val decls = case str of - (Elab.StrConst decls, _) => decls - | _ => raise Fail ("Impossible: Source.StrConst did not become Elab.StrConst after elaboration") - val () = debug ("Finished calculateFileState for " ^ fileName ^ " with " ^ Int.toString (List.length errors) ^ " errors. " ^ Int.toString (List.length decls) ^ " decls found") + val (parsedUrO: (Source.decl list) option) = + C.run (C.transform C.parseUr "parseUr") fileName in - ({ envOfPreviousModules = envBeforeThisFile - , decls = decls - }, - List.map - (fn err => { 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 - } - ) - errors - ) + case parsedUrO of + NONE => (* Parse error *) (NONE, List.map errorToDiagnostic (ErrorMsg.readErrorLog ())) + | SOME parsedUr => + (* .ur file found -> typecheck *) + let + val (str, sgn', gs) = + Elaborate.elabStr + (envBeforeThisFile, Disjoint.empty) + (Source.StrConst parsedUr, {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}) + val () = + (* .urs file found -> check and compare with .ur file *) + (case parsedUrs of + NONE => () + | SOME parsedUrs => + let + val (sgn, gs) = Elaborate.elabSgn + (envBeforeThisFile, Disjoint.empty) + ( Source.SgnConst parsedUrs + , {file = fileName ^ "s", first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}); + in + Elaborate.subSgn envBeforeThisFile ErrorMsg.dummySpan sgn' sgn + end) + (* report back errors (as Diagnostics) *) + val errors = ErrorMsg.readErrorLog () + val decls = case str of + (Elab.StrConst decls, _) => decls + | _ => raise Fail ("Impossible: Source.StrConst did not become Elab.StrConst after elaboration") + in + (SOME { envOfPreviousModules = envBeforeThisFile + , decls = decls + }, + List.map errorToDiagnostic errors) + end end fun handleFullDocument (state: state) (toclient: LspSpec.toclient) (documentUri: LspSpec.documentUri) = @@ -549,11 +599,14 @@ fun handleFullDocument (state: state) (toclient: LspSpec.toclient) (documentUri: val path = #path documentUri val res = calculateFileState state path in - stateRef := SOME { urpPath = #urpPath state - , fileStates = SM.insert ( #fileStates state - , path - , #1 res) - }; + (case #1 res of + NONE => () + | SOME fs => + stateRef := SOME { urpPath = #urpPath state + , fileStates = SM.insert ( #fileStates state + , path + , fs) + }) ; #publishDiagnostics toclient { uri = documentUri , diagnostics = #2 res} end @@ -590,21 +643,26 @@ fun serverLoop () = | SOME state => (case requestMessage of LspSpec.Notification n => - LspSpec.handleNotification - n - { initialized = fn () => () - , textDocument_didOpen = fn ctx => fn p => handleFullDocument state ctx (#uri (#textDocument p)) - , textDocument_didChange = fn ctx => fn didChangeParams => () - , textDocument_didSave = fn ctx => fn p => handleFullDocument state ctx (#uri (#textDocument p)) - } + ((LspSpec.handleNotification + n + { initialized = fn () => () + , textDocument_didOpen = fn ctx => fn p => handleFullDocument state ctx (#uri (#textDocument p)) + , textDocument_didChange = fn ctx => fn didChangeParams => () + , textDocument_didSave = fn ctx => fn p => handleFullDocument state ctx (#uri (#textDocument p)) + }) + handle LspError e => handleLspErrorInNotification e + | ex => handleLspErrorInNotification (InternalError (General.exnMessage ex))) | LspSpec.RequestMessage m => - LspSpec.handleMessage - m - { initialize = fn _ => LspSpec.Error (~32600, "Server already initialized") - , shutdown = fn () => LspSpec.Success () - , textDocument_hover = fn ctx => fn _ => LspSpec.Success NONE - } - ) handle ex => (debug (General.exnMessage ex); raise ex) + (* TODO should error handling here be inside handleMessage? *) + ((LspSpec.handleMessage + m + { initialize = fn _ => LspSpec.Error (~32600, "Server already initialized") + , shutdown = fn () => LspSpec.Success () + , textDocument_hover = fn ctx => fn _ => LspSpec.Success NONE + }) + handle LspError e => handleLspErrorInRequest (#id m) e + | ex => handleLspErrorInRequest (#id m) (InternalError (General.exnMessage ex))) + ) end fun startServer () = while true do serverLoop () -- cgit v1.2.3