From 92c75061155116a1fc5daa5c52a918d149c7ee3c Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 11 Apr 2024 10:24:19 +0200 Subject: [PATCH] fix(engine): allow default generics Default generics are just a nicety provided by Rust, but at the end, Rustc always inline the default when not provided. We don't want to propagate this nicety in the backends, since it's useful only to ease writing new code. Thus, this PR just drops the default information if any. Fixes #596 --- engine/backends/fstar/fstar_backend.ml | 4 +- engine/lib/import_thir.ml | 5 +-- .../toolchain__generics into-fstar.snap | 10 +++++ tests/Cargo.lock | 45 ++----------------- tests/generics/src/lib.rs | 6 +++ 5 files changed, 22 insertions(+), 48 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 5897caa03..ba830aace 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/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) = diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 8c20cdfe9..8555fa751 100644 --- a/engine/lib/import_thir.ml +++ b/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 diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index 64e3362fe..eee521479 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/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" diff --git a/tests/Cargo.lock b/tests/Cargo.lock index e1fad0d42..610369e3c 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -214,12 +214,6 @@ dependencies = [ "cfg-if", ] -[[package]] -name = "dyn-clone" -version = "1.0.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "23d2f3407d9a573d666de4b5bdf10569d73ca9478087346697dcbae6244bfbcd" - [[package]] name = "either" version = "1.9.0" @@ -300,6 +294,9 @@ checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" [[package]] name = "hax-lib" version = "0.1.0-pre.1" +dependencies = [ + "hax-lib-macros", +] [[package]] name = "hax-lib-macros" @@ -318,7 +315,6 @@ version = "0.1.0-pre.1" dependencies = [ "proc-macro2", "quote", - "schemars", "serde", "serde_json", "uuid", @@ -813,30 +809,6 @@ dependencies = [ "winapi-util", ] -[[package]] -name = "schemars" -version = "0.8.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1f7b0ce13155372a76ee2e1c5ffba1fe61ede73fbea5630d61eee6fac4929c0c" -dependencies = [ - "dyn-clone", - "schemars_derive", - "serde", - "serde_json", -] - -[[package]] -name = "schemars_derive" -version = "0.8.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e85e2a16b12bdb763244c69ab79363d71db2b4b918a2def53f80b02e0574b13c" -dependencies = [ - "proc-macro2", - "quote", - "serde_derive_internals", - "syn 1.0.109", -] - [[package]] name = "secret_integers" version = "0.1.7" @@ -862,17 +834,6 @@ dependencies = [ "syn 1.0.109", ] -[[package]] -name = "serde_derive_internals" -version = "0.26.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "85bf8229e7920a9f636479437026331ce11aa132b4dde37d121944a44d6e5f3c" -dependencies = [ - "proc-macro2", - "quote", - "syn 1.0.109", -] - [[package]] name = "serde_json" version = "1.0.99" diff --git a/tests/generics/src/lib.rs b/tests/generics/src/lib.rs index 1f201bbcf..cb14662fd 100644 --- a/tests/generics/src/lib.rs +++ b/tests/generics/src/lib.rs @@ -45,3 +45,9 @@ struct Bar; impl Bar { fn inherent_impl_generics(x: [T; N]) {} } + +/// Test defaults types and constants +mod defaults_generics { + struct Defaults([T; N]); + fn f(_: Defaults) {} +}