feat(engine): add feature for trait item defaults

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
   ]

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 } ->

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
 

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
   ]

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)
 

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 *)

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

engine/lib/features.ml

@@ -25,7 +25,8 @@ loop,
   quote,
   block,
   dyn,
-  match_guard]
+  match_guard,
+  trait_item_default]
 
 module Full = On
 

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,18 +1425,14 @@ 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
              {
                name =
                  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

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)

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

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

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

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 =
       {