From 5c148ec8bd9fffac7a80fc3d6acb98c1fb5ec3c4 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 12 Nov 2024 10:33:59 +0100 Subject: [PATCH] chore(engine): ocamlformat: update: 0.24.1 -> 0.26.2 This updates ocamlformat to the latest version. Whence the various changes in the files. Fixes #1095 The other tools are not pinned specifically, if we want to update, updating the flake.lock will do the job. --- engine/.ocamlformat | 2 +- engine/backends/coq/coq/coq_backend.ml | 17 +- engine/backends/coq/coq_ast.ml | 16 +- .../backends/coq/ssprove/ssprove_backend.ml | 46 ++-- .../backends/easycrypt/easycrypt_backend.ml | 12 +- engine/backends/fstar/fstar_backend.ml | 11 +- engine/backends/proverif/proverif_backend.ml | 16 +- engine/lib/analyses/mutable_variables.ml | 13 +- .../deprecated_generic_printer_base.ml | 156 +++++++------- engine/lib/feature_gate.ml | 16 +- engine/lib/generic_printer/generic_printer.ml | 23 +- .../generic_printer_template.ml | 3 +- engine/lib/import_thir.ml | 6 +- engine/lib/phase_utils.ml | 15 +- engine/lib/phases/phase_cf_into_monads.ml | 2 +- engine/lib/phases/phase_direct_and_mut.ml | 4 +- engine/lib/phases/phase_drop_blocks.ml | 2 +- engine/lib/phases/phase_drop_match_guards.ml | 3 +- engine/lib/phases/phase_drop_references.ml | 2 +- .../phase_drop_return_break_continue.ml | 2 +- .../lib/phases/phase_functionalize_loops.ml | 2 +- engine/lib/phases/phase_local_mutation.ml | 2 +- .../phase_reconstruct_for_index_loops.ml | 2 +- .../lib/phases/phase_reconstruct_for_loops.ml | 2 +- .../phase_reconstruct_question_marks.ml | 2 +- .../phases/phase_reconstruct_while_loops.ml | 2 +- .../phases/phase_simplify_question_marks.ml | 2 +- .../phases/phase_transform_hax_lib_inline.ml | 10 +- .../lib/phases/phase_trivialize_assign_lhs.ml | 2 +- engine/lib/side_effect_utils.ml | 28 +-- .../generate_from_ast/codegen_ast_builder.ml | 14 +- .../generate_from_ast/codegen_ast_destruct.ml | 2 +- .../generate_from_ast/codegen_printer.ml | 16 +- engine/utils/generate_from_ast/visitors.ml | 4 +- .../ppx_generate_features.ml | 201 +++++++++--------- .../utils/sourcemaps/mappings/instruction.ml | 12 +- flake.nix | 2 +- 37 files changed, 342 insertions(+), 330 deletions(-) diff --git a/engine/.ocamlformat b/engine/.ocamlformat index 9d647c5ac..d2136f096 100644 --- a/engine/.ocamlformat +++ b/engine/.ocamlformat @@ -1,2 +1,2 @@ profile = default -version = 0.24.1 \ No newline at end of file +version = 0.26.2 \ No newline at end of file diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 2db7c6cee..7258e44ea 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -86,10 +86,11 @@ let hardcoded_coq_headers = module BasePrinter = Generic_printer.Make (InputLanguage) -module Make (Default : sig - val default : string -> string -end) -(Attrs : Attrs.WITH_ITEMS) = +module Make + (Default : sig + val default : string -> string + end) + (Attrs : Attrs.WITH_ITEMS) = struct open PPrint @@ -648,10 +649,10 @@ struct method trait_item'_TIDefault ~params ~body ~witness:_ = (if List.is_empty params then empty - else - string "fun" ^^ space - ^^ separate_map space (fun x -> x#p) params - ^^ space ^^ string "=>") + else + string "fun" ^^ space + ^^ separate_map space (fun x -> x#p) params + ^^ space ^^ string "=>") ^^ nest 2 (break 1 ^^ body#p) method trait_item'_TIFn x1 = x1#p diff --git a/engine/backends/coq/coq_ast.ml b/engine/backends/coq/coq_ast.ml index 1fd848982..2ce4b5b83 100644 --- a/engine/backends/coq/coq_ast.ml +++ b/engine/backends/coq/coq_ast.ml @@ -578,10 +578,10 @@ functor Some ("let" ^ " " ^ name ^ " " ^ ":=" ^ " " ^ (if List.is_empty arguments then "" - else - "fun" ^ " " - ^ params_to_string_typed arguments - ^ " " ^ "=>" ^ " ") + else + "fun" ^ " " + ^ params_to_string_typed arguments + ^ " " ^ "=>" ^ " ") ^ term_to_string_without_paren term 1 ^ " " ^ ":" ^ " " ^ ty_to_string_without_paren ty @@ -601,10 +601,10 @@ functor | InlineDef (name, arguments, term, ty) -> name ^ " " ^ ":=" ^ " " ^ "(" ^ (if List.is_empty arguments then "" - else - "fun" ^ " " - ^ params_to_string_typed arguments - ^ " " ^ "=>" ^ " ") + else + "fun" ^ " " + ^ params_to_string_typed arguments + ^ " " ^ "=>" ^ " ") ^ term_to_string_without_paren term 1 ^ " " ^ ":" ^ " " ^ ty_to_string_without_paren ty diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml index 54393f0dd..8c1870339 100644 --- a/engine/backends/coq/ssprove/ssprove_backend.ml +++ b/engine/backends/coq/ssprove/ssprove_backend.ml @@ -334,7 +334,7 @@ module SSPExtraDefinitions (* : ANALYSIS *) = struct ~f:(fun x y -> SSP.AST.App (SSP.AST.Var x, [ y ])) ((if Stdlib.(i != 0) then [ "snd" ] - else []) + else []) @ List.init (List.length fields - 1 - i) ~f:(fun _ -> "fst")), @@ -437,9 +437,9 @@ module SSPExtraDefinitions (* : ANALYSIS *) = struct [ SSP.AST.Value ( (if Stdlib.(j == i) then SSP.AST.Var "y" - else - SSP.AST.App - (SSP.AST.Var x, [ SSP.AST.Var "x" ])), + else + SSP.AST.App + (SSP.AST.Var x, [ SSP.AST.Var "x" ])), false, 0 ); ] )) @@ -534,12 +534,12 @@ end module StaticAnalysis (* : ANALYSIS *) = struct module FunctionDependency (* : ANALYSIS *) = - [%functor_application - Analyses.Function_dependency InputLanguage] + [%functor_application + Analyses.Function_dependency InputLanguage] module MutableVariables (* : ANALYSIS *) = - [%functor_application - Analyses.Mutable_variables InputLanguage] + [%functor_application + Analyses.Mutable_variables InputLanguage] type analysis_data = { mut_var : MutableVariables.analysis_data } @@ -1470,16 +1470,16 @@ struct let g = pgeneric span generics in [ (if List.is_empty g then - SSP.AST.Notation - ( "'" ^ pconcrete_ident name ^ "'", - SSP.AST.Type (pty span ty), - None ) - else - SSP.AST.Definition - ( pconcrete_ident name, - g, - SSP.AST.Type (pty span ty), - SSP.AST.TypeTy )); + SSP.AST.Notation + ( "'" ^ pconcrete_ident name ^ "'", + SSP.AST.Type (pty span ty), + None ) + else + SSP.AST.Definition + ( pconcrete_ident name, + g, + SSP.AST.Type (pty span ty), + SSP.AST.TypeTy )); ] (* record *) | Type @@ -1741,11 +1741,11 @@ struct (if include_extra_loc then [ loc_name ] else []) in (if include_extra_loc then - [ - SSP.AST.Named - (loc_name, SSP.AST.NameTy "{fset Location}"); - ] - else []) + [ + SSP.AST.Named + (loc_name, SSP.AST.NameTy "{fset Location}"); + ] + else []) @ [ SSP.AST.Named ( pconcrete_ident x.ti_ident, diff --git a/engine/backends/easycrypt/easycrypt_backend.ml b/engine/backends/easycrypt/easycrypt_backend.ml index c0739d2b7..bf2ed8e6b 100644 --- a/engine/backends/easycrypt/easycrypt_backend.ml +++ b/engine/backends/easycrypt/easycrypt_backend.ml @@ -348,12 +348,12 @@ let translate _ (bo : BackendOptions.t) ~(bundles : AST.item list list) open Phase_utils module TransformToInputLanguage = -[%functor_application -Phases.Reject.RawOrMutPointer Features.Rust |> Phases.Reject.Unsafe -|> Phases.And_mut_defsite |> Phases.Reconstruct_asserts -|> Phases.Reconstruct_for_loops |> Phases.Direct_and_mut |> Phases.Drop_blocks -|> Phases.Reject.Continue |> Phases.Drop_references |> Phases.Bundle_cycles -|> RejectNotEC] + [%functor_application + Phases.Reject.RawOrMutPointer Features.Rust |> Phases.Reject.Unsafe + |> Phases.And_mut_defsite |> Phases.Reconstruct_asserts + |> Phases.Reconstruct_for_loops |> Phases.Direct_and_mut |> Phases.Drop_blocks + |> Phases.Reject.Continue |> Phases.Drop_references |> Phases.Bundle_cycles + |> RejectNotEC] let apply_phases (_bo : BackendOptions.t) (items : Ast.Rust.item list) : AST.item list = diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 845a90854..a060ddfd0 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -104,7 +104,8 @@ let module_name (ns : string * string list) : string = (List.map ~f:(map_first_letter String.uppercase) (fst ns :: snd ns)) module Make - (Attrs : Attrs.WITH_ITEMS) (Ctx : sig + (Attrs : Attrs.WITH_ITEMS) + (Ctx : sig val ctx : Context.t end) = struct @@ -1174,11 +1175,9 @@ struct (* in *) (F.id name, None, [], t) :: List.map - ~f: - (fun { - goal = { trait; args }; - name = impl_ident_name; - } -> + ~f:(fun + { goal = { trait; args }; name = impl_ident_name } + -> let base = F.term @@ F.AST.Name (pconcrete_ident trait) in diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 2be7b4348..3b1c6e56b 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -38,14 +38,14 @@ module SubtypeToInputLanguage and type macro = Features.On.macro and type quote = Features.On.quote and type construct_base = Features.On.construct_base - (* and type as_pattern = Features.Off.as_pattern *) - (* and type nontrivial_lhs = Features.Off.nontrivial_lhs *) - (* and type arbitrary_lhs = Features.Off.arbitrary_lhs *) - (* and type lifetime = Features.Off.lifetime *) - (* and type construct_base = Features.Off.construct_base *) - (* and type monadic_action = Features.Off.monadic_action *) - (* and type monadic_binding = Features.Off.monadic_binding *) - (* and type block = Features.Off.block *)) = +(* and type as_pattern = Features.Off.as_pattern *) +(* and type nontrivial_lhs = Features.Off.nontrivial_lhs *) +(* and type arbitrary_lhs = Features.Off.arbitrary_lhs *) +(* and type lifetime = Features.Off.lifetime *) +(* and type construct_base = Features.Off.construct_base *) +(* and type monadic_action = Features.Off.monadic_action *) +(* and type monadic_binding = Features.Off.monadic_binding *) +(* and type block = Features.Off.block *)) = struct module FB = InputLanguage diff --git a/engine/lib/analyses/mutable_variables.ml b/engine/lib/analyses/mutable_variables.ml index eb9e71683..63e8f5f18 100644 --- a/engine/lib/analyses/mutable_variables.ml +++ b/engine/lib/analyses/mutable_variables.ml @@ -39,11 +39,10 @@ module%inlined_contents Make (F : Features.T) = struct include W include Set.M (W) - class type ['s] monoid = - object - method zero : 's - method plus : 's -> 's -> 's - end + class type ['s] monoid = object + method zero : 's + method plus : 's -> 's -> 's + end class ['s, 't] prod_monoid (fst : 's monoid) (snd : 't monoid) (* : ['s * 't] monoid *) = @@ -153,8 +152,8 @@ module%inlined_contents Make (F : Features.T) = struct end let rec analyse (func_dep : pre_data) (items : A.item list) : analysis_data = - let (mut_var_list, _) - : (concrete_ident * (U.TypedLocalIdent.t * id_order) list) list * _ = + let (mut_var_list, _) : + (concrete_ident * (U.TypedLocalIdent.t * id_order) list) list * _ = List.fold_left ~init:([], 0) ~f:(fun (y, count) (name, body) -> let items, count = analyse_function_body body count in diff --git a/engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml b/engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml index c887ecdf1..780ce2bcf 100644 --- a/engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml +++ b/engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml @@ -276,85 +276,83 @@ module Make (F : Features.T) = struct ; items : item list fn > (** In the end, an printer *object* should be of the type {!print_object}. *) - class type print_class = - object - inherit print_base - method printer_name : string - method get_span_data : unit -> Annotation.t list - - method namespace_of_concrete_ident : - concrete_ident -> string * string list - (** The namespace a concrete identifier was defined in. *) - - method par_state : ast_position -> par_state - method concrete_ident' : under_current_ns:bool -> concrete_ident fn - method concrete_ident : concrete_ident fn - method name_of_concrete_ident : concrete_ident fn - method mutability : 'a. 'a mutability fn - method primitive_ident : primitive_ident fn - method local_ident : local_ident fn - method literal : literal_ctx -> literal fn - method generic_value : generic_value fn - method lhs : lhs fn - method ty_bool : document - method ty_char : document - method ty_str : document - method ty_int : int_kind fn - method ty_float : float_kind fn - method generic_values : generic_value list fn - method ty_app : concrete_ident -> generic_value list fn - method ty_tuple : int -> ty list fn - method ty : par_state -> ty fn - method expr' : par_state -> expr' fn - - method expr_monadic_let : - monad:supported_monads * F.monadic_binding -> - lhs:pat -> - rhs:expr -> - expr fn - - method expr_let : lhs:pat -> rhs:expr -> expr fn - method tuple_projection : size:int -> nth:int -> expr fn - method field_projection : concrete_ident -> expr fn - method expr_app : expr -> expr list -> generic_value list fn - method doc_construct_tuple : document list fn - method expr_construct_tuple : expr list fn - method pat_construct_tuple : pat list fn - method global_ident_projector : global_ident fn - - method doc_construct_inductive : - is_record:bool -> - is_struct:bool -> - constructor:concrete_ident -> - base:document option -> - (global_ident * document) list fn - - method expr_construct_inductive : - is_record:bool -> - is_struct:bool -> - constructor:concrete_ident -> - base:(expr * F.construct_base) option -> - (global_ident * expr) list fn - - method attr : attr fn - method attrs : attrs fn - method pat' : par_state -> pat' fn - method pat_ascription : typ:ty -> typ_span:span -> pat fn - method pat : par_state -> pat fn - method expr_unwrapped : par_state -> expr fn - method param : param fn - method item' : item' fn - method item_unwrapped : item fn - method generic_param' : generic_param fn - method generic_param : generic_param fn - method generic_params : generic_param list fn - method arm' : arm' fn - method arm : arm fn - method expr : par_state -> expr fn - method item : item fn - method quote : quote fn - method items : item list fn - end + class type print_class = object + inherit print_base + method printer_name : string + method get_span_data : unit -> Annotation.t list + + method namespace_of_concrete_ident : concrete_ident -> string * string list + (** The namespace a concrete identifier was defined in. *) + + method par_state : ast_position -> par_state + method concrete_ident' : under_current_ns:bool -> concrete_ident fn + method concrete_ident : concrete_ident fn + method name_of_concrete_ident : concrete_ident fn + method mutability : 'a. 'a mutability fn + method primitive_ident : primitive_ident fn + method local_ident : local_ident fn + method literal : literal_ctx -> literal fn + method generic_value : generic_value fn + method lhs : lhs fn + method ty_bool : document + method ty_char : document + method ty_str : document + method ty_int : int_kind fn + method ty_float : float_kind fn + method generic_values : generic_value list fn + method ty_app : concrete_ident -> generic_value list fn + method ty_tuple : int -> ty list fn + method ty : par_state -> ty fn + method expr' : par_state -> expr' fn + + method expr_monadic_let : + monad:supported_monads * F.monadic_binding -> + lhs:pat -> + rhs:expr -> + expr fn + + method expr_let : lhs:pat -> rhs:expr -> expr fn + method tuple_projection : size:int -> nth:int -> expr fn + method field_projection : concrete_ident -> expr fn + method expr_app : expr -> expr list -> generic_value list fn + method doc_construct_tuple : document list fn + method expr_construct_tuple : expr list fn + method pat_construct_tuple : pat list fn + method global_ident_projector : global_ident fn + + method doc_construct_inductive : + is_record:bool -> + is_struct:bool -> + constructor:concrete_ident -> + base:document option -> + (global_ident * document) list fn + + method expr_construct_inductive : + is_record:bool -> + is_struct:bool -> + constructor:concrete_ident -> + base:(expr * F.construct_base) option -> + (global_ident * expr) list fn + + method attr : attr fn + method attrs : attrs fn + method pat' : par_state -> pat' fn + method pat_ascription : typ:ty -> typ_span:span -> pat fn + method pat : par_state -> pat fn + method expr_unwrapped : par_state -> expr fn + method param : param fn + method item' : item' fn + method item_unwrapped : item fn + method generic_param' : generic_param fn + method generic_param : generic_param fn + method generic_params : generic_param list fn + method arm' : arm' fn + method arm : arm fn + method expr : par_state -> expr fn + method item : item fn + method quote : quote fn + method items : item list fn + end module type API = sig type aux_info diff --git a/engine/lib/feature_gate.ml b/engine/lib/feature_gate.ml index fa5625da9..597f9511a 100644 --- a/engine/lib/feature_gate.ml +++ b/engine/lib/feature_gate.ml @@ -20,17 +20,17 @@ module Make (FA : Features.T) (FB : Features.T) (S0 : sig - include Features.SUBTYPE.T + include Features.SUBTYPE.T - type error [@@deriving show, yojson, eq] + type error [@@deriving show, yojson, eq] - exception E of error + exception E of error - val explain : error -> Features.Enumeration.t -> string - val metadata : Phase_utils.Metadata.t - end - with module A = FA - and module B = FB) = + val explain : error -> Features.Enumeration.t -> string + val metadata : Phase_utils.Metadata.t + end + with module A = FA + and module B = FB) = struct let metadata = S0.metadata diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml index 181aef257..c82312e44 100644 --- a/engine/lib/generic_printer/generic_printer.ml +++ b/engine/lib/generic_printer/generic_printer.ml @@ -91,17 +91,16 @@ module AnnotatedString = struct end (** Helper class that brings imperative span *) -class span_helper : - object - method span_data : Annotation.t list - (** Get the span annotation accumulated while printing *) +class span_helper : object + method span_data : Annotation.t list + (** Get the span annotation accumulated while printing *) - method with_span : span:span -> (unit -> document) -> document - (** Runs the printer `f` under a node of span `span` *) + method with_span : span:span -> (unit -> document) -> document + (** Runs the printer `f` under a node of span `span` *) - method current_span : span - (** Get the current span *) - end = + method current_span : span + (** Get the current span *) +end = object (self) val mutable current_span = Span.default val mutable span_data : Annotation.t list = [] @@ -202,9 +201,9 @@ module Make (F : Features.T) = struct method concrete_ident ~local (id : Concrete_ident.view) : document = string (if local then id.definition - else - String.concat ~sep:self#module_path_separator - (id.crate :: (id.path @ [ id.definition ]))) + else + String.concat ~sep:self#module_path_separator + (id.crate :: (id.path @ [ id.definition ]))) (** [concrete_ident ~local id] prints a name without path if [local] is true, otherwise it prints the full path, separated by `module_path_separator`. *) diff --git a/engine/lib/generic_printer/generic_printer_template.ml b/engine/lib/generic_printer/generic_printer_template.ml index 9105966aa..1bcd61085 100644 --- a/engine/lib/generic_printer/generic_printer_template.ml +++ b/engine/lib/generic_printer/generic_printer_template.ml @@ -3,7 +3,8 @@ open! Ast open! PPrint module Make - (F : Features.T) (Default : sig + (F : Features.T) + (Default : sig val default : string -> string end) = struct diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index c9dc1a8a4..e841b3591 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -945,7 +945,7 @@ end) : EXPR = struct e = Literal (Int { kind = { size = S8; signedness = Unsigned }; _ } - as lit); + as lit); _; } -> lit @@ -1526,8 +1526,8 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = in let variants = List.map - ~f: - (fun ({ data; def_id = variant_id; attributes; _ } as original) -> + ~f:(fun + ({ data; def_id = variant_id; attributes; _ } as original) -> let is_record = [%matches? (Struct { fields = _ :: _; _ } : Types.variant_data)] data diff --git a/engine/lib/phase_utils.ml b/engine/lib/phase_utils.ml index 1085c86d4..19298a0a1 100644 --- a/engine/lib/phase_utils.ml +++ b/engine/lib/phase_utils.ml @@ -62,8 +62,9 @@ end (** Make a monomorphic phase: a phase that transform an AST with feature set [F] into an AST with the same feature set [F] *) -module MakeMonomorphicPhase (F : Features.T) (M : MAKE_MONOMORPHIC_PHASE(F).ARG) : - MAKE_MONOMORPHIC_PHASE(F).T = struct +module MakeMonomorphicPhase + (F : Features.T) + (M : MAKE_MONOMORPHIC_PHASE(F).ARG) : MAKE_MONOMORPHIC_PHASE(F).T = struct module FA = F module FB = F module A = Ast.Make (F) @@ -129,7 +130,8 @@ end module MakeBase (FA : Features.T) - (FB : Features.T) (M : sig + (FB : Features.T) + (M : sig val phase_id : Diagnostics.Phase.t end) = struct @@ -290,8 +292,11 @@ struct let ditems (items : A.item list) : B.item list = let nth = List.length @@ Metadata.previous_phases D1'.metadata in (if Int.equal nth 0 then - let coerce_to_full_ast : D1'.A.item -> Ast.Full.item = Stdlib.Obj.magic in - DebugBindPhase.add Before 0 (fun _ -> List.map ~f:coerce_to_full_ast items)); + let coerce_to_full_ast : D1'.A.item -> Ast.Full.item = + Stdlib.Obj.magic + in + DebugBindPhase.add Before 0 (fun _ -> + List.map ~f:coerce_to_full_ast items)); let items' = D1'.ditems items in let coerce_to_full_ast : D2'.A.item list -> Ast.Full.item list = Stdlib.Obj.magic diff --git a/engine/lib/phases/phase_cf_into_monads.ml b/engine/lib/phases/phase_cf_into_monads.ml index 54f8d035e..373bc06ef 100644 --- a/engine/lib/phases/phase_cf_into_monads.ml +++ b/engine/lib/phases/phase_cf_into_monads.ml @@ -231,7 +231,7 @@ struct else UB.call Rust_primitives__hax__control_flow_monad__ControlFlowMonad__lift [ e ] e.span target_type - [@@inline_ands bindings_of dexpr - dexpr'] + [@@inline_ands bindings_of dexpr - dexpr'] module Item = struct module OverrideDExpr = struct diff --git a/engine/lib/phases/phase_direct_and_mut.ml b/engine/lib/phases/phase_direct_and_mut.ml index c33d18096..c0b557834 100644 --- a/engine/lib/phases/phase_direct_and_mut.ml +++ b/engine/lib/phases/phase_direct_and_mut.ml @@ -280,7 +280,7 @@ struct | _ -> let e = dexpr' span expr.e in B.{ e; typ = dty expr.span expr.typ; span = expr.span } - [@@inline_ands bindings_of dexpr] + [@@inline_ands bindings_of dexpr] [%%inline_defs dgeneric_param + dgeneric_constraint + dgenerics + dparam + dvariant @@ -290,7 +290,7 @@ struct let vars = UA.Reducers.collect_local_idents#visit_item' () item in out_var := UA.fresh_local_ident_in (Set.to_list vars) "out"; [%inline_body ditem'] span item - [@@inline_ands "Item.*"] + [@@inline_ands "Item.*"] end include Implem diff --git a/engine/lib/phases/phase_drop_blocks.ml b/engine/lib/phases/phase_drop_blocks.ml index 45844e7eb..088156347 100644 --- a/engine/lib/phases/phase_drop_blocks.ml +++ b/engine/lib/phases/phase_drop_blocks.ml @@ -30,7 +30,7 @@ module%inlined_contents Make (F : Features.T) = struct match (UA.unbox_underef_expr { e; span; typ = UA.never_typ }).e with | [%inline_arms "dexpr'.*" - Block] -> auto | Block { e; _ } -> (dexpr e).e - [@@inline_ands bindings_of dexpr - dexpr'] + [@@inline_ands bindings_of dexpr - dexpr'] [%%inline_defs "Item.*"] end diff --git a/engine/lib/phases/phase_drop_match_guards.ml b/engine/lib/phases/phase_drop_match_guards.ml index b4cf7524d..f54e61a53 100644 --- a/engine/lib/phases/phase_drop_match_guards.ml +++ b/engine/lib/phases/phase_drop_match_guards.ml @@ -188,8 +188,7 @@ module%inlined_contents Make (F : Features.T) = struct new_body ~span in transform_arms scrutinee remaining [ new_arm ] - [@@inline_ands - bindings_of dexpr - dexpr' - darm - darm' - dguard - dguard'] + [@@inline_ands bindings_of dexpr - dexpr' - darm - darm' - dguard - dguard'] [%%inline_defs "Item.*"] end diff --git a/engine/lib/phases/phase_drop_references.ml b/engine/lib/phases/phase_drop_references.ml index dcd7f36ad..4eda38665 100644 --- a/engine/lib/phases/phase_drop_references.ml +++ b/engine/lib/phases/phase_drop_references.ml @@ -129,7 +129,7 @@ struct let bounds_impls = List.map ~f:(dimpl_expr span) bounds_impls in App { f; args; generic_args; trait; bounds_impls } | _ -> . - [@@inline_ands bindings_of dexpr - dbinding_mode] + [@@inline_ands bindings_of dexpr - dbinding_mode] let dgeneric_param (_span : span) ({ ident; kind; attrs; span } : A.generic_param) : diff --git a/engine/lib/phases/phase_drop_return_break_continue.ml b/engine/lib/phases/phase_drop_return_break_continue.ml index 937bfeb69..ad0e6d201 100644 --- a/engine/lib/phases/phase_drop_return_break_continue.ml +++ b/engine/lib/phases/phase_drop_return_break_continue.ml @@ -164,7 +164,7 @@ module%inlined_contents Make (F : Features.T) = struct let kind = dloop_kind span kind in let state = Option.map ~f:(dloop_state span) state in Loop { body; control_flow; kind; state; label; witness } - [@@inline_ands bindings_of dexpr - dexpr'] + [@@inline_ands bindings_of dexpr - dexpr'] [%%inline_defs "Item.*" - ditems] diff --git a/engine/lib/phases/phase_functionalize_loops.ml b/engine/lib/phases/phase_functionalize_loops.ml index 956952368..3855c1e12 100644 --- a/engine/lib/phases/phase_functionalize_loops.ml +++ b/engine/lib/phases/phase_functionalize_loops.ml @@ -286,7 +286,7 @@ struct | [%inline_arms "dexpr'.*" - Loop - Break - Continue - Return] -> map (fun e -> B.{ e; typ = dty expr.span expr.typ; span = expr.span }) | _ -> . - [@@inline_ands bindings_of dexpr - dexpr' - dloop_kind - dloop_state] + [@@inline_ands bindings_of dexpr - dexpr' - dloop_kind - dloop_state] [%%inline_defs "Item.*"] end diff --git a/engine/lib/phases/phase_local_mutation.ml b/engine/lib/phases/phase_local_mutation.ml index 705c6624a..53b83fd71 100644 --- a/engine/lib/phases/phase_local_mutation.ml +++ b/engine/lib/phases/phase_local_mutation.ml @@ -397,7 +397,7 @@ struct else UB.make_tuple_expr ~span [ vars; e' ]) and dexpr_unwrapped e = dexpr_s Instructions.zero e - [@@inline_ands bindings_of dexpr - dexpr'] + [@@inline_ands bindings_of dexpr - dexpr'] [%%inline_defs "Item.*"] end diff --git a/engine/lib/phases/phase_reconstruct_for_index_loops.ml b/engine/lib/phases/phase_reconstruct_for_index_loops.ml index 15333d8aa..dac997226 100644 --- a/engine/lib/phases/phase_reconstruct_for_index_loops.ml +++ b/engine/lib/phases/phase_reconstruct_for_index_loops.ml @@ -87,7 +87,7 @@ module%inlined_contents Make (FA : Features.T) = struct witness = Features.On.for_index_loop; } | [%inline_arms "dloop_kind.*"] -> auto - [@@inline_ands bindings_of dexpr] + [@@inline_ands bindings_of dexpr] [%%inline_defs "Item.*"] end diff --git a/engine/lib/phases/phase_reconstruct_for_loops.ml b/engine/lib/phases/phase_reconstruct_for_loops.ml index 2c7df3b8f..809c1a96d 100644 --- a/engine/lib/phases/phase_reconstruct_for_loops.ml +++ b/engine/lib/phases/phase_reconstruct_for_loops.ml @@ -261,7 +261,7 @@ struct typ = UB.unit_typ; } | None -> h expr - [@@inline_ands bindings_of dexpr] + [@@inline_ands bindings_of dexpr] [%%inline_defs "Item.*"] end diff --git a/engine/lib/phases/phase_reconstruct_question_marks.ml b/engine/lib/phases/phase_reconstruct_question_marks.ml index c1faf65c8..d25841b05 100644 --- a/engine/lib/phases/phase_reconstruct_question_marks.ml +++ b/engine/lib/phases/phase_reconstruct_question_marks.ml @@ -222,7 +222,7 @@ module%inlined_contents Make (FA : Features.T) = struct typ = dty expr.span expr.typ; } | None -> h expr - [@@inline_ands bindings_of dexpr] + [@@inline_ands bindings_of dexpr] [%%inline_defs "Item.*"] end diff --git a/engine/lib/phases/phase_reconstruct_while_loops.ml b/engine/lib/phases/phase_reconstruct_while_loops.ml index 53062c7ec..3f4a79689 100644 --- a/engine/lib/phases/phase_reconstruct_while_loops.ml +++ b/engine/lib/phases/phase_reconstruct_while_loops.ml @@ -101,7 +101,7 @@ module%inlined_contents Make (FA : Features.T) = struct typ = UB.unit_typ; } | None -> h expr - [@@inline_ands bindings_of dexpr] + [@@inline_ands bindings_of dexpr] [%%inline_defs "Item.*"] end diff --git a/engine/lib/phases/phase_simplify_question_marks.ml b/engine/lib/phases/phase_simplify_question_marks.ml index 3cda9ad7f..22233e33a 100644 --- a/engine/lib/phases/phase_simplify_question_marks.ml +++ b/engine/lib/phases/phase_simplify_question_marks.ml @@ -295,7 +295,7 @@ module%inlined_contents Make (FA : Features.T) = struct let rec dexpr_unwrapped (expr : A.expr) : B.expr = QuestionMarks.extract expr |> Option.value ~default:expr |> [%inline_body dexpr_unwrapped] - [@@inline_ands bindings_of dexpr] + [@@inline_ands bindings_of dexpr] [%%inline_defs "Item.*"] end diff --git a/engine/lib/phases/phase_transform_hax_lib_inline.ml b/engine/lib/phases/phase_transform_hax_lib_inline.ml index 7122047aa..6d739ebaa 100644 --- a/engine/lib/phases/phase_transform_hax_lib_inline.ml +++ b/engine/lib/phases/phase_transform_hax_lib_inline.ml @@ -156,7 +156,7 @@ module%inlined_contents Make (F : Features.T) = struct in Some { contents; witness = Features.On.quote } | _ -> None - [@@inline_ands bindings_of dexpr - dexpr'] + [@@inline_ands bindings_of dexpr - dexpr'] [%%inline_defs "Item.*" - ditems] @@ -199,10 +199,10 @@ module%inlined_contents Make (F : Features.T) = struct item_ident = item.ident; position = (if replace then `Replace - else - match position with - | After -> `After - | Before -> `Before); + else + match position with + | After -> `After + | Before -> `Before); } in Quote { quote; origin } diff --git a/engine/lib/phases/phase_trivialize_assign_lhs.ml b/engine/lib/phases/phase_trivialize_assign_lhs.ml index 030b7528f..540af1485 100644 --- a/engine/lib/phases/phase_trivialize_assign_lhs.ml +++ b/engine/lib/phases/phase_trivialize_assign_lhs.ml @@ -91,7 +91,7 @@ module%inlined_contents Make (F : Features.T) = struct UB.M.expr_Assign ~lhs ~inner_e ~witness ~span ~typ:UB.unit_typ | [%inline_arms "dexpr'.*" - Assign] -> map (fun e -> B.{ e; typ = dty span expr.typ; span }) - [@@inline_ands bindings_of dexpr - dlhs - dexpr'] + [@@inline_ands bindings_of dexpr - dlhs - dexpr'] [%%inline_defs "Item.*"] end diff --git a/engine/lib/side_effect_utils.ml b/engine/lib/side_effect_utils.ml index 8526de37a..801a3b268 100644 --- a/engine/lib/side_effect_utils.ml +++ b/engine/lib/side_effect_utils.ml @@ -171,20 +171,20 @@ struct ~f:(fun (expr, { lbs; effects = effects0 }) (effects, l) -> ( SideEffects.plus effects0 effects, (if - SideEffects.reads_local_mut_only effects0 - && SideEffects.commute effects0 effects - then (lbs, expr) - else - let var = - (* if the body is a local variable, use that, - otherwise get a fresh one *) - match snd @@ U.collect_let_bindings expr with - (* TODO: this optimization is disabled because it fails in cases like f(x, {x = 3; x}) *) - | { e = LocalVar var; _ } when false -> var - | _ -> fresh () - in - ( lbs @ [ (U.make_var_pat var expr.typ expr.span, expr) ], - { expr with e = LocalVar var } )) + SideEffects.reads_local_mut_only effects0 + && SideEffects.commute effects0 effects + then (lbs, expr) + else + let var = + (* if the body is a local variable, use that, + otherwise get a fresh one *) + match snd @@ U.collect_let_bindings expr with + (* TODO: this optimization is disabled because it fails in cases like f(x, {x = 3; x}) *) + | { e = LocalVar var; _ } when false -> var + | _ -> fresh () + in + ( lbs @ [ (U.make_var_pat var expr.typ expr.span, expr) ], + { expr with e = LocalVar var } )) :: l )) in let lbs = List.concat_map ~f:fst l in diff --git a/engine/utils/generate_from_ast/codegen_ast_builder.ml b/engine/utils/generate_from_ast/codegen_ast_builder.ml index e817f041b..de3a23eb4 100644 --- a/engine/utils/generate_from_ast/codegen_ast_builder.ml +++ b/engine/utils/generate_from_ast/codegen_ast_builder.ml @@ -8,7 +8,7 @@ let rec print_ty (t : Type.t) = else "(" ^ (if List.is_empty t.args then "" - else "(" ^ String.concat ~sep:", " (List.map t.args ~f:print_ty) ^ ") ") + else "(" ^ String.concat ~sep:", " (List.map t.args ~f:print_ty) ^ ") ") ^ t.typ ^ ")" let print_record_or_tuple is_record x = @@ -50,12 +50,12 @@ let mk_builder (provided_fields : string list) |> List.map ~f:(fun (name, ty) -> ( true, (if List.mem ~equal:[%eq: string] record_names name then ( - let name' = "inner_" ^ name in - (* if not ([%eq: string] field_name_raw name) then *) - extra_lb := - !extra_lb ^ "let " ^ name ^ " = " ^ name' ^ " in\n"; - name') - else name), + let name' = "inner_" ^ name in + (* if not ([%eq: string] field_name_raw name) then *) + extra_lb := + !extra_lb ^ "let " ^ name ^ " = " ^ name' ^ " in\n"; + name') + else name), ty )) | Tuple types -> List.mapi ~f:(fun i ty -> (false, "x" ^ Int.to_string i, ty)) types diff --git a/engine/utils/generate_from_ast/codegen_ast_destruct.ml b/engine/utils/generate_from_ast/codegen_ast_destruct.ml index 16a4b4b39..150b37ebc 100644 --- a/engine/utils/generate_from_ast/codegen_ast_destruct.ml +++ b/engine/utils/generate_from_ast/codegen_ast_destruct.ml @@ -8,7 +8,7 @@ let rec print_ty (t : Type.t) = else "(" ^ (if List.is_empty t.args then "" - else "(" ^ String.concat ~sep:", " (List.map t.args ~f:print_ty) ^ ") ") + else "(" ^ String.concat ~sep:", " (List.map t.args ~f:print_ty) ^ ") ") ^ t.typ ^ ")" let print_record_or_tuple is_record x = diff --git a/engine/utils/generate_from_ast/codegen_printer.ml b/engine/utils/generate_from_ast/codegen_printer.ml index 3e764c892..cc34663f1 100644 --- a/engine/utils/generate_from_ast/codegen_printer.ml +++ b/engine/utils/generate_from_ast/codegen_printer.ml @@ -99,14 +99,14 @@ and string_ty_of_ty' (state : state) (t : Type.t) = else "(" ^ (if List.is_empty t.args then "" - else - "(" - ^ String.concat ~sep:", " (List.map t.args ~f:(string_ty_of_ty' state)) - ^ ") ") + else + "(" + ^ String.concat ~sep:", " (List.map t.args ~f:(string_ty_of_ty' state)) + ^ ") ") ^ t.typ ^ (if List.mem ~equal:[%eq: string] state.names_with_doc t.typ then - " lazy_doc" - else "") + " lazy_doc" + else "") ^ ")" and is_lazy_doc_typ (state : state) = string_ty_of_ty' state >> is_lazy_doc_typ' @@ -203,8 +203,8 @@ let print_datatype state (dt : Datatype.t) in let body = (if Option.is_some (get_child_type dt.name) then - "\n let super = value in" - else "") + "\n let super = value in" + else "") ^ "\n match value with" ^ String.concat ~sep:"" (List.map diff --git a/engine/utils/generate_from_ast/visitors.ml b/engine/utils/generate_from_ast/visitors.ml index eb67edc91..c2301771c 100644 --- a/engine/utils/generate_from_ast/visitors.ml +++ b/engine/utils/generate_from_ast/visitors.ml @@ -173,8 +173,8 @@ let collect_used_types = let typ = t.typ in self#plus (if String.is_prefix ~prefix:"'" typ || String.equal typ "list" then - self#zero - else Set.singleton (module String) typ) + self#zero + else Set.singleton (module String) typ) (super#visit_Type__t () t) end) #visit_datatypes diff --git a/engine/utils/ppx_generate_features/ppx_generate_features.ml b/engine/utils/ppx_generate_features/ppx_generate_features.ml index 5bd2235c4..51aab8ca1 100644 --- a/engine/utils/ppx_generate_features/ppx_generate_features.ml +++ b/engine/utils/ppx_generate_features/ppx_generate_features.ml @@ -121,56 +121,62 @@ let expand ~(ctxt : Expansion_context.Extension.t) (features : string list) : *) module On = - [%m - List.concat_map - ~f:(fun txt -> - (rename - [ ("placeholder", txt); ("Placeholder", uppercase_first_char txt) ]) - #structure - [%str - module Placeholder : sig - type placeholder - [@@deriving show, yojson, hash, compare, sexp, hash, eq] + [%m + List.concat_map + ~f:(fun txt -> + (rename + [ + ("placeholder", txt); ("Placeholder", uppercase_first_char txt); + ]) + #structure + [%str + module Placeholder : sig + type placeholder + [@@deriving show, yojson, hash, compare, sexp, hash, eq] - val placeholder : placeholder - end = struct - type placeholder = Placeholder - [@@deriving show, yojson, hash, compare, sexp, hash, eq] + val placeholder : placeholder + end = struct + type placeholder = Placeholder + [@@deriving show, yojson, hash, compare, sexp, hash, eq] - let placeholder = Placeholder - end + let placeholder = Placeholder + end - include Placeholder]) - features - |> B.pmod_structure] + include Placeholder]) + features + |> B.pmod_structure] module ToFull = - [%m - List.concat_map - ~f:(fun txt -> - (rename - [ ("placeholder", txt); ("Placeholder", uppercase_first_char txt) ]) - #structure - [%str let placeholder _ = On.placeholder]) - features - |> B.pmod_structure] + [%m + List.concat_map + ~f:(fun txt -> + (rename + [ + ("placeholder", txt); ("Placeholder", uppercase_first_char txt); + ]) + #structure + [%str let placeholder _ = On.placeholder]) + features + |> B.pmod_structure] module Off = - [%m - List.concat_map - ~f:(fun txt -> - (rename - [ ("placeholder", txt); ("Placeholder", uppercase_first_char txt) ]) - #structure - [%str - module Placeholder = struct - type placeholder = | - [@@deriving show, yojson, hash, compare, sexp, hash, eq] - end + [%m + List.concat_map + ~f:(fun txt -> + (rename + [ + ("placeholder", txt); ("Placeholder", uppercase_first_char txt); + ]) + #structure + [%str + module Placeholder = struct + type placeholder = | + [@@deriving show, yojson, hash, compare, sexp, hash, eq] + end - include Placeholder]) - features - |> B.pmod_structure] + include Placeholder]) + features + |> B.pmod_structure] module SUBTYPE = struct module type T = sig @@ -194,69 +200,74 @@ let expand ~(ctxt : Expansion_context.Extension.t) (features : string list) : end module Map (S : T) (Mapper : MAPPER) = - [%m - let f txt = - [%stri - let [%p B.ppat_var { loc; txt }] = - let kind = - [%e - B.pexp_construct - { - loc; - txt = Ldot (Lident "Enumeration", uppercase_first_char txt); - } - None] - in - let f = [%e B.pexp_ident { loc; txt = Ldot (Lident "S", txt) }] in - Mapper.map f kind] - in - B.pmod_structure @@ ([%stri include S] :: List.map ~f features)] + [%m + let f txt = + [%stri + let [%p B.ppat_var { loc; txt }] = + let kind = + [%e + B.pexp_construct + { + loc; + txt = + Ldot (Lident "Enumeration", uppercase_first_char txt); + } + None] + in + let f = + [%e B.pexp_ident { loc; txt = Ldot (Lident "S", txt) }] + in + Mapper.map f kind] + in + B.pmod_structure @@ ([%stri include S] :: List.map ~f features)] module On = - [%m - List.concat_map - ~f:(fun txt -> - (rename - [ - ("placeholder", txt); ("Placeholder", uppercase_first_char txt); - ]) - #structure - [%str - module Placeholder = struct - let placeholder _span _witness = On.placeholder - end + [%m + List.concat_map + ~f:(fun txt -> + (rename + [ + ("placeholder", txt); + ("Placeholder", uppercase_first_char txt); + ]) + #structure + [%str + module Placeholder = struct + let placeholder _span _witness = On.placeholder + end - include Placeholder]) - features - |> B.pmod_structure] + include Placeholder]) + features + |> B.pmod_structure] module Reject (R : sig val reject : 'a. unit -> 'a end) = - [%m - List.concat_map - ~f:(fun txt -> - (rename - [ - ("placeholder", txt); ("Placeholder", uppercase_first_char txt); - ]) - #structure - [%str - module Placeholder = struct - let placeholder _span _witness = R.reject () - end + [%m + List.concat_map + ~f:(fun txt -> + (rename + [ + ("placeholder", txt); + ("Placeholder", uppercase_first_char txt); + ]) + #structure + [%str + module Placeholder = struct + let placeholder _span _witness = R.reject () + end - include Placeholder]) - features - |> B.pmod_structure] + include Placeholder]) + features + |> B.pmod_structure] module Id = - [%m - List.map - ~f:(fun txt -> - [%stri let [%p B.ppat_var { loc; txt }] = fun _span -> Base.Fn.id]) - features - |> B.pmod_structure] + [%m + List.map + ~f:(fun txt -> + [%stri let [%p B.ppat_var { loc; txt }] = fun _span -> Base.Fn.id]) + features + |> B.pmod_structure] end end] (* let attrs = *) diff --git a/engine/utils/sourcemaps/mappings/instruction.ml b/engine/utils/sourcemaps/mappings/instruction.ml index 966e4cba3..922e1593a 100644 --- a/engine/utils/sourcemaps/mappings/instruction.ml +++ b/engine/utils/sourcemaps/mappings/instruction.ml @@ -49,11 +49,11 @@ let rec decode' (s : string) : t option list = |> Option.value ~default:(String.length s) in (if n > 0 then Some (decode_one (String.prefix s n)) - else - match String.get s 0 with - | ';' -> Some (ShiftGenLinesResetGenCols { lines = 1 }) - | ',' -> None - | _ -> failwith "should not be possible") + else + match String.get s 0 with + | ';' -> Some (ShiftGenLinesResetGenCols { lines = 1 }) + | ',' -> None + | _ -> failwith "should not be possible") :: decode' (String.drop_prefix s (Int.max 1 n)) let decode : string -> t list = decode' >> List.filter_map ~f:Fn.id @@ -83,7 +83,7 @@ let from_points : point list -> t list = let shift_gen_col = (if Int.(d.gen.line = 0) then d else x).gen.col in let output = (if Int.(d.gen.line = 0) then [] - else [ ShiftGenLinesResetGenCols { lines = d.gen.line } ]) + else [ ShiftGenLinesResetGenCols { lines = d.gen.line } ]) @ match m with | Some meta -> [ Full { shift_gen_col; shift_src = d.src; meta } ] diff --git a/flake.nix b/flake.nix index 736de0705..168556d28 100644 --- a/flake.nix +++ b/flake.nix @@ -45,7 +45,7 @@ }; rustc = pkgs.rust-bin.fromRustupToolchainFile ./rust-toolchain.toml; craneLib = (crane.mkLib pkgs).overrideToolchain rustc; - ocamlformat = pkgs.ocamlformat_0_24_1; + ocamlformat = pkgs.ocamlformat_0_26_2; rustfmt = pkgs.rustfmt; fstar = inputs.fstar.packages.${system}.default; hax-env-file = pkgs.writeText "hax-env-file" ''