From ad7b218543bc7f6776086b61d96fd3bd00c414a5 Mon Sep 17 00:00:00 2001
From: Andrew Kent <andrew@galois.com>
Date: Thu, 17 Mar 2022 15:09:52 -0700
Subject: [PATCH] add integration test for newtypes

---
 examples/misc/cryptol_newtype.cry |  6 -----
 examples/misc/cryptol_newtype.saw |  1 -
 intTests/test_newtype/complex.cry | 40 +++++++++++++++++++++++++++++++
 intTests/test_newtype/test.saw    |  8 +++++++
 4 files changed, 48 insertions(+), 7 deletions(-)
 delete mode 100644 examples/misc/cryptol_newtype.cry
 delete mode 100644 examples/misc/cryptol_newtype.saw
 create mode 100644 intTests/test_newtype/complex.cry
 create mode 100644 intTests/test_newtype/test.saw

diff --git a/examples/misc/cryptol_newtype.cry b/examples/misc/cryptol_newtype.cry
deleted file mode 100644
index fc200093a8..0000000000
--- a/examples/misc/cryptol_newtype.cry
+++ /dev/null
@@ -1,6 +0,0 @@
-
-type MyT1 = { value : [2] }
-someT1 = { value = 0b00 }
-
-newtype MyNewT2 = { myT1 : MyT1 }
-someT2 = MyNewT2 { myT1 = someT1 }
diff --git a/examples/misc/cryptol_newtype.saw b/examples/misc/cryptol_newtype.saw
deleted file mode 100644
index b30c68ab83..0000000000
--- a/examples/misc/cryptol_newtype.saw
+++ /dev/null
@@ -1 +0,0 @@
-import "cryptol_newtype.cry";
diff --git a/intTests/test_newtype/complex.cry b/intTests/test_newtype/complex.cry
new file mode 100644
index 0000000000..91695074fc
--- /dev/null
+++ b/intTests/test_newtype/complex.cry
@@ -0,0 +1,40 @@
+// This is a development of rational complex numbers
+
+type Int = Integer
+
+// Complex rational numbers in rectangular coordinates
+newtype CplxInt =
+  { real : Int, imag : Int }
+
+embedQ : Int -> CplxInt
+embedQ x = CplxInt{ real = x, imag = 0 }
+
+cplxAdd : CplxInt -> CplxInt -> CplxInt
+cplxAdd x y = CplxInt { real = r, imag = i }
+  where
+  r = x.real + y.real
+  i = x.imag + y.imag
+
+cplxMul : CplxInt -> CplxInt -> CplxInt
+cplxMul x y = CplxInt { real = r, imag = i }
+  where
+  r = x.real * y.real - x.imag * y.imag
+  i = x.real * y.imag + x.imag * y.real
+
+cplxEq : CplxInt -> CplxInt -> Bit
+cplxEq x y = (x.real == y.real) && (x.imag == y.imag)
+
+cplxAddAssoc : CplxInt -> CplxInt -> CplxInt -> Bit
+cplxAddAssoc x y z =
+  cplxEq (cplxAdd (cplxAdd x y) z)
+         (cplxAdd x (cplxAdd y z))
+
+cplxMulAssoc : CplxInt -> CplxInt -> CplxInt -> Bit
+cplxMulAssoc x y z =
+  cplxEq (cplxMul (cplxMul x y) z)
+         (cplxMul x (cplxMul y z))
+
+cplxMulDistrib : CplxInt -> CplxInt -> CplxInt -> Bit
+cplxMulDistrib x y z =
+  cplxEq (cplxMul x (cplxAdd y z))
+         (cplxAdd (cplxMul x y) (cplxMul x z))
\ No newline at end of file
diff --git a/intTests/test_newtype/test.saw b/intTests/test_newtype/test.saw
new file mode 100644
index 0000000000..f4725b47bc
--- /dev/null
+++ b/intTests/test_newtype/test.saw
@@ -0,0 +1,8 @@
+import "complex.cry";
+
+prove_print cvc4 {{ \ x y z -> cplxAddAssoc x y z}};
+
+prove_print cvc4 {{ \ x y z -> cplxMulAssoc x y z}};
+
+prove_print cvc4 {{ \ x y z -> cplxMulDistrib x y z}};
+