add integration test for newtypes

GaloisInc · Mar 17, 2022 · ad7b218 · ad7b218
1 parent b488b4c
commit ad7b218
Show file tree

Hide file tree

Showing 4 changed files with 48 additions and 7 deletions.
diff --git a/examples/misc/cryptol_newtype.cry b/examples/misc/cryptol_newtype.cry
diff --git a/examples/misc/cryptol_newtype.saw b/examples/misc/cryptol_newtype.saw
diff --git a/intTests/test_newtype/complex.cry 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))
diff --git a/intTests/test_newtype/test.saw 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}};
+