Some housekeeping

Update ocamlformat to 0.26.0

Some lem backend warnings were not actually fixed because `dune build
--release` seems to just suppress them - need `dune build` for accurate
warnings, so re-enable 27 for now

Fix some other warnings

.github/workflows/formatting.yml

@@ -34,7 +34,7 @@ jobs:
       run: |
         opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
         eval $(opam env)
-        opam install "ocamlformat=0.25.1" --yes
+        opam install "ocamlformat=0.26.0" --yes
 
     - name: Save cached opam
       if: steps.cache-opam-restore.outputs.cache-hit != 'true'

.ocamlformat

@@ -1,5 +1,5 @@
 profile = default
-version = 0.25.1
+version = 0.26.0
 margin = 120
 exp-grouping = preserve
 parens-ite = true

sailcov/.ocamlformat

@@ -1,5 +1,5 @@
 profile = default
-version = 0.25.1
+version = 0.26.0
 margin = 120
 exp-grouping = preserve
 parens-ite = true

src/lem_interp/pretty_interp.ml

@@ -426,7 +426,7 @@ let doc_exp, doc_let =
         ( l,
           ( Id_aux
               (Id ("*" | "/" | "div" | "quot" | "rem" | "mod" | "quot_s" | "mod_s" | "*_s" | "*_si" | "*_u" | "*_ui"), _)
-          as op
+            as op
           ),
           r
         ) ->

src/lib/ast_util.ml

@@ -145,9 +145,6 @@ let rec is_gen_loc = function
   | Parse_ast.Hint (_, l1, l2) -> is_gen_loc l1 || is_gen_loc l2
   | Parse_ast.Range (p1, p2) -> false
 
-let inc_ord = Ord_aux (Ord_inc, Parse_ast.Unknown)
-let dec_ord = Ord_aux (Ord_dec, Parse_ast.Unknown)
-
 let mk_id str = Id_aux (Id str, Parse_ast.Unknown)
 
 let mk_nc nc_aux = NC_aux (nc_aux, Parse_ast.Unknown)
@@ -469,8 +466,6 @@ let mk_kopt ?loc:(l = Parse_ast.Unknown) kind_aux v =
   let l = match l with Parse_ast.Unknown -> kid_loc v | l -> l in
   KOpt_aux (KOpt_kind (K_aux (kind_aux, l), v), l)
 
-let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown)
-
 let unknown_typ = mk_typ Typ_internal_unknown
 let int_typ = mk_id_typ (mk_id "int")
 let nat_typ = mk_id_typ (mk_id "nat")
@@ -580,7 +575,6 @@ let is_quant_kopt = function QI_aux (QI_id _, _) -> true | _ -> false
 let is_quant_constraint = function QI_aux (QI_constraint _, _) -> true | _ -> false
 
 let unaux_nexp (Nexp_aux (nexp, _)) = nexp
-let unaux_order (Ord_aux (ord, _)) = ord
 let unaux_typ (Typ_aux (typ, _)) = typ
 let unaux_kind (K_aux (k, _)) = k
 let unaux_constraint (NC_aux (nc, _)) = nc
