18 files changed, 58 insertions, 234 deletions

diff --git a/src/Assumed.ml b/src/Assumed.ml
index b3128b9b..1e8bb669 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -38,13 +38,9 @@ module Sig = struct
   (** A few utilities *)
 
   let rvar_id_0 = T.RegionVarId.of_int 0
-
   let rvar_0 : T.RegionVarId.id T.region = T.Var rvar_id_0
-
   let rg_id_0 = T.RegionGroupId.of_int 0
-
   let tvar_id_0 = T.TypeVarId.of_int 0
-
   let tvar_0 : T.sty = T.TypeVar tvar_id_0
 
   (** Region 'a of id 0 *)
@@ -218,8 +214,7 @@ module Sig = struct
     let inputs =
       [
         mk_ref_ty rvar_0 (mk_vec_ty tvar_0) is_mut (* &'a (mut) Vec<T> *);
-        mk_usize_ty;
-        (* usize *)
+        mk_usize_ty (* usize *);
       ]
     in
     let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in
diff --git a/src/Collections.ml b/src/Collections.ml
index 614857e6..2cb298a7 100644
--- a/src/Collections.ml
+++ b/src/Collections.ml
@@ -88,9 +88,7 @@ module type OrderedType = sig
   include Map.OrderedType
 
   val to_string : t -> string
-
   val pp_t : Format.formatter -> t -> unit
-
   val show_t : t -> string
 end
 
@@ -99,9 +97,7 @@ module OrderedString : OrderedType with type t = string = struct
   include String
 
   let to_string s = s
-
   let pp_t fmt s = Format.pp_print_string fmt s
-
   let show_t s = s
 end
 
@@ -109,7 +105,6 @@ module type Map = sig
   include Map.S
 
   val add_list : (key * 'a) list -> 'a t -> 'a t
-
   val of_list : (key * 'a) list -> 'a t
 
   val to_string : string option -> ('a -> string) -> 'a t -> string
@@ -123,7 +118,6 @@ module type Map = sig
    *)
 
   val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
-
   val show : ('a -> string) -> 'a t -> string
 end
 
@@ -132,7 +126,6 @@ module MakeMap (Ord : OrderedType) : Map with type key = Ord.t = struct
   include Map
 
   let add_list bl m = List.fold_left (fun s (key, e) -> add key e s) m bl
-
   let of_list bl = add_list bl empty
 
   let to_string indent_opt a_to_string m =
@@ -177,7 +170,6 @@ module type Set = sig
   include Set.S
 
   val add_list : elt list -> t -> t
-
   val of_list : elt list -> t
 
   val to_string : string option -> t -> string
@@ -191,7 +183,6 @@ module type Set = sig
    *)
 
   val pp : Format.formatter -> t -> unit
-
   val show : t -> string
 end
 
@@ -200,7 +191,6 @@ module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
   include Set
 
   let add_list bl s = List.fold_left (fun s e -> add e s) s bl
-
   let of_list bl = add_list bl empty
 
   let to_string indent_opt m =
@@ -239,79 +229,43 @@ end
  *)
 module type InjMap = sig
   type key
-
   type elem
-
   type t
 
   val empty : t
-
   val is_empty : t -> bool
-
   val mem : key -> t -> bool
-
   val add : key -> elem -> t -> t
-
   val singleton : key -> elem -> t
-
   val remove : key -> t -> t
-
   val compare : (elem -> elem -> int) -> t -> t -> int
-
   val equal : (elem -> elem -> bool) -> t -> t -> bool
-
   val iter : (key -> elem -> unit) -> t -> unit
-
   val fold : (key -> elem -> 'b -> 'b) -> t -> 'b -> 'b
-
   val for_all : (key -> elem -> bool) -> t -> bool
-
   val exists : (key -> elem -> bool) -> t -> bool
-
   val filter : (key -> elem -> bool) -> t -> t
-
   val partition : (key -> elem -> bool) -> t -> t * t
-
   val cardinal : t -> int
-
   val bindings : t -> (key * elem) list
-
   val min_binding : t -> key * elem
-
   val min_binding_opt : t -> (key * elem) option
-
   val max_binding : t -> key * elem
-
   val max_binding_opt : t -> (key * elem) option
-
   val choose : t -> key * elem
-
   val choose_opt : t -> (key * elem) option
-
   val split : key -> t -> t * elem option * t
-
   val find : key -> t -> elem
-
   val find_opt : key -> t -> elem option
-
   val find_first : (key -> bool) -> t -> key * elem
-
   val find_first_opt : (key -> bool) -> t -> (key * elem) option
-
   val find_last : (key -> bool) -> t -> key * elem
-
   val find_last_opt : (key -> bool) -> t -> (key * elem) option
-
   val to_seq : t -> (key * elem) Seq.t
-
   val to_seq_from : key -> t -> (key * elem) Seq.t
-
   val add_seq : (key * elem) Seq.t -> t -> t
-
   val of_seq : (key * elem) Seq.t -> t
-
   val add_list : (key * elem) list -> t -> t
-
   val of_list : (key * elem) list -> t
 end
 
@@ -322,15 +276,11 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
   module Set = MakeSet (Elem)
 
   type key = Key.t
-
   type elem = Elem.t
-
   type t = { map : elem Map.t; elems : Set.t }
 
   let empty = { map = Map.empty; elems = Set.empty }
-
   let is_empty m = Map.is_empty m.map
-
   let mem k m = Map.mem k m.map
 
   let add k e m =
@@ -345,15 +295,10 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
     | Some x -> { map = Map.remove k m.map; elems = Set.remove x m.elems }
 
   let compare f m1 m2 = Map.compare f m1.map m2.map
-
   let equal f m1 m2 = Map.equal f m1.map m2.map
-
   let iter f m = Map.iter f m.map
-
   let fold f m x = Map.fold f m.map x
-
   let for_all f m = Map.for_all f m.map
-
   let exists f m = Map.exists f m.map
 
   (** Small helper *)
@@ -381,19 +326,12 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
     (map_to_t map1, map_to_t map2)
 
   let cardinal m = Map.cardinal m.map
-
   let bindings m = Map.bindings m.map
-
   let min_binding m = Map.min_binding m.map
-
   let min_binding_opt m = Map.min_binding_opt m.map
-
   let max_binding m = Map.max_binding m.map
-
   let max_binding_opt m = Map.max_binding_opt m.map
-
   let choose m = Map.choose m.map
-
   let choose_opt m = Map.choose_opt m.map
 
   let split k m =
@@ -403,19 +341,12 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
     (l, data, r)
 
   let find k m = Map.find k m.map
-
   let find_opt k m = Map.find_opt k m.map
-
   let find_first k m = Map.find_first k m.map
-
   let find_first_opt k m = Map.find_first_opt k m.map
-
   let find_last k m = Map.find_last k m.map
-
   let find_last_opt k m = Map.find_last_opt k m.map
-
   let to_seq m = Map.to_seq m.map
-
   let to_seq_from k m = Map.to_seq_from k m.map
 
   let rec add_seq s m =
@@ -428,8 +359,6 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
         add_seq s m
 
   let of_seq s = add_seq s empty
-
   let add_list ls m = List.fold_left (fun m (key, elem) -> add key elem m) m ls
-
   let of_list ls = add_list ls empty
 end
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 4f1e1506..716326cf 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -62,7 +62,6 @@ let symbolic_value_id_counter, fresh_symbolic_value_id =
   SymbolicValueId.fresh_stateful_generator ()
 
 let borrow_id_counter, fresh_borrow_id = BorrowId.fresh_stateful_generator ()
-
 let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator ()
 
 let abstraction_id_counter, fresh_abstraction_id =
@@ -217,14 +216,9 @@ type type_context = {
 }
 [@@deriving show]
 
-type fun_context = {
-  fun_decls : fun_decl FunDeclId.Map.t;
-}
-[@@deriving show]
+type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show]
 
-type global_context = {
-  global_decls : global_decl GlobalDeclId.Map.t;
-}
+type global_context = { global_decls : global_decl GlobalDeclId.Map.t }
 [@@deriving show]
 
 type eval_ctx = {
@@ -265,7 +259,8 @@ let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl =
   FunDeclId.Map.find fid ctx.fun_context.fun_decls
 
 (** TODO: make this more efficient with maps *)
-let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : global_decl =
+let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) :
+    global_decl =
   GlobalDeclId.Map.find gid ctx.global_context.global_decls
 
 (** Retrieve a variable's value in an environment *)
diff --git a/src/Errors.ml b/src/Errors.ml
index 69a030b1..31a53cf4 100644
--- a/src/Errors.ml
+++ b/src/Errors.ml
@@ -1,3 +1,2 @@
 exception IntegerOverflow of unit
-
 exception Unimplemented
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 61238aac..9f6a863d 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -13,15 +13,10 @@ module type Id = sig
   (** Id generator - simply a counter *)
 
   val zero : id
-
   val generator_zero : generator
-
   val generator_from_incr_id : id -> generator
-
   val fresh_stateful_generator : unit -> generator ref * (unit -> id)
-
   val mk_stateful_generator : generator -> generator ref * (unit -> id)
-
   val incr : id -> id
 
   (* TODO: this should be stateful! - but we may want to be able to duplicate
@@ -30,29 +25,17 @@ module type Id = sig
      TODO: change the order of the returned types
   *)
   val fresh : generator -> id * generator
-
   val to_string : id -> string
-
   val pp_id : Format.formatter -> id -> unit
-
   val show_id : id -> string
-
   val id_of_json : Yojson.Basic.t -> (id, string) result
-
   val compare_id : id -> id -> int
-
   val max : id -> id -> id
-
   val min : id -> id -> id
-
   val pp_generator : Format.formatter -> generator -> unit
-
   val show_generator : generator -> string
-
   val to_int : id -> int
-
   val of_int : int -> id
-
   val nth : 'a list -> id -> 'a
   (* TODO: change the signature (invert the index and the list *)
 
@@ -75,9 +58,7 @@ module type Id = sig
   val iteri : (id -> 'a -> unit) -> 'a list -> unit
 
   module Ord : C.OrderedType with type t = id
-
   module Set : C.Set with type elt = id
-
   module Map : C.Map with type key = id
 end
 
@@ -88,11 +69,9 @@ end
 module IdGen () : Id = struct
   (* TODO: use Z.t *)
   type id = int [@@deriving show]
-
   type generator = id [@@deriving show]
 
   let zero = 0
-
   let generator_zero = 0
 
   let incr x =
@@ -113,13 +92,9 @@ module IdGen () : Id = struct
     (g, fresh)
 
   let fresh_stateful_generator () = mk_stateful_generator 0
-
   let fresh gen = (gen, incr gen)
-
   let to_string = string_of_int
-
   let to_int x = x
-
   let of_int x = x
 
   let id_of_json js =
@@ -129,13 +104,9 @@ module IdGen () : Id = struct
     | _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js)
 
   let compare_id = compare
-
   let max id0 id1 = if id0 > id1 then id0 else id1
-
   let min id0 id1 = if id0 < id1 then id0 else id1
-
   let nth v id = List.nth v id
-
   let nth_opt v id = List.nth_opt v id
 
   let rec update_nth vec id v =
@@ -158,11 +129,8 @@ module IdGen () : Id = struct
     type t = id
 
     let compare = compare
-
     let to_string = to_string
-
     let pp_t = pp_id
-
     let show_t = show_id
   end
 
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index d47989c3..f2f10944 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -582,7 +582,6 @@ let get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
   let obj =
     object
       inherit [_] V.iter_typed_value
-
       method! visit_loan_content _ lc = raise (FoundLoanContent lc)
     end
   in
@@ -597,7 +596,6 @@ let get_first_borrow_in_value (v : V.typed_value) : V.borrow_content option =
   let obj =
     object
       inherit [_] V.iter_typed_value
-
       method! visit_borrow_content _ bc = raise (FoundBorrowContent bc)
     end
   in
@@ -700,7 +698,6 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool)
   let obj =
     object
       inherit [_] C.iter_eval_ctx as super
-
       method! visit_abs _ abs = super#visit_abs (Some abs) abs
 
       method! visit_abstract_shared_borrows abs asb =
@@ -791,7 +788,6 @@ let update_intersecting_aproj_borrows (can_update_shared : bool)
   let obj =
     object
       inherit [_] C.map_eval_ctx as super
-
       method! visit_abs _ abs = super#visit_abs (Some abs) abs
 
       method! visit_abstract_shared_borrows abs asb =
@@ -920,7 +916,6 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
   let obj =
     object
       inherit [_] C.map_eval_ctx as super
-
       method! visit_abs _ abs = super#visit_abs (Some abs) abs
 
       method! visit_aproj abs sproj =
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 6ef66f1d..fed5ff9b 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -12,33 +12,19 @@ module PA = Print.EvalCtxLlbcAst
 (** Some utilities *)
 
 let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
-
 let ety_to_string = PA.ety_to_string
-
 let rty_to_string = PA.rty_to_string
-
 let symbolic_value_to_string = PA.symbolic_value_to_string
-
 let borrow_content_to_string = PA.borrow_content_to_string
-
 let loan_content_to_string = PA.loan_content_to_string
-
 let aborrow_content_to_string = PA.aborrow_content_to_string
-
 let aloan_content_to_string = PA.aloan_content_to_string
-
 let aproj_to_string = PA.aproj_to_string
-
 let typed_value_to_string = PA.typed_value_to_string
-
 let typed_avalue_to_string = PA.typed_avalue_to_string
-
 let place_to_string = PA.place_to_string
-
 let operand_to_string = PA.operand_to_string
-
 let statement_to_string ctx = PA.statement_to_string ctx "" "  "
-
 let statement_to_string_with_tab ctx = PA.statement_to_string ctx "  " "  "
 
 let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
@@ -211,7 +197,6 @@ let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) :
   let obj =
     object
       inherit [_] V.iter_typed_value
-
       method! visit_Bottom _ = raise Found
 
       method! visit_symbolic_value _ s =
@@ -238,7 +223,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
               raise Found
             else ()
         | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
-        | V.SynthRetGivenBack -> ()
+        | V.SynthRetGivenBack ->
+            ()
         | V.Global -> ()
     end
   in
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 81e35de3..ef255010 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -399,7 +399,6 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
   let visitor =
     object
       inherit [_] C.iter_eval_ctx as super
-
       method! visit_abs _ abs = super#visit_abs (Some abs) abs
 
       method! visit_typed_value info tv =
@@ -705,9 +704,7 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
   let obj =
     object
       inherit [_] C.iter_eval_ctx as super
-
       method! visit_abs _ abs = super#visit_abs (Some abs) abs
-
       method! visit_Symbolic _ sv = add_env_sv sv
 
       method! visit_abstract_shared_borrows abs asb =
diff --git a/src/Names.ml b/src/Names.ml
index 0db5291a..209f8547 100644
--- a/src/Names.ml
+++ b/src/Names.ml
@@ -1,5 +1,4 @@
 open Identifiers
-
 module Disambiguator = IdGen ()
 
 (** See the comments for [Name] *)
@@ -49,11 +48,8 @@ type name = path_elem list [@@deriving show, ord]
 let to_name (ls : string list) : name = List.map (fun s -> Ident s) ls
 
 type module_name = name [@@deriving show, ord]
-
 type type_name = name [@@deriving show, ord]
-
 type fun_name = name [@@deriving show, ord]
-
 type global_name = name [@@deriving show, ord]
 
 (** Filter the disambiguators equal to 0 in a name *)
diff --git a/src/Print.ml b/src/Print.ml
index 6b11a3ff..c10c5989 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -761,11 +761,9 @@ module LlbcAst = struct
       global_decl_id_to_string;
     }
 
-  let fun_decl_to_ast_formatter
-      (type_decls : T.type_decl T.TypeDeclId.Map.t)
+  let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t)
       (fun_decls : A.fun_decl A.FunDeclId.Map.t)
-      (global_decls : A.global_decl A.GlobalDeclId.Map.t)
-      (fdef : A.fun_decl) :
+      (global_decls : A.global_decl A.GlobalDeclId.Map.t) (fdef : A.fun_decl) :
       ast_formatter =
     let rvar_to_string r =
       let rvar = T.RegionVarId.nth fdef.signature.region_params r in
@@ -942,7 +940,8 @@ module LlbcAst = struct
     | A.Assign (p, rv) ->
         indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
     | A.AssignGlobal { dst; global } ->
-        indent ^ fmt.var_id_to_string dst ^ " := global " ^ fmt.global_decl_id_to_string global
+        indent ^ fmt.var_id_to_string dst ^ " := global "
+        ^ fmt.global_decl_id_to_string global
     | A.FakeRead p -> indent ^ "fake_read " ^ place_to_string fmt p
     | A.SetDiscriminant (p, variant_id) ->
         (* TODO: improve this to lookup the variant name by using the def id *)
@@ -1132,11 +1131,9 @@ module Module = struct
 
   (** Generate an [ast_formatter] by using a definition context in combination
       with the variables local to a function's definition *)
-  let def_ctx_to_ast_formatter
-      (type_context : T.type_decl T.TypeDeclId.Map.t)
+  let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t)
       (fun_context : A.fun_decl A.FunDeclId.Map.t)
