From c276599b9823e7f717a41021bea6df4f0c438c36 Mon Sep 17 00:00:00 2001 From: Paul Mure Date: Tue, 3 Sep 2024 11:38:34 -0700 Subject: [PATCH] fix(engine/backend): import trait goal in concrete impl_expr --- engine/backends/fstar/fstar_backend.ml | 2 +- engine/lib/ast.ml | 2 +- engine/lib/import_thir.ml | 16 ++++++++++------ .../phases/phase_reconstruct_question_marks.ml | 5 ++++- .../lib/phases/phase_simplify_question_marks.ml | 5 ++++- engine/lib/subtype.ml | 4 +++- .../snapshots/toolchain__traits into-fstar.snap | 1 + 7 files changed, 24 insertions(+), 11 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 6430fc633..da0e2dd30 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -343,7 +343,7 @@ struct let some = Option.some in let hax_unstable_impl_exprs = false in match ie with - | Concrete tr -> c_trait_goal span tr |> some + | Concrete { impl = tr; _ } -> c_trait_goal span tr |> some | LocalBound { id } -> let local_ident = Local_ident.{ name = id; id = Local_ident.mk_id Expr 0 } diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index 2bb7ac202..d9356190b 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -143,7 +143,7 @@ functor and impl_expr = | Self - | Concrete of trait_goal + | Concrete of { trait : trait_goal; impl : trait_goal } | LocalBound of { id : string } | Parent of { impl : impl_expr; ident : impl_ident } | Projection of { diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index e479fd013..e836759ea 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1026,7 +1026,7 @@ end) : EXPR = struct (* fun _ -> Ok Bool *) and c_impl_expr (span : Thir.span) (ie : Thir.impl_expr) : impl_expr = - let impl = c_impl_expr_atom span ie.impl in + let impl = c_impl_expr_atom span ie.trait ie.impl in match ie.args with | [] -> impl | args -> @@ -1038,8 +1038,8 @@ end) : EXPR = struct let args = List.map ~f:(c_generic_value span) tr.generic_args in { trait; args } - and c_impl_expr_atom (span : Thir.span) (ie : Thir.impl_expr_atom) : impl_expr - = + and c_impl_expr_atom (span : Thir.span) (trait : Types.trait_ref) + (ie : Thir.impl_expr_atom) : impl_expr = let browse_path (impl : impl_expr) (chunk : Thir.impl_expr_path_chunk) = match chunk with | AssocItem @@ -1062,9 +1062,13 @@ end) : EXPR = struct in match ie with | Concrete { id; generics } -> - let trait = Concrete_ident.of_def_id Impl id in - let args = List.map ~f:(c_generic_value span) generics in - Concrete { trait; args } + let trait = c_trait_ref span trait in + let impl = + let trait = Concrete_ident.of_def_id Impl id in + let args = List.map ~f:(c_generic_value span) generics in + { trait; args } + in + Concrete { trait; impl } | LocalBound { predicate_id; path; _ } -> let init = LocalBound { id = predicate_id } in List.fold ~init ~f:browse_path path diff --git a/engine/lib/phases/phase_reconstruct_question_marks.ml b/engine/lib/phases/phase_reconstruct_question_marks.ml index 174789873..6ef2bddc1 100644 --- a/engine/lib/phases/phase_reconstruct_question_marks.ml +++ b/engine/lib/phases/phase_reconstruct_question_marks.ml @@ -53,7 +53,10 @@ module%inlined_contents Make (FA : Features.T) = struct let expect_residual_impl_result (impl : impl_expr) : impl_expr option = match impl with | ImplApp - { impl = Concrete { trait; _ }; args = [ _; _; _; from_impl ] } + { + impl = Concrete { impl = { trait; _ }; _ }; + args = [ _; _; _; from_impl ]; + } when Concrete_ident.eq_name Core__result__Impl_27 trait -> Some from_impl | _ -> None diff --git a/engine/lib/phases/phase_simplify_question_marks.ml b/engine/lib/phases/phase_simplify_question_marks.ml index 85fd0b16e..1a1d1cada 100644 --- a/engine/lib/phases/phase_simplify_question_marks.ml +++ b/engine/lib/phases/phase_simplify_question_marks.ml @@ -53,7 +53,10 @@ module%inlined_contents Make (FA : Features.T) = struct let expect_residual_impl_result (impl : impl_expr) : impl_expr option = match impl with | ImplApp - { impl = Concrete { trait; _ }; args = [ _; _; _; from_impl ] } + { + impl = Concrete { impl = { trait; _ }; _ }; + args = [ _; _; _; from_impl ]; + } when Concrete_ident.eq_name Core__result__Impl_27 trait -> Some from_impl | _ -> None diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml index 7f180d730..7307d563d 100644 --- a/engine/lib/subtype.ml +++ b/engine/lib/subtype.ml @@ -80,7 +80,9 @@ struct and dimpl_expr (span : span) (i : A.impl_expr) : B.impl_expr = match i with | Self -> Self - | Concrete tr -> Concrete (dtrait_goal span tr) + | Concrete { trait; impl } -> + Concrete + { trait = dtrait_goal span trait; impl = dtrait_goal span impl } | LocalBound { id } -> LocalBound { id } | Parent { impl; ident } -> Parent { impl = dimpl_expr span impl; ident = dimpl_ident span ident } diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index cf3903bb6..fb8f52483 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -195,6 +195,7 @@ let _ = (* This module has implicit dependencies, here we make them explicit. *) (* The implicit dependencies arise from typeclasses instances. *) let open Traits.Implicit_dependencies_issue_667_.Impl_type in + let open Traits.Implicit_dependencies_issue_667_.Trait_definition in () let some_function (x: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) : Prims.unit =