From 1d7b5f0ddaa6b80babc34180fee5fb4f191283e4 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 20 Aug 2018 15:30:29 +0100
Subject: Add some more test cases for C compilation

Test that basic bi-directional mappings compile correctly

Test that a minimal file importing the prelude compiles correctly
---
 lib/flow.sail | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/flow.sail b/lib/flow.sail
index b4440eaa..c16763ee 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -1,6 +1,10 @@
 $ifndef _FLOW
 $define _FLOW
 
+val eq_unit : (unit, unit) -> bool
+
+function eq_unit(_, _) = true
+
 val not_bool = {coq: "negb", _: "not"} : bool -> bool
 /* NB: There are special cases in Sail for effectful uses of and_bool and
    or_bool that are not shown here. */
@@ -45,7 +49,7 @@ val gteq_int = {coq: "Z.geb", _:"gteq"} : (int, int) -> bool
 val lt_int = {coq: "Z.ltb", _:"lt"} : (int, int) -> bool
 val gt_int = {coq: "Z.gtb", _:"gt"} : (int, int) -> bool
 
-overload operator == = {eq_atom, eq_range, eq_int, eq_bool}
+overload operator == = {eq_atom, eq_range, eq_int, eq_bool, eq_unit}
 overload operator != = {neq_atom, neq_range, neq_int, neq_bool}
 overload operator | = {or_bool}
 overload operator & = {and_bool}
-- 
cgit v1.2.3