-      (global_context : A.global_decl A.GlobalDeclId.Map.t)
-      (def : A.fun_decl) :
+      (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) :
       PA.ast_formatter =
     let rvar_to_string vid =
       let var = T.RegionVarId.nth def.signature.region_params vid in
@@ -1188,23 +1185,28 @@ module Module = struct
 
   (** This function pretty-prints a function definition by using a definition
       context *)
-  let fun_decl_to_string
-      (type_context : T.type_decl T.TypeDeclId.Map.t)
+  let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
       (fun_context : A.fun_decl A.FunDeclId.Map.t)
-      (global_context : A.global_decl A.GlobalDeclId.Map.t)
-      (def : A.fun_decl) : string =
-    let fmt = def_ctx_to_ast_formatter type_context fun_context global_context def in
+      (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) :
+      string =
+    let fmt =
+      def_ctx_to_ast_formatter type_context fun_context global_context def
+    in
     PA.fun_decl_to_string fmt "" "  " def
 
   let module_to_string (m : M.llbc_module) : string =
-    let types_defs_map, funs_defs_map, globals_defs_map = M.compute_defs_maps m in
+    let types_defs_map, funs_defs_map, globals_defs_map =
+      M.compute_defs_maps m
+    in
 
     (* The types *)
     let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in
 
     (* The functions *)
     let fun_decls =
