Theory Native_Word_Test_GHC

(*  Title:      Native_Word_Test_GHC.thy
    Author:     Andreas Lochbihler, ETH Zurich
*)

theory Native_Word_Test_GHC imports
  Native_Word_Test
begin

section ‹Test with GHC›

declare [[code_test_ghc = "-XTypeSynonymInstances"]]

test_code
  test_uint64 "test_uint64' = 0x12"
  test_uint32 "test_uint32' = 0x12"
  test_uint16
  test_uint8 "test_uint8' = 0x12"
  test_uint
  test_casts test_casts' test_casts''
  test_casts_uint test_casts_uint' test_casts_uint''
in GHC

subsection ‹Test quickcheck narrowing›

context
  includes bit_operations_syntax
begin

lemma "(x :: uint64) AND y = x OR y"
quickcheck[narrowing, expect=counterexample]
oops

lemma "(f :: uint64 ⇒ bool) = g"
quickcheck[narrowing, size=3, expect=counterexample]
oops

lemma "(x :: uint32) AND y = x OR y"
quickcheck[narrowing, expect=counterexample]
oops

lemma "(f :: uint32 ⇒ bool) = g"
quickcheck[narrowing, size=3, expect=counterexample]
oops

lemma "(x :: uint16) AND y = x OR y"
quickcheck[narrowing, expect=counterexample]
oops

lemma "(f :: uint16 ⇒ bool) = g"
quickcheck[narrowing, size=3, expect=counterexample]
oops

lemma "(x :: uint8) AND y = x OR y"
quickcheck[narrowing, expect=counterexample]
oops

lemma "(f :: uint8 ⇒ bool) = g"
quickcheck[narrowing, size=3, expect=counterexample]
oops

lemma "(x :: uint) AND y = x OR y"
quickcheck[narrowing, expect=counterexample]
oops

lemma "(f :: uint ⇒ bool) = g"
quickcheck[narrowing, size=3, expect=counterexample]
oops

end

end