• Home
  • Features
  • Pricing
  • Docs
  • Announcements
  • Sign In

input-output-hk / constrained-generators / 500

08 Jan 2026 10:49AM UTC coverage: 77.318% (+0.1%) from 77.177%
500

push

github

web-flow
Test and fix for bad behaviour of chooseSpec (#68)

32 of 34 new or added lines in 4 files covered. (94.12%)

2 existing lines in 2 files now uncovered.

4019 of 5198 relevant lines covered (77.32%)

1.46 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

73.94
/src/Constrained/NumOrd.hs
1
{-# LANGUAGE AllowAmbiguousTypes #-}
2
{-# LANGUAGE CPP #-}
3
{-# LANGUAGE ConstraintKinds #-}
4
{-# LANGUAGE DataKinds #-}
5
{-# LANGUAGE DefaultSignatures #-}
6
{-# LANGUAGE DerivingVia #-}
7
{-# LANGUAGE FlexibleContexts #-}
8
{-# LANGUAGE FlexibleInstances #-}
9
{-# LANGUAGE GADTs #-}
10
{-# LANGUAGE LambdaCase #-}
11
{-# LANGUAGE PatternSynonyms #-}
12
{-# LANGUAGE ScopedTypeVariables #-}
13
{-# LANGUAGE StandaloneDeriving #-}
14
{-# LANGUAGE TypeApplications #-}
15
{-# LANGUAGE TypeFamilies #-}
16
{-# LANGUAGE TypeOperators #-}
17
{-# LANGUAGE UndecidableInstances #-}
18
{-# LANGUAGE UndecidableSuperClasses #-}
19
{-# LANGUAGE ViewPatterns #-}
20
-- Random Natural, Arbitrary Natural, Uniform Natural
21
{-# OPTIONS_GHC -Wno-orphans #-}
22

23
-- | Everything we need to deal with numbers and comparisons between them
24
module Constrained.NumOrd (
25
  NumSpec (..),
26
  (>.),
27
  (<.),
28
  (-.),
29
  (>=.),
30
  (<=.),
31
  (+.),
32
  (*.),
33
  negate_,
34
  cardinality,
35
  caseBoolSpec,
36
  addSpecInt,
37
  emptyNumSpec,
38
  cardinalNumSpec,
39
  combineNumSpec,
40
  genFromNumSpec,
41
  shrinkWithNumSpec,
42
  fixupWithNumSpec,
43
  fixupWithTypeSpec,
44
  conformsToNumSpec,
45
  toPredsNumSpec,
46
  OrdLike (..),
47
  MaybeBounded (..),
48
  NumLike (..),
49
  HasDivision (..),
50
  Numeric,
51
  Number,
52
  nubOrd,
53
  IntW (..),
54
  OrdW (..),
55
) where
56

57
import Constrained.AbstractSyntax
58
import Constrained.Base
59
import Constrained.Conformance
60
import Constrained.Core (Value (..), unionWithMaybe)
61
import Constrained.FunctionSymbol
62
import Constrained.GenT
63
import Constrained.Generic
64
import Constrained.List
65
import Constrained.PrettyUtils
66
import Control.Applicative ((<|>))
67
import Control.Arrow (first)
68
import Data.Containers.ListUtils
69
import Data.Foldable
70
import Data.Kind
71
import Data.List (nub)
72
import Data.List.NonEmpty (NonEmpty ((:|)))
73
import qualified Data.List.NonEmpty as NE
74
import Data.Maybe
75
import Data.Typeable (typeOf)
76
import Data.Word
77
import GHC.Int
78
import GHC.Natural
79
import GHC.Real
80
import System.Random.Stateful (Random (..), Uniform (..))
81
import Test.QuickCheck (Arbitrary (arbitrary, shrink), choose, frequency)
82

83
-- | Witnesses for comparison operations (<=. and <. and <=. and >=.) on numbers
84
-- The other operations are defined in terms of these.
85
data OrdW (dom :: [Type]) (rng :: Type) where
86
  LessOrEqualW :: OrdLike a => OrdW '[a, a] Bool
87
  LessW :: OrdLike a => OrdW '[a, a] Bool
88
  GreaterOrEqualW :: OrdLike a => OrdW '[a, a] Bool
89
  GreaterW :: OrdLike a => OrdW '[a, a] Bool
90

91
deriving instance Eq (OrdW ds r)
×
92

93
instance Show (OrdW ds r) where
×
94
  show LessOrEqualW = "<=."
2✔
95
  show LessW = "<."
2✔
96
  show GreaterOrEqualW = ">=."
×
97
  show GreaterW = ">."
2✔
98

99
instance Semantics OrdW where
100
  semantics LessOrEqualW = (<=)
2✔
101
  semantics LessW = (<)
2✔
102
  semantics GreaterW = (>)
2✔
103
  semantics GreaterOrEqualW = (>=)
2✔
104

105
instance Syntax OrdW where
2✔
106
  isInfix _ = True
2✔
107

108
-- =============================================
109
-- OrdLike. Ord for Numbers in the Logic
110
-- =============================================
111

112
-- | Ancillary things we need to be able to implement `Logic` instances for
113
-- `OrdW` that make sense for a given type we are comparing things on.
114
class (Ord a, HasSpec a) => OrdLike a where
115
  leqSpec :: a -> Specification a
116
  default leqSpec ::
117
    ( GenericRequires a
118
    , OrdLike (SimpleRep a)
119
    ) =>
120
    a ->
121
    Specification a
122
  leqSpec = fromSimpleRepSpec . leqSpec . toSimpleRep
×
123

124
  ltSpec :: a -> Specification a
125
  default ltSpec ::
126
    ( OrdLike (SimpleRep a)
127
    , GenericRequires a
128
    ) =>
129
    a ->
130
    Specification a
131
  ltSpec = fromSimpleRepSpec . ltSpec . toSimpleRep
×
132

133
  geqSpec :: a -> Specification a
134
  default geqSpec ::
135
    ( OrdLike (SimpleRep a)
136
    , GenericRequires a
137
    ) =>
138
    a ->
139
    Specification a
140
  geqSpec = fromSimpleRepSpec . geqSpec . toSimpleRep
×
141

142
  gtSpec :: a -> Specification a
143
  default gtSpec ::
144
    ( OrdLike (SimpleRep a)
145
    , GenericRequires a
146
    ) =>
147
    a ->
148
    Specification a
149
  gtSpec = fromSimpleRepSpec . gtSpec . toSimpleRep
×
150

151
-- | This instance should be general enough for every type of Number that has a NumSpec as its TypeSpec
152
instance {-# OVERLAPPABLE #-} (Ord a, HasSpec a, MaybeBounded a, Num a, TypeSpec a ~ NumSpec a) => OrdLike a where
153
  leqSpec l = typeSpec $ NumSpecInterval Nothing (Just l)
2✔
154
  ltSpec l
2✔
155
    | Just b <- lowerBound
2✔
156
    , l == b =
1✔
157
        ErrorSpec (pure ("ltSpec @" ++ show (typeOf l) ++ " " ++ show l))
×
158
    | otherwise = typeSpec $ NumSpecInterval Nothing (Just (l - 1))
1✔
159
  geqSpec l = typeSpec $ NumSpecInterval (Just l) Nothing
2✔
160
  gtSpec l
2✔
161
    | Just b <- upperBound
2✔
162
    , l == b =
1✔
163
        ErrorSpec (pure ("gtSpec @" ++ show (typeOf l) ++ " " ++ show l))
×
164
    | otherwise = typeSpec $ NumSpecInterval (Just (l + 1)) Nothing
1✔
165

166
-- ========================================================================
167
-- helper functions for the TypeSpec for Numbers
168
-- ========================================================================
169

170
-- | Helper class for talking about things that _might_ be `Bounded`
171
class MaybeBounded a where
172
  lowerBound :: Maybe a
173
  upperBound :: Maybe a
174

175
  default lowerBound :: Bounded a => Maybe a
176
  lowerBound = Just minBound
2✔
177

178
  default upperBound :: Bounded a => Maybe a
179
  upperBound = Just maxBound
2✔
180

181
newtype Unbounded a = Unbounded a
182

183
instance MaybeBounded (Unbounded a) where
184
  lowerBound = Nothing
2✔
185
  upperBound = Nothing
2✔
186

187
instance MaybeBounded Int
2✔
188

189
instance MaybeBounded Int64
2✔
190

191
instance MaybeBounded Int32
2✔
192

193
instance MaybeBounded Int16
2✔
194

195
instance MaybeBounded Int8
2✔
196

197
instance MaybeBounded Word64
2✔
198

199
instance MaybeBounded Word32
2✔
200

201
instance MaybeBounded Word16
2✔
202

203
instance MaybeBounded Word8
2✔
204

205
deriving via Unbounded Integer instance MaybeBounded Integer
2✔
206

207
deriving via Unbounded (Ratio Integer) instance MaybeBounded (Ratio Integer)
×
208

209
deriving via Unbounded Float instance MaybeBounded Float
2✔
210

211
deriving via Unbounded Double instance MaybeBounded Double
2✔
212

213
instance MaybeBounded Natural where
214
  lowerBound = Just 0
2✔
215
  upperBound = Nothing
2✔
216

217
-- ===================================================================
218
-- The TypeSpec for numbers
219
-- ===================================================================
220

221
-- | t`TypeSpec` for numbers - represented as a single interval
222
data NumSpec n = NumSpecInterval (Maybe n) (Maybe n)
223

224
instance Ord n => Eq (NumSpec n) where
×
225
  NumSpecInterval ml mh == NumSpecInterval ml' mh'
2✔
226
    | isEmpty ml mh = isEmpty ml' mh'
2✔
227
    | isEmpty ml' mh' = isEmpty ml mh
1✔
228
    | otherwise = ml == ml' && mh == mh'
1✔
229
    where
230
      isEmpty (Just a) (Just b) = a > b
2✔
231
      isEmpty _ _ = False
2✔
232

233
instance Show n => Show (NumSpec n) where
×
234
  show (NumSpecInterval ml mu) = lb ++ ".." ++ ub
2✔
235
    where
236
      lb = "[" ++ maybe "" show ml
2✔
237
      ub = maybe "" show mu ++ "]"
2✔
238

239
instance Ord n => Semigroup (NumSpec n) where
×
240
  NumSpecInterval ml mu <> NumSpecInterval ml' mu' =
2✔
241
    NumSpecInterval
2✔
242
      (unionWithMaybe max ml ml')
2✔
243
      (unionWithMaybe min mu mu')
2✔
244

245
instance Ord n => Monoid (NumSpec n) where
×
246
  mempty = NumSpecInterval Nothing Nothing
2✔
247

248
-- ===========================================
249
-- Arbitrary for Num like things
250
-- ===========================================
251

252
instance (Arbitrary a, Ord a) => Arbitrary (NumSpec a) where
253
  arbitrary = do
2✔
254
    m <- arbitrary
2✔
255
    m' <- arbitrary
2✔
256
    frequency [(10, pure $ mkLoHiInterval m m'), (1, pure $ NumSpecInterval m m')]
2✔
257
    where
258
      mkLoHiInterval (Just a) (Just b) = NumSpecInterval (Just $ min a b) (Just $ max a b)
2✔
259
      mkLoHiInterval m m' = NumSpecInterval m m'
2✔
260
  shrink (NumSpecInterval m m') =
×
261
    uncurry NumSpecInterval <$> shrink (m, m')
×
262

263
#if !MIN_VERSION_QuickCheck(2, 17, 0)
264
instance Arbitrary Natural where
265
  arbitrary = wordToNatural . abs <$> arbitrary
×
266
  shrink n = [wordToNatural w | w <- shrink (naturalToWord n)]
2✔
267
#endif
268

269
instance Uniform Natural where
270
  uniformM g = wordToNatural . abs <$> uniformM g
×
271

272
instance Random Natural where
×
273
  randomR (lo, hi) g = first fromIntegral $ randomR (toInteger lo, toInteger hi) g
2✔
274

275
instance Random (Ratio Integer) where
×
276
  randomR (lo, hi) g =
2✔
277
    let (r, g') = random g
2✔
278
     in (lo + (hi - lo) * r, g')
1✔
279
  random g =
2✔
280
    let (d, g') = first ((+ 1) . abs) $ random g
2✔
281
        (n, g'') = randomR (0, d) g'
2✔
282
     in (n % d, g'')
1✔
283

284
-- ==============================================================================
285
-- Operations on NumSpec, that give it the required properties of a TypeSpec
286
-- ==============================================================================
287

288
-- | Admits anything
289
emptyNumSpec :: Ord a => NumSpec a
290
emptyNumSpec = mempty
2✔
291

292
guardNumSpec ::
293
  (Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
294
  [String] ->
295
  NumSpec n ->
296
  Specification n
297
guardNumSpec msg s@(NumSpecInterval (Just a) (Just b))
2✔
298
  | a > b = ErrorSpec ("NumSpec has low bound greater than hi bound" :| (("   " ++ show s) : msg))
2✔
299
  | a == b = equalSpec a
2✔
300
guardNumSpec _ s = typeSpec s
2✔
301

302
-- | Conjunction
303
combineNumSpec ::
304
  (HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
305
  NumSpec n ->
306
  NumSpec n ->
307
  Specification n
308
combineNumSpec s s' = guardNumSpec ["when combining two NumSpecs", "   " ++ show s, "   " ++ show s'] (s <> s')
2✔
309

310
-- | Generate a value that satisfies the spec
311
genFromNumSpec ::
312
  (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) =>
313
  NumSpec n ->
314
  GenT m n
315
genFromNumSpec (NumSpecInterval ml mu) = do
2✔
316
  n <- sizeT
2✔
317
  pureGen . choose =<< constrainInterval (ml <|> lowerBound) (mu <|> upperBound) (fromIntegral n)
2✔
318

319
-- TODO: fixme
320

321
-- | Try to shrink using a `NumSpec`
322
shrinkWithNumSpec :: Arbitrary n => NumSpec n -> n -> [n]
323
shrinkWithNumSpec _ = shrink
2✔
324

325
-- TODO: fixme
326

327
fixupWithNumSpec :: Arbitrary n => NumSpec n -> n -> Maybe n
328
fixupWithNumSpec _ = listToMaybe . shrink
2✔
329

330
constrainInterval ::
331
  (MonadGenError m, Ord a, Num a, Show a) => Maybe a -> Maybe a -> Integer -> m (a, a)
332
constrainInterval ml mu r =
2✔
333
  case (ml, mu) of
2✔
334
    (Nothing, Nothing) -> pure (-r', r')
2✔
335
    (Just l, Nothing)
336
      | l < 0 -> pure (max l (negate r'), r')
2✔
337
      | otherwise -> pure (l, l + 2 * r')
1✔
338
    (Nothing, Just u)
339
      | u > 0 -> pure (negate r', min u r')
2✔
340
      | otherwise -> pure (u - r' - r', u)
1✔
341
    (Just l, Just u)
342
      | l > u -> genError ("bad interval: " ++ show l ++ " " ++ show u)
1✔
343
      | u < 0 -> pure (safeSub l (safeSub l u r') r', u)
2✔
344
      | l >= 0 -> pure (l, safeAdd u (safeAdd u l r') r')
2✔
345
      -- TODO: this is a bit suspect if the bounds are lopsided
346
      | otherwise -> pure (max l (-r'), min u r')
1✔
347
  where
348
    r' = abs $ fromInteger r
2✔
349
    safeSub l a b
2✔
350
      | a - b > a = l
2✔
351
      | otherwise = max l (a - b)
1✔
352
    safeAdd u a b
2✔
353
      | a + b < a = u
2✔
354
      | otherwise = min u (a + b)
1✔
355

356
-- | Check that a value is in the spec
357
conformsToNumSpec :: Ord n => n -> NumSpec n -> Bool
358
conformsToNumSpec i (NumSpecInterval ml mu) = maybe True (<= i) ml && maybe True (i <=) mu
2✔
359

360
-- =======================================================================
361
-- Several of the methods of HasSpec that have default implementations
362
-- could benefit from type specific implementations for numbers. Those
363
-- implementations are found here
364
-- =====================================================================
365

366
-- | Builds a MemberSpec, but returns an Error spec if the list is empty
367
nubOrdMemberSpec :: Ord a => String -> [a] -> Specification a
368
nubOrdMemberSpec message xs =
2✔
369
  memberSpec
2✔
370
    (nubOrd xs)
2✔
371
    ( NE.fromList
×
372
        [ "In call to nubOrdMemberSpec"
×
373
        , "Called from context"
×
374
        , message
×
375
        , "The input is the empty list."
×
376
        ]
377
    )
378

379
lowBound :: Bounded n => Maybe n -> n
380
lowBound Nothing = minBound
2✔
381
lowBound (Just n) = n
×
382

383
highBound :: Bounded n => Maybe n -> n
384
highBound Nothing = maxBound
2✔
385
highBound (Just n) = n
×
386

387
-- | The exact count of the number elements in a Bounded NumSpec
388
countSpec :: forall n. (Bounded n, Integral n) => NumSpec n -> Integer
389
countSpec (NumSpecInterval lo hi) = if lo > hi then 0 else toInteger high - toInteger low + 1
1✔
390
  where
391
    high = highBound hi
2✔
392
    low = lowBound lo
2✔
393

394
-- | The exact number of elements in a Bounded Integral type.
395
finiteSize :: forall n. (Integral n, Bounded n) => Integer
396
finiteSize = toInteger (maxBound @n) - toInteger (minBound @n) + 1
2✔
397

398
-- | This is an optimizing version of  TypeSpec :: TypeSpec n -> [n] -> Specification n
399
--   for Bounded NumSpecs.
400
--                    notInNumSpec :: Bounded n => TypeSpec n -> [n] -> Specification n
401
--   We use this function to specialize the (HasSpec t) method 'typeSpecOpt' for Bounded n.
402
--   So given (TypeSpec interval badlist) we might want to transform it to (MemberSpec goodlist)
403
--   There are 2 opportunities where this can payoff big time.
404
--   1) Suppose the total count of the elements in the interval is < length badlist
405
--      we can then return (MemberSpec (filter elements (`notElem` badlist)))
406
--      this must be smaller than (TypeSpec interval badlist) because the filtered list must be smaller than badlist
407
--   2) Suppose the type 't' is finite with size N. If the length of the badlist > (N/2), then the number of possible
408
--      good things must be smaller than (length badlist), because (possible good + bad == N), so regardless of the
409
--      count of the interval (MemberSpec (filter elements (`notElem` badlist))) is better. Sometimes much better.
410
--      Example, let 'n' be the finite set {0,1,2,3,4,5,6,7,8,9} and the bad list be [0,1,3,4,5,6,8,9]
411
--      (TypeSpec [0..9]  [0,1,3,4,5,6,8,9]) = filter  {0,1,2,3,4,5,6,7,8,9} (`notElem` [0,1,3,4,5,6,8,9]) = [2,7]
412
--      So (MemberSpec [2,7]) is better than  (TypeSpec [0..9]  [0,1,3,4,5,6,8,9]). This works no matter what
413
--      the count of interval is. We only need the (length badlist > (N/2)).
414
notInNumSpec ::
415
  forall n.
416
  ( HasSpec n
417
  , TypeSpec n ~ NumSpec n
418
  , Bounded n
419
  , Integral n
420
  ) =>
421
  NumSpec n ->
422
  [n] ->
423
  Specification n
424
notInNumSpec ns@(NumSpecInterval a b) bad
2✔
425
  | toInteger (length bad) > (finiteSize @n `div` 2) || countSpec ns < toInteger (length bad) =
1✔
426
      nubOrdMemberSpec
×
427
        ("call to: (notInNumSpec " ++ show ns ++ " " ++ show bad ++ ")")
×
428
        [x | x <- [lowBound a .. highBound b], notElem x bad]
×
429
  | otherwise = TypeSpec @n ns bad
1✔
430

431
-- ==========================================================================
432
-- Num n => (NumSpec n) can support operation of Num as interval arithmetic.
433
-- So we will make a (Num (NumSpec Integer)) instance. We won't make other
434
-- instances, because  they would be subject to overflow.
435
-- Given operator ☉, then (a,b) ☉ (c,d) = (minimum s, maximum s) where s = [a ☉ c, a ☉ d, b ☉ c, b ☉ d]
436
-- There are simpler rules for (+) and (-), but for (*) we need to use the general rule.
437
-- ==========================================================================
438

439
guardEmpty :: (Ord n, Num n) => Maybe n -> Maybe n -> NumSpec n -> NumSpec n
440
guardEmpty (Just a) (Just b) s
2✔
441
  | a <= b = s
2✔
442
  | otherwise = NumSpecInterval (Just 1) (Just 0)
1✔
443
guardEmpty _ _ s = s
2✔
444

445
addNumSpec :: (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
446
addNumSpec (NumSpecInterval x y) (NumSpecInterval a b) =
2✔
447
  guardEmpty x y $
2✔
448
    guardEmpty a b $
2✔
449
      NumSpecInterval ((+) <$> x <*> a) ((+) <$> y <*> b)
2✔
450

451
subNumSpec :: (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
452
subNumSpec (NumSpecInterval x y) (NumSpecInterval a b) =
2✔
453
  guardEmpty x y $
2✔
454
    guardEmpty a b $
2✔
455
      NumSpecInterval ((-) <$> x <*> b) ((-) <$> y <*> a)
2✔
456

457
multNumSpec :: (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
458
multNumSpec (NumSpecInterval a b) (NumSpecInterval c d) =
2✔
459
  guardEmpty a b $
2✔
460
    guardEmpty c d $
2✔
461
      NumSpecInterval (unT (minimum s)) (unT (maximum s))
2✔
462
  where
463
    s = [multT (neg a) (neg c), multT (neg a) (pos d), multT (pos b) (neg c), multT (pos b) (pos d)]
2✔
464

465
negNumSpec :: Num n => NumSpec n -> NumSpec n
466
negNumSpec (NumSpecInterval lo hi) = NumSpecInterval (negate <$> hi) (negate <$> lo)
2✔
467

468
instance Num (NumSpec Integer) where
469
  (+) = addNumSpec
2✔
470
  (-) = subNumSpec
2✔
471
  (*) = multNumSpec
2✔
472
  negate = negNumSpec
2✔
473
  fromInteger n = NumSpecInterval (Just (fromInteger n)) (Just (fromInteger n))
2✔
474
  abs = error "No abs in the Num (NumSpec  Integer) instance"
×
475
  signum = error "No signum in the Num (NumSpec  Integer) instance"
×
476

477
-- ========================================================================
478
-- Helper functions for interval multiplication
479
--  (a,b) * (c,d) = (minimum s, maximum s) where s = [a * c, a * d, b * c, b * d]
480

481
-- | T is a sort of special version of Maybe, with two Nothings.
482
--   Given:: NumSpecInterval (Maybe n) (Maybe n) -> Numspec
483
--   We can't distinguish between the two Nothings in (NumSpecInterval Nothing Nothing)
484
--   But using (NumSpecInterval NegInf PosInf) we can, In fact we can make a total ordering on 'T'
485
--   So an ascending Sorted [T x] would all the NegInf on the left and all the PosInf on the right, with
486
--   the Ok's sorted in between. I.e. [NegInf, NegInf, Ok 3, Ok 6, Ok 12, Pos Inf]
487
data T x = NegInf | Ok x | PosInf
488
  deriving (Show, Eq, Ord)
×
489

490
-- \| Conversion between (T x) and (Maybe x)
491
unT :: T x -> Maybe x
492
unT (Ok x) = Just x
2✔
493
unT _ = Nothing
2✔
494

495
-- | Use this on the lower bound. I.e. lo from pair (lo,hi)
496
neg :: Maybe x -> T x
497
neg Nothing = NegInf
2✔
498
neg (Just x) = Ok x
2✔
499

500
-- | Use this on the upper bound. I.e. hi from pair (lo,hi)
501
pos :: Maybe x -> T x
502
pos Nothing = PosInf
2✔
503
pos (Just x) = Ok x
2✔
504

505
-- | multiply two (T x), correctly handling the infinities NegInf and PosInf
506
multT :: Num x => T x -> T x -> T x
507
multT NegInf NegInf = PosInf
2✔
508
multT NegInf PosInf = NegInf
2✔
509
multT NegInf (Ok _) = NegInf
2✔
510
multT (Ok _) NegInf = NegInf
2✔
511
multT (Ok x) (Ok y) = Ok (x * y)
2✔
512
multT (Ok _) PosInf = PosInf
2✔
513
multT PosInf PosInf = PosInf
2✔
514
multT PosInf NegInf = NegInf
2✔
515
multT PosInf (Ok _) = PosInf
2✔
516

517
-- ========================================================================
518
-- We have
519
-- (1) Num Integer
520
-- (2) Num (NumSpec Integer)   And we need
521
-- (3) Num (Specification Integer)
522
-- We need this to implement the method cardinalTypeSpec of (HasSpec t).
523
-- cardinalTypeSpec :: HasSpec a => TypeSpec a -> Specification Integer
524
-- Basically for defining these two cases
525
-- cardinalTypeSpec (Cartesian x y) = (cardinality x) * (cardinality y)
526
-- cardinalTypeSpec (SumSpec leftspec rightspec) = (cardinality leftspec) + (cardinality rightspec)
527
-- So we define addSpecInt for (+)   and  multSpecInt for (*)
528

529
-- | What constraints we need to make HasSpec instance for a Haskell numeric type.
530
--   By abstracting over this, we can avoid making actual HasSpec instances until
531
--   all the requirements (HasSpec Bool, HasSpec(Sum a b)) have been met in
532
--   Constrained.TheKnot.
533
type Number n = (Num n, Enum n, TypeSpec n ~ NumSpec n, Num (NumSpec n), HasSpec n, Ord n)
534

535
-- | Addition on `Specification` for `Number`
536
addSpecInt ::
537
  Number n =>
538
  Specification n ->
539
  Specification n ->
540
  Specification n
541
addSpecInt x y = operateSpec " + " (+) (+) x y
1✔
542

543
subSpecInt ::
544
  Number n =>
545
  Specification n ->
546
  Specification n ->
547
  Specification n
548
subSpecInt x y = operateSpec " - " (-) (-) x y
1✔
549

550
multSpecInt ::
551
  Number n =>
552
  Specification n ->
553
  Specification n ->
554
  Specification n
555
multSpecInt x y = operateSpec " * " (*) (*) x y
×
556

557
-- | let 'n' be some numeric type, and 'f' and 'ft' be operations on 'n' and (TypeSpec n)
558
--   Then lift these operations from (TypeSpec n) to (Specification n)
559
--   Normally 'f' will be a (Num n) instance method (+,-,*) on n,
560
--   and 'ft' will be a a (Num (TypeSpec n)) instance method (+,-,*) on (TypeSpec n)
561
--   But this will work for any operations 'f' and 'ft' with the right types
562
operateSpec ::
563
  Number n =>
564
  String ->
565
  (n -> n -> n) ->
566
  (TypeSpec n -> TypeSpec n -> TypeSpec n) ->
567
  Specification n ->
568
  Specification n ->
569
  Specification n
570
operateSpec operator f ft (ExplainSpec es x) y = explainSpec es $ operateSpec operator f ft x y
1✔
571
operateSpec operator f ft x (ExplainSpec es y) = explainSpec es $ operateSpec operator f ft x y
×
572
operateSpec operator f ft x y = case (x, y) of
2✔
573
  (ErrorSpec xs, ErrorSpec ys) -> ErrorSpec (xs <> ys)
×
574
  (ErrorSpec xs, _) -> ErrorSpec xs
×
575
  (_, ErrorSpec ys) -> ErrorSpec ys
×
576
  (TrueSpec, _) -> TrueSpec
2✔
577
  (_, TrueSpec) -> TrueSpec
2✔
578
  (_, SuspendedSpec _ _) -> TrueSpec
×
579
  (SuspendedSpec _ _, _) -> TrueSpec
×
580
  (TypeSpec a bad1, TypeSpec b bad2) -> TypeSpec (ft a b) [f b1 b2 | b1 <- bad1, b2 <- bad2]
×
581
  (MemberSpec xs, MemberSpec ys) ->
582
    nubOrdMemberSpec
2✔
583
      (show x ++ operator ++ show y)
×
584
      [f x1 y1 | x1 <- NE.toList xs, y1 <- NE.toList ys]
2✔
585
  -- This block is all (MemberSpec{}, TypeSpec{}) with MemberSpec on the left
586
  (MemberSpec ys, TypeSpec (NumSpecInterval (Just i) (Just j)) bad) ->
587
    let xs = NE.toList ys
×
588
     in nubOrdMemberSpec
589
          (show x ++ operator ++ show y)
×
590
          [f x1 y1 | x1 <- xs, y1 <- [i .. j], not (elem y1 bad)]
×
591
  -- Somewhat loose spec here, but more accurate then TrueSpec, it is exact if 'xs' has one element (i.e. 'xs' = [i])
592
  (MemberSpec ys, TypeSpec (NumSpecInterval lo hi) bads) ->
593
    -- We use the specialized version of 'TypeSpec' 'typeSpecOpt'
594
    let xs = NE.toList ys
2✔
595
     in typeSpecOpt
596
          (NumSpecInterval (f (minimum xs) <$> lo) (f (maximum xs) <$> hi))
1✔
597
          [f x1 b | x1 <- xs, b <- bads]
1✔
598
  -- we flip the arguments, so we need to flip the functions as well
599
  (sleft, sright) -> operateSpec operator (\a b -> f b a) (\u v -> ft v u) sright sleft
1✔
600

601
-- | This is very liberal, since in lots of cases it returns TrueSpec.
602
--  for example all operations on SuspendedSpec, and certain
603
--  operations between TypeSpec and MemberSpec. Perhaps we should
604
--  remove it. Only the addSpec (+) and multSpec (*) methods are used.
605
--  But, it is kind of cool ...
606
--  In Fact we can use this to make Num(Specification n) instance for any 'n'.
607
--  But, only Integer is safe, because in all other types (+) and especially
608
--  (-) can lead to overflow or underflow failures.
609
instance Number Integer => Num (Specification Integer) where
×
610
  (+) = addSpecInt
2✔
611
  (-) = subSpecInt
×
612
  (*) = multSpecInt
×
613
  fromInteger n = TypeSpec (NumSpecInterval (Just n) (Just n)) []
×
614
  abs _ = TrueSpec
×
615
  signum _ = TrueSpec
×
616

617
-- ===========================================================================
618

619
-- | Put some (admittedly loose bounds) on the number of solutions that
620
--   'genFromTypeSpec' might return. For lots of types, there is no way to be very accurate.
621
--   Here we lift the HasSpec methods 'cardinalTrueSpec' and 'cardinalTypeSpec'
622
--   from (TypeSpec Integer) to (Specification Integer)
623
cardinality ::
624
  forall a. (Number Integer, HasSpec a) => Specification a -> Specification Integer
625
cardinality (ExplainSpec es s) = explainSpec es (cardinality s)
2✔
626
cardinality TrueSpec = cardinalTrueSpec @a
2✔
627
cardinality (MemberSpec es) = equalSpec (toInteger $ length (nub (NE.toList es)))
2✔
628
cardinality ErrorSpec {} = equalSpec 0
2✔
629
cardinality (TypeSpec s cant) =
630
  subSpecInt
2✔
631
    (cardinalTypeSpec @a s)
2✔
632
    (equalSpec (toInteger $ length (nub $ filter (\c -> conformsTo @a c s) cant)))
2✔
633
cardinality SuspendedSpec {} = cardinalTrueSpec @a
2✔
634

635
-- | A generic function to use as an instance for the HasSpec method
636
--   cardinalTypeSpec :: HasSpec a => TypeSpec a -> Specification Integer
637
--   for types 'n' such that (TypeSpec n ~ NumSpec n)
638
cardinalNumSpec ::
639
  forall n. (Integral n, MaybeBounded n, HasSpec n) => NumSpec n -> Specification Integer
640
cardinalNumSpec (NumSpecInterval (Just lo) (Just hi)) =
2✔
641
  if hi >= lo
1✔
642
    then equalSpec (toInteger hi - toInteger lo + 1)
2✔
UNCOV
643
    else equalSpec 0
×
644
cardinalNumSpec (NumSpecInterval Nothing (Just hi)) =
645
  case lowerBound @n of
2✔
646
    Just lo -> equalSpec (toInteger hi - toInteger lo)
2✔
647
    Nothing -> TrueSpec
×
648
cardinalNumSpec (NumSpecInterval (Just lo) Nothing) =
649
  case upperBound @n of
2✔
650
    Just hi -> equalSpec (toInteger hi - toInteger lo)
2✔
651
    Nothing -> TrueSpec
×
652
cardinalNumSpec (NumSpecInterval Nothing Nothing) = cardinalTrueSpec @n
2✔
653

654
-- ====================================================================
655
-- Now the operations on Numbers
656

657
-- | Everything we need to make the number operations make sense on a given type
658
class (Num a, HasSpec a, HasDivision a, OrdLike a) => NumLike a where
659
  subtractSpec :: a -> TypeSpec a -> Specification a
660
  default subtractSpec ::
661
    ( NumLike (SimpleRep a)
662
    , GenericRequires a
663
    ) =>
664
    a ->
665
    TypeSpec a ->
666
    Specification a
667
  subtractSpec a ts = fromSimpleRepSpec $ subtractSpec (toSimpleRep a) ts
×
668

669
  negateSpec :: TypeSpec a -> Specification a
670
  default negateSpec ::
671
    ( NumLike (SimpleRep a)
672
    , GenericRequires a
673
    ) =>
674
    TypeSpec a ->
675
    Specification a
676
  negateSpec = fromSimpleRepSpec . negateSpec @(SimpleRep a)
×
677

678
  safeSubtract :: a -> a -> Maybe a
679
  default safeSubtract ::
680
    ( NumLike (SimpleRep a)
681
    , GenericRequires a
682
    ) =>
683
    a ->
684
    a ->
685
    Maybe a
686
  safeSubtract a b = fromSimpleRep <$> safeSubtract @(SimpleRep a) (toSimpleRep a) (toSimpleRep b)
×
687

688
-- | Operations on numbers.
689
-- The reason there is no implementation of abs here is that you can't easily deal with abs
690
-- without specifications becoming very large. Consider the following example:
691
-- > constrained $ \ x -> [1000 <. abs_ x, abs_ x <. 1050]
692
-- The natural `Specification` here would be something like `(-1050, -1000) || (1000, 1050)`
693
-- - the disjoint union of two open, non-overlapping, intervals. However, this doesn't work
694
-- because number type-specs only support a single interval. You could fudge it in all sorts of ways
695
-- by using `chooseSpec` or by using the can't set (which would blow up to be 2000 elements large in this
696
-- case). In short, there is no _satisfactory_ solution here.
697
data IntW (as :: [Type]) b where
698
  AddW :: NumLike a => IntW '[a, a] a
699
  MultW :: NumLike a => IntW '[a, a] a
700
  NegateW :: NumLike a => IntW '[a] a
701
  SignumW :: NumLike a => IntW '[a] a
702

703
deriving instance Eq (IntW dom rng)
×
704

705
instance Show (IntW d r) where
×
706
  show AddW = "+"
2✔
707
  show NegateW = "negate_"
2✔
708
  show MultW = "*"
2✔
709
  show SignumW = "signum_"
2✔
710

711
instance Semantics IntW where
712
  semantics AddW = (+)
2✔
713
  semantics NegateW = negate
2✔
714
  semantics MultW = (*)
2✔
715
  semantics SignumW = signum
2✔
716

717
instance Syntax IntW where
2✔
718
  isInfix AddW = True
2✔
719
  isInfix NegateW = False
×
720
  isInfix MultW = True
×
721
  isInfix SignumW = False
×
722

723
class HasDivision a where
724
  doDivide :: a -> a -> a
725
  default doDivide ::
726
    ( HasDivision (SimpleRep a)
727
    , GenericRequires a
728
    ) =>
729
    a ->
730
    a ->
731
    a
732
  doDivide a b = fromSimpleRep $ doDivide (toSimpleRep a) (toSimpleRep b)
×
733

734
  divideSpec :: a -> TypeSpec a -> Specification a
735
  default divideSpec ::
736
    ( HasDivision (SimpleRep a)
737
    , GenericRequires a
738
    ) =>
739
    a ->
740
    TypeSpec a ->
741
    Specification a
742
  divideSpec a ts = fromSimpleRepSpec $ divideSpec (toSimpleRep a) ts
×
743

744
divideSpecIntegral :: (HasSpec a, MaybeBounded a, Integral a, TypeSpec a ~ NumSpec a) => a -> TypeSpec a -> Specification a
745
divideSpecIntegral 0 _ = TrueSpec
1✔
746
divideSpecIntegral a (NumSpecInterval (unionWithMaybe max lowerBound -> ml) (unionWithMaybe min upperBound -> mu)) = typeSpec ts
2✔
747
    where
748
      ts
2✔
749
        | a > 0 = NumSpecInterval ml' mu'
2✔
750
        | otherwise = NumSpecInterval mu' ml'
1✔
751
      ml' = adjustLowerBound <$> ml
2✔
752
      mu' = adjustUpperBound <$> mu
2✔
753

754
      -- NOTE: negate has different overflow semantics than div, so that's why we use negate below...
755

756
      adjustLowerBound l
2✔
757
        | a == 1 = l
2✔
758
        | a == -1 = negate l
2✔
759
        | otherwise =
×
760
            let r = l `div` a
2✔
761
             in if toInteger r * toInteger a < toInteger l
2✔
762
                  then r + signum a
2✔
763
                  else r
2✔
764

765
      adjustUpperBound u
2✔
766
        | a == 1 = u
2✔
767
        | a == -1 = negate u
2✔
768
        | otherwise =
×
769
            let r = u `div` a
2✔
770
             in if toInteger r * toInteger a > toInteger u
2✔
771
                  then r - signum a
2✔
772
                  else r
2✔
773

774
instance HasDivision Integer where
775
  doDivide = div
2✔
776
  divideSpec = divideSpecIntegral
2✔
777

778
instance HasDivision Natural where
779
  doDivide = div
×
780
  divideSpec = divideSpecIntegral
×
781

782
instance HasDivision Int where
783
  doDivide = div
2✔
784
  divideSpec = divideSpecIntegral
2✔
785

786
instance HasDivision Int8 where
787
  doDivide = div
2✔
788
  divideSpec = divideSpecIntegral
2✔
789

790
instance HasDivision Int16 where
791
  doDivide = div
×
792
  divideSpec = divideSpecIntegral
×
793

794
instance HasDivision Int32 where
795
  doDivide = div
×
796
  divideSpec = divideSpecIntegral
×
797

798
instance HasDivision Int64 where
799
  doDivide = div
×
800
  divideSpec = divideSpecIntegral
×
801

802
instance HasDivision Word8 where
803
  doDivide = div
2✔
804
  divideSpec = divideSpecIntegral
2✔
805

806
instance HasDivision Word16 where
807
  doDivide = div
×
808
  divideSpec = divideSpecIntegral
×
809

810
instance HasDivision Word32 where
811
  doDivide = div
×
812
  divideSpec = divideSpecIntegral
×
813

814
instance HasDivision Word64 where
815
  doDivide = div
×
816
  divideSpec = divideSpecIntegral
×
817

818
instance HasDivision (Ratio Integer) where
819
  doDivide = (/)
2✔
820

821
  divideSpec 0 _ = TrueSpec
1✔
822
  divideSpec a (NumSpecInterval ml mu) = typeSpec ts
2✔
823
    where
824
      ts
2✔
825
        | a > 0 = NumSpecInterval ml' mu'
1✔
826
        | otherwise = NumSpecInterval mu' ml'
×
827
      ml' = adjustLowerBound <$> ml
2✔
828
      mu' = adjustUpperBound <$> mu
1✔
829
      adjustLowerBound l =
2✔
830
        let r = l / a
2✔
831
            l' = r * a
2✔
832
         in if l' < l
1✔
833
              then r + (l - l') * 2 / a
×
834
              else r
2✔
835

836
      adjustUpperBound u =
×
837
        let r = u / a
×
838
            u' = r * a
×
839
         in if u < u'
×
840
              then r - (u' - u) * 2 / a
×
841
              else r
×
842

843
instance HasDivision Float where
844
  doDivide = (/)
2✔
845

846
  divideSpec 0 _ = TrueSpec
1✔
847
  divideSpec a (NumSpecInterval ml mu) = typeSpec ts
2✔
848
    where
849
      ts
2✔
850
        | a > 0 = NumSpecInterval ml' mu'
2✔
851
        | otherwise = NumSpecInterval mu' ml'
1✔
852
      ml' = adjustLowerBound <$> ml
2✔
853
      mu' = adjustUpperBound <$> mu
2✔
854
      adjustLowerBound l =
2✔
855
        let r = l / a
2✔
856
            l' = r * a
2✔
857
         in if l' < l
2✔
858
              then r + (l - l') * 2 / a
2✔
859
              else r
2✔
860

861
      adjustUpperBound u =
2✔
862
        let r = u / a
2✔
863
            u' = r * a
2✔
864
         in if u < u'
2✔
865
              then r - (u' - u) * 2 / a
2✔
866
              else r
2✔
867

868
instance HasDivision Double where
869
  doDivide = (/)
2✔
870

871
  divideSpec 0 _ = TrueSpec
1✔
872
  divideSpec a (NumSpecInterval ml mu) = typeSpec ts
2✔
873
    where
874
      ts
2✔
875
        | a > 0 = NumSpecInterval ml' mu'
2✔
876
        | otherwise = NumSpecInterval mu' ml'
1✔
877
      ml' = adjustLowerBound <$> ml
2✔
878
      mu' = adjustUpperBound <$> mu
2✔
879
      adjustLowerBound l =
2✔
880
        let r = l / a
2✔
881
            l' = r * a
2✔
882
         in if l' < l
2✔
883
              then r + (l - l') * 2 / a
2✔
884
              else r
2✔
885

886
      adjustUpperBound u =
2✔
887
        let r = u / a
2✔
888
            u' = r * a
2✔
889
         in if u < u'
2✔
890
              then r - (u' - u) * 2 / a
2✔
891
              else r
2✔
892

893
-- | A type that we can reason numerically about in constraints
894
type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a, HasDivision a)
895

896
instance {-# OVERLAPPABLE #-} Numeric a => NumLike a where
897
  subtractSpec a ts@(NumSpecInterval ml mu)
2✔
898
    | Just u <- mu
2✔
899
    , a > 0
2✔
900
    , Nothing <- safeSubtract a u =
2✔
901
        ErrorSpec $
2✔
902
          NE.fromList
×
903
            [ "Underflow in subtractSpec (" ++ showType @a ++ "):"
×
904
            , "  a = " ++ show a
×
905
            , "  ts = " ++ show ts
×
906
            ]
907
    | Just l <- ml
2✔
908
    , a < 0
2✔
909
    , Nothing <- safeSubtract a l =
2✔
910
        ErrorSpec $
2✔
911
          NE.fromList
×
912
            [ "Overflow in subtractSpec (" ++ showType @a ++ "):"
×
913
            , "  a = " ++ show a
×
914
            , "  ts = " ++ show ts
×
915
            ]
916
    | otherwise = typeSpec $ NumSpecInterval (safeSub a <$> ml) (safeSub a <$> mu)
1✔
917
    where
918
      safeSub :: a -> a -> a
919
      safeSub a1 x
2✔
920
        | Just r <- safeSubtract a1 x = r
2✔
921
        | a1 < 0 = fromJust upperBound
2✔
922
        | otherwise = fromJust lowerBound
1✔
923

924
  negateSpec (NumSpecInterval ml mu) = typeSpec $ NumSpecInterval (negate <$> mu) (negate <$> ml)
2✔
925

926
  safeSubtract a x
2✔
927
    | a > 0
2✔
928
    , Just lb <- lowerBound
2✔
929
    , lb + a > x =
2✔
930
        Nothing
2✔
931
    | a < 0
2✔
932
    , Just ub <- upperBound
2✔
933
    , ub + a < x =
2✔
934
        Nothing
2✔
935
    | otherwise = Just $ x - a
1✔
936

937
instance NumLike a => Num (Term a) where
2✔
938
  (+) = (+.)
2✔
939
  negate = negate_
2✔
940
  fromInteger = Lit . fromInteger
2✔
941
  (*) = (*.)
2✔
942
  signum = signum_
2✔
943
  abs = error "No implementation for abs @(Term a)"
×
944

945
invertMult :: (HasSpec a, Num a, HasDivision a) => a -> a -> Maybe a
946
invertMult a b =
2✔
947
  let r = a `doDivide` b in if r * b == a then Just r else Nothing
2✔
948

949
-- | Just a note that these instances won't work until we are in a context where
950
--   there is a HasSpec instance of 'a', which (NumLike a) demands.
951
--   This happens in Constrained.Experiment.TheKnot
952
instance Logic IntW where
1✔
953
  propagateTypeSpec AddW (HOLE :<: i) ts cant = subtractSpec i ts <> notMemberSpec (mapMaybe (safeSubtract i) cant)
2✔
954
  propagateTypeSpec AddW ctx ts cant = propagateTypeSpec AddW (flipCtx ctx) ts cant
2✔
955
  propagateTypeSpec NegateW (Unary HOLE) ts cant = negateSpec ts <> notMemberSpec (map negate cant)
2✔
956
  propagateTypeSpec MultW (HOLE :<: 0) ts cant
957
    | 0 `conformsToSpec` TypeSpec ts cant = TrueSpec
2✔
958
    | otherwise = ErrorSpec $ NE.fromList ["zero"]
1✔
959
  propagateTypeSpec MultW (HOLE :<: i) ts cant = divideSpec i ts <> notMemberSpec (mapMaybe (flip invertMult i) cant)
2✔
960
  propagateTypeSpec MultW ctx ts cant = propagateTypeSpec MultW (flipCtx ctx) ts cant
2✔
961
  propagateTypeSpec SignumW (Unary HOLE) ts cant =
962
    constrained $ \x ->
2✔
963
      [x `satisfies` notMemberSpec [0] | not $ ok 0]
2✔
964
        ++ [Assert $ 0 <=. x | not $ ok (-1)]
2✔
965
        ++ [Assert $ x <=. 0 | not $ ok 1]
2✔
966
    where
967
      ok = flip conformsToSpec (TypeSpec ts cant)
2✔
968

969
  propagateMemberSpec AddW (HOLE :<: i) es =
2✔
970
    memberSpec
2✔
971
      (nubOrd $ mapMaybe (safeSubtract i) (NE.toList es))
2✔
972
      ( NE.fromList
×
973
          [ "propagateSpecFn on (" ++ show i ++ " +. HOLE)"
×
974
          , "The Spec is a MemberSpec = " ++ show es -- show (MemberSpec @HasSpec @TS es)
×
975
          , "We can't safely subtract " ++ show i ++ " from any choice in the MemberSpec."
×
976
          ]
977
      )
978
  propagateMemberSpec AddW ctx es = propagateMemberSpec AddW (flipCtx ctx) es
2✔
979
  propagateMemberSpec NegateW (Unary HOLE) es = MemberSpec $ NE.nub $ fmap negate es
2✔
980
  propagateMemberSpec MultW (HOLE :<: 0) es
981
    | 0 `elem` es = TrueSpec
2✔
982
    | otherwise = ErrorSpec $ NE.fromList ["zero"]
1✔
983
  propagateMemberSpec MultW (HOLE :<: i) es = memberSpec (mapMaybe (flip invertMult i) (NE.toList es)) (NE.fromList ["propagateSpec"])
1✔
984
  propagateMemberSpec MultW ctx es = propagateMemberSpec MultW (flipCtx ctx) es
2✔
985
  propagateMemberSpec SignumW (Unary HOLE) es
986
    | all ((`notElem` [-1, 0, 1]) . signum) es =
1✔
987
        ErrorSpec $ NE.fromList ["signum for invalid member spec", show es]
×
988
    | otherwise = constrained $ \x ->
1✔
989
        [x `satisfies` notMemberSpec [0] | 0 `notElem` es]
2✔
990
          ++ [Assert $ 0 <=. x | -1 `notElem` es]
2✔
991
          ++ [Assert $ x <=. 0 | 1 `notElem` es]
2✔
992

993
  rewriteRules AddW (x :> y :> Nil) _ | x == y = Just $ 2 * x
2✔
994
  rewriteRules _ _ _ = Nothing
2✔
995

996
infix 4 +.
997

998
-- | `Term`-level `(+)`
999
(+.) :: NumLike a => Term a -> Term a -> Term a
1000
(+.) = appTerm AddW
2✔
1001

1002
infixl 7 *.
1003

1004
-- | `Term`-level `(+)`
1005
(*.) :: NumLike a => Term a -> Term a -> Term a
1006
(*.) = appTerm MultW
2✔
1007

1008
-- | `Term`-level `negate`
1009
negate_ :: NumLike a => Term a -> Term a
1010
negate_ = appTerm NegateW
2✔
1011

1012
-- | `Term`-level `signum`
1013
signum_ :: NumLike a => Term a -> Term a
1014
signum_ = appTerm SignumW
2✔
1015

1016
infix 4 -.
1017

1018
-- | `Term`-level `(-)`
1019
(-.) :: Numeric n => Term n -> Term n -> Term n
1020
(-.) x y = x +. negate_ y
×
1021

1022
infixr 4 <=.
1023

1024
-- | `Term`-level `(<=)`
1025
(<=.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
1026
(<=.) = appTerm LessOrEqualW
2✔
1027

1028
infixr 4 <.
1029

1030
-- | `Term`-level `(<)`
1031
(<.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
1032
(<.) = appTerm LessW
2✔
1033

1034
infixr 4 >=.
1035

1036
-- | `Term`-level `(>=)`
1037
(>=.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
1038
(>=.) = appTerm GreaterOrEqualW
2✔
1039

1040
infixr 4 >.
1041

1042
-- | `Term`-level `(>)`
1043
(>.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
1044
(>.) = appTerm GreaterW
2✔
1045

1046
-- | t`TypeSpec`-level `satisfies` to implement `toPreds` in
1047
-- `HasSpec` instance
1048
toPredsNumSpec ::
1049
  OrdLike n =>
1050
  Term n ->
1051
  NumSpec n ->
1052
  Pred
1053
toPredsNumSpec v (NumSpecInterval ml mu) =
2✔
1054
  fold $
2✔
1055
    [Assert $ Lit l <=. v | l <- maybeToList ml]
2✔
1056
      ++ [Assert $ v <=. Lit u | u <- maybeToList mu]
2✔
1057

1058
instance Logic OrdW where
×
1059
  propagate f ctxt (ExplainSpec [] s) = propagate f ctxt s
1✔
1060
  propagate f ctxt (ExplainSpec es s) = ExplainSpec es $ propagate f ctxt s
2✔
1061
  propagate _ _ TrueSpec = TrueSpec
2✔
1062
  propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs
1✔
1063
  propagate GreaterW (HOLE :? x :> Nil) spec =
1064
    propagate LessW (x :! Unary HOLE) spec
2✔
1065
  propagate GreaterW (x :! Unary HOLE) spec =
1066
    propagate LessW (HOLE :? x :> Nil) spec
2✔
1067
  propagate LessOrEqualW (HOLE :? Value x :> Nil) (SuspendedSpec v ps) =
1068
    constrained $ \v' -> Let (App LessOrEqualW (v' :> Lit x :> Nil)) (v :-> ps)
2✔
1069
  propagate LessOrEqualW (Value x :! Unary HOLE) (SuspendedSpec v ps) =
1070
    constrained $ \v' -> Let (App LessOrEqualW (Lit x :> v' :> Nil)) (v :-> ps)
2✔
1071
  propagate LessOrEqualW (HOLE :? Value l :> Nil) spec =
1072
    caseBoolSpec spec $ \case True -> leqSpec l; False -> gtSpec l
2✔
1073
  propagate LessOrEqualW (Value l :! Unary HOLE) spec =
1074
    caseBoolSpec spec $ \case True -> geqSpec l; False -> ltSpec l
2✔
1075
  propagate GreaterOrEqualW (HOLE :? Value x :> Nil) spec =
1076
    propagate LessOrEqualW (Value x :! Unary HOLE) spec
2✔
1077
  propagate GreaterOrEqualW (x :! Unary HOLE) spec =
1078
    propagate LessOrEqualW (HOLE :? x :> Nil) spec
×
1079
  propagate LessW (HOLE :? Value x :> Nil) (SuspendedSpec v ps) =
1080
    constrained $ \v' -> Let (App LessW (v' :> Lit x :> Nil)) (v :-> ps)
2✔
1081
  propagate LessW (Value x :! Unary HOLE) (SuspendedSpec v ps) =
1082
    constrained $ \v' -> Let (App LessW (Lit x :> v' :> Nil)) (v :-> ps)
2✔
1083
  propagate LessW (HOLE :? Value l :> Nil) spec =
1084
    caseBoolSpec spec $ \case True -> ltSpec l; False -> geqSpec l
2✔
1085
  propagate LessW (Value l :! Unary HOLE) spec =
1086
    caseBoolSpec spec $ \case True -> gtSpec l; False -> leqSpec l
2✔
1087

1088
-- | @if-then-else@ on a specification, useful for writing `propagate` implementations
1089
-- of predicates, e.g.:
1090
-- > propagate LessW (Value l :! Unary HOLE) spec =
1091
-- >   caseBoolSpec spec $ \case True -> gtSpec l; False -> leqSpec l
1092
caseBoolSpec ::
1093
  HasSpec a => Specification Bool -> (Bool -> Specification a) -> Specification a
1094
caseBoolSpec spec cont = case possibleValues spec of
2✔
1095
  [] -> ErrorSpec (NE.fromList ["No possible values in caseBoolSpec"])
1✔
1096
  [b] -> cont b
2✔
1097
  _ -> mempty
2✔
1098
  where
1099
    -- This will always get the same result, and probably faster since running 2
1100
    -- conformsToSpec on True and False takes less time than simplifying the spec.
1101
    -- Since we are in TheKnot, we could keep the simplifySpec. Is there a good reason to?
1102
    possibleValues s = filter (flip conformsToSpec s) [True, False]
2✔
1103

1104
------------------------------------------------------------------------
1105
-- Instances of HasSpec for numeric types
1106
------------------------------------------------------------------------
1107

1108
instance HasSpec Integer where
×
1109
  type TypeSpec Integer = NumSpec Integer
1110
  emptySpec = emptyNumSpec
2✔
1111
  combineSpec = combineNumSpec
2✔
1112
  genFromTypeSpec = genFromNumSpec
2✔
1113
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1114
  fixupWithTypeSpec = fixupWithNumSpec
×
1115
  conformsTo = conformsToNumSpec
2✔
1116
  toPreds = toPredsNumSpec
2✔
1117
  cardinalTypeSpec = cardinalNumSpec
×
1118
  guardTypeSpec = guardNumSpec
2✔
1119

1120
instance HasSpec Int where
×
1121
  type TypeSpec Int = NumSpec Int
1122
  emptySpec = emptyNumSpec
2✔
1123
  combineSpec = combineNumSpec
2✔
1124
  genFromTypeSpec = genFromNumSpec
2✔
1125
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1126
  fixupWithTypeSpec = fixupWithNumSpec
2✔
1127
  conformsTo = conformsToNumSpec
2✔
1128
  toPreds = toPredsNumSpec
2✔
1129
  cardinalTypeSpec = cardinalNumSpec
2✔
1130
  guardTypeSpec = guardNumSpec
2✔
1131

1132
instance HasSpec (Ratio Integer) where
×
1133
  type TypeSpec (Ratio Integer) = NumSpec (Ratio Integer)
1134
  emptySpec = emptyNumSpec
2✔
1135
  combineSpec = combineNumSpec
2✔
1136
  genFromTypeSpec = genFromNumSpec
2✔
1137
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1138
  fixupWithTypeSpec = fixupWithNumSpec
×
1139
  conformsTo = conformsToNumSpec
2✔
1140
  toPreds = toPredsNumSpec
2✔
1141
  cardinalTypeSpec _ = TrueSpec
×
1142
  guardTypeSpec = guardNumSpec
2✔
1143

1144
instance HasSpec Natural where
×
1145
  type TypeSpec Natural = NumSpec Natural
1146
  emptySpec = emptyNumSpec
2✔
1147
  combineSpec = combineNumSpec
2✔
1148
  genFromTypeSpec = genFromNumSpec
2✔
1149
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1150
  fixupWithTypeSpec = fixupWithNumSpec
×
1151
  conformsTo = conformsToNumSpec
2✔
1152
  toPreds = toPredsNumSpec
×
1153
  cardinalTypeSpec (NumSpecInterval (fromMaybe 0 -> lo) (Just hi)) =
×
1154
    if lo < hi
×
1155
      then equalSpec (fromIntegral $ hi - lo + 1)
×
1156
      else equalSpec 0
×
1157
  cardinalTypeSpec _ = TrueSpec
×
1158
  guardTypeSpec = guardNumSpec
2✔
1159

1160
instance HasSpec Word8 where
×
1161
  type TypeSpec Word8 = NumSpec Word8
1162
  emptySpec = emptyNumSpec
2✔
1163
  combineSpec = combineNumSpec
2✔
1164
  genFromTypeSpec = genFromNumSpec
2✔
1165
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1166
  fixupWithTypeSpec = fixupWithNumSpec
×
1167
  conformsTo = conformsToNumSpec
2✔
1168
  toPreds = toPredsNumSpec
2✔
1169
  cardinalTypeSpec = cardinalNumSpec
×
1170
  cardinalTrueSpec = equalSpec 256
×
1171
  typeSpecOpt = notInNumSpec
2✔
1172
  guardTypeSpec = guardNumSpec
2✔
1173

1174
instance HasSpec Word16 where
×
1175
  type TypeSpec Word16 = NumSpec Word16
1176
  emptySpec = emptyNumSpec
2✔
1177
  combineSpec = combineNumSpec
2✔
1178
  genFromTypeSpec = genFromNumSpec
2✔
1179
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1180
  fixupWithTypeSpec = fixupWithNumSpec
×
1181
  conformsTo = conformsToNumSpec
2✔
1182
  toPreds = toPredsNumSpec
×
1183
  cardinalTypeSpec = cardinalNumSpec
×
1184
  cardinalTrueSpec = equalSpec 65536
×
1185
  guardTypeSpec = guardNumSpec
2✔
1186

1187
instance HasSpec Word32 where
×
1188
  type TypeSpec Word32 = NumSpec Word32
1189
  emptySpec = emptyNumSpec
2✔
1190
  combineSpec = combineNumSpec
2✔
1191
  genFromTypeSpec = genFromNumSpec
2✔
1192
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1193
  fixupWithTypeSpec = fixupWithNumSpec
×
1194
  conformsTo = conformsToNumSpec
2✔
1195
  toPreds = toPredsNumSpec
×
1196
  cardinalTypeSpec = cardinalNumSpec
×
1197
  guardTypeSpec = guardNumSpec
2✔
1198

1199
instance HasSpec Word64 where
×
1200
  type TypeSpec Word64 = NumSpec Word64
1201
  emptySpec = emptyNumSpec
2✔
1202
  combineSpec = combineNumSpec
2✔
1203
  genFromTypeSpec = genFromNumSpec
2✔
1204
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1205
  fixupWithTypeSpec = fixupWithNumSpec
×
1206
  conformsTo = conformsToNumSpec
2✔
1207
  toPreds = toPredsNumSpec
2✔
1208
  cardinalTypeSpec = cardinalNumSpec
2✔
1209
  guardTypeSpec = guardNumSpec
2✔
1210

1211
instance HasSpec Int8 where
×
1212
  type TypeSpec Int8 = NumSpec Int8
1213
  emptySpec = emptyNumSpec
2✔
1214
  combineSpec = combineNumSpec
2✔
1215
  genFromTypeSpec = genFromNumSpec
2✔
1216
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1217
  fixupWithTypeSpec = fixupWithNumSpec
×
1218
  conformsTo = conformsToNumSpec
2✔
1219
  toPreds = toPredsNumSpec
2✔
1220
  cardinalTrueSpec = equalSpec 256
×
1221
  cardinalTypeSpec = cardinalNumSpec
×
1222
  guardTypeSpec = guardNumSpec
2✔
1223

1224
instance HasSpec Int16 where
×
1225
  type TypeSpec Int16 = NumSpec Int16
1226
  emptySpec = emptyNumSpec
2✔
1227
  combineSpec = combineNumSpec
2✔
1228
  genFromTypeSpec = genFromNumSpec
2✔
1229
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1230
  fixupWithTypeSpec = fixupWithNumSpec
×
1231
  conformsTo = conformsToNumSpec
2✔
1232
  toPreds = toPredsNumSpec
×
1233
  cardinalTypeSpec = cardinalNumSpec
×
1234
  cardinalTrueSpec = equalSpec 65536
×
1235
  guardTypeSpec = guardNumSpec
2✔
1236

1237
instance HasSpec Int32 where
×
1238
  type TypeSpec Int32 = NumSpec Int32
1239
  emptySpec = emptyNumSpec
2✔
1240
  combineSpec = combineNumSpec
2✔
1241
  genFromTypeSpec = genFromNumSpec
2✔
1242
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1243
  fixupWithTypeSpec = fixupWithNumSpec
×
1244
  conformsTo = conformsToNumSpec
2✔
1245
  toPreds = toPredsNumSpec
×
1246
  cardinalTypeSpec = cardinalNumSpec
×
1247
  guardTypeSpec = guardNumSpec
2✔
1248

1249
instance HasSpec Int64 where
×
1250
  type TypeSpec Int64 = NumSpec Int64
1251
  emptySpec = emptyNumSpec
2✔
1252
  combineSpec = combineNumSpec
2✔
1253
  genFromTypeSpec = genFromNumSpec
2✔
1254
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1255
  fixupWithTypeSpec = fixupWithNumSpec
×
1256
  conformsTo = conformsToNumSpec
2✔
1257
  toPreds = toPredsNumSpec
×
1258
  cardinalTypeSpec = cardinalNumSpec
×
1259
  guardTypeSpec = guardNumSpec
2✔
1260

1261
instance HasSpec Float where
×
1262
  type TypeSpec Float = NumSpec Float
1263
  emptySpec = emptyNumSpec
2✔
1264
  combineSpec = combineNumSpec
2✔
1265
  genFromTypeSpec = genFromNumSpec
2✔
1266
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1267
  fixupWithTypeSpec = fixupWithNumSpec
×
1268
  conformsTo = conformsToNumSpec
2✔
1269
  toPreds = toPredsNumSpec
2✔
1270
  cardinalTypeSpec _ = TrueSpec
×
1271
  guardTypeSpec = guardNumSpec
2✔
1272

1273
instance HasSpec Double where
×
1274
  type TypeSpec Double = NumSpec Double
1275
  emptySpec = emptyNumSpec
2✔
1276
  combineSpec = combineNumSpec
2✔
1277
  genFromTypeSpec = genFromNumSpec
2✔
1278
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1279
  fixupWithTypeSpec = fixupWithNumSpec
×
1280
  conformsTo = conformsToNumSpec
2✔
1281
  toPreds = toPredsNumSpec
2✔
1282
  cardinalTypeSpec _ = TrueSpec
×
1283
  guardTypeSpec = guardNumSpec
2✔
STATUS · Troubleshooting · Open an Issue · Sales · Support · CAREERS · ENTERPRISE · START FREE · SCHEDULE DEMO
ANNOUNCEMENTS · TWITTER · TOS & SLA · Supported CI Services · What's a CI service? · Automated Testing

© 2026 Coveralls, Inc