-      List.map (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map) m.M.functions
+      List.map
+        (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map)
+        m.M.functions
     in
 
     (* Put everything together *)
diff --git a/src/PureTypeCheck.ml b/src/PureTypeCheck.ml
index 39fb5073..5aefb0be 100644
--- a/src/PureTypeCheck.ml
+++ b/src/PureTypeCheck.ml
@@ -40,7 +40,8 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
 
 type tc_ctx = {
   type_decls : type_decl TypeDeclId.Map.t;  (** The type declarations *)
-  global_decls : A.global_decl A.GlobalDeclId.Map.t;  (** The global declarations *)
+  global_decls : A.global_decl A.GlobalDeclId.Map.t;
+      (** The global declarations *)
   env : ty VarId.Map.t;  (** Environment from variables to types *)
 }
 
@@ -112,7 +113,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
       check_texpression ctx body
   | Qualif qualif -> (
       match qualif.id with
-      | Func   _ -> () (* TODO *)
+      | Func _ -> () (* TODO *)
       | Global _ -> () (* TODO *)
       | Proj { adt_id = proj_adt_id; field_id } ->
           (* Note we can only project fields of structures (not enumerations) *)
diff --git a/src/Scalars.ml b/src/Scalars.ml
index 3324c24b..03ca506c 100644
--- a/src/Scalars.ml
+++ b/src/Scalars.ml
@@ -4,43 +4,24 @@ open Values
 (** The minimum/maximum values an integer type can have depending on its type *)
 
 let i8_min = Z.of_string "-128"
-
 let i8_max = Z.of_string "127"
-
 let i16_min = Z.of_string "-32768"
-
 let i16_max = Z.of_string "32767"
-
 let i32_min = Z.of_string "-2147483648"
-
 let i32_max = Z.of_string "2147483647"
-
 let i64_min = Z.of_string "-9223372036854775808"
-
 let i64_max = Z.of_string "9223372036854775807"
-
 let i128_min = Z.of_string "-170141183460469231731687303715884105728"
-
 let i128_max = Z.of_string "170141183460469231731687303715884105727"
-
 let u8_min = Z.of_string "0"
-
 let u8_max = Z.of_string "255"
-
 let u16_min = Z.of_string "0"
-
 let u16_max = Z.of_string "65535"
-
 let u32_min = Z.of_string "0"
-
 let u32_max = Z.of_string "4294967295"
-
 let u64_min = Z.of_string "0"
-
 let u64_max = Z.of_string "18446744073709551615"
-
 let u128_min = Z.of_string "0"
-
 let u128_max = Z.of_string "340282366920938463463374607431768211455"
 
 (** Being a bit conservative about isize/usize: depending on the system,
@@ -48,11 +29,8 @@ let u128_max = Z.of_string "340282366920938463463374607431768211455"
     want to take that into account in the future *)
 
 let isize_min = i32_min
-
 let isize_max = i32_max
-
 let usize_min = u32_min
-
 let usize_max = u32_max
 
 (** Check that an integer value is in range *)
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index fa244649..a2256bdd 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -114,11 +114,9 @@ let synthesize_function_call (call_id : call_id)
       in
       Some (FunCall (call, expr))
 
-let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value) (expr : expression option)
-    : expression option =
-  match expr with
-  | None   -> None
-  | Some e -> Some (EvalGlobal (gid, dest, e))
+let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value)
+    (expr : expression option) : expression option =
+  match expr with None -> None | Some e -> Some (EvalGlobal (gid, dest, e))
 
 let synthesize_regular_function_call (fun_id : A.fun_id)
     (call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list)
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index e77445cd..326bb05f 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -24,7 +24,7 @@ type global_context = C.global_context [@@deriving show]
 type trans_ctx = {
   type_context : type_context;
   fun_context : fun_context;
-  global_context : global_context
+  global_context : global_context;
 }
 
 type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list
