From 24c2f4c5d9224d094083e2b4859b39c2ca0b1071 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 18 Dec 2018 18:06:55 +0000
Subject: Fix rewriter issues

Fixes some re-writer issues that was preventing RISC-V from building
with new flow-typing constraints. Unfortunately because the flow
typing now understands slightly more about boolean variables, the very
large nested case statements with matches predicates produced by the
string-matching end up causing a huge blowup in the overall
compilation time.
---
 lib/flow.sail | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'lib')

diff --git a/lib/flow.sail b/lib/flow.sail
index 1655a719..cb77f5b1 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -20,6 +20,9 @@ val not_bool = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> bool(no
    or_bool that are not shown here. */
 
 val and_bool = {coq: "andb", _: "and_bool"} : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p & 'q)
+
+val and_bool_no_flow = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
+
 val or_bool = {coq: "orb", _: "or_bool"} : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p | 'q)
 
 val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (int('n), int('m)) -> bool('n == 'm)
-- 
cgit v1.2.3