From 84f2068fe2f0367647d8c237220c81438998ec54 Mon Sep 17 00:00:00 2001 From: Paul Mure Date: Mon, 5 Aug 2024 16:04:04 -0700 Subject: [PATCH] feat(engine): add feature for trait item defaults --- engine/backends/coq/coq/coq_backend.ml | 5 +++- .../backends/coq/ssprove/ssprove_backend.ml | 8 ++++-- .../backends/easycrypt/easycrypt_backend.ml | 1 + engine/backends/fstar/fstar_backend.ml | 5 +++- engine/backends/proverif/proverif_backend.ml | 1 + engine/lib/ast.ml | 9 ++++++- engine/lib/diagnostics.ml | 1 + engine/lib/features.ml | 3 ++- engine/lib/import_thir.ml | 26 +++++++++++------- engine/lib/phases/phase_and_mut_defsite.ml | 4 +++ engine/lib/phases/phase_reject.ml | 18 +++++++++++++ engine/lib/phases/phase_traits_specs.ml | 1 + engine/lib/print_rust.ml | 27 ++++++++++++------- engine/lib/subtype.ml | 7 +++++ 14 files changed, 92 insertions(+), 24 deletions(-) diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 8cad93684..a4564bb5a 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -42,7 +42,8 @@ module SubtypeToInputLanguage and type quote = Features.Off.quote and type state_passing_loop = Features.Off.state_passing_loop and type dyn = Features.Off.dyn - and type match_guard = Features.Off.match_guard) = + and type match_guard = Features.Off.match_guard + and type trait_item_default = Features.Off.trait_item_default) = struct module FB = InputLanguage @@ -575,6 +576,7 @@ struct ( U.Concrete_ident_view.to_definition_name x.ti_ident, match x.ti_v with | TIFn fn_ty -> pty span fn_ty + | TIDefault _ -> . | _ -> __TODO_ty__ span "field_ty" )) items ); ] @@ -719,6 +721,7 @@ module TransformToInputLanguage = |> Phases.Functionalize_loops |> Phases.Reject.As_pattern |> Phases.Reject.Dyn + |> Phases.Reject.Trait_item_default |> SubtypeToInputLanguage |> Identity ] diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml index b9cc001cd..7d8207385 100644 --- a/engine/backends/coq/ssprove/ssprove_backend.ml +++ b/engine/backends/coq/ssprove/ssprove_backend.ml @@ -42,7 +42,8 @@ module SubtypeToInputLanguage and type quote = Features.Off.quote and type block = Features.Off.block and type dyn = Features.Off.dyn - and type match_guard = Features.Off.match_guard) = + and type match_guard = Features.Off.match_guard + and type trait_item_default = Features.Off.trait_item_default) = struct module FB = InputLanguage @@ -585,6 +586,7 @@ module TransformToInputLanguage (* : PHASE *) = (* |> Phases.Functionalize_loops *) |> Phases.Reject.As_pattern |> Phases.Reject.Dyn + |> Phases.Reject.Trait_item_default |> SubtypeToInputLanguage |> Identity ] @@ -1762,7 +1764,8 @@ struct SSP.AST.NameTy (pconcrete_ident x.ti_ident); ] ) )) - impl_idents) + impl_idents + | _ -> .) items ); ] @ List.concat_map @@ -1773,6 +1776,7 @@ struct SSP.AST.HintUnfold (pconcrete_ident x.ti_ident ^ "_loc", None); ] + | TIDefault _ -> . | _ -> []) items | Impl { generics; self_ty; of_trait = name, gen_vals; items } -> diff --git a/engine/backends/easycrypt/easycrypt_backend.ml b/engine/backends/easycrypt/easycrypt_backend.ml index 206db2496..fd5bbc02f 100644 --- a/engine/backends/easycrypt/easycrypt_backend.ml +++ b/engine/backends/easycrypt/easycrypt_backend.ml @@ -60,6 +60,7 @@ module RejectNotEC (FA : Features.T) = struct let quote = reject let dyn = reject let match_guard = reject + let trait_item_default = reject let construct_base _ _ = Features.On.construct_base let for_index_loop _ _ = Features.On.for_index_loop diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 5c58e855e..5f48597a3 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -41,7 +41,8 @@ module SubtypeToInputLanguage and type while_loop = Features.Off.while_loop and type for_index_loop = Features.Off.for_index_loop and type state_passing_loop = Features.Off.state_passing_loop - and type match_guard = Features.Off.match_guard) = + and type match_guard = Features.Off.match_guard + and type trait_item_default = Features.Off.trait_item_default) = struct module FB = InputLanguage @@ -1332,6 +1333,7 @@ struct (generics |> List.map ~f:FStarBinder.to_binder, ty) in [ (F.id name, None, [], ty) ] + | _ -> . in List.map ~f:Fn.id (* ~f:(fun (n, q, a, ty) -> (n, q, a, F.mk_e_app bds ty)) *) @@ -1686,6 +1688,7 @@ module TransformToInputLanguage = |> Phases.Traits_specs |> Phases.Simplify_hoisting |> Phases.Newtype_as_refinement + |> Phases.Reject.Trait_item_default |> SubtypeToInputLanguage |> Identity ] diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 2146c2bac..8a65f6246 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -78,6 +78,7 @@ struct let block = reject let dyn = reject let match_guard = reject + let trait_item_default = reject let metadata = Phase_reject.make_metadata (NotInBackendLang ProVerif) end) diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index 10495a620..563b8002f 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -443,7 +443,14 @@ functor ii_attrs : attrs; } - and trait_item' = TIType of impl_ident list | TIFn of ty + and trait_item' = + | TIType of impl_ident list + | TIFn of ty + | TIDefault of { + params : param list; + body : expr; + witness : F.trait_item_default; + } and trait_item = { (* TODO: why do I need to prefix by `ti_` here? I guess visitors fail or something *) diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml index 2e26d733a..66cd25dcd 100644 --- a/engine/lib/diagnostics.ml +++ b/engine/lib/diagnostics.ml @@ -16,6 +16,7 @@ module Phase = struct | EarlyExit | AsPattern | Dyn + | TraitItemDefault [@@deriving show { with_path = false }, eq, yojson, compare, hash, sexp] let display = function diff --git a/engine/lib/features.ml b/engine/lib/features.ml index 852b0b4ab..82be3dc1d 100644 --- a/engine/lib/features.ml +++ b/engine/lib/features.ml @@ -25,7 +25,8 @@ loop, quote, block, dyn, - match_guard] + match_guard, + trait_item_default] module Full = On diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 9e6e8a811..4cef3c46e 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -226,6 +226,7 @@ module type EXPR = sig val c_generic_value : Thir.span -> Thir.generic_arg -> generic_value val c_generics : Thir.generics -> generics val c_param : Thir.span -> Thir.param -> param + val c_fn_params : Thir.span -> Thir.param list -> param list val c_trait_item' : Thir.trait_item -> Thir.trait_item_kind -> trait_item' val c_trait_ref : Thir.span -> Thir.trait_ref -> trait_goal val c_impl_expr : Thir.span -> Thir.impl_expr -> impl_expr @@ -1114,6 +1115,10 @@ end) : EXPR = struct attrs = c_attrs param.attributes; } + let c_fn_params span (params : Thir.param list) : param list = + if List.is_empty params then [ U.make_unit_param (Span.of_thir span) ] + else List.map ~f:(c_param span) params + let c_generic_param (param : Thir.generic_param) : generic_param = let ident = let kind = @@ -1184,11 +1189,11 @@ end) : EXPR = struct trait_item' = let span = super.span in match item with - | Const (_, Some _) -> - unimplemented [ span ] - "TODO: traits: no support for defaults in traits for now" + | Const (_, Some default) -> + TIDefault + { params = []; body = c_expr default; witness = W.trait_item_default } | Const (ty, None) -> TIFn (c_ty span ty) - | ProvidedFn (sg, _) | RequiredFn (sg, _) -> + | RequiredFn (sg, _) -> let (Thir.{ inputs; output; _ } : Thir.fn_decl) = sg.decl in let output = match output with @@ -1200,6 +1205,13 @@ end) : EXPR = struct else List.map ~f:(c_ty span) inputs in TIFn (TArrow (inputs, output)) + | ProvidedFn (_, { params; body; _ }) -> + TIDefault + { + params = c_fn_params span params; + body = c_expr body; + witness = W.trait_item_default; + } | Type (bounds, None) -> let bounds = List.filter_map ~f:(c_clause span) bounds @@ -1413,10 +1425,6 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = ty = c_ty item.span ty; } | Fn (generics, { body; params; _ }) -> - let params = - if List.is_empty params then [ U.make_unit_param span ] - else List.map ~f:(c_param item.span) params - in mk @@ Fn { @@ -1424,7 +1432,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = Concrete_ident.of_def_id Value (Option.value_exn item.def_id); generics = c_generics generics; body = c_body body; - params; + params = c_fn_params item.span params; } | Enum (variants, generics, repr) -> let def_id = Option.value_exn item.def_id in diff --git a/engine/lib/phases/phase_and_mut_defsite.ml b/engine/lib/phases/phase_and_mut_defsite.ml index 25583e2f1..8a43df7ee 100644 --- a/engine/lib/phases/phase_and_mut_defsite.ml +++ b/engine/lib/phases/phase_and_mut_defsite.ml @@ -286,6 +286,10 @@ struct let output = body.typ in let ty = B.TArrow (inputs, output) in Some (B.TIFn ty) + | TIDefault { params; body; witness } -> + let* params, body = rewrite_function params body in + let witness = S.trait_item_default span witness in + Some (B.TIDefault { params; body; witness }) | _ -> None) |> Option.value_or_thunk ~default:(Fn.flip super#visit_trait_item' item.ti_v) diff --git a/engine/lib/phases/phase_reject.ml b/engine/lib/phases/phase_reject.ml index daf1e5fe3..df2bb9e7e 100644 --- a/engine/lib/phases/phase_reject.ml +++ b/engine/lib/phases/phase_reject.ml @@ -116,3 +116,21 @@ module Dyn (FA : Features.T) = struct let metadata = make_metadata Dyn end) end + +module Trait_item_default (FA : Features.T) = struct + module FB = struct + include FA + include Features.Off.Trait_item_default + end + + include + Feature_gate.Make (FA) (FB) + (struct + module A = FA + module B = FB + include Feature_gate.DefaultSubtype + + let trait_item_default = reject + let metadata = make_metadata TraitItemDefault + end) +end diff --git a/engine/lib/phases/phase_traits_specs.ml b/engine/lib/phases/phase_traits_specs.ml index 6f31247a2..79d17ae3f 100644 --- a/engine/lib/phases/phase_traits_specs.ml +++ b/engine/lib/phases/phase_traits_specs.ml @@ -62,6 +62,7 @@ module Make (F : Features.T) = ] | TIFn _ -> [ (* REFINEMENTS FOR CONSTANTS? *) ] | TIType _ -> [ (* TODO REFINEMENTS FOR TYPES *) ] + | TIDefault _ -> [ (* TODO REFINEMENTS FOR DEFAULT ITEMS *) ] in let items = List.concat_map diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml index de4a64962..900921b62 100644 --- a/engine/lib/print_rust.ml +++ b/engine/lib/print_rust.ml @@ -458,6 +458,15 @@ module Raw = struct let ( ! ) = pure span in concat ~sep:!", " (List.map ~f:(pvariant span) variants) + let pparam span ({ pat; typ; typ_span; attrs } : param) = + let ( ! ) = pure span in + pattrs attrs & ppat pat & !": " + & pty (Option.value ~default:pat.span typ_span) typ + + let pparams span (l : param list) = + let ( ! ) = pure span in + !"(" & List.map ~f:(pparam span) l |> concat ~sep:!"," & !")" + let ptrait_item (ti : trait_item) = let ( ! ) = pure ti.ti_span in let generics = pgeneric_params ti.ti_generics.params in @@ -480,15 +489,15 @@ module Raw = struct in !"fn " & ident & generics & !"(" & params & !") -> " & return_type & bounds & !";" - - let pparam span ({ pat; typ; typ_span; attrs } : param) = - let ( ! ) = pure span in - pattrs attrs & ppat pat & !": " - & pty (Option.value ~default:pat.span typ_span) typ - - let pparams span (l : param list) = - let ( ! ) = pure span in - !"(" & List.map ~f:(pparam span) l |> concat ~sep:!"," & !")" + | TIDefault { params; body; _ } -> + let params = pparams ti.ti_span params in + let generics_constraints = + pgeneric_constraints ti.ti_span ti.ti_generics.constraints + in + let return_type = pty ti.ti_span body.typ in + let body = pexpr body in + !"fn " & ident & generics & !"(" & params & !") -> " & return_type + & generics_constraints & !"{" & body & !"}" let pimpl_item (ii : impl_item) = let span = ii.ii_span in diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml index 8d33834fb..a2fc68e19 100644 --- a/engine/lib/subtype.ml +++ b/engine/lib/subtype.ml @@ -409,6 +409,13 @@ struct match ti with | TIType idents -> TIType (List.map ~f:(dimpl_ident span) idents) | TIFn t -> TIFn (dty span t) + | TIDefault { params; body; witness } -> + TIDefault + { + params = List.map ~f:(dparam span) params; + body = dexpr body; + witness = S.trait_item_default span witness; + } and dtrait_item (ti : A.trait_item) : B.trait_item = {