Fix compilation moving to PTree

6 files changed, 48 insertions, 36 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,
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index 43f9065..88b13a6 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -198,6 +198,10 @@ Definition empty_assocmap : assocmap := AssocMap.empty value.
 
 Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value.
 
+Ltac unfold_merge :=
+  unfold merge_assocmap; try (repeat (rewrite merge_add_assoc));
+  rewrite AssocMapExt.merge_base_1.
+
 Module AssocMapNotation.
   Notation "a ! b" := (AssocMap.get b a) (at level 1).
   Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1).
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 36e4434..a21064c 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -20,6 +20,7 @@ From Coq Require Import FSets.FMapPositive.
 From coqup Require Import Coquplib Value AssocMap.
 From coqup Require Verilog.
 From compcert Require Events Globalenvs Smallstep Integers.
+From compcert Require Import Maps.
 
 Import HexNotationValue.
 
@@ -29,13 +30,11 @@ hardware-like layout that is still similar to the register transfer language
 instantiations and that we now describe a state machine instead of a
 control-flow graph. *)
 
-Notation "a ! b" := (PositiveMap.find b a) (at level 1).
-
 Definition reg := positive.
 Definition node := positive.
 
-Definition datapath := PositiveMap.t Verilog.stmnt.
-Definition controllogic := PositiveMap.t Verilog.stmnt.
+Definition datapath := PTree.t Verilog.stmnt.
+Definition controllogic := PTree.t Verilog.stmnt.
 
 Record module: Type :=
   mkmodule {
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index c1e0a79..ce7ddd9 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -171,13 +171,13 @@ Definition posToLit (p : positive) : expr :=
 Coercion Vlit : value >-> expr.
 Coercion Vvar : reg >-> expr.
 
-Definition fext := PositiveMap.t value.
+Definition fext := AssocMap.t value.
 Definition fextclk := nat -> fext.
 
 (** ** State
 
 The [state] contains the following items:
-
+n
 - Current [module] that is being worked on, so that the state variable can be
 retrieved and set appropriately.
 - Current [module_item] which is being worked on.
@@ -300,7 +300,7 @@ Definition handle_def {A : Type} (a : A) (val : option A)
 Local Open Scope error_monad_scope.
 
 Definition access_fext (f : fext) (r : reg) : res value :=
-  match PositiveMap.find r f with
+  match AssocMap.get r f with
   | Some v => OK v
   | _ => OK (ZToValue 1 0)
   end.
@@ -452,7 +452,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
     forall lhs name rhs rhsval assoc assoc' nbassoc f,
     assign_name lhs = OK name ->
     expr_runp f assoc rhs rhsval ->
-    assoc' = (PositiveMap.add name rhsval assoc) ->
+    assoc' = (AssocMap.set name rhsval assoc) ->
     stmnt_runp f (mkassociations assoc nbassoc)
                  (Vblock lhs rhs)
                  (mkassociations assoc' nbassoc)
@@ -460,7 +460,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
     forall lhs name rhs rhsval assoc nbassoc nbassoc' f,
     assign_name lhs = OK name ->
     expr_runp f assoc rhs rhsval ->
-    nbassoc' = (PositiveMap.add name rhsval nbassoc) ->
+    nbassoc' = (AssocMap.set name rhsval nbassoc) ->
     stmnt_runp f (mkassociations assoc nbassoc)
                  (Vnonblock lhs rhs)
                  (mkassociations assoc nbassoc').
@@ -534,8 +534,8 @@ other arguments to the module are also to be supported. *)
 
 Definition initial_fextclk (m : module) : fextclk :=
   fun x => match x with
-           | S O => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap)
-           | _ => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap)
+           | S O => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap)
+           | _ => (AssocMap.set (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap)
            end.
 
 (*Definition module_run (n : nat) (m : module) : res assocmap :=