Commit 7db018ac authored by Michael Sammler's avatar Michael Sammler
Browse files

improve solve_loc_eq

parent 2b7608f5
Pipeline #42423 passed with stage
in 14 minutes and 43 seconds
......@@ -35,7 +35,7 @@ int* roundtrip1(int* p){
[[rc::parameters("p : loc", "n : Z")]]
[[rc::args("p @ &own<n @ int<i32>>")]]
[[rc::returns("p @ &own<n @ int<i32>>")]]
[[rc::tactics("all: try f_equal; solve_loc_eq.")]]
[[rc::tactics("all: try solve_loc_eq.")]]
int* roundtrip2(int* p){
size_t i = (size_t) p;
int *q = (void*) i;
......
......@@ -21,7 +21,7 @@ Section proof_roundtrip2.
- repeat liRStep; liShow.
all: print_typesystem_goal "roundtrip2" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: try f_equal; solve_loc_eq.
all: try solve_loc_eq.
all: print_sidecondition_goal "roundtrip2".
Qed.
End proof_roundtrip2.
......@@ -30,6 +30,7 @@ succeeds if the compared locations have convertible allocation ids. *)
Ltac prepare_loc_eq :=
(* Sanity check on the goal. *)
lazymatch goal with
| |- @eq val (val_of_loc _) (val_of_loc _) => f_equal
| |- @eq ?A _ _ => unify A loc
| |- @eq _ _ _ => fail "[simpl_loc_eq]: goal not an equality between locations"
| |- _ => fail "[simpl_loc_eq]: goal not an equality"
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment