Merge remote-tracking branch 'absint/master' into towards_3.10

Mostly changes in PTree

3 files changed, 56 insertions, 28 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index c10b8ac2..b3895768 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -419,8 +419,7 @@ Lemma transfer_regs_dead inputs rs r:
   ~List.In r inputs -> (transfer_regs inputs rs)#r = Vundef.
 Proof.
   unfold transfer_regs; induction inputs; simpl; intuition subst.
-  - rewrite Regmap.gi; auto.
-  - rewrite Regmap.gso; auto.
+  rewrite Regmap.gso; auto.
 Qed.
 
 Fixpoint union_inputs (f:function) (tbl: list exit): Regset.t :=
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index cf35abad..0cbc46e6 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -380,7 +380,7 @@ Global Opaque hSstore.
 Local Hint Resolve hSstore_correct: wlp.
 
 Definition hrs_sreg_get (hrs: ristate) r: ?? sval :=
-   match PTree.get r hrs with
+   match PTree.get r (ris_sreg hrs) with
    | None => if ris_input_init hrs then hSinput r else hSundef
    | Some sv => RET sv
    end.
@@ -629,15 +629,15 @@ Definition red_PTree_set (r: reg) (sv: sval) (hrs: ristate): PTree.t sval :=
   match (ris_input_init hrs), sv with
   | true, Sinput r' _ =>
       if Pos.eq_dec r r' 
-      then PTree.remove r' hrs
-      else PTree.set r sv hrs
+      then PTree.remove r' (ris_sreg hrs)
+      else PTree.set r sv (ris_sreg hrs)
   | false, Sundef _ =>
-      PTree.remove r hrs
-  | _, _ => PTree.set r sv hrs
+      PTree.remove r (ris_sreg hrs)
+  | _, _ => PTree.set r sv (ris_sreg hrs)
   end.
 
 Lemma red_PTree_set_correct (r r0:reg) sv (hrs: ristate) ctx:
-  sval_refines ctx ((ris_sreg_set hrs (red_PTree_set r sv hrs)) r0) ((ris_sreg_set hrs (PTree.set r sv hrs)) r0).
+  sval_refines ctx ((ris_sreg_set hrs (red_PTree_set r sv hrs)) r0) ((ris_sreg_set hrs (PTree.set r sv (ris_sreg hrs))) r0).
 Proof.
   unfold red_PTree_set, ris_sreg_set, ris_sreg_get; simpl.
   destruct (ris_input_init hrs) eqn:Hinit, sv; simpl; auto.
@@ -703,10 +703,8 @@ Lemma hrs_init_correct:
 Proof.
   unfold hrs_init, sis_init; wlp_simplify.
   econstructor; simpl in *; eauto.
-  + split; destruct 1; econstructor; simpl in *;
+  split; destruct 1; econstructor; simpl in *;
     try rewrite H; try congruence; trivial.
-  + destruct 1; simpl in *. unfold ris_sreg_get; simpl.
-    intros; rewrite PTree.gempty; eauto.
 Qed.
 Local Hint Resolve hrs_init_correct: wlp.
 Global Opaque hrs_init.
@@ -879,8 +877,7 @@ Proof.
       - constructor; simpl; rewrite OK_EQUIV in X; inv X; assumption.
       - rewrite OK_EQUIV; constructor; inv X; assumption.
     * intros X; inv X; simpl; apply MEM_EQ; constructor; auto.
-    * simpl. unfold ris_sreg_get.
-      intros;rewrite PTree.gempty. simpl; auto.
+    * simpl. unfold ris_sreg_get. auto.
   + constructor.
     * erewrite ok_hrset_red_sreg; eauto.
       inv H2. rewrite <- OK_EQUIV.
@@ -1246,21 +1243,56 @@ Hint Resolve option_eq_check_correct:wlp.
 
 Import PTree.
 
-Fixpoint PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit :=
+Fixpoint PTree_eq_check' {A} (d1 d2: PTree.tree' A): ?? unit :=
+    match d1, d2 with
+    | Node001 r1, Node001 r2 => PTree_eq_check' r1 r2
+    | Node010 x1, Node010 x2 =>
+        phys_check x1 x2 "PTree_eq_check': data physically differ"
+    | Node011 x1 r1, Node011 x2 r2 =>
+        phys_check x1 x2 "PTree_eq_check': data physically differ" ;;
+        PTree_eq_check' r1 r2
+    | Node100 l1, Node100 l2 => PTree_eq_check' l1 l2
+    | Node101 l1 r1, Node101 l2 r2 =>
+        PTree_eq_check' l1 l2 ;;
+        PTree_eq_check' r1 r2
+    | Node110 l1 x1, Node110 l2 x2 =>
+        phys_check x1 x2 "PTree_eq_check': data physically differ" ;;
+        PTree_eq_check' l1 l2
+    | Node111 l1 x1 r1, Node111 l2 x2 r2  =>
+        phys_check x1 x2 "PTree_eq_check': data physically differ" ;;
+        PTree_eq_check' l1 l2 ;;
+        PTree_eq_check' r1 r2
+    | _, _ => FAILWITH "PTree_eq_check': different shapes"
+    end.
+
+Lemma PTree_eq_check'_correct A : forall (d1 d2: PTree.tree' A),
+    WHEN PTree_eq_check' d1 d2 ~> _ THEN d1 = d2.
+Proof.
+  induction d1; destruct d2; cbn; wlp_simplify; try congruence.
+Qed.
+                                    
+Definition PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit :=
   match d1, d2 with
-  | Leaf, Leaf => RET tt
-  | Node l1 o1 r1, Node l2 o2 r2 =>
-      option_eq_check o1 o2;;
-      PTree_eq_check l1 l2;;
-      PTree_eq_check r1 r2
-  | _, _ => FAILWITH "PTree_eq_check: some key is absent"
+  | Empty, Empty => RET tt
+  | Nodes m1, Nodes m2 => PTree_eq_check' m1 m2
+  | _, _ => FAILWITH "PTree_eq_check: empty vs nonempty"
   end.
 
+Lemma PTree_eq_check_correct' A : forall (d1 d2: PTree.tree A),
+    WHEN PTree_eq_check d1 d2 ~> _ THEN d1 = d2.
+Proof.
+  Local Hint Resolve PTree_eq_check'_correct: wlp.
+  destruct d1 as [ | m1]; destruct d2 as [ | m2]; cbn; wlp_simplify.
+  congruence.
+Qed.                                    
+
 Lemma PTree_eq_check_correct A d1: forall (d2: t A),
  WHEN PTree_eq_check d1 d2 ~> _ THEN forall x, PTree.get x d1 = PTree.get x d2.
 Proof.
-  induction d1 as [|l1 Hl1 o1 r1 Hr1]; destruct d2 as [|l2 o2 r2]; simpl; 
-  wlp_simplify. destruct x; simpl; auto.
+  Local Hint Resolve PTree_eq_check_correct': wlp.
+  intros.
+  wlp_simplify.
+  congruence.
 Qed.
 Global Opaque PTree_eq_check.
 Local Hint Resolve PTree_eq_check_correct: wlp.
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index d47e53b8..51b562c7 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -32,10 +32,11 @@ Record ristate :=
   }.
 
 Definition ris_sreg_get (ris: ristate) r: sval :=
-   match PTree.get r ris with
+   match PTree.get r (ris_sreg ris) with
    | None => if ris_input_init ris then fSinput r else fSundef
    | Some sv => sv
    end.
+
 Coercion ris_sreg_get: ristate >-> Funclass.
 
 Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate :=
@@ -479,10 +480,8 @@ Lemma ris_init_correct ctx:
   ris_refines ctx ris_init sis_init.
 Proof.
   unfold ris_init, sis_init; econstructor; simpl in *; eauto.
-  + split; destruct 1; econstructor; simpl in *; eauto.
+  split; destruct 1; econstructor; simpl in *; eauto.
     congruence.
-  + destruct 1; simpl in *. unfold ris_sreg_get; simpl.
-    intros; rewrite PTree.gempty; eauto.
 Qed.
 
 Definition rset_smem rm (ris:ristate): ristate :=
@@ -655,8 +654,6 @@ Proof.
   + econstructor; eauto.
     * erewrite ok_transfer_sis, ok_transfer_ris; eauto.
     * erewrite ok_transfer_ris; eauto.
-    * erewrite ok_transfer_ris; simpl; unfold ris_sreg_get; simpl; eauto.
-      intros; rewrite PTree.gempty. simpl; auto.
   + econstructor; eauto.
     * erewrite ok_transfer_sis, ok_transfer_ris; eauto.
     * erewrite ok_transfer_ris; simpl.