Interactive: Auto-complete options and add hints

2 files changed, 32 insertions, 2 deletions

diff --git a/opam b/opam
index 0ff18a02..3377edf4 100644
--- a/opam
+++ b/opam
@@ -28,7 +28,7 @@ depends: [
   "ocamlbuild"
   "zarith"
   "menhir"
-  "linenoise"
+  "linenoise" {>= "1.1.0"}
   "ott" {>= "0.28"}
   "lem" {>= "2018-12-14"}
   "linksem" {>= "0.3"}
diff --git a/src/isail.ml b/src/isail.ml
index f7b4b1d7..3eea268d 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -552,7 +552,7 @@ let () =
       fun line_so_far ln_completions ->
       let line_so_far, last_id =
         try
-          let p = Str.search_backward (Str.regexp "[^a-zA-Z0-9_/]") line_so_far (String.length line_so_far - 1) in
+          let p = Str.search_backward (Str.regexp "[^a-zA-Z0-9_/-]") line_so_far (String.length line_so_far - 1) in
           Str.string_before line_so_far (p + 1), Str.string_after line_so_far (p + 1)
         with
         | Not_found -> "", line_so_far
@@ -575,6 +575,11 @@ let () =
                     (line_so_far ^ Filename.concat dirname contents.(i) ^ (if is_dir then Filename.dir_sep else ""))
               done
           end
+        else if cmd = ":option" then
+          List.map (fun (opt, _, _) -> opt) options
+          |> List.filter (fun opt -> Str.string_match (Str.regexp_string last_id) opt 0)
+          |> List.map (fun completion -> line_so_far ^ completion)
+          |> List.iter (LNoise.add_completion ln_completions)
         else
           IdSet.elements !vs_ids
           |> List.map string_of_id
@@ -584,6 +589,31 @@ let () =
       else ()
     );
 
+  LNoise.set_hints_callback (
+      fun line_so_far ->
+      let hint str = Some (" " ^ str, LNoise.Yellow, false) in
+      match String.trim line_so_far with
+      | _ when !Interactive.opt_emacs_mode -> None
+      | ":load"  | ":l" -> hint "<sail file>"
+      | ":bind"  | ":b" -> hint "<id> : <type>"
+      | ":infer" | ":i" -> hint "<expression>"
+      | ":type"  | ":t" -> hint "<function id>"
+      | ":let" -> hint "<id> = <expression>"
+      | ":def" -> hint "<definition>"
+      | ":prove" -> hint "<constraint>"
+      | ":assume" -> hint "<constraint>"
+      | str ->
+         let args = Str.split (Str.regexp " +") str in
+         match args with
+         | [":option"] -> hint "<flag>"
+         | [":option"; flag] ->
+            begin match List.find_opt (fun (opt, _, _) -> flag = opt) options with
+            | Some (_, _, help) -> hint (Str.global_replace (Str.regexp " +") " " help)
+            | None -> None
+            end
+         | _ -> None
+    );
+
   (* Read the script file if it is set with the -is option, and excute them *)
   begin
     match !opt_interactive_script with