From ff199bf43e4c2a9c662f81383bc096c93b591b6a Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 16 Jun 2020 18:04:35 -0700
Subject: [PATCH] Add regression tests for superclass inference and solving

---
 tests/regression/superclass.cry         | 29 +++++++++++++++++++++++++
 tests/regression/superclass.icry        |  8 +++++++
 tests/regression/superclass.icry.stdout | 10 +++++++++
 3 files changed, 47 insertions(+)
 create mode 100644 tests/regression/superclass.cry
 create mode 100644 tests/regression/superclass.icry
 create mode 100644 tests/regression/superclass.icry.stdout

diff --git a/tests/regression/superclass.cry b/tests/regression/superclass.cry
new file mode 100644
index 00000000..50f73e9b
--- /dev/null
+++ b/tests/regression/superclass.cry
@@ -0,0 +1,29 @@
+//zeroRing : {a} (Ring a) => a
+zeroRing = zero
+
+zeroLogic : {a} (Logic a) => a
+zeroLogic = zero
+
+zeroIntegral : {a} (Integral a) => a
+zeroIntegral = zero
+
+zeroField : {a} (Field a) => a
+zeroField = zero
+
+zeroRound : {a} (Round a) => a
+zeroRound = zero
+
+fromIntIntegral : {a} (Integral a) => a
+fromIntIntegral = fromInteger 42
+
+fromIntField : {a} (Field a) => a
+fromIntField = fromInteger 42
+
+fromIntRound : {a} (Round a) => a
+fromIntRound = fromInteger 42
+
+recipRound : {a} (Round a) => a -> Integer
+recipRound x = trunc (recip x)
+
+compareRound : {a} (Round a) => a -> a -> Bit
+compareRound x y = x < y
diff --git a/tests/regression/superclass.icry b/tests/regression/superclass.icry
new file mode 100644
index 00000000..7379acbb
--- /dev/null
+++ b/tests/regression/superclass.icry
@@ -0,0 +1,8 @@
+:l superclass.cry
+
+:t (fromInteger 42 + zero)
+:t (trunc (recip (fromInteger 5)))
+:t (\x -> x < fromInteger (floor (recip x)))
+:t (\x -> x == zero /. x)
+:t (zero == ~zero)
+:t (\x -> toInteger (x + zero))
\ No newline at end of file
diff --git a/tests/regression/superclass.icry.stdout b/tests/regression/superclass.icry.stdout
new file mode 100644
index 00000000..dc9c04ec
--- /dev/null
+++ b/tests/regression/superclass.icry.stdout
@@ -0,0 +1,10 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+(fromInteger 42 + zero) : {a} (Ring a) => a
+(trunc (recip (fromInteger 5))) : {a} (Round a) => Integer
+(\x -> x < fromInteger (floor (recip x))) : {a} (Round a) =>
+                                              a -> Bit
+(\x -> x == zero /. x) : {a} (Cmp a, Field a) => a -> Bit
+(zero == ~zero) : {a} (Cmp a, Logic a) => Bit
+(\x -> toInteger (x + zero)) : {a} (Integral a) => a -> Integer