{-
   Copyright 2016, Dominic Orchard, Andrew Rice, Mistral Contrastin, Matthew Danish

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
-}

{-

This files gives an executable implementation of the model for
abstract stencil specifications. This model is used to drive both
the specification checking and program synthesis features.

-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE MultiWayIf #-}

module Camfort.Specification.Stencils.Model ( Interval(..)
                                            , Bound(..)
                                            , approxVec
                                            , Offsets(..)
                                            , UnionNF
                                            , vecLength
                                            , unfCompare
                                            , optimise
                                            , maximas
                                            , Approximation(..)
                                            , lowerBound, upperBound
                                            , fromExact
                                            , Multiplicity(..)
                                            , Peelable(..)
                                            ) where

import           Prelude hiding (pred)

import qualified Control.Monad as CM

import           Algebra.Lattice
import qualified Data.List.NonEmpty as NE
import qualified Data.Set as S
import           Data.Foldable
import           Data.SBV
import           Data.Data
import           Data.List (sortBy, nub)
import           Data.Maybe (fromJust)
import qualified Camfort.Specification.Stencils.PartialOrd as PO

import qualified Camfort.Helpers.Vec as V
import System.IO.Unsafe

-- Utility container
class Container a where
  type MemberTyp a
  type CompTyp a

  member :: MemberTyp a -> a -> Bool
  compile :: a -> (CompTyp a -> SBool)

--------------------------------------------------------------------------------
-- Arbitrary sets representing offsets
--------------------------------------------------------------------------------

data Offsets =
    Offsets (S.Set Int64)
  | SetOfIntegers
  deriving Offsets -> Offsets -> Bool
(Offsets -> Offsets -> Bool)
-> (Offsets -> Offsets -> Bool) -> Eq Offsets
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Offsets -> Offsets -> Bool
$c/= :: Offsets -> Offsets -> Bool
== :: Offsets -> Offsets -> Bool
$c== :: Offsets -> Offsets -> Bool
Eq

instance Ord Offsets where
    Offsets Set Int64
s compare :: Offsets -> Offsets -> Ordering
`compare` Offsets Set Int64
s' = Set Int64
s Set Int64 -> Set Int64 -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Set Int64
s'
    Offsets Set Int64
_ `compare` Offsets
SetOfIntegers = Ordering
LT
    Offsets
SetOfIntegers `compare` Offsets Set Int64
_ = Ordering
GT
    Offsets
SetOfIntegers `compare` Offsets
SetOfIntegers = Ordering
EQ

instance Container Offsets where
  type MemberTyp Offsets = Int64
  type CompTyp Offsets = SInt64

  member :: MemberTyp Offsets -> Offsets -> Bool
member MemberTyp Offsets
i (Offsets Set Int64
s) = Int64
MemberTyp Offsets
i Int64 -> Set Int64 -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Int64
s
  member MemberTyp Offsets
_ Offsets
_ = Bool
True

  compile :: Offsets -> CompTyp Offsets -> SBool
compile (Offsets Set Int64
s) CompTyp Offsets
i = SInt64
CompTyp Offsets
i SInt64 -> [SInt64] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` (Int64 -> SInt64) -> [Int64] -> [SInt64]
forall a b. (a -> b) -> [a] -> [b]
map Int64 -> SInt64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Set Int64 -> [Int64]
forall a. Set a -> [a]
S.toList Set Int64
s)
  compile Offsets
SetOfIntegers CompTyp Offsets
_ = SBool
sTrue

instance Lattice Offsets where
  (Offsets Set Int64
s) \/ :: Offsets -> Offsets -> Offsets
\/ (Offsets Set Int64
s') = Set Int64 -> Offsets
Offsets (Set Int64 -> Offsets) -> Set Int64 -> Offsets
forall a b. (a -> b) -> a -> b
$ Set Int64
s Set Int64 -> Set Int64 -> Set Int64
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Set Int64
s'
  Offsets
_ \/ Offsets
_ = Offsets
SetOfIntegers
  (Offsets Set Int64
s) /\ :: Offsets -> Offsets -> Offsets
/\ (Offsets Set Int64
s') = Set Int64 -> Offsets
Offsets (Set Int64 -> Offsets) -> Set Int64 -> Offsets
forall a b. (a -> b) -> a -> b
$ Set Int64
s Set Int64 -> Set Int64 -> Set Int64
forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` Set Int64
s'
  off :: Offsets
off@Offsets{} /\ Offsets
_ = Offsets
off
  Offsets
_ /\ Offsets
o = Offsets
o

instance BoundedJoinSemiLattice Offsets where
  bottom :: Offsets
bottom = Set Int64 -> Offsets
Offsets Set Int64
forall a. Set a
S.empty

instance BoundedMeetSemiLattice Offsets where
  top :: Offsets
top = Offsets
SetOfIntegers

--------------------------------------------------------------------------------
-- Interval as defined in the paper
--------------------------------------------------------------------------------

data Bound = Arbitrary | Standard

-- | Interval data structure assumes the following:
-- 1. The first num. param. is less than the second;
-- 2. For holed intervals, first num. param. <= 0 <= second num. param.;
data Interval a where
  IntervArbitrary :: Int -> Int -> Interval 'Arbitrary
  IntervInfiniteArbitrary :: Interval 'Arbitrary
  IntervHoled     :: Int64 -> Int64 -> Bool -> Interval 'Standard
  IntervInfinite  :: Interval 'Standard

deriving instance Eq (Interval a)

instance Show (Interval 'Standard) where
  show :: Interval 'Standard -> String
show Interval 'Standard
IntervInfinite = String
"IntervInfinite"
  show (IntervHoled Int64
lb Int64
up Bool
p) =
    String
"Interv [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int64 -> String
forall a. Show a => a -> String
show Int64
lb String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int64 -> String
forall a. Show a => a -> String
show Int64
up String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]^" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
p

approxInterv :: Interval 'Arbitrary -> Approximation (Interval 'Standard)
approxInterv :: Interval 'Arbitrary -> Approximation (Interval 'Standard)
approxInterv (IntervArbitrary Int
a Int
b)
  | Int
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
b = String -> Approximation (Interval 'Standard)
forall a. HasCallStack => String -> a
error
    String
"Interval condition violated: lower bound is bigger than the upper bound."
  | Int
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=  Int
0, Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>=  Int
0 = Interval 'Standard -> Approximation (Interval 'Standard)
forall a. a -> Approximation a
Exact  (Interval 'Standard -> Approximation (Interval 'Standard))
-> Interval 'Standard -> Approximation (Interval 'Standard)
forall a b. (a -> b) -> a -> b
$ Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled Int64
a' Int64
b' Bool
True
  | Int
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= -Int
1, Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== -Int
1 = Interval 'Standard -> Approximation (Interval 'Standard)
forall a. a -> Approximation a
Exact  (Interval 'Standard -> Approximation (Interval 'Standard))
-> Interval 'Standard -> Approximation (Interval 'Standard)
forall a b. (a -> b) -> a -> b
$ Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled Int64
a' Int64
0  Bool
False
  | Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==  Int
1, Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>=  Int
1 = Interval 'Standard -> Approximation (Interval 'Standard)
forall a. a -> Approximation a
Exact  (Interval 'Standard -> Approximation (Interval 'Standard))
-> Interval 'Standard -> Approximation (Interval 'Standard)
forall a b. (a -> b) -> a -> b
$ Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled Int64
0  Int64
b' Bool
False
  | Int
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>   Int
1, Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>   Int
1 = Maybe (Interval 'Standard)
-> Maybe (Interval 'Standard) -> Approximation (Interval 'Standard)
forall a. Maybe a -> Maybe a -> Approximation a
Bound Maybe (Interval 'Standard)
forall a. Maybe a
Nothing (Maybe (Interval 'Standard) -> Approximation (Interval 'Standard))
-> Maybe (Interval 'Standard) -> Approximation (Interval 'Standard)
forall a b. (a -> b) -> a -> b
$ Interval 'Standard -> Maybe (Interval 'Standard)
forall a. a -> Maybe a
Just (Interval 'Standard -> Maybe (Interval 'Standard))
-> Interval 'Standard -> Maybe (Interval 'Standard)
forall a b. (a -> b) -> a -> b
$ Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled Int64
0  Int64
b' Bool
False
  | Int
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<  -Int
1, Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<  -Int
1 = Maybe (Interval 'Standard)
-> Maybe (Interval 'Standard) -> Approximation (Interval 'Standard)
forall a. Maybe a -> Maybe a -> Approximation a
Bound Maybe (Interval 'Standard)
forall a. Maybe a
Nothing (Maybe (Interval 'Standard) -> Approximation (Interval 'Standard))
-> Maybe (Interval 'Standard) -> Approximation (Interval 'Standard)
forall a b. (a -> b) -> a -> b
$ Interval 'Standard -> Maybe (Interval 'Standard)
forall a. a -> Maybe a
Just (Interval 'Standard -> Maybe (Interval 'Standard))
-> Interval 'Standard -> Maybe (Interval 'Standard)
forall a b. (a -> b) -> a -> b
$ Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled Int64
a' Int64
0  Bool
False
  | Bool
otherwise = String -> Approximation (Interval 'Standard)
forall a. HasCallStack => String -> a
error String
"Impossible: All posibilities are covered."
  where
    a' :: Int64
a' = Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
a
    b' :: Int64
b' = Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b
approxInterv Interval 'Arbitrary
IntervInfiniteArbitrary = Interval 'Standard -> Approximation (Interval 'Standard)
forall a. a -> Approximation a
Exact Interval 'Standard
IntervInfinite

