Reformat the code

7 files changed, 68 insertions, 22 deletions

diff --git a/compiler/Crates.ml b/compiler/Crates.ml
index 844afb94..eb47a8e1 100644
--- a/compiler/Crates.ml
+++ b/compiler/Crates.ml
@@ -16,6 +16,7 @@ type declaration_group =
   | Global of GlobalDeclId.id
 [@@deriving show]
 
+(** LLBC crate *)
 type llbc_crate = {
   name : string;
   declarations : declaration_group list;
@@ -23,7 +24,6 @@ type llbc_crate = {
   functions : fun_decl list;
   globals : global_decl list;
 }
-(** LLBC crate *)
 
 let compute_defs_maps (c : llbc_crate) :
     type_decl TypeDeclId.Map.t
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 248ad8b3..39f85581 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -11,6 +11,10 @@ open LlbcAst
 open Crates
 module EU = ExpressionsUtils
 
+(** Various information about a function.
+
+    Note that not all this information is used yet to adjust the extraction yet.
+ *)
 type fun_info = {
   can_fail : bool;
   (* Not used yet: all the extracted functions use an error monad *)
@@ -18,13 +22,9 @@ type fun_info = {
   divergent : bool; (* Not used yet *)
 }
 [@@deriving show]
-(** Various information about a function.
 
-    Note that not all this information is used yet to adjust the extraction yet.
- *)
-
-type modules_funs_info = fun_info FunDeclId.Map.t
 (** Various information about a module's functions *)
+type modules_funs_info = fun_info FunDeclId.Map.t
 
 let analyze_module (m : llbc_crate) (funs_map : fun_decl FunDeclId.Map.t)
     (globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) :
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index d74ee85f..0f6ed530 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -110,8 +110,8 @@ let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool)
     ctx
 
 (** Convert an operand constant operand value to a typed value *)
-let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) : V.typed_value
-    =
+let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) :
+    V.typed_value =
   (* Check the type while converting - we actually need some information
      * contained in the type *)
   log#ldebug
@@ -522,7 +522,8 @@ let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)
             | Error _ -> raise (Failure "Disciminant id out of range")
             (* Should really never happen *)
             | Ok sv ->
-                cf { V.value = V.Primitive (PV.Scalar sv); ty = Integer Isize }))
+                cf { V.value = V.Primitive (PV.Scalar sv); ty = Integer Isize })
+        )
     | _ ->
         raise
           (Failure ("Invalid input for `discriminant`: " ^ V.show_typed_value v))
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 1d95c4b9..6dc8b402 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -136,7 +136,8 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
   else
     let value : V.avalue =
       match (v.V.value, ty) with
-      | V.Primitive cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.APrimitive cv
+      | V.Primitive cv, (T.Bool | T.Char | T.Integer _ | T.Str) ->
+          V.APrimitive cv
       | V.Adt adt, T.Adt (id, region_params, tys) ->
           (* Retrieve the types of the fields *)
           let field_types =
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index f5756046..30a89fee 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -42,7 +42,8 @@ let compute_primitive_value_ty (cv : primitive_value) : ty =
   | Char _ -> Char
   | String _ -> Str
 
-let mk_typed_pattern_from_primitive_value (cv : primitive_value) : typed_pattern =
+let mk_typed_pattern_from_primitive_value (cv : primitive_value) : typed_pattern
+    =
   let ty = compute_primitive_value_ty cv in
   { value = PatConstant cv; ty }
 
diff --git a/compiler/Utils.ml b/compiler/Utils.ml
index a285e869..9a79eb55 100644
--- a/compiler/Utils.ml
+++ b/compiler/Utils.ml
@@ -1,6 +1,6 @@
-exception Found
 (** Utility exception
 
     When looking for something while exploring a term, it can be easier to
     just throw an exception to signal we found what we were looking for.
  *)
+exception Found
diff --git a/compiler/dune b/compiler/dune
index 08b0d30f..f0fd2102 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -15,16 +15,59 @@
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
  (libraries ppx_deriving yojson zarith easy_logging core_unix)
- (modules Assumed Collections ConstStrings Contexts Cps Crates Errors
-   Expressions ExpressionsUtils ExtractToFStar FunsAnalysis Identifiers
-   InterpreterBorrowsCore InterpreterBorrows InterpreterExpansion
-   InterpreterExpressions Interpreter InterpreterPaths InterpreterProjectors
-   InterpreterStatements InterpreterUtils Invariants LlbcAst LlbcAstUtils
-   LlbcOfJson Logging Meta Names OfJsonBasic PrePasses Print PrintPure
-   PureMicroPasses Pure PureToExtract PureTypeCheck PureUtils Scalars
-   StringUtils Substitute SymbolicAst SymbolicToPure SynthesizeSymbolic
-   TranslateCore Translate TypesAnalysis Types TypesUtils Utils Values
-   ValuesUtils PrimitiveValues))
+ (modules
+  Assumed
+  Collections
+  ConstStrings
+  Contexts
+  Cps
+  Crates
+  Errors
+  Expressions
+  ExpressionsUtils
+  ExtractToFStar
+  FunsAnalysis
+  Identifiers
+  InterpreterBorrowsCore
+  InterpreterBorrows
+  InterpreterExpansion
+  InterpreterExpressions
+  Interpreter
+  InterpreterPaths
+  InterpreterProjectors
+  InterpreterStatements
+  InterpreterUtils
+  Invariants
+  LlbcAst
+  LlbcAstUtils
+  LlbcOfJson
+  Logging
+  Meta
+  Names
+  OfJsonBasic
+  PrePasses
+  Print
+  PrintPure
+  PureMicroPasses
+  Pure
+  PureToExtract
+  PureTypeCheck
+  PureUtils
+  Scalars
+  StringUtils
+  Substitute
+  SymbolicAst
+  SymbolicToPure
+  SynthesizeSymbolic
+  TranslateCore
+  Translate
+  TypesAnalysis
+  Types
+  TypesUtils
+  Utils
+  Values
+  ValuesUtils
+  PrimitiveValues))
 
 (documentation
  (package aeneas))