Merge pull request #597 from hacspec/allow-default-const-values-in-ge…

…nerics

fix(engine): allow default generics

engine/backends/fstar/fstar_backend.ml

@@ -578,10 +578,8 @@ struct
       let ident = plocal_ident p.ident in
       match p.kind with
       | GPLifetime _ -> Error.assertion_failure span "pgeneric_param:LIFETIME"
-      | GPType { default = None } ->
+      | GPType { default = _ } ->
           { kind; typ = F.term @@ F.AST.Name (F.lid [ "Type" ]); ident }
-      | GPType _ ->
-          Error.unimplemented span ~details:"pgeneric_param:Type with default"
       | GPConst { typ } -> { kind = Explicit; typ = pty span typ; ident }
 
     let of_generic_constraint span (nth : int) (c : generic_constraint) =

engine/lib/import_thir.ml

@@ -1003,9 +1003,8 @@ end) : EXPR = struct
       | Type { default; _ } ->
           let default = Option.map ~f:(c_ty param.span) default in
           GPType { default }
-      | Const { default = Some _; _ } ->
-          unimplemented [ param.span ] "c_generic_param:Const with a default"
-      | Const { default = None; ty } -> GPConst { typ = c_ty param.span ty }
+      (* Rustc always fills in const generics on use. Thus we can drop this information. *)
+      | Const { default = _; ty } -> GPConst { typ = c_ty param.span ty }
     in
     let span = Span.of_thir param.span in
     let attrs = c_attrs param.attributes in

test-harness/src/snapshots/toolchain__generics into-fstar.snap

@@ -29,6 +29,16 @@ Compiling generics v0.1.0 (WORKSPACE_ROOT/generics)
 diagnostics = []
 
 [stdout.files]
+"Generics.Defaults_generics.fst" = '''
+module Generics.Defaults_generics
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_Defaults (v_T: Type) (v_N: usize) = | Defaults : t_Array v_T v_N -> t_Defaults v_T v_N
+
+let f (_: t_Defaults Prims.unit (sz 2)) : Prims.unit = ()
+'''
 "Generics.fst" = '''
 module Generics
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/generics/src/lib.rs

@@ -45,3 +45,9 @@ struct Bar;
 impl Bar {
     fn inherent_impl_generics<T, const N: usize>(x: [T; N]) {}
 }
+
+/// Test defaults types and constants
+mod defaults_generics {
+    struct Defaults<T = (), const N: usize = 2>([T; N]);
+    fn f(_: Defaults) {}
+}