Merge remote-tracking branch 'origin/main' into son/update-lean

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-aeeae1d46704810bf498db552a75dff15aa3abcc
+e0bf68d674edbb154fe2343b2315ccac325a0c7a

compiler/.ocamlformat

@@ -1 +1,5 @@
-doc-comments=before
+break-cases = fit-or-vertical
+doc-comments = before
+exp-grouping = preserve
+parens-tuple = always
+parens-tuple-patterns = multi-line-only

compiler/AssociatedTypes.ml

@@ -94,9 +94,14 @@ let ctx_add_norm_trait_types_from_preds (span : Meta.span) (ctx : eval_ctx)
 let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool =
   match id with
   | Self | Clause _ -> true
-  | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ | FnPointer _
-  | Closure _ | Unsolved _ | Dyn _ ->
-      false
+  | TraitImpl _
+  | BuiltinOrAuto _
+  | TraitRef _
+  | UnknownTrait _
+  | FnPointer _
+  | Closure _
+  | Unsolved _
+  | Dyn _ -> false
   | ParentClause (id, _, _) | ItemClause (id, _, _, _) ->
       trait_instance_id_is_local_clause id
 
@@ -293,7 +298,9 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
       in
       let tr : trait_type_ref = { trait_ref; type_name } in
       (* Lookup the representative, if there is *)
-      match norm_ctx_get_ty_repr ctx tr with None -> ty | Some ty -> ty)
+      match norm_ctx_get_ty_repr ctx tr with
+      | None -> ty
+      | Some ty -> ty)
   | TDynTrait _ ->
       craise_opt_span __FILE__ __LINE__ ctx.span
         "Dynamic trait types are not supported yet"

compiler/Assumed.ml

@@ -139,7 +139,10 @@ module Sig = struct
       ]
     in
     let inputs =
-      List.append inputs (match index_ty with None -> [] | Some ty -> [ ty ])
+      List.append inputs
+        (match index_ty with
+        | None -> []
+        | Some ty -> [ ty ])
     in
     let output =
       mk_ref_ty rvar_0

compiler/Config.ml

@@ -41,7 +41,9 @@ let borrow_check = ref false
 let backend () : backend = Option.get !opt_backend
 
 let if_backend (f : unit -> 'a) (default : 'a) : 'a =
-  match !opt_backend with None -> default | Some _ -> f ()
+  match !opt_backend with
+  | None -> default
+  | Some _ -> f ()
 
 (** {1 Interpreter} *)
 
@@ -374,7 +376,9 @@ let variant_concatenate_type_name = ref true
 let use_tuple_structs = ref true
 
 let backend_has_tuple_projectors backend =
-  match backend with Lean -> true | Coq | FStar | HOL4 -> false
+  match backend with
+  | Lean -> true
+  | Coq | FStar | HOL4 -> false
 
 (** Toggle the use of tuple projectors *)
 let use_tuple_projectors = ref false

compiler/Contexts.ml

@@ -570,7 +570,9 @@ let ctx_set_abs_can_end (span : Meta.span) (ctx : eval_ctx)
 
 let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
   let decl_group = TypeDeclId.Map.find id ctx.type_ctx.type_decls_groups in
-  match decl_group with RecGroup _ -> true | NonRecGroup _ -> false
+  match decl_group with
+  | RecGroup _ -> true
+  | NonRecGroup _ -> false
 
 (** Visitor to iterate over the values in the *current* frame *)
 class ['self] iter_frame =
@@ -626,17 +628,23 @@ class ['self] map_eval_ctx =
 let env_iter_abs (f : abs -> unit) (env : env) : unit =
   List.iter
     (fun (ee : env_elem) ->
-      match ee with EBinding _ | EFrame -> () | EAbs abs -> f abs)
+      match ee with
+      | EBinding _ | EFrame -> ()
+      | EAbs abs -> f abs)
     env
 
 let env_map_abs (f : abs -> abs) (env : env) : env =
   List.map
     (fun (ee : env_elem) ->
-      match ee with EBinding _ | EFrame -> ee | EAbs abs -> EAbs (f abs))
+      match ee with
+      | EBinding _ | EFrame -> ee
+      | EAbs abs -> EAbs (f abs))
     env
 
 let env_filter_abs (f : abs -> bool) (env : env) : env =
   List.filter
     (fun (ee : env_elem) ->
-      match ee with EBinding _ | EFrame -> true | EAbs abs -> f abs)
+      match ee with
+      | EBinding _ | EFrame -> true
+      | EAbs abs -> f abs)
     env

compiler/Cps.ml

@@ -92,10 +92,14 @@ let map_apply_continuation (f : 'a -> 'c -> 'b * 'c * ('e -> 'e))
   eval_list inputs ctx
 
 let cc_singleton file line span cf el =
