fix: formattting

src/bin/dune

@@ -249,6 +249,6 @@
   (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean
    as
    src/sail_lean_backend/Sail/Sail.lean)
-   (%{workspace_root}/src/sail_lean_backend/Sail/BitVec.lean
+  (%{workspace_root}/src/sail_lean_backend/Sail/BitVec.lean
    as
    src/sail_lean_backend/Sail/BitVec.lean)))

src/sail_lean_backend/pretty_print_lean.ml

@@ -280,23 +280,23 @@ let lean_escape_string s = Str.global_replace (Str.regexp "\"") "\"\"" s
 
 let doc_lit (L_aux (lit, l)) =
   match lit with
-  | L_unit  -> string "()"
-  | L_zero  -> string "0#1"
-  | L_one   -> string "1#1" 
+  | L_unit -> string "()"
+  | L_zero -> string "0#1"
+  | L_one -> string "1#1"
   | L_false -> string "false"
-  | L_true  -> string "true"
+  | L_true -> string "true"
   | L_num i -> doc_big_int i
   | L_hex n -> utf8string ("0x" ^ n)
   | L_bin n -> utf8string ("0b" ^ n)
   | L_undef -> utf8string "(Fail \"undefined value of unsupported type\")"
   | L_string s -> utf8string ("\"" ^ lean_escape_string s ^ "\"")
   | L_real s -> utf8string s (* TODO test if this is really working *)
 
-let doc_vec_lit (L_aux (lit, _) as l) = 
+let doc_vec_lit (L_aux (lit, _) as l) =
   match lit with
   | L_zero -> string "0"
-  | L_one  -> string "1"
-  | _ -> failwith "Unexpected litteral found in vector: " ^^  doc_lit l
+  | L_one -> string "1"
+  | _ -> failwith "Unexpected litteral found in vector: " ^^ doc_lit l
 
 let string_of_exp_con (E_aux (e, _)) =
   match e with
@@ -367,20 +367,19 @@ let rec doc_pat ?(in_vector = false) (P_aux (p, (l, annot)) as pat) =
   | P_wild -> underscore
   | P_lit lit when in_vector -> doc_vec_lit lit
   | P_lit lit -> doc_lit lit
-  | P_typ (Typ_aux (Typ_id (Id_aux (Id "bit", _)),_), p) when in_vector -> 
-    doc_pat p ^^ string ":1"
-  | P_typ (Typ_aux (Typ_app (Id_aux (Id id, _), [A_aux (A_nexp (Nexp_aux (Nexp_constant i,_)), _)]),_), p)
-    when in_vector && (id = "bits" || id = "bitvector") -> 
-    doc_pat p ^^ (string ":") ^^ doc_big_int i
+  | P_typ (Typ_aux (Typ_id (Id_aux (Id "bit", _)), _), p) when in_vector -> doc_pat p ^^ string ":1"
+  | P_typ (Typ_aux (Typ_app (Id_aux (Id id, _), [A_aux (A_nexp (Nexp_aux (Nexp_constant i, _)), _)]), _), p)
+    when in_vector && (id = "bits" || id = "bitvector") ->
+      doc_pat p ^^ string ":" ^^ doc_big_int i
   | P_typ (ptyp, p) -> doc_pat p
   | P_id id -> fixup_match_id id |> doc_id_ctor
   | P_tuple pats -> separate (string ", ") (List.map doc_pat pats) |> parens
   | P_list pats -> separate (string ", ") (List.map doc_pat pats) |> brackets
   | P_vector pats -> concat (List.map (doc_pat ~in_vector:true) pats)
-  | P_vector_concat (pats) -> separate (string ",") (List.map (doc_pat ~in_vector:true) pats) |> brackets
+  | P_vector_concat pats -> separate (string ",") (List.map (doc_pat ~in_vector:true) pats) |> brackets
   | P_app (Id_aux (Id "None", _), p) -> string "none"
   | P_app (cons, pats) -> doc_id_ctor (fixup_match_id cons) ^^ space ^^ separate_map (string ", ") doc_pat pats
-  | P_as (pat,id) -> doc_pat pat
+  | P_as (pat, id) -> doc_pat pat
   | _ -> failwith ("Doc Pattern " ^ string_of_pat_con pat ^ " " ^ string_of_pat pat ^ " not translatable yet.")
 
 (* Copied from the Coq PP *)
@@ -421,18 +420,12 @@ let get_fn_implicits (Typ_aux (t, _)) : bool list =
   in
   match t with Typ_fn (args, cod) -> List.map arg_implicit args | _ -> []
 
-let rec is_bitvector_pattern (P_aux (pat,_)) = match pat with
-  | P_vector _ | P_vector_concat _ -> true
-  | P_as (pat,_) -> is_bitvector_pattern pat
-  | _ -> false
+let rec is_bitvector_pattern (P_aux (pat, _)) =
+  match pat with P_vector _ | P_vector_concat _ -> true | P_as (pat, _) -> is_bitvector_pattern pat | _ -> false
 
-let match_or_match_bv brs = 
-  if List.exists (function 
-      | Pat_aux (Pat_exp (pat,_),_) -> is_bitvector_pattern pat 
-      | _ -> false) brs then 
-    "match_bv " 
-  else 
-    "match "
+let match_or_match_bv brs =
+  if List.exists (function Pat_aux (Pat_exp (pat, _), _) -> is_bitvector_pattern pat | _ -> false) brs then "match_bv "
+  else "match "
 
 let rec doc_match_clause (as_monadic : bool) ctx (Pat_aux (cl, l)) =
   match cl with
@@ -521,7 +514,9 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
         (braces (space ^^ doc_exp false ctx exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space))
   | E_match (discr, brs) ->
       let cases = separate_map hardline (doc_match_clause as_monadic ctx) brs in
-      string (match_or_match_bv brs) ^^ doc_exp (effectful (effect_of discr)) ctx discr ^^ string " with" ^^ hardline ^^ cases
+      string (match_or_match_bv brs)
+      ^^ doc_exp (effectful (effect_of discr)) ctx discr
+      ^^ string " with" ^^ hardline ^^ cases
   | E_assign ((LE_aux (le_act, tannot) as le), e) -> (
       match le_act with
       | LE_id id | LE_typ (_, id) -> string "writeReg " ^^ doc_id_ctor id ^^ space ^^ doc_exp false ctx e