Fix compilation moving to PTree

3 files changed, 34 insertions, 25 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 26dc630..4564237 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -120,8 +120,8 @@ Lemma add_instr_state_incr :
        s.(st_st)
        s.(st_freshreg)
        (st_freshstate s)
-       (AssocMap.add n st s.(st_datapath))
-       (AssocMap.add n (state_goto s.(st_st) n') s.(st_controllogic))).
+       (AssocMap.set n st s.(st_datapath))
+       (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
 Proof.
   constructor; intros;
     try (simpl; destruct (peq n n0); subst);
@@ -136,8 +136,8 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
                s.(st_st)
                s.(st_freshreg)
                (st_freshstate s)
-               (AssocMap.add n st s.(st_datapath))
-               (AssocMap.add n (state_goto s.(st_st) n') s.(st_controllogic)))
+               (AssocMap.set n st s.(st_datapath))
+               (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)))
          (add_instr_state_incr s n n' st STM TRANS)
     | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
@@ -151,8 +151,8 @@ Lemma add_instr_skip_state_incr :
        s.(st_st)
        s.(st_freshreg)
        (st_freshstate s)
-       (AssocMap.add n st s.(st_datapath))
-       (AssocMap.add n Vskip s.(st_controllogic))).
+       (AssocMap.set n st s.(st_datapath))
+       (AssocMap.set n Vskip s.(st_controllogic))).
 Proof.
   constructor; intros;
     try (simpl; destruct (peq n n0); subst);
@@ -167,8 +167,8 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
                s.(st_st)
                s.(st_freshreg)
                (st_freshstate s)
-               (AssocMap.add n st s.(st_datapath))
-               (AssocMap.add n Vskip s.(st_controllogic)))
+               (AssocMap.set n st s.(st_datapath))
+               (AssocMap.set n Vskip s.(st_controllogic)))
          (add_instr_skip_state_incr s n st STM TRANS)
     | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
@@ -274,8 +274,8 @@ Lemma add_branch_instr_state_incr:
                  s.(st_st)
                 (st_freshreg s)
                 (st_freshstate s)
-                (AssocMap.add n Vskip (st_datapath s))
-                (AssocMap.add n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
+                (AssocMap.set n Vskip (st_datapath s))
+                (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
 Proof.
   intros. apply state_incr_intro; simpl;
             try (intros; destruct (peq n0 n); subst);
@@ -290,8 +290,8 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
                s.(st_st)
                 (st_freshreg s)
                 (st_freshstate s)
-                (AssocMap.add n Vskip (st_datapath s))
-                (AssocMap.add n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
+                (AssocMap.set n Vskip (st_datapath s))
+                (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
          (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS)
     | _, _ => Error (Errors.msg "Veriloggen: add_branch_instr")
     end.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index b7b9d27..2d2129c 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -26,6 +26,8 @@ Hint Resolve Smallstep.forward_simulation_plus : htlproof.
 Hint Resolve AssocMap.gss : htlproof.
 Hint Resolve AssocMap.gso : htlproof.
 
+Hint Unfold find_assocmap AssocMapExt.get_default : htlproof.
+
 Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
   match_assocmap : forall f rs am,
     (forall r, Ple r (RTL.max_reg_function f) ->
@@ -61,37 +63,39 @@ Inductive match_program : RTL.program -> HTL.module -> Prop :=
     match_program p m.
 Hint Constructors match_program : htlproof.
 
-Lemma regs_lessdef_regs :
+Lemma regs_lessdef_add_greater :
   forall f rs1 rs2 n v,
     Plt (RTL.max_reg_function f) n ->
     match_assocmaps f rs1 rs2 ->
-    match_assocmaps f rs1 (AssocMap.add n v rs2).
+    match_assocmaps f rs1 (AssocMap.set n v rs2).
 Proof.
   inversion 2; subst.
   intros. constructor.
-  intros. unfold find_assocmap. unfold AssocMapExt.find_default.
+  intros. unfold find_assocmap. unfold AssocMapExt.get_default.
   rewrite AssocMap.gso. eauto.
   apply Pos.le_lt_trans with _ _ n in H2.
   unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption.
 Qed.
+Hint Resolve regs_lessdef_add_greater : htlproof.
 
-Lemma regs_add_match :
+Lemma regs_lessdef_add_match :
   forall f rs am r v v',
     val_value_lessdef v v' ->
     match_assocmaps f rs am ->
-    match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.add r v' am).
+    match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am).
 Proof.
   inversion 2; subst.
   constructor. intros.
   destruct (peq r0 r); subst.
   rewrite Registers.Regmap.gss.
-  unfold find_assocmap. unfold AssocMapExt.find_default.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
   rewrite AssocMap.gss. assumption.
 
   rewrite Registers.Regmap.gso; try assumption.
-  unfold find_assocmap. unfold AssocMapExt.find_default.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
   rewrite AssocMap.gso; eauto.
 Qed.
+Hint Resolve regs_lessdef_add_match : htlproof.
 
 Lemma valToValue_lessdef :
   forall v v',
@@ -198,6 +202,11 @@ Section CORRECTNESS.
       exists assoc',
         HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc').
 
+  Lemma greater_than_max_func :
+    forall f st,
+      Plt (RTL.max_reg_function f) st.
+  Proof. Admitted.
+
   Theorem transl_step_correct:
     forall (S1 : RTL.state) t S2,
       RTL.step ge S1 t S2 ->
@@ -218,14 +227,14 @@ Section CORRECTNESS.
       econstructor.
 
       (* prove stval *)
-      unfold merge_assocmap. apply AssocMapExt.merge_add. simpl. apply AssocMap.gss.
+      unfold_merge. simpl. apply AssocMap.gss.
 
       (* prove match_state *)
       rewrite assumption_32bit.
       constructor; auto.
-      unfold merge_assocmap. rewrite AssocMapExt.merge_add. simpl. apply AssocMap.gss.
-      apply regs_lessdef_regs. assumption.
-      unfold state_st_wf. inversion 1. subst. apply AssocMap.gss.
+      unfold_merge. simpl. apply regs_lessdef_regs. apply greater_than_max_func.
+      assumption.
+      unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss.
     - (* Iop *)
       econstructor.
       split.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index b9d483c..5a61a9c 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -16,8 +16,8 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From Coq Require Import FSets.FMapPositive.
 From compcert Require RTL Op Maps Errors.
+From compcert Require Import Maps.
 From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap.
 
 Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
@@ -160,7 +160,7 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr
                (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
 Hint Constructors tr_instr : htlspec.
 
-Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PositiveMap.t stmnt)
+Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
           (fin rtrn st : reg) : Prop :=
   tr_code_intro :
     forall s t,