Add AssocMap

1 files changed, 25 insertions, 39 deletions

diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index ba7e83d..c0bce25 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -27,24 +27,21 @@ From Coq Require Import
 
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.Value.
+From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap.
 From compcert Require Integers Events.
 From compcert Require Import Errors Smallstep Globalenvs.
 
 Import HexNotationValue.
-
-Notation "a ! b" := (PositiveMap.find b a) (at level 1).
+Import AssocMapNotation.
 
 Definition reg : Type := positive.
 Definition node : Type := positive.
 Definition szreg : Type := reg * nat.
 
-Definition assocset : Type := PositiveMap.t value.
-
 Record associations : Type :=
   mkassociations {
-    assoc_blocking : assocset;
-    assoc_nonblocking : assocset
+    assoc_blocking : assocmap;
+    assoc_nonblocking : assocmap
   }.
 
 (** * Verilog AST
@@ -58,8 +55,6 @@ The Verilog [value] is a bitvector containg a size and the actual bitvector. In
 this case, the [Word.word] type is used as many theorems about that bitvector
 have already been proven. *)
 
-Definition estate : Type := assocset * assocset.
-
 (** ** Binary Operators
 
 These are the binary operations that can be represented in Verilog. Ideally,
@@ -167,8 +162,7 @@ Record module : Type := mkmodule {
   mod_state : szreg; (**r Variable that defines the current state, it should be internal. *)
   mod_args : list szreg;
   mod_body : list module_item;
-}.
-
+                        }.
 (** Convert a [positive] to an expression directly, setting it to the right
     size. *)
 Definition posToLit (p : positive) : expr :=
@@ -204,8 +198,8 @@ retrieved and set appropriately.
 Inductive state : Type :=
 | State:
     forall (m : module)
-           (assoc : assocset)
-           (nbassoc : assocset)
+           (assoc : assocmap)
+           (nbassoc : assocmap)
            (f : fextclk)
            (cycle : nat)
            (stvar : value),
@@ -246,7 +240,7 @@ Definition unop_run (op : unop) : value -> value :=
   | Vnot => vbitneg
   end.
 
-Inductive expr_runp : fext -> assocset -> expr -> value -> Prop :=
+Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop :=
   | erun_Vlit :
       forall fext assoc v,
       expr_runp fext assoc (Vlit v) v
@@ -312,7 +306,7 @@ Definition access_fext (f : fext) (r : reg) : res value :=
   end.
 
 (* TODO FIX Vvar case without default *)
-(*Fixpoint expr_run (assoc : assocset) (e : expr)
+(*Fixpoint expr_run (assoc : assocmap) (e : expr)
          {struct e} : res value :=
   match e with
   | Vlit v => OK v
@@ -461,7 +455,7 @@ Inductive stmnt_runp: fext -> associations -> stmnt -> associations -> Prop :=
     assoc' = (PositiveMap.add name rhsval assoc) ->
     stmnt_runp f (mkassociations assoc nbassoc)
                  (Vblock lhs rhs)
-                 (mkassociations assoc nbassoc)
+                 (mkassociations assoc' nbassoc)
 | stmnt_runp_Vnonblock:
     forall lhs name rhs rhsval assoc nbassoc nbassoc' f,
     assign_name lhs = OK name ->
@@ -514,28 +508,20 @@ Inductive mis_stepp : fext -> associations -> list module_item -> associations -
     mis_stepp f s nil s.
 Hint Constructors mis_stepp : verilog.
 
-Definition add_assocset (r : reg) (v : value) (assoc : assocset) : assocset :=
-  PositiveMap.add r v assoc.
-
-Definition merge_assocset (nbassoc assoc : assocset) : assocset :=
-  PositiveMap.fold add_assocset nbassoc assoc.
-
-Definition empty_assocset : assocset := PositiveMap.empty value.
-
 (*Definition mi_step_commit (s : state) (m : list module_item) : res state :=
   match mi_step s m with
   | OK (State m assoc nbassoc f c) =>
-    OK (State m (merge_assocset nbassoc assoc) empty_assocset f c)
+    OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c)
   | Error msg => Error msg
   | _ => Error (msg "Verilog: Wrong state")
-  end.*)
+  end.
 
-(*Fixpoint mi_run (f : fextclk) (assoc : assocset) (m : list module_item) (n : nat)
-         {struct n} : res assocset :=
+Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat)
+         {struct n} : res assocmap :=
   match n with
   | S n' =>
     do assoc' <- mi_run f assoc m n';
-    match mi_step_commit (State assoc' empty_assocset f (Pos.of_nat n')) m with
+    match mi_step_commit (State assoc' empty_assocmap f (Pos.of_nat n')) m with
     | OK (State assoc _ _ _) => OK assoc
     | Error m => Error m
     end
@@ -548,12 +534,12 @@ other arguments to the module are also to be supported. *)
 
 Definition initial_fextclk (m : module) : fextclk :=
   fun x => match x with
-           | S O => (add_assocset (fst (mod_reset m)) (ZToValue 1 1) empty_assocset)
-           | _ => (add_assocset (fst (mod_reset m)) (ZToValue 1 0) empty_assocset)
+           | S O => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 1) empty_assocmap)
+           | _ => (AssocMap.add (fst (mod_reset m)) (ZToValue 1 0) empty_assocmap)
            end.
 
-(*Definition module_run (n : nat) (m : module) : res assocset :=
-  mi_run (initial_fextclk m) empty_assocset (mod_body m) n.*)
+(*Definition module_run (n : nat) (m : module) : res assocmap :=
+  mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*)
 
 Local Close Scope error_monad_scope.
 
@@ -601,18 +587,18 @@ Definition genv := Genv.t unit unit.
 Inductive step : state -> state -> Prop :=
 | step_module :
     forall m stvar stvar' cycle f assoc0 assoc1 assoc2 nbassoc,
-    mis_stepp (f cycle) (mkassociations assoc0 empty_assocset)
+    mis_stepp (f cycle) (mkassociations assoc0 empty_assocmap)
               m.(mod_body)
               (mkassociations assoc1 nbassoc) ->
-    assoc2 = merge_assocset nbassoc assoc1 ->
+    assoc2 = merge_assocmap nbassoc assoc1 ->
     Some stvar' = assoc2!(fst m.(mod_state)) ->
-    step (State m assoc0 empty_assocset f cycle stvar)
-         (State m assoc2 empty_assocset f (S cycle) stvar')
+    step (State m assoc0 empty_assocmap f cycle stvar)
+         (State m assoc2 empty_assocmap f (S cycle) stvar')
 | step_finish :
     forall m assoc f cycle stvar result,
     assoc!(fst m.(mod_finish)) = Some (1'h"1") ->
     assoc!(fst m.(mod_return)) = Some result ->
-    step (State m assoc empty_assocset f cycle stvar)
+    step (State m assoc empty_assocmap f cycle stvar)
          (Finishstate result).
 Hint Constructors step : verilog.
 
@@ -620,7 +606,7 @@ Hint Constructors step : verilog.
 | initial_state_intro:
     forall hmi tmi,
     hmi::tmi = mod_body m ->
-    initial_state m (State m hmi tmi empty_assocset empty_assocset (initial_fextclk m) O xH).
+    initial_state m (State m hmi tmi empty_assocmap empty_assocmap (initial_fextclk m) O xH).
 
 (** A final state is a [Returnstate] with an empty call stack. *)