diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-29 18:14:59 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-29 18:14:59 +0100 |
| commit | e06577fe952a3c268520b280b020bb2bff252529 (patch) | |
| tree | 6a96dd75f90a81ea80108c909a98bc78ecdabd66 /src/verilog/Verilog.v | |
| parent | 3f3623f533033aca29fc7c5a05d2dad716133811 (diff) | |
| download | vericert-e06577fe952a3c268520b280b020bb2bff252529.tar.gz vericert-e06577fe952a3c268520b280b020bb2bff252529.zip | |
Fix compilation moving to PTree
Diffstat (limited to 'src/verilog/Verilog.v')
| -rw-r--r-- | src/verilog/Verilog.v | 14 |
1 files changed, 7 insertions, 7 deletions
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 := |