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

input-output-hk / constrained-generators / 427

21 Nov 2025 08:35AM UTC coverage: 77.476% (+1.0%) from 76.458%
427

push

github

web-flow
fourmolu (#60)

179 of 191 new or added lines in 14 files covered. (93.72%)

6 existing lines in 3 files now uncovered.

3990 of 5150 relevant lines covered (77.48%)

1.47 hits per line

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

75.55
/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
  fixupWithTypeSpec,
43
  conformsToNumSpec,
44
  toPredsNumSpec,
45
  OrdLike (..),
46
  MaybeBounded (..),
47
  NumLike (..),
48
  HasDivision (..),
49
  Numeric,
50
  Number,
51
  nubOrd,
52
  IntW (..),
53
  OrdW (..),
54
) where
55

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

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

90
deriving instance Eq (OrdW ds r)
×
91

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

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

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

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

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

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

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

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

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

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

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

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

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

180
newtype Unbounded a = Unbounded a
181

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

186
instance MaybeBounded Int
2✔
187

188
instance MaybeBounded Int64
2✔
189

190
instance MaybeBounded Int32
2✔
191

192
instance MaybeBounded Int16
2✔
193

194
instance MaybeBounded Int8
2✔
195

196
instance MaybeBounded Word64
2✔
197

198
instance MaybeBounded Word32
2✔
199

200
instance MaybeBounded Word16
2✔
201

202
instance MaybeBounded Word8
2✔
203

204
deriving via Unbounded Integer instance MaybeBounded Integer
2✔
205

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

208
deriving via Unbounded Float instance MaybeBounded Float
2✔
209

210
deriving via Unbounded Double instance MaybeBounded Double
2✔
211

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

318
-- TODO: fixme
319

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

324
-- TODO: fixme
325

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

616
-- ===========================================================================
617

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

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

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

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

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

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

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

700
deriving instance Eq (IntW dom rng)
×
701

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

708
instance Semantics IntW where
709
  semantics AddW = (+)
2✔
710
  semantics NegateW = negate
2✔
711
  semantics MultW = (*)
2✔
712
  semantics SignumW = signum
2✔
713

714
instance Syntax IntW where
2✔
715
  isInfix AddW = True
2✔
716
  isInfix NegateW = False
×
717
  isInfix MultW = True
×
718
  isInfix SignumW = False
×
719

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

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

741
instance {-# OVERLAPPABLE #-} (HasSpec a, MaybeBounded a, Integral a, TypeSpec a ~ NumSpec a) => HasDivision a where
742
  doDivide = div
2✔
743

744
  divideSpec 0 _ = TrueSpec
1✔
745
  divideSpec a (NumSpecInterval (unionWithMaybe max lowerBound -> ml) (unionWithMaybe min upperBound -> mu)) = typeSpec ts
2✔
746
    where
747
      ts
2✔
748
        | a > 0 = NumSpecInterval ml' mu'
2✔
749
        | otherwise = NumSpecInterval mu' ml'
1✔
750
      ml' = adjustLowerBound <$> ml
2✔
751
      mu' = adjustUpperBound <$> mu
2✔
752

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

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

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

773
instance HasDivision (Ratio Integer) where
774
  doDivide = (/)
2✔
775

776
  divideSpec 0 _ = TrueSpec
1✔
777
  divideSpec a (NumSpecInterval ml mu) = typeSpec ts
2✔
778
    where
779
      ts
2✔
780
        | a > 0 = NumSpecInterval ml' mu'
1✔
NEW
781
        | otherwise = NumSpecInterval mu' ml'
×
782
      ml' = adjustLowerBound <$> ml
2✔
783
      mu' = adjustUpperBound <$> mu
1✔
784
      adjustLowerBound l =
2✔
785
        let r = l / a
2✔
786
            l' = r * a
2✔
787
         in if l' < l
1✔
NEW
788
              then r + (l - l') * 2 / a
×
789
              else r
2✔
790

791
      adjustUpperBound u =
×
792
        let r = u / a
×
793
            u' = r * a
×
NEW
794
         in if u < u'
×
NEW
795
              then r - (u' - u) * 2 / a
×
NEW
796
              else r
×
797

798
instance HasDivision Float where
799
  doDivide = (/)
2✔
800

801
  divideSpec 0 _ = TrueSpec
1✔
802
  divideSpec a (NumSpecInterval ml mu) = typeSpec ts
2✔
803
    where
804
      ts
2✔
805
        | a > 0 = NumSpecInterval ml' mu'
2✔
806
        | otherwise = NumSpecInterval mu' ml'
1✔
807
      ml' = adjustLowerBound <$> ml
2✔
808
      mu' = adjustUpperBound <$> mu
2✔
809
      adjustLowerBound l =
2✔
810
        let r = l / a
2✔
811
            l' = r * a
2✔
812
         in if l' < l
2✔
813
              then r + (l - l') * 2 / a
2✔
814
              else r
2✔
815

816
      adjustUpperBound u =
2✔
817
        let r = u / a
2✔
818
            u' = r * a
2✔
819
         in if u < u'
2✔
820
              then r - (u' - u) * 2 / a
2✔
821
              else r
2✔
822

823
instance HasDivision Double where
824
  doDivide = (/)
2✔
825

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

841
      adjustUpperBound u =
2✔
842
        let r = u / a
2✔
843
            u' = r * a
2✔
844
         in if u < u'
2✔
845
              then r - (u' - u) * 2 / a
2✔
846
              else r
2✔
847

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

851
instance {-# OVERLAPPABLE #-} Numeric a => NumLike a where
852
  subtractSpec a ts@(NumSpecInterval ml mu)
2✔
853
    | Just u <- mu
2✔
854
    , a > 0
2✔
855
    , Nothing <- safeSubtract a u =
2✔
856
        ErrorSpec $
2✔
857
          NE.fromList
×
858
            [ "Underflow in subtractSpec (" ++ showType @a ++ "):"
×
859
            , "  a = " ++ show a
×
860
            , "  ts = " ++ show ts
×
861
            ]
862
    | Just l <- ml
2✔
863
    , a < 0
2✔
864
    , Nothing <- safeSubtract a l =
2✔
865
        ErrorSpec $
2✔
866
          NE.fromList
×
867
            [ "Overflow in subtractSpec (" ++ showType @a ++ "):"
×
868
            , "  a = " ++ show a
×
869
            , "  ts = " ++ show ts
×
870
            ]
871
    | otherwise = typeSpec $ NumSpecInterval (safeSub a <$> ml) (safeSub a <$> mu)
1✔
872
    where
873
      safeSub :: a -> a -> a
874
      safeSub a1 x
2✔
875
        | Just r <- safeSubtract a1 x = r
2✔
876
        | a1 < 0 = fromJust upperBound
2✔
877
        | otherwise = fromJust lowerBound
1✔
878

879
  negateSpec (NumSpecInterval ml mu) = typeSpec $ NumSpecInterval (negate <$> mu) (negate <$> ml)
2✔
880

881
  safeSubtract a x
2✔
882
    | a > 0
2✔
883
    , Just lb <- lowerBound
2✔
884
    , lb + a > x =
2✔
885
        Nothing
2✔
886
    | a < 0
2✔
887
    , Just ub <- upperBound
2✔
888
    , ub + a < x =
2✔
889
        Nothing
2✔
890
    | otherwise = Just $ x - a
1✔
891

892
instance NumLike a => Num (Term a) where
2✔
893
  (+) = (+.)
2✔
894
  negate = negate_
2✔
895
  fromInteger = Lit . fromInteger
2✔
896
  (*) = (*.)
2✔
897
  signum = signum_
2✔
898
  abs = error "No implementation for abs @(Term a)"
×
899

900
invertMult :: (HasSpec a, Num a, HasDivision a) => a -> a -> Maybe a
901
invertMult a b =
2✔
902
  let r = a `doDivide` b in if r * b == a then Just r else Nothing
2✔
903

904
-- | Just a note that these instances won't work until we are in a context where
905
--   there is a HasSpec instance of 'a', which (NumLike a) demands.
906
--   This happens in Constrained.Experiment.TheKnot
907
instance Logic IntW where
1✔
908
  propagateTypeSpec AddW (HOLE :<: i) ts cant = subtractSpec i ts <> notMemberSpec (mapMaybe (safeSubtract i) cant)
2✔
909
  propagateTypeSpec AddW ctx ts cant = propagateTypeSpec AddW (flipCtx ctx) ts cant
2✔
910
  propagateTypeSpec NegateW (Unary HOLE) ts cant = negateSpec ts <> notMemberSpec (map negate cant)
2✔
911
  propagateTypeSpec MultW (HOLE :<: 0) ts cant
912
    | 0 `conformsToSpec` TypeSpec ts cant = TrueSpec
2✔
913
    | otherwise = ErrorSpec $ NE.fromList ["zero"]
1✔
914
  propagateTypeSpec MultW (HOLE :<: i) ts cant = divideSpec i ts <> notMemberSpec (mapMaybe (flip invertMult i) cant)
2✔
915
  propagateTypeSpec MultW ctx ts cant = propagateTypeSpec MultW (flipCtx ctx) ts cant
2✔
916
  propagateTypeSpec SignumW (Unary HOLE) ts cant =
917
    constrained $ \x ->
2✔
918
      [x `satisfies` notMemberSpec [0] | not $ ok 0]
2✔
919
        ++ [Assert $ 0 <=. x | not $ ok (-1)]
2✔
920
        ++ [Assert $ x <=. 0 | not $ ok 1]
2✔
921
    where
922
      ok = flip conformsToSpec (TypeSpec ts cant)
2✔
923

924
  propagateMemberSpec AddW (HOLE :<: i) es =
2✔
925
    memberSpec
2✔
926
      (nubOrd $ mapMaybe (safeSubtract i) (NE.toList es))
2✔
927
      ( NE.fromList
×
928
          [ "propagateSpecFn on (" ++ show i ++ " +. HOLE)"
×
929
          , "The Spec is a MemberSpec = " ++ show es -- show (MemberSpec @HasSpec @TS es)
×
930
          , "We can't safely subtract " ++ show i ++ " from any choice in the MemberSpec."
×
931
          ]
932
      )
933
  propagateMemberSpec AddW ctx es = propagateMemberSpec AddW (flipCtx ctx) es
2✔
934
  propagateMemberSpec NegateW (Unary HOLE) es = MemberSpec $ NE.nub $ fmap negate es
2✔
935
  propagateMemberSpec MultW (HOLE :<: 0) es
936
    | 0 `elem` es = TrueSpec
2✔
937
    | otherwise = ErrorSpec $ NE.fromList ["zero"]
1✔
938
  propagateMemberSpec MultW (HOLE :<: i) es = memberSpec (mapMaybe (flip invertMult i) (NE.toList es)) (NE.fromList ["propagateSpec"])
1✔
939
  propagateMemberSpec MultW ctx es = propagateMemberSpec MultW (flipCtx ctx) es
2✔
940
  propagateMemberSpec SignumW (Unary HOLE) es
941
    | all ((`notElem` [-1, 0, 1]) . signum) es =
1✔
NEW
942
        ErrorSpec $ NE.fromList ["signum for invalid member spec", show es]
×
943
    | otherwise = constrained $ \x ->
1✔
944
        [x `satisfies` notMemberSpec [0] | 0 `notElem` es]
2✔
945
          ++ [Assert $ 0 <=. x | -1 `notElem` es]
2✔
946
          ++ [Assert $ x <=. 0 | 1 `notElem` es]
2✔
947

948
  rewriteRules AddW (x :> y :> Nil) _ | x == y = Just $ 2 * x
2✔
949
  rewriteRules _ _ _ = Nothing
2✔
950

951
infix 4 +.
952

953
-- | `Term`-level `(+)`
954
(+.) :: NumLike a => Term a -> Term a -> Term a
955
(+.) = appTerm AddW
2✔
956

957
infixl 7 *.
958

959
-- | `Term`-level `(+)`
960
(*.) :: NumLike a => Term a -> Term a -> Term a
961
(*.) = appTerm MultW
2✔
962

963
-- | `Term`-level `negate`
964
negate_ :: NumLike a => Term a -> Term a
965
negate_ = appTerm NegateW
2✔
966

967
-- | `Term`-level `signum`
968
signum_ :: NumLike a => Term a -> Term a
969
signum_ = appTerm SignumW
2✔
970

971
infix 4 -.
972

973
-- | `Term`-level `(-)`
974
(-.) :: Numeric n => Term n -> Term n -> Term n
975
(-.) x y = x +. negate_ y
×
976

977
infixr 4 <=.
978

979
-- | `Term`-level `(<=)`
980
(<=.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
981
(<=.) = appTerm LessOrEqualW
2✔
982

983
infixr 4 <.
984

985
-- | `Term`-level `(<)`
986
(<.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
987
(<.) = appTerm LessW
2✔
988

989
infixr 4 >=.
990

991
-- | `Term`-level `(>=)`
992
(>=.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
993
(>=.) = appTerm GreaterOrEqualW
2✔
994

995
infixr 4 >.
996

997
-- | `Term`-level `(>)`
998
(>.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
999
(>.) = appTerm GreaterW
2✔
1000

1001
-- | t`TypeSpec`-level `satisfies` to implement `toPreds` in
1002
-- `HasSpec` instance
1003
toPredsNumSpec ::
1004
  OrdLike n =>
1005
  Term n ->
1006
  NumSpec n ->
1007
  Pred
1008
toPredsNumSpec v (NumSpecInterval ml mu) =
2✔
1009
  fold $
2✔
1010
    [Assert $ Lit l <=. v | l <- maybeToList ml]
2✔
1011
      ++ [Assert $ v <=. Lit u | u <- maybeToList mu]
2✔
1012

1013
instance Logic OrdW where
×
1014
  propagate f ctxt (ExplainSpec [] s) = propagate f ctxt s
1✔
1015
  propagate f ctxt (ExplainSpec es s) = ExplainSpec es $ propagate f ctxt s
2✔
1016
  propagate _ _ TrueSpec = TrueSpec
2✔
1017
  propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs
1✔
1018
  propagate GreaterW (HOLE :? x :> Nil) spec =
1019
    propagate LessW (x :! Unary HOLE) spec
2✔
1020
  propagate GreaterW (x :! Unary HOLE) spec =
1021
    propagate LessW (HOLE :? x :> Nil) spec
2✔
1022
  propagate LessOrEqualW (HOLE :? Value x :> Nil) (SuspendedSpec v ps) =
1023
    constrained $ \v' -> Let (App LessOrEqualW (v' :> Lit x :> Nil)) (v :-> ps)
2✔
1024
  propagate LessOrEqualW (Value x :! Unary HOLE) (SuspendedSpec v ps) =
1025
    constrained $ \v' -> Let (App LessOrEqualW (Lit x :> v' :> Nil)) (v :-> ps)
2✔
1026
  propagate LessOrEqualW (HOLE :? Value l :> Nil) spec =
1027
    caseBoolSpec spec $ \case True -> leqSpec l; False -> gtSpec l
2✔
1028
  propagate LessOrEqualW (Value l :! Unary HOLE) spec =
1029
    caseBoolSpec spec $ \case True -> geqSpec l; False -> ltSpec l
2✔
1030
  propagate GreaterOrEqualW (HOLE :? Value x :> Nil) spec =
1031
    propagate LessOrEqualW (Value x :! Unary HOLE) spec
2✔
1032
  propagate GreaterOrEqualW (x :! Unary HOLE) spec =
1033
    propagate LessOrEqualW (HOLE :? x :> Nil) spec
×
1034
  propagate LessW (HOLE :? Value x :> Nil) (SuspendedSpec v ps) =
1035
    constrained $ \v' -> Let (App LessW (v' :> Lit x :> Nil)) (v :-> ps)
2✔
1036
  propagate LessW (Value x :! Unary HOLE) (SuspendedSpec v ps) =
1037
    constrained $ \v' -> Let (App LessW (Lit x :> v' :> Nil)) (v :-> ps)
2✔
1038
  propagate LessW (HOLE :? Value l :> Nil) spec =
1039
    caseBoolSpec spec $ \case True -> ltSpec l; False -> geqSpec l
2✔
1040
  propagate LessW (Value l :! Unary HOLE) spec =
1041
    caseBoolSpec spec $ \case True -> gtSpec l; False -> leqSpec l
2✔
1042

1043
-- | @if-then-else@ on a specification, useful for writing `propagate` implementations
1044
-- of predicates, e.g.:
1045
-- > propagate LessW (Value l :! Unary HOLE) spec =
1046
-- >   caseBoolSpec spec $ \case True -> gtSpec l; False -> leqSpec l
1047
caseBoolSpec ::
1048
  HasSpec a => Specification Bool -> (Bool -> Specification a) -> Specification a
1049
caseBoolSpec spec cont = case possibleValues spec of
2✔
1050
  [] -> ErrorSpec (NE.fromList ["No possible values in caseBoolSpec"])
1✔
1051
  [b] -> cont b
2✔
1052
  _ -> mempty
2✔
1053
  where
1054
    -- This will always get the same result, and probably faster since running 2
1055
    -- conformsToSpec on True and False takes less time than simplifying the spec.
1056
    -- Since we are in TheKnot, we could keep the simplifySpec. Is there a good reason to?
1057
    possibleValues s = filter (flip conformsToSpec s) [True, False]
2✔
1058

1059
------------------------------------------------------------------------
1060
-- Instances of HasSpec for numeric types
1061
------------------------------------------------------------------------
1062

1063
instance HasSpec Integer where
×
1064
  type TypeSpec Integer = NumSpec Integer
1065
  emptySpec = emptyNumSpec
2✔
1066
  combineSpec = combineNumSpec
2✔
1067
  genFromTypeSpec = genFromNumSpec
2✔
1068
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1069
  fixupWithTypeSpec = fixupWithNumSpec
×
1070
  conformsTo = conformsToNumSpec
2✔
1071
  toPreds = toPredsNumSpec
2✔
1072
  cardinalTypeSpec = cardinalNumSpec
×
1073
  guardTypeSpec = guardNumSpec
2✔
1074

1075
instance HasSpec Int where
×
1076
  type TypeSpec Int = NumSpec Int
1077
  emptySpec = emptyNumSpec
2✔
1078
  combineSpec = combineNumSpec
2✔
1079
  genFromTypeSpec = genFromNumSpec
2✔
1080
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1081
  fixupWithTypeSpec = fixupWithNumSpec
2✔
1082
  conformsTo = conformsToNumSpec
2✔
1083
  toPreds = toPredsNumSpec
2✔
1084
  cardinalTypeSpec = cardinalNumSpec
2✔
1085
  guardTypeSpec = guardNumSpec
2✔
1086

1087
instance HasSpec (Ratio Integer) where
×
1088
  type TypeSpec (Ratio Integer) = NumSpec (Ratio Integer)
1089
  emptySpec = emptyNumSpec
2✔
1090
  combineSpec = combineNumSpec
2✔
1091
  genFromTypeSpec = genFromNumSpec
2✔
1092
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1093
  fixupWithTypeSpec = fixupWithNumSpec
×
1094
  conformsTo = conformsToNumSpec
2✔
1095
  toPreds = toPredsNumSpec
2✔
1096
  cardinalTypeSpec _ = TrueSpec
×
1097
  guardTypeSpec = guardNumSpec
2✔
1098

1099
instance HasSpec Natural where
×
1100
  type TypeSpec Natural = NumSpec Natural
1101
  emptySpec = emptyNumSpec
2✔
1102
  combineSpec = combineNumSpec
2✔
1103
  genFromTypeSpec = genFromNumSpec
2✔
1104
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1105
  fixupWithTypeSpec = fixupWithNumSpec
×
1106
  conformsTo = conformsToNumSpec
2✔
1107
  toPreds = toPredsNumSpec
×
1108
  cardinalTypeSpec (NumSpecInterval (fromMaybe 0 -> lo) (Just hi)) =
×
1109
    if lo < hi
×
1110
      then equalSpec (fromIntegral $ hi - lo + 1)
×
1111
      else equalSpec 0
×
1112
  cardinalTypeSpec _ = TrueSpec
×
1113
  guardTypeSpec = guardNumSpec
2✔
1114

1115
instance HasSpec Word8 where
×
1116
  type TypeSpec Word8 = NumSpec Word8
1117
  emptySpec = emptyNumSpec
2✔
1118
  combineSpec = combineNumSpec
2✔
1119
  genFromTypeSpec = genFromNumSpec
2✔
1120
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1121
  fixupWithTypeSpec = fixupWithNumSpec
×
1122
  conformsTo = conformsToNumSpec
2✔
1123
  toPreds = toPredsNumSpec
2✔
1124
  cardinalTypeSpec = cardinalNumSpec
×
1125
  cardinalTrueSpec = equalSpec 256
×
1126
  typeSpecOpt = notInNumSpec
2✔
1127
  guardTypeSpec = guardNumSpec
2✔
1128

1129
instance HasSpec Word16 where
×
1130
  type TypeSpec Word16 = NumSpec Word16
1131
  emptySpec = emptyNumSpec
2✔
1132
  combineSpec = combineNumSpec
2✔
1133
  genFromTypeSpec = genFromNumSpec
2✔
1134
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1135
  fixupWithTypeSpec = fixupWithNumSpec
×
1136
  conformsTo = conformsToNumSpec
2✔
1137
  toPreds = toPredsNumSpec
×
1138
  cardinalTypeSpec = cardinalNumSpec
×
1139
  cardinalTrueSpec = equalSpec 65536
×
1140
  guardTypeSpec = guardNumSpec
2✔
1141

1142
instance HasSpec Word32 where
×
1143
  type TypeSpec Word32 = NumSpec Word32
1144
  emptySpec = emptyNumSpec
2✔
1145
  combineSpec = combineNumSpec
2✔
1146
  genFromTypeSpec = genFromNumSpec
2✔
1147
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1148
  fixupWithTypeSpec = fixupWithNumSpec
×
1149
  conformsTo = conformsToNumSpec
2✔
1150
  toPreds = toPredsNumSpec
×
1151
  cardinalTypeSpec = cardinalNumSpec
×
1152
  guardTypeSpec = guardNumSpec
2✔
1153

1154
instance HasSpec Word64 where
×
1155
  type TypeSpec Word64 = NumSpec Word64
1156
  emptySpec = emptyNumSpec
2✔
1157
  combineSpec = combineNumSpec
2✔
1158
  genFromTypeSpec = genFromNumSpec
2✔
1159
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1160
  fixupWithTypeSpec = fixupWithNumSpec
×
1161
  conformsTo = conformsToNumSpec
2✔
1162
  toPreds = toPredsNumSpec
2✔
1163
  cardinalTypeSpec = cardinalNumSpec
2✔
1164
  guardTypeSpec = guardNumSpec
2✔
1165

1166
instance HasSpec Int8 where
×
1167
  type TypeSpec Int8 = NumSpec Int8
1168
  emptySpec = emptyNumSpec
2✔
1169
  combineSpec = combineNumSpec
2✔
1170
  genFromTypeSpec = genFromNumSpec
2✔
1171
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1172
  fixupWithTypeSpec = fixupWithNumSpec
×
1173
  conformsTo = conformsToNumSpec
2✔
1174
  toPreds = toPredsNumSpec
2✔
1175
  cardinalTrueSpec = equalSpec 256
×
1176
  cardinalTypeSpec = cardinalNumSpec
×
1177
  guardTypeSpec = guardNumSpec
2✔
1178

1179
instance HasSpec Int16 where
×
1180
  type TypeSpec Int16 = NumSpec Int16
1181
  emptySpec = emptyNumSpec
2✔
1182
  combineSpec = combineNumSpec
2✔
1183
  genFromTypeSpec = genFromNumSpec
2✔
1184
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1185
  fixupWithTypeSpec = fixupWithNumSpec
×
1186
  conformsTo = conformsToNumSpec
2✔
1187
  toPreds = toPredsNumSpec
×
1188
  cardinalTypeSpec = cardinalNumSpec
×
1189
  cardinalTrueSpec = equalSpec 65536
×
1190
  guardTypeSpec = guardNumSpec
2✔
1191

1192
instance HasSpec Int32 where
×
1193
  type TypeSpec Int32 = NumSpec Int32
1194
  emptySpec = emptyNumSpec
2✔
1195
  combineSpec = combineNumSpec
2✔
1196
  genFromTypeSpec = genFromNumSpec
2✔
1197
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1198
  fixupWithTypeSpec = fixupWithNumSpec
×
1199
  conformsTo = conformsToNumSpec
2✔
1200
  toPreds = toPredsNumSpec
×
1201
  cardinalTypeSpec = cardinalNumSpec
×
1202
  guardTypeSpec = guardNumSpec
2✔
1203

1204
instance HasSpec Int64 where
×
1205
  type TypeSpec Int64 = NumSpec Int64
1206
  emptySpec = emptyNumSpec
2✔
1207
  combineSpec = combineNumSpec
2✔
1208
  genFromTypeSpec = genFromNumSpec
2✔
1209
  shrinkWithTypeSpec = shrinkWithNumSpec
2✔
1210
  fixupWithTypeSpec = fixupWithNumSpec
×
1211
  conformsTo = conformsToNumSpec
2✔
1212
  toPreds = toPredsNumSpec
×
1213
  cardinalTypeSpec = cardinalNumSpec
×
1214
  guardTypeSpec = guardNumSpec
2✔
1215

1216
instance HasSpec Float where
×
1217
  type TypeSpec Float = NumSpec Float
1218
  emptySpec = emptyNumSpec
2✔
1219
  combineSpec = combineNumSpec
2✔
1220
  genFromTypeSpec = genFromNumSpec
2✔
1221
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1222
  fixupWithTypeSpec = fixupWithNumSpec
×
1223
  conformsTo = conformsToNumSpec
2✔
1224
  toPreds = toPredsNumSpec
2✔
1225
  cardinalTypeSpec _ = TrueSpec
×
1226
  guardTypeSpec = guardNumSpec
2✔
1227

1228
instance HasSpec Double where
×
1229
  type TypeSpec Double = NumSpec Double
1230
  emptySpec = emptyNumSpec
2✔
1231
  combineSpec = combineNumSpec
2✔
1232
  genFromTypeSpec = genFromNumSpec
2✔
1233
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1234
  fixupWithTypeSpec = fixupWithNumSpec
×
1235
  conformsTo = conformsToNumSpec
2✔
1236
  toPreds = toPredsNumSpec
2✔
1237
  cardinalTypeSpec _ = TrueSpec
×
1238
  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