aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-29 17:11:34 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-29 17:11:34 +0100
commitab1e748f622f4345a3fc13ebbdbc8f223bd10e5c (patch)
treedb3b7aaf01b76cd55e9d490dcbf40ebec84508f9
parent4101773e008b04c88cb5c78565afc6e08a9c4b5f (diff)
downloadvericert-kvx-ab1e748f622f4345a3fc13ebbdbc8f223bd10e5c.tar.gz
vericert-kvx-ab1e748f622f4345a3fc13ebbdbc8f223bd10e5c.zip
Make all OCaml files compile
Reverted commit to get back the scheduling and pretty printing files.
-rw-r--r--src/hls/PrintRTLBlockInstr.ml2
-rw-r--r--src/hls/Schedule.ml6
2 files changed, 4 insertions, 4 deletions
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
| [] -> ()
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index c6c8bf4..7756181 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -88,7 +88,7 @@ end)(struct
end)
let reg r = sprintf "r%d" (P.to_int r)
-let print_pred r = sprintf "p%d" (Nat.to_int r)
+let print_pred r = sprintf "p%d" (P.to_int r)
let print_instr = function
| RBnop -> ""
@@ -400,7 +400,7 @@ let accumulate_WAW_mem_deps instrs dfg curri =
let rec in_predicate p p' =
match p' with
- | Pvar p'' -> Nat.to_int p = Nat.to_int p''
+ | Pvar p'' -> P.to_int p = P.to_int p''
| Pnot p'' -> in_predicate p p''
| Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2
| Por (p1, p2) -> in_predicate p p1 || in_predicate p p2
@@ -509,7 +509,7 @@ let get_pred = function
| RBsetpred (_, _, _) -> None
let independant_pred p p' =
- match sat_pred_temp (Nat.of_int 100000) (Pand (p, p')) with
+ match sat_pred_simple (Nat.of_int 100000) (Pand (p, p')) with
| Some None -> true
| _ -> false