diff options
Diffstat (limited to 'src/hls/RICtransf.v')
| -rw-r--r-- | src/hls/RICtransf.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v index 3b82b29..886c23d 100644 --- a/src/hls/RICtransf.v +++ b/src/hls/RICtransf.v @@ -49,11 +49,10 @@ Fixpoint existsb_val {A B} (f: A -> option B) (l : list A) : option B := end end. -Definition includes_setpred (bb: list (list instr)) := - existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end)) bb. +Definition includes_setpred (bb: bb) := + existsb_val (existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end))) bb. -Definition add_bb (should_split: bool) (i: list (list instr)) - (bbc: list (list (list instr)) * list (list (list instr))) := +Definition add_bb (should_split: bool) (i: bb) (bbc: list bb * list bb) := match bbc with | (a, b) => if should_split then (a, i::b) else (i::a, b) end. |