Cleanup a bit

5 files changed, 10 insertions, 14 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index f457dcca..2994d95f 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -324,7 +324,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
 let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) :
     extraction_ctx =
   (* Compute and register the type def name *)
-  let ctx, def_name = ctx_add_type_def def ctx in
+  let ctx = ctx_add_type_def def ctx in
   (* Compute and register:
    * - the variant names, if this is an enumeration
    * - the field names, if this is a structure
@@ -597,12 +597,13 @@ let extract_adt_g_value
        * We could update the code to print something of the form:
        * `{ field0=...; ...; fieldn=...; }` in case of structures.
        *)
-      let adt_ident =
+      let cons =
         match variant_id with
         | Some vid -> ctx_get_variant adt_id vid ctx
         | None -> ctx_get_struct adt_id ctx
       in
       if inside && field_values <> [] then F.pp_print_string fmt "(";
+      F.pp_print_string fmt cons;
       let ctx =
         Collections.List.fold_left_link
           (fun () -> F.pp_print_space fmt ())
@@ -875,7 +876,7 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
   let def_name = ctx_get_local_function def.def_id def.back_id ctx in
   (* Add the type parameters - note that we need those bindings only for the
    * body translation (they are not top-level) *)
-  let ctx, type_params = ctx_add_type_params def.signature.type_params ctx in
+  let ctx, _ = ctx_add_type_params def.signature.type_params ctx in
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 7e74835a..66442ec7 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -1,6 +1,5 @@
 (** The following module defines micro-passes which operate on the pure AST *)
 
-open Errors
 open Pure
 open PureUtils
 open TranslateCore
@@ -605,7 +604,9 @@ let filter_unused (filter_monadic_calls : bool) (ctx : trans_ctx)
   (* Return *)
   { def with body; inputs_lvs }
 
-(** Add unit arguments for functions with no arguments, and change their return type. *)
+(** Add unit arguments for functions with no arguments, and change their return type.
+    TODO: filter the backward functions with no outputs.
+ *)
 let to_monadic (def : fun_def) : fun_def =
   (* Update the body *)
   let obj =
@@ -677,7 +678,7 @@ let unit_vars_to_unit (def : fun_def) : fun_def =
   { def with body; inputs_lvs }
 
 (** Unfold the monadic let-bindings to explicit matches. *)
-let unfold_monadic_let_bindings (ctx : trans_ctx) (def : fun_def) : fun_def =
+let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_def) : fun_def =
   (* It is a very simple map *)
   let obj =
     object (self)
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 47097d7d..bd69837a 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -4,7 +4,6 @@
     backends we target.
  *)
 
-open Errors
 open Pure
 open TranslateCore
 module C = Contexts
@@ -386,11 +385,10 @@ let ctx_add_type_def_struct (def : type_def) (ctx : extraction_ctx) :
   let ctx = ctx_add (StructId (AdtId def.def_id)) cons_name ctx in
   (ctx, cons_name)
 
-let ctx_add_type_def (def : type_def) (ctx : extraction_ctx) :
-    extraction_ctx * string =
+let ctx_add_type_def (def : type_def) (ctx : extraction_ctx) : extraction_ctx =
   let def_name = ctx.fmt.type_name def.name in
   let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in
-  (ctx, def_name)
+  ctx
 
 let ctx_add_field (def : type_def) (field_id : FieldId.id) (field : field)
     (ctx : extraction_ctx) : extraction_ctx * string =
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 4eca712a..aad5de15 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -3,7 +3,6 @@
     the symbolic execution: we later apply transformations to generate the
     pure AST that we export. *)
 
-open Identifiers
 module T = Types
 module V = Values
 module E = Expressions
diff --git a/src/main.ml b/src/main.ml
index c52b7bd3..842f06a4 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -6,9 +6,6 @@ module A = CfimAst
 module I = Interpreter
 module EL = Easy_logging.Logging
 module TA = TypesAnalysis
-open PureToExtract
-open ExtractAst
-open ExtractToFStar
 
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work.