@@ -46,7 +46,9 @@ let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
   let type_decls = ctx.type_context.type_decls in
   let fun_decls = ctx.fun_context.fun_decls in
   let global_decls = ctx.global_context.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 : trans_ctx) (def : Pure.fun_decl) : string =
@@ -54,7 +56,9 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
   let type_decls = ctx.type_context.type_decls in
   let fun_decls = ctx.fun_context.fun_decls in
   let global_decls = ctx.global_context.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
 
 let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string =
diff --git a/src/Types.ml b/src/Types.ml
index 5ff407c9..5bd172cb 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -1,12 +1,8 @@
 open Identifiers
 open Names
-
 module TypeVarId = IdGen ()
-
 module TypeDeclId = IdGen ()
-
 module VariantId = IdGen ()
-
 module FieldId = IdGen ()
 
 module RegionVarId = IdGen ()
@@ -24,7 +20,6 @@ type ('id, 'name) indexed_var = {
 [@@deriving show]
 
 type type_var = (TypeVarId.id, string) indexed_var [@@deriving show]
-
 type region_var = (RegionVarId.id, string option) indexed_var [@@deriving show]
 
 (** A region.
@@ -82,13 +77,10 @@ type integer_type =
 [@@deriving show, ord]
 
 let all_signed_int_types = [ Isize; I8; I16; I32; I64; I128 ]
-
 let all_unsigned_int_types = [ Usize; U8; U16; U32; U64; U128 ]
-
 let all_int_types = List.append all_signed_int_types all_unsigned_int_types
 
 type ref_kind = Mut | Shared [@@deriving show, ord]
-
 type assumed_ty = Box | Vec | Option [@@deriving show, ord]
 
 (** The variant id for `Option::None` *)
@@ -109,15 +101,10 @@ type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty
 class ['self] iter_ty_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
-
     method visit_'r : 'env -> 'r -> unit = fun _ _ -> ()
-
     method visit_id : 'env -> TypeVarId.id -> unit = fun _ _ -> ()
-
     method visit_type_id : 'env -> type_id -> unit = fun _ _ -> ()
-
     method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
-
     method visit_ref_kind : 'env -> ref_kind -> unit = fun _ _ -> ()
   end
 
@@ -125,11 +112,8 @@ class ['self] iter_ty_base =
 class ['self] map_ty_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
-
     method visit_'r : 'env -> 'r -> 'r = fun _ r -> r
-
     method visit_id : 'env -> TypeVarId.id -> TypeVarId.id = fun _ id -> id
-
     method visit_type_id : 'env -> type_id -> type_id = fun _ id -> id
 
     method visit_integer_type : 'env -> integer_type -> integer_type =
@@ -196,7 +180,6 @@ type ety = erased_region ty [@@deriving show, ord]
  *)
 
 type field = { field_name : string option; field_ty : sty } [@@deriving show]
-
 type variant = { variant_name : string; fields : field list } [@@deriving show]
 
 type type_decl_kind =
diff --git a/src/Values.ml b/src/Values.ml
index 13cd2580..fb927fb5 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -65,7 +65,7 @@ type sv_kind =
        *)
   | SynthInputGivenBack
       (** The value was given back upon ending one of the input abstractions *)
-  | Global (** The value is a global *)
+  | Global  (** The value is a global *)
 [@@deriving show]
 
 type symbolic_value = {
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index 2814615c..bc205622 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -11,7 +11,6 @@ let mk_unit_value : typed_value =
   { value = Adt { variant_id = None; field_values = [] }; ty = mk_unit_ty }
 
 let mk_typed_value (ty : ety) (value : value) : typed_value = { value; ty }
-
 let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty }
 
 (** Box a value *)
@@ -38,7 +37,6 @@ let borrows_in_value (v : typed_value) : bool =
   let obj =
     object
       inherit [_] iter_typed_value
-
       method! visit_borrow_content _env _ = raise Found
     end
   in
@@ -53,7 +51,6 @@ let inactivated_in_value (v : typed_value) : bool =
   let obj =
     object
       inherit [_] iter_typed_value
-
       method! visit_InactivatedMutBorrow _env _ = raise Found
     end
   in
@@ -68,7 +65,6 @@ let loans_in_value (v : typed_value) : bool =
   let obj =
     object
       inherit [_] iter_typed_value
-
       method! visit_loan_content _env _ = raise Found
     end
   in
@@ -84,9 +80,7 @@ let outer_loans_in_value (v : typed_value) : bool =
   let obj =
     object
       inherit [_] iter_typed_value
-
       method! visit_loan_content _env _ = raise Found
-
       method! visit_borrow_content _ _ = ()
     end
   in
diff --git a/src/dune b/src/dune
index ba6c076b..ccf726c9 100644
--- a/src/dune
+++ b/src/dune
@@ -1,21 +1,25 @@
 ;; core: for Core.Unix.mkdir_p
+
 (executable
  (name main)
- (preprocess (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
+ (preprocess
+  (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
  (libraries ppx_deriving yojson zarith easy_logging core_unix))
 
 (env
-  (dev (flags
-    :standard
-    -safe-string
-    -g
-    ;-dsource
-    -warn-error -5-8-9-11-14-33-20-21-26-27-39
-  ))
-  (release (flags
-    :standard
-    -safe-string
-    -g
-    ;-dsource
-    -warn-error -5-8-9-11-14-33-20-21-26-27-39
-  )))
+ (dev
+  (flags
+   :standard
+   -safe-string
+   -g
+   ;-dsource
+   -warn-error
+   -5-8-9-11-14-33-20-21-26-27-39))
+ (release
+  (flags
+   :standard
+   -safe-string
+   -g
+   ;-dsource
+   -warn-error
+   -5-8-9-11-14-33-20-21-26-27-39)))