Add multiplication to the way we deal with numbers

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

@@ -28,6 +28,7 @@ module Constrained.NumOrd (
   (>=.),
   (<=.),
   (+.),
+  (*.),
   negate_,
   cardinality,
   caseBoolSpec,
@@ -202,6 +203,8 @@ deriving via Unbounded (Ratio Integer) instance MaybeBounded (Ratio Integer)
 
 deriving via Unbounded Float instance MaybeBounded Float
 
+deriving via Unbounded Double instance MaybeBounded Double
+
 instance MaybeBounded Natural where
   lowerBound = Just 0
   upperBound = Nothing
@@ -651,7 +654,7 @@ cardinalNumSpec (NumSpecInterval Nothing Nothing) = cardinalTrueSpec @n
 -- Now the operations on Numbers
 
 -- | Everything we need to make the number operations make sense on a given type
-class (Num a, HasSpec a) => NumLike a where
+class (Num a, HasSpec a, HasDivision a) => NumLike a where
   subtractSpec :: a -> TypeSpec a -> Specification a
   default subtractSpec ::
     ( NumLike (SimpleRep a)
@@ -682,24 +685,132 @@ class (Num a, HasSpec a) => NumLike a where
 -- | Operations on numbers
 data IntW (as :: [Type]) b where
   AddW :: NumLike a => IntW '[a, a] a
+  MultW :: NumLike a => IntW '[a, a] a
   NegateW :: NumLike a => IntW '[a] a
 
 deriving instance Eq (IntW dom rng)
 
 instance Show (IntW d r) where
   show AddW = "+"
   show NegateW = "negate_"
+  show MultW = "*"
 
 instance Semantics IntW where
   semantics AddW = (+)
   semantics NegateW = negate
+  semantics MultW = (*)
 
 instance Syntax IntW where
   isInfix AddW = True
   isInfix NegateW = False
+  isInfix MultW = True
+
+class HasDivision a where
+  doDivide :: a -> a -> a
+  default doDivide ::
+    ( HasDivision (SimpleRep a)
+    , GenericRequires a
+    ) =>
+    a ->
+    a ->
+    a
+  doDivide a b = fromSimpleRep $ doDivide (toSimpleRep a) (toSimpleRep b)
+
+  divideSpec :: a -> TypeSpec a -> Specification a
+  default divideSpec ::
+    ( HasDivision (SimpleRep a)
+    , GenericRequires a
+    ) =>
+    a ->
+    TypeSpec a ->
+    Specification a
+  divideSpec a ts = fromSimpleRepSpec $ divideSpec (toSimpleRep a) ts
+
+instance {-# OVERLAPPABLE #-} (HasSpec a, MaybeBounded a, Integral a, TypeSpec a ~ NumSpec a) => HasDivision a where
+  doDivide = div
+
+  divideSpec 0 _ = TrueSpec
+  divideSpec a (NumSpecInterval (unionWithMaybe max lowerBound -> ml) (unionWithMaybe min upperBound -> mu)) = typeSpec ts
+    where
+      ts | a > 0 = NumSpecInterval ml' mu'
+         | otherwise = NumSpecInterval mu' ml'
+      ml' = adjustLowerBound <$> ml
+      mu' = adjustUpperBound <$> mu
+
+      -- NOTE: negate has different overflow semantics than div, so that's why we use negate below...
+
+      adjustLowerBound l
+        | a == 1 = l
+        | a == -1 = negate l
+        | otherwise =
+          let r = l `div` a in
+          if toInteger r * toInteger a < toInteger l
+          then r + signum a
+          else r
+
+      adjustUpperBound u
+        | a == 1  = u
+        | a == -1 = negate u
+        | otherwise =
+          let r = u `div` a in
+          if toInteger r * toInteger a > toInteger u
+          then r - signum a
+          else r
+
+instance HasDivision Float where
+  doDivide = (/)
+
+  divideSpec 0 _ = TrueSpec
+  divideSpec a (NumSpecInterval ml mu) = typeSpec ts
+    where
+      ts | a > 0 = NumSpecInterval ml' mu'
+         | otherwise = NumSpecInterval mu' ml'
+      ml' = adjustLowerBound <$> ml
+      mu' = adjustUpperBound <$> mu
+      adjustLowerBound l =
+        let r = l / a
+            l' = r * a
+        in
+        if l' < l
+        then r + (l - l') * 2 / a
+        else r
+
+      adjustUpperBound u =
+        let r = u / a
+            u' = r * a
+        in
+        if u < u'
+        then r - (u' - u) * 2 / a
+        else r
+
+instance HasDivision Double where
+  doDivide = (/)
+
+  divideSpec 0 _ = TrueSpec
+  divideSpec a (NumSpecInterval ml mu) = typeSpec ts
+    where
+      ts | a > 0 = NumSpecInterval ml' mu'
+         | otherwise = NumSpecInterval mu' ml'
+      ml' = adjustLowerBound <$> ml
+      mu' = adjustUpperBound <$> mu
+      adjustLowerBound l =
+        let r = l / a
+            l' = r * a
+        in
+        if l' < l
+        then r + (l - l') * 2 / a
+        else r
+
+      adjustUpperBound u =
+        let r = u / a
+            u' = r * a
+        in
+        if u < u'
+        then r - (u' - u) * 2 / a
+        else r
 
 -- | A type that we can reason numerically about in constraints
-type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a)
+type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a, HasDivision a)
 
 instance {-# OVERLAPPABLE #-} Numeric a => NumLike a where
   subtractSpec a ts@(NumSpecInterval ml mu)
@@ -728,6 +839,7 @@ instance {-# OVERLAPPABLE #-} Numeric a => NumLike a where
         | Just r <- safeSubtract a1 x = r
         | a1 < 0 = fromJust upperBound
         | otherwise = fromJust lowerBound
+
   negateSpec (NumSpecInterval ml mu) = typeSpec $ NumSpecInterval (negate <$> mu) (negate <$> ml)
 
   safeSubtract a x
@@ -742,20 +854,29 @@ instance {-# OVERLAPPABLE #-} Numeric a => NumLike a where
     | otherwise = Just $ x - a
 
 instance NumLike a => Num (Term a) where
-  (+) = addFn
-  negate = negateFn
+  (+) = (+.)
+  negate = negate_
   fromInteger = Lit . fromInteger
-  (*) = error "(*) not implemented for Term Fn Int"
+  (*) = (*.)
   abs = error "abs not implemented for Term Fn Int"
   signum = error "signum not implemented for Term Fn Int"
 
+invertMult :: (HasSpec a, Num a, HasDivision a) => a -> a -> Maybe a
+invertMult a b =
+  let r = a `doDivide` b in if r * b == a then Just r else Nothing
+
 -- | Just a note that these instances won't work until we are in a context where
 --   there is a HasSpec instance of 'a', which (NumLike a) demands.
 --   This happens in Constrained.Experiment.TheKnot
 instance Logic IntW where
   propagateTypeSpec AddW (HOLE :<: i) ts cant = subtractSpec i ts <> notMemberSpec (mapMaybe (safeSubtract i) cant)
   propagateTypeSpec AddW ctx ts cant = propagateTypeSpec AddW (flipCtx ctx) ts cant
   propagateTypeSpec NegateW (Unary HOLE) ts cant = negateSpec ts <> notMemberSpec (map negate cant)
+  propagateTypeSpec MultW (HOLE :<: 0) ts cant
+    | 0 `conformsToSpec` TypeSpec ts cant = TrueSpec
+    | otherwise = ErrorSpec $ NE.fromList [ "zero" ]
+  propagateTypeSpec MultW (HOLE :<: i) ts cant = divideSpec i ts <> notMemberSpec (mapMaybe (flip invertMult i) cant)
+  propagateTypeSpec MultW ctx ts cant = propagateTypeSpec MultW (flipCtx ctx) ts cant
 
   propagateMemberSpec AddW (HOLE :<: i) es =
     memberSpec
@@ -768,28 +889,36 @@ instance Logic IntW where
       )
   propagateMemberSpec AddW ctx es = propagateMemberSpec AddW (flipCtx ctx) es
   propagateMemberSpec NegateW (Unary HOLE) es = MemberSpec $ NE.nub $ fmap negate es
+  propagateMemberSpec MultW (HOLE :<: 0) es
+    | 0 `elem` es = TrueSpec
+    | otherwise = ErrorSpec $ NE.fromList [ "zero" ]
+  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
 
-addFn :: forall a. NumLike a => Term a -> Term a -> Term a
-addFn = appTerm AddW
-
-negateFn :: forall a. NumLike a => Term a -> Term a
-negateFn = appTerm NegateW
+  rewriteRules AddW (x :> y :> Nil) _ | x == y = Just $ 2 * x
+  rewriteRules _ _ _ = Nothing
 
 infix 4 +.
 
 -- | `Term`-level `(+)`
 (+.) :: NumLike a => Term a -> Term a -> Term a
-(+.) = addFn
+(+.) = appTerm AddW
+
+infixl 7 *.
+
+-- | `Term`-level `(+)`
+(*.) :: NumLike a => Term a -> Term a -> Term a
+(*.) = appTerm MultW
 
 -- | `Term`-level `negate`
 negate_ :: NumLike a => Term a -> Term a
-negate_ = negateFn
+negate_ = appTerm NegateW
 
 infix 4 -.
 
 -- | `Term`-level `(-)`
 (-.) :: Numeric n => Term n -> Term n -> Term n
-(-.) x y = addFn x (negateFn y)
+(-.) x y = x +. negate_ y
 
 infixr 4 <=.
 
@@ -1029,3 +1158,14 @@ instance HasSpec Float where
   toPreds = toPredsNumSpec
   cardinalTypeSpec _ = TrueSpec
   guardTypeSpec = guardNumSpec
+
+instance HasSpec Double where
+  type TypeSpec Double = NumSpec Double
+  emptySpec = emptyNumSpec
+  combineSpec = combineNumSpec
+  genFromTypeSpec = genFromNumSpec
+  shrinkWithTypeSpec = shrinkWithNumSpec
+  conformsTo = conformsToNumSpec
+  toPreds = toPredsNumSpec
+  cardinalTypeSpec _ = TrueSpec
+  guardTypeSpec = guardNumSpec

src/Constrained/SumList.hs

@@ -166,10 +166,8 @@ genNumList ::
   ( MonadGenError m
   , Arbitrary a
   , Integral a
-  , MaybeBounded a
-  , TypeSpec a ~ NumSpec a
-  , -- , Foldy a
-    Random a
+  , Numeric a
+  , Random a
   , Complete a
   ) =>
   Specification a ->
@@ -470,12 +468,11 @@ narrowByFuelAndSize fuel size specpair =
 genListWithSize ::
   forall a m.
   ( Complete a
-  , TypeSpec a ~ NumSpec a
   , MonadGenError m
   , Random a
   , Integral a
   , Arbitrary a
-  , MaybeBounded a
+  , Numeric a
   , Complete Integer
   ) =>
   Specification Integer ->

src/Constrained/Test.hs

@@ -24,6 +24,7 @@ module Constrained.Test (
   prop_propagateSpecSound,
   prop_gen_sound,
   specType,
+  TestableFn(..),
 ) where
 
 import Constrained.API.Extend
@@ -47,6 +48,8 @@ import Data.Typeable (Typeable, typeOf)
 import Prettyprinter
 import Test.QuickCheck hiding (Fun)
 import qualified Test.QuickCheck as QC
+import Data.Word
+import Data.Int
 
 -- | Check that a generator from a given `Specification` is sound, it never
 -- generates a bad value that doesn't satisfy the constraint
@@ -324,6 +327,10 @@ instance (HasSpec a, Arbitrary (TypeSpec a)) => Arbitrary (Specification a) wher
       , (10, pure baseSpec)
       ]
 
+  shrink (TypeSpec ts cant) = flip TypeSpec cant <$> shrink ts
+  shrink (ExplainSpec _ s) = [s]
+  shrink _ = []
+
 instance
   ( Arbitrary a
   , Arbitrary (FoldSpec a)
@@ -389,6 +396,13 @@ instance QC.Arbitrary TestableFn where
       [ -- data IntW
         TestableFn $ AddW @Int
       , TestableFn $ NegateW @Int
+      , TestableFn $ MultW @Int
+      , TestableFn $ MultW @Integer
+      -- These are representative of the bounded types
+      , TestableFn $ MultW @Word8
+      , TestableFn $ MultW @Int8
+      , TestableFn $ MultW @Float
+      , TestableFn $ MultW @Double
       , TestableFn $ SizeOfW @(Map Int Int)
       , -- data BaseW
         TestableFn $ EqualW @Int

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 =