Separate data and control in the interactive protocol

Apart from using JSON messages, the new protocol is essentially the same as the
old one.  Significant differences:

- Instead of crashing, invalid requests (missing fields, unsupported queries,
  etc) now cause F* to print a reasonably helpful diagnostic message.
- Each query now includes an editor-supplied query id, and each response
  contains the id of the corresponding query.
- Some of the queries were renamed (info → lookup, completions → autocomplete)
  for consistency (all query names are now verbs).
- Messages that F* used to print to stdout or stderr are now translated into
  proper JSON messages and labeled with a severity level (a review of these
  messages is needed to decide which of these should be turned into properly
  reported errors or warnings including range information).
- F* now prints the protocol's version and a list of supported interactive
  features before starting the interactive loop.  This lets the Emacs mode do
  dynamic capability detection instead of relying on version numbers. The same
  information is available through a new "describe-protocol" query.
- A failed “push” doesn't require the editor to immediately send a corresponding
  “pop” any more — instead, the pop happens automatically.

Fixes #361, #366, and #828.

src/basic/FStar.Options.fs

@@ -112,6 +112,7 @@ let init () =
         ("hide_uvar_nums"               , Bool false);
         ("hint_info"                    , Bool false);
         ("in"                           , Bool false);
+        ("ide"                          , Bool false);
         ("include"                      , List []);
         ("indent"                       , Bool false);
         ("initial_fuel"                 , Int 2);
@@ -203,6 +204,7 @@ let get_hide_genident_nums      ()      = lookup_opt "hide_genident_nums"
 let get_hide_uvar_nums          ()      = lookup_opt "hide_uvar_nums"           as_bool
 let get_hint_info               ()      = lookup_opt "hint_info"                as_bool
 let get_in                      ()      = lookup_opt "in"                       as_bool
+let get_ide                     ()      = lookup_opt "ide"                      as_bool
 let get_include                 ()      = lookup_opt "include"                  (as_list as_string)
 let get_indent                  ()      = lookup_opt "indent"                   as_bool
 let get_initial_fuel            ()      = lookup_opt "initial_fuel"             as_int
@@ -447,6 +449,11 @@ let rec specs () : list<Getopt.opt> =
         ZeroArgs (fun () -> Bool true),
         "Legacy interactive mode; reads input from stdin");
 
+       ( noshort,
+        "ide",
+        ZeroArgs (fun () -> Bool true),
+        "JSON-based interactive mode for IDEs");
+
        ( noshort,
         "include",
         OneArg ((fun s -> List (List.map String (get_include()) @ [Path s])),
@@ -928,12 +935,14 @@ let full_context_dependency      () = true
 let hide_genident_nums           () = get_hide_genident_nums          ()
 let hide_uvar_nums               () = get_hide_uvar_nums              ()
 let hint_info                    () = get_hint_info                   ()
+let ide                          () = get_ide                         ()
 let indent                       () = get_indent                      ()
 let initial_fuel                 () = min (get_initial_fuel ()) (get_max_fuel ())
 let initial_ifuel                () = min (get_initial_ifuel ()) (get_max_ifuel ())
 let inline_arith                 () = get_inline_arith                ()
-let interactive                  () = get_in                          ()
+let interactive                  () = get_in () || get_ide ()
 let lax                          () = get_lax                         ()
+let legacy_interactive           () = get_in                          ()
 let log_queries                  () = get_log_queries                 ()
 let log_types                    () = get_log_types                   ()
 let max_fuel                     () = get_max_fuel                    ()

src/basic/FStar.Options.fsi

@@ -78,13 +78,15 @@ val full_context_dependency     : unit    -> bool
 val hide_genident_nums          : unit    -> bool
 val hide_uvar_nums              : unit    -> bool
 val hint_info                   : unit    -> bool
+val ide                         : unit    -> bool
 val include_path                : unit    -> list<string>
 val indent                      : unit    -> bool
 val initial_fuel                : unit    -> int
 val initial_ifuel               : unit    -> int
 val inline_arith                : unit    -> bool
 val interactive                 : unit    -> bool
 val lax                         : unit    -> bool
+val legacy_interactive          : unit    -> bool
 val log_queries                 : unit    -> bool
 val log_types                   : unit    -> bool
 val max_fuel                    : unit    -> int

src/basic/ml/FStar_Util.ml

@@ -359,6 +359,7 @@ let default_printer =
 let current_printer = ref default_printer
 let set_printer printer = current_printer := printer
 
+let print_raw s = pr "%s" s; flush stdout
 let print_string s = (!current_printer).printer_prinfo s
 let print_any s = (!current_printer).printer_prinfo (Marshal.to_string s [])
 let strcat s1 s2 = s1 ^ s2
@@ -528,6 +529,8 @@ let rec find_map l f =
      | None -> find_map tl f
      | y -> y
 
+let try_find f l = try Some (List.find f l) with Not_found -> None
+
 let try_find_index f l =
   let rec aux i = function
     | [] -> None

src/basic/util.fs

@@ -341,6 +341,7 @@ let default_printer =
 let current_printer = ref default_printer
 let set_printer printer = current_printer := printer
 
+let print_raw s = pr "%s" s
 let print_string s = (!current_printer).printer_prinfo s
 let print_any s = print_string (spr "%A" s)
 let strcat s1 s2 = s1 ^ s2
@@ -477,6 +478,8 @@ let find_opt f l =
     | hd::tl -> if f hd then Some hd else aux tl in
     aux l
 
+let try_find f l = List.tryFind f l
+
 let try_find_index f l = List.tryFindIndex f l
 
 let sort_with f l = List.sortWith f l

src/basic/util.fsi

@@ -139,6 +139,7 @@ type printer = {
 val default_printer : printer
 val set_printer : printer -> unit
 
+val print_raw : string -> unit
 val print_string : string -> unit
 val print_any : 'a -> unit
 val strcat : string -> string -> string
@@ -237,6 +238,7 @@ val sort_with: ('a -> 'a -> int) -> list<'a> -> list<'a>
 val set_eq: ('a -> 'a -> int) -> list<'a> -> list<'a> -> bool
 val remove_dups: ('a -> 'a -> bool) -> list<'a> -> list<'a>
 val add_unique: ('a -> 'a -> bool) -> 'a -> list<'a> -> list<'a>
+val try_find: ('a -> bool) -> list<'a> -> option<'a>
 val try_find_i: (int -> 'a -> bool) -> list<'a> -> option<(int * 'a)>
 val find_map: list<'a> -> ('a -> option<'b>) -> option<'b>
 val try_find_index: ('a -> bool) -> list<'a> -> option<int>