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/translation/HTLgen.v | |
| parent | 3f3623f533033aca29fc7c5a05d2dad716133811 (diff) | |
| download | vericert-kvx-e06577fe952a3c268520b280b020bb2bff252529.tar.gz vericert-kvx-e06577fe952a3c268520b280b020bb2bff252529.zip | |
Fix compilation moving to PTree
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 24 |
1 files changed, 12 insertions, 12 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. |