Fixed parsing errors and loading of interfaces

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 ()