Fix compilation of new intermediate languages

6 files changed, 21 insertions, 12 deletions

diff --git a/default.nix b/default.nix
index fa60637..0e5b40d 100644
--- a/default.nix
+++ b/default.nix
@@ -9,11 +9,12 @@ stdenv.mkDerivation {
 
   buildInputs = [ ncoq dune_2 gcc
                   ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir
-                  ncoq.ocamlPackages.ocamlgraph
-		  ncoqPackages.serapi
-		  python3 python3Packages.docutils python3Packages.pygments
-		  python3Packages.dominate
-		  python3Packages.pelican
+                  ncoq.ocamlPackages.ocamlgraph ncoq.ocamlPackages.merlin
+
+                  ncoqPackages.serapi
+                  python3 python3Packages.docutils python3Packages.pygments
+                  python3Packages.dominate
+                  python3Packages.pelican
                 ];
 
   enableParallelBuilding = true;
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 0706d79..a36f375 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -66,6 +66,7 @@ let compile_c_file sourcename ifile ofile =
   set_dest Vericert.PrintCminor.destination option_dcminor ".cm";
   set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
   set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock";
+  set_dest Vericert.PrintRTLPar.destination option_drtlpar ".rtlpar";
   set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
   set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
   set_dest Vericert.PrintLTL.destination option_dltl ".ltl";
@@ -391,6 +392,7 @@ let cmdline_actions =
   Exact "-dcminor", Set option_dcminor;
   Exact "-drtl", Set option_drtl;
   Exact "-drtlblock", Set option_drtlblock;
+  Exact "-drtlpar", Set option_drtlpar;
   Exact "-dhtl", Set option_dhtl;
   Exact "-dltl", Set option_dltl;
   Exact "-dalloctrace", Set option_dalloctrace;
@@ -404,6 +406,7 @@ let cmdline_actions =
     option_dcminor := true;
     option_drtl := true;
     option_drtlblock := true;
+    option_drtlpar := true;
     option_dhtl := true;
     option_dltl := true;
     option_dalloctrace := true;
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