Fix if-conversion and translation with Plit

2 files changed, 5 insertions, 5 deletions

diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index e8b18dc..6058f62 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -658,7 +658,7 @@ Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
 
 Fixpoint pred_expr (preg: reg) (p: pred_op) :=
   match p with
-  | Pvar (b, pred) =>
+  | Plit (b, pred) =>
     if b
     then Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred))
     else Vunop Vnot (Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)))
@@ -696,7 +696,7 @@ Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr)
     translate_predicate a preg p dst (Vvar src)
   | RBsetpred c args p =>
     do cond <- translate_condition c args;
-    ret (a (pred_expr preg (Pvar (true, p))) cond)
+    ret (a (pred_expr preg (Plit (true, p))) cond)
   end.
 
 Lemma create_new_state_state_incr:
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 205506c..67bd2a8 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -58,10 +58,10 @@ Definition if_convert_block (c: code) (p: predicate) (bb: bblock) : bblock :=
   | RBcond cond args n1 n2 =>
     match PTree.get n1 c, PTree.get n2 c with
     | Some bb1, Some bb2 =>
-      let bb1' := List.map (map_if_convert (Pvar (true, p))) bb1.(bb_body) in
-      let bb2' := List.map (map_if_convert (Pvar (false, p))) bb2.(bb_body) in
+      let bb1' := List.map (map_if_convert (Plit (true, p))) bb1.(bb_body) in
+      let bb2' := List.map (map_if_convert (Plit (false, p))) bb2.(bb_body) in
       mk_bblock (List.concat (bb.(bb_body) :: ((RBsetpred cond args p) :: bb1') :: bb2' :: nil))
-                (RBpred_cf (Pvar (true, p)) bb1.(bb_exit) bb2.(bb_exit))
+                (RBpred_cf (Plit (true, p)) bb1.(bb_exit) bb2.(bb_exit))
     | _, _ => bb
     end
   | _ => bb