From e7cafecf3f8c43ed3302f09e000d4f8775356876 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 3 Sep 2020 09:02:52 +0100
Subject: Add fixes to run scheduling on compilation

---
 src/Compiler.v | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'src/Compiler.v')

diff --git a/src/Compiler.v b/src/Compiler.v
index 6efd7a2..7a99bdb 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -51,7 +51,9 @@ From vericert Require
      Verilog
      Veriloggen
      Veriloggenproof
-     HTLgen.
+     HTLgen
+     RTLBlock
+     RTLBlockgen.
 
 From compcert Require Import Smallstep.
 
@@ -99,6 +101,17 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
   @@ print (print_RTL 0)
   @@@ transf_backend.
 
+Definition transf_hls_temp (p : Csyntax.program) : res RTLBlock.program :=
+  OK p
+  @@@ SimplExpr.transl_program
+  @@@ SimplLocals.transf_program
+  @@@ Cshmgen.transl_program
+  @@@ Cminorgen.transl_program
+  @@@ Selection.sel_program
+  @@@ RTLgen.transl_program
+  @@ print (print_RTL 0)
+  @@@ RTLBlockgen.transl_program.
+
 Local Open Scope linking_scope.
 
 Definition CompCert's_passes :=
-- 
cgit