-  match el with [ e ] -> cf e | _ -> internal_error file line span
+  match el with
+  | [ e ] -> cf e
+  | _ -> internal_error file line span
 
 let cf_singleton file line span el =
-  match el with [ e ] -> e | _ -> internal_error file line span
+  match el with
+  | [ e ] -> e
+  | _ -> internal_error file line span
 
 (** It happens that we need to concatenate lists of results, for
     instance when evaluating the branches of a match. When applying

compiler/Errors.ml

@@ -1,7 +1,10 @@
 let log = Logging.errors_log
 
 let raw_span_to_string (raw_span : Meta.raw_span) =
-  let file = match raw_span.file with Virtual s | Local s -> s in
+  let file =
+    match raw_span.file with
+    | Virtual s | Local s -> s
+  in
   let loc_to_string (l : Meta.loc) : string =
     string_of_int l.line ^ ":" ^ string_of_int l.col
   in
@@ -14,7 +17,9 @@ let span_to_string (span : Meta.span) = raw_span_to_string span.span
 
 let format_error_message (span : Meta.span option) (msg : string) =
   let span =
-    match span with None -> "" | Some span -> "\n" ^ span_to_string span
+    match span with
+    | None -> ""
+    | Some span -> "\n" ^ span_to_string span
   in
   msg ^ span
 

compiler/Extract.ml

@@ -586,7 +586,9 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
         | _ -> None
       in
       let has_one_field =
-        match num_fields with Some len -> len = 1 | None -> false
+        match num_fields with
+        | Some len -> len = 1
+        | None -> false
       in
       if is_tuple_struct && has_one_field then
         extract_texpression span ctx fmt inside arg
@@ -924,7 +926,9 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
       extract_texpression span ctx fmt scrut_inside scrut;
       F.pp_print_space fmt ();
       let match_scrut_end =
-        match backend () with FStar | Coq | Lean -> "with" | HOL4 -> "of"
+        match backend () with
+        | FStar | Coq | Lean -> "with"
+        | HOL4 -> "of"
       in
       F.pp_print_string fmt match_scrut_end;
       (* Close the box for the [match ... with] *)
@@ -943,7 +947,9 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         let ctx = extract_typed_pattern span ctx fmt false false br.pat in
         F.pp_print_space fmt ();
         let arrow =
-          match backend () with FStar -> "->" | Coq | Lean | HOL4 -> "=>"
+          match backend () with
+          | FStar -> "->"
+          | Coq | Lean | HOL4 -> "=>"
         in
         F.pp_print_string fmt arrow;
         (* Close the box for the pattern *)
@@ -1049,10 +1055,14 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
         print_bracket true ilb;
         F.pp_open_hvbox fmt 0;
         let delimiter =
-          match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";"
+          match backend () with
+          | Lean -> ","
+          | Coq | FStar | HOL4 -> ";"
         in
         let assign =
-          match backend () with Coq | Lean | HOL4 -> ":=" | FStar -> "="
+          match backend () with
+          | Coq | Lean | HOL4 -> ":="
+          | FStar -> "="
         in
         Collections.List.iter_link
           (fun () ->
@@ -1100,7 +1110,9 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
         F.pp_close_box fmt ();
         (* Print the values *)
         let delimiter =
-          match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";"
+          match backend () with
+          | Lean -> ","
+          | Coq | FStar | HOL4 -> ";"
         in
         F.pp_print_space fmt ();
         F.pp_open_hovbox fmt 0;
@@ -1599,7 +1611,11 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   (* Print the "=" *)
   if not is_opaque then (
     F.pp_print_space fmt ();
-    let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
+    let eq =
+      match backend () with
+      | FStar | HOL4 -> "="
+      | Coq | Lean -> ":="
+    in
     F.pp_print_string fmt eq);
   (* Close the box for "(PARAMS) : EFFECT =" *)
   F.pp_close_box fmt ();
@@ -1833,7 +1849,11 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
   if not is_opaque then (
     (* Print " =" *)
     F.pp_print_space fmt ();
-    let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
+    let eq =
+      match backend () with
+      | FStar | HOL4 -> "="
+      | Coq | Lean -> ":="
+    in
     F.pp_print_string fmt eq);
   (* Close ": TYPE =" box (depth=2) *)
   F.pp_close_box fmt ();
@@ -2310,7 +2330,9 @@ let extract_trait_item (ctx : extraction_ctx) (fmt : F.formatter)
   (* ":" or "=" *)
   F.pp_print_string fmt separator;
   ty ();
-  (match backend () with Lean -> () | _ -> F.pp_print_string fmt ";");
+  (match backend () with
+  | Lean -> ()
+  | _ -> F.pp_print_string fmt ";");
   F.pp_close_box fmt ()
 
 let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter)
@@ -2319,7 +2341,11 @@ let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter)
 
 let extract_trait_impl_item (ctx : extraction_ctx) (fmt : F.formatter)
     (item_name : string) (ty : unit -> unit) : unit =
