content: -----------------------------------------------------------------------------
  -- |
  -- Module    : TestSuite.Uninterpreted.Function
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Testsuite for Documentation.SBV.Examples.Uninterpreted.Function
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell     #-}
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module TestSuite.Uninterpreted.Function(tests) where
  
  import Documentation.SBV.Examples.Uninterpreted.Function
  
  import Utils.SBVTestFramework
  
  data A1
  mkSymbolic [''A1]
  
  data A2
  mkSymbolic [''A2]
  
  data A3
  mkSymbolic [''A3]
  
  data A4
  mkSymbolic [''A4]
  
  data A5
  mkSymbolic [''A5]
  
  data A6
  mkSymbolic [''A6]
  
  data A7
  mkSymbolic [''A7]
  
  data A8
  mkSymbolic [''A8]
  
  data A9
  mkSymbolic [''A9]
  
  data A10
  mkSymbolic [''A10]
  
  data A11
  mkSymbolic [''A11]
  
  data A12
  mkSymbolic [''A12]
  
  
  f1 :: SA1 -> SBool
  f1 = uninterpret "f1"
  
  f2 :: SA1 -> SA2 -> SBool
  f2 = uninterpret "f2"
  
  f3 :: SA1 -> SA2 -> SA3 -> SBool
  f3 = uninterpret "f3"
  
  f4 :: SA1 -> SA2 -> SA3 -> SA4 -> SBool
  f4 = uninterpret "f4"
  
  f5 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SBool
  f5 = uninterpret "f5"
  
  f6 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SBool
  f6 = uninterpret "f6"
  
  f7 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SBool
  f7 = uninterpret "f7"
  
  f8 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SBool
  f8 = uninterpret "f8"
  
  f9 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SBool
  f9 = uninterpret "f9"
  
  f10 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SBool
  f10 = uninterpret "f10"
  
  f11 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SBool
  f11 = uninterpret "f11"
  
  f12 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SA12 -> SBool
  f12 = uninterpret "f12"
  
  thm1 :: SA1 -> SA1 -> SBool
  thm1 x a1 =
    x .== a1
    .=> f1 x .== f1 a1
  
  thm2 :: SA1 -> SA1 -> SA2 -> SBool
  thm2 x a1 a2 =
    x .== a1
    .=> f2 x a2 .== f2 a1 a2
  
  thm3 :: SA1 -> SA1 -> SA2 -> SA3 -> SBool
  thm3 x a1 a2 a3 =
    x .== a1
    .=> f3 x a2 a3 .== f3 a1 a2 a3
  
  thm4 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SBool
  thm4 x a1 a2 a3 a4 =
    x .== a1
    .=> f4 x a2 a3 a4 .== f4 a1 a2 a3 a4
  
  thm5 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SBool
  thm5 x a1 a2 a3 a4 a5 =
    x .== a1
    .=> f5 x a2 a3 a4 a5 .== f5 a1 a2 a3 a4 a5
  
  thm6 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SBool
  thm6 x a1 a2 a3 a4 a5 a6 =
    x .== a1
    .=> f6 x a2 a3 a4 a5 a6 .== f6 a1 a2 a3 a4 a5 a6
  
  thm7 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SBool
  thm7 x a1 a2 a3 a4 a5 a6 a7 =
    x .== a1
    .=> f7 x a2 a3 a4 a5 a6 a7 .== f7 a1 a2 a3 a4 a5 a6 a7
  
  thm8 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SBool
  thm8 x a1 a2 a3 a4 a5 a6 a7 a8 =
    x .== a1
    .=> f8 x a2 a3 a4 a5 a6 a7 a8 .== f8 a1 a2 a3 a4 a5 a6 a7 a8
  
  thm9 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SBool
  thm9 x a1 a2 a3 a4 a5 a6 a7 a8 a9 =
    x .== a1
    .=> f9 x a2 a3 a4 a5 a6 a7 a8 a9 .== f9 a1 a2 a3 a4 a5 a6 a7 a8 a9
  
  thm10 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SBool
  thm10 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 =
    x .== a1
    .=> f10 x a2 a3 a4 a5 a6 a7 a8 a9 a10 .== f10 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10
  
  thm11 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SBool
  thm11 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 =
    x .== a1
    .=> f11 x a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 .== f11 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
  
  thm12 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SA12 -> SBool
  thm12 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 =
    x .== a1
    .=> f12 x a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 .== f12 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12
  
  tests :: TestTree
  tests =
    testGroup "Uninterpreted.Function"
    [ testCase "aufunc-0" (assertIsThm thmGood)
    , testCase "aufunc-1" (assertIsThm thm1)
    , testCase "aufunc-2" (assertIsThm thm2)
    , testCase "aufunc-3" (assertIsThm thm3)
    , testCase "aufunc-4" (assertIsThm thm4)
    , testCase "aufunc-5" (assertIsThm thm5)
    , testCase "aufunc-6" (assertIsThm thm6)
    , testCase "aufunc-7" (assertIsThm thm7)
    , testCase "aufunc-8" (assertIsThm thm8)
    , testCase "aufunc-9" (assertIsThm thm9)
    , testCase "aufunc-10" (assertIsThm thm10)
    , testCase "aufunc-11" (assertIsThm thm11)
    , testCase "aufunc-12" (assertIsThm thm12)
    ]
  