content: -- | An example showing the usage of the What4 backend in copilot-theorem for
  -- simple arithmetic.
  
  module Main where
  
  import qualified Prelude as P
  import Control.Monad (void, forM_)
  
  import Language.Copilot
  import Copilot.Theorem.What4
  
  spec :: Spec
  spec = do
    -- Define some external streams. Their values are not important, so external
    -- streams suffice.
    let eint8  :: Stream Int8
        eint8  = extern "eint8" Nothing
        eword8 :: Stream Word8
        eword8 = extern "eword8" Nothing
        efloat :: Stream Float
        efloat = extern "efloat" Nothing
  
    -- The simplest example involving numbers: equality on constant values.
    void $ prop "Example 1" (forAll ((constant (1 :: Int8)) == (constant 1)))
  
    -- Testing "a < a + 1". This should fail, because it isn't true.
    void $ prop "Example 2" (forAll (eint8 < (eint8 + 1)))
  
    -- Adding another condition to the above property to make it true.
    void $ prop "Example 3" (forAll ((eint8 < (eint8 + 1)) || (eint8 == 127)))
  
    -- Just like the previous example, but with words.
    void $ prop "Example 4" (forAll ((eword8 < (eword8 + 1)) || (eword8 == 255)))
  
    -- An example with floats.
    void $ prop "Example 5" (forAll ((2 * efloat) == (efloat + efloat)))
  
    -- Another example with floats. This fails, because it isn't true.
    void $ prop "Example 6" (forAll ((efloat + 1) /= efloat))
  
  main :: IO ()
  main = do
    spec' <- reify spec
  
    -- Use Z3 to prove the properties.
    results <- prove Z3 spec'
  
    -- Print the results.
    forM_ results $ \(nm, res) -> do
      putStr $ nm <> ": "
      case res of
        Valid   -> putStrLn "valid"
        Invalid -> putStrLn "invalid"
        Unknown -> putStrLn "unknown"
  