Add new if-conversion pass with top-level fold

1 files changed, 12 insertions, 16 deletions

diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 9719ae6..6693b82 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -35,10 +35,9 @@ Require Import vericert.hls.GibleSeq.
 Require Import vericert.hls.Predicate.
 Require Import vericert.bourdoncle.Bourdoncle.
 
-Definition if_conv_t : Type := PTree.t (list (node * node)).
+Definition if_conv_t : Type := list (node * node).
 
 Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N).
-Parameter get_if_conv_t : program -> list if_conv_t.
 
 #[local] Open Scope positive.
 
@@ -225,7 +224,7 @@ Definition ifconv_list (headers: list node) (c: code) :=
 Definition if_convert_code (c: code) iflist :=
   fold_left (fun s n => if_convert c s (fst n) (snd n)) iflist c.
 
-Definition transf_function (l: if_conv_t) (i: ident) (f: function) : function :=
+Definition transf_function (l: option if_conv_t) (f: function) : function :=
   let (b, _) := build_bourdoncle f in
   let b' := get_loops b in
   let iflist := ifconv_list b' f.(fn_code) in
@@ -235,28 +234,25 @@ Definition transf_function (l: if_conv_t) (i: ident) (f: function) : function :=
 
 Section TRANSF_PROGRAM.
 
-  Context {A B V: Type}.
-  Variable transf: ident -> A -> B.
+  Context {A B V DATA: Type}.
+  Variable transf: option DATA -> A -> B.
 
-  Definition transform_program_globdef' (idg: ident * globdef A V) : ident * globdef B V :=
+  Definition transform_program_globdef' (data: PTree.t DATA) (idg: ident * globdef A V) : ident * globdef B V :=
     match idg with
-    | (id, Gfun f) => (id, Gfun (transf id f))
+    | (id, Gfun f) => (id, Gfun (transf (data!id) f))
     | (id, Gvar v) => (id, Gvar v)
     end.
 
-  Definition transform_program' (p: AST.program A V) : AST.program B V :=
+  Definition transform_program_data (data: PTree.t DATA) (p: AST.program A V) : AST.program B V :=
     mkprogram
-      (List.map transform_program_globdef' p.(prog_defs))
+      (List.map (transform_program_globdef' data) p.(prog_defs))
       p.(prog_public)
           p.(prog_main).
 
 End TRANSF_PROGRAM.
 
-Definition transf_fundef (l: if_conv_t) (i: ident) (fd: fundef) : fundef :=
-  transf_fundef (transf_function l i) fd.
+Definition transf_fundef (l: option if_conv_t) (fd: fundef) : fundef :=
+  transf_fundef (transf_function l) fd.
 
-Definition transf_program_rec (p: program) (l: if_conv_t) : program :=
-  transform_program' (transf_fundef l) p.
-
-Definition transf_program (p: program) : program :=
-  fold_left transf_program_rec (get_if_conv_t p) p.
+Definition transf_program (l: PTree.t if_conv_t) (p: program) : program :=
+  transform_program_data transf_fundef l p.