content: module SimplifyTests (tests) where
  
  import Arbitrary (subexprs)
  import Language.Fixpoint.Types.Refinements (Bop (Minus), Constant (I), Expr, ExprV (..))
  import qualified SimplifyInterpreter
  import qualified SimplifyPLE
  import Test.Tasty
    ( TestTree,
      localOption,
      testGroup,
    )
  import Test.Tasty.QuickCheck
    ( Property,
      QuickCheckMaxSize (..),
      QuickCheckTests (..),
      counterexample,
      label,
      testProperty,
    )
  
  tests :: TestTree
  tests =
    withOptions $
      testGroup
        "simplify does not increase expression size"
        [ testProperty "PLE" (prop_no_increase SimplifyPLE.simplify'),
          testProperty "Interpreter" (prop_no_increase SimplifyInterpreter.simplify')
        ]
    where
      withOptions tests' = localOption (QuickCheckMaxSize 4) (localOption (QuickCheckTests 500) tests')
  
  prop_no_increase :: (Expr -> Expr) -> Expr -> Property
  prop_no_increase f e =
    let originalSize = exprSize e
        simplified = f e
        simplifiedSize = exprSize simplified
     in label ("reduced size by " ++ show (originalSize - simplifiedSize)) $
          counterexample
            ( unlines
                [ show simplifiedSize ++ " > " ++ show originalSize,
                  "simplified: " ++ show simplified
                ]
            )
            (simplifiedSize <= originalSize)
  
  exprSize :: Expr -> Int
  -- Undo the removal of ENeg in @simplify@ so it does not count as increasing the size of the expression.
  exprSize (EBin Minus (ECon (I 0)) e) = exprSize (ENeg e)
  exprSize e = 1 + sum (exprSize <$> subexprs e)
  