WIP: Complete Num instance

Author: MaximilianAlgehed

src/Constrained/NumOrd.hs

@@ -656,7 +656,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, HasDivision a) => NumLike a where
+class (Num a, HasSpec a, HasDivision a, OrdLike a) => NumLike a where
   subtractSpec :: a -> TypeSpec a -> Specification a
   default subtractSpec ::
     ( NumLike (SimpleRep a)
@@ -689,23 +689,31 @@ 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)
 
 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
   doDivide :: a -> a -> a
@@ -860,8 +868,8 @@ instance NumLike a => Num (Term a) where
   negate = negate_
   fromInteger = Lit . fromInteger
   (*) = (*.)
-  abs = error "abs not implemented for Term Fn Int"
-  signum = error "signum not implemented for Term Fn Int"
+  abs = abs_
+  signum = signum_
 
 invertMult :: (HasSpec a, Num a, HasDivision a) => a -> a -> Maybe a
 invertMult a b =
@@ -879,6 +887,13 @@ 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 ] ++
+      [ Assert $ 0 <=. x                | not $ ok (-1) ] ++
+      [ Assert $ x <=. x                | not $ ok 1 ]
+    where ok = flip conformsToSpec (TypeSpec ts cant)
 
   propagateMemberSpec AddW (HOLE :<: i) es =
     memberSpec
@@ -896,6 +911,15 @@ 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 ->
+                    [ x `satisfies` notMemberSpec [0] | 0  `notElem` es ] ++
+                    [ Assert $ 0 <=. x                | -1 `notElem` es ] ++
+                    [ Assert $ x <=. x                | 1  `notElem` es ]
 
   rewriteRules AddW (x :> y :> Nil) _ | x == y = Just $ 2 * x
   rewriteRules _ _ _ = Nothing
@@ -916,6 +940,14 @@ 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
+
 infix 4 -.
 
 -- | `Term`-level `(-)`