Fix compilation moving to PTree

3 files changed, 14 insertions, 11 deletions

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 :=