diff options
| author | Alasdair Armstrong | 2018-12-18 18:06:55 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-18 18:06:55 +0000 |
| commit | 24c2f4c5d9224d094083e2b4859b39c2ca0b1071 (patch) | |
| tree | afba2ea5caca3d95bb789f668b6c51d3720f4b15 /lib | |
| parent | 3da039c72efa210b7b162c4571925504f275a978 (diff) | |
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.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flow.sail | 3 |
1 files changed, 3 insertions, 0 deletions
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) |