From 2e232deb0aed4af2448eb9f1031e8084181174b7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 31 Mar 2022 15:39:18 +0100 Subject: Add list of bb to semantics --- src/hls/RICtransf.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/hls/RICtransf.v') diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v index 643a3a7..3b82b29 100644 --- a/src/hls/RICtransf.v +++ b/src/hls/RICtransf.v @@ -58,7 +58,7 @@ Definition add_bb (should_split: bool) (i: list (list instr)) | (a, b) => if should_split then (a, i::b) else (i::a, b) end. -Fixpoint first_split (saw_pred: bool) (bb: bb) := +Fixpoint first_split (saw_pred: bool) (bb: list bb) := match bb with | a :: b => match includes_setpred a with @@ -72,7 +72,7 @@ Fixpoint first_split (saw_pred: bool) (bb: bb) := | nil => (None, (nil, nil)) end. -Definition split_bb (fresh: node) (b: bb) : bb * bb * bb := +Definition split_bb (fresh: node) (b: list bb) : list bb * list bb * list bb := match first_split false b with | (Some p, (bb1, bb2)) => (bb1 ++ bb2, nil, nil) | (None, (bb1, bb2)) => (bb1 ++ bb2, nil, nil) -- cgit