-  let assign = match backend () with Lean | Coq -> ":=" | _ -> "=" in
+  let assign =
+    match backend () with
+    | Lean | Coq -> ":="
+    | _ -> "="
+  in
   extract_trait_item ctx fmt item_name assign ty
 
 (** Small helper - TODO: move *)
@@ -2366,7 +2392,9 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
         f.signature.llbc_generics generics ctx
     in
     let backend_uses_forall =
-      match backend () with Coq | Lean -> true | FStar | HOL4 -> false
+      match backend () with
+      | Coq | Lean -> true
+      | FStar | HOL4 -> false
     in
     let generics_not_empty = generics <> empty_generic_params in
     let use_forall = generics_not_empty && backend_uses_forall in

compiler/ExtractBase.ml

@@ -389,14 +389,18 @@ type names_maps = {
 (** Return [true] if we are strict on collisions for this id (i.e., we forbid
     collisions even with the ids in the unsafe names map) *)
 let strict_collisions (id : id) : bool =
-  match id with UnknownId | TypeId _ -> true | _ -> false
+  match id with
+  | UnknownId | TypeId _ -> true
+  | _ -> false
 
 (** We might not check for collisions for some specific ids (ex.: field names) *)
 let allow_collisions (id : id) : bool =
   match id with
-  | FieldId _ | TraitItemClauseId _ | TraitParentClauseId _ | TraitItemId _
-  | TraitMethodId _ ->
-      !Config.record_fields_short_names
+  | FieldId _
+  | TraitItemClauseId _
+  | TraitParentClauseId _
+  | TraitItemId _
+  | TraitMethodId _ -> !Config.record_fields_short_names
   | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _)) ->
       (* We map several assumed functions to the same id *)
       true
@@ -534,9 +538,13 @@ let scalar_name (ty : literal_type) : string =
   match ty with
   | TInteger ty -> int_name ty
   | TBool -> (
-      match backend () with FStar | Coq | HOL4 -> "bool" | Lean -> "Bool")
+      match backend () with
+      | FStar | Coq | HOL4 -> "bool"
+      | Lean -> "Bool")
   | TChar -> (
-      match backend () with FStar | Coq | HOL4 -> "char" | Lean -> "Char")
+      match backend () with
+      | FStar | Coq | HOL4 -> "char"
+      | Lean -> "Char")
 
 (** Extraction context.
 
@@ -801,7 +809,9 @@ let unop_name (unop : unop) : string =
       | Coq -> "negb"
       | HOL4 -> "~")
   | Neg (int_ty : integer_type) -> (
-      match backend () with Lean -> "-." | _ -> int_name int_ty ^ "_neg")
+      match backend () with
+      | Lean -> "-."
+      | _ -> int_name int_ty ^ "_neg")
   | Cast _ ->
       (* We never directly use the unop name in this case *)
       raise (Failure "Unsupported")
@@ -1676,7 +1686,9 @@ let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl)
      can't disambiguate fields coming from different ADTs if they have the same
      names), and thus don't need to add a prefix starting with a lowercase.
   *)
-  match backend () with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name
+  match backend () with
+  | FStar -> "t" ^ name
+  | Coq | Lean | HOL4 -> name
 
 let ctx_compute_trait_const_name (ctx : extraction_ctx)
     (trait_decl : trait_decl) (item : string) : string =
@@ -1685,7 +1697,9 @@ let ctx_compute_trait_const_name (ctx : extraction_ctx)
     else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
   in
   (* See [trait_type_name] *)
-  match backend () with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
+  match backend () with
+  | FStar -> "c" ^ name
+  | Coq | Lean | HOL4 -> name
 
 let ctx_compute_trait_method_name (ctx : extraction_ctx)
     (trait_decl : trait_decl) (item : string) : string =
@@ -1826,7 +1840,10 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
           | FStar -> "x" (* lacking inspiration here... *)
           | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
       | TLiteral lty -> (
-          match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
+          match lty with
+          | TBool -> "b"
+          | TChar -> "c"
+          | TInteger _ -> "i")
       | TArrow _ -> "f"
       | TTraitType (_, name) -> name_from_type_ident name
       | Error -> "x")
@@ -2055,7 +2072,9 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
          between the name for the default constant and the name for the field
          in the trait declaration *)
       let suffix =
-        match def.kind with TraitItemProvided _ -> "_default" | _ -> ""
+        match def.kind with
+        | TraitItemProvided _ -> "_default"
+        | _ -> ""
       in
       let ctx = ctx_add def.item_meta.span decl (name ^ suffix) ctx in
       let ctx = ctx_add def.item_meta.span body (name ^ suffix ^ "_body") ctx in