{-# 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 #-}

-- The pattern completeness checker is much weaker before ghc-9.0. Rather than introducing redundant
-- cases and turning off the overlap check in newer ghc versions we disable the check for old
-- versions.
#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}  -- Somehow in GHC 8.10.7, Natural can only be imported from GHC.Natural
#endif

module Constrained.NumSpec where

import Constrained.Base (
  HOLE (..),
  HasSpec (..),
  Logic (..),
  Semantics (..),
  Specification (..),
  Syntax (..),
  Term (..),
  appTerm,
  equalSpec,
  explainSpecOpt,
  flipCtx,
  fromSimpleRepSpec,
  memberSpecList,
  notMemberSpec,
  showType,
  typeSpec,
  pattern Unary,
  pattern (:<:),
 )
import Constrained.Conformance ()
import Constrained.Core (unionWithMaybe)
import Constrained.GenT (
  GenT,
  MonadGenError (..),
  genError,
  pureGen,
  sizeT,
 )
import Constrained.Generic (
  HasSimpleRep (..),
  SimpleRep,
 )

import Control.Applicative ((<|>))
import Control.Arrow (first)
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)

-- ====================================================================
-- NumOrdW  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 NumOrdW (dom :: [Type]) (rng :: Type) where
  LessOrEqualW :: OrdLike a => NumOrdW '[a, a] Bool
  LessW :: OrdLike a => NumOrdW '[a, a] Bool
  GreaterOrEqualW :: OrdLike a => NumOrdW '[a, a] Bool
  GreaterW :: OrdLike a => NumOrdW '[a, a] Bool

deriving instance Eq (NumOrdW ds r)

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

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

instance Syntax NumOrdW where
  inFix :: forall (dom :: [*]) rng. NumOrdW dom rng -> Bool
inFix NumOrdW dom rng
LessOrEqualW = Bool
True
  inFix NumOrdW dom rng
LessW = Bool
True
  inFix NumOrdW dom rng
GreaterOrEqualW = Bool
True
  inFix NumOrdW dom rng
GreaterW = Bool
True

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

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

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

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

  gtSpec :: a -> Specification a
  default gtSpec ::
    ( TypeSpec a ~ TypeSpec (SimpleRep a)
    , HasSimpleRep a
    , OrdLike (SimpleRep a)
    ) =>
    a ->
    Specification a
  gtSpec = forall a.
(HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. OrdLike a => a -> Specification a
gtSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just a
l)
  ltSpec :: a -> Specification a
ltSpec a
l
    | Just a
b <- forall a. MaybeBounded a => Maybe a
lowerBound
    , a
l forall a. Eq a => a -> a -> Bool
== a
b =
        forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"ltSpec @" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Typeable a => a -> TypeRep
typeOf a
l) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
l))
    | Bool
otherwise = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just (a
l forall a. Num a => a -> a -> a
- a
1))
  geqSpec :: a -> Specification a
geqSpec a
l = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just a
l) forall a. Maybe a
Nothing
  gtSpec :: a -> Specification a
gtSpec a
l
    | Just a
b <- forall a. MaybeBounded a => Maybe a
upperBound
    , a
l forall a. Eq a => a -> a -> Bool
== a
b =
        forall a. NonEmpty String -> Specification a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"gtSpec @" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Typeable a => a -> TypeRep
typeOf a
l) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
l))
    | Bool
otherwise = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just (a
l forall a. Num a => a -> a -> a
+ a
1)) 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 = forall a. a -> Maybe a
Just forall a. Bounded a => a
minBound

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

newtype Unbounded a = Unbounded a

instance MaybeBounded (Unbounded a) where
  lowerBound :: Maybe (Unbounded a)
lowerBound = forall a. Maybe a
Nothing
  upperBound :: Maybe (Unbounded a)
upperBound = 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 = forall a. a -> Maybe a
Just Natural
0
  upperBound :: Maybe Natural
upperBound = 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'
    | forall {a}. Ord a => Maybe a -> Maybe a -> Bool
isEmpty Maybe n
ml Maybe n
mh = forall {a}. Ord a => Maybe a -> Maybe a -> Bool
isEmpty Maybe n
ml' Maybe n
mh'
    | forall {a}. Ord a => Maybe a -> Maybe a -> Bool
