{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
-- Random Natural, Arbitrary Natural, Uniform Natural
{-# OPTIONS_GHC -Wno-orphans #-}

module Constrained.NumOrd where

import Constrained.AbstractSyntax
import Constrained.Base (
  GenericRequires,
  HOLE (..),
  HasSpec (..),
  Logic (..),
  Pred,
  Specification,
  Term,
  appTerm,
  constrained,
  equalSpec,
  explainSpecOpt,
  flipCtx,
  fromSimpleRepSpec,
  memberSpecList,
  notMemberSpec,
  typeSpec,
  pattern TypeSpec,
  pattern Unary,
  pattern (:<:),
 )
import Constrained.Conformance
import Constrained.Conformance ()
import Constrained.Core (Value (..), unionWithMaybe)
import Constrained.FunctionSymbol
import Constrained.GenT (
  GenT,
  MonadGenError (..),
  genError,
  pureGen,
  sizeT,
 )
import Constrained.Generic (
  HasSimpleRep (..),
  SimpleRep,
 )
import Constrained.List
import Constrained.PrettyUtils
import Control.Applicative ((<|>))
import Control.Arrow (first)
import Data.Foldable
import Data.Kind
import Data.List (nub)
import Data.List.NonEmpty (NonEmpty ((:|)))
import qualified Data.List.NonEmpty as NE
import Data.Maybe
import qualified Data.Set as Set
import Data.Typeable (typeOf)
import Data.Word
import GHC.Int
import GHC.Natural
import GHC.Real
import System.Random.Stateful (Random (..), Uniform (..))
import Test.QuickCheck (Arbitrary (arbitrary, shrink), choose, frequency)

-- ====================================================================
-- OrdW  witnesses for comparison operations (<=. and <. and <=. and >=.) on numbers
-- The other operations are defined in terms of these. These things
-- will eventually get Logic instances
-- =====================================================================

data OrdW (dom :: [Type]) (rng :: Type) where
  LessOrEqualW :: OrdLike a => OrdW '[a, a] Bool
  LessW :: OrdLike a => OrdW '[a, a] Bool
  GreaterOrEqualW :: OrdLike a => OrdW '[a, a] Bool
  GreaterW :: OrdLike a => OrdW '[a, a] Bool

deriving instance Eq (OrdW ds r)

instance Show (OrdW ds r) where
  show :: OrdW ds r -> String
show OrdW ds r
LessOrEqualW = String
"<=."
  show OrdW ds r
LessW = String
"<."
  show OrdW ds r
GreaterOrEqualW = String
">=."
  show OrdW ds r
GreaterW = String
">."

instance Semantics OrdW where
  semantics :: forall (d :: [*]) r. OrdW d r -> FunTy d r
semantics OrdW d r
LessOrEqualW = FunTy d r
a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
  semantics OrdW d r
LessW = FunTy d r
a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<)
  semantics OrdW d r
GreaterW = FunTy d r
a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>)
  semantics OrdW d r
GreaterOrEqualW = FunTy d r
a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>=)

instance Syntax OrdW where
  isInfix :: forall (dom :: [*]) rng. OrdW dom rng -> Bool
isInfix OrdW dom rng
_ = Bool
True

-- =============================================
-- OrdLike. Ord for Numbers in the Logic
-- =============================================

class (Ord a, HasSpec a) => OrdLike a where
  leqSpec :: a -> Specification a
  default leqSpec ::
    ( GenericRequires a
    , OrdLike (SimpleRep a)
    ) =>
    a ->
    Specification a
  leqSpec = Specification (SimpleRep a) -> Specification a
forall a.
GenericRequires a =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec (Specification (SimpleRep a) -> Specification a)
-> (a -> Specification (SimpleRep a)) -> a -> Specification a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleRep a -> Specification (SimpleRep a)
forall a. OrdLike a => a -> Specification a
leqSpec (SimpleRep a -> Specification (SimpleRep a))
-> (a -> SimpleRep a) -> a -> Specification (SimpleRep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SimpleRep a
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep

  ltSpec :: a -> Specification a
  default ltSpec ::
    ( OrdLike (SimpleRep a)
    , GenericRequires a
    ) =>
    a ->
    Specification a
  ltSpec = Specification (SimpleRep a) -> Specification a
forall a.
GenericRequires a =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec (Specification (SimpleRep a) -> Specification a)
-> (a -> Specification (SimpleRep a)) -> a -> Specification a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleRep a -> Specification (SimpleRep a)
forall a. OrdLike a => a -> Specification a
ltSpec (SimpleRep a -> Specification (SimpleRep a))
-> (a -> SimpleRep a) -> a -> Specification (SimpleRep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SimpleRep a
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep

  geqSpec :: a -> Specification a
  default geqSpec ::
    ( OrdLike (SimpleRep a)
    , GenericRequires a
    ) =>
    a ->
    Specification a
  geqSpec = Specification (SimpleRep a) -> Specification a
forall a.
GenericRequires a =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec (Specification (SimpleRep a) -> Specification a)
-> (a -> Specification (SimpleRep a)) -> a -> Specification a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleRep a -> Specification (SimpleRep a)
forall a. OrdLike a => a -> Specification a
geqSpec (SimpleRep a -> Specification (SimpleRep a))
-> (a -> SimpleRep a) -> a -> Specification (SimpleRep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SimpleRep a
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep

  gtSpec :: a -> Specification a
  default gtSpec ::
    ( OrdLike (SimpleRep a)
    , GenericRequires a
    ) =>
    a ->
    Specification a
  gtSpec = Specification (SimpleRep a) -> Specification a
forall a.
GenericRequires a =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec (Specification (SimpleRep a) -> Specification a)
-> (a -> Specification (SimpleRep a)) -> a -> Specification a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleRep a -> Specification (SimpleRep a)
forall a. OrdLike a => a -> Specification a
gtSpec (SimpleRep a -> Specification (SimpleRep a))
-> (a -> SimpleRep a) -> a -> Specification (SimpleRep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SimpleRep a
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep

-- | This instance should be general enough for every type of Number that has a NumSpec as its TypeSpec
instance {-# OVERLAPPABLE #-} (Ord a, HasSpec a, MaybeBounded a, Num a, TypeSpec a ~ NumSpec a) => OrdLike a where
  leqSpec :: a -> Specification a
leqSpec a
l = TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval Maybe a
forall a. Maybe a
Nothing (a -> Maybe a
forall a. a -> Maybe a
Just a
l)
  ltSpec :: a -> Specification a
ltSpec a
l
    | Just a
b <- Maybe a
forall a. MaybeBounded a => Maybe a
lowerBound
    , a
l a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b =
        NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"ltSpec @" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf a
l) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
l))
    | Bool
otherwise = TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval Maybe a
forall a. Maybe a
Nothing (a -> Maybe a
forall a. a -> Maybe a
Just (a
l a -> a -> a
forall a. Num a => a -> a -> a
- a
1))
  geqSpec :: a -> Specification a
geqSpec a
l = TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (a -> Maybe a
forall a. a -> Maybe a
Just a
l) Maybe a
forall a. Maybe a
Nothing
  gtSpec :: a -> Specification a
gtSpec a
l
    | Just a
b <- Maybe a
forall a. MaybeBounded a => Maybe a
upperBound
    , a
l a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b =
        NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"gtSpec @" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf a
l) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
l))
    | Bool
otherwise = TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (a -> Maybe a
forall a. a -> Maybe a
Just (a
l a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)) Maybe a
forall a. Maybe a
Nothing

-- ========================================================================
-- helper functions for the TypeSpec for Numbers
-- ========================================================================

class MaybeBounded a where
  lowerBound :: Maybe a
  upperBound :: Maybe a

  default lowerBound :: Bounded a => Maybe a
  lowerBound = a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. Bounded a => a
minBound

  default upperBound :: Bounded a => Maybe a
  upperBound = a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. Bounded a => a
maxBound

newtype Unbounded a = Unbounded a

instance MaybeBounded (Unbounded a) where
  lowerBound :: Maybe (Unbounded a)
lowerBound = Maybe (Unbounded a)
forall a. Maybe a
Nothing
  upperBound :: Maybe (Unbounded a)
upperBound = Maybe (Unbounded a)
forall a. Maybe a
Nothing

instance MaybeBounded Int

instance MaybeBounded Int64

instance MaybeBounded Int32

instance MaybeBounded Int16

instance MaybeBounded Int8

instance MaybeBounded Word64

instance MaybeBounded Word32

instance MaybeBounded Word16

instance MaybeBounded Word8

deriving via Unbounded Integer instance MaybeBounded Integer

deriving via Unbounded (Ratio Integer) instance MaybeBounded (Ratio Integer)

deriving via Unbounded Float instance MaybeBounded Float

instance MaybeBounded Natural where
  lowerBound :: Maybe Natural
lowerBound = Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
0
  upperBound :: Maybe Natural
upperBound = Maybe Natural
forall a. Maybe a
Nothing

-- ===================================================================
-- The TypeSpec for numbers
-- ===================================================================

data NumSpec n = NumSpecInterval (Maybe n) (Maybe n)

instance Ord n => Eq (NumSpec n) where
  NumSpecInterval Maybe n
ml Maybe n
mh == :: NumSpec n -> NumSpec n -> Bool
== NumSpecInterval Maybe n
ml' Maybe n
mh'
    | Maybe n -> Maybe n -> Bool
forall {a}. Ord a => Maybe a -> Maybe a -> Bool
isEmpty Maybe n
ml Maybe n
mh = Maybe n -> Maybe n -> Bool
forall {a}. Ord a => Maybe a -> Maybe a -> Bool
isEmpty Maybe n
ml' Maybe n
mh'
    | Maybe n -> Maybe n -> Bool
forall {a}. Ord a => Maybe a -> Maybe a -> Bool
isEmpty Maybe n
ml' Maybe n
mh' = Maybe n -> Maybe n -> Bool
forall {a}. Ord a => Maybe a -> Maybe a -> Bool
isEmpty Maybe n
ml Maybe n
mh
    | Bool
otherwise = Maybe n
ml Maybe n -> Maybe n -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe n
ml' Bool -> Bool -> Bool
&& Maybe n
mh Maybe n -> Maybe n -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe n
mh'
    where
      isEmpty :: Maybe a -> Maybe a -> Bool
isEmpty (Just a
a) (Just a
b) = a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
b
      isEmpty Maybe a
_ Maybe a
_ = Bool
False

instance Show n => Show (NumSpec n) where
  show :: NumSpec n -> String
show (NumSpecInterval Maybe n
ml Maybe n
mu) = String
lb String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ub
    where
      lb :: String
lb = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (n -> String) -> Maybe n -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" n -> String
forall a. Show a => a -> String
show Maybe n
ml
      ub :: String
ub = String -> (n -> String) -> Maybe n -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" n -> String
forall a. Show a => a -> String
show Maybe n
mu String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

instance Ord n => Semigroup (NumSpec n) where
  NumSpecInterval Maybe n
ml Maybe n
mu <> :: NumSpec n -> NumSpec n -> NumSpec n
<> NumSpecInterval Maybe n
ml' Maybe n
mu' =
    Maybe n -> Maybe n -> NumSpec n
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval
      ((n -> n -> n) -> Maybe n -> Maybe n -> Maybe n
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe n -> n -> n
forall a. Ord a => a -> a -> a
max Maybe n
ml Maybe n
ml')
      ((n -> n -> n) -> Maybe n -> Maybe n -> Maybe n
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe n -> n -> n
forall a. Ord a => a -> a -> a
min Maybe n
mu Maybe n
mu')

instance Ord n => Monoid (NumSpec n) where
  mempty :: NumSpec n
mempty = Maybe n -> Maybe n -> NumSpec n
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval Maybe n
forall a. Maybe a
Nothing Maybe n
forall a. Maybe a
Nothing

-- ===========================================
-- Arbitrary for Num like things
-- ===========================================

instance (Arbitrary a, Ord a) => Arbitrary (NumSpec a) where
  arbitrary :: Gen (NumSpec a)
arbitrary = do
    Maybe a
m <- Gen (Maybe a)
forall a. Arbitrary a => Gen a
arbitrary
    Maybe a
m' <- Gen (Maybe a)
forall a. Arbitrary a => Gen a
arbitrary
    [(Int, Gen (NumSpec a))] -> Gen (NumSpec a)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
10, NumSpec a -> Gen (NumSpec a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NumSpec a -> Gen (NumSpec a)) -> NumSpec a -> Gen (NumSpec a)
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe a -> NumSpec a
forall {n}. Ord n => Maybe n -> Maybe n -> NumSpec n
mkLoHiInterval Maybe a
m Maybe a
m'), (Int
1, NumSpec a -> Gen (NumSpec a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NumSpec a -> Gen (NumSpec a)) -> NumSpec a -> Gen (NumSpec a)
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval Maybe a
m Maybe a
m')]
    where
      mkLoHiInterval :: Maybe n -> Maybe n -> NumSpec n
mkLoHiInterval (Just n
a) (Just n
b) = Maybe n -> Maybe n -> NumSpec n
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (n -> Maybe n
forall a. a -> Maybe a
Just (n -> Maybe n) -> n -> Maybe n
forall a b. (a -> b) -> a -> b
$ n -> n -> n
forall a. Ord a => a -> a -> a
min n
a n
b) (n -> Maybe n
forall a. a -> Maybe a
Just (n -> Maybe n) -> n -> Maybe n
forall a b. (a -> b) -> a -> b
$ n -> n -> n
forall a. Ord a => a -> a -> a
max n
a n
b)
      mkLoHiInterval Maybe n
m Maybe n
m' = Maybe n -> Maybe n -> NumSpec n
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval Maybe n
m Maybe n
m'
  shrink :: NumSpec a -> [NumSpec a]
shrink (NumSpecInterval Maybe a
m Maybe a
m') =
    (Maybe a -> Maybe a -> NumSpec a)
-> (Maybe a, Maybe a) -> NumSpec a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval ((Maybe a, Maybe a) -> NumSpec a)
-> [(Maybe a, Maybe a)] -> [NumSpec a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe a, Maybe a) -> [(Maybe a, Maybe a)]
forall a. Arbitrary a => a -> [a]
shrink (Maybe a
m, Maybe a
m')

instance Arbitrary Natural where
  arbitrary :: Gen Natural
arbitrary = Word -> Natural
wordToNatural (Word -> Natural) -> (Word -> Word) -> Word -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> Word
forall a. Num a => a -> a
abs (Word -> Natural) -> Gen Word -> Gen Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: Natural -> [Natural]
shrink Natural
n = [Word -> Natural
wordToNatural Word
w | Word
w <- Word -> [Word]
forall a. Arbitrary a => a -> [a]
shrink (Natural -> Word
naturalToWord Natural
n)]

instance Uniform Natural where
  uniformM :: forall g (m :: * -> *). StatefulGen g m => g -> m Natural
uniformM g
g = Word -> Natural
wordToNatural (Word -> Natural) -> (Word -> Word) -> Word -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> Word
forall a. Num a => a -> a
abs (Word -> Natural) -> m Word -> m Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g -> m Word
forall a g (m :: * -> *). (Uniform a, StatefulGen g m) => g -> m a
forall g (m :: * -> *). StatefulGen g m => g -> m Word
uniformM g
g

instance Random Natural where
  randomR :: forall g. RandomGen g => (Natural, Natural) -> g -> (Natural, g)
randomR (Natural
lo, Natural
hi) g
g = (Integer -> Natural) -> (Integer, g) -> (Natural, g)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ((Integer, g) -> (Natural, g)) -> (Integer, g) -> (Natural, g)
forall a b. (a -> b) -> a -> b
$ (Integer, Integer) -> g -> (Integer, g)
forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
lo, Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
hi) g
g

instance Random (Ratio Integer) where
  randomR :: forall g.
RandomGen g =>
(Ratio Integer, Ratio Integer) -> g -> (Ratio Integer, g)
randomR (Ratio Integer
lo, Ratio Integer
hi) g
g =
    let (Ratio Integer
r, g
g') = g -> (Ratio Integer, g)
forall g. RandomGen g => g -> (Ratio Integer, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
     in (Ratio Integer
lo Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Num a => a -> a -> a
+ (Ratio Integer
hi Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Num a => a -> a -> a
- Ratio Integer
lo) Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Num a => a -> a -> a
* Ratio Integer
r, g
g')
  random :: forall g. RandomGen g => g -> (Ratio Integer, g)
random g
g =
    let (Integer
d, g
g') = (Integer -> Integer) -> (Integer, g) -> (Integer, g)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
abs) ((Integer, g) -> (Integer, g)) -> (Integer, g) -> (Integer, g)
forall a b. (a -> b) -> a -> b
$ g -> (Integer, g)
forall g. RandomGen g => g -> (Integer, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
        (Integer
n, g
g'') = (Integer, Integer) -> g -> (Integer, g)
forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0, Integer
d) g
g'
     in (Integer
n Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
d, g
g'')

-- ==============================================================================
-- Operations on NumSpec, that give it the required properties of a TypeSpec
-- ==============================================================================

emptyNumSpec :: Ord a => NumSpec a
emptyNumSpec :: forall n. Ord n => NumSpec n
emptyNumSpec = NumSpec a
forall a. Monoid a => a
mempty

guardNumSpec ::
  (Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
  [String] ->
  NumSpec n ->
  Specification n
guardNumSpec :: forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec [String]
msg s :: NumSpec n
s@(NumSpecInterval (Just n
a) (Just n
b))
  | n
a n -> n -> Bool
forall a. Ord a => a -> a -> Bool
> n
b = NonEmpty String -> SpecificationD Deps n
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (String
"NumSpec has low bound greater than hi bound" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| ((String
"   " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NumSpec n -> String
forall a. Show a => a -> String
show NumSpec n
s) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
msg))
  | n
a n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
b = n -> SpecificationD Deps n
forall a. a -> Specification a
equalSpec n
a
guardNumSpec [String]
_ NumSpec n
s = TypeSpec n -> SpecificationD Deps n
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec TypeSpec n
NumSpec n
s

combineNumSpec ::
  (HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
  NumSpec n ->
  NumSpec n ->
  Specification n
combineNumSpec :: forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec NumSpec n
s NumSpec n
s' = [String] -> NumSpec n -> Specification n
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec [String
"when combining two NumSpecs", String
"   " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NumSpec n -> String
forall a. Show a => a -> String
show NumSpec n
s, String
"   " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NumSpec n -> String
forall a. Show a => a -> String
show NumSpec n
s'] (NumSpec n
s NumSpec n -> NumSpec n -> NumSpec n
forall a. Semigroup a => a -> a -> a
<> NumSpec n
s')

genFromNumSpec ::
  (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) =>
  NumSpec n ->
  GenT m n
genFromNumSpec :: forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec (NumSpecInterval Maybe n
ml Maybe n
mu) = do
  Int
n <- GenT m Int
forall (m :: * -> *). Monad m => GenT m Int
sizeT
  Gen n -> GenT m n
forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (Gen n -> GenT m n) -> ((n, n) -> Gen n) -> (n, n) -> GenT m n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n, n) -> Gen n
forall a. Random a => (a, a) -> Gen a
choose ((n, n) -> GenT m n) -> GenT m (n, n) -> GenT m n
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe n -> Maybe n -> Integer -> GenT m (n, n)
forall (m :: * -> *) a.
(MonadGenError m, Ord a, Num a, Show a) =>
Maybe a -> Maybe a -> Integer -> m (a, a)
constrainInterval (Maybe n
ml Maybe n -> Maybe n -> Maybe n
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe n
forall a. MaybeBounded a => Maybe a
lowerBound) (Maybe n
mu Maybe n -> Maybe n -> Maybe n
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe n
forall a. MaybeBounded a => Maybe a
upperBound) (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)

-- TODO: fixme (?)
shrinkWithNumSpec :: Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec :: forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec NumSpec n
_ = n -> [n]
forall a. Arbitrary a => a -> [a]
shrink

constrainInterval ::
  (MonadGenError m, Ord a, Num a, Show a) => Maybe a -> Maybe a -> Integer -> m (a, a)
constrainInterval :: forall (m :: * -> *) a.
(MonadGenError m, Ord a, Num a, Show a) =>
Maybe a -> Maybe a -> Integer -> m (a, a)
constrainInterval Maybe a
ml Maybe a
mu Integer
r =
  case (Maybe a
ml, Maybe a
mu) of
    (Maybe a
Nothing, Maybe a
Nothing) -> (a, a) -> m (a, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (-a
r', a
r')
    (Just a
l, Maybe a
Nothing)
      | a
l a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 -> (a, a) -> m (a, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> a -> a
forall a. Ord a => a -> a -> a
max a
l (a -> a
forall a. Num a => a -> a
negate a
r'), a
r')
      | Bool
otherwise -> (a, a) -> m (a, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
l, a
l a -> a -> a
forall a. Num a => a -> a -> a
+ a
2 a -> a -> a
forall a. Num a => a -> a -> a
* a
r')
    (Maybe a
Nothing, Just a
u)
      | a
u a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 -> (a, a) -> m (a, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> a
forall a. Num a => a -> a
negate a
r', a -> a -> a
forall a. Ord a => a -> a -> a
min a
u a
r')
      | Bool
otherwise -> (a, a) -> m (a, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
u a -> a -> a
forall a. Num a => a -> a -> a
- a
r' a -> a -> a
forall a. Num a => a -> a -> a
- a
r', a
u)
    (Just a
l, Just a
u)
      | a
l a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
u -> String -> m (a, a)
forall (m :: * -> *) a. MonadGenError m => String -> m a
genError (String
"bad interval: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
u)
      | a
u a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 -> (a, a) -> m (a, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> a -> a -> a
forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeSub a
l (a -> a -> a -> a
forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeSub a
l a
u a
r') a
r', a
u)
      | a
l a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 -> (a, a) -> m (a, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
l, a -> a -> a -> a
forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeAdd a
u (a -> a -> a -> a
forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeAdd a
u a
l a
r') a
r')
      -- TODO: this is a bit suspect if the bounds are lopsided
      | Bool
otherwise -> (a, a) -> m (a, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> a -> a
forall a. Ord a => a -> a -> a
max a
l (-a
r'), a -> a -> a
forall a. Ord a => a -> a -> a
min a
u a
r')
  where
    r' :: a
r' = a -> a
forall a. Num a => a -> a
abs (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Integer -> a
forall a. Num a => Integer -> a
fromInteger Integer
r
    safeSub :: p -> p -> p -> p
safeSub p
l p
a p
b
      | p
a p -> p -> p
forall a. Num a => a -> a -> a
- p
b p -> p -> Bool
forall a. Ord a => a -> a -> Bool
> p
a = p
l
      | Bool
otherwise = p -> p -> p
forall a. Ord a => a -> a -> a
max p
l (p
a p -> p -> p
forall a. Num a => a -> a -> a
- p
b)
    safeAdd :: p -> p -> p -> p
safeAdd p
u p
a p
b
      | p
a p -> p -> p
forall a. Num a => a -> a -> a
+ p
b p -> p -> Bool
forall a. Ord a => a -> a -> Bool
< p
a = p
u
      | Bool
otherwise = p -> p -> p
forall a. Ord a => a -> a -> a
min p
u (p
a p -> p -> p
forall a. Num a => a -> a -> a
+ p
b)

conformsToNumSpec :: Ord n => n -> NumSpec n -> Bool
conformsToNumSpec :: forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec n
i (NumSpecInterval Maybe n
ml Maybe n
mu) = Bool -> (n -> Bool) -> Maybe n -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<= n
i) Maybe n
ml Bool -> Bool -> Bool
&& Bool -> (n -> Bool) -> Maybe n -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (n
i n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<=) Maybe n
mu

-- =======================================================================
-- Several of the methods of HasSpec that have default implementations
-- could benefit from type specific implementations for numbers. Those
-- implementations are found here
-- =====================================================================

-- | Strip out duplicates (in n-log(n) time, by building an intermediate Set)
nubOrd :: Ord a => [a] -> [a]
nubOrd :: forall a. Ord a => [a] -> [a]
nubOrd =
  Set a -> [a] -> [a]
forall {a}. Ord a => Set a -> [a] -> [a]
loop Set a
forall a. Monoid a => a
mempty
  where
    loop :: Set a -> [a] -> [a]
loop Set a
_ [] = []
    loop Set a
s (a
a : [a]
as)
      | a
a a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set a
s = Set a -> [a] -> [a]
loop Set a
s [a]
as
      | Bool
otherwise =
          let s' :: Set a
s' = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
a Set a
s in Set a
s' Set a -> [a] -> [a]
forall a b. a -> b -> b
`seq` a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Set a -> [a] -> [a]
loop Set a
s' [a]
as

-- | Builds a MemberSpec, but returns an Error spec if the list is empty
nubOrdMemberSpec :: Ord a => String -> [a] -> Specification a
nubOrdMemberSpec :: forall a. Ord a => String -> [a] -> Specification a
nubOrdMemberSpec String
message [a]
xs =
  [a] -> NonEmpty String -> Specification a
forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
    ([a] -> [a]
forall a. Ord a => [a] -> [a]
nubOrd [a]
xs)
    ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
        [ String
"In call to nubOrdMemberSpec"
        , String
"Called from context"
        , String
message
        , String
"The input is the empty list."
        ]
    )

lowBound :: Bounded n => Maybe n -> n
lowBound :: forall n. Bounded n => Maybe n -> n
lowBound Maybe n
Nothing = n
forall a. Bounded a => a
minBound
lowBound (Just n
n) = n
n

highBound :: Bounded n => Maybe n -> n
highBound :: forall n. Bounded n => Maybe n -> n
highBound Maybe n
Nothing = n
forall a. Bounded a => a
maxBound
highBound (Just n
n) = n
n

-- | The exact count of the number elements in a Bounded NumSpec
countSpec :: forall n. (Bounded n, Integral n) => NumSpec n -> Integer
countSpec :: forall n. (Bounded n, Integral n) => NumSpec n -> Integer
countSpec (NumSpecInterval Maybe n
lo Maybe n
hi) = if Maybe n
lo Maybe n -> Maybe n -> Bool
forall a. Ord a => a -> a -> Bool
> Maybe n
hi then Integer
0 else n -> Integer
forall a. Integral a => a -> Integer
toInteger n
high Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- n -> Integer
forall a. Integral a => a -> Integer
toInteger n
low Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
  where
    high :: n
high = Maybe n -> n
forall n. Bounded n => Maybe n -> n
highBound Maybe n
hi
    low :: n
low = Maybe n -> n
forall n. Bounded n => Maybe n -> n
lowBound Maybe n
lo

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

-- | This is an optimizing version of  TypeSpec :: TypeSpec n -> [n] -> Specification n
--   for Bounded NumSpecs.
--                    notInNumSpec :: Bounded n => TypeSpec n -> [n] -> Specification n
--   We use this function to specialize the (HasSpec t) method 'typeSpecOpt' for Bounded n.
--   So given (TypeSpec interval badlist) we might want to transform it to (MemberSpec goodlist)
--   There are 2 opportunities where this can payoff big time.
--   1) Suppose the total count of the elements in the interval is < length badlist
--      we can then return (MemberSpec (filter elements (`notElem` badlist)))
--      this must be smaller than (TypeSpec interval badlist) because the filtered list must be smaller than badlist
--   2) Suppose the type 't' is finite with size N. If the length of the badlist > (N/2), then the number of possible
--      good things must be smaller than (length badlist), because (possible good + bad == N), so regardless of the
--      count of the interval (MemberSpec (filter elements (`notElem` badlist))) is better. Sometimes much better.
--      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]
--      (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]
--      So (MemberSpec [2,7]) is better than  (TypeSpec [0..9]  [0,1,3,4,5,6,8,9]). This works no matter what
--      the count of interval is. We only need the (length badlist > (N/2)).
notInNumSpec ::
  forall n.
  ( HasSpec n
  , TypeSpec n ~ NumSpec n
  , Bounded n
  , Integral n
  ) =>
  NumSpec n ->
  [n] ->
  Specification n
notInNumSpec :: forall n.
(HasSpec n, TypeSpec n ~ NumSpec n, Bounded n, Integral n) =>
NumSpec n -> [n] -> Specification n
notInNumSpec ns :: NumSpec n
ns@(NumSpecInterval Maybe n
a Maybe n
b) [n]
bad
  | Int -> Integer
forall a. Integral a => a -> Integer
toInteger ([n] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [n]
bad) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> (forall n. (Integral n, Bounded n) => Integer
finiteSize @n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2) Bool -> Bool -> Bool
|| NumSpec n -> Integer
forall n. (Bounded n, Integral n) => NumSpec n -> Integer
countSpec NumSpec n
ns Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger ([n] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [n]
bad) =
      String -> [n] -> Specification n
forall a. Ord a => String -> [a] -> Specification a
nubOrdMemberSpec
        (String
"call to: (notInNumSpec " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NumSpec n -> String
forall a. Show a => a -> String
show NumSpec n
ns String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [n] -> String
forall a. Show a => a -> String
show [n]
bad String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")")
        [n
x | n
x <- [Maybe n -> n
forall n. Bounded n => Maybe n -> n
lowBound Maybe n
a .. Maybe n -> n
forall n. Bounded n => Maybe n -> n
highBound Maybe n
b], n -> [n] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem n
x [n]
bad]
  | Bool
otherwise = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec @n TypeSpec n
NumSpec n
ns [n]
bad

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

guardEmpty :: (Ord n, Num n) => Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty :: forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty (Just n
a) (Just n
b) NumSpec n
s
  | n
a n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<= n
b = NumSpec n
s
  | Bool
otherwise = Maybe n -> Maybe n -> NumSpec n
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (n -> Maybe n
forall a. a -> Maybe a
Just n
1) (n -> Maybe n
forall a. a -> Maybe a
Just n
0)
guardEmpty Maybe n
_ Maybe n
_ NumSpec n
s = NumSpec n
s

addNumSpec :: (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
addNumSpec :: forall n. (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
addNumSpec (NumSpecInterval Maybe n
x Maybe n
y) (NumSpecInterval Maybe n
a Maybe n
b) =
  Maybe n -> Maybe n -> NumSpec n -> NumSpec n
forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
x Maybe n
y (NumSpec n -> NumSpec n) -> NumSpec n -> NumSpec n
forall a b. (a -> b) -> a -> b
$
    Maybe n -> Maybe n -> NumSpec n -> NumSpec n
forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
a Maybe n
b (NumSpec n -> NumSpec n) -> NumSpec n -> NumSpec n
forall a b. (a -> b) -> a -> b
$
      Maybe n -> Maybe n -> NumSpec n
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (n -> n -> n
forall a. Num a => a -> a -> a
(+) (n -> n -> n) -> Maybe n -> Maybe (n -> n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
x Maybe (n -> n) -> Maybe n -> Maybe n
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe n
a) (n -> n -> n
forall a. Num a => a -> a -> a
(+) (n -> n -> n) -> Maybe n -> Maybe (n -> n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
y Maybe (n -> n) -> Maybe n -> Maybe n
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe n
b)

subNumSpec :: (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
subNumSpec :: forall n. (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
subNumSpec (NumSpecInterval Maybe n
x Maybe n
y) (NumSpecInterval Maybe n
a Maybe n
b) =
  Maybe n -> Maybe n -> NumSpec n -> NumSpec n
forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
x Maybe n
y (NumSpec n -> NumSpec n) -> NumSpec n -> NumSpec n
forall a b. (a -> b) -> a -> b
$
    Maybe n -> Maybe n -> NumSpec n -> NumSpec n
forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
a Maybe n
b (NumSpec n -> NumSpec n) -> NumSpec n -> NumSpec n
forall a b. (a -> b) -> a -> b
$
      Maybe n -> Maybe n -> NumSpec n
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval ((-) (n -> n -> n) -> Maybe n -> Maybe (n -> n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
x Maybe (n -> n) -> Maybe n -> Maybe n
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe n
b) ((-) (n -> n -> n) -> Maybe n -> Maybe (n -> n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
y Maybe (n -> n) -> Maybe n -> Maybe n
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe n
a)

multNumSpec :: (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
multNumSpec :: forall n. (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
multNumSpec (NumSpecInterval Maybe n
a Maybe n
b) (NumSpecInterval Maybe n
c Maybe n
d) =
  Maybe n -> Maybe n -> NumSpec n -> NumSpec n
forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
a Maybe n
b (NumSpec n -> NumSpec n) -> NumSpec n -> NumSpec n
forall a b. (a -> b) -> a -> b
$
    Maybe n -> Maybe n -> NumSpec n -> NumSpec n
forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
c Maybe n
d (NumSpec n -> NumSpec n) -> NumSpec n -> NumSpec n
forall a b. (a -> b) -> a -> b
$
      Maybe n -> Maybe n -> NumSpec n
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (T n -> Maybe n
forall x. T x -> Maybe x
unT ([T n] -> T n
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [T n]
s)) (T n -> Maybe n
forall x. T x -> Maybe x
unT ([T n] -> T n
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [T n]
s))
  where
    s :: [T n]
s = [T n -> T n -> T n
forall x. Num x => T x -> T x -> T x
multT (Maybe n -> T n
forall x. Maybe x -> T x
neg Maybe n
a) (Maybe n -> T n
forall x. Maybe x -> T x
neg Maybe n
c), T n -> T n -> T n
forall x. Num x => T x -> T x -> T x
multT (Maybe n -> T n
forall x. Maybe x -> T x
neg Maybe n
a) (Maybe n -> T n
forall x. Maybe x -> T x
pos Maybe n
d), T n -> T n -> T n
forall x. Num x => T x -> T x -> T x
multT (Maybe n -> T n
forall x. Maybe x -> T x
pos Maybe n
b) (Maybe n -> T n
forall x. Maybe x -> T x
neg Maybe n
c), T n -> T n -> T n
forall x. Num x => T x -> T x -> T x
multT (Maybe n -> T n
forall x. Maybe x -> T x
pos Maybe n
b) (Maybe n -> T n
forall x. Maybe x -> T x
pos Maybe n
d)]

negNumSpec :: Num n => NumSpec n -> NumSpec n
negNumSpec :: forall n. Num n => NumSpec n -> NumSpec n
negNumSpec (NumSpecInterval Maybe n
lo Maybe n
hi) = Maybe n -> Maybe n -> NumSpec n
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (n -> n
forall a. Num a => a -> a
negate (n -> n) -> Maybe n -> Maybe n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
hi) (n -> n
forall a. Num a => a -> a
negate (n -> n) -> Maybe n -> Maybe n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
lo)

instance Num (NumSpec Integer) where
  + :: NumSpec Integer -> NumSpec Integer -> NumSpec Integer
(+) = NumSpec Integer -> NumSpec Integer -> NumSpec Integer
forall n. (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
addNumSpec
  (-) = NumSpec Integer -> NumSpec Integer -> NumSpec Integer
forall n. (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
subNumSpec
  * :: NumSpec Integer -> NumSpec Integer -> NumSpec Integer
(*) = NumSpec Integer -> NumSpec Integer -> NumSpec Integer
forall n. (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
multNumSpec
  negate :: NumSpec Integer -> NumSpec Integer
negate = NumSpec Integer -> NumSpec Integer
forall n. Num n => NumSpec n -> NumSpec n
negNumSpec
  fromInteger :: Integer -> NumSpec Integer
fromInteger Integer
n = Maybe Integer -> Maybe Integer -> NumSpec Integer
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Integer
forall a. Num a => Integer -> a
fromInteger Integer
n)) (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Integer
forall a. Num a => Integer -> a
fromInteger Integer
n))
  abs :: NumSpec Integer -> NumSpec Integer
abs = String -> NumSpec Integer -> NumSpec Integer
forall a. HasCallStack => String -> a
error String
"No abs in the Num (NumSpec  Integer) instance"
  signum :: NumSpec Integer -> NumSpec Integer
signum = String -> NumSpec Integer -> NumSpec Integer
forall a. HasCallStack => String -> a
error String
"No signum in the Num (NumSpec  Integer) instance"

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

-- | T is a sort of special version of Maybe, with two Nothings.
--   Given:: NumSpecInterval (Maybe n) (Maybe n) -> Numspec
--   We can't distinguish between the two Nothings in (NumSpecInterval Nothing Nothing)
--   But using (NumSpecInterval NegInf PosInf) we can, In fact we can make a total ordering on 'T'
--   So an ascending Sorted [T x] would all the NegInf on the left and all the PosInf on the right, with
--   the Ok's sorted in between. I.e. [NegInf, NegInf, Ok 3, Ok 6, Ok 12, Pos Inf]
data T x = NegInf | Ok x | PosInf
  deriving (Int -> T x -> ShowS
[T x] -> ShowS
T x -> String
(Int -> T x -> ShowS)
-> (T x -> String) -> ([T x] -> ShowS) -> Show (T x)
forall x. Show x => Int -> T x -> ShowS
forall x. Show x => [T x] -> ShowS
forall x. Show x => T x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall x. Show x => Int -> T x -> ShowS
showsPrec :: Int -> T x -> ShowS
$cshow :: forall x. Show x => T x -> String
show :: T x -> String
$cshowList :: forall x. Show x => [T x] -> ShowS
showList :: [T x] -> ShowS
Show, T x -> T x -> Bool
(T x -> T x -> Bool) -> (T x -> T x -> Bool) -> Eq (T x)
forall x. Eq x => T x -> T x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall x. Eq x => T x -> T x -> Bool
== :: T x -> T x -> Bool
$c/= :: forall x. Eq x => T x -> T x -> Bool
/= :: T x -> T x -> Bool
Eq, Eq (T x)
Eq (T x) =>
(T x -> T x -> Ordering)
-> (T x -> T x -> Bool)
-> (T x -> T x -> Bool)
-> (T x -> T x -> Bool)
-> (T x -> T x -> Bool)
-> (T x -> T x -> T x)
-> (T x -> T x -> T x)
-> Ord (T x)
T x -> T x -> Bool
T x -> T x -> Ordering
T x -> T x -> T x
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall x. Ord x => Eq (T x)
forall x. Ord x => T x -> T x -> Bool
forall x. Ord x => T x -> T x -> Ordering
forall x. Ord x => T x -> T x -> T x
$ccompare :: forall x. Ord x => T x -> T x -> Ordering
compare :: T x -> T x -> Ordering
$c< :: forall x. Ord x => T x -> T x -> Bool
< :: T x -> T x -> Bool
$c<= :: forall x. Ord x => T x -> T x -> Bool
<= :: T x -> T x -> Bool
$c> :: forall x. Ord x => T x -> T x -> Bool
> :: T x -> T x -> Bool
$c>= :: forall x. Ord x => T x -> T x -> Bool
>= :: T x -> T x -> Bool
$cmax :: forall x. Ord x => T x -> T x -> T x
max :: T x -> T x -> T x
$cmin :: forall x. Ord x => T x -> T x -> T x
min :: T x -> T x -> T x
Ord)

-- \| Conversion between (T x) and (Maybe x)
unT :: T x -> Maybe x
unT :: forall x. T x -> Maybe x
unT (Ok x
x) = x -> Maybe x
forall a. a -> Maybe a
Just x
x
unT T x
_ = Maybe x
forall a. Maybe a
Nothing

-- | Use this on the lower bound. I.e. lo from pair (lo,hi)
neg :: Maybe x -> T x
neg :: forall x. Maybe x -> T x
neg Maybe x
Nothing = T x
forall x. T x
NegInf
neg (Just x
x) = x -> T x
forall x. x -> T x
Ok x
x

-- | Use this on the upper bound. I.e. hi from pair (lo,hi)
pos :: Maybe x -> T x
pos :: forall x. Maybe x -> T x
pos Maybe x
Nothing = T x
forall x. T x
PosInf
pos (Just x
x) = x -> T x
forall x. x -> T x
Ok x
x

-- | multiply two (T x), correctly handling the infinities NegInf and PosInf
multT :: Num x => T x -> T x -> T x
multT :: forall x. Num x => T x -> T x -> T x
multT T x
NegInf T x
NegInf = T x
forall x. T x
PosInf
multT T x
NegInf T x
PosInf = T x
forall x. T x
NegInf
multT T x
NegInf (Ok x
_) = T x
forall x. T x
NegInf
multT (Ok x
_) T x
NegInf = T x
forall x. T x
NegInf
multT (Ok x
x) (Ok x
y) = x -> T x
forall x. x -> T x
Ok (x
x x -> x -> x
forall a. Num a => a -> a -> a
* x
y)
multT (Ok x
_) T x
PosInf = T x
forall x. T x
PosInf
multT T x
PosInf T x
PosInf = T x
forall x. T x
PosInf
multT T x
PosInf T x
NegInf = T x
forall x. T x
NegInf
multT T x
PosInf (Ok x
_) = T x
forall x. T x
PosInf

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

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

addSpecInt ::
  Number n =>
  Specification n ->
  Specification n ->
  Specification n
addSpecInt :: forall n.
Number n =>
Specification n -> Specification n -> Specification n
addSpecInt Specification n
x Specification n
y = String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
forall n.
Number n =>
String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
operateSpec String
" + " n -> n -> n
forall a. Num a => a -> a -> a
(+) TypeSpec n -> TypeSpec n -> TypeSpec n
NumSpec n -> NumSpec n -> NumSpec n
forall a. Num a => a -> a -> a
(+) Specification n
x Specification n
y

subSpecInt ::
  Number n =>
  Specification n ->
  Specification n ->
  Specification n
subSpecInt :: forall n.
Number n =>
Specification n -> Specification n -> Specification n
subSpecInt Specification n
x Specification n
y = String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
forall n.
Number n =>
String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
operateSpec String
" - " (-) (-) Specification n
x Specification n
y

multSpecInt ::
  Number n =>
  Specification n ->
  Specification n ->
  Specification n
multSpecInt :: forall n.
Number n =>
Specification n -> Specification n -> Specification n
multSpecInt Specification n
x Specification n
y = String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
forall n.
Number n =>
String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
operateSpec String
" * " n -> n -> n
forall a. Num a => a -> a -> a
(*) TypeSpec n -> TypeSpec n -> TypeSpec n
NumSpec n -> NumSpec n -> NumSpec n
forall a. Num a => a -> a -> a
(*) Specification n
x Specification n
y

-- | let 'n' be some numeric type, and 'f' and 'ft' be operations on 'n' and (TypeSpec n)
--   Then lift these operations from (TypeSpec n) to (Specification n)
--   Normally 'f' will be a (Num n) instance method (+,-,*) on n,
--   and 'ft' will be a a (Num (TypeSpec n)) instance method (+,-,*) on (TypeSpec n)
--   But this will work for any operations 'f' and 'ft' with the right types
operateSpec ::
  Number n =>
  String ->
  (n -> n -> n) ->
  (TypeSpec n -> TypeSpec n -> TypeSpec n) ->
  Specification n ->
  Specification n ->
  Specification n
operateSpec :: forall n.
Number n =>
String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
operateSpec String
operator n -> n -> n
f TypeSpec n -> TypeSpec n -> TypeSpec n
ft (ExplainSpec [String]
es Specification n
x) Specification n
y = [String] -> Specification n -> Specification n
forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (Specification n -> Specification n)
-> Specification n -> Specification n
forall a b. (a -> b) -> a -> b
$ String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
forall n.
Number n =>
String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
operateSpec String
operator n -> n -> n
f TypeSpec n -> TypeSpec n -> TypeSpec n
ft Specification n
x Specification n
y
operateSpec String
operator n -> n -> n
f TypeSpec n -> TypeSpec n -> TypeSpec n
ft Specification n
x (ExplainSpec [String]
es Specification n
y) = [String] -> Specification n -> Specification n
forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (Specification n -> Specification n)
-> Specification n -> Specification n
forall a b. (a -> b) -> a -> b
$ String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
forall n.
Number n =>
String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
operateSpec String
operator n -> n -> n
f TypeSpec n -> TypeSpec n -> TypeSpec n
ft Specification n
x Specification n
y
operateSpec String
operator n -> n -> n
f TypeSpec n -> TypeSpec n -> TypeSpec n
ft Specification n
x Specification n
y = case (Specification n
x, Specification n
y) of
  (ErrorSpec NonEmpty String
xs, ErrorSpec NonEmpty String
ys) -> NonEmpty String -> Specification n
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String
xs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
ys)
  (ErrorSpec NonEmpty String
xs, Specification n
_) -> NonEmpty String -> Specification n
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec NonEmpty String
xs
  (Specification n
_, ErrorSpec NonEmpty String
ys) -> NonEmpty String -> Specification n
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec NonEmpty String
ys
  (Specification n
TrueSpec, Specification n
_) -> Specification n
forall deps a. SpecificationD deps a
TrueSpec
  (Specification n
_, Specification n
TrueSpec) -> Specification n
forall deps a. SpecificationD deps a
TrueSpec
  (Specification n
_, SuspendedSpec Var n
_ PredD Deps
_) -> Specification n
forall deps a. SpecificationD deps a
TrueSpec
  (SuspendedSpec Var n
_ PredD Deps
_, Specification n
_) -> Specification n
forall deps a. SpecificationD deps a
TrueSpec
  (TypeSpec TypeSpec n
a [n]
bad1, TypeSpec TypeSpec n
b [n]
bad2) -> TypeSpec n -> [n] -> Specification n
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (TypeSpec n -> TypeSpec n -> TypeSpec n
ft TypeSpec n
a TypeSpec n
b) [n -> n -> n
f n
b1 n
b2 | n
b1 <- [n]
bad1, n
b2 <- [n]
bad2]
  (MemberSpec NonEmpty n
xs, MemberSpec NonEmpty n
ys) ->
    String -> [n] -> Specification n
forall a. Ord a => String -> [a] -> Specification a
nubOrdMemberSpec
      (Specification n -> String
forall a. Show a => a -> String
show Specification n
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
operator String -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification n -> String
forall a. Show a => a -> String
show Specification n
y)
      [n -> n -> n
f n
x1 n
y1 | n
x1 <- NonEmpty n -> [n]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty n
xs, n
y1 <- NonEmpty n -> [n]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty n
ys]
  -- This block is all (MemberSpec{}, TypeSpec{}) with MemberSpec on the left
  (MemberSpec NonEmpty n
ys, TypeSpec (NumSpecInterval (Just n
i) (Just n
j)) [n]
bad) ->
    let xs :: [n]
xs = NonEmpty n -> [n]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty n
ys
     in String -> [n] -> Specification n
forall a. Ord a => String -> [a] -> Specification a
nubOrdMemberSpec
          (Specification n -> String
forall a. Show a => a -> String
show Specification n
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
operator String -> ShowS
forall a. [a] -> [a] -> [a]
++ Specification n -> String
forall a. Show a => a -> String
show Specification n
y)
          [n -> n -> n
f n
x1 n
y1 | n
x1 <- [n]
xs, n
y1 <- [n
i .. n
j], Bool -> Bool
not (n -> [n] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem n
y1 [n]
bad)]
  -- Somewhat loose spec here, but more accurate then TrueSpec, it is exact if 'xs' has one element (i.e. 'xs' = [i])
  (MemberSpec NonEmpty n
ys, TypeSpec (NumSpecInterval Maybe n
lo Maybe n
hi) [n]
bads) ->
    -- We use the specialized version of 'TypeSpec' 'typeSpecOpt'
    let xs :: [n]
xs = NonEmpty n -> [n]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty n
ys
     in TypeSpec n -> [n] -> Specification n
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
typeSpecOpt
          (Maybe n -> Maybe n -> NumSpec n
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (n -> n -> n
f ([n] -> n
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [n]
xs) (n -> n) -> Maybe n -> Maybe n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
lo) (n -> n -> n
f ([n] -> n
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [n]
xs) (n -> n) -> Maybe n -> Maybe n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
hi))
          [n -> n -> n
f n
x1 n
b | n
x1 <- [n]
xs, n
b <- [n]
bads]
  -- we flip the arguments, so we need to flip the functions as well
  (Specification n
sleft, Specification n
sright) -> String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
forall n.
Number n =>
String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
operateSpec String
operator (\n
a n
b -> n -> n -> n
f n
b n
a) (\TypeSpec n
u TypeSpec n
v -> TypeSpec n -> TypeSpec n -> TypeSpec n
ft TypeSpec n
v TypeSpec n
u) Specification n
sright Specification n
sleft

-- | This is very liberal, since in lots of cases it returns TrueSpec.
--  for example all operations on SuspendedSpec, and certain
--  operations between TypeSpec and MemberSpec. Perhaps we should
--  remove it. Only the addSpec (+) and multSpec (*) methods are used.
--  But, it is kind of cool ...
--  In Fact we can use this to make Num(Specification n) instance for any 'n'.
--  But, only Integer is safe, because in all other types (+) and especially
--  (-) can lead to overflow or underflow failures.
instance Number Integer => Num (Specification Integer) where
  + :: Specification Integer
-> Specification Integer -> Specification Integer
(+) = Specification Integer
-> Specification Integer -> Specification Integer
forall n.
Number n =>
Specification n -> Specification n -> Specification n
addSpecInt
  (-) = Specification Integer
-> Specification Integer -> Specification Integer
forall n.
Number n =>
Specification n -> Specification n -> Specification n
subSpecInt
  * :: Specification Integer
-> Specification Integer -> Specification Integer
(*) = Specification Integer
-> Specification Integer -> Specification Integer
forall n.
Number n =>
Specification n -> Specification n -> Specification n
multSpecInt
  fromInteger :: Integer -> Specification Integer
fromInteger Integer
n = TypeSpec Integer -> [Integer] -> Specification Integer
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (Maybe Integer -> Maybe Integer -> NumSpec Integer
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n) (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n)) []
  abs :: Specification Integer -> Specification Integer
abs Specification Integer
_ = Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
  signum :: Specification Integer -> Specification Integer
signum Specification Integer
_ = Specification Integer
forall deps a. SpecificationD deps a
TrueSpec

-- ===========================================================================

-- | Put some (admittedly loose bounds) on the number of solutions that
--   'genFromTypeSpec' might return. For lots of types, there is no way to be very accurate.
--   Here we lift the HasSpec methods 'cardinalTrueSpec' and 'cardinalTypeSpec'
--   from (TypeSpec Integer) to (Specification Integer)
cardinality ::
  forall a. (Number Integer, HasSpec a) => Specification a -> Specification Integer
cardinality :: forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality (ExplainSpec [String]
es SpecificationD Deps a
s) = [String] -> Specification Integer -> Specification Integer
forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (SpecificationD Deps a -> Specification Integer
forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality SpecificationD Deps a
s)
cardinality SpecificationD Deps a
TrueSpec = forall a. HasSpec a => Specification Integer
cardinalTrueSpec @a
cardinality (MemberSpec NonEmpty a
es) = Integer -> Specification Integer
forall a. a -> Specification a
equalSpec (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
es)))
cardinality ErrorSpec {} = Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
0
cardinality (TypeSpec TypeSpec a
s [a]
cant) =
  Specification Integer
-> Specification Integer -> Specification Integer
forall n.
Number n =>
Specification n -> Specification n -> Specification n
subSpecInt
    (forall a. HasSpec a => TypeSpec a -> Specification Integer
cardinalTypeSpec @a TypeSpec a
s)
    (Integer -> Specification Integer
forall a. a -> Specification a
equalSpec (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (\a
c -> forall a. (HasSpec a, HasCallStack) => a -> TypeSpec a -> Bool
conformsTo @a a
c TypeSpec a
s) [a]
cant)))
cardinality SuspendedSpec {} = forall a. HasSpec a => Specification Integer
cardinalTrueSpec @a

-- | A generic function to use as an instance for the HasSpec method
--   cardinalTypeSpec :: HasSpec a => TypeSpec a -> Specification Integer
--   for types 'n' such that (TypeSpec n ~ NumSpec n)
cardinalNumSpec ::
  forall n. (Integral n, MaybeBounded n, HasSpec n) => NumSpec n -> Specification Integer
cardinalNumSpec :: forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec (NumSpecInterval (Just n
lo) (Just n
hi)) =
  if n
hi n -> n -> Bool
forall a. Ord a => a -> a -> Bool
>= n
lo
    then Integer -> Specification Integer
forall a. a -> Specification a
equalSpec (n -> Integer
forall a. Integral a => a -> Integer
toInteger n
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- n -> Integer
forall a. Integral a => a -> Integer
toInteger n
lo Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
    else Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
0
cardinalNumSpec (NumSpecInterval Maybe n
Nothing (Just n
hi)) =
  case forall a. MaybeBounded a => Maybe a
lowerBound @n of
    Just n
lo -> Integer -> Specification Integer
forall a. a -> Specification a
equalSpec (n -> Integer
forall a. Integral a => a -> Integer
toInteger n
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- n -> Integer
forall a. Integral a => a -> Integer
toInteger n
lo)
    Maybe n
Nothing -> Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
cardinalNumSpec (NumSpecInterval (Just n
lo) Maybe n
Nothing) =
  case forall a. MaybeBounded a => Maybe a
upperBound @n of
    Just n
hi -> Integer -> Specification Integer
forall a. a -> Specification a
equalSpec (n -> Integer
forall a. Integral a => a -> Integer
toInteger n
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- n -> Integer
forall a. Integral a => a -> Integer
toInteger n
lo)
    Maybe n
Nothing -> Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
cardinalNumSpec (NumSpecInterval Maybe n
Nothing Maybe n
Nothing) = forall a. HasSpec a => Specification Integer
cardinalTrueSpec @n

-- ====================================================================
-- Now the operations on Numbers

class (Num a, HasSpec a) => NumLike a where
  subtractSpec :: a -> TypeSpec a -> Specification a
  default subtractSpec ::
    ( NumLike (SimpleRep a)
    , GenericRequires a
    ) =>
    a ->
    TypeSpec a ->
    Specification a
  subtractSpec a
a TypeSpec a
ts = Specification (SimpleRep a) -> Specification a
forall a.
GenericRequires a =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec (Specification (SimpleRep a) -> Specification a)
-> Specification (SimpleRep a) -> Specification a
forall a b. (a -> b) -> a -> b
$ SimpleRep a
-> TypeSpec (SimpleRep a) -> Specification (SimpleRep a)
forall a. NumLike a => a -> TypeSpec a -> Specification a
subtractSpec (a -> SimpleRep a
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep a
a) TypeSpec a
TypeSpec (SimpleRep a)
ts

  negateSpec :: TypeSpec a -> Specification a
  default negateSpec ::
    ( NumLike (SimpleRep a)
    , GenericRequires a
    ) =>
    TypeSpec a ->
    Specification a
  negateSpec = Specification (SimpleRep a) -> Specification a
forall a.
GenericRequires a =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec (Specification (SimpleRep a) -> Specification a)
-> (TypeSpec (SimpleRep a) -> Specification (SimpleRep a))
-> TypeSpec (SimpleRep a)
-> Specification a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NumLike a => TypeSpec a -> Specification a
negateSpec @(SimpleRep a)

  safeSubtract :: a -> a -> Maybe a
  default safeSubtract ::
    (HasSimpleRep a, NumLike (SimpleRep a)) =>
    a ->
    a ->
    Maybe a
  safeSubtract a
a a
b = SimpleRep a -> a
forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep (SimpleRep a -> a) -> Maybe (SimpleRep a) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. NumLike a => a -> a -> Maybe a
safeSubtract @(SimpleRep a) (a -> SimpleRep a
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep a
a) (a -> SimpleRep a
forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep a
b)

data IntW (as :: [Type]) b where
  AddW :: NumLike a => IntW '[a, a] a
  NegateW :: NumLike a => IntW '[a] a

deriving instance Eq (IntW dom rng)

instance Show (IntW d r) where
  show :: IntW d r -> String
show IntW d r
AddW = String
"addFn"
  show IntW d r
NegateW = String
"negateFn"

instance Semantics IntW where
  semantics :: forall (d :: [*]) r. IntW d r -> FunTy d r
semantics IntW d r
AddW = FunTy d r
r -> r -> r
forall a. Num a => a -> a -> a
(+)
  semantics IntW d r
NegateW = FunTy d r
r -> r
forall a. Num a => a -> a
negate

instance Syntax IntW -- Use default methods

type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a)

instance {-# OVERLAPPABLE #-} Numeric a => NumLike a where
  subtractSpec :: a -> TypeSpec a -> Specification a
subtractSpec a
a ts :: TypeSpec a
ts@(NumSpecInterval Maybe a
ml Maybe a
mu)
    | Just a
u <- Maybe a
mu
    , a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0
    , Maybe a
Nothing <- a -> a -> Maybe a
forall a. NumLike a => a -> a -> Maybe a
safeSubtract a
a a
u =
        NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String -> Specification a)
-> NonEmpty String -> Specification a
forall a b. (a -> b) -> a -> b
$
          [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
            [ String
"Underflow in subtractSpec (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ forall t. Typeable t => String
forall {k} (t :: k). Typeable t => String
showType @a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"):"
            , String
"  a = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a
            , String
"  ts = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NumSpec a -> String
forall a. Show a => a -> String
show TypeSpec a
NumSpec a
ts
            ]
    | Just a
l <- Maybe a
ml
    , a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0
    , Maybe a
Nothing <- a -> a -> Maybe a
forall a. NumLike a => a -> a -> Maybe a
safeSubtract a
a a
l =
        NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String -> Specification a)
-> NonEmpty String -> Specification a
forall a b. (a -> b) -> a -> b
$
          [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
            [ String
"Overflow in subtractSpec (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ forall t. Typeable t => String
forall {k} (t :: k). Typeable t => String
showType @a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"):"
            , String
"  a = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a
            , String
"  ts = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NumSpec a -> String
forall a. Show a => a -> String
show TypeSpec a
NumSpec a
ts
            ]
    | Bool
otherwise = TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (a -> a -> a
safeSub a
a (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
ml) (a -> a -> a
safeSub a
a (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
mu)
    where
      safeSub :: a -> a -> a
      safeSub :: a -> a -> a
safeSub a
a1 a
x
        | Just a
r <- a -> a -> Maybe a
forall a. NumLike a => a -> a -> Maybe a
safeSubtract a
a1 a
x = a
r
        | a
a1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust Maybe a
forall a. MaybeBounded a => Maybe a
upperBound
        | Bool
otherwise = Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust Maybe a
forall a. MaybeBounded a => Maybe a
lowerBound
  negateSpec :: TypeSpec a -> Specification a
negateSpec (NumSpecInterval Maybe a
ml Maybe a
mu) = TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a) -> TypeSpec a -> Specification a
forall a b. (a -> b) -> a -> b
$ Maybe a -> Maybe a -> NumSpec a
forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (a -> a
forall a. Num a => a -> a
negate (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
mu) (a -> a
forall a. Num a => a -> a
negate (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
ml)

  safeSubtract :: a -> a -> Maybe a
safeSubtract a
a a
x
    | a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0
    , Just a
lb <- Maybe a
forall a. MaybeBounded a => Maybe a
lowerBound
    , a
lb a -> a -> a
forall a. Num a => a -> a -> a
+ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
x =
        Maybe a
forall a. Maybe a
Nothing
    | a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0
    , Just a
ub <- Maybe a
forall a. MaybeBounded a => Maybe a
upperBound
    , a
ub a -> a -> a
forall a. Num a => a -> a -> a
+ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
x =
        Maybe a
forall a. Maybe a
Nothing
    | Bool
otherwise = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
a

instance NumLike a => Num (Term a) where
  + :: Term a -> Term a -> Term a
(+) = Term a -> Term a -> Term a
forall a. NumLike a => Term a -> Term a -> Term a
addFn
  negate :: Term a -> Term a
negate = Term a -> Term a
forall a. NumLike a => Term a -> Term a
negateFn
  fromInteger :: Integer -> Term a
fromInteger = a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit (a -> Term a) -> (Integer -> a) -> Integer -> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a
forall a. Num a => Integer -> a
fromInteger
  * :: Term a -> Term a -> Term a
(*) = String -> Term a -> Term a -> Term a
forall a. HasCallStack => String -> a
error String
"(*) not implemented for Term Fn Int"
  abs :: Term a -> Term a
abs = String -> Term a -> Term a
forall a. HasCallStack => String -> a
error String
"abs not implemented for Term Fn Int"
  signum :: Term a -> Term a
signum = String -> Term a -> Term a
forall a. HasCallStack => String -> a
error String
"signum not implemented for Term Fn Int"

-- | Just a note that these instances won't work until we are in a context where
--   there is a HasSpec instance of 'a', which (NumLike a) demands.
--   This happens in Constrained.Experiment.TheKnot
instance Logic IntW where
  propagateTypeSpec :: forall (as :: [*]) b a.
(AppRequires IntW as b, HasSpec a) =>
IntW as b
-> ListCtx Value as (HOLE a)
-> TypeSpec b
-> [b]
-> Specification a
propagateTypeSpec IntW as b
AddW (HOLE a b
HOLE :<: b
i) TypeSpec b
ts [b]
cant = a -> TypeSpec a -> Specification a
forall a. NumLike a => a -> TypeSpec a -> Specification a
subtractSpec b
a
i TypeSpec b
TypeSpec a
ts Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> [a] -> Specification a
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec ((a -> Maybe a) -> [a] -> [a]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (a -> a -> Maybe a
forall a. NumLike a => a -> a -> Maybe a
safeSubtract b
a
i) [b]
[a]
cant)
  propagateTypeSpec IntW as b
AddW ListCtx Value as (HOLE a)
ctx TypeSpec b
ts [b]
cant = IntW '[b, b] b
-> ListCtx Value '[b, b] (HOLE a)
-> TypeSpec b
-> [b]
-> Specification a
forall (as :: [*]) b a.
(AppRequires IntW as b, HasSpec a) =>
IntW as b
-> ListCtx Value as (HOLE a)
-> TypeSpec b
-> [b]
-> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a)
-> TypeSpec b
-> [b]
-> Specification a
propagateTypeSpec IntW '[b, b] b
forall a. NumLike a => IntW '[a, a] a
AddW (ListCtx Value '[b, b] (HOLE a) -> ListCtx Value '[b, b] (HOLE a)
forall a b c.
(Typeable a, Show a, Typeable b, Show b) =>
ListCtx Value '[a, b] (HOLE c) -> ListCtx Value '[b, a] (HOLE c)
flipCtx ListCtx Value as (HOLE a)
ListCtx Value '[b, b] (HOLE a)
ctx) TypeSpec b
ts [b]
cant
  propagateTypeSpec IntW as b
NegateW (Unary HOLE a b
HOLE) TypeSpec b
ts [b]
cant = TypeSpec a -> Specification a
forall a. NumLike a => TypeSpec a -> Specification a
negateSpec TypeSpec b
TypeSpec a
ts Specification a -> Specification a -> Specification a
forall a. Semigroup a => a -> a -> a
<> [a] -> Specification a
forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec ((a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
forall a. Num a => a -> a
negate [b]
[a]
cant)

  propagateMemberSpec :: forall (as :: [*]) b a.
(AppRequires IntW as b, HasSpec a) =>
IntW as b
-> ListCtx Value as (HOLE a) -> NonEmpty b -> Specification a
propagateMemberSpec IntW as b
AddW (HOLE a b
HOLE :<: b
i) NonEmpty b
es =
    [a] -> NonEmpty String -> Specification a
forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
      ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> Maybe a) -> [a] -> [a]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (a -> a -> Maybe a
forall a. NumLike a => a -> a -> Maybe a
safeSubtract b
a
i) (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
NonEmpty a
es))
      ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [ String
"propagateSpecFn on (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" +. HOLE)"
          , String
"The Spec is a MemberSpec = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NonEmpty b -> String
forall a. Show a => a -> String
show NonEmpty b
es -- show (MemberSpec @HasSpec @TS es)
          , String
"We can't safely subtract " String -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" from any choice in the MemberSpec."
          ]
      )
  propagateMemberSpec IntW as b
AddW ListCtx Value as (HOLE a)
ctx NonEmpty b
es = IntW '[b, b] b
-> ListCtx Value '[b, b] (HOLE a) -> NonEmpty b -> Specification a
forall (as :: [*]) b a.
(AppRequires IntW as b, HasSpec a) =>
IntW as b
-> ListCtx Value as (HOLE a) -> NonEmpty b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> NonEmpty b -> Specification a
propagateMemberSpec IntW '[b, b] b
forall a. NumLike a => IntW '[a, a] a
AddW (ListCtx Value '[b, b] (HOLE a) -> ListCtx Value '[b, b] (HOLE a)
forall a b c.
(Typeable a, Show a, Typeable b, Show b) =>
ListCtx Value '[a, b] (HOLE c) -> ListCtx Value '[b, a] (HOLE c)
flipCtx ListCtx Value as (HOLE a)
ListCtx Value '[b, b] (HOLE a)
ctx) NonEmpty b
es
  propagateMemberSpec IntW as b
NegateW (Unary HOLE a b
HOLE) NonEmpty b
es = NonEmpty a -> Specification a
forall a deps. NonEmpty a -> SpecificationD deps a
MemberSpec (NonEmpty a -> Specification a) -> NonEmpty a -> Specification a
forall a b. (a -> b) -> a -> b
$ NonEmpty a -> NonEmpty a
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (NonEmpty a -> NonEmpty a) -> NonEmpty a -> NonEmpty a
forall a b. (a -> b) -> a -> b
$ (a -> a) -> NonEmpty a -> NonEmpty a
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. Num a => a -> a
negate NonEmpty b
NonEmpty a
es

addFn :: forall a. NumLike a => Term a -> Term a -> Term a
addFn :: forall a. NumLike a => Term a -> Term a -> Term a
addFn = IntW '[a, a] a -> FunTy (MapList Term '[a, a]) (TermD Deps a)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm IntW '[a, a] a
forall a. NumLike a => IntW '[a, a] a
AddW

negateFn :: forall a. NumLike a => Term a -> Term a
negateFn :: forall a. NumLike a => Term a -> Term a
negateFn = IntW '[a] a -> FunTy (MapList Term '[a]) (TermD Deps a)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm IntW '[a] a
forall a. NumLike a => IntW '[a] a
NegateW

infix 4 +.

(+.) :: NumLike a => Term a -> Term a -> Term a
+. :: forall a. NumLike a => Term a -> Term a -> Term a
(+.) = Term a -> Term a -> Term a
forall a. NumLike a => Term a -> Term a -> Term a
addFn

negate_ :: NumLike a => Term a -> Term a
negate_ :: forall a. NumLike a => Term a -> Term a
negate_ = Term a -> Term a
forall a. NumLike a => Term a -> Term a
negateFn

infix 4 -.

(-.) :: Numeric n => Term n -> Term n -> Term n
-. :: forall n. Numeric n => Term n -> Term n -> Term n
(-.) Term n
x Term n
y = Term n -> Term n -> Term n
forall a. NumLike a => Term a -> Term a -> Term a
addFn Term n
x (Term n -> Term n
forall a. NumLike a => Term a -> Term a
negateFn Term n
y)

toPredsNumSpec ::
  OrdLike n =>
  Term n ->
  NumSpec n ->
  Pred
toPredsNumSpec :: forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec Term n
v (NumSpecInterval Maybe n
ml Maybe n
mu) =
  [PredD Deps] -> PredD Deps
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ([PredD Deps] -> PredD Deps) -> [PredD Deps] -> PredD Deps
forall a b. (a -> b) -> a -> b
$
    [TermD Deps Bool -> PredD Deps
forall deps. TermD deps Bool -> PredD deps
Assert (TermD Deps Bool -> PredD Deps) -> TermD Deps Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ n -> Term n
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit n
l Term n -> Term n -> TermD Deps Bool
forall a. OrdLike a => Term a -> Term a -> TermD Deps Bool
<=. Term n
v | n
l <- Maybe n -> [n]
forall a. Maybe a -> [a]
maybeToList Maybe n
ml]
      [PredD Deps] -> [PredD Deps] -> [PredD Deps]
forall a. [a] -> [a] -> [a]
++ [TermD Deps Bool -> PredD Deps
forall deps. TermD deps Bool -> PredD deps
Assert (TermD Deps Bool -> PredD Deps) -> TermD Deps Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term n
v Term n -> Term n -> TermD Deps Bool
forall a. OrdLike a => Term a -> Term a -> TermD Deps Bool
<=. n -> Term n
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit n
u | n
u <- Maybe n -> [n]
forall a. Maybe a -> [a]
maybeToList Maybe n
mu]

infixr 4 <=.

(<=.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. :: forall a. OrdLike a => Term a -> Term a -> TermD Deps Bool
(<=.) = OrdW '[a, a] Bool -> FunTy (MapList Term '[a, a]) (TermD Deps Bool)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
LessOrEqualW

infixr 4 <.

(<.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
<. :: forall a. OrdLike a => Term a -> Term a -> TermD Deps Bool
(<.) = OrdW '[a, a] Bool -> FunTy (MapList Term '[a, a]) (TermD Deps Bool)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
LessW

infixr 4 >=.

(>=.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. :: forall a. OrdLike a => Term a -> Term a -> TermD Deps Bool
(>=.) = OrdW '[a, a] Bool -> FunTy (MapList Term '[a, a]) (TermD Deps Bool)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
GreaterOrEqualW

infixr 4 >.

(>.) :: forall a. OrdLike a => Term a -> Term a -> Term Bool
>. :: forall a. OrdLike a => Term a -> Term a -> TermD Deps Bool
(>.) = OrdW '[a, a] Bool -> FunTy (MapList Term '[a, a]) (TermD Deps Bool)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
GreaterW

instance Logic OrdW where
  propagate :: forall (as :: [*]) b a.
(AppRequires OrdW as b, HasSpec a) =>
OrdW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate OrdW as b
f ListCtx Value as (HOLE a)
ctxt (ExplainSpec [] SpecificationD Deps b
s) = OrdW as b
-> ListCtx Value as (HOLE a)
-> SpecificationD Deps b
-> Specification a
forall (as :: [*]) b a.
(AppRequires OrdW as b, HasSpec a) =>
OrdW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate OrdW as b
f ListCtx Value as (HOLE a)
ctxt SpecificationD Deps b
s
  propagate OrdW as b
f ListCtx Value as (HOLE a)
ctxt (ExplainSpec [String]
es SpecificationD Deps b
s) = [String] -> Specification a -> Specification a
forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String]
es (Specification a -> Specification a)
-> Specification a -> Specification a
forall a b. (a -> b) -> a -> b
$ OrdW as b
-> ListCtx Value as (HOLE a)
-> SpecificationD Deps b
-> Specification a
forall (as :: [*]) b a.
(AppRequires OrdW as b, HasSpec a) =>
OrdW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate OrdW as b
f ListCtx Value as (HOLE a)
ctxt SpecificationD Deps b
s
  propagate OrdW as b
_ ListCtx Value as (HOLE a)
_ SpecificationD Deps b
TrueSpec = Specification a
forall deps a. SpecificationD deps a
TrueSpec
  propagate OrdW as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
msgs) = NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec NonEmpty String
msgs
  propagate OrdW as b
GreaterW (HOLE a a
HOLE :? Value a
x :> List Value as1
Nil) SpecificationD Deps b
spec =
    OrdW '[a, a] Bool
-> ListCtx Value '[a, a] (HOLE a)
-> Specification Bool
-> Specification a
forall (as :: [*]) b a.
(AppRequires OrdW as b, HasSpec a) =>
OrdW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
LessW (Value a
x Value a
-> ListCtx Value '[a] (HOLE a) -> ListCtx Value '[a, a] (HOLE a)
forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:! HOLE a a -> ListCtx Value '[a] (HOLE a)
forall a' a (f :: * -> *). HOLE a' a -> ListCtx f '[a] (HOLE a')
Unary HOLE a a
HOLE a a
forall {k} (a :: k). HOLE a a
HOLE) SpecificationD Deps b
Specification Bool
spec
  propagate OrdW as b
GreaterW (Value a
x :! Unary HOLE a a
HOLE) SpecificationD Deps b
spec =
    OrdW '[a, a] Bool
-> ListCtx Value '[a, a] (HOLE a)
-> Specification Bool
-> Specification a
forall (as :: [*]) b a.
(AppRequires OrdW as b, HasSpec a) =>
OrdW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
LessW (HOLE a a
forall {k} (a :: k). HOLE a a
HOLE HOLE a a -> List Value '[a] -> ListCtx Value '[a, a] (HOLE a)
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? Value a
Value a
x Value a -> List Value '[] -> List Value '[a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Value '[]
forall {k} (f :: k -> *). List f '[]
Nil) SpecificationD Deps b
Specification Bool
spec
  propagate OrdW as b
LessOrEqualW (HOLE a a
HOLE :? Value a
x :> List Value as1
Nil) (SuspendedSpec Var b
v PredD Deps
ps) =
    (Term a -> PredD Deps) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> PredD Deps) -> Specification a)
-> (Term a -> PredD Deps) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> TermD Deps Bool -> BinderD Deps Bool -> PredD Deps
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (OrdW '[a, a] Bool -> List Term '[a, a] -> TermD Deps Bool
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
LessOrEqualW (Term a
v' Term a -> List Term '[a] -> List Term '[a, a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
a
x Term a -> List Term '[] -> List Term '[a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)) (Var b
Var Bool
v Var Bool -> PredD Deps -> BinderD Deps Bool
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> PredD Deps
ps)
  propagate OrdW as b
LessOrEqualW (Value a
x :! Unary HOLE a a
HOLE) (SuspendedSpec Var b
v PredD Deps
ps) =
    (Term a -> PredD Deps) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> PredD Deps) -> Specification a)
-> (Term a -> PredD Deps) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> TermD Deps Bool -> BinderD Deps Bool -> PredD Deps
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (OrdW '[a, a] Bool -> List Term '[a, a] -> TermD Deps Bool
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
LessOrEqualW (a -> TermD Deps a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
x TermD Deps a -> List Term '[a] -> List Term '[a, a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term a
TermD Deps a
v' TermD Deps a -> List Term '[] -> List Term '[a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)) (Var b
Var Bool
v Var Bool -> PredD Deps -> BinderD Deps Bool
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> PredD Deps
ps)
  propagate OrdW as b
LessOrEqualW (HOLE a a
HOLE :? Value a
l :> List Value as1
Nil) SpecificationD Deps b
spec =
    Specification Bool -> (Bool -> Specification a) -> Specification a
forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec SpecificationD Deps b
Specification Bool
spec ((Bool -> Specification a) -> Specification a)
-> (Bool -> Specification a) -> Specification a
forall a b. (a -> b) -> a -> b
$ \case Bool
True -> a -> Specification a
forall a. OrdLike a => a -> Specification a
leqSpec a
a
l; Bool
False -> a -> Specification a
forall a. OrdLike a => a -> Specification a
gtSpec a
a
l
  propagate OrdW as b
LessOrEqualW (Value a
l :! Unary HOLE a a
HOLE) SpecificationD Deps b
spec =
    Specification Bool -> (Bool -> Specification a) -> Specification a
forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec SpecificationD Deps b
Specification Bool
spec ((Bool -> Specification a) -> Specification a)
-> (Bool -> Specification a) -> Specification a
forall a b. (a -> b) -> a -> b
$ \case Bool
True -> a -> Specification a
forall a. OrdLike a => a -> Specification a
geqSpec a
a
l; Bool
False -> a -> Specification a
forall a. OrdLike a => a -> Specification a
ltSpec a
a
l
  propagate OrdW as b
GreaterOrEqualW (HOLE a a
HOLE :? Value a
x :> List Value as1
Nil) SpecificationD Deps b
spec =
    OrdW '[a, a] Bool
-> ListCtx Value '[a, a] (HOLE a)
-> Specification Bool
-> Specification a
forall (as :: [*]) b a.
(AppRequires OrdW as b, HasSpec a) =>
OrdW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
LessOrEqualW (a -> Value a
forall a. Show a => a -> Value a
Value a
x Value a
-> ListCtx Value '[a] (HOLE a) -> ListCtx Value '[a, a] (HOLE a)
forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:! HOLE a a -> ListCtx Value '[a] (HOLE a)
forall a' a (f :: * -> *). HOLE a' a -> ListCtx f '[a] (HOLE a')
Unary HOLE a a
HOLE a a
forall {k} (a :: k). HOLE a a
HOLE) SpecificationD Deps b
Specification Bool
spec
  propagate OrdW as b
GreaterOrEqualW (Value a
x :! Unary HOLE a a
HOLE) SpecificationD Deps b
spec =
    OrdW '[a, a] Bool
-> ListCtx Value '[a, a] (HOLE a)
-> Specification Bool
-> Specification a
forall (as :: [*]) b a.
(AppRequires OrdW as b, HasSpec a) =>
OrdW as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
LessOrEqualW (HOLE a a
forall {k} (a :: k). HOLE a a
HOLE HOLE a a -> List Value '[a] -> ListCtx Value '[a, a] (HOLE a)
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? Value a
Value a
x Value a -> List Value '[] -> List Value '[a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Value '[]
forall {k} (f :: k -> *). List f '[]
Nil) SpecificationD Deps b
Specification Bool
spec
  propagate OrdW as b
LessW (HOLE a a
HOLE :? Value a
x :> List Value as1
Nil) (SuspendedSpec Var b
v PredD Deps
ps) =
    (Term a -> PredD Deps) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> PredD Deps) -> Specification a)
-> (Term a -> PredD Deps) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> TermD Deps Bool -> BinderD Deps Bool -> PredD Deps
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (OrdW '[a, a] Bool -> List Term '[a, a] -> TermD Deps Bool
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
LessW (Term a
v' Term a -> List Term '[a] -> List Term '[a, a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
a
x Term a -> List Term '[] -> List Term '[a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)) (Var b
Var Bool
v Var Bool -> PredD Deps -> BinderD Deps Bool
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> PredD Deps
ps)
  propagate OrdW as b
LessW (Value a
x :! Unary HOLE a a
HOLE) (SuspendedSpec Var b
v PredD Deps
ps) =
    (Term a -> PredD Deps) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> PredD Deps) -> Specification a)
-> (Term a -> PredD Deps) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> TermD Deps Bool -> BinderD Deps Bool -> PredD Deps
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (OrdW '[a, a] Bool -> List Term '[a, a] -> TermD Deps Bool
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App OrdW '[a, a] Bool
forall a. OrdLike a => OrdW '[a, a] Bool
LessW (a -> TermD Deps a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
x TermD Deps a -> List Term '[a] -> List Term '[a, a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term a
TermD Deps a
v' TermD Deps a -> List Term '[] -> List Term '[a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)) (Var b
Var Bool
v Var Bool -> PredD Deps -> BinderD Deps Bool
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> PredD Deps
ps)
  propagate OrdW as b
LessW (HOLE a a
HOLE :? Value a
l :> List Value as1
Nil) SpecificationD Deps b
spec =
    Specification Bool -> (Bool -> Specification a) -> Specification a
forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec SpecificationD Deps b
Specification Bool
spec ((Bool -> Specification a) -> Specification a)
-> (Bool -> Specification a) -> Specification a
forall a b. (a -> b) -> a -> b
$ \case Bool
True -> a -> Specification a
forall a. OrdLike a => a -> Specification a
ltSpec a
a
l; Bool
False -> a -> Specification a
forall a. OrdLike a => a -> Specification a
geqSpec a
a
l
  propagate OrdW as b
LessW (Value a
l :! Unary HOLE a a
HOLE) SpecificationD Deps b
spec =
    Specification Bool -> (Bool -> Specification a) -> Specification a
forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec SpecificationD Deps b
Specification Bool
spec ((Bool -> Specification a) -> Specification a)
-> (Bool -> Specification a) -> Specification a
forall a b. (a -> b) -> a -> b
$ \case Bool
True -> a -> Specification a
forall a. OrdLike a => a -> Specification a
gtSpec a
a
l; Bool
False -> a -> Specification a
forall a. OrdLike a => a -> Specification a
leqSpec a
a
l

caseBoolSpec ::
  HasSpec a => Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec :: forall a.
HasSpec a =>
Specification Bool -> (Bool -> Specification a) -> Specification a
caseBoolSpec Specification Bool
spec Bool -> Specification a
cont = case Specification Bool -> [Bool]
possibleValues Specification Bool
spec of
  [] -> NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"No possible values in caseBoolSpec"])
  [Bool
b] -> Bool -> Specification a
cont Bool
b
  [Bool]
_ -> Specification a
forall a. Monoid a => a
mempty
  where
    -- where possibleValues s = filter (flip conformsToSpec (simplifySpec s)) [True, False]
    -- This will always get the same result, and probably faster since running 2
    -- conformsToSpec on True and False takes less time than simplifying the spec.
    -- Since we are in TheKnot, we could keep the simplifySpec. Is there a good reason to?
    possibleValues :: Specification Bool -> [Bool]
possibleValues Specification Bool
s = (Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Bool -> Specification Bool -> Bool)
-> Specification Bool -> Bool -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Bool -> Specification Bool -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec Specification Bool
s) [Bool
True, Bool
False]

------------------------------------------------------------------------
-- Instances of HasSpec for numeric types
------------------------------------------------------------------------

instance HasSpec Integer where
  type TypeSpec Integer = NumSpec Integer
  emptySpec :: TypeSpec Integer
emptySpec = TypeSpec Integer
NumSpec Integer
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Integer -> TypeSpec Integer -> Specification Integer
combineSpec = TypeSpec Integer -> TypeSpec Integer -> Specification Integer
NumSpec Integer -> NumSpec Integer -> Specification Integer
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Integer -> GenT m Integer
genFromTypeSpec = TypeSpec Integer -> GenT m Integer
NumSpec Integer -> GenT m Integer
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Integer -> Integer -> [Integer]
shrinkWithTypeSpec = TypeSpec Integer -> Integer -> [Integer]
NumSpec Integer -> Integer -> [Integer]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Integer -> TypeSpec Integer -> Bool
conformsTo = Integer -> TypeSpec Integer -> Bool
Integer -> NumSpec Integer -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Integer -> TypeSpec Integer -> PredD Deps
toPreds = Term Integer -> TypeSpec Integer -> PredD Deps
Term Integer -> NumSpec Integer -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Integer -> Specification Integer
cardinalTypeSpec = TypeSpec Integer -> Specification Integer
NumSpec Integer -> Specification Integer
forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec
  guardTypeSpec :: [String] -> TypeSpec Integer -> Specification Integer
guardTypeSpec = [String] -> TypeSpec Integer -> Specification Integer
[String] -> NumSpec Integer -> Specification Integer
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Int where
  type TypeSpec Int = NumSpec Int
  emptySpec :: TypeSpec Int
emptySpec = TypeSpec Int
NumSpec Int
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Int -> TypeSpec Int -> Specification Int
combineSpec = TypeSpec Int -> TypeSpec Int -> Specification Int
NumSpec Int -> NumSpec Int -> Specification Int
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Int -> GenT m Int
genFromTypeSpec = TypeSpec Int -> GenT m Int
NumSpec Int -> GenT m Int
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Int -> Int -> [Int]
shrinkWithTypeSpec = TypeSpec Int -> Int -> [Int]
NumSpec Int -> Int -> [Int]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Int -> TypeSpec Int -> Bool
conformsTo = Int -> TypeSpec Int -> Bool
Int -> NumSpec Int -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Int -> TypeSpec Int -> PredD Deps
toPreds = Term Int -> TypeSpec Int -> PredD Deps
Term Int -> NumSpec Int -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Int -> Specification Integer
cardinalTypeSpec = TypeSpec Int -> Specification Integer
NumSpec Int -> Specification Integer
forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec
  guardTypeSpec :: [String] -> TypeSpec Int -> Specification Int
guardTypeSpec = [String] -> TypeSpec Int -> Specification Int
[String] -> NumSpec Int -> Specification Int
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec (Ratio Integer) where
  type TypeSpec (Ratio Integer) = NumSpec (Ratio Integer)
  emptySpec :: TypeSpec (Ratio Integer)
emptySpec = TypeSpec (Ratio Integer)
NumSpec (Ratio Integer)
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec (Ratio Integer)
-> TypeSpec (Ratio Integer) -> Specification (Ratio Integer)
combineSpec = TypeSpec (Ratio Integer)
-> TypeSpec (Ratio Integer) -> Specification (Ratio Integer)
NumSpec (Ratio Integer)
-> NumSpec (Ratio Integer) -> Specification (Ratio Integer)
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec (Ratio Integer) -> GenT m (Ratio Integer)
genFromTypeSpec = TypeSpec (Ratio Integer) -> GenT m (Ratio Integer)
NumSpec (Ratio Integer) -> GenT m (Ratio Integer)
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec (Ratio Integer) -> Ratio Integer -> [Ratio Integer]
shrinkWithTypeSpec = TypeSpec (Ratio Integer) -> Ratio Integer -> [Ratio Integer]
NumSpec (Ratio Integer) -> Ratio Integer -> [Ratio Integer]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Ratio Integer -> TypeSpec (Ratio Integer) -> Bool
conformsTo = Ratio Integer -> TypeSpec (Ratio Integer) -> Bool
Ratio Integer -> NumSpec (Ratio Integer) -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term (Ratio Integer) -> TypeSpec (Ratio Integer) -> PredD Deps
toPreds = Term (Ratio Integer) -> TypeSpec (Ratio Integer) -> PredD Deps
Term (Ratio Integer) -> NumSpec (Ratio Integer) -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec (Ratio Integer) -> Specification Integer
cardinalTypeSpec TypeSpec (Ratio Integer)
_ = Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
  guardTypeSpec :: [String]
-> TypeSpec (Ratio Integer) -> Specification (Ratio Integer)
guardTypeSpec = [String]
-> TypeSpec (Ratio Integer) -> Specification (Ratio Integer)
[String]
-> NumSpec (Ratio Integer) -> Specification (Ratio Integer)
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Natural where
  type TypeSpec Natural = NumSpec Natural
  emptySpec :: TypeSpec Natural
emptySpec = TypeSpec Natural
NumSpec Natural
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Natural -> TypeSpec Natural -> Specification Natural
combineSpec = TypeSpec Natural -> TypeSpec Natural -> Specification Natural
NumSpec Natural -> NumSpec Natural -> Specification Natural
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Natural -> GenT m Natural
genFromTypeSpec = TypeSpec Natural -> GenT m Natural
NumSpec Natural -> GenT m Natural
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Natural -> Natural -> [Natural]
shrinkWithTypeSpec = TypeSpec Natural -> Natural -> [Natural]
NumSpec Natural -> Natural -> [Natural]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Natural -> TypeSpec Natural -> Bool
conformsTo = Natural -> TypeSpec Natural -> Bool
Natural -> NumSpec Natural -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Natural -> TypeSpec Natural -> PredD Deps
toPreds = Term Natural -> TypeSpec Natural -> PredD Deps
Term Natural -> NumSpec Natural -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Natural -> Specification Integer
cardinalTypeSpec (NumSpecInterval (Natural -> Maybe Natural -> Natural
forall a. a -> Maybe a -> a
fromMaybe Natural
0 -> Natural
lo) (Just Natural
hi)) =
    if Natural
lo Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
hi
      then Integer -> Specification Integer
forall a. a -> Specification a
equalSpec (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Integer) -> Natural -> Integer
forall a b. (a -> b) -> a -> b
$ Natural
hi Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
lo Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1)
      else Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
0
  cardinalTypeSpec TypeSpec Natural
_ = Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
  guardTypeSpec :: [String] -> TypeSpec Natural -> Specification Natural
guardTypeSpec = [String] -> TypeSpec Natural -> Specification Natural
[String] -> NumSpec Natural -> Specification Natural
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Word8 where
  type TypeSpec Word8 = NumSpec Word8
  emptySpec :: TypeSpec Word8
emptySpec = TypeSpec Word8
NumSpec Word8
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Word8 -> TypeSpec Word8 -> Specification Word8
combineSpec = TypeSpec Word8 -> TypeSpec Word8 -> Specification Word8
NumSpec Word8 -> NumSpec Word8 -> Specification Word8
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Word8 -> GenT m Word8
genFromTypeSpec = TypeSpec Word8 -> GenT m Word8
NumSpec Word8 -> GenT m Word8
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Word8 -> Word8 -> [Word8]
shrinkWithTypeSpec = TypeSpec Word8 -> Word8 -> [Word8]
NumSpec Word8 -> Word8 -> [Word8]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Word8 -> TypeSpec Word8 -> Bool
conformsTo = Word8 -> TypeSpec Word8 -> Bool
Word8 -> NumSpec Word8 -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Word8 -> TypeSpec Word8 -> PredD Deps
toPreds = Term Word8 -> TypeSpec Word8 -> PredD Deps
Term Word8 -> NumSpec Word8 -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Word8 -> Specification Integer
cardinalTypeSpec = TypeSpec Word8 -> Specification Integer
NumSpec Word8 -> Specification Integer
forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec
  cardinalTrueSpec :: Specification Integer
cardinalTrueSpec = Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
256
  typeSpecOpt :: TypeSpec Word8 -> [Word8] -> Specification Word8
typeSpecOpt = TypeSpec Word8 -> [Word8] -> Specification Word8
NumSpec Word8 -> [Word8] -> Specification Word8
forall n.
(HasSpec n, TypeSpec n ~ NumSpec n, Bounded n, Integral n) =>
NumSpec n -> [n] -> Specification n
notInNumSpec
  guardTypeSpec :: [String] -> TypeSpec Word8 -> Specification Word8
guardTypeSpec = [String] -> TypeSpec Word8 -> Specification Word8
[String] -> NumSpec Word8 -> Specification Word8
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Word16 where
  type TypeSpec Word16 = NumSpec Word16
  emptySpec :: TypeSpec Word16
emptySpec = TypeSpec Word16
NumSpec Word16
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Word16 -> TypeSpec Word16 -> Specification Word16
combineSpec = TypeSpec Word16 -> TypeSpec Word16 -> Specification Word16
NumSpec Word16 -> NumSpec Word16 -> Specification Word16
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Word16 -> GenT m Word16
genFromTypeSpec = TypeSpec Word16 -> GenT m Word16
NumSpec Word16 -> GenT m Word16
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Word16 -> Word16 -> [Word16]
shrinkWithTypeSpec = TypeSpec Word16 -> Word16 -> [Word16]
NumSpec Word16 -> Word16 -> [Word16]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Word16 -> TypeSpec Word16 -> Bool
conformsTo = Word16 -> TypeSpec Word16 -> Bool
Word16 -> NumSpec Word16 -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Word16 -> TypeSpec Word16 -> PredD Deps
toPreds = Term Word16 -> TypeSpec Word16 -> PredD Deps
Term Word16 -> NumSpec Word16 -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Word16 -> Specification Integer
cardinalTypeSpec = TypeSpec Word16 -> Specification Integer
NumSpec Word16 -> Specification Integer
forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec
  cardinalTrueSpec :: Specification Integer
cardinalTrueSpec = Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
65536
  guardTypeSpec :: [String] -> TypeSpec Word16 -> Specification Word16
guardTypeSpec = [String] -> TypeSpec Word16 -> Specification Word16
[String] -> NumSpec Word16 -> Specification Word16
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Word32 where
  type TypeSpec Word32 = NumSpec Word32
  emptySpec :: TypeSpec Word32
emptySpec = TypeSpec Word32
NumSpec Word32
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Word32 -> TypeSpec Word32 -> Specification Word32
combineSpec = TypeSpec Word32 -> TypeSpec Word32 -> Specification Word32
NumSpec Word32 -> NumSpec Word32 -> Specification Word32
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Word32 -> GenT m Word32
genFromTypeSpec = TypeSpec Word32 -> GenT m Word32
NumSpec Word32 -> GenT m Word32
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Word32 -> Word32 -> [Word32]
shrinkWithTypeSpec = TypeSpec Word32 -> Word32 -> [Word32]
NumSpec Word32 -> Word32 -> [Word32]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Word32 -> TypeSpec Word32 -> Bool
conformsTo = Word32 -> TypeSpec Word32 -> Bool
Word32 -> NumSpec Word32 -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Word32 -> TypeSpec Word32 -> PredD Deps
toPreds = Term Word32 -> TypeSpec Word32 -> PredD Deps
Term Word32 -> NumSpec Word32 -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Word32 -> Specification Integer
cardinalTypeSpec = TypeSpec Word32 -> Specification Integer
NumSpec Word32 -> Specification Integer
forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec
  guardTypeSpec :: [String] -> TypeSpec Word32 -> Specification Word32
guardTypeSpec = [String] -> TypeSpec Word32 -> Specification Word32
[String] -> NumSpec Word32 -> Specification Word32
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Word64 where
  type TypeSpec Word64 = NumSpec Word64
  emptySpec :: TypeSpec Word64
emptySpec = TypeSpec Word64
NumSpec Word64
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Word64 -> TypeSpec Word64 -> Specification Word64
combineSpec = TypeSpec Word64 -> TypeSpec Word64 -> Specification Word64
NumSpec Word64 -> NumSpec Word64 -> Specification Word64
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Word64 -> GenT m Word64
genFromTypeSpec = TypeSpec Word64 -> GenT m Word64
NumSpec Word64 -> GenT m Word64
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Word64 -> Word64 -> [Word64]
shrinkWithTypeSpec = TypeSpec Word64 -> Word64 -> [Word64]
NumSpec Word64 -> Word64 -> [Word64]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Word64 -> TypeSpec Word64 -> Bool
conformsTo = Word64 -> TypeSpec Word64 -> Bool
Word64 -> NumSpec Word64 -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Word64 -> TypeSpec Word64 -> PredD Deps
toPreds = Term Word64 -> TypeSpec Word64 -> PredD Deps
Term Word64 -> NumSpec Word64 -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Word64 -> Specification Integer
cardinalTypeSpec = TypeSpec Word64 -> Specification Integer
NumSpec Word64 -> Specification Integer
forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec
  guardTypeSpec :: [String] -> TypeSpec Word64 -> Specification Word64
guardTypeSpec = [String] -> TypeSpec Word64 -> Specification Word64
[String] -> NumSpec Word64 -> Specification Word64
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Int8 where
  type TypeSpec Int8 = NumSpec Int8
  emptySpec :: TypeSpec Int8
emptySpec = TypeSpec Int8
NumSpec Int8
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Int8 -> TypeSpec Int8 -> Specification Int8
combineSpec = TypeSpec Int8 -> TypeSpec Int8 -> Specification Int8
NumSpec Int8 -> NumSpec Int8 -> Specification Int8
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Int8 -> GenT m Int8
genFromTypeSpec = TypeSpec Int8 -> GenT m Int8
NumSpec Int8 -> GenT m Int8
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Int8 -> Int8 -> [Int8]
shrinkWithTypeSpec = TypeSpec Int8 -> Int8 -> [Int8]
NumSpec Int8 -> Int8 -> [Int8]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Int8 -> TypeSpec Int8 -> Bool
conformsTo = Int8 -> TypeSpec Int8 -> Bool
Int8 -> NumSpec Int8 -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Int8 -> TypeSpec Int8 -> PredD Deps
toPreds = Term Int8 -> TypeSpec Int8 -> PredD Deps
Term Int8 -> NumSpec Int8 -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTrueSpec :: Specification Integer
cardinalTrueSpec = Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
256
  cardinalTypeSpec :: TypeSpec Int8 -> Specification Integer
cardinalTypeSpec = TypeSpec Int8 -> Specification Integer
NumSpec Int8 -> Specification Integer
forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec
  guardTypeSpec :: [String] -> TypeSpec Int8 -> Specification Int8
guardTypeSpec = [String] -> TypeSpec Int8 -> Specification Int8
[String] -> NumSpec Int8 -> Specification Int8
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Int16 where
  type TypeSpec Int16 = NumSpec Int16
  emptySpec :: TypeSpec Int16
emptySpec = TypeSpec Int16
NumSpec Int16
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Int16 -> TypeSpec Int16 -> Specification Int16
combineSpec = TypeSpec Int16 -> TypeSpec Int16 -> Specification Int16
NumSpec Int16 -> NumSpec Int16 -> Specification Int16
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Int16 -> GenT m Int16
genFromTypeSpec = TypeSpec Int16 -> GenT m Int16
NumSpec Int16 -> GenT m Int16
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Int16 -> Int16 -> [Int16]
shrinkWithTypeSpec = TypeSpec Int16 -> Int16 -> [Int16]
NumSpec Int16 -> Int16 -> [Int16]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Int16 -> TypeSpec Int16 -> Bool
conformsTo = Int16 -> TypeSpec Int16 -> Bool
Int16 -> NumSpec Int16 -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Int16 -> TypeSpec Int16 -> PredD Deps
toPreds = Term Int16 -> TypeSpec Int16 -> PredD Deps
Term Int16 -> NumSpec Int16 -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Int16 -> Specification Integer
cardinalTypeSpec = TypeSpec Int16 -> Specification Integer
NumSpec Int16 -> Specification Integer
forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec
  cardinalTrueSpec :: Specification Integer
cardinalTrueSpec = Integer -> Specification Integer
forall a. a -> Specification a
equalSpec Integer
65536
  guardTypeSpec :: [String] -> TypeSpec Int16 -> Specification Int16
guardTypeSpec = [String] -> TypeSpec Int16 -> Specification Int16
[String] -> NumSpec Int16 -> Specification Int16
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Int32 where
  type TypeSpec Int32 = NumSpec Int32
  emptySpec :: TypeSpec Int32
emptySpec = TypeSpec Int32
NumSpec Int32
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Int32 -> TypeSpec Int32 -> Specification Int32
combineSpec = TypeSpec Int32 -> TypeSpec Int32 -> Specification Int32
NumSpec Int32 -> NumSpec Int32 -> Specification Int32
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Int32 -> GenT m Int32
genFromTypeSpec = TypeSpec Int32 -> GenT m Int32
NumSpec Int32 -> GenT m Int32
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Int32 -> Int32 -> [Int32]
shrinkWithTypeSpec = TypeSpec Int32 -> Int32 -> [Int32]
NumSpec Int32 -> Int32 -> [Int32]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Int32 -> TypeSpec Int32 -> Bool
conformsTo = Int32 -> TypeSpec Int32 -> Bool
Int32 -> NumSpec Int32 -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Int32 -> TypeSpec Int32 -> PredD Deps
toPreds = Term Int32 -> TypeSpec Int32 -> PredD Deps
Term Int32 -> NumSpec Int32 -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Int32 -> Specification Integer
cardinalTypeSpec = TypeSpec Int32 -> Specification Integer
NumSpec Int32 -> Specification Integer
forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec
  guardTypeSpec :: [String] -> TypeSpec Int32 -> Specification Int32
guardTypeSpec = [String] -> TypeSpec Int32 -> Specification Int32
[String] -> NumSpec Int32 -> Specification Int32
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Int64 where
  type TypeSpec Int64 = NumSpec Int64
  emptySpec :: TypeSpec Int64
emptySpec = TypeSpec Int64
NumSpec Int64
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Int64 -> TypeSpec Int64 -> Specification Int64
combineSpec = TypeSpec Int64 -> TypeSpec Int64 -> Specification Int64
NumSpec Int64 -> NumSpec Int64 -> Specification Int64
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Int64 -> GenT m Int64
genFromTypeSpec = TypeSpec Int64 -> GenT m Int64
NumSpec Int64 -> GenT m Int64
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Int64 -> Int64 -> [Int64]
shrinkWithTypeSpec = TypeSpec Int64 -> Int64 -> [Int64]
NumSpec Int64 -> Int64 -> [Int64]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Int64 -> TypeSpec Int64 -> Bool
conformsTo = Int64 -> TypeSpec Int64 -> Bool
Int64 -> NumSpec Int64 -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Int64 -> TypeSpec Int64 -> PredD Deps
toPreds = Term Int64 -> TypeSpec Int64 -> PredD Deps
Term Int64 -> NumSpec Int64 -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Int64 -> Specification Integer
cardinalTypeSpec = TypeSpec Int64 -> Specification Integer
NumSpec Int64 -> Specification Integer
forall n.
(Integral n, MaybeBounded n, HasSpec n) =>
NumSpec n -> Specification Integer
cardinalNumSpec
  guardTypeSpec :: [String] -> TypeSpec Int64 -> Specification Int64
guardTypeSpec = [String] -> TypeSpec Int64 -> Specification Int64
[String] -> NumSpec Int64 -> Specification Int64
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec

instance HasSpec Float where
  type TypeSpec Float = NumSpec Float
  emptySpec :: TypeSpec Float
emptySpec = TypeSpec Float
NumSpec Float
forall n. Ord n => NumSpec n
emptyNumSpec
  combineSpec :: TypeSpec Float -> TypeSpec Float -> Specification Float
combineSpec = TypeSpec Float -> TypeSpec Float -> Specification Float
NumSpec Float -> NumSpec Float -> Specification Float
forall n.
(HasSpec n, Ord n, TypeSpec n ~ NumSpec n) =>
NumSpec n -> NumSpec n -> Specification n
combineNumSpec
  genFromTypeSpec :: forall (m :: * -> *).
(HasCallStack, MonadGenError m) =>
TypeSpec Float -> GenT m Float
genFromTypeSpec = TypeSpec Float -> GenT m Float
NumSpec Float -> GenT m Float
forall (m :: * -> *) n.
(MonadGenError m, Show n, Random n, Ord n, Num n,
 MaybeBounded n) =>
NumSpec n -> GenT m n
genFromNumSpec
  shrinkWithTypeSpec :: TypeSpec Float -> Float -> [Float]
shrinkWithTypeSpec = TypeSpec Float -> Float -> [Float]
NumSpec Float -> Float -> [Float]
forall n. Arbitrary n => NumSpec n -> n -> [n]
shrinkWithNumSpec
  conformsTo :: HasCallStack => Float -> TypeSpec Float -> Bool
conformsTo = Float -> TypeSpec Float -> Bool
Float -> NumSpec Float -> Bool
forall n. Ord n => n -> NumSpec n -> Bool
conformsToNumSpec
  toPreds :: Term Float -> TypeSpec Float -> PredD Deps
toPreds = Term Float -> TypeSpec Float -> PredD Deps
Term Float -> NumSpec Float -> PredD Deps
forall n. OrdLike n => Term n -> NumSpec n -> PredD Deps
toPredsNumSpec
  cardinalTypeSpec :: TypeSpec Float -> Specification Integer
cardinalTypeSpec TypeSpec Float
_ = Specification Integer
forall deps a. SpecificationD deps a
TrueSpec
  guardTypeSpec :: [String] -> TypeSpec Float -> Specification Float
guardTypeSpec = [String] -> TypeSpec Float -> Specification Float
[String] -> NumSpec Float -> Specification Float
forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec