1 files changed, 10 insertions, 12 deletions
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
index 808d342..b8e1e2e 100644
--- a/src/hls/PrintRTLBlockInstr.ml
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -4,13 +4,14 @@ open Datatypes
 open Maps
 open AST
 open RTLBlockInstr
+open Predicate
 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)
+  fprintf pp "p%d" (P.to_int r)
 
 let rec regs pp = function
   | [] -> ()
@@ -22,10 +23,11 @@ let ros pp = function
   | 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
+  | Plit p -> if fst p then pred pp (snd p) else fprintf pp "~%a" pred (snd 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
+  | Ptrue -> fprintf pp "T"
+  | Pfalse -> fprintf pp "⟂"
 
 let print_pred_option pp = function
   | Some x -> fprintf pp "(%a)" print_pred_op x
@@ -48,15 +50,11 @@ let print_bblock_body pp i =
        (name_of_chunk chunk)
        (PrintOp.print_addressing reg) (addr, args)
        reg src
-  | RBsetpred (c, args, p) ->
-    fprintf pp "%a = %a\n"
+  | RBsetpred (p', c, args, p) ->
+    fprintf pp "%a %a = %a\n"
+      print_pred_option p'
       pred p
       (PrintOp.print_condition reg) (c, args)
-  | RBpiped (p, fu, args) ->
-    fprintf pp "%a piped\n" print_pred_option p
-  | RBassign (p, fu, src, dst) ->
-    fprintf pp "%a %a = %a" print_pred_option p
-      reg src reg dst
 
 let rec print_bblock_exit pp i =
   fprintf pp "\t\t";