-- | 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"