@@ -1682,8 +1676,6 @@ let locate_kinded_id f (KOpt_aux (KOpt_kind (k, kid), l)) = KOpt_aux (KOpt_kind
 
 let locate_lit f (L_aux (lit, l)) = L_aux (lit, f l)
 
-let locate_order f (Ord_aux (ord_aux, l)) = Ord_aux (ord_aux, f l)
-
 let rec locate_nexp f (Nexp_aux (nexp_aux, l)) =
   let nexp_aux =
     match nexp_aux with

src/lib/chunk_ast.ml

@@ -69,7 +69,7 @@ open Parse_ast
 
 let string_of_id_aux = function Id v -> v | Operator v -> v
 
-let string_of_id (Id_aux (id, l)) = string_of_id_aux id
+let string_of_id (Id_aux (id, _)) = string_of_id_aux id
 
 let id_loc (Id_aux (_, l)) = l
 
@@ -80,11 +80,6 @@ let starting_column_num l =
 
 let ending_line_num l = match Reporting.simp_loc l with Some (_, e) -> Some e.pos_lnum | None -> None
 
-let merge_loc l1 l2 =
-  match (Reporting.simp_loc l1, Reporting.simp_loc l2) with
-  | Some (s, _), Some (_, e) -> Parse_ast.Range (s, e)
-  | _, _ -> Parse_ast.Unknown
-
 type binder = Var_binder | Let_binder | Internal_plet_binder
 
 type if_format = { then_brace : bool; else_brace : bool }
@@ -374,7 +369,7 @@ let rec prerr_chunk indent = function
       Queue.iter (prerr_chunk (indent ^ "    ")) exp;
       Printf.eprintf "%s  with:" indent;
       List.iter (fun exp -> Queue.iter (prerr_chunk (indent ^ "    ")) exp) exps
-  | Vector_updates (exp, updates) -> Printf.eprintf "%sVector_updates:\n" indent
+  | Vector_updates (_exp, _updates) -> Printf.eprintf "%sVector_updates:\n" indent
   | Index (exp, ix) ->
       Printf.eprintf "%sIndex:\n" indent;
       List.iter
@@ -492,7 +487,7 @@ let have_linebreak line_num1 line_num2 = match (line_num1, line_num2) with Some
 let have_blank_linebreak line_num1 line_num2 =
   match (line_num1, line_num2) with Some p1, Some p2 -> p1 + 1 < p2 | _, _ -> false
 
-let chunk_delimit ?delim ~get_loc ~chunk comments chunks xs =
+let chunk_delimit ?delim ~get_loc ~chunk comments xs =
   map_peek
     (fun next x ->
       let l = get_loc x in
@@ -577,19 +572,13 @@ let rec chunk_atyp comments chunks (ATyp_aux (aux, l)) =
       let rhs_chunks = rec_chunk_atyp rhs in
       Queue.add (Binary (lhs_chunks, op, rhs_chunks)) chunks
   | ATyp_app (id, ([_] as args)) when string_of_id id = "atom" ->
-      let args =
-        chunk_delimit ~delim:"," ~get_loc:(fun (ATyp_aux (_, l)) -> l) ~chunk:chunk_atyp comments chunks args
-      in
+      let args = chunk_delimit ~delim:"," ~get_loc:(fun (ATyp_aux (_, l)) -> l) ~chunk:chunk_atyp comments args in
       Queue.add (App (Id_aux (Id "int", id_loc id), args)) chunks
   | ATyp_app (id, args) ->
-      let args =
-        chunk_delimit ~delim:"," ~get_loc:(fun (ATyp_aux (_, l)) -> l) ~chunk:chunk_atyp comments chunks args
-      in
+      let args = chunk_delimit ~delim:"," ~get_loc:(fun (ATyp_aux (_, l)) -> l) ~chunk:chunk_atyp comments args in
       Queue.add (App (id, args)) chunks
   | ATyp_tuple args ->
-      let args =
-        chunk_delimit ~delim:"," ~get_loc:(fun (ATyp_aux (_, l)) -> l) ~chunk:chunk_atyp comments chunks args
-      in
+      let args = chunk_delimit ~delim:"," ~get_loc:(fun (ATyp_aux (_, l)) -> l) ~chunk:chunk_atyp comments args in
       Queue.add (Tuple ("(", ")", 0, args)) chunks
   | ATyp_wild -> Queue.add (Atom "_") chunks
   | ATyp_exist (vars, constr, typ) ->
@@ -613,22 +602,22 @@ let rec chunk_pat comments chunks (P_aux (aux, l)) =
   | P_lit lit -> Queue.add (chunk_of_lit lit) chunks
   | P_app (id, [P_aux (P_lit (L_aux (L_unit, _)), _)]) -> Queue.add (App (id, [])) chunks
   | P_app (id, pats) ->
-      let pats = chunk_delimit ~delim:"," ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments chunks pats in
+      let pats = chunk_delimit ~delim:"," ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments pats in
       Queue.add (App (id, pats)) chunks
   | P_tuple pats ->
-      let pats = chunk_delimit ~delim:"," ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments chunks pats in
+      let pats = chunk_delimit ~delim:"," ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments pats in
       Queue.add (Tuple ("(", ")", 0, pats)) chunks
   | P_vector pats ->
-      let pats = chunk_delimit ~delim:"," ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments chunks pats in
+      let pats = chunk_delimit ~delim:"," ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments pats in
       Queue.add (Tuple ("[", "]", 0, pats)) chunks
   | P_list pats ->
-      let pats = chunk_delimit ~delim:"," ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments chunks pats in
+      let pats = chunk_delimit ~delim:"," ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments pats in
       Queue.add (Tuple ("[|", "|]", 0, pats)) chunks
   | P_string_append pats ->
-      let pats = chunk_delimit ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments chunks pats in
+      let pats = chunk_delimit ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments pats in
       Queue.add (Intersperse ("^", pats)) chunks
   | P_vector_concat pats ->
-      let pats = chunk_delimit ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments chunks pats in
+      let pats = chunk_delimit ~get_loc:(fun (P_aux (_, l)) -> l) ~chunk:chunk_pat comments pats in
       Queue.add (Intersperse ("@", pats)) chunks
   | P_vector_subrange (id, n, m) ->
       let id_chunks = Queue.create () in
@@ -671,9 +660,7 @@ let rec chunk_pat comments chunks (P_aux (aux, l)) =
             Queue.add (Binary (field_chunks, "=", pat_chunks)) chunks
         | FP_wild -> Queue.add (Atom "_") chunks
       in
-      let fpats =
-        chunk_delimit ~delim:"," ~get_loc:(fun (FP_aux (_, l)) -> l) ~chunk:chunk_fpat comments chunks fpats
-      in
+      let fpats = chunk_delimit ~delim:"," ~get_loc:(fun (FP_aux (_, l)) -> l) ~chunk:chunk_fpat comments fpats in
       Queue.add (Tuple ("struct {", "}", 1, fpats)) chunks
   | P_attribute (attr, arg, pat) ->
       Queue.add (Atom (Printf.sprintf "$[%s %s]" attr arg)) chunks;
@@ -747,7 +734,7 @@ let rec chunk_exp comments chunks (E_aux (aux, l)) =
       chunk_exp comments chunks exp
   | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> Queue.add (App (id, [])) chunks
   | E_app (id, args) ->
-      let args = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments chunks args in
+      let args = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments args in
       Queue.add (App (id, args)) chunks
   | (E_sizeof atyp | E_constraint atyp) as typ_app ->
       let name =
@@ -788,22 +775,22 @@ let rec chunk_exp comments chunks (E_aux (aux, l)) =
       chunk_atyp comments typ_chunks typ;
       Queue.add (Binary (exp_chunks, ":", typ_chunks)) chunks
   | E_tuple exps ->
-      let exps = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments chunks exps in
+      let exps = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments exps in
       Queue.add (Tuple ("(", ")", 0, exps)) chunks
   | E_vector [] -> Queue.add (Atom "[]") chunks
   | E_vector exps ->
-      let exps = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments chunks exps in
+      let exps = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments exps in
       Queue.add (Tuple ("[", "]", 0, exps)) chunks
   | E_list [] -> Queue.add (Atom "[||]") chunks
   | E_list exps ->
-      let exps = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments chunks exps in
+      let exps = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments exps in
       Queue.add (Tuple ("[|", "|]", 0, exps)) chunks
   | E_struct fexps ->
-      let fexps = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments chunks fexps in
+      let fexps = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments fexps in
       Queue.add (Tuple ("struct {", "}", 1, fexps)) chunks
   | E_struct_update (exp, fexps) ->
       let exp = rec_chunk_exp exp in
-      let fexps = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments chunks fexps in
+      let fexps = chunk_delimit ~delim:"," ~get_loc:(fun (E_aux (_, l)) -> l) ~chunk:chunk_exp comments fexps in
       Queue.add (Struct_update (exp, fexps)) chunks
   | E_block exps ->
       let block_exps = flatten_block exps in
@@ -1190,18 +1177,16 @@ let chunk_type_def comments chunks (TD_aux (aux, l)) =
   match aux with
   | TD_enum (id, [], members, _) ->
       let members =
-        chunk_delimit ~delim:"," ~get_loc:(fun x -> id_loc (fst x)) ~chunk:chunk_enum_member comments chunks members
+        chunk_delimit ~delim:"," ~get_loc:(fun x -> id_loc (fst x)) ~chunk:chunk_enum_member comments members
       in
       Queue.add (Enum { id; enum_functions = None; members }) chunks;
       Queue.add (Spacer (true, 1)) chunks
   | TD_enum (id, enum_functions, members, _) ->
       let enum_functions =
-        chunk_delimit ~delim:","
-          ~get_loc:(fun x -> id_loc (fst x))
-          ~chunk:chunk_enum_function comments chunks enum_functions
+        chunk_delimit ~delim:"," ~get_loc:(fun x -> id_loc (fst x)) ~chunk:chunk_enum_function comments enum_functions
       in
       let members =
-        chunk_delimit ~delim:"," ~get_loc:(fun x -> id_loc (fst x)) ~chunk:chunk_enum_member comments chunks members
+        chunk_delimit ~delim:"," ~get_loc:(fun x -> id_loc (fst x)) ~chunk:chunk_enum_member comments members
       in
       Queue.add (Enum { id; enum_functions = Some enum_functions; members }) chunks;
       Queue.add (Spacer (true, 1)) chunks

src/lib/monomorphise.ml

@@ -4227,7 +4227,7 @@ module BitvectorSizeCasts = struct
 end
 
 module ToplevelNexpRewrites = struct
-  let replace_nexp_in_typ env typ orig new_nexp =
+  let _replace_nexp_in_typ env typ orig new_nexp =
     let rec aux (Typ_aux (t, l) as typ) =
       match t with
       | Typ_id _ | Typ_var _ -> (false, typ)

src/lib/sail_lib.ml

@@ -1115,7 +1115,7 @@ let is_hex_char ch =
   || (Char.code 'a' <= c && c <= Char.code 'f')
   || (Char.code 'A' <= c && c <= Char.code 'F')
 
-let valid_hex_bits (n, s) =
+let valid_hex_bits (_, s) =
   let len = String.length s in
   (* We must have at least the 0x prefix, then one character *)
   if len < 3 || String.sub s 0 2 <> "0x" then false

src/lib/type_check.ml

@@ -543,7 +543,6 @@ module Env : sig
   val add_enum_clause : id -> id -> t -> t
   val get_enum : id -> t -> id list
   val get_enums : t -> IdSet.t Bindings.t
-  val is_enum : id -> t -> bool
   val allow_polymorphic_undefineds : t -> t
   val polymorphic_undefineds : t -> bool
   val lookup_id : id -> t -> typ lvar
@@ -1394,8 +1393,6 @@ end = struct
 
   let get_enums env = Bindings.map snd env.enums
 
-  let is_enum id env = Bindings.mem id env.enums
-
   let is_record id env = Bindings.mem id env.records
 
   let get_record id env = Bindings.find id env.records
@@ -1619,11 +1616,6 @@ let wf_binding l env (typq, typ) =
 
 let wf_typschm env (TypSchm_aux (TypSchm_ts (typq, typ), l)) = wf_binding l env (typq, typ)
 
-(* Create vectors with the default order from the environment *)
-
-let default_order_error_string =
-  "No default Order (if you have set a default Order, move it earlier in the specification)"
-
 let dvector_typ env n typ = vector_typ n typ
 let bits_typ env n = bitvector_typ n
 
@@ -5644,7 +5636,7 @@ and check_scattered : Env.t -> def_annot -> uannot scattered_def -> tannot def l
       ( [DEF_aux (DEF_scattered (SD_aux (SD_variant (id, typq), (l, empty_tannot))), def_annot)],
         Env.add_scattered_variant id typq env
       )
-  | SD_unioncl (id, tu) -> (
+  | SD_unioncl (id, tu) ->
       ( [DEF_aux (DEF_scattered (SD_aux (SD_unioncl (id, tu), (l, empty_tannot))), def_annot)],
         let env = Env.add_variant_clause id tu env in
         let typq, _ = Env.get_variant id env in
@@ -5657,7 +5649,6 @@ and check_scattered : Env.t -> def_annot -> uannot scattered_def -> tannot def l
           in
           raise (Type_error (env, l', err_because (err, id_loc id, Err_other msg)))
       )
-    )
   | SD_funcl (FCL_aux (FCL_funcl (id, _), (fcl_def_annot, _)) as funcl) ->
       let typq, typ = Env.get_val_spec id env in
       let funcl_env = Env.add_typquant fcl_def_annot.loc typq env in

src/sail_c_backend/c_backend.ml

@@ -851,7 +851,7 @@ let rec sgen_ctyp = function
   | CT_rounding_mode -> "uint_fast8_t"
   | CT_poly _ -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *)
 
-let rec sgen_const_ctyp = function CT_string -> "const_sail_string" | ty -> sgen_ctyp ty
+let sgen_const_ctyp = function CT_string -> "const_sail_string" | ty -> sgen_ctyp ty
 
 let rec sgen_ctyp_name = function
   | CT_unit -> "unit"

src/sail_coq_backend/pretty_print_coq.ml

@@ -3269,13 +3269,12 @@ let doc_val avoid_target_names pat exp =
         let typ = expand_range_type (Env.expand_synonyms env typ) in
         match destruct_exist_plain typ with
         | None -> (typpp, exp)
-        | Some _ -> (
+        | Some _ ->
             ( empty,
               match exp with
               | E_aux (E_typ (typ', _), _) when alpha_equivalent env typ typ' -> exp
               | _ -> E_aux (E_typ (typ, exp), (Parse_ast.Unknown, mk_tannot env typ))
             )
-          )
       )
   in
   let idpp = doc_id bare_ctxt id in

src/sail_doc_backend/docinfo.ml

@@ -600,9 +600,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct
          specified via -doc_file, we push true to skip it. If no
          -doc_file flags are passed, include everything. *)
       | DEF_pragma (("file_start" | "include_start"), path, _) -> (docinfo, skip_file path :: skips)
-      | DEF_pragma (("file_end" | "include_end"), _, _) -> (
-          (docinfo, match skips with _ :: skips -> skips | [] -> [])
-        )
+      | DEF_pragma (("file_end" | "include_end"), _, _) -> (docinfo, match skips with _ :: skips -> skips | [] -> [])
       (* Function definiton may be scattered, so we can't skip it *)
       | DEF_fundef fdef ->
           let id = id_of_fundef fdef in

src/sail_lem_backend/dune

@@ -1,3 +1,11 @@
+(env
+ (dev
+  (flags
+   (:standard -w -27)))
+ (release
+  (flags
+   (:standard -w -27))))
+
 (executable
  (name sail_plugin_lem)
  (modes