approxVec :: forall n .
             V.Vec n (Interval 'Arbitrary)
          -> Approximation (V.Vec n (Interval 'Standard))
approxVec :: Vec n (Interval 'Arbitrary)
-> Approximation (Vec n (Interval 'Standard))
approxVec Vec n (Interval 'Arbitrary)
v =
  case Vec n (Approximation (Interval 'Standard)) -> ([Int], [Int])
forall (n' :: Nat).
Vec n' (Approximation (Interval 'Standard)) -> ([Int], [Int])
findApproxIntervs Vec n (Approximation (Interval 'Standard))
stdVec of
    ([],[Int]
_) -> Vec n (Interval 'Standard)
-> Approximation (Vec n (Interval 'Standard))
forall a. a -> Approximation a
Exact (Vec n (Interval 'Standard)
 -> Approximation (Vec n (Interval 'Standard)))
-> (Vec n (Approximation (Interval 'Standard))
    -> Vec n (Interval 'Standard))
-> Vec n (Approximation (Interval 'Standard))
-> Approximation (Vec n (Interval 'Standard))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Approximation (Interval 'Standard) -> Interval 'Standard)
-> Vec n (Approximation (Interval 'Standard))
-> Vec n (Interval 'Standard)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Approximation (Interval 'Standard) -> Interval 'Standard
forall a. Approximation a -> a
fromExact (Vec n (Approximation (Interval 'Standard))
 -> Approximation (Vec n (Interval 'Standard)))
-> Vec n (Approximation (Interval 'Standard))
-> Approximation (Vec n (Interval 'Standard))
forall a b. (a -> b) -> a -> b
$ Vec n (Approximation (Interval 'Standard))
stdVec
    ([Int], [Int])
_      -> Maybe (Vec n (Interval 'Standard))
-> Maybe (Vec n (Interval 'Standard))
-> Approximation (Vec n (Interval 'Standard))
forall a. Maybe a -> Maybe a -> Approximation a
Bound Maybe (Vec n (Interval 'Standard))
forall a. Maybe a
Nothing (Vec n (Interval 'Standard) -> Maybe (Vec n (Interval 'Standard))
forall a. a -> Maybe a
Just (Vec n (Interval 'Standard) -> Maybe (Vec n (Interval 'Standard)))
-> Vec n (Interval 'Standard) -> Maybe (Vec n (Interval 'Standard))
forall a b. (a -> b) -> a -> b
$ Approximation (Interval 'Standard) -> Interval 'Standard
forall a. Approximation a -> a
upperBound (Approximation (Interval 'Standard) -> Interval 'Standard)
-> Vec n (Approximation (Interval 'Standard))
-> Vec n (Interval 'Standard)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec n (Approximation (Interval 'Standard))
stdVec)
  where
    stdVec :: V.Vec n (Approximation (Interval 'Standard))
    stdVec :: Vec n (Approximation (Interval 'Standard))
stdVec = (Interval 'Arbitrary -> Approximation (Interval 'Standard))
-> Vec n (Interval 'Arbitrary)
-> Vec n (Approximation (Interval 'Standard))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Interval 'Arbitrary -> Approximation (Interval 'Standard)
approxInterv Vec n (Interval 'Arbitrary)
v

    findApproxIntervs :: forall n' . V.Vec n' (Approximation (Interval 'Standard))
                      -> ([ Int ], [ Int ])
    findApproxIntervs :: Vec n' (Approximation (Interval 'Standard)) -> ([Int], [Int])
findApproxIntervs Vec n' (Approximation (Interval 'Standard))
v' = Int
-> Vec n' (Approximation (Interval 'Standard))
-> ([Int], [Int])
-> ([Int], [Int])
forall (n' :: Nat).
Int
-> Vec n' (Approximation (Interval 'Standard))
-> ([Int], [Int])
-> ([Int], [Int])
findApproxIntervs' Int
0 Vec n' (Approximation (Interval 'Standard))
v' ([],[])

    findApproxIntervs' :: forall n' . Int
                       -> V.Vec n' (Approximation (Interval 'Standard))
                       -> ([ Int ], [ Int ])
                       -> ([ Int ], [ Int ])
    findApproxIntervs' :: Int
-> Vec n' (Approximation (Interval 'Standard))
-> ([Int], [Int])
-> ([Int], [Int])
findApproxIntervs' Int
_ Vec n' (Approximation (Interval 'Standard))
V.Nil ([Int], [Int])
acc = ([Int], [Int])
acc
    findApproxIntervs' Int
i (V.Cons Approximation (Interval 'Standard)
x Vec n (Approximation (Interval 'Standard))
xs) ([Int]
bixs, [Int]
eixs) =
      Int
-> Vec n (Approximation (Interval 'Standard))
-> ([Int], [Int])
-> ([Int], [Int])
forall (n' :: Nat).
Int
-> Vec n' (Approximation (Interval 'Standard))
-> ([Int], [Int])
-> ([Int], [Int])
findApproxIntervs' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Vec n (Approximation (Interval 'Standard))
xs (([Int], [Int]) -> ([Int], [Int]))
-> ([Int], [Int]) -> ([Int], [Int])
forall a b. (a -> b) -> a -> b
$
        case Approximation (Interval 'Standard)
x of
          Bound{} -> (Int
iInt -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[Int]
bixs, [Int]
eixs)
          Exact{} -> ([Int]
bixs, Int
iInt -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[Int]
eixs)

instance Container (Interval 'Standard) where
  type MemberTyp (Interval 'Standard) = Int64
  type CompTyp (Interval 'Standard) = SInt64

  member :: MemberTyp (Interval 'Standard) -> Interval 'Standard -> Bool
member MemberTyp (Interval 'Standard)
0 (IntervHoled Int64
_ Int64
_ Bool
b) = Bool
b
  member MemberTyp (Interval 'Standard)
i (IntervHoled Int64
a Int64
b Bool
_) = Int64
MemberTyp (Interval 'Standard)
i Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int64
a Bool -> Bool -> Bool
&& Int64
MemberTyp (Interval 'Standard)
i Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int64
b
  member MemberTyp (Interval 'Standard)
_ Interval 'Standard
_ = Bool
True

  compile :: Interval 'Standard -> CompTyp (Interval 'Standard) -> SBool
compile (IntervHoled Int64
i1 Int64
i2 Bool
b) CompTyp (Interval 'Standard)
i
    | Bool
b = SInt64 -> (SInt64, SInt64) -> SBool
forall a. OrdSymbolic a => a -> (a, a) -> SBool
inRange SInt64
CompTyp (Interval 'Standard)
i (SInt64, SInt64)
range
    | Bool
otherwise = SInt64 -> (SInt64, SInt64) -> SBool
forall a. OrdSymbolic a => a -> (a, a) -> SBool
inRange SInt64
CompTyp (Interval 'Standard)
i (SInt64, SInt64)
range SBool -> SBool -> SBool
.&& SInt64
CompTyp (Interval 'Standard)
i SInt64 -> SInt64 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInt64
0
    where
      range :: (SInt64, SInt64)
range = (Int64 -> SInt64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
i1, Int64 -> SInt64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
i2)
  compile Interval 'Standard
IntervInfinite CompTyp (Interval 'Standard)
_ = SBool
sTrue

instance Lattice (Interval 'Standard) where
  (IntervHoled Int64
lb Int64
ub Bool
noHole) \/ :: Interval 'Standard -> Interval 'Standard -> Interval 'Standard
\/ (IntervHoled Int64
lb' Int64
ub' Bool
noHole') =
    Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled (Int64 -> Int64 -> Int64
forall a. Ord a => a -> a -> a
min Int64
lb Int64
lb') (Int64 -> Int64 -> Int64
forall a. Ord a => a -> a -> a
max Int64
ub Int64
ub') (Bool
noHole Bool -> Bool -> Bool
|| Bool
noHole')
  Interval 'Standard
_ \/ Interval 'Standard
_ = Interval 'Standard
forall a. BoundedMeetSemiLattice a => a
top
  (IntervHoled Int64
lb Int64
ub Bool
noHole) /\ :: Interval 'Standard -> Interval 'Standard -> Interval 'Standard
/\ (IntervHoled Int64
lb' Int64
ub' Bool
noHole') =
    Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled (Int64 -> Int64 -> Int64
forall a. Ord a => a -> a -> a
max Int64
lb Int64
lb') (Int64 -> Int64 -> Int64
forall a. Ord a => a -> a -> a
min Int64
ub Int64
ub') (Bool
noHole Bool -> Bool -> Bool
&& Bool
noHole')
  int :: Interval 'Standard
int@IntervHoled{} /\ Interval 'Standard
_ = Interval 'Standard
int
  Interval 'Standard
_ /\ Interval 'Standard
int = Interval 'Standard
int

instance BoundedJoinSemiLattice (Interval 'Standard) where
  bottom :: Interval 'Standard
bottom = Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled Int64
0 Int64
0 Bool
False

instance BoundedMeetSemiLattice (Interval 'Standard) where
  top :: Interval 'Standard
top = Interval 'Standard
IntervInfinite

-- instance BoundedLattice (Interval 'Standard)

--------------------------------------------------------------------------------
-- Union of cartesian products normal form
--------------------------------------------------------------------------------

type UnionNF n a = NE.NonEmpty (V.Vec n a)

vecLength :: UnionNF n a -> V.Natural n
vecLength :: UnionNF n a -> Natural n
vecLength = Vec n a -> Natural n
forall (n :: Nat) a. Vec n a -> Natural n
V.lengthN (Vec n a -> Natural n)
-> (UnionNF n a -> Vec n a) -> UnionNF n a -> Natural n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionNF n a -> Vec n a
forall a. NonEmpty a -> a
NE.head

instance Container a => Container (UnionNF n a) where
  type MemberTyp (UnionNF n a) = V.Vec n (MemberTyp a)
  type CompTyp (UnionNF n a) = V.Vec n (CompTyp a)
  member :: MemberTyp (UnionNF n a) -> UnionNF n a -> Bool
member MemberTyp (UnionNF n a)
is = (Vec n a -> Bool) -> UnionNF n a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Vec n (MemberTyp a) -> Vec n a -> Bool
forall a (n :: Nat).
Container a =>
Vec n (MemberTyp a) -> Vec n a -> Bool
member' Vec n (MemberTyp a)
MemberTyp (UnionNF n a)
is)
    where
      member' :: Vec n (MemberTyp a) -> Vec n a -> Bool
member' Vec n (MemberTyp a)
is' Vec n a
space = Vec n Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (Vec n Bool -> Bool) -> Vec n Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (MemberTyp a -> a -> Bool)
-> Vec n (MemberTyp a) -> Vec n a -> Vec n Bool
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
V.zipWith MemberTyp a -> a -> Bool
forall a. Container a => MemberTyp a -> a -> Bool
member Vec n (MemberTyp a)
is' Vec n a
space

  compile :: UnionNF n a -> CompTyp (UnionNF n a) -> SBool
compile UnionNF n a
spaces CompTyp (UnionNF n a)
is = (SBool -> SBool -> SBool) -> NonEmpty SBool -> SBool
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SBool -> SBool -> SBool
(.||) (NonEmpty SBool -> SBool) -> NonEmpty SBool -> SBool
forall a b. (a -> b) -> a -> b
$ (Vec n a -> SBool) -> UnionNF n a -> NonEmpty SBool
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (Vec n a -> Vec n (CompTyp a) -> SBool
forall a (n :: Nat).
Container a =>
Vec n a -> Vec n (CompTyp a) -> SBool
`compile'` Vec n (CompTyp a)
CompTyp (UnionNF n a)
is) UnionNF n a
spaces
    where
      compile' :: Vec n a -> Vec n (CompTyp a) -> SBool
compile' Vec n a
space Vec n (CompTyp a)
is' =
        ((a, CompTyp a) -> SBool -> SBool)
-> SBool -> Vec n (a, CompTyp a) -> SBool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' (\(a
set, CompTyp a
i) -> SBool -> SBool -> SBool
(.&&) (SBool -> SBool -> SBool) -> SBool -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ a -> CompTyp a -> SBool
forall a. Container a => a -> CompTyp a -> SBool
compile a
set CompTyp a
i) SBool
sTrue (Vec n (a, CompTyp a) -> SBool) -> Vec n (a, CompTyp a) -> SBool
forall a b. (a -> b) -> a -> b
$ Vec n a -> Vec n (CompTyp a) -> Vec n (a, CompTyp a)
forall (n :: Nat) a b. Vec n a -> Vec n b -> Vec n (a, b)
V.zip Vec n a
space Vec n (CompTyp a)
is'

instance BoundedMeetSemiLattice a => Lattice (UnionNF n a) where
  UnionNF n a
oi \/ :: UnionNF n a -> UnionNF n a -> UnionNF n a
\/ UnionNF n a
oi' = UnionNF n a
oi UnionNF n a -> UnionNF n a -> UnionNF n a
forall a. Semigroup a => a -> a -> a
<> UnionNF n a
oi'
  /\ :: UnionNF n a -> UnionNF n a -> UnionNF n a
(/\) = (Vec n a -> Vec n a -> Vec n a)
-> UnionNF n a -> UnionNF n a -> UnionNF n a
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
CM.liftM2 ((a -> a -> a) -> Vec n a -> Vec n a -> Vec n a
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
V.zipWith a -> a -> a
forall a. Lattice a => a -> a -> a
(/\))

unfCompare :: forall a b n . ( Container a,          Container b
                             , MemberTyp a ~ Int64,  MemberTyp b ~ Int64
                             , CompTyp a ~ SInt64,   CompTyp b ~ SInt64
                             )
           => UnionNF n a -> UnionNF n b -> Ordering
unfCompare :: UnionNF n a -> UnionNF n b -> Ordering
unfCompare UnionNF n a
oi UnionNF n b
oi' = IO Ordering -> Ordering
forall a. IO a -> a
unsafePerformIO (IO Ordering -> Ordering) -> IO Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ do
    ThmResult
thmRes <- Predicate -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove Predicate
pred
    case ThmResult
thmRes of
      -- Tell the user if there was a hard proof error (e.g., if
      -- z3 is not installed/accessible).
      -- TODO: give more information
      ThmResult (ProofError SMTConfig
_ [String]
msgs Maybe SMTResult
_) -> String -> IO Ordering
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO Ordering) -> String -> IO Ordering
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
msgs
      ThmResult
_ ->
        if ThmResult -> Bool
forall a. Modelable a => a -> Bool
modelExists ThmResult
thmRes
        then do
          [Int64]
ce <- ThmResult -> IO [Int64]
counterExample ThmResult
thmRes
          case [Int64] -> VecBox Int64
forall a. [a] -> VecBox a
V.fromList [Int64]
ce of
             V.VecBox Vec n Int64
cev ->
               case Vec n a -> Vec n Int64 -> Maybe (EqT n n)
forall (n :: Nat) a (m :: Nat) b.
Vec n a -> Vec m b -> Maybe (EqT m n)
V.proveEqSize (UnionNF n a -> Vec n a
forall a. NonEmpty a -> a
NE.head UnionNF n a
oi) Vec n Int64
cev of
                 Just EqT n n
V.ReflEq ->
                   -- TODO: The second branch is defensive programming the
                   -- member check is not necessary unless the counter example
                   -- is bogus (it shouldn't be). Delete if it adversely
                   -- effects the performance.
                   if | Vec n Int64
MemberTyp (UnionNF n a)
cev MemberTyp (UnionNF n a) -> UnionNF n a -> Bool
forall a. Container a => MemberTyp a -> a -> Bool
`member` UnionNF n a
oi  -> Ordering -> IO Ordering
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
GT
                      | Vec n Int64
MemberTyp (UnionNF n b)
cev MemberTyp (UnionNF n b) -> UnionNF n b -> Bool
forall a. Container a => MemberTyp a -> a -> Bool
`member` UnionNF n b
oi' -> Ordering -> IO Ordering
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
LT
                      | Bool
otherwise -> String -> IO Ordering
forall (m :: * -> *) a. MonadFail m => String -> m a
fail
                         String
"Impossible: counter example is in \
                          \neither of the operands"
                 Maybe (EqT n n)
Nothing -> String -> IO Ordering
forall (m :: * -> *) a. MonadFail m => String -> m a
fail
                    String
"Impossible: Counter example size doesn't \
                    \match the original vector size."
        else Ordering -> IO Ordering
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
EQ
  where
    counterExample :: ThmResult -> IO [ Int64 ]
    counterExample :: ThmResult -> IO [Int64]
counterExample ThmResult
thmRes =
      case ThmResult -> Either String (Bool, [Int64])
forall a b.
(Modelable a, SatModel b) =>
a -> Either String (Bool, b)
getModelAssignment ThmResult
thmRes of
        Right (Bool
False, [Int64]
ce) -> [Int64] -> IO [Int64]
forall (m :: * -> *) a. Monad m => a -> m a
return [Int64]
ce
        Right (Bool
True, [Int64]
_) -> String -> IO [Int64]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Returned probable model."
        Left String
str -> String -> IO [Int64]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
str

    pred :: Predicate
    pred :: Predicate
pred = do
      [SInt64]
freeVars <- (Int -> Symbolic [SInt64]
forall a. SymVal a => Int -> Symbolic [SBV a]
mkFreeVars (Int -> Symbolic [SInt64])
-> (UnionNF n a -> Int) -> UnionNF n a -> Symbolic [SInt64]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionNF n a -> Int
forall (n :: Nat) a. NonEmpty (Vec n a) -> Int
dimensionality) UnionNF n a
oi :: Symbolic [ SInt64 ]
      case [SInt64] -> VecBox SInt64
forall a. [a] -> VecBox a
V.fromList [SInt64]
freeVars of
        V.VecBox Vec n SInt64
freeVarVec ->
          case Vec n a -> Vec n SInt64 -> Maybe (EqT n n)
forall (n :: Nat) a (m :: Nat) b.
Vec n a -> Vec m b -> Maybe (EqT m n)
V.proveEqSize (UnionNF n a -> Vec n a
forall a. NonEmpty a -> a
NE.head UnionNF n a
oi) Vec n SInt64
freeVarVec of
            Just EqT n n
V.ReflEq -> SBool -> Predicate
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> Predicate) -> SBool -> Predicate
forall a b. (a -> b) -> a -> b
$
              UnionNF n a -> CompTyp (UnionNF n a) -> SBool
forall a. Container a => a -> CompTyp a -> SBool
compile UnionNF n a
oi Vec n SInt64
CompTyp (UnionNF n a)
freeVarVec SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== UnionNF n b -> CompTyp (UnionNF n b) -> SBool
forall a. Container a => a -> CompTyp a -> SBool
compile UnionNF n b
oi' Vec n SInt64
CompTyp (UnionNF n b)
freeVarVec
            Maybe (EqT n n)
Nothing -> String -> Predicate
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Predicate) -> String -> Predicate
forall a b. (a -> b) -> a -> b
$
              String
"Impossible: Free variables size doesn't match that of the " String -> ShowS
forall a. [a] -> [a] -> [a]
++
              String
"union parameter."
    dimensionality :: NonEmpty (Vec n a) -> Int
dimensionality = Vec n a -> Int
forall (n :: Nat) a. Vec n a -> Int
V.length (Vec n a -> Int)
-> (NonEmpty (Vec n a) -> Vec n a) -> NonEmpty (Vec n a) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (Vec n a) -> Vec n a
forall a. NonEmpty a -> a
NE.head

--------------------------------------------------------------------------------
-- Optimise unions
--------------------------------------------------------------------------------

instance PO.PartialOrd Offsets where
  (Offsets Set Int64
s) <= :: Offsets -> Offsets -> Bool
<= (Offsets Set Int64
s') = Set Int64
s Set Int64 -> Set Int64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Set Int64
s'
  Offsets
SetOfIntegers <= Offsets{} = Bool
False
  Offsets
_ <= Offsets
SetOfIntegers = Bool
True

instance PO.PartialOrd (Interval 'Standard) where
  (IntervHoled Int64
lb Int64
ub Bool
p) <= :: Interval 'Standard -> Interval 'Standard -> Bool
<= (IntervHoled Int64
lb' Int64
ub' Bool
p') =
    (Bool
p' Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
p) Bool -> Bool -> Bool
&& Int64
lb Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int64
lb' Bool -> Bool -> Bool
&& Int64
ub Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int64
ub'
  Interval 'Standard
IntervInfinite <= IntervHoled{} = Bool
False
  Interval 'Standard
_ <= Interval 'Standard
IntervInfinite = Bool
True

instance PO.PartialOrd a => PO.PartialOrd (V.Vec n a) where
  Vec n a
v <= :: Vec n a -> Vec n a -> Bool
<= Vec n a
v' = Vec n Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (Vec n Bool -> Bool) -> Vec n Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (a -> a -> Bool) -> Vec n a -> Vec n a -> Vec n Bool
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
V.zipWith a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
(PO.<=) Vec n a
v Vec n a
v'

optimise :: UnionNF n (Interval 'Standard) -> UnionNF n (Interval 'Standard)
optimise :: UnionNF n (Interval 'Standard) -> UnionNF n (Interval 'Standard)
optimise = [Vec n (Interval 'Standard)] -> UnionNF n (Interval 'Standard)
forall a. [a] -> NonEmpty a
NE.fromList ([Vec n (Interval 'Standard)] -> UnionNF n (Interval 'Standard))
-> (UnionNF n (Interval 'Standard) -> [Vec n (Interval 'Standard)])
-> UnionNF n (Interval 'Standard)
-> UnionNF n (Interval 'Standard)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
forall (n :: Nat).
[Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
maximas ([Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)])
-> (UnionNF n (Interval 'Standard) -> [Vec n (Interval 'Standard)])
-> UnionNF n (Interval 'Standard)
-> [Vec n (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
forall (n :: Nat).
[Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
fixedPointUnion ([Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)])
-> (UnionNF n (Interval 'Standard) -> [Vec n (Interval 'Standard)])
-> UnionNF n (Interval 'Standard)
-> [Vec n (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionNF n (Interval 'Standard) -> [Vec n (Interval 'Standard)]
forall a. NonEmpty a -> [a]
NE.toList
  where
    fixedPointUnion :: [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
fixedPointUnion [Vec n (Interval 'Standard)]
unf =
      let unf' :: [Vec n (Interval 'Standard)]
unf' = [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
forall (n :: Nat).
[Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
unionLemma ([Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)])
-> ([Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)])
-> [Vec n (Interval 'Standard)]
-> [Vec n (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
forall (n :: Nat).
[Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
maximas ([Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)])
-> [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
forall a b. (a -> b) -> a -> b
$ [Vec n (Interval 'Standard)]
unf
      in if [Vec n (Interval 'Standard)]
unf' [Vec n (Interval 'Standard)]
-> [Vec n (Interval 'Standard)] -> Bool
forall a. Eq a => a -> a -> Bool
== [Vec n (Interval 'Standard)]
unf then [Vec n (Interval 'Standard)]
unf' else [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
fixedPointUnion [Vec n (Interval 'Standard)]
unf'

sensibleGroupBy :: Eq a =>
                   (a -> a -> Ordering)
                -> (a -> a -> Bool)
                -> [ a ]
                -> [ [ a ] ]
sensibleGroupBy :: (a -> a -> Ordering) -> (a -> a -> Bool) -> [a] -> [[a]]
sensibleGroupBy a -> a -> Ordering
ord a -> a -> Bool
p [a]
l = [[a]] -> [[a]]
forall a. Eq a => [a] -> [a]
nub ([[a]] -> [[a]]) -> ([a] -> [[a]]) -> [a] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> [a]) -> [a] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (\a
el -> (a -> a -> Ordering) -> [a] -> [a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy a -> a -> Ordering
ord ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (a -> a -> Bool
p a
el) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ [a]
l) ([a] -> [[a]]) -> [a] -> [[a]]
forall a b. (a -> b) -> a -> b
$ [a]
l

maximas :: [ V.Vec n (Interval 'Standard) ] -> [ V.Vec n (Interval 'Standard) ]
maximas :: [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
maximas = [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
forall a. Eq a => [a] -> [a]
nub
        ([Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)])
-> ([Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)])
-> [Vec n (Interval 'Standard)]
-> [Vec n (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Vec n (Interval 'Standard)] -> Vec n (Interval 'Standard))
-> [[Vec n (Interval 'Standard)]] -> [Vec n (Interval 'Standard)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Vec n (Interval 'Standard)] -> Vec n (Interval 'Standard)
forall a. [a] -> a
head ([Vec n (Interval 'Standard)] -> Vec n (Interval 'Standard))
-> ([Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)])
-> [Vec n (Interval 'Standard)]
-> Vec n (Interval 'Standard)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
forall a. PartialOrd a => [a] -> [a]
PO.maxima)
        ([[Vec n (Interval 'Standard)]] -> [Vec n (Interval 'Standard)])
-> ([Vec n (Interval 'Standard)] -> [[Vec n (Interval 'Standard)]])
-> [Vec n (Interval 'Standard)]
-> [Vec n (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec n (Interval 'Standard)
 -> Vec n (Interval 'Standard) -> Ordering)
-> (Vec n (Interval 'Standard)
    -> Vec n (Interval 'Standard) -> Bool)
-> [Vec n (Interval 'Standard)]
-> [[Vec n (Interval 'Standard)]]
forall a.
Eq a =>
(a -> a -> Ordering) -> (a -> a -> Bool) -> [a] -> [[a]]
sensibleGroupBy Vec n (Interval 'Standard)
-> Vec n (Interval 'Standard) -> Ordering
forall a. PartialOrd a => a -> a -> Ordering
ord Vec n (Interval 'Standard) -> Vec n (Interval 'Standard) -> Bool
forall a. PartialOrd a => a -> a -> Bool
(PO.<=)
  where
    ord :: a -> a -> Ordering
ord a
a a
b = Maybe Ordering -> Ordering
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Ordering -> Ordering) -> Maybe Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Maybe Ordering
forall a. PartialOrd a => a -> a -> Maybe Ordering
`PO.compare` a
b

-- | Union lemma says that if we have a product of intervals (as defined in
-- the paper) and we union two that agrees in each dimension except one.
-- The union is again a product of intervals that agrees with the original
-- dimensions in all dimensions except the original differing one. At that
-- point it is the union of intervals, which is itself still an interval.
unionLemma :: [ V.Vec n (Interval 'Standard) ] -> [ V.Vec n (Interval 'Standard) ]
unionLemma :: [Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
unionLemma = ([Vec n (Interval 'Standard)] -> Vec n (Interval 'Standard))
-> [[Vec n (Interval 'Standard)]] -> [Vec n (Interval 'Standard)]
forall a b. (a -> b) -> [a] -> [b]
map ((Vec n (Interval 'Standard)
 -> Vec n (Interval 'Standard) -> Vec n (Interval 'Standard))
-> [Vec n (Interval 'Standard)] -> Vec n (Interval 'Standard)
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ((Interval 'Standard -> Interval 'Standard -> Interval 'Standard)
-> Vec n (Interval 'Standard)
-> Vec n (Interval 'Standard)
-> Vec n (Interval 'Standard)
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
V.zipWith Interval 'Standard -> Interval 'Standard -> Interval 'Standard
forall a. Lattice a => a -> a -> a
(\/)))
           ([[Vec n (Interval 'Standard)]] -> [Vec n (Interval 'Standard)])
-> ([Vec n (Interval 'Standard)] -> [[Vec n (Interval 'Standard)]])
-> [Vec n (Interval 'Standard)]
-> [Vec n (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec n (Interval 'Standard)
 -> Vec n (Interval 'Standard) -> Ordering)
-> (Vec n (Interval 'Standard)
    -> Vec n (Interval 'Standard) -> Bool)
-> [Vec n (Interval 'Standard)]
-> [[Vec n (Interval 'Standard)]]
forall a.
Eq a =>
(a -> a -> Ordering) -> (a -> a -> Bool) -> [a] -> [[a]]
sensibleGroupBy (\Vec n (Interval 'Standard)
a Vec n (Interval 'Standard)
b -> if Vec n (Interval 'Standard)
a Vec n (Interval 'Standard) -> Vec n (Interval 'Standard) -> Bool
forall a. Eq a => a -> a -> Bool
== Vec n (Interval 'Standard)
b then Ordering
EQ else Ordering
LT) Vec n (Interval 'Standard) -> Vec n (Interval 'Standard) -> Bool
forall a (n :: Nat). Eq a => Vec n a -> Vec n a -> Bool
agreeButOne
  where
    -- This function returns true if two vectors agree at all points but one.
    -- It also holds if two vectors are identical.
    agreeButOne :: Eq a => V.Vec n a -> V.Vec n a -> Bool
    agreeButOne :: Vec n a -> Vec n a -> Bool
agreeButOne = Bool -> Vec n a -> Vec n a -> Bool
forall a (n :: Nat). Eq a => Bool -> Vec n a -> Vec n a -> Bool
go Bool
False
      where
        go :: Eq a => Bool -> V.Vec n a -> V.Vec n a -> Bool
        go :: Bool -> Vec n a -> Vec n a -> Bool
go Bool
_ Vec n a
V.Nil Vec n a
V.Nil = Bool
True
        go Bool
False (V.Cons a
x Vec n a
xs) (V.Cons a
y Vec n a
ys)
          | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = Bool -> Vec n a -> Vec n a -> Bool
forall a (n :: Nat). Eq a => Bool -> Vec n a -> Vec n a -> Bool
go Bool
False Vec n a
xs Vec n a
Vec n a
ys
          | Bool
otherwise = Bool -> Vec n a -> Vec n a -> Bool
forall a (n :: Nat). Eq a => Bool -> Vec n a -> Vec n a -> Bool
go Bool
True Vec n a
xs Vec n a
Vec n a
ys
        go Bool
True (V.Cons a
x Vec n a
xs) (V.Cons a
y Vec n a
ys)
          | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = Bool -> Vec n a -> Vec n a -> Bool
forall a (n :: Nat). Eq a => Bool -> Vec n a -> Vec n a -> Bool
go Bool
True Vec n a
xs Vec n a
Vec n a
ys
          | Bool
otherwise = Bool
False

--------------------------------------------------------------------------------
-- Injections for multiplicity and exactness
--------------------------------------------------------------------------------

data Approximation a = Exact a | Bound (Maybe a) (Maybe a)
  deriving (Approximation a -> Approximation a -> Bool
(Approximation a -> Approximation a -> Bool)
-> (Approximation a -> Approximation a -> Bool)
-> Eq (Approximation a)
forall a. Eq a => Approximation a -> Approximation a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Approximation a -> Approximation a -> Bool
$c/= :: forall a. Eq a => Approximation a -> Approximation a -> Bool
== :: Approximation a -> Approximation a -> Bool
$c== :: forall a. Eq a => Approximation a -> Approximation a -> Bool
Eq, Int -> Approximation a -> ShowS
[Approximation a] -> ShowS
Approximation a -> String
(Int -> Approximation a -> ShowS)
-> (Approximation a -> String)
-> ([Approximation a] -> ShowS)
-> Show (Approximation a)
forall a. Show a => Int -> Approximation a -> ShowS
forall a. Show a => [Approximation a] -> ShowS
forall a. Show a => Approximation a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Approximation a] -> ShowS
$cshowList :: forall a. Show a => [Approximation a] -> ShowS
show :: Approximation a -> String
$cshow :: forall a. Show a => Approximation a -> String
showsPrec :: Int -> Approximation a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Approximation a -> ShowS
Show, a -> Approximation b -> Approximation a
(a -> b) -> Approximation a -> Approximation b
(forall a b. (a -> b) -> Approximation a -> Approximation b)
-> (forall a b. a -> Approximation b -> Approximation a)
-> Functor Approximation
forall a b. a -> Approximation b -> Approximation a
forall a b. (a -> b) -> Approximation a -> Approximation b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Approximation b -> Approximation a
$c<$ :: forall a b. a -> Approximation b -> Approximation a
fmap :: (a -> b) -> Approximation a -> Approximation b
$cfmap :: forall a b. (a -> b) -> Approximation a -> Approximation b
Functor, Approximation a -> Bool
(a -> m) -> Approximation a -> m
(a -> b -> b) -> b -> Approximation a -> b
(forall m. Monoid m => Approximation m -> m)
-> (forall m a. Monoid m => (a -> m) -> Approximation a -> m)
-> (forall m a. Monoid m => (a -> m) -> Approximation a -> m)
-> (forall a b. (a -> b -> b) -> b -> Approximation a -> b)
-> (forall a b. (a -> b -> b) -> b -> Approximation a -> b)
-> (forall b a. (b -> a -> b) -> b -> Approximation a -> b)
-> (forall b a. (b -> a -> b) -> b -> Approximation a -> b)
-> (forall a. (a -> a -> a) -> Approximation a -> a)
-> (forall a. (a -> a -> a) -> Approximation a -> a)
-> (forall a. Approximation a -> [a])
-> (forall a. Approximation a -> Bool)
-> (forall a. Approximation a -> Int)
-> (forall a. Eq a => a -> Approximation a -> Bool)
-> (forall a. Ord a => Approximation a -> a)
-> (forall a. Ord a => Approximation a -> a)
-> (forall a. Num a => Approximation a -> a)
-> (forall a. Num a => Approximation a -> a)
-> Foldable Approximation
forall a. Eq a => a -> Approximation a -> Bool
forall a. Num a => Approximation a -> a
forall a. Ord a => Approximation a -> a
forall m. Monoid m => Approximation m -> m
forall a. Approximation a -> Bool
forall a. Approximation a -> Int
forall a. Approximation a -> [a]
forall a. (a -> a -> a) -> Approximation a -> a
forall m a. Monoid m => (a -> m) -> Approximation a -> m
forall b a. (b -> a -> b) -> b -> Approximation a -> b
forall a b. (a -> b -> b) -> b -> Approximation a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Approximation a -> a
$cproduct :: forall a. Num a => Approximation a -> a
sum :: Approximation a -> a
$csum :: forall a. Num a => Approximation a -> a
minimum :: Approximation a -> a
$cminimum :: forall a. Ord a => Approximation a -> a
maximum :: Approximation a -> a
$cmaximum :: forall a. Ord a => Approximation a -> a
elem :: a -> Approximation a -> Bool
$celem :: forall a. Eq a => a -> Approximation a -> Bool
length :: Approximation a -> Int
$clength :: forall a. Approximation a -> Int
null :: Approximation a -> Bool
$cnull :: forall a. Approximation a -> Bool
toList :: Approximation a -> [a]
$ctoList :: forall a. Approximation a -> [a]
foldl1 :: (a -> a -> a) -> Approximation a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Approximation a -> a
foldr1 :: (a -> a -> a) -> Approximation a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Approximation a -> a
foldl' :: (b -> a -> b) -> b -> Approximation a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Approximation a -> b
foldl :: (b -> a -> b) -> b -> Approximation a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Approximation a -> b
foldr' :: (a -> b -> b) -> b -> Approximation a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Approximation a -> b
foldr :: (a -> b -> b) -> b -> Approximation a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Approximation a -> b
foldMap' :: (a -> m) -> Approximation a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Approximation a -> m
foldMap :: (a -> m) -> Approximation a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Approximation a -> m
fold :: Approximation m -> m
$cfold :: forall m. Monoid m => Approximation m -> m
Foldable, Functor Approximation
Foldable Approximation
Functor Approximation
-> Foldable Approximation
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Approximation a -> f (Approximation b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Approximation (f a) -> f (Approximation a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Approximation a -> m (Approximation b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Approximation (m a) -> m (Approximation a))
-> Traversable Approximation
(a -> f b) -> Approximation a -> f (Approximation b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Approximation (m a) -> m (Approximation a)
forall (f :: * -> *) a.
Applicative f =>
Approximation (f a) -> f (Approximation a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Approximation a -> m (Approximation b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Approximation a -> f (Approximation b)
sequence :: Approximation (m a) -> m (Approximation a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Approximation (m a) -> m (Approximation a)
mapM :: (a -> m b) -> Approximation a -> m (Approximation b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Approximation a -> m (Approximation b)
sequenceA :: Approximation (f a) -> f (Approximation a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Approximation (f a) -> f (Approximation a)
traverse :: (a -> f b) -> Approximation a -> f (Approximation b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Approximation a -> f (Approximation b)
$cp2Traversable :: Foldable Approximation
$cp1Traversable :: Functor Approximation
Traversable, Typeable (Approximation a)
DataType
Constr
Typeable (Approximation a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Approximation a -> c (Approximation a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Approximation a))
-> (Approximation a -> Constr)
-> (Approximation a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Approximation a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Approximation a)))
-> ((forall b. Data b => b -> b)
    -> Approximation a -> Approximation a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Approximation a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Approximation a -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> Approximation a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Approximation a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> Approximation a -> m (Approximation a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Approximation a -> m (Approximation a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Approximation a -> m (Approximation a))
-> Data (Approximation a)
Approximation a -> DataType
Approximation a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Approximation a))
(forall b. Data b => b -> b) -> Approximation a -> Approximation a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Approximation a -> c (Approximation a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Approximation a)
forall a. Data a => Typeable (Approximation a)
forall a. Data a => Approximation a -> DataType
forall a. Data a => Approximation a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Approximation a -> Approximation a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Approximation a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Approximation a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Approximation a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Approximation a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> Approximation a -> m (Approximation a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Approximation a -> m (Approximation a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Approximation a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Approximation a -> c (Approximation a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Approximation a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Approximation a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> Approximation a -> u
forall u. (forall d. Data d => d -> u) -> Approximation a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Approximation a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Approximation a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Approximation a -> m (Approximation a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Approximation a -> m (Approximation a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Approximation a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Approximation a -> c (Approximation a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Approximation a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Approximation a))
$cBound :: Constr
$cExact :: Constr
$tApproximation :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> Approximation a -> m (Approximation a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Approximation a -> m (Approximation a)
gmapMp :: (forall d. Data d => d -> m d)
-> Approximation a -> m (Approximation a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Approximation a -> m (Approximation a)
gmapM :: (forall d. Data d => d -> m d)
-> Approximation a -> m (Approximation a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> Approximation a -> m (Approximation a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Approximation a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Approximation a -> u
gmapQ :: (forall d. Data d => d -> u) -> Approximation a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Approximation a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Approximation a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Approximation a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Approximation a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Approximation a -> r
gmapT :: (forall b. Data b => b -> b) -> Approximation a -> Approximation a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Approximation a -> Approximation a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Approximation a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Approximation a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Approximation a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Approximation a))
dataTypeOf :: Approximation a -> DataType
$cdataTypeOf :: forall a. Data a => Approximation a -> DataType
toConstr :: Approximation a -> Constr
$ctoConstr :: forall a. Data a => Approximation a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Approximation a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Approximation a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Approximation a -> c (Approximation a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Approximation a -> c (Approximation a)
$cp1Data :: forall a. Data a => Typeable (Approximation a)
Data, Typeable)

fromExact :: Approximation a -> a
fromExact :: Approximation a -> a
fromExact (Exact a
a) = a
a
fromExact Approximation a
_ = String -> a
forall a. HasCallStack => String -> a
error String
"Can't retrieve from bounded as if it was exact."

lowerBound :: Approximation a -> a
lowerBound :: Approximation a -> a
lowerBound (Bound (Just a
a) Maybe a
_) = a
a
lowerBound (Bound Maybe a
Nothing Maybe a
_) = String -> a
forall a. HasCallStack => String -> a
error String
"Approximation doesn't have a lower bound."
lowerBound (Exact a
a) = a
a

upperBound :: Approximation a -> a
upperBound :: Approximation a -> a
upperBound (Bound Maybe a
_ (Just a
a)) = a
a
upperBound (Bound Maybe a
_ Maybe a
Nothing) = String -> a
forall a. HasCallStack => String -> a
error String
"Approximation doesn't have a upper bound."
upperBound (Exact a
a) = a
a

class Peelable a where
  type CoreTyp a
  peel :: a -> CoreTyp a

data Multiplicity a = Mult a | Once a
  deriving (Multiplicity a -> Multiplicity a -> Bool
(Multiplicity a -> Multiplicity a -> Bool)
-> (Multiplicity a -> Multiplicity a -> Bool)
-> Eq (Multiplicity a)
forall a. Eq a => Multiplicity a -> Multiplicity a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Multiplicity a -> Multiplicity a -> Bool
$c/= :: forall a. Eq a => Multiplicity a -> Multiplicity a -> Bool
== :: Multiplicity a -> Multiplicity a -> Bool
$c== :: forall a. Eq a => Multiplicity a -> Multiplicity a -> Bool
Eq, Int -> Multiplicity a -> ShowS
[Multiplicity a] -> ShowS
Multiplicity a -> String
(Int -> Multiplicity a -> ShowS)
-> (Multiplicity a -> String)
-> ([Multiplicity a] -> ShowS)
-> Show (Multiplicity a)
forall a. Show a => Int -> Multiplicity a -> ShowS
forall a. Show a => [Multiplicity a] -> ShowS
forall a. Show a => Multiplicity a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Multiplicity a] -> ShowS
$cshowList :: forall a. Show a => [Multiplicity a] -> ShowS
show :: Multiplicity a -> String
$cshow :: forall a. Show a => Multiplicity a -> String
showsPrec :: Int -> Multiplicity a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Multiplicity a -> ShowS
Show, a -> Multiplicity b -> Multiplicity a
(a -> b) -> Multiplicity a -> Multiplicity b
(forall a b. (a -> b) -> Multiplicity a -> Multiplicity b)
-> (forall a b. a -> Multiplicity b -> Multiplicity a)
-> Functor Multiplicity
forall a b. a -> Multiplicity b -> Multiplicity a
forall a b. (a -> b) -> Multiplicity a -> Multiplicity b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Multiplicity b -> Multiplicity a
$c<$ :: forall a b. a -> Multiplicity b -> Multiplicity a
fmap :: (a -> b) -> Multiplicity a -> Multiplicity b
$cfmap :: forall a b. (a -> b) -> Multiplicity a -> Multiplicity b
Functor, Multiplicity a -> Bool
(a -> m) -> Multiplicity a -> m
(a -> b -> b) -> b -> Multiplicity a -> b
(forall m. Monoid m => Multiplicity m -> m)
-> (forall m a. Monoid m => (a -> m) -> Multiplicity a -> m)
-> (forall m a. Monoid m => (a -> m) -> Multiplicity a -> m)
-> (forall a b. (a -> b -> b) -> b -> Multiplicity a -> b)
-> (forall a b. (a -> b -> b) -> b -> Multiplicity a -> b)
-> (forall b a. (b -> a -> b) -> b -> Multiplicity a -> b)
-> (forall b a. (b -> a -> b) -> b -> Multiplicity a -> b)
-> (forall a. (a -> a -> a) -> Multiplicity a -> a)
-> (forall a. (a -> a -> a) -> Multiplicity a -> a)
-> (forall a. Multiplicity a -> [a])
-> (forall a. Multiplicity a -> Bool)
-> (forall a. Multiplicity a -> Int)
-> (forall a. Eq a => a -> Multiplicity a -> Bool)
-> (forall a. Ord a => Multiplicity a -> a)
-> (forall a. Ord a => Multiplicity a -> a)
-> (forall a. Num a => Multiplicity a -> a)
-> (forall a. Num a => Multiplicity a -> a)
-> Foldable Multiplicity
forall a. Eq a => a -> Multiplicity a -> Bool
forall a. Num a => Multiplicity a -> a
forall a. Ord a => Multiplicity a -> a
forall m. Monoid m => Multiplicity m -> m
forall a. Multiplicity a -> Bool
forall a. Multiplicity a -> Int
forall a. Multiplicity a -> [a]
forall a. (a -> a -> a) -> Multiplicity a -> a
forall m a. Monoid m => (a -> m) -> Multiplicity a -> m
forall b a. (b -> a -> b) -> b -> Multiplicity a -> b
forall a b. (a -> b -> b) -> b -> Multiplicity a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Multiplicity a -> a
$cproduct :: forall a. Num a => Multiplicity a -> a
sum :: Multiplicity a -> a
$csum :: forall a. Num a => Multiplicity a -> a
minimum :: Multiplicity a -> a
$cminimum :: forall a. Ord a => Multiplicity a -> a
maximum :: Multiplicity a -> a
$cmaximum :: forall a. Ord a => Multiplicity a -> a
elem :: a -> Multiplicity a -> Bool
$celem :: forall a. Eq a => a -> Multiplicity a -> Bool
length :: Multiplicity a -> Int
$clength :: forall a. Multiplicity a -> Int
null :: Multiplicity a -> Bool
$cnull :: forall a. Multiplicity a -> Bool
toList :: Multiplicity a -> [a]
$ctoList :: forall a. Multiplicity a -> [a]
foldl1 :: (a -> a -> a) -> Multiplicity a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Multiplicity a -> a
foldr1 :: (a -> a -> a) -> Multiplicity a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Multiplicity a -> a
foldl' :: (b -> a -> b) -> b -> Multiplicity a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Multiplicity a -> b
foldl :: (b -> a -> b) -> b -> Multiplicity a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Multiplicity a -> b
foldr' :: (a -> b -> b) -> b -> Multiplicity a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Multiplicity a -> b
foldr :: (a -> b -> b) -> b -> Multiplicity a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Multiplicity a -> b
foldMap' :: (a -> m) -> Multiplicity a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Multiplicity a -> m
foldMap :: (a -> m) -> Multiplicity a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Multiplicity a -> m
fold :: Multiplicity m -> m
$cfold :: forall m. Monoid m => Multiplicity m -> m
Foldable, Functor Multiplicity
Foldable Multiplicity
Functor Multiplicity
-> Foldable Multiplicity
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Multiplicity a -> f (Multiplicity b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Multiplicity (f a) -> f (Multiplicity a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Multiplicity a -> m (Multiplicity b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Multiplicity (m a) -> m (Multiplicity a))
-> Traversable Multiplicity
(a -> f b) -> Multiplicity a -> f (Multiplicity b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Multiplicity (m a) -> m (Multiplicity a)
forall (f :: * -> *) a.
Applicative f =>
Multiplicity (f a) -> f (Multiplicity a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Multiplicity a -> m (Multiplicity b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Multiplicity a -> f (Multiplicity b)
sequence :: Multiplicity (m a) -> m (Multiplicity a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Multiplicity (m a) -> m (Multiplicity a)
mapM :: (a -> m b) -> Multiplicity a -> m (Multiplicity b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Multiplicity a -> m (Multiplicity b)
sequenceA :: Multiplicity (f a) -> f (Multiplicity a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Multiplicity (f a) -> f (Multiplicity a)
traverse :: (a -> f b) -> Multiplicity a -> f (Multiplicity b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Multiplicity a -> f (Multiplicity b)
$cp2Traversable :: Foldable Multiplicity
$cp1Traversable :: Functor Multiplicity
Traversable, Typeable (Multiplicity a)
DataType
Constr
Typeable (Multiplicity a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Multiplicity a -> c (Multiplicity a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Multiplicity a))
-> (Multiplicity a -> Constr)
-> (Multiplicity a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Multiplicity a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Multiplicity a)))
-> ((forall b. Data b => b -> b)
    -> Multiplicity a -> Multiplicity a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Multiplicity a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Multiplicity a -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> Multiplicity a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Multiplicity a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> Multiplicity a -> m (Multiplicity a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Multiplicity a -> m (Multiplicity a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Multiplicity a -> m (Multiplicity a))
-> Data (Multiplicity a)
Multiplicity a -> DataType
Multiplicity a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Multiplicity a))
(forall b. Data b => b -> b) -> Multiplicity a -> Multiplicity a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Multiplicity a -> c (Multiplicity a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Multiplicity a)
forall a. Data a => Typeable (Multiplicity a)
forall a. Data a => Multiplicity a -> DataType
forall a. Data a => Multiplicity a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Multiplicity a -> Multiplicity a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Multiplicity a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Multiplicity a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Multiplicity a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Multiplicity a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> Multiplicity a -> m (Multiplicity a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Multiplicity a -> m (Multiplicity a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Multiplicity a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Multiplicity a -> c (Multiplicity a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Multiplicity a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Multiplicity a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> Multiplicity a -> u
forall u. (forall d. Data d => d -> u) -> Multiplicity a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Multiplicity a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Multiplicity a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Multiplicity a -> m (Multiplicity a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Multiplicity a -> m (Multiplicity a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Multiplicity a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Multiplicity a -> c (Multiplicity a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Multiplicity a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Multiplicity a))
$cOnce :: Constr
$cMult :: Constr
$tMultiplicity :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> Multiplicity a -> m (Multiplicity a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Multiplicity a -> m (Multiplicity a)
gmapMp :: (forall d. Data d => d -> m d)
-> Multiplicity a -> m (Multiplicity a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Multiplicity a -> m (Multiplicity a)
gmapM :: (forall d. Data d => d -> m d)
-> Multiplicity a -> m (Multiplicity a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> Multiplicity a -> m (Multiplicity a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Multiplicity a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Multiplicity a -> u
gmapQ :: (forall d. Data d => d -> u) -> Multiplicity a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Multiplicity a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Multiplicity a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Multiplicity a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Multiplicity a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Multiplicity a -> r
gmapT :: (forall b. Data b => b -> b) -> Multiplicity a -> Multiplicity a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Multiplicity a -> Multiplicity a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Multiplicity a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Multiplicity a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Multiplicity a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Multiplicity a))
dataTypeOf :: Multiplicity a -> DataType
$cdataTypeOf :: forall a. Data a => Multiplicity a -> DataType
toConstr :: Multiplicity a -> Constr
$ctoConstr :: forall a. Data a => Multiplicity a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Multiplicity a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Multiplicity a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Multiplicity a -> c (Multiplicity a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Multiplicity a -> c (Multiplicity a)
$cp1Data :: forall a. Data a => Typeable (Multiplicity a)
Data, Typeable)

instance Peelable (Multiplicity a) where
  type CoreTyp (Multiplicity a) = a

  peel :: Multiplicity a -> CoreTyp (Multiplicity a)
peel (Mult a
a) = a
CoreTyp (Multiplicity a)
a
  peel (Once a
a) = a
CoreTyp (Multiplicity a)
a

{-
data Approximation a = Exact a | Lower a | Upper a
  deriving (Eq, Show, Functor, Data, Typeable)

instance Peelable Approximation where
  peel (Exact a) = a
  peel (Lower a) = a
  peel (Upper a) = a
-}