Merge pull request #739 from PrincetonUniversity/SC_tac

Adjusted SC_tac, adjusted change_compspecs warning message, store_tac

Author: andrew-appel

floyd/VSU.v

@@ -888,13 +888,52 @@ Ltac SC_tac :=
  lazymatch goal with
          | |- Funspecs_must_match ?i _ _ =>
                  try solve [constructor; unfold abbreviate; 
-                 try simple apply eq_refl;
+                 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;
+ simpl SC_test;
+ repeat (apply conj);
+ lazymatch goal with
+         | |- Funspecs_must_match ?i _ _ =>
+                 constructor;
+                 apply mk_funspec_congr;
+                 [ try reflexivity 
+                 | try reflexivity 
+                 | try reflexivity
+                 | (*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 
    intros i ? ? H1 H2;

floyd/forward.v

@@ -712,6 +712,10 @@ a "versus" b ")"
  else fail
 end.
 
+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
   | |- context [@data_at cs' ?sh ?t ?v1] => erewrite (@data_at_change_composite cs' cs _ sh t); [| apply JMeq_refl | prove_cs_preserve_type]
@@ -721,22 +725,22 @@ Ltac change_compspecs' cs cs' :=
   | |- _ => 
     match goal with 
   | |- context [?A cs'] => 
-     idtac "Warning: attempting change_compspecs on user-defined mpred:" A;
+     change_compspecs_warning A cs cs';
          change (A cs') with (A cs)
   | |- context [?A cs' ?B] => 
-     idtac "Warning: attempting change_compspecs on user-defined mpred:" A;
+     change_compspecs_warning A cs cs';
          change (A cs' B) with (A cs B)
   | |- context [?A cs' ?B ?C] => 
-     idtac "Warning: attempting change_compspecs on user-defined mpred:" A;
+     change_compspecs_warning A cs cs';
          change (A cs' B C) with (A cs B C)
   | |- context [?A cs' ?B ?C ?D] => 
-     idtac "Warning: attempting change_compspecs on user-defined mpred:" 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] => 
-     idtac "Warning: attempting change_compspecs on user-defined mpred:" 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] => 
-     idtac "Warning: attempting change_compspecs on user-defined mpred:" 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.

floyd/simpl_reptype.v

@@ -335,15 +335,17 @@ Ltac subst_indexes gfs :=
   end.
 
 Ltac solve_store_rule_evaluation :=
-  match goal with |- upd_reptype ?t ?gfs ?v0 ?v1 = ?B =>
+  match goal with |- @upd_reptype ?cs ?t ?gfs ?v0 ?v1 = ?B =>
    let rhs := fresh "rhs" in set (rhs := B);
   match type of rhs with ?A =>
    let a := fresh "a" in set (a:=A) in rhs; 
     lazy beta zeta iota delta [reptype reptype_gen] in a;
     cbn in a; subst a
   end;
    let h0 := fresh "h0" in let h1 := fresh "h1" in
-   set (h0:=v0); set (h1:=v1); change (upd_reptype t gfs h0 h1 = rhs);
+   set (h0:=v0 : @reptype cs t); 
+   set (h1:=v1 : @reptype cs (@nested_field_type cs t gfs)); 
+   change (upd_reptype t gfs h0 h1 = rhs);
    remember_indexes gfs;
    let j := fresh "j" in match type of h0 with ?J => set (j := J) in h0 end;
    lazy beta zeta iota delta in j; subst j;