Nits

src/extraction/FStarC.Extraction.ML.PrintML.fsti

@@ -17,4 +17,8 @@ module FStarC.Extraction.ML.PrintML
 
 open FStarC.Extraction.ML.Syntax
 
-val print: option string -> string -> mllib -> unit
+val print
+  (odir : option string)
+  (extension : string)
+  (defs : mllib)
+  : unit

src/fstar/FStarC.Main.fst

@@ -69,6 +69,7 @@ let report_errors fmods =
   end
 
 let load_native_tactics () =
+    let open FStarC.Errors.Msg in
     let modules_to_load = Options.load() |> List.map Ident.lid_of_str in
     let cmxs_to_load = Options.load_cmxs () |> List.map Ident.lid_of_str in
     let ml_module_name m = FStarC.Extraction.ML.Util.ml_module_name_of_lid m in
@@ -83,15 +84,19 @@ let load_native_tactics () =
           else  //else try to find and compile the ml file
             match Find.find_file_odir (ml_file m) with
             | None ->
-              E.raise_error0 E.Fatal_FailToCompileNativeTactic
-                (Util.format1 "Failed to compile native tactic; extracted module %s not found" (ml_file m))
+              E.raise_error0 E.Fatal_FailToCompileNativeTactic [
+                text "Failed to compile native tactic.";
+                text (format1 "Extracted module %s not found." (ml_file m))
+              ]
             | Some ml ->
               let dir = Util.dirname ml in
               Plugins.compile_modules dir [ml_module_name m];
               begin match Find.find_file_odir cmxs with
                 | None ->
-                  E.raise_error0 E.Fatal_FailToCompileNativeTactic
-                    (Util.format1 "Failed to compile native tactic; compiled object %s not found" cmxs)
+                  E.raise_error0 E.Fatal_FailToCompileNativeTactic [
+                    text "Failed to compile native tactic.";
+                    text (format1 "Compilation seemingly succeeded, but compiled object %s not found." cmxs);
+                  ]
                 | Some f -> f
               end
     in

src/interactive/FStarC.Interactive.Ide.Types.fst

@@ -38,6 +38,13 @@ module SS = FStarC.Syntax.Syntax
 let initial_range =
   Range.mk_range "<input>" (Range.mk_pos 1 0) (Range.mk_pos 1 0)
 
+instance showable_push_kind : showable push_kind = {
+  show = (function
+          | SyntaxCheck -> "SyntaxCheck"
+          | LaxCheck -> "LaxCheck"
+          | FullCheck -> "FullCheck");
+}
+
 (*************************)
 (* REPL tasks and states *)
 (*************************)
@@ -98,22 +105,15 @@ let repl_state_to_string (r:repl_state)
        | Some m -> Ident.string_of_lid m.name);
       string_of_repl_stack r.repl_deps_stack]
 
-
 let push_query_to_string pq =
-  let pk =
-    match pq.push_kind with
-    | SyntaxCheck -> "SyntaxCheck"
-    | LaxCheck -> "LaxCheck"
-    | FullCheck -> "FullCheck"
-  in
   let code_or_decl =
     match pq.push_code_or_decl with
     | Inl code -> code
     | Inr (_decl, code) -> code.code
   in
   FStarC.Util.format "{ push_kind = %s; push_line = %s; \
                push_column = %s; push_peek_only = %s; push_code_or_decl = %s }"
-    [pk; string_of_int pq.push_line;
+    [show pq.push_kind; string_of_int pq.push_line;
      string_of_int pq.push_column;
      string_of_bool pq.push_peek_only;
      code_or_decl]

src/interactive/FStarC.Interactive.Ide.Types.fsti

@@ -36,6 +36,8 @@ val initial_range : range
 
 type push_kind = | SyntaxCheck | LaxCheck | FullCheck
 
+instance val showable_push_kind : Class.Show.showable push_kind
+
 type completion_context =
 | CKCode
 | CKOption of bool (* #set-options (false) or #reset-options (true) *)

src/interactive/FStarC.Interactive.Ide.fst

@@ -29,6 +29,8 @@ open FStarC.Interactive.PushHelper
 open FStarC.Interactive.Ide.Types
 module BU = FStarC.Util
 
+open FStarC.Class.Show
+
 let dbg = Debug.get_toggle "IDE"
 
 open FStarC.Universal

src/parser/FStarC.Parser.Dep.fst

@@ -25,12 +25,8 @@ module FStarC.Parser.Dep
 open FStarC
 open FStarC.Effect   //for ref, failwith etc
 open FStarC.List
-open FStarC.Parser
 open FStarC.Parser.AST
-open FStarC.Util
 open FStarC.Const
-open FStar.String
-open FStarC.Ident
 open FStarC.Errors
 open FStarC.Class.Show
 
@@ -142,10 +138,10 @@ let module_name_of_file f =
 let lowercase_module_name f = String.lowercase (module_name_of_file f)
 
 let namespace_of_module f =
-    let lid = FStarC.Ident.lid_of_path (FStarC.Ident.path_of_text f) Range.dummyRange in
+    let lid = Ident.lid_of_path (Ident.path_of_text f) Range.dummyRange in
     match ns_of_lid lid with
     | [] -> None
-    | ns -> Some (FStarC.Ident.lid_of_ids ns)
+    | ns -> Some (Ident.lid_of_ids ns)
 
 type file_name = string
 type dependence =

src/parser/FStarC.Parser.Dep.fsti

@@ -17,7 +17,6 @@ module FStarC.Parser.Dep
 
 open FStarC
 open FStarC.Effect
-open FStarC.Parser.AST
 open FStarC.Util
 open FStarC.Ident