From 23c700b5fb35fb00d994cb66e4597fe8ea0b28e1 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 1 Oct 2021 14:16:31 +0100
Subject: Fix compilation of new intermediate languages

---
 src/Compiler.v              | 13 ++++++++-----
 src/VericertClflags.ml      |  1 +
 src/extraction/Extraction.v |  1 +
 src/hls/PrintHTL.ml         |  4 ++--
 4 files changed, 12 insertions(+), 7 deletions(-)

(limited to 'src')

diff --git a/src/Compiler.v b/src/Compiler.v
index 268f451..ecea2fc 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -81,8 +81,9 @@ We then need to declare the external OCaml functions used to print out intermedi
 |*)
 
 Parameter print_RTL: Z -> RTL.program -> unit.
-Parameter print_HTL: HTL.program -> unit.
+Parameter print_HTL: Z -> HTL.program -> unit.
 Parameter print_RTLBlock: Z -> RTLBlock.program -> unit.
+Parameter print_RTLPar: Z -> RTLPar.program -> unit.
 
 Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
   let unused := printer prog in prog.
@@ -191,8 +192,9 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
   @@@ HTLgen.transl_program
-   @@ print print_HTL
+   @@ print (print_HTL 0)
    @@ total_if HLSOpts.optim_ram Memorygen.transf_program
+   @@ print (print_HTL 1)
    @@ Veriloggen.transl_program.
 
 (*|
@@ -239,12 +241,13 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
   @@@ RTLBlockgen.transl_program
-   @@ print (print_RTLBlock 1)
+   @@ print (print_RTLBlock 0)
    @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program
-   @@ print (print_RTLBlock 2)
+   @@ print (print_RTLBlock 1)
   @@@ RTLPargen.transl_program
+   @@ print (print_RTLPar 0)
   @@@ HTLPargen.transl_program
-   @@ print print_HTL
+   @@ print (print_HTL 0)
    @@ Veriloggen.transl_program.
 
 (*|
diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml
index 977ca00..ab3c949 100644
--- a/src/VericertClflags.ml
+++ b/src/VericertClflags.ml
@@ -5,6 +5,7 @@ let option_debug_hls = ref false
 let option_initial = ref false
 let option_dhtl = ref false
 let option_drtlblock = ref false
+let option_drtlpar = ref false
 let option_hls_schedule = ref false
 let option_fif_conv = ref false
 let option_fram = ref true
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 6bbfc05..97f0d2a 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -144,6 +144,7 @@ Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if".
 Extract Constant Compiler.print_RTL => "PrintRTL.print_if".
 Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if".
 Extract Constant Compiler.print_HTL => "PrintHTL.print_if".
+Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if".
 Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
 Extract Constant Compiler.print_Mach => "PrintMach.print_if".
 Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x".
diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml
index a75d0ee..5963be0 100644
--- a/src/hls/PrintHTL.ml
+++ b/src/hls/PrintHTL.ml
@@ -71,10 +71,10 @@ let print_program pp prog =
 
 let destination : string option ref = ref None
 
-let print_if prog =
+let print_if passno prog =
   match !destination with
   | None -> ()
   | Some f ->
-    let oc = open_out f in
+    let oc = open_out (f ^ "." ^ Z.to_string passno) in
     print_program oc prog;
     close_out oc
-- 
cgit