Add tests

tests/ide/lsp/nonexisting_dependency.in

@@ -0,0 +1,6 @@
+Content-Length: 3960
+
+{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///root/non-existing/fstar/FStar/src/basic/FStar.Const.fst","languageId":"fstar","version":1,"text":"(*\n   Copyright 2008-2020 Microsoft Research\n\n   Licensed under the Apache License, Version 2.0 (the \"License\");\n   you may not use this file except in compliance with the License.\n   You may obtain a copy of the License at\n\n       http://www.apache.org/licenses/LICENSE-2.0\n\n   Unless required by applicable law or agreed to in writing, software\n   distributed under the License is distributed on an \"AS IS\" BASIS,\n   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\n   See the License for the specific language governing permissions and\n   limitations under the License.\n*)\nmodule FStar.Const\nopen FStar.Compiler.Effect module List = FStar.Compiler.List\nopen FStar.Compiler.Effect module List = FStar.Compiler.List\n\nopen FStar.BaseTypes\n\n// IN F*: [@@ PpxDerivingYoJson; PpxDerivingShow ]\ntype signedness = | Unsigned | Signed\n// IN F*: [@@ PpxDerivingYoJson; PpxDerivingShow ]\ntype width = | Int8 | Int16 | Int32 | Int64\n\n(* NB:\n    Const_int (_, None) is not a canonical representation for a mathematical integer\n    e.g., you can have both\n    Const_int(\"0x3ffffff\", None)\n    and\n    Const_int(\"67108863\", None)\n    which represent the same number\n    You should do an \"FStar.Compiler.Util.ensure_decimal\" on the\n    string representation before comparing integer constants.\n\n    eq_const below does that for you\n*)\n\n// IN F*: [@@ PpxDerivingYoJson; PpxDerivingShow ]\ntype sconst =\n  | Const_effect\n  | Const_unit\n  | Const_bool        of bool\n  | Const_int         of string * option (signedness * width) (* When None, means \"mathematical integer\", i.e. Prims.int. *)\n  | Const_char        of char (* unicode code point: char in F#, int in OCaml *)\n  | Const_float       of double\n  | Const_real        of string\n  | Const_bytearray   of array byte * FStar.Compiler.Range.range\n  | Const_string      of string * FStar.Compiler.Range.range                (* UTF-8 encoded *)\n  | Const_range_of                                           (* `range_of` primitive *)\n  | Const_set_range_of                                       (* `set_range_of` primitive *)\n  | Const_range       of FStar.Compiler.Range.range                         (* not denotable by the programmer *)\n  | Const_reify                                              (* a coercion from a computation to a Tot term *)\n  | Const_reflect     of Ident.lid                           (* a coercion from a Tot term to an l-computation type *)\n\nlet eq_const c1 c2 =\n    match c1, c2 with\n    | Const_int (s1, o1), Const_int(s2, o2) ->\n      FStar.Compiler.Util.ensure_decimal s1 = FStar.Compiler.Util.ensure_decimal s2 &&\n      o1=o2\n    | Const_bytearray(a, _), Const_bytearray(b, _) -> a=b\n    | Const_string(a, _), Const_string(b, _) -> a=b\n    | Const_reflect l1, Const_reflect l2 -> Ident.lid_equals l1 l2\n    | _ -> c1=c2\n\nopen FStar.BigInt\nlet rec pow2 (x:bigint) : bigint =\n  if eq_big_int x zero\n  then one\n  else mult_big_int two (pow2 (pred_big_int x))\n\n\nlet bounds signedness width =\n    let n =\n        match width with\n        | Int8 -> big_int_of_string \"8\"\n        | Int16 -> big_int_of_string \"16\"\n        | Int32 -> big_int_of_string \"32\"\n        | Int64 -> big_int_of_string \"64\"\n    in\n    let lower, upper =\n      match signedness with\n      | Unsigned ->\n        zero, pred_big_int (pow2 n)\n      | Signed ->\n        let upper = pow2 (pred_big_int n) in\n        minus_big_int upper, pred_big_int upper\n    in\n    lower, upper\n\nlet within_bounds repr signedness width =\n  let lower, upper = bounds signedness width in\n  let value = big_int_of_string (FStar.Compiler.Util.ensure_decimal repr) in\n  le_big_int lower value && le_big_int value upper\n"}}}
+Content-Length: 46
+
+{"jsonrpc":"2.0","method":"exit","params":{}}

tests/ide/lsp/nonexisting_dependency.out.expected

@@ -0,0 +1,4 @@
+[E] Failed to load deps. Error File /root/non-existing/fstar/FStar/src/basic/FStar.Const.fst could not be found
+Content-Length: 160
+
+{"jsonrpc": "2.0", "method": "textDocument/publishDiagnostics", "params": {"diagnostics": [], "uri": "file:///root/non-existing/fstar/FStar/src/basic/FStar.Const.fst"}}