Fix compilation issues with new types

4 files changed, 37 insertions, 46 deletions

diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 97f0d2a..3544f9d 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -25,7 +25,9 @@ From vericert Require
      RTLBlockInstr
      HTLgen
      Pipeline
-     HLSOpts.
+     HLSOpts
+     Predicate
+.
 
 From Coq Require DecidableClass.
 
@@ -192,7 +194,7 @@ Separate Extraction
          RTLBlockgen.transl_program RTLBlockInstr.successors_instr
          HTLgen.tbl_to_case_expr
          Pipeline.pipeline
-         RTLBlockInstr.sat_pred_simple
+         Predicate.sat_pred_simple
          Verilog.stmnt_to_list
 
    Compiler.transf_c_program Compiler.transf_cminor_program
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
index 979ca38..8e24575 100644
--- a/src/hls/PrintRTLBlockInstr.ml
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -4,6 +4,7 @@ open Datatypes
 open Maps
 open AST
 open RTLBlockInstr
+open Predicate
 open PrintAST
 
 let reg pp r =
@@ -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
+  | 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,8 +50,9 @@ 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)
 
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 13d9480..30a35f3 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -30,10 +30,12 @@ Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.RTLBlock.
 Require Import vericert.hls.RTLPar.
 Require Import vericert.hls.RTLBlockInstr.
+Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
 
 #[local] Open Scope positive.
 #[local] Open Scope forest.
+#[local] Open Scope pred_op.
 
 (*Parameter op_le : Op.operation -> Op.operation -> bool.
 Parameter chunk_le : AST.memory_chunk -> AST.memory_chunk -> bool.
@@ -271,20 +273,11 @@ Definition merge'' x :=
   end.
 
 Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) :=
-  match p1, p2 with
-  | Psingle a, Psingle b => Psingle (a, b)
-  | Psingle a, Plist b => Plist (NE.map (fun x => (fst x, (a, snd x))) b)
-  | Plist b, Psingle a => Plist (NE.map (fun x => (fst x, (snd x, a))) b)
-  | Plist a, Plist b =>
-    Plist (NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end)
-                  (NE.non_empty_prod a b))
-  end.
+  NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end)
+         (NE.non_empty_prod p1 p2).
 
 Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A): predicated B :=
-  match p with
-  | Psingle a => Psingle (f a)
-  | Plist b => Plist (NE.map (fun x => (fst x, f (snd x))) b)
-  end.
+  NE.map (fun x => (fst x, f (snd x))) p.
 
 (*map (fun x => (fst x, Econs (snd x) Enil)) pel*)
 Definition merge' (pel: pred_expr) (tpel: predicated expression_list) :=
@@ -292,7 +285,7 @@ Definition merge' (pel: pred_expr) (tpel: predicated expression_list) :=
 
 Fixpoint merge (pel: list pred_expr): predicated expression_list :=
   match pel with
-  | nil => Psingle Enil
+  | nil => NE.singleton (T, Enil)
   | a :: b => merge' a (merge b)
   end.
 
@@ -305,29 +298,20 @@ Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A): pr
   predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa).
 
 Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A): predicated B :=
-  match pf with
-  | Psingle f => Psingle (f pa)
-  | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa)) pf')
-  end.
+  NE.map (fun x => (fst x, (snd x) pa)) pf.
 
 Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C :=
-  match pf with
-  | Psingle f => Psingle (f pa pb)
-  | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa pb)) pf')
-  end.
+  NE.map (fun x => (fst x, (snd x) pa pb)) pf.
 
 Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D)) (pa: A) (pb: B) (pc: C): predicated D :=
-  match pf with
-  | Psingle f => Psingle (f pa pb pc)
-  | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa pb pc)) pf')
-  end.
+  NE.map (fun x => (fst x, (snd x) pa pb pc)) pf.
 
 (*Compute merge (((Some (Pvar 2), Ebase (Reg 4))::nil)::((Some (Pvar 3), Ebase (Reg 3))::(Some (Pvar 1), Ebase (Reg 3))::nil)::nil).*)
 
 Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) :=
   match p with
-  | None => Psingle a
-  | Some x => Plist (NE.singleton (x, a))
+  | Some p' => NE.singleton (p', a)
+  | None => NE.singleton (T, a)
   end.
 
 Definition update (f : forest) (i : instr) : forest :=
@@ -347,7 +331,7 @@ Definition update (f : forest) (i : instr) : forest :=
      (map_predicated
       (predicated_apply2 (map_predicated (predicated_from_opt p Estore) (f # (Reg r))) chunk addr)
       (merge (list_translation rl f))) (f # Mem))
-  | RBsetpred c addr p => f
+  | RBsetpred p' c addr p => f
   end.
 
 (*|
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 2389369..dd3e39f 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -26,6 +26,7 @@ open AST
 open Kildall
 open Op
 open RTLBlockInstr
+open Predicate
 open RTLBlock
 open HTL
 open Verilog
@@ -105,7 +106,7 @@ let print_instr = function
   | RBnop -> ""
   | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r)
   | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r)
-  | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p)
+  | RBsetpred (_, _, _, p) -> sprintf "setpred(%s)" (print_pred p)
   | RBop (_, op, args, d) ->
     (match op, args with
     | Omove, _ -> "mov"
@@ -354,7 +355,7 @@ let rec find_all_next_dst_read i dst i' curr =
   | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr'
   | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr'
   | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr'
-  | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr'
+  | RBsetpred (_, _, rs, _) :: curr' -> check_dst rs curr'
 
 let drop i lst =
   let rec drop' i' lst' =
@@ -413,10 +414,11 @@ let accumulate_WAW_mem_deps instrs dfg curri =
 
 let rec in_predicate p p' =
   match p' with
-  | Pvar p'' -> P.to_int p = P.to_int p''
-  | Pnot p'' -> in_predicate p p''
+  | Plit p'' -> P.to_int p = P.to_int (snd p'')
   | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2
   | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2
+  | Ptrue -> false
+  | Pfalse -> false
 
 let get_predicate = function
   | RBop (p, _, _, _) -> p
@@ -426,7 +428,7 @@ let get_predicate = function
 
 let rec next_setpred p i = function
   | [] -> None
-  | RBsetpred (_, _, p') :: rst ->
+  | RBsetpred (_, _, _, p') :: rst ->
     if in_predicate p' p then
       Some i
     else
@@ -459,7 +461,7 @@ let accumulate_RAW_pred_deps instrs dfg curri =
 let accumulate_WAR_pred_deps instrs dfg curri =
   let i, curr = curri in
   match curr with
-  | RBsetpred (_, _, p) -> (
+  | RBsetpred (_, _, _, p) -> (
       match next_preduse p 0 (take i instrs |> List.rev) with
       | None -> dfg
       | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
@@ -468,8 +470,8 @@ let accumulate_WAR_pred_deps instrs dfg curri =
 let accumulate_WAW_pred_deps instrs dfg curri =
   let i, curr = curri in
   match curr with
-  | RBsetpred (_, _, p) -> (
-      match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with
+  | RBsetpred (_, _, _, p) -> (
+      match next_setpred (Plit (true, p)) 0 (take i instrs |> List.rev) with
       | None -> dfg
       | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
   | _ -> dfg
@@ -512,18 +514,18 @@ let assigned_vars vars = function
   | RBop (_, _, _, dst) -> dst :: vars
   | RBload (_, _, _, _, dst) -> dst :: vars
   | RBstore (_, _, _, _, _) -> vars
-  | RBsetpred (_, _, _) -> vars
+  | RBsetpred (_, _, _, _) -> vars
 
 let get_pred = function
   | RBnop -> None
   | RBop (op, _, _, _) -> op
   | RBload (op, _, _, _, _) -> op
   | RBstore (op, _, _, _, _) -> op
-  | RBsetpred (_, _, _) -> None
+  | RBsetpred (_, _, _, _) -> None
 
 let independant_pred p p' =
-  match sat_pred_simple (Nat.of_int 100000) (Pand (p, p')) with
-  | Some None -> true
+  match sat_pred_simple (Pand (p, p')) with
+  | None -> true
   | _ -> false
 
 let check_dependent op1 op2 =