From 34fcf895a3924a2def0026cec03bb030555529a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Mon, 3 Mar 2025 09:41:20 +0100
Subject: [PATCH] fix
---
case_studies/tests/src/trait_deps.rs | 57 +++++++++--------------
theories/rust_typing/automation/solvers.v | 20 +++++---
2 files changed, 36 insertions(+), 41 deletions(-)
diff --git a/case_studies/tests/src/trait_deps.rs b/case_studies/tests/src/trait_deps.rs
index d164a0a..ac52631 100644
--- a/case_studies/tests/src/trait_deps.rs
+++ b/case_studies/tests/src/trait_deps.rs
@@ -99,21 +99,21 @@ mod dep3 {
}
}
-mod dep4 {
+/// Check that lifetime parameters are resolved correctly.
+mod dep6 {
+ trait Foo { }
- trait Bar {
- type BT;
- }
+ impl<'a, T> Foo for &'a T { }
- // TODO: does not work -- the base spec is currently not aware of the Self req.
- // debug more.
- trait Foo: Bar {
- //#[rr::exists("x")]
- //#[rr::returns("x")]
- fn foo() -> Self::BT;
+ #[rr::verify]
+ fn foo<U: Foo>(x: U) {
}
+ #[rr::verify]
+ fn call_foo<T>(x: T) {
+ foo(&x);
+ }
}
mod dep7 {
@@ -138,6 +138,7 @@ mod dep7 {
}
+/// HRTB tests
mod dep5 {
trait Foo<T> {
@@ -157,8 +158,6 @@ mod dep5 {
}
- // Q: how do I show that I satisfy a HRTB requirement?
- // - by finding an impl which can be partially instantiated accordingly.
impl<'a> Foo<&'a i32> for i32 {
#[rr::default_spec]
fn foo(&self, x: &'a i32) {
@@ -166,8 +165,7 @@ mod dep5 {
}
}
- // TODO fix
- //#[rr::verify]
+ #[rr::verify]
fn call_bla2() {
bla(42);
}
@@ -189,15 +187,6 @@ mod dep5 {
let y = 42;
let y_ref = &y;
-
- // Now I'm calling that function of the generic trait requirement.
- // - TODO In the function spec assumption, I need to quantify over that as well.
- // - TODO I need to instantiate the lifetimes.
- // => i.e., when computing the generic abstraction, I need to take these into account.
- // I guess we'll need to do some work to compute the instantiation, because it is not
- // apparent from the args. Maybe do some unification again, this time based on the
- // function's args?
-
x.foo(&y_ref);
}
@@ -210,20 +199,18 @@ mod dep5 {
}
-/*
-mod dep6 {
- trait Foo { }
-
- impl<'a, T> Foo for &'a T { }
-
+mod dep4 {
- #[rr::verify]
- fn foo<U: Foo>(x: U) {
+ trait Bar {
+ type BT;
}
- #[rr::verify]
- fn call_foo<T>(x: T) {
- foo(&x);
+ // TODO: does not work -- the base spec is currently not aware of the Self req.
+ // debug more.
+ trait Foo: Bar {
+
+ //#[rr::exists("x")]
+ //#[rr::returns("x")]
+ fn foo() -> Self::BT;
}
}
-*/
diff --git a/theories/rust_typing/automation/solvers.v b/theories/rust_typing/automation/solvers.v
index 59f5f5c..48a06f9 100644
--- a/theories/rust_typing/automation/solvers.v
+++ b/theories/rust_typing/automation/solvers.v
@@ -3578,6 +3578,12 @@ Ltac function_subtype_solve_trait :=
Global Hint Extern 3 (FunctionSubtype _ _) => function_subtype_solve_trait : typeclass_instances.
+Ltac strip_all_applied_params a acc cont :=
+ match a with
+ | ?a1 ?a2 =>
+ strip_all_applied_params a1 uconstr:(a2 +:: acc) cont
+ | _ => cont a acc
+ end.
Ltac solve_trait_incl :=
lazymatch goal with
| |- trait_incl_marker ?P =>
@@ -3593,17 +3599,19 @@ Ltac solve_trait_incl :=
first [
(* look for an assumption we can specialize *)
is_var spec1;
- idtac spec1 spec1_tys spec1_lfts;
prove_trait_incl_for spec1 spec1_tys spec1_lfts ltac:(fun t1 t2 H2 =>
(* TODO: ideally, we should use transitivity instead and then go on *)
apply H2
)
| (* directly solve the inclusion *)
- hnf;
- intros;
- split_and?;
- intros;
- first [solve_function_subtype | done ]
+ (* first unfold the inclusion *)
+ strip_all_applied_params incl (hnil id) ltac:(fun a _ =>
+ unfold a;
+ intros;
+ split_and?;
+ intros;
+ first [solve_function_subtype | done ]
+ )
]
)
end
--
GitLab