Improve some rewrite rules

Author: MaximilianAlgehed

examples/Constrained/Examples/Fold.hs

@@ -35,6 +35,12 @@ evenSpec = explainSpec ["even via (x+x)"] $
       (\eval -> pure (div (eval evenx) 2))
       (\ [var|somey|] -> [assert $ evenx ==. somey + somey])
 
+composeEvenSpec :: Specification Int
+composeEvenSpec = constrained $ \ x -> [satisfies x evenSpec, assert $ x >. 10]
+
+composeOddSpec :: Specification Int
+composeOddSpec = constrained $ \ x -> [satisfies x oddSpec, assert $ x >. 10]
+
 sum3WithLength :: Integer -> Specification ([Int], Int, Int, Int)
 sum3WithLength n =
   constrained $ \ [var|quad|] ->

src/Constrained/NumOrd.hs

@@ -895,6 +895,9 @@ instance Logic IntW where
   propagateMemberSpec MultW (HOLE :<: i) es = memberSpec (mapMaybe (flip invertMult i) (NE.toList es)) (NE.fromList ["propagateSpec"])
   propagateMemberSpec MultW ctx es = propagateMemberSpec MultW (flipCtx ctx) es
 
+  rewriteRules AddW (x :> y :> Nil) _ | x == y = Just $ 2 * x
+  rewriteRules _ _ _ = Nothing
+
 infix 4 +.
 
 -- | `Term`-level `(+)`

test/Constrained/Tests.hs

@@ -20,9 +20,11 @@ import Constrained.Examples.Either
 import Constrained.Examples.Fold (
   Outcome (..),
   evenSpec,
+  composeEvenSpec,
   listSumComplex,
   logishProp,
   oddSpec,
+  composeOddSpec,
   pickProp,
   sum3,
   sum3WithLength,
@@ -203,6 +205,10 @@ tests nightly =
     prop "prop_noNarrowLoop" $ withMaxSuccess 1000 prop_noNarrowLoop
     conformsToSpecESpec
     foldWithSizeTests
+    testSpec "evenSpec" (evenSpec @Int)
+    testSpec "composeEvenSpec" composeEvenSpec
+    testSpec "oddSpec" oddSpec
+    testSpec "composeOddSpec" composeOddSpec
 
 negativeTests :: Spec
 negativeTests =