isEmpty Maybe n
ml' Maybe n
mh' = forall {a}. Ord a => Maybe a -> Maybe a -> Bool
isEmpty Maybe n
ml Maybe n
mh
    | Bool
otherwise = Maybe n
ml forall a. Eq a => a -> a -> Bool
== Maybe n
ml' Bool -> Bool -> Bool
&& Maybe n
mh 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 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 forall a. [a] -> [a] -> [a]
++ String
".." forall a. [a] -> [a] -> [a]
++ String
ub
    where
      lb :: String
lb = String
"[" forall a. [a] -> [a] -> [a]
++ forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" forall a. Show a => a -> String
show Maybe n
ml
      ub :: String
ub = forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" forall a. Show a => a -> String
show Maybe n
mu 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' =
    forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval
      (forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe forall a. Ord a => a -> a -> a
max Maybe n
ml Maybe n
ml')
      (forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe 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 = forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval forall a. Maybe a
Nothing 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 <- forall a. Arbitrary a => Gen a
arbitrary
    Maybe a
m' <- forall a. Arbitrary a => Gen a
arbitrary
    forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
10, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall {n}. Ord n => Maybe n -> Maybe n -> NumSpec n
mkLoHiInterval Maybe a
m Maybe a
m'), (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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) = forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
min n
a n
b) (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
max n
a n
b)
      mkLoHiInterval Maybe n
m Maybe n
m' = 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') =
    forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => a -> [a]
