From 36ab0fca83ce41bb906bc49b396f39c814119029 Mon Sep 17 00:00:00 2001
From: LennartBeringer <eberinge@cs.princeton.edu>
Date: Mon, 30 Oct 2023 18:21:27 -0400
Subject: [PATCH] VSU.v: removed some intermediate simplicifications in SC_tac
 as they lead to nontermination in some examples. Variant with
 mk_funspecs_congr likewise fails on some examples that require additional
 change_compspecs applications to user-defined predicates. forward.v: added
 the two compspecs in questions in the warning message to make it more
 informative

---
 floyd/VSU.v     | 39 +++++++++++++++++++++++++++++++++++++--
 floyd/forward.v | 18 +++++++++---------
 2 files changed, 46 insertions(+), 11 deletions(-)

diff --git a/floyd/VSU.v b/floyd/VSU.v
index 2b9d7a3b1..57c93d8ef 100644
--- a/floyd/VSU.v
+++ b/floyd/VSU.v
@@ -880,6 +880,40 @@ Ltac HImports_tac' := clear; repeat apply Forall_cons; try apply Forall_nil;
                        fail "Imports disagree at identifier" i end).
 
 Ltac SC_tac :=
+ match goal with |- SC_test ?ids _ _ =>
+  let a := eval compute in ids in change ids with a
+ end;
+ simpl SC_test;
+ repeat (apply conj);
+ lazymatch goal with
+         | |- Funspecs_must_match ?i _ _ =>
+                 try solve [constructor; unfold abbreviate; 
+                 repeat f_equal
+                 (*occasionally leaves a subgoal, typically because a
+                   change_compspecs needs to be inserted that could not
+                    be identified automatically*)]
+         | |- Identifier_not_found ?i ?fds2 =>
+                 fail "identifer" i "not found in funspecs" fds2
+         | |- True => trivial
+          end.
+(*Alternatives:
+Ltac SC_tac1 :=
+ match goal with |- SC_test ?ids _ _ =>
+  let a := eval compute in ids in change ids with a
+ end;
+ simpl SC_test;
+ repeat (apply conj);
+ lazymatch goal with
+         | |- Funspecs_must_match ?i _ _ =>
+                 try solve [constructor; unfold abbreviate; 
+                 (*leads sometimes to nontermination: try simple apply eq_refl;*)
+                 repeat f_equal]
+         | |- Identifier_not_found ?i ?fds2 =>
+                 fail "identifer" i "not found in funspecs" fds2
+         | |- True => trivial
+          end.
+
+Ltac SC_tac2 :=
  match goal with |- SC_test ?ids _ _ =>
   let a := eval compute in ids in change ids with a
  end;
@@ -892,12 +926,13 @@ Ltac SC_tac :=
                  [ try reflexivity 
                  | try reflexivity 
                  | try reflexivity
-                 | try (apply eq_JMeq; trivial)
-                 | try (apply eq_JMeq; trivial)]
+                 | (*too aggressive here: try (apply eq_JMeq; trivial)*)
+                 | (*too aggressive here: try (apply eq_JMeq; trivial)*)]
          | |- Identifier_not_found ?i ?fds2 =>
                  fail "identifer" i "not found in funspecs" fds2
          | |- True => trivial
           end.
+*)
 
 Ltac HImports_tac := simpl;
   let i := fresh "i" in 
diff --git a/floyd/forward.v b/floyd/forward.v
index de09acda9..134fe5cde 100644
--- a/floyd/forward.v
+++ b/floyd/forward.v
@@ -712,9 +712,9 @@ a "versus" b ")"
  else fail
 end.
 
-Ltac change_compspecs_warning A := 
-     idtac "Remark: change_compspecs on user-defined mpred:" A
- "(to disable this message, Ltac change_compspecs_warning A ::= idtac".
+Ltac change_compspecs_warning A cs cs' := 
+     idtac "Remark: change_compspecs on user-defined mpred:" A cs cs'
+ "(to disable this message, Ltac change_compspecs_warning A cs cs' ::= idtac".
 
 Ltac change_compspecs' cs cs' :=
   lazymatch goal with
@@ -725,22 +725,22 @@ Ltac change_compspecs' cs cs' :=
   | |- _ => 
     match goal with 
   | |- context [?A cs'] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs') with (A cs)
   | |- context [?A cs' ?B] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs' B) with (A cs B)
   | |- context [?A cs' ?B ?C] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs' B C) with (A cs B C)
   | |- context [?A cs' ?B ?C ?D] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs' B C D) with (A cs B C D)
   | |- context [?A cs' ?B ?C ?D ?E] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs' B C D E) with (A cs B C D E)
   | |- context [?A cs' ?B ?C ?D ?E ?F] => 
-     change_compspecs_warning A;
+     change_compspecs_warning A cs cs';
          change (A cs' B C D E F) with (A cs B C D E F)
    end
  end.