signum_ is doable, abs_ isn't super neat

Author: MaximilianAlgehed

src/Constrained/NumOrd.hs

@@ -684,12 +684,19 @@ class (Num a, HasSpec a, HasDivision a, OrdLike a) => NumLike a where
     Maybe a
   safeSubtract a b = fromSimpleRep <$> safeSubtract @(SimpleRep a) (toSimpleRep a) (toSimpleRep b)
 
--- | Operations on numbers
+-- | Operations on numbers.
+-- The reason there is no implementation of abs here is that you can't easily deal with abs
+-- without specifications becoming very large. Consider the following example:
+-- > constrained $ \ x -> [1000 <. abs_ x, abs_ x <. 1050]
+-- The natural `Specification` here would be something like `(-1050, -1000) || (1000, 1050)`
+-- - the disjoint union of two open, non-overlapping, intervals. However, this doesn't work
+-- because number type-specs only support a single interval. You could fudge it in all sorts of ways
+-- by using `chooseSpec` or by using the can't set (which would blow up to be 2000 elements large in this
+-- case). In short, there is no _satisfactory_ solution here.
 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
-  AbsW :: NumLike a => IntW '[a] a
   SignumW :: NumLike a => IntW '[a] a
 
 deriving instance Eq (IntW dom rng)
@@ -698,21 +705,18 @@ instance Show (IntW d r) where
   show AddW = "+"
   show NegateW = "negate_"
   show MultW = "*"
-  show AbsW = "abs_"
   show SignumW = "signum_"
 
 instance Semantics IntW where
   semantics AddW = (+)
   semantics NegateW = negate
   semantics MultW = (*)
-  semantics AbsW = abs
   semantics SignumW = signum
 
 instance Syntax IntW where
   isInfix AddW = True
   isInfix NegateW = False
   isInfix MultW = True
-  isInfix AbsW = False
   isInfix SignumW = False
 
 class HasDivision a where
@@ -868,8 +872,8 @@ instance NumLike a => Num (Term a) where
   negate = negate_
   fromInteger = Lit . fromInteger
   (*) = (*.)
-  abs = abs_
   signum = signum_
+  abs = error "No implementation for abs @(Term a)"
 
 invertMult :: (HasSpec a, Num a, HasDivision a) => a -> a -> Maybe a
 invertMult a b =
@@ -887,7 +891,6 @@ instance Logic IntW where
     | 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
-  propagateTypeSpec AbsW (Unary HOLE) ts cant = error "TODO"
   propagateTypeSpec SignumW (Unary HOLE) ts cant =
     constrained $ \ x ->
       [ x `satisfies` notMemberSpec [0] | not $ ok 0 ] ++
@@ -911,9 +914,6 @@ instance Logic IntW where
     | 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
-  propagateMemberSpec AbsW (Unary HOLE) es
-    | all ((== -1) . signum) es = ErrorSpec $ NE.fromList [ "abs for all negative member spec", show es ]
-    | otherwise = MemberSpec $ NE.nub . NE.fromList $ concat $ [ [e, negate e] | e <- NE.toList es, signum e /= -1 ]
   propagateMemberSpec SignumW (Unary HOLE) es
     | all ((`notElem` [-1, 0, 1]) . signum) es = ErrorSpec $ NE.fromList [ "signum for invalid member spec", show es ]
     | otherwise = constrained $ \ x ->
@@ -940,10 +940,6 @@ infixl 7 *.
 negate_ :: NumLike a => Term a -> Term a
 negate_ = appTerm NegateW
 
--- | `Term`-level `abs`
-abs_ :: NumLike a => Term a -> Term a
-abs_ = appTerm AbsW
-
 -- | `Term`-level `signum`
 signum_ :: NumLike a => Term a -> Term a
 signum_ = appTerm SignumW