From 4101773e008b04c88cb5c78565afc6e08a9c4b5f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 27 Sep 2021 20:25:27 +0100
Subject: Revert "Remove more OCaml files to compile successfully without
 admits."

This reverts commit 9a4122dba9bdc33a8e912d5a45bae35e05afb229.
---
 src/hls/PrintRTLBlockInstr.ml | 87 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)
 create mode 100644 src/hls/PrintRTLBlockInstr.ml

(limited to 'src/hls/PrintRTLBlockInstr.ml')

diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
new file mode 100644
index 0000000..ba7241b
--- /dev/null
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -0,0 +1,87 @@
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open RTLBlockInstr
+open PrintAST
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let pred pp r =
+  fprintf pp "p%d" (Nat.to_int r)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+  | Coq_inl r -> reg pp r
+  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let rec print_pred_op pp = function
+  | Pvar p -> pred pp p
+  | Pnot p -> fprintf pp "(~ %a)" print_pred_op p
+  | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2
+  | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2
+
+let print_pred_option pp = function
+  | Some x -> fprintf pp "(%a)" print_pred_op x
+  | None -> ()
+
+let print_bblock_body pp i =
+  fprintf pp "\t\t";
+  match i with
+  | RBnop -> fprintf pp "nop\n"
+  | RBop(p, op, ls, dst) ->
+     fprintf pp "%a %a = %a\n"
+       print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls)
+  | RBload(p, chunk, addr, args, dst) ->
+     fprintf pp "%a %a = %s[%a]\n"
+       print_pred_option p reg dst (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+  | RBstore(p, chunk, addr, args, src) ->
+     fprintf pp "%a %s[%a] = %a\n"
+       print_pred_option p
+       (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+       reg src
+  | RBsetpred (c, args, p) ->
+    fprintf pp "%a = %a\n"
+      pred p
+      (PrintOp.print_condition reg) (c, args)
+
+let rec print_bblock_exit pp i =
+  fprintf pp "\t\t";
+  match i with
+  | RBcall(_, fn, args, res, _) ->
+      fprintf pp "%a = %a(%a)\n"
+        reg res ros fn regs args;
+  | RBtailcall(_, fn, args) ->
+      fprintf pp "tailcall %a(%a)\n"
+        ros fn regs args
+  | RBbuiltin(ef, args, res, _) ->
+      fprintf pp "%a = %s(%a)\n"
+        (print_builtin_res reg) res
+        (name_of_external ef)
+        (print_builtin_args reg) args
+  | RBcond(cond, args, s1, s2) ->
+      fprintf pp "if (%a) goto %d else goto %d\n"
+        (PrintOp.print_condition reg) (cond, args)
+        (P.to_int s1) (P.to_int s2)
+  | RBjumptable(arg, tbl) ->
+      let tbl = Array.of_list tbl in
+      fprintf pp "jumptable (%a)\n" reg arg;
+      for i = 0 to Array.length tbl - 1 do
+        fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+      done
+  | RBreturn None ->
+      fprintf pp "return\n"
+  | RBreturn (Some arg) ->
+      fprintf pp "return %a\n" reg arg
+  | RBgoto n ->
+     fprintf pp "goto %d\n" (P.to_int n)
+  | RBpred_cf (p, c1, c2) ->
+    fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2
-- 
cgit 


From ab1e748f622f4345a3fc13ebbdbc8f223bd10e5c Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 29 Sep 2021 17:11:34 +0100
Subject: Make all OCaml files compile

Reverted commit to get back the scheduling and pretty printing files.
---
 src/hls/PrintRTLBlockInstr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/hls/PrintRTLBlockInstr.ml')

diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
index ba7241b..979ca38 100644
--- a/src/hls/PrintRTLBlockInstr.ml
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -10,7 +10,7 @@ let reg pp r =
   fprintf pp "x%d" (P.to_int r)
 
 let pred pp r =
-  fprintf pp "p%d" (Nat.to_int r)
+  fprintf pp "p%d" (P.to_int r)
 
 let rec regs pp = function
   | [] -> ()
-- 
cgit