content: -- | An example showing the usage of the What4 backend in copilot-theorem for
  -- simple arithmetic. This example uses the 'proveWithCounterExamples' function
  -- to demonstrate counterexamples in the event of invalid properties.
  
  module Main where
  
  import qualified Prelude as P
  import Control.Monad (void, forM_)
  import qualified Data.Map as Map
  
  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 <- proveWithCounterExample Z3 spec'
  
    -- Print the results.
    forM_ results $ \(nm, res) -> do
      putStr $ nm <> ": "
      case res of
        ValidCex -> putStrLn "valid"
        InvalidCex cex -> do
          putStrLn "invalid"
          putStrLn $ ppCounterExample cex
        UnknownCex -> putStrLn "unknown"
  
  -- | Pretty-print a counterexample for user display.
  ppCounterExample :: CounterExample -> String
  ppCounterExample cex
      | any P.not (baseCases cex)
      = if Map.null baseCaseVals
          then
            "  All possible extern values during the base case(s) " P.++
            "constitute a counterexample."
          else
            unlines $
              "  The base cases failed with the following extern values:" :
              map
                (\((name, _), val) -> "    " P.++ name P.++ ": " P.++ show val)
                (Map.toList baseCaseVals)
  
      | P.not (inductionStep cex)
      = if Map.null inductionStepVals
          then
            "  All possible extern values during the induction step " P.++
            "constitute a counterexample."
          else
            unlines $
              "  The induction step failed with the following extern values:" :
              map
                (\((name, _), val) -> "    " P.++ name P.++ ": " P.++ show val)
                (Map.toList inductionStepVals)
  
      | otherwise
      = error $
          "ppCounterExample: " P.++
          "Counterexample without failing base cases or induction step"
    where
      allExternVals = concreteExternValues cex
  
      baseCaseVals =
        Map.filterWithKey
          (\(_, offset) _ ->
            case offset of
              AbsoluteOffset {} -> True
              RelativeOffset {} -> False
          )
          allExternVals
  
      inductionStepVals =
        Map.filterWithKey
          (\(_, offset) _ ->
            case offset of
              AbsoluteOffset {} -> False
              RelativeOffset {} -> True
          )
          allExternVals
  