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

input-output-hk / constrained-generators / 315

17 Oct 2025 06:03AM UTC coverage: 73.983% (-0.7%) from 74.661%
315

push

github

web-flow
Coveralls and stack support (#44)

* Implement coveralls support

12 of 20 new or added lines in 2 files covered. (60.0%)

88 existing lines in 5 files now uncovered.

3711 of 5016 relevant lines covered (73.98%)

1.39 hits per line

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

74.61
/src/Constrained/NumOrd.hs
1
{-# LANGUAGE AllowAmbiguousTypes #-}
2
{-# LANGUAGE ConstraintKinds #-}
3
{-# LANGUAGE CPP #-}
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
  conformsToNumSpec,
43
  toPredsNumSpec,
44
  OrdLike (..),
45
  MaybeBounded (..),
46
  NumLike (..),
47
  HasDivision (..),
48
  Numeric,
49
  Number,
50
  nubOrd,
51
  IntW (..),
52
  OrdW (..),
53
) where
54

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

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

89
deriving instance Eq (OrdW ds r)
×
90

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

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

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

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

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

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

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

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

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

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

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

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

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

179
newtype Unbounded a = Unbounded a
180

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

185
instance MaybeBounded Int
2✔
186

187
instance MaybeBounded Int64
2✔
188

189
instance MaybeBounded Int32
2✔
190

191
instance MaybeBounded Int16
2✔
192

193
instance MaybeBounded Int8
2✔
194

195
instance MaybeBounded Word64
2✔
196

197
instance MaybeBounded Word32
2✔
198

199
instance MaybeBounded Word16
2✔
200

201
instance MaybeBounded Word8
2✔
202

203
deriving via Unbounded Integer instance MaybeBounded Integer
2✔
204

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

207
deriving via Unbounded Float instance MaybeBounded Float
2✔
208

209
deriving via Unbounded Double instance MaybeBounded Double
2✔
210

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

317
-- TODO: fixme
318

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

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

349
-- | Check that a value is in the spec
350
conformsToNumSpec :: Ord n => n -> NumSpec n -> Bool
351
conformsToNumSpec i (NumSpecInterval ml mu) = maybe True (<= i) ml && maybe True (i <=) mu
2✔
352

353
-- =======================================================================
354
-- Several of the methods of HasSpec that have default implementations
355
-- could benefit from type specific implementations for numbers. Those
356
-- implementations are found here
357
-- =====================================================================
358

359
-- | Strip out duplicates (in n-log(n) time, by building an intermediate Set)
360
nubOrd :: Ord a => [a] -> [a]
361
nubOrd =
2✔
362
  loop mempty
2✔
363
  where
364
    loop _ [] = []
2✔
365
    loop s (a : as)
366
      | a `Set.member` s = loop s as
1✔
367
      | otherwise =
×
368
          let s' = Set.insert a s in s' `seq` a : loop s' as
2✔
369

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

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

387
highBound :: Bounded n => Maybe n -> n
388
highBound Nothing = maxBound
2✔
389
highBound (Just n) = n
×
390

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

398
-- | The exact number of elements in a Bounded Integral type.
399
finiteSize :: forall n. (Integral n, Bounded n) => Integer
400
finiteSize = toInteger (maxBound @n) - toInteger (minBound @n) + 1
2✔
401

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

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

443
guardEmpty :: (Ord n, Num n) => Maybe n -> Maybe n -> NumSpec n -> NumSpec n
444
guardEmpty (Just a) (Just b) s
2✔
445
  | a <= b = s
2✔
446
  | otherwise = NumSpecInterval (Just 1) (Just 0)
1✔
447
guardEmpty _ _ s = s
2✔
448

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

455
subNumSpec :: (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
456
subNumSpec (NumSpecInterval x y) (NumSpecInterval a b) =
2✔
457
  guardEmpty x y $
2✔
458
    guardEmpty a b $
2✔
459
      NumSpecInterval ((-) <$> x <*> b) ((-) <$> y <*> a)
2✔
460

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

469
negNumSpec :: Num n => NumSpec n -> NumSpec n
470
negNumSpec (NumSpecInterval lo hi) = NumSpecInterval (negate <$> hi) (negate <$> lo)
2✔
471

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

481
-- ========================================================================
482
-- Helper functions for interval multiplication
483
--  (a,b) * (c,d) = (minimum s, maximum s) where s = [a * c, a * d, b * c, b * d]
484

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

494
-- \| Conversion between (T x) and (Maybe x)
495
unT :: T x -> Maybe x
496
unT (Ok x) = Just x
2✔
497
unT _ = Nothing
2✔
498

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

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

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

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

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

539
-- | Addition on `Specification` for `Number`
540
addSpecInt ::
541
  Number n =>
542
  Specification n ->
543
  Specification n ->
544
  Specification n
545
addSpecInt x y = operateSpec " + " (+) (+) x y
1✔
546

547
subSpecInt ::
548
  Number n =>
549
  Specification n ->
550
  Specification n ->
551
  Specification n
552
subSpecInt x y = operateSpec " - " (-) (-) x y
1✔
553

554
multSpecInt ::
555
  Number n =>
556
  Specification n ->
557
  Specification n ->
558
  Specification n
559
multSpecInt x y = operateSpec " * " (*) (*) x y
×
560

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

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

621
-- ===========================================================================
622

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

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

658
-- ====================================================================
659
-- Now the operations on Numbers
660

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

673
  negateSpec :: TypeSpec a -> Specification a
674
  default negateSpec ::
675
    ( NumLike (SimpleRep a)
676
    , GenericRequires a
677
    ) =>
678
    TypeSpec a ->
679
    Specification a
680
  negateSpec = fromSimpleRepSpec . negateSpec @(SimpleRep a)
×
681

682
  safeSubtract :: a -> a -> Maybe a
683
  default safeSubtract ::
684
    (HasSimpleRep a, NumLike (SimpleRep a)) =>
685
    a ->
686
    a ->
687
    Maybe a
688
  safeSubtract a b = fromSimpleRep <$> safeSubtract @(SimpleRep a) (toSimpleRep a) (toSimpleRep b)
×
689

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

705
deriving instance Eq (IntW dom rng)
×
706

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

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

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

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

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

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

749
  divideSpec 0 _ = TrueSpec
1✔
750
  divideSpec a (NumSpecInterval (unionWithMaybe max lowerBound -> ml) (unionWithMaybe min upperBound -> mu)) = typeSpec ts
2✔
751
    where
752
      ts | a > 0 = NumSpecInterval ml' mu'
2✔
753
         | otherwise = NumSpecInterval mu' ml'
1✔
754
      ml' = adjustLowerBound <$> ml
2✔
755
      mu' = adjustUpperBound <$> mu
2✔
756

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

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

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

777
instance HasDivision (Ratio Integer) where
778
  doDivide = (/)
2✔
779

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

NEW
795
      adjustUpperBound u =
×
NEW
796
        let r = u / a
×
NEW
797
            u' = r * a
×
798
        in
NEW
799
        if u < u'
×
NEW
800
        then r - (u' - u) * 2 / a
×
NEW
801
        else r
×
802

803

804
instance HasDivision Float where
805
  doDivide = (/)
2✔
806

807
  divideSpec 0 _ = TrueSpec
1✔
808
  divideSpec a (NumSpecInterval ml mu) = typeSpec ts
2✔
809
    where
810
      ts | a > 0 = NumSpecInterval ml' mu'
2✔
811
         | otherwise = NumSpecInterval mu' ml'
1✔
812
      ml' = adjustLowerBound <$> ml
2✔
813
      mu' = adjustUpperBound <$> mu
2✔
814
      adjustLowerBound l =
2✔
815
        let r = l / a
2✔
816
            l' = r * a
2✔
817
        in
818
        if l' < l
2✔
819
        then r + (l - l') * 2 / a
2✔
820
        else r
2✔
821

822
      adjustUpperBound u =
2✔
823
        let r = u / a
2✔
824
            u' = r * a
2✔
825
        in
826
        if u < u'
2✔
827
        then r - (u' - u) * 2 / a
2✔
828
        else r
2✔
829

830
instance HasDivision Double where
831
  doDivide = (/)
2✔
832

833
  divideSpec 0 _ = TrueSpec
1✔
834
  divideSpec a (NumSpecInterval ml mu) = typeSpec ts
2✔
835
    where
836
      ts | a > 0 = NumSpecInterval ml' mu'
2✔
837
         | otherwise = NumSpecInterval mu' ml'
1✔
838
      ml' = adjustLowerBound <$> ml
2✔
839
      mu' = adjustUpperBound <$> mu
2✔
840
      adjustLowerBound l =
2✔
841
        let r = l / a
2✔
842
            l' = r * a
2✔
843
        in
844
        if l' < l
2✔
845
        then r + (l - l') * 2 / a
2✔
846
        else r
2✔
847

848
      adjustUpperBound u =
2✔
849
        let r = u / a
2✔
850
            u' = r * a
2✔
851
        in
852
        if u < u'
2✔
853
        then r - (u' - u) * 2 / a
2✔
854
        else r
2✔
855

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

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

887
  negateSpec (NumSpecInterval ml mu) = typeSpec $ NumSpecInterval (negate <$> mu) (negate <$> ml)
2✔
888

889
  safeSubtract a x
2✔
890
    | a > 0
2✔
891
    , Just lb <- lowerBound
2✔
892
    , lb + a > x =
2✔
893
        Nothing
2✔
894
    | a < 0
2✔
895
    , Just ub <- upperBound
2✔
896
    , ub + a < x =
2✔
897
        Nothing
2✔
898
    | otherwise = Just $ x - a
1✔
899

900
instance NumLike a => Num (Term a) where
2✔
901
  (+) = (+.)
2✔
902
  negate = negate_
2✔
903
  fromInteger = Lit . fromInteger
2✔
904
  (*) = (*.)
2✔
905
  signum = signum_
2✔
UNCOV
906
  abs = error "No implementation for abs @(Term a)"
×
907

908
invertMult :: (HasSpec a, Num a, HasDivision a) => a -> a -> Maybe a
909
invertMult a b =
2✔
910
  let r = a `doDivide` b in if r * b == a then Just r else Nothing
2✔
911

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

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

954
  rewriteRules AddW (x :> y :> Nil) _ | x == y = Just $ 2 * x
2✔
955
  rewriteRules _ _ _ = Nothing
2✔
956

957
infix 4 +.
958

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

963
infixl 7 *.
964

965
-- | `Term`-level `(+)`
966
(*.) :: NumLike a => Term a -> Term a -> Term a
967
(*.) = appTerm MultW
2✔
968

969
-- | `Term`-level `negate`
970
negate_ :: NumLike a => Term a -> Term a
971
negate_ = appTerm NegateW
2✔
972

973
-- | `Term`-level `signum`
974
signum_ :: NumLike a => Term a -> Term a
975
signum_ = appTerm SignumW
2✔
976

977
infix 4 -.
978

979
-- | `Term`-level `(-)`
980
(-.) :: Numeric n => Term n -> Term n -> Term n
UNCOV
981
(-.) x y = x +. negate_ y
×
982

983
infixr 4 <=.
984

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

989
infixr 4 <.
990

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

995
infixr 4 >=.
996

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

1001
infixr 4 >.
1002

1003
-- | `Term`-level `(>)`
1004
(>.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
1005
(>.) = appTerm GreaterW
2✔
1006

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

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

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

1066
------------------------------------------------------------------------
1067
-- Instances of HasSpec for numeric types
1068
------------------------------------------------------------------------
1069

UNCOV
1070
instance HasSpec Integer where
×
1071
  type TypeSpec Integer = NumSpec Integer
1072
  emptySpec = emptyNumSpec
2✔
1073
  combineSpec = combineNumSpec
2✔
1074
  genFromTypeSpec = genFromNumSpec
2✔
UNCOV
1075
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1076
  conformsTo = conformsToNumSpec
2✔
1077
  toPreds = toPredsNumSpec
2✔
UNCOV
1078
  cardinalTypeSpec = cardinalNumSpec
×
1079
  guardTypeSpec = guardNumSpec
2✔
1080

UNCOV
1081
instance HasSpec Int where
×
1082
  type TypeSpec Int = NumSpec Int
1083
  emptySpec = emptyNumSpec
2✔
1084
  combineSpec = combineNumSpec
2✔
1085
  genFromTypeSpec = genFromNumSpec
2✔
UNCOV
1086
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1087
  conformsTo = conformsToNumSpec
2✔
1088
  toPreds = toPredsNumSpec
2✔
1089
  cardinalTypeSpec = cardinalNumSpec
2✔
1090
  guardTypeSpec = guardNumSpec
2✔
1091

UNCOV
1092
instance HasSpec (Ratio Integer) where
×
1093
  type TypeSpec (Ratio Integer) = NumSpec (Ratio Integer)
1094
  emptySpec = emptyNumSpec
2✔
1095
  combineSpec = combineNumSpec
2✔
1096
  genFromTypeSpec = genFromNumSpec
2✔
1097
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1098
  conformsTo = conformsToNumSpec
2✔
1099
  toPreds = toPredsNumSpec
2✔
UNCOV
1100
  cardinalTypeSpec _ = TrueSpec
×
1101
  guardTypeSpec = guardNumSpec
2✔
1102

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

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

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

UNCOV
1143
instance HasSpec Word32 where
×
1144
  type TypeSpec Word32 = NumSpec Word32
1145
  emptySpec = emptyNumSpec
2✔
1146
  combineSpec = combineNumSpec
2✔
1147
  genFromTypeSpec = genFromNumSpec
2✔
UNCOV
1148
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1149
  conformsTo = conformsToNumSpec
2✔
1150
  toPreds = toPredsNumSpec
×
UNCOV
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✔
UNCOV
1159
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1160
  conformsTo = conformsToNumSpec
2✔
1161
  toPreds = toPredsNumSpec
2✔
1162
  cardinalTypeSpec = cardinalNumSpec
2✔
1163
  guardTypeSpec = guardNumSpec
2✔
1164

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

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

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

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

1211
instance HasSpec Float where
×
1212
  type TypeSpec Float = NumSpec Float
1213
  emptySpec = emptyNumSpec
2✔
1214
  combineSpec = combineNumSpec
2✔
1215
  genFromTypeSpec = genFromNumSpec
2✔
1216
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1217
  conformsTo = conformsToNumSpec
2✔
1218
  toPreds = toPredsNumSpec
2✔
UNCOV
1219
  cardinalTypeSpec _ = TrueSpec
×
1220
  guardTypeSpec = guardNumSpec
2✔
1221

UNCOV
1222
instance HasSpec Double where
×
1223
  type TypeSpec Double = NumSpec Double
1224
  emptySpec = emptyNumSpec
2✔
1225
  combineSpec = combineNumSpec
2✔
1226
  genFromTypeSpec = genFromNumSpec
2✔
1227
  shrinkWithTypeSpec = shrinkWithNumSpec
×
1228
  conformsTo = conformsToNumSpec
2✔
1229
  toPreds = toPredsNumSpec
2✔
UNCOV
1230
  cardinalTypeSpec _ = TrueSpec
×
1231
  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