diff options
Diffstat (limited to 'src/hls/HTLPargen.v')
-rw-r--r-- | src/hls/HTLPargen.v | 33 |
1 files changed, 18 insertions, 15 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 88fb9b4..01588f6 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -40,6 +40,8 @@ Hint Resolve AssocMap.gss : htlh. Hint Resolve Ple_refl : htlh. Hint Resolve Ple_succ : htlh. +Definition assignment : Type := expr -> expr -> stmnt. + Record state: Type := mkstate { st_st: reg; st_freshreg: reg; @@ -673,35 +675,33 @@ Fixpoint pred_expr (preg: reg) (p: pred_op) := Vbinop Vor (pred_expr preg p1) (pred_expr preg p2) end. -Definition translate_predicate (preg: reg) (p: option pred_op) (dst e: expr) := +Definition translate_predicate (a : assignment) + (preg: reg) (p: option pred_op) (dst e: expr) := match p with - | None => ret (Vnonblock dst e) + | None => ret (a dst e) | Some pos => - ret (Vnonblock dst (Vternary (pred_expr preg pos) e dst)) + ret (a dst (Vternary (pred_expr preg pos) e dst)) end. -Definition translate_inst (fin rtrn stack preg : reg) (n : node) (i : instr) - : mon unit := +Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) + : mon stmnt := match i with | RBnop => - add_data_instr n Vskip + ret Vskip | RBop p op args dst => do instr <- translate_instr op args; do _ <- declare_reg None dst 32; - do pred <- translate_predicate preg p (Vvar dst) instr; - add_data_instr n pred + translate_predicate a preg p (Vvar dst) instr | RBload p chunk addr args dst => do src <- translate_arr_access chunk addr args stack; do _ <- declare_reg None dst 32; - do pred <- translate_predicate preg p (Vvar dst) src; - add_data_instr n pred + translate_predicate a preg p (Vvar dst) src | RBstore p chunk addr args src => do dst <- translate_arr_access chunk addr args stack; - do pred <- translate_predicate preg p dst (Vvar src); - add_data_instr n pred + translate_predicate a preg p dst (Vvar src) | RBsetpred c args p => do cond <- translate_condition c args; - add_data_instr n (Vnonblock (pred_expr preg (Pvar p)) cond) + ret (a (pred_expr preg (Pvar p)) cond) end. Lemma create_new_state_state_incr: @@ -731,10 +731,13 @@ Definition create_new_state (p: node): mon node := s.(st_funct_units)) (create_new_state_state_incr s p). -Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list instr) := +Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list (list instr)) := match ni with | (n, p, li) => - do _ <- collectlist (translate_inst fin rtrn stack preg n) li; + do _ <- collectlist + (fun l => + do stmnt <- translate_inst Vblock fin rtrn stack preg n l; + add_data_instr n stmnt) (concat li); do st <- get; add_control_instr n (state_goto st.(st_st) p) end. |