Make minor cleanup

11 files changed, 135 insertions, 131 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index eb88b916..ec0f88a4 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -800,7 +800,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
 (** Simply add the global name to the context. *)
 let extract_global_decl_register_names (ctx : extraction_ctx)
     (def : A.global_decl) : extraction_ctx =
-  ctx_add_global_decl_body def ctx
+  ctx_add_global_decl_and_body def ctx
 
 (** The following function factorizes the extraction of ADT values.
 
@@ -1364,7 +1364,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
 let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) :
     unit =
-  assert (not def.is_global_body);
+  assert (not def.is_global_decl_body);
   (* Retrieve the function name *)
   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
@@ -1552,7 +1552,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
  *)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (global : A.global_decl) (body : fun_decl) (interface : bool) : unit =
-  assert body.is_global_body;
+  assert body.is_global_decl_body;
   assert (Option.is_none body.back_id);
   assert (List.length body.signature.inputs = 0);
   assert (List.length body.signature.doutputs = 1);
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index 2aebc144..615f45b3 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -92,25 +92,25 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
         end
       in
       (* Sanity check: global bodies don't contain stateful calls *)
-      assert ((not f.is_global_body) || not !stateful);
+      assert ((not f.is_global_decl_body) || not !stateful);
       match f.body with
       | None ->
           (* Opaque function: we consider they fail by default *)
           obj#may_fail true;
-          stateful := (not f.is_global_body) && use_state
+          stateful := (not f.is_global_decl_body) && use_state
       | Some body -> obj#visit_statement () body.body
     in
     List.iter visit_fun d;
     (* We need to know if the declaration group contains a global - note that
      * groups containing globals contain exactly one declaration *)
-    let is_global_body = List.exists (fun f -> f.is_global_body) d in
-    assert ((not is_global_body) || List.length d == 1);
+    let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in
+    assert ((not is_global_decl_body) || List.length d == 1);
     (* We ignore on purpose functions that cannot fail and consider they *can*
      * fail: the result of the analysis is not used yet to adjust the translation
      * so that the functions which syntactically can't fail don't use an error monad.
      * However, we do keep the result of the analysis for global bodies.
      * *)
-    can_fail := (not is_global_body) || !can_fail;
+    can_fail := (not is_global_decl_body) || !can_fail;
     { can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
   in
 
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 51144ba2..3a2939ef 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -13,7 +13,7 @@ module SA = SymbolicAst
 (** The local logger *)
 let log = L.interpreter_log
 
-let compute_type_fun_contexts (m : M.llbc_module) :
+let compute_type_fun_global_contexts (m : M.llbc_module) :
     C.type_context * C.fun_context * C.global_context =
   let type_decls_list, _, _ = M.split_declarations m.declarations in
   let type_decls, fun_decls, global_decls = M.compute_defs_maps m in
@@ -28,10 +28,8 @@ let compute_type_fun_contexts (m : M.llbc_module) :
   let global_context = { C.global_decls } in
   (type_context, fun_context, global_context)
 
-let initialize_eval_context
-    (type_context : C.type_context)
-    (fun_context : C.fun_context)
-    (global_context : C.global_context)
+let initialize_eval_context (type_context : C.type_context)
+    (fun_context : C.fun_context) (global_context : C.global_context)
     (type_vars : T.type_var list) : C.eval_ctx =
   C.reset_global_counters ();
   {
@@ -56,12 +54,9 @@ let initialize_eval_context
       - the list of symbolic values introduced for the input values
       - the instantiated function signature
  *)
-let initialize_symbolic_context_for_fun
-    (type_context : C.type_context)
-    (fun_context : C.fun_context)
-    (global_context : C.global_context)
-    (fdef : A.fun_decl) :
-    C.eval_ctx * V.symbolic_value list * A.inst_fun_sig =
+let initialize_symbolic_context_for_fun (type_context : C.type_context)
+    (fun_context : C.fun_context) (global_context : C.global_context)
+    (fdef : A.fun_decl) : C.eval_ctx * V.symbolic_value list * A.inst_fun_sig =
   (* The abstractions are not initialized the same way as for function
    * calls: they contain *loan* projectors, because they "provide" us
    * with the input values (which behave as if they had been returned
@@ -75,7 +70,10 @@ let initialize_symbolic_context_for_fun
    * *)
   let sg = fdef.signature in
   (* Create the context *)
-  let ctx = initialize_eval_context type_context fun_context global_context sg.type_params in
+  let ctx =
+    initialize_eval_context type_context fun_context global_context
+      sg.type_params
+  in
   (* Instantiate the signature *)
   let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in
   let inst_sg = instantiate_fun_sig type_params sg in
@@ -212,8 +210,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return
     - the symbolic AST generated by the symbolic execution
  *)
 let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
-    (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context)
-    (fdef : A.fun_decl) (back_id : T.RegionGroupId.id option) :
+    (type_context : C.type_context) (fun_context : C.fun_context)
+    (global_context : C.global_context) (fdef : A.fun_decl)
+    (back_id : T.RegionGroupId.id option) :
     V.symbolic_value list * SA.expression option =
   (* Debug *)
   let name_to_string () =
@@ -226,7 +225,8 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
 
   (* Create the evaluation context *)
   let ctx, input_svs, inst_sg =
-    initialize_symbolic_context_for_fun type_context fun_context global_context fdef
+    initialize_symbolic_context_for_fun type_context fun_context global_context
+      fdef
   in
 
   (* Create the continuation to finish the evaluation *)
@@ -293,8 +293,12 @@ module Test = struct
     assert (body.A.arg_count = 0);
 
     (* Create the evaluation context *)
-    let type_context, fun_context, global_context = compute_type_fun_contexts m in
-    let ctx = initialize_eval_context type_context fun_context global_context [] in
+    let type_context, fun_context, global_context =
+      compute_type_fun_global_contexts m
+    in
+    let ctx =
+      initialize_eval_context type_context fun_context global_context []
+    in
 
     (* Insert the (uninitialized) local variables *)
     let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in
@@ -338,15 +342,16 @@ module Test = struct
 
   (** Execute the symbolic interpreter on a function. *)
   let test_function_symbolic (config : C.partial_config) (synthesize : bool)
-      (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context)
-      (fdef : A.fun_decl) : unit =
+      (type_context : C.type_context) (fun_context : C.fun_context)
+      (global_context : C.global_context) (fdef : A.fun_decl) : unit =
     (* Debug *)
     log#ldebug
       (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name));
 
     (* Evaluate *)
     let evaluate =
-      evaluate_function_symbolic config synthesize type_context fun_context global_context fdef
+      evaluate_function_symbolic config synthesize type_context fun_context
+        global_context fdef
     in
     (* Execute the forward function *)
     let _ = evaluate None in
@@ -376,12 +381,15 @@ module Test = struct
     in
     (* Filter the opaque functions *)
     let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in
-    let type_context, fun_context, global_context = compute_type_fun_contexts m in
+    let type_context, fun_context, global_context =
+      compute_type_fun_global_contexts m
+    in
     let test_fun (def : A.fun_decl) : unit =
       (* Execute the function - note that as the symbolic interpreter explores
        * all the path, some executions are expected to "panic": we thus don't
        * check the return value *)
-      test_function_symbolic config synthesize type_context fun_context global_context def
+      test_function_symbolic config synthesize type_context fun_context
+        global_context def
     in
     List.iter test_fun no_loop_funs
 end
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index 94566f9b..ccc870dc 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -3,7 +3,6 @@ open Types
 open Values
 open Expressions
 open Identifiers
-
 module FunDeclId = IdGen ()
 module GlobalDeclId = IdGen ()
 
@@ -37,10 +36,7 @@ type assumed_fun_id =
 type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
 [@@deriving show, ord]
 
-type global_assignment = {
-  dst : VarId.id;
-  global : GlobalDeclId.id;
-}
+type global_assignment = { dst : VarId.id; global : GlobalDeclId.id }
 [@@deriving show]
 
 type assertion = { cond : operand; expected : bool } [@@deriving show]
@@ -84,22 +80,16 @@ class ['self] iter_statement_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
 
-    method visit_global_assignment : 'env -> global_assignment -> unit = fun _ _ -> ()
+    method visit_global_assignment : 'env -> global_assignment -> unit =
+      fun _ _ -> ()
 
     method visit_place : 'env -> place -> unit = fun _ _ -> ()
-
     method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> ()
-
     method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> ()
-
     method visit_assertion : 'env -> assertion -> unit = fun _ _ -> ()
-
     method visit_operand : 'env -> operand -> unit = fun _ _ -> ()
-
     method visit_call : 'env -> call -> unit = fun _ _ -> ()
-
     method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
-
     method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> ()
   end
 
@@ -108,18 +98,15 @@ class ['self] map_statement_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
 
-    method visit_global_assignment : 'env -> global_assignment -> global_assignment = fun _ x -> x
+    method visit_global_assignment
+        : 'env -> global_assignment -> global_assignment =
+      fun _ x -> x
 
     method visit_place : 'env -> place -> place = fun _ x -> x
-
     method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x
-
     method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x
-
     method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x
-
     method visit_operand : 'env -> operand -> operand = fun _ x -> x
-
     method visit_call : 'env -> call -> call = fun _ x -> x
 
     method visit_integer_type : 'env -> integer_type -> integer_type =
@@ -190,14 +177,14 @@ type fun_decl = {
   name : fun_name;
   signature : fun_sig;
   body : fun_body option;
-  is_global_body : bool;
+  is_global_decl_body : bool;
 }
 [@@deriving show]
 
 type global_decl = {
   def_id : GlobalDeclId.id;
-  body_id: FunDeclId.id;
+  body_id : FunDeclId.id;
   name : global_name;
-  ty: ety;
+  ty : ety;
 }
 [@@deriving show]
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 846d7232..4e10c642 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -631,7 +631,7 @@ let fun_decl_of_json (js : json) : (A.fun_decl, string) result =
         let* name = fun_name_of_json name in
         let* signature = fun_sig_of_json signature in
         let* body = option_of_json fun_body_of_json body in
-        Ok { A.def_id; name; signature; body; is_global_body = false }
+        Ok { A.def_id; name; signature; body; is_global_decl_body = false }
     | _ -> Error "")
 
 (* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
@@ -670,8 +670,13 @@ let global_decl_of_json (js : json) (gid_conv : global_id_converter) :
         in
         Ok
           ( { A.def_id = global_id; body_id = fun_id; name; ty },
-            { A.def_id = fun_id; name; signature; body; is_global_body = true }
-          )
+            {
+              A.def_id = fun_id;
+              name;
+              signature;
+              body;
+              is_global_decl_body = true;
+            } )
     | _ -> Error "")
 
 let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
diff --git a/src/Pure.ml b/src/Pure.ml
index 5244b0bc..ced56c6a 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -575,6 +575,6 @@ type fun_decl = {
           (to identify the forward/backward functions) later.
        *)
   signature : fun_sig;
-  is_global_body : bool;
+  is_global_decl_body : bool;
   body : fun_body option;
 }
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index b7d45deb..255d4e1b 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -29,11 +29,8 @@ module StringSet = Collections.MakeSet (Collections.OrderedString)
 module StringMap = Collections.MakeMap (Collections.OrderedString)
 
 type name = Names.name
-
 type type_name = Names.type_name
-
 type global_name = Names.global_name
-
 type fun_name = Names.fun_name
 
 (* TODO: this should a module we give to a functor! *)
@@ -229,11 +226,8 @@ module IdOrderedType = struct
   type t = id
 
   let compare = compare_id
-
   let to_string = show_id
-
   let pp_t = pp_id
-
   let show_t = show_id
 end
 
@@ -452,13 +446,11 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string =
 let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
   ctx_get (GlobalId id) ctx
 
-let ctx_get_function (id : A.fun_id)
-    (rg : RegionGroupId.id option)
+let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option)
     (ctx : extraction_ctx) : string =
   ctx_get (FunId (id, rg)) ctx
 
-let ctx_get_local_function (id : A.FunDeclId.id)
-    (rg : RegionGroupId.id option)
+let ctx_get_local_function (id : A.FunDeclId.id) (rg : RegionGroupId.id option)
     (ctx : extraction_ctx) : string =
   ctx_get_function (A.Regular id) rg ctx
 
@@ -582,7 +574,7 @@ let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) :
   let name = ctx.fmt.decreases_clause_name def.def_id def.basename in
   ctx_add (DecreasesClauseId (A.Regular def.def_id)) name ctx
 
-let ctx_add_global_decl_body (def : A.global_decl) (ctx : extraction_ctx) :
+let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let name = ctx.fmt.global_name def.name in
   let decl = GlobalId def.def_id in
@@ -622,9 +614,8 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
     ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs)
   in
   (* Add the function name if it's not a global *)
-  if def.is_global_body
-    then ctx
-    else ctx_add (FunId (def_id, def.back_id)) name ctx
+  if def.is_global_decl_body then ctx
+  else ctx_add (FunId (def_id, def.back_id)) name ctx
 
 type names_map_init = {
   keywords : string list;
@@ -690,11 +681,8 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
     information.
     TODO: move all those helpers.
 *)
-let default_fun_suffix
-    (num_region_groups : int)
-    (rg : region_group_info option)
-    ((keep_fwd, num_backs) : bool * int)
-    : string =
+let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
+    ((keep_fwd, num_backs) : bool * int) : string =
   (* There are several cases:
      - [rg] is `Some`: this is a forward function:
        - we add "_fwd"
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 4b0a04ca..5a21e637 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -219,7 +219,7 @@ let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) (op : E.operand) :
   | E.Move p -> E.Move (p_subst p)
   | E.Constant (ety, cv) ->
       let rsubst x = x in
-      E.Constant ( ty_substitute rsubst tsubst ety, cv )
+      E.Constant (ty_substitute rsubst tsubst ety, cv)
 
 (** Apply a type substitution to an rvalue *)
 let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) (rv : E.rvalue) :
@@ -281,7 +281,9 @@ let rec statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
       let p = place_substitute tsubst p in
       let rvalue = rvalue_substitute tsubst rvalue in
       A.Assign (p, rvalue)
-  | A.AssignGlobal g -> A.AssignGlobal g
+  | A.AssignGlobal g ->
+      (* Globals don't have type parameters *)
+      A.AssignGlobal g
   | A.FakeRead p ->
       let p = place_substitute tsubst p in
       A.FakeRead p
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 81af6a8b..f321ce8c 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -72,9 +72,7 @@ type fun_context = {
   fun_infos : FA.fun_info A.FunDeclId.Map.t;
 }
 
-type global_context = {
-  llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t;
-}
+type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t }
 
 type call_info = {
   forward : S.call;
@@ -127,29 +125,31 @@ type bs_ctx = {
 
 let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
   let env = VarId.Map.empty in
-  let ctx = {
-    PureTypeCheck.type_decls = ctx.type_context.type_decls; 
-    global_decls = ctx.global_context.llbc_global_decls;
-    env
-  } in
+  let ctx =
+    {
+      PureTypeCheck.type_decls = ctx.type_context.type_decls;
+      global_decls = ctx.global_context.llbc_global_decls;
+      env;
+    }
+  in
   let _ = PureTypeCheck.check_typed_pattern ctx v in
   ()
 
 let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
   let env = VarId.Map.empty in
-  let ctx = {
-    PureTypeCheck.type_decls = ctx.type_context.type_decls;
-    global_decls = ctx.global_context.llbc_global_decls;
-    env
-  } in
+  let ctx =
+    {
+      PureTypeCheck.type_decls = ctx.type_context.type_decls;
+      global_decls = ctx.global_context.llbc_global_decls;
+      env;
+    }
+  in
   PureTypeCheck.check_texpression ctx e
 
 (* TODO: move *)
 let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.LlbcAst.ast_formatter =
-  Print.LlbcAst.fun_decl_to_ast_formatter
-    ctx.type_context.llbc_type_decls
-    ctx.fun_context.llbc_fun_decls
-    ctx.global_context.llbc_global_decls
+  Print.LlbcAst.fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
+    ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls
     ctx.fun_decl
 
 let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
@@ -179,7 +179,9 @@ let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
-  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
+  let fmt =
+    PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
+  in
   PrintPure.fun_sig_to_string fmt sg
 
 let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
@@ -187,7 +189,9 @@ let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
-  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
+  let fmt =
+    PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
+  in
   PrintPure.fun_decl_to_string fmt def
 
 (* TODO: move *)
@@ -214,8 +218,8 @@ let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
     T.type_decl =
   TypeDeclId.Map.find id ctx.type_context.llbc_type_decls
 
-let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : A.fun_decl
-    =
+let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
+    A.fun_decl =
   A.FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls
 
 (* TODO: move *)
@@ -1462,9 +1466,8 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
         given_back_inputs next_e
 
 and translate_global_eval (config : config) (gid : A.GlobalDeclId.id)
-  (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx)
-    : texpression =
-  let (ctx, var) = fresh_var_for_symbolic_value sval ctx in
+    (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression =
+  let ctx, var = fresh_var_for_symbolic_value sval ctx in
   let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in
   let global_expr = { id = Global gid; type_args = [] } in
   (* We use translate_fwd_ty to translate the global type *)
@@ -1751,7 +1754,16 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
         Some { inputs; inputs_lvs; body }
   in
   (* Assemble the declaration *)
-  let def = { def_id; back_id = bid; basename; signature; is_global_body = def.is_global_body; body } in
+  let def =
+    {
+      def_id;
+      back_id = bid;
+      basename;
+      signature;
+      is_global_decl_body = def.is_global_decl_body;
+      body;
+    }
+  in
   (* Debugging *)
   log#ldebug
     (lazy
diff --git a/src/Translate.ml b/src/Translate.ml
index 25aff2b2..c9dc7943 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -64,9 +64,7 @@ let translate_function_to_symbolics (config : C.partial_config)
       ^ Print.fun_name_to_string fdef.A.name));
 
   let { type_context; fun_context; global_context } = trans_ctx in
-  let fun_context = {
-    C.fun_decls = fun_context.fun_decls;
-  } in
+  let fun_context = { C.fun_decls = fun_context.fun_decls } in
 
   match fdef.body with
   | None -> None
@@ -75,9 +73,8 @@ let translate_function_to_symbolics (config : C.partial_config)
       let synthesize = true in
       let evaluate gid =
         let inputs, symb =
-          evaluate_function_symbolic config synthesize
-            type_context fun_context global_context
-            fdef gid
+          evaluate_function_symbolic config synthesize type_context fun_context
+            global_context fdef gid
         in
         (inputs, Option.get symb)
       in
@@ -102,8 +99,7 @@ let translate_function_to_symbolics (config : C.partial_config)
 let translate_function_to_pure (config : C.partial_config)
     (mp_config : Micro.config) (trans_ctx : trans_ctx)
     (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t)
-    (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
-    (fdef : A.fun_decl)
+    (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl)
     : pure_fun_translation =
   (* Debug *)
   log#ldebug
@@ -144,9 +140,8 @@ let translate_function_to_pure (config : C.partial_config)
       fun_infos = fun_context.fun_infos;
     }
   in
-  let global_context = {
-      SymbolicToPure.llbc_global_decls = global_context.global_decls
-    }
+  let global_context =
+    { SymbolicToPure.llbc_global_decls = global_context.global_decls }
   in
   let ctx =
     {
@@ -297,12 +292,14 @@ let translate_module_to_pure (config : C.partial_config)
   log#ldebug (lazy "translate_module_to_pure");
 
   (* Compute the type and function contexts *)
-  let type_context, fun_context, global_context = compute_type_fun_contexts m in
-  let fun_infos = FA.analyze_module m fun_context.C.fun_decls global_context.C.global_decls use_state in
-  let fun_context = {
-    fun_decls = fun_context.fun_decls;
-    fun_infos;
-  } in
+  let type_context, fun_context, global_context =
+    compute_type_fun_global_contexts m
+  in
+  let fun_infos =
+    FA.analyze_module m fun_context.C.fun_decls global_context.C.global_decls
+      use_state
+  in
+  let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in
   let trans_ctx = { type_context; fun_context; global_context } in
 
   (* Translate all the type definitions *)
@@ -498,8 +495,9 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
          if
            ((not is_opaque) && config.extract_transparent)
            || (is_opaque && config.extract_opaque)
-         then ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def
-        )
+         then
+           ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif
+             has_decr_clause def)
        fls);
     (* Insert unit tests if necessary *)
     if config.test_unit_functions then
@@ -514,13 +512,18 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
   let export_global (id : A.GlobalDeclId.id) : unit =
     let global_decls = ctx.extract_ctx.trans_ctx.global_context.global_decls in
     let global = A.GlobalDeclId.Map.find id global_decls in
-    let (_, (body, body_backs)) = A.FunDeclId.Map.find global.body_id ctx.trans_funs in
+    let _, (body, body_backs) =
+      A.FunDeclId.Map.find global.body_id ctx.trans_funs
+    in
     assert (List.length body_backs = 0);
-    
+
     let is_opaque = Option.is_none body.Pure.body in
-    if ((not is_opaque) && config.extract_transparent)
-         || (is_opaque  && config.extract_opaque)
-    then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt global body config.interface
+    if
+      ((not is_opaque) && config.extract_transparent)
+      || (is_opaque && config.extract_opaque)
+    then
+      ExtractToFStar.extract_global_decl ctx.extract_ctx fmt global body
+        config.interface
   in
 
   let export_state_type () : unit =
@@ -558,8 +561,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         in
         (* Translate *)
         export_functions true pure_funs
-    | Global id ->
-        export_global id
+    | Global id -> export_global id
   in
 
   (* If we need to export the state type: we try to export it after we defined
@@ -677,8 +679,9 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
       ctx trans_funs
   in
 
-  let ctx = List.fold_left
-    ExtractToFStar.extract_global_decl_register_names ctx m.globals
+  let ctx =
+    List.fold_left ExtractToFStar.extract_global_decl_register_names ctx
+      m.globals
   in
 
   (* Open the output file *)
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index 8088be7f..b5ea6fca 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -87,7 +87,6 @@ let rty_regions (ty : rty) : RegionId.Set.t =
   let obj =
     object
       inherit [_] iter_ty
-
       method! visit_'r _env r = add_region r
     end
   in