shrink (Maybe a
m, Maybe a
m')

instance Arbitrary Natural where
  arbitrary :: Gen Natural
arbitrary = Word -> Natural
wordToNatural forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
abs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
  shrink :: Natural -> [Natural]
shrink Natural
n = [Word -> Natural
wordToNatural Word
w | Word
w <- 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
abs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a g (m :: * -> *). (Uniform a, StatefulGen g m) => g -> m a
uniformM g
g
instance Random Natural where
  randomR :: forall g. RandomGen g => (Natural, Natural) -> g -> (Natural, g)
randomR (Natural
lo, Natural
hi) g
g = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (forall a. Integral a => a -> Integer
toInteger Natural
lo, 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') = forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
     in (Ratio Integer
lo forall a. Num a => a -> a -> a
+ (Ratio Integer
hi forall a. Num a => a -> a -> a
- Ratio Integer
lo) 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') = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((forall a. Num a => a -> a -> a
+ Integer
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
abs) forall a b. (a -> b) -> a -> b
$ forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
        (Integer
n, g
g'') = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0, Integer
d) g
g'
     in (Integer
n 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 = 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 forall a. Ord a => a -> a -> Bool
> n
b = forall a. NonEmpty String -> Specification a
ErrorSpec (String
"NumSpec has low bound greater than hi bound" forall a. a -> [a] -> NonEmpty a
:| ((String
"   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NumSpec n
s) forall a. a -> [a] -> [a]
: [String]
msg))
  | n
a forall a. Eq a => a -> a -> Bool
== n
b = forall a. a -> Specification a
equalSpec n
a
guardNumSpec [String]
_ NumSpec n
s = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec 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' = forall n.
(Ord n, HasSpec n, TypeSpec n ~ NumSpec n) =>
[String] -> NumSpec n -> Specification n
guardNumSpec [String
"when combining two NumSpecs", String
"   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NumSpec n
s, String
"   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NumSpec n
s'] (NumSpec n
s 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 <- forall (m :: * -> *). Monad m => GenT m Int
sizeT
  forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Random a => (a, a) -> Gen a
choose forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
(MonadGenError m, Ord a, Num a, Show a) =>
Maybe a -> Maybe a -> Integer -> m (a, a)
constrainInterval (Maybe n
ml forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
lowerBound) (Maybe n
mu forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. MaybeBounded a => Maybe a
upperBound) (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
_ = 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) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (-a
r', a
r')
    (Just a
l, Maybe a
Nothing)
      | a
l forall a. Ord a => a -> a -> Bool
< a
0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => a -> a -> a
max a
l (forall a. Num a => a -> a
negate a
r'), a
r')
      | Bool
otherwise -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
l, a
l forall a. Num a => a -> a -> a
+ a
2 forall a. Num a => a -> a -> a
* a
r')
    (Maybe a
Nothing, Just a
u)
      | a
u forall a. Ord a => a -> a -> Bool
> a
0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Num a => a -> a
negate a
r', forall a. Ord a => a -> a -> a
min a
u a
r')
      | Bool
otherwise -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
u forall a. Num a => a -> a -> a
- a
r' forall a. Num a => a -> a -> a
- a
r', a
u)
    (Just a
l, Just a
u)
      | a
l forall a. Ord a => a -> a -> Bool
> a
u -> forall (m :: * -> *) a. MonadGenError m => String -> m a
genError (String
"bad interval: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
l forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
u)
      | a
u forall a. Ord a => a -> a -> Bool
< a
0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeSub a
l (forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeSub a
l a
u a
r') a
r', a
u)
      | a
l forall a. Ord a => a -> a -> Bool
>= a
0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
l, forall {p}. (Ord p, Num p) => p -> p -> p -> p
safeAdd a
u (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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => a -> a -> a
max a
l (-a
r'), forall a. Ord a => a -> a -> a
min a
u a
r')
  where
    r' :: a
r' = forall a. Num a => a -> a
abs forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
r
    safeSub :: p -> p -> p -> p
safeSub p
l p
a p
b
      | p
a forall a. Num a => a -> a -> a
- p
b forall a. Ord a => a -> a -> Bool
> p
a = p
l
      | Bool
otherwise = forall a. Ord a => a -> a -> a
max p
l (p
a forall a. Num a => a -> a -> a
- p
b)
    safeAdd :: p -> p -> p -> p
safeAdd p
u p
a p
b
      | p
a forall a. Num a => a -> a -> a
+ p
b forall a. Ord a => a -> a -> Bool
< p
a = p
u
      | Bool
otherwise = forall a. Ord a => a -> a -> a
min p
u (p
a 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) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (forall a. Ord a => a -> a -> Bool
<= n
i) Maybe n
ml Bool -> Bool -> Bool
&& forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (n
i 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 =
  forall {a}. Ord a => Set a -> [a] -> [a]
loop 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 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' = forall a. Ord a => a -> Set a -> Set a
Set.insert a
a Set a
s in Set a
s' seq :: forall a b. a -> b -> b
`seq` 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 =
  forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
    (forall a. Ord a => [a] -> [a]
nubOrd [a]
xs)
    ( forall a. [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 = 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 = 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 forall a. Ord a => a -> a -> Bool
> Maybe n
hi then Integer
0 else forall a. Integral a => a -> Integer
toInteger n
high forall a. Num a => a -> a -> a
- forall a. Integral a => a -> Integer
toInteger n
low forall a. Num a => a -> a -> a
+ Integer
1
  where
    high :: n
high = forall n. Bounded n => Maybe n -> n
highBound Maybe n
hi
    low :: n
low = 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 = forall a. Integral a => a -> Integer
toInteger (forall a. Bounded a => a
maxBound @n) forall a. Num a => a -> a -> a
- forall a. Integral a => a -> Integer
toInteger (forall a. Bounded a => a
minBound @n) 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
  | forall a. Integral a => a -> Integer
toInteger (forall (t :: * -> *) a. Foldable t => t a -> Int
length [n]
bad) forall a. Ord a => a -> a -> Bool
> (forall n. (Integral n, Bounded n) => Integer
finiteSize @n forall a. Integral a => a -> a -> a
`div` Integer
2) Bool -> Bool -> Bool
|| forall n. (Bounded n, Integral n) => NumSpec n -> Integer
countSpec NumSpec n
ns forall a. Ord a => a -> a -> Bool
< forall a. Integral a => a -> Integer
toInteger (forall (t :: * -> *) a. Foldable t => t a -> Int
length [n]
bad) =
      forall a. Ord a => String -> [a] -> Specification a
nubOrdMemberSpec
        (String
"call to: (notInNumSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NumSpec n
ns forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [n]
bad forall a. [a] -> [a] -> [a]
++ String
")")
        [n
x | n
x <- [forall n. Bounded n => Maybe n -> n
lowBound Maybe n
a .. forall n. Bounded n => Maybe n -> n
highBound Maybe n
b], 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 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 forall a. Ord a => a -> a -> Bool
<= n
b = NumSpec n
s
  | Bool
otherwise = forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just n
1) (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) =
  forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
x Maybe n
y forall a b. (a -> b) -> a -> b
$
    forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
a Maybe n
b forall a b. (a -> b) -> a -> b
$
      forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe n
a) (forall a. Num a => a -> a -> a
(+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
y 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) =
  forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
x Maybe n
y forall a b. (a -> b) -> a -> b
$
    forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
a Maybe n
b forall a b. (a -> b) -> a -> b
$
      forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval ((-) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe n
b) ((-) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
y 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) =
  forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
a Maybe n
b forall a b. (a -> b) -> a -> b
$
    forall n.
(Ord n, Num n) =>
Maybe n -> Maybe n -> NumSpec n -> NumSpec n
guardEmpty Maybe n
c Maybe n
d forall a b. (a -> b) -> a -> b
$
      forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall x. T x -> Maybe x
unT (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [T n]
s)) (forall x. T x -> Maybe x
unT (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [T n]
s))
  where
    s :: [T n]
s = [forall x. Num x => T x -> T x -> T x
multT (forall x. Maybe x -> T x
neg Maybe n
a) (forall x. Maybe x -> T x
neg Maybe n
c), forall x. Num x => T x -> T x -> T x
multT (forall x. Maybe x -> T x
neg Maybe n
a) (forall x. Maybe x -> T x
pos Maybe n
d), forall x. Num x => T x -> T x -> T x
multT (forall x. Maybe x -> T x
pos Maybe n
b) (forall x. Maybe x -> T x
neg Maybe n
c), forall x. Num x => T x -> T x -> T x
multT (forall x. Maybe x -> T x
pos Maybe n
b) (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) = forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. Num a => a -> a
negate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
hi) (forall a. Num a => a -> a
negate 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
(+) = forall n. (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
addNumSpec
  (-) = forall n. (Ord n, Num n) => NumSpec n -> NumSpec n -> NumSpec n
subNumSpec
  * :: 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 = forall n. Num n => NumSpec n -> NumSpec n
negNumSpec
  fromInteger :: Integer -> NumSpec Integer
fromInteger Integer
n = forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just (forall a. Num a => Integer -> a
fromInteger Integer
n)) (forall a. a -> Maybe a
Just (forall a. Num a => Integer -> a
fromInteger Integer
n))
  abs :: NumSpec Integer -> NumSpec Integer
abs = forall a. HasCallStack => String -> a
error String
"No abs in the Num (NumSpec  Integer) instance"
  signum :: NumSpec Integer -> NumSpec Integer
signum = 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
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
showList :: [T x] -> ShowS
$cshowList :: forall x. Show x => [T x] -> ShowS
show :: T x -> String
$cshow :: forall x. Show x => T x -> String
showsPrec :: Int -> T x -> ShowS
$cshowsPrec :: forall x. Show x => Int -> T x -> ShowS
Show)

instance Ord x => Eq (T x) where
  T x
x == :: T x -> T x -> Bool
== T x
y = forall a. Ord a => a -> a -> Ordering
compare T x
x T x
y forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord x => Ord (T x) where
  compare :: T x -> T x -> Ordering
compare T x
NegInf T x
NegInf = Ordering
EQ
  compare T x
NegInf T x
_ = Ordering
LT
  compare (Ok x
_) T x
NegInf = Ordering
GT
  compare (Ok x
x) (Ok x
y) = forall a. Ord a => a -> a -> Ordering
compare x
x x
y
  compare (Ok x
_) T x
PosInf = Ordering
LT
  compare T x
PosInf T x
PosInf = Ordering
EQ
  compare T x
PosInf T x
_ = Ordering
GT

-- \| Conversion between (T x) and (Maybe x)
unT :: T x -> Maybe x
unT :: forall x. T x -> Maybe x
unT (Ok x
x) = forall a. a -> Maybe a
Just x
x
unT T 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 = forall x. T x
NegInf
neg (Just x
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 = forall x. T x
PosInf
pos (Just x
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 = forall x. T x
PosInf
multT T x
NegInf T x
PosInf = forall x. T x
NegInf
multT T x
NegInf (Ok x
_) = forall x. T x
NegInf
multT (Ok x
_) T x
NegInf = forall x. T x
NegInf
multT (Ok x
x) (Ok x
y) = forall x. x -> T x
Ok (x
x forall a. Num a => a -> a -> a
* x
y)
multT (Ok x
_) T x
PosInf = forall x. T x
PosInf
multT T x
PosInf T x
PosInf = forall x. T x
PosInf
multT T x
PosInf T x
NegInf = forall x. T x
NegInf
multT T x
PosInf (Ok 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 = forall n.
Number n =>
String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
operateSpec String
" + " forall a. Num a => a -> a -> a
(+) 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 = 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 = forall n.
Number n =>
String
-> (n -> n -> n)
-> (TypeSpec n -> TypeSpec n -> TypeSpec n)
-> Specification n
-> Specification n
-> Specification n
operateSpec String
" * " forall a. Num a => a -> a -> a
(*) 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 = forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es forall a b. (a -> b) -> a -> b
$ 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) = forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es forall a b. (a -> b) -> a -> b
$ 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) -> forall a. NonEmpty String -> Specification a
ErrorSpec (NonEmpty String
xs forall a. Semigroup a => a -> a -> a
<> NonEmpty String
ys)
  (ErrorSpec NonEmpty String
xs, Specification n
_) -> forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
xs
  (Specification n
_, ErrorSpec NonEmpty String
ys) -> forall a. NonEmpty String -> Specification a
ErrorSpec NonEmpty String
ys
  (Specification n
TrueSpec, Specification n
_) -> forall a. Specification a
TrueSpec
  (Specification n
_, Specification n
TrueSpec) -> forall a. Specification a
TrueSpec
  (Specification n
_, SuspendedSpec Var n
_ Pred
_) -> forall a. Specification a
TrueSpec
  (SuspendedSpec Var n
_ Pred
_, Specification n
_) -> forall a. Specification a
TrueSpec
  (TypeSpec TypeSpec n
a [n]
bad1, TypeSpec TypeSpec n
b [n]
bad2) -> 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) ->
    forall a. Ord a => String -> [a] -> Specification a
nubOrdMemberSpec
      (forall a. Show a => a -> String
show Specification n
x forall a. [a] -> [a] -> [a]
++ String
operator forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Specification n
y)
      [n -> n -> n
f n
x1 n
y1 | n
x1 <- forall a. NonEmpty a -> [a]
NE.toList NonEmpty n
xs, n
y1 <- 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 = forall a. NonEmpty a -> [a]
NE.toList NonEmpty n
ys
     in forall a. Ord a => String -> [a] -> Specification a
nubOrdMemberSpec
          (forall a. Show a => a -> String
show Specification n
x forall a. [a] -> [a] -> [a]
++ String
operator forall a. [a] -> [a] -> [a]
++ 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 (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 = forall a. NonEmpty a -> [a]
NE.toList NonEmpty n
ys
     in forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
typeSpecOpt
          (forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (n -> n -> n
f (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [n]
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe n
lo) (n -> n -> n
f (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [n]
xs) 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) -> 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
(+) = forall n.
Number n =>
Specification n -> Specification n -> Specification n
addSpecInt
  (-) = forall n.
Number n =>
Specification n -> Specification n -> Specification n
subSpecInt
  * :: Specification Integer
-> Specification Integer -> Specification Integer
(*) = forall n.
Number n =>
Specification n -> Specification n -> Specification n
multSpecInt
  fromInteger :: Integer -> Specification Integer
fromInteger Integer
n = forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. a -> Maybe a
Just Integer
n) (forall a. a -> Maybe a
Just Integer
n)) []
  abs :: Specification Integer -> Specification Integer
abs Specification Integer
_ = forall a. Specification a
TrueSpec
  signum :: Specification Integer -> Specification Integer
signum Specification Integer
_ = forall a. Specification 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 Specification a
s) = forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (forall a.
(Number Integer, HasSpec a) =>
Specification a -> Specification Integer
cardinality Specification a
s)
cardinality Specification a
TrueSpec = forall a. HasSpec a => Specification Integer
cardinalTrueSpec @a
cardinality (MemberSpec NonEmpty a
es) = forall a. a -> Specification a
equalSpec (forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Eq a => [a] -> [a]
nub (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
es)))
cardinality ErrorSpec {} = forall a. a -> Specification a
equalSpec Integer
0
cardinality (TypeSpec TypeSpec a
s [a]
cant) =
  forall n.
Number n =>
Specification n -> Specification n -> Specification n
subSpecInt
    (forall a. HasSpec a => TypeSpec a -> Specification Integer
cardinalTypeSpec @a TypeSpec a
s)
    (forall a. a -> Specification a
equalSpec (forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ 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) => NumSpec n -> Specification Integer
cardinalNumSpec :: forall n.
(Integral n, MaybeBounded n) =>
NumSpec n -> Specification Integer
cardinalNumSpec (NumSpecInterval (Just n
lo) (Just n
hi)) =
  if n
hi forall a. Ord a => a -> a -> Bool
>= n
lo then forall a. NonEmpty a -> Specification a
MemberSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Integral a => a -> Integer
toInteger n
hi forall a. Num a => a -> a -> a
- forall a. Integral a => a -> Integer
toInteger n
lo forall a. Num a => a -> a -> a
+ Integer
1)) else forall a. NonEmpty a -> Specification a
MemberSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0)
cardinalNumSpec (NumSpecInterval Maybe n
Nothing (Just n
hi)) =
  case forall a. MaybeBounded a => Maybe a
lowerBound @n of
    Just n
lo -> forall a. NonEmpty a -> Specification a
MemberSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Integral a => a -> Integer
toInteger n
hi forall a. Num a => a -> a -> a
- forall a. Integral a => a -> Integer
toInteger n
lo))
    Maybe n
Nothing -> forall a. Specification a
TrueSpec
cardinalNumSpec (NumSpecInterval (Just n
lo) Maybe n
Nothing) =
  case forall a. MaybeBounded a => Maybe a
upperBound @n of
    Just n
hi -> forall a. NonEmpty a -> Specification a
MemberSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Integral a => a -> Integer
toInteger n
hi forall a. Num a => a -> a -> a
- forall a. Integral a => a -> Integer
toInteger n
lo))
    Maybe n
Nothing -> forall a. Specification a
TrueSpec
cardinalNumSpec (NumSpecInterval Maybe n
Nothing Maybe n
Nothing) = forall a. Specification a
TrueSpec

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

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

  negateSpec :: TypeSpec a -> Specification a
  default negateSpec ::
    ( TypeSpec a ~ TypeSpec (SimpleRep a)
    , HasSimpleRep a
    , NumLike (SimpleRep a)
    ) =>
    TypeSpec a ->
    Specification a
  negateSpec = forall a.
(HasSpec a, HasSimpleRep a, TypeSpec a ~ TypeSpec (SimpleRep a)) =>
Specification (SimpleRep a) -> Specification a
fromSimpleRepSpec 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 = forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. NumLike a => a -> a -> Maybe a
safeSubtract @(SimpleRep a) (forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep a
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 = forall a. Num a => a -> a -> a
(+)
  semantics IntW d r
NegateW = 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 forall a. Ord a => a -> a -> Bool
> a
0
    , Maybe a
Nothing <- forall a. NumLike a => a -> a -> Maybe a
safeSubtract a
a a
u =
        forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
          forall a. [a] -> NonEmpty a
NE.fromList
            [ String
"Underflow in subtractSpec (" forall a. [a] -> [a] -> [a]
++ forall {k} (t :: k). Typeable t => String
showType @a forall a. [a] -> [a] -> [a]
++ String
"):"
            , String
"  a = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
a
            , String
"  ts = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeSpec a
ts
            ]
    | Just a
l <- Maybe a
ml
    , a
a forall a. Ord a => a -> a -> Bool
< a
0
    , Maybe a
Nothing <- forall a. NumLike a => a -> a -> Maybe a
safeSubtract a
a a
l =
        forall a. NonEmpty String -> Specification a
ErrorSpec forall a b. (a -> b) -> a -> b
$
          forall a. [a] -> NonEmpty a
NE.fromList
            [ String
"Overflow in subtractSpec (" forall a. [a] -> [a] -> [a]
++ forall {k} (t :: k). Typeable t => String
showType @a forall a. [a] -> [a] -> [a]
++ String
"):"
            , String
"  a = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
a
            , String
"  ts = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeSpec a
ts
            ]
    | Bool
otherwise = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (a -> a -> a
safeSub a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
ml) (a -> a -> a
safeSub a
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 <- forall a. NumLike a => a -> a -> Maybe a
safeSubtract a
a1 a
x = a
r
        | a
a1 forall a. Ord a => a -> a -> Bool
< a
0 = forall a. HasCallStack => Maybe a -> a
fromJust forall a. MaybeBounded a => Maybe a
upperBound
        | Bool
otherwise = forall a. HasCallStack => Maybe a -> a
fromJust forall a. MaybeBounded a => Maybe a
lowerBound
  negateSpec :: TypeSpec a -> Specification a
negateSpec (NumSpecInterval Maybe a
ml Maybe a
mu) = forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec forall a b. (a -> b) -> a -> b
$ forall n. Maybe n -> Maybe n -> NumSpec n
NumSpecInterval (forall a. Num a => a -> a
negate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
mu) (forall a. Num a => a -> a
negate 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 forall a. Ord a => a -> a -> Bool
> a
0
    , Just a
lb <- forall a. MaybeBounded a => Maybe a
lowerBound
    , a
lb forall a. Num a => a -> a -> a
+ a
a forall a. Ord a => a -> a -> Bool
> a
x =
        forall a. Maybe a
Nothing
    | a
a forall a. Ord a => a -> a -> Bool
< a
0
    , Just a
ub <- forall a. MaybeBounded a => Maybe a
upperBound
    , a
ub forall a. Num a => a -> a -> a
+ a
a forall a. Ord a => a -> a -> Bool
< a
x =
        forall a. Maybe a
Nothing
    | Bool
otherwise = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ a
x forall a. Num a => a -> a -> a
- a
a

instance NumLike a => Num (Term a) where
  + :: Term a -> Term a -> Term a
(+) = forall a. NumLike a => Term a -> Term a -> Term a
addFn
  negate :: Term a -> Term a
negate = forall a. NumLike a => Term a -> Term a
negateFn
  fromInteger :: Integer -> Term a
fromInteger = forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger
  * :: 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 = forall a. HasCallStack => String -> a
error String
"abs not implemented for Term Fn Int"
  signum :: Term a -> Term a
signum = 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 = forall a. NumLike a => a -> TypeSpec a -> Specification a
subtractSpec b
i TypeSpec b
ts forall a. Semigroup a => a -> a -> a
<> forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall a. NumLike a => a -> a -> Maybe a
safeSubtract b
i) [b]
cant)
  propagateTypeSpec IntW as b
AddW ListCtx Value as (HOLE a)
ctx TypeSpec b
ts [b]
cant = 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 forall a. NumLike a => IntW '[a, a] a
AddW (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)
ctx) TypeSpec b
ts [b]
cant
  propagateTypeSpec IntW as b
NegateW (Unary HOLE a b
HOLE) TypeSpec b
ts [b]
cant = forall a. NumLike a => TypeSpec a -> Specification a
negateSpec TypeSpec b
ts forall a. Semigroup a => a -> a -> a
<> forall a (f :: * -> *).
(HasSpec a, Foldable f) =>
f a -> Specification a
notMemberSpec (forall a b. (a -> b) -> [a] -> [b]
map forall a. Num a => a -> a
negate [b]
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 =
    forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
      (forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall a. NumLike a => a -> a -> Maybe a
safeSubtract b
i) (forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es))
      ( forall a. [a] -> NonEmpty a
NE.fromList
          [ String
"propagateSpecFn on (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show b
i forall a. [a] -> [a] -> [a]
++ String
" +. HOLE)"
          , String
"The Spec is a MemberSpec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. NonEmpty a -> Specification a
MemberSpec NonEmpty b
es)
          , String
"We can't safely subtract " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show b
i 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 = 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 forall a. NumLike a => IntW '[a, a] a
AddW (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)
ctx) NonEmpty b
es
  propagateMemberSpec IntW as b
NegateW (Unary HOLE a b
HOLE) NonEmpty b
es = forall a. NonEmpty a -> Specification a
MemberSpec forall a b. (a -> b) -> a -> b
$ forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Num a => a -> a
negate NonEmpty b
es

addFn :: forall a. NumLike a => Term a -> Term a -> Term a
addFn :: forall a. NumLike a => Term a -> Term a -> Term a
addFn = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm 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 = forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm forall a. NumLike a => IntW '[a] a
NegateW