From ef61b884cecc2c8ab11d7db1c1c593005be865e6 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Mon, 14 Jan 2019 21:06:01 +0000
Subject: Add a function to perform re-writes in parallel

rewrite_defs_base_parallel j is the same as rewrite_defs_base
except it performs the re-writes in j parallel processes. Currently
only the trivial_sizeof re-write is parallelised this way with a
default of 4. This works on my machine (TM) but may fail elsewhere.
Because 2019 OCaml concurrency support is lacking, we use Unix.fork
and Marshal.to_channel to send the info from the child processes
performing the re-write back to the parent.

Also fix a missing case in pretty_print_lem
---
 src/rewriter.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/rewriter.mli')

diff --git a/src/rewriter.mli b/src/rewriter.mli
index 53b892d4..ec4e381c 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -70,6 +70,8 @@ val rewrite_defs : tannot defs -> tannot defs
 
 val rewrite_defs_base : tannot rewriters -> tannot defs -> tannot defs
 
+val rewrite_defs_base_parallel : int -> tannot rewriters -> tannot defs -> tannot defs
+  
 (* Same as rewrite_defs base but display a progress bar when verbosity >= 1 *)
 val rewrite_defs_base_progress : string -> tannot rewriters -> tannot defs -> tannot defs
 
-- 
cgit v1.2.3