1 files changed, 19 insertions, 0 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 0b1c852..ce6149b 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -230,6 +230,25 @@ Definition transf_function (f: function) : function :=
              (if_convert_code f.(fn_code) iflist)
              f.(fn_entrypoint).
 
+Section TRANSF_PROGRAM.
+
+Variable A B V: Type.
+Variable transf: ident -> A -> B.
+
+Definition transform_program_globdef (idg: ident * globdef A V) : ident * globdef B V :=
+  match idg with
+  | (id, Gfun f) => (id, Gfun (transf id f))
+  | (id, Gvar v) => (id, Gvar v)
+  end.
+
+Definition transform_program (p: AST.program A V) : AST.program B V :=
+  mkprogram
+    (List.map transform_program_globdef p.(prog_defs))
+    p.(prog_public)
+    p.(prog_main).
+
+End TRANSF_PROGRAM.
+
 Definition transf_fundef (fd: fundef) : fundef :=
   transf_fundef transf_function fd.