{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
module Camfort.Specification.Stencils.InferenceBackend
( coalesce
, containedWithin
, inferFromIndicesWithoutLinearity
, inferMinimalVectorRegions
, spansToApproxSpatial
, Span
) where
import Data.List
import qualified Data.List.NonEmpty as NE
import Data.Maybe
import Algebra.Lattice (joins1)
import Camfort.Specification.Stencils.Model
import Camfort.Specification.Stencils.DenotationalSemantics
import qualified Camfort.Helpers.Vec as V
import Camfort.Specification.Stencils.Syntax
type Span a = (a, a)
spansToApproxSpatial :: [ Span (V.Vec ('V.S n) Int) ]
-> Either String (Approximation Spatial)
spansToApproxSpatial :: forall (n :: Nat).
[Span (Vec ('S n) Int)] -> Either String (Approximation Spatial)
spansToApproxSpatial [Span (Vec ('S n) Int)]
spans = Approximation (Either String Spatial)
-> Either String (Approximation Spatial)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a.
Monad m =>
Approximation (m a) -> m (Approximation a)
sequence (Approximation (Either String Spatial)
-> Either String (Approximation Spatial))
-> (Approximation (UnionNF ('S n) (Interval 'Standard))
-> Approximation (Either String Spatial))
-> Approximation (UnionNF ('S n) (Interval 'Standard))
-> Either String (Approximation Spatial)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnionNF ('S n) (Interval 'Standard) -> Either String Spatial)
-> Approximation (UnionNF ('S n) (Interval 'Standard))
-> Approximation (Either String Spatial)
forall a b. (a -> b) -> Approximation a -> Approximation b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UnionNF ('S n) (Interval 'Standard) -> Either String Spatial
forall (n :: Nat).
UnionNF ('S n) (Interval 'Standard) -> Either String Spatial
intervalsToRegions (Approximation (UnionNF ('S n) (Interval 'Standard))
-> Either String (Approximation Spatial))
-> Approximation (UnionNF ('S n) (Interval 'Standard))
-> Either String (Approximation Spatial)
forall a b. (a -> b) -> a -> b
$ Approximation (UnionNF ('S n) (Interval 'Standard))
approxUnion
where
approxVecs :: Approximation [Vec ('S n) (Interval 'Standard)]
approxVecs =
[Vec ('S n) (Interval 'Arbitrary)]
-> Approximation [Vec ('S n) (Interval 'Standard)]
forall (n :: Nat).
[Vec n (Interval 'Arbitrary)]
-> Approximation [Vec n (Interval 'Standard)]
toApprox ([Vec ('S n) (Interval 'Arbitrary)]
-> Approximation [Vec ('S n) (Interval 'Standard)])
-> ([Span (Vec ('S n) Int)] -> [Vec ('S n) (Interval 'Arbitrary)])
-> [Span (Vec ('S n) Int)]
-> Approximation [Vec ('S n) (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Span (Vec ('S n) Int) -> Vec ('S n) (Interval 'Arbitrary))
-> [Span (Vec ('S n) Int)] -> [Vec ('S n) (Interval 'Arbitrary)]
forall a b. (a -> b) -> [a] -> [b]
map ((Interval 'Arbitrary -> Interval 'Arbitrary)
-> Vec ('S n) (Interval 'Arbitrary)
-> Vec ('S n) (Interval 'Arbitrary)
forall a b. (a -> b) -> Vec ('S n) a -> Vec ('S n) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Interval 'Arbitrary -> Interval 'Arbitrary
absRepToInf (Vec ('S n) (Interval 'Arbitrary)
-> Vec ('S n) (Interval 'Arbitrary))
-> (Span (Vec ('S n) Int) -> Vec ('S n) (Interval 'Arbitrary))
-> Span (Vec ('S n) Int)
-> Vec ('S n) (Interval 'Arbitrary)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Span (Vec ('S n) Int) -> Vec ('S n) (Interval 'Arbitrary)
forall (n :: Nat). Span (Vec n Int) -> Vec n (Interval 'Arbitrary)
transposeVecInterval) ([Span (Vec ('S n) Int)]
-> Approximation [Vec ('S n) (Interval 'Standard)])
-> [Span (Vec ('S n) Int)]
-> Approximation [Vec ('S n) (Interval 'Standard)]
forall a b. (a -> b) -> a -> b
$ [Span (Vec ('S n) Int)]
spans
approxUnion :: Approximation (UnionNF ('S n) (Interval 'Standard))
approxUnion = ([Vec ('S n) (Interval 'Standard)]
-> UnionNF ('S n) (Interval 'Standard))
-> Approximation [Vec ('S n) (Interval 'Standard)]
-> Approximation (UnionNF ('S n) (Interval 'Standard))
forall a b. (a -> b) -> Approximation a -> Approximation b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (UnionNF ('S n) (Interval 'Standard)
-> UnionNF ('S n) (Interval 'Standard)
forall (n :: Nat).
UnionNF n (Interval 'Standard) -> UnionNF n (Interval 'Standard)
optimise (UnionNF ('S n) (Interval 'Standard)
-> UnionNF ('S n) (Interval 'Standard))
-> ([Vec ('S n) (Interval 'Standard)]
-> UnionNF ('S n) (Interval 'Standard))
-> [Vec ('S n) (Interval 'Standard)]
-> UnionNF ('S n) (Interval 'Standard)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (UnionNF ('S n) (Interval 'Standard))
-> UnionNF ('S n) (Interval 'Standard)
forall a (f :: * -> *). (Lattice a, Foldable1 f) => f a -> a
joins1 (NonEmpty (UnionNF ('S n) (Interval 'Standard))
-> UnionNF ('S n) (Interval 'Standard))
-> ([Vec ('S n) (Interval 'Standard)]
-> NonEmpty (UnionNF ('S n) (Interval 'Standard)))
-> [Vec ('S n) (Interval 'Standard)]
-> UnionNF ('S n) (Interval 'Standard)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionNF ('S n) (Interval 'Standard)]
-> NonEmpty (UnionNF ('S n) (Interval 'Standard))
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList ([UnionNF ('S n) (Interval 'Standard)]
-> NonEmpty (UnionNF ('S n) (Interval 'Standard)))
-> ([Vec ('S n) (Interval 'Standard)]
-> [UnionNF ('S n) (Interval 'Standard)])
-> [Vec ('S n) (Interval 'Standard)]
-> NonEmpty (UnionNF ('S n) (Interval 'Standard))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec ('S n) (Interval 'Standard)
-> UnionNF ('S n) (Interval 'Standard))
-> [Vec ('S n) (Interval 'Standard)]
-> [UnionNF ('S n) (Interval 'Standard)]
forall a b. (a -> b) -> [a] -> [b]
map Vec ('S n) (Interval 'Standard)
-> UnionNF ('S n) (Interval 'Standard)
forall a. a -> NonEmpty a
forall (m :: * -> *) a. Monad m => a -> m a
return) Approximation [Vec ('S n) (Interval 'Standard)]
approxVecs
toApprox :: [ V.Vec n (Interval 'Arbitrary) ]
-> Approximation [ V.Vec n (Interval 'Standard) ]
toApprox :: forall (n :: Nat).
[Vec n (Interval 'Arbitrary)]
-> Approximation [Vec n (Interval 'Standard)]
toApprox [Vec n (Interval 'Arbitrary)]
vs
| ([Approximation (Vec n (Interval 'Standard))],
[Approximation (Vec n (Interval 'Standard))])
parts <- ([Approximation (Vec n (Interval 'Standard))]
-> ([Approximation (Vec n (Interval 'Standard))],
[Approximation (Vec n (Interval 'Standard))])
forall {a}.
[Approximation a] -> ([Approximation a], [Approximation a])
elongatedPartitions ([Approximation (Vec n (Interval 'Standard))]
-> ([Approximation (Vec n (Interval 'Standard))],
[Approximation (Vec n (Interval 'Standard))]))
-> ([Vec n (Interval 'Arbitrary)]
-> [Approximation (Vec n (Interval 'Standard))])
-> [Vec n (Interval 'Arbitrary)]
-> ([Approximation (Vec n (Interval 'Standard))],
[Approximation (Vec n (Interval 'Standard))])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec n (Interval 'Arbitrary)
-> Approximation (Vec n (Interval 'Standard)))
-> [Vec n (Interval 'Arbitrary)]
-> [Approximation (Vec n (Interval 'Standard))]
forall a b. (a -> b) -> [a] -> [b]
map Vec n (Interval 'Arbitrary)
-> Approximation (Vec n (Interval 'Standard))
forall (n :: Nat).
Vec n (Interval 'Arbitrary)
-> Approximation (Vec n (Interval 'Standard))
approxVec) [Vec n (Interval 'Arbitrary)]
vs =
case ([Approximation (Vec n (Interval 'Standard))],
[Approximation (Vec n (Interval 'Standard))])
parts of
([Approximation (Vec n (Interval 'Standard))]
orgs, []) -> [Vec n (Interval 'Standard)]
-> Approximation [Vec n (Interval 'Standard)]
forall a. a -> Approximation a
Exact ([Vec n (Interval 'Standard)]
-> Approximation [Vec n (Interval 'Standard)])
-> ([Approximation (Vec n (Interval 'Standard))]
-> [Vec n (Interval 'Standard)])
-> [Approximation (Vec n (Interval 'Standard))]
-> Approximation [Vec n (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Approximation (Vec n (Interval 'Standard))
-> Vec n (Interval 'Standard))
-> [Approximation (Vec n (Interval 'Standard))]
-> [Vec n (Interval 'Standard)]
forall a b. (a -> b) -> [a] -> [b]
map Approximation (Vec n (Interval 'Standard))
-> Vec n (Interval 'Standard)
forall a. Approximation a -> a
fromExact ([Approximation (Vec n (Interval 'Standard))]
-> Approximation [Vec n (Interval 'Standard)])
-> [Approximation (Vec n (Interval 'Standard))]
-> Approximation [Vec n (Interval 'Standard)]
forall a b. (a -> b) -> a -> b
$ [Approximation (Vec n (Interval 'Standard))]
orgs
([], [Approximation (Vec n (Interval 'Standard))]
elongs) -> 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 (Vec n (Interval 'Standard))
-> Vec n (Interval 'Standard))
-> [Approximation (Vec n (Interval 'Standard))]
-> [Vec n (Interval 'Standard)]
forall a b. (a -> b) -> [a] -> [b]
map Approximation (Vec n (Interval 'Standard))
-> Vec n (Interval 'Standard)
forall a. Approximation a -> a
upperBound [Approximation (Vec n (Interval 'Standard))]
elongs)
([Approximation (Vec n (Interval 'Standard))]
orgs, [Approximation (Vec n (Interval 'Standard))]
elongs) -> Maybe [Vec n (Interval 'Standard)]
-> Maybe [Vec n (Interval 'Standard)]
-> Approximation [Vec n (Interval 'Standard)]
forall a. Maybe a -> Maybe a -> Approximation a
Bound ([Vec n (Interval 'Standard)] -> Maybe [Vec n (Interval 'Standard)]
forall a. a -> Maybe a
Just ([Vec n (Interval 'Standard)]
-> Maybe [Vec n (Interval 'Standard)])
-> ([Approximation (Vec n (Interval 'Standard))]
-> [Vec n (Interval 'Standard)])
-> [Approximation (Vec n (Interval 'Standard))]
-> Maybe [Vec n (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Approximation (Vec n (Interval 'Standard))
-> Vec n (Interval 'Standard))
-> [Approximation (Vec n (Interval 'Standard))]
-> [Vec n (Interval 'Standard)]
forall a b. (a -> b) -> [a] -> [b]
map Approximation (Vec n (Interval 'Standard))
-> Vec n (Interval 'Standard)
forall a. Approximation a -> a
upperBound ([Approximation (Vec n (Interval 'Standard))]
-> Maybe [Vec n (Interval 'Standard)])
-> [Approximation (Vec n (Interval 'Standard))]
-> Maybe [Vec n (Interval 'Standard)]
forall a b. (a -> b) -> a -> b
$ [Approximation (Vec n (Interval 'Standard))]
orgs)
([Vec n (Interval 'Standard)] -> Maybe [Vec n (Interval 'Standard)]
forall a. a -> Maybe a
Just ([Vec n (Interval 'Standard)]
-> Maybe [Vec n (Interval 'Standard)])
-> ([Approximation (Vec n (Interval 'Standard))]
-> [Vec n (Interval 'Standard)])
-> [Approximation (Vec n (Interval 'Standard))]
-> Maybe [Vec n (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Approximation (Vec n (Interval 'Standard))
-> Vec n (Interval 'Standard))
-> [Approximation (Vec n (Interval 'Standard))]
-> [Vec n (Interval 'Standard)]
forall a b. (a -> b) -> [a] -> [b]
map Approximation (Vec n (Interval 'Standard))
-> Vec n (Interval 'Standard)
forall a. Approximation a -> a
upperBound ([Approximation (Vec n (Interval 'Standard))]
-> Maybe [Vec n (Interval 'Standard)])
-> [Approximation (Vec n (Interval 'Standard))]
-> Maybe [Vec n (Interval 'Standard)]
forall a b. (a -> b) -> a -> b
$ [Approximation (Vec n (Interval 'Standard))]
orgs [Approximation (Vec n (Interval 'Standard))]
-> [Approximation (Vec n (Interval 'Standard))]
-> [Approximation (Vec n (Interval 'Standard))]
forall a. [a] -> [a] -> [a]
++ [Approximation (Vec n (Interval 'Standard))]
elongs)
elongatedPartitions :: [Approximation a] -> ([Approximation a], [Approximation a])
elongatedPartitions =
(Approximation a -> Bool)
-> [Approximation a] -> ([Approximation a], [Approximation a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((Approximation a -> Bool)
-> [Approximation a] -> ([Approximation a], [Approximation a]))
-> (Approximation a -> Bool)
-> [Approximation a]
-> ([Approximation a], [Approximation a])
forall a b. (a -> b) -> a -> b
$ \case { Exact{} -> Bool
True; Bound{} -> Bool
False }
absRepToInf :: Interval 'Arbitrary -> Interval 'Arbitrary
absRepToInf :: Interval 'Arbitrary -> Interval 'Arbitrary
absRepToInf interv :: Interval 'Arbitrary
interv@(IntervArbitrary Int
a Int
b)
| Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
absoluteRep = Interval 'Arbitrary
IntervInfiniteArbitrary
| Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
absoluteRep = Interval 'Arbitrary
IntervInfiniteArbitrary
| Bool
otherwise = Interval 'Arbitrary
interv
absRepToInf Interval 'Arbitrary
interv = Interval 'Arbitrary
interv
transposeVecInterval :: Span (V.Vec n Int) -> V.Vec n (Interval 'Arbitrary)
transposeVecInterval :: forall (n :: Nat). Span (Vec n Int) -> Vec n (Interval 'Arbitrary)
transposeVecInterval (Vec n Int
us, Vec n Int
vs) = (Int -> Int -> Interval 'Arbitrary)
-> Vec n Int -> Vec n Int -> Vec n (Interval 'Arbitrary)
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
V.zipWith Int -> Int -> Interval 'Arbitrary
IntervArbitrary Vec n Int
us Vec n Int
vs
mkTrivialSpan :: V.Vec n Int -> Span (V.Vec n Int)
mkTrivialSpan :: forall (n :: Nat). Vec n Int -> Span (Vec n Int)
mkTrivialSpan Vec n Int
V.Nil = (Vec n Int
Vec 'Z Int
forall a. Vec 'Z a
V.Nil, Vec n Int
Vec 'Z Int
forall a. Vec 'Z a
V.Nil)
mkTrivialSpan (V.Cons Int
x Vec n1 Int
xs) =
if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
absoluteRep
then (Int -> Vec n1 Int -> Vec ('S n1) Int
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
V.Cons (-Int
absoluteRep) Vec n1 Int
ys, Int -> Vec n1 Int -> Vec ('S n1) Int
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
V.Cons Int
absoluteRep Vec n1 Int
zs)
else (Int -> Vec n1 Int -> Vec ('S n1) Int
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
V.Cons Int
x Vec n1 Int
ys, Int -> Vec n1 Int -> Vec ('S n1) Int
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
V.Cons Int
x Vec n1 Int
zs)
where
(Vec n1 Int
ys, Vec n1 Int
zs) = Vec n1 Int -> (Vec n1 Int, Vec n1 Int)
forall (n :: Nat). Vec n Int -> Span (Vec n Int)
mkTrivialSpan Vec n1 Int
xs
inferFromIndicesWithoutLinearity :: V.VecList Int -> Specification
inferFromIndicesWithoutLinearity :: VecList Int -> Specification
inferFromIndicesWithoutLinearity (V.VL [Vec n Int]
ixs) =
Multiplicity (Approximation Spatial) -> Bool -> Specification
Specification (Approximation Spatial -> Multiplicity (Approximation Spatial)
forall a. a -> Multiplicity a
Mult (Approximation Spatial -> Multiplicity (Approximation Spatial))
-> ([Vec n Int] -> Approximation Spatial)
-> [Vec n Int]
-> Multiplicity (Approximation Spatial)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec n Int] -> Approximation Spatial
forall (n :: Nat). [Vec n Int] -> Approximation Spatial
inferCore ([Vec n Int] -> Multiplicity (Approximation Spatial))
-> [Vec n Int] -> Multiplicity (Approximation Spatial)
forall a b. (a -> b) -> a -> b
$ [Vec n Int]
ixs) Bool
True
inferCore :: [V.Vec n Int] -> Approximation Spatial
inferCore :: forall (n :: Nat). [Vec n Int] -> Approximation Spatial
inferCore [Vec n Int]
subs =
case Vec n Int -> Maybe (ExistsEqT 'S n)
forall (n :: Nat) a. Vec n a -> Maybe (ExistsEqT 'S n)
V.proveNonEmpty (Vec n Int -> Maybe (ExistsEqT 'S n))
-> ([Vec n Int] -> Vec n Int)
-> [Vec n Int]
-> Maybe (ExistsEqT 'S n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec n Int] -> Vec n Int
forall a. HasCallStack => [a] -> a
head ([Vec n Int] -> Maybe (ExistsEqT 'S n))
-> [Vec n Int] -> Maybe (ExistsEqT 'S n)
forall a b. (a -> b) -> a -> b
$ [Vec n Int]
subs of
Just (V.ExistsEqT EqT ('S m) n
V.ReflEq) ->
case [Span (Vec ('S m) Int)] -> Either String (Approximation Spatial)
forall (n :: Nat).
[Span (Vec ('S n) Int)] -> Either String (Approximation Spatial)
spansToApproxSpatial ([Span (Vec ('S m) Int)] -> Either String (Approximation Spatial))
-> ([Vec n Int] -> [Span (Vec ('S m) Int)])
-> [Vec n Int]
-> Either String (Approximation Spatial)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec n Int] -> [Span (Vec n Int)]
[Vec n Int] -> [Span (Vec ('S m) Int)]
forall (n :: Nat). [Vec n Int] -> [Span (Vec n Int)]
inferMinimalVectorRegions ([Vec n Int] -> Either String (Approximation Spatial))
-> [Vec n Int] -> Either String (Approximation Spatial)
forall a b. (a -> b) -> a -> b
$ [Vec n Int]
subs of
Right Approximation Spatial
a -> Approximation Spatial
a
Left String
msg -> String -> Approximation Spatial
forall a. HasCallStack => String -> a
error String
msg
Maybe (ExistsEqT 'S n)
Nothing -> String -> Approximation Spatial
forall a. HasCallStack => String -> a
error String
"Input vectors are empty!"
inferMinimalVectorRegions :: [V.Vec n Int] -> [Span (V.Vec n Int)]
inferMinimalVectorRegions :: forall (n :: Nat). [Vec n Int] -> [Span (Vec n Int)]
inferMinimalVectorRegions = [Span (Vec n Int)] -> [Span (Vec n Int)]
forall {n :: Nat}. [Span (Vec n Int)] -> [Span (Vec n Int)]
fixCoalesce ([Span (Vec n Int)] -> [Span (Vec n Int)])
-> ([Vec n Int] -> [Span (Vec n Int)])
-> [Vec n Int]
-> [Span (Vec n Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec n Int -> Span (Vec n Int))
-> [Vec n Int] -> [Span (Vec n Int)]
forall a b. (a -> b) -> [a] -> [b]
map Vec n Int -> Span (Vec n Int)
forall (n :: Nat). Vec n Int -> Span (Vec n Int)
mkTrivialSpan
where fixCoalesce :: [Span (Vec n Int)] -> [Span (Vec n Int)]
fixCoalesce [Span (Vec n Int)]
spans =
let spans' :: [Span (Vec n Int)]
spans' = [Span (Vec n Int)] -> [Span (Vec n Int)]
forall {n :: Nat}. [Span (Vec n Int)] -> [Span (Vec n Int)]
minimaliseRegions ([Span (Vec n Int)] -> [Span (Vec n Int)])
-> ([Span (Vec n Int)] -> [Span (Vec n Int)])
-> [Span (Vec n Int)]
-> [Span (Vec n Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Span (Vec n Int)] -> [Span (Vec n Int)]
forall {n :: Nat}. [Span (Vec n Int)] -> [Span (Vec n Int)]
coalesceContiguous ([Span (Vec n Int)] -> [Span (Vec n Int)])
-> [Span (Vec n Int)] -> [Span (Vec n Int)]
forall a b. (a -> b) -> a -> b
$ [Span (Vec n Int)]
spans
in if [Span (Vec n Int)]
spans' [Span (Vec n Int)] -> [Span (Vec n Int)] -> Bool
forall a. Eq a => a -> a -> Bool
== [Span (Vec n Int)]
spans then [Span (Vec n Int)]
spans' else [Span (Vec n Int)] -> [Span (Vec n Int)]
fixCoalesce [Span (Vec n Int)]
spans'
coalesceContiguous :: [Span (V.Vec n Int)] -> [Span (V.Vec n Int)]
coalesceContiguous :: forall {n :: Nat}. [Span (Vec n Int)] -> [Span (Vec n Int)]
coalesceContiguous [] = []
coalesceContiguous [Span (Vec n Int)
x] = [Span (Vec n Int)
x]
coalesceContiguous [Span (Vec n Int)
x, Span (Vec n Int)
y] =
case Span (Vec n Int) -> Span (Vec n Int) -> Maybe (Span (Vec n Int))
forall (n :: Nat).
Span (Vec n Int) -> Span (Vec n Int) -> Maybe (Span (Vec n Int))
coalesce Span (Vec n Int)
x Span (Vec n Int)
y of
Maybe (Span (Vec n Int))
Nothing -> [Span (Vec n Int)
x, Span (Vec n Int)
y]
Just Span (Vec n Int)
c -> [Span (Vec n Int)
c]
coalesceContiguous (Span (Vec n Int)
x:[Span (Vec n Int)]
xs) =
case [Maybe (Span (Vec n Int))] -> Maybe [Span (Vec n Int)]
forall a. Eq a => [Maybe a] -> Maybe [a]
sequenceMaybes ((Span (Vec n Int) -> Maybe (Span (Vec n Int)))
-> [Span (Vec n Int)] -> [Maybe (Span (Vec n Int))]
forall a b. (a -> b) -> [a] -> [b]
map (Span (Vec n Int) -> Span (Vec n Int) -> Maybe (Span (Vec n Int))
forall (n :: Nat).
Span (Vec n Int) -> Span (Vec n Int) -> Maybe (Span (Vec n Int))
coalesce Span (Vec n Int)
x) [Span (Vec n Int)]
xs) of
Maybe [Span (Vec n Int)]
Nothing -> Span (Vec n Int)
x Span (Vec n Int) -> [Span (Vec n Int)] -> [Span (Vec n Int)]
forall a. a -> [a] -> [a]
: [Span (Vec n Int)] -> [Span (Vec n Int)]
forall {n :: Nat}. [Span (Vec n Int)] -> [Span (Vec n Int)]
coalesceContiguous [Span (Vec n Int)]
xs
Just [Span (Vec n Int)]
cs -> [Span (Vec n Int)] -> [Span (Vec n Int)]
forall {n :: Nat}. [Span (Vec n Int)] -> [Span (Vec n Int)]
coalesceContiguous ([Span (Vec n Int)]
cs [Span (Vec n Int)] -> [Span (Vec n Int)] -> [Span (Vec n Int)]
forall a. [a] -> [a] -> [a]
++ [Span (Vec n Int)]
xs)
sequenceMaybes :: Eq a => [Maybe a] -> Maybe [a]
sequenceMaybes :: forall a. Eq a => [Maybe a] -> Maybe [a]
sequenceMaybes [Maybe a]
xs | (Maybe a -> Bool) -> [Maybe a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe a
forall a. Maybe a
Nothing) [Maybe a]
xs = Maybe [a]
forall a. Maybe a
Nothing
| Bool
otherwise = [a] -> Maybe [a]
forall a. a -> Maybe a
Just ([Maybe a] -> [a]
forall a. [Maybe a] -> [a]
catMaybes [Maybe a]
xs)
coalesce :: Span (V.Vec n Int) -> Span (V.Vec n Int) -> Maybe (Span (V.Vec n Int))
coalesce :: forall (n :: Nat).
Span (Vec n Int) -> Span (Vec n Int) -> Maybe (Span (Vec n Int))
coalesce (Vec n Int
V.Nil, Vec n Int
V.Nil) (Vec n Int
V.Nil, Vec n Int
V.Nil) = Span (Vec n Int) -> Maybe (Span (Vec n Int))
forall a. a -> Maybe a
Just (Vec n Int
Vec 'Z Int
forall a. Vec 'Z a
V.Nil, Vec n Int
Vec 'Z Int
forall a. Vec 'Z a
V.Nil)
coalesce Span (Vec n Int)
x Span (Vec n Int)
y | Span (Vec n Int)
x Span (Vec n Int) -> Span (Vec n Int) -> Bool
forall a. Eq a => a -> a -> Bool
== Span (Vec n Int)
y = Maybe (Span (Vec n Int))
forall a. Maybe a
Nothing
coalesce (V.Cons Int
l1 Vec n1 Int
ls1, V.Cons Int
u1 Vec n1 Int
us1) (V.Cons Int
l2 Vec n1 Int
ls2, V.Cons Int
u2 Vec n1 Int
us2)
| Int
l1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
l2 Bool -> Bool -> Bool
&& Int
u1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
u2
= case Span (Vec n1 Int) -> Span (Vec n1 Int) -> Maybe (Span (Vec n1 Int))
forall (n :: Nat).
Span (Vec n Int) -> Span (Vec n Int) -> Maybe (Span (Vec n Int))
coalesce (Vec n1 Int
ls1, Vec n1 Int
Vec n1 Int
us1) (Vec n1 Int
Vec n1 Int
ls2, Vec n1 Int
Vec n1 Int
us2) of
Just (Vec n1 Int
l, Vec n1 Int
u) -> Span (Vec n Int) -> Maybe (Span (Vec n Int))
forall a. a -> Maybe a
Just (Int -> Vec n1 Int -> Vec ('S n1) Int
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
V.Cons Int
l1 Vec n1 Int
l, Int -> Vec n1 Int -> Vec ('S n1) Int
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
V.Cons Int
u1 Vec n1 Int
u)
Maybe (Span (Vec n1 Int))
Nothing -> Maybe (Span (Vec n Int))
forall a. Maybe a
Nothing
| (Int
u1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
l2) Bool -> Bool -> Bool
&& (Vec n1 Int
us1 Vec n1 Int -> Vec n1 Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vec n1 Int
Vec n1 Int
us2) Bool -> Bool -> Bool
&& (Vec n1 Int
ls1 Vec n1 Int -> Vec n1 Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vec n1 Int
Vec n1 Int
ls2)
= Span (Vec n Int) -> Maybe (Span (Vec n Int))
forall a. a -> Maybe a
Just (Int -> Vec n1 Int -> Vec ('S n1) Int
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
V.Cons Int
l1 Vec n1 Int
ls1, Int -> Vec n1 Int -> Vec ('S n1) Int
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
V.Cons Int
u2 Vec n1 Int
us2)
| (Int
u2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
l1) Bool -> Bool -> Bool
&& (Vec n1 Int
us1 Vec n1 Int -> Vec n1 Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vec n1 Int
Vec n1 Int
us2) Bool -> Bool -> Bool
&& (Vec n1 Int
ls1 Vec n1 Int -> Vec n1 Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vec n1 Int
Vec n1 Int
ls2)
= Span (Vec n Int) -> Maybe (Span (Vec n Int))
forall a. a -> Maybe a
Just (Int -> Vec n1 Int -> Vec ('S n1) Int
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
V.Cons Int
l2 Vec n1 Int
ls2, Int -> Vec n1 Int -> Vec ('S n1) Int
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
V.Cons Int
u1 Vec n1 Int
us1)
coalesce Span (Vec n Int)
_ Span (Vec n Int)
_
= Maybe (Span (Vec n Int))
forall a. Maybe a
Nothing
minimaliseRegions :: [Span (V.Vec n Int)] -> [Span (V.Vec n Int)]
minimaliseRegions :: forall {n :: Nat}. [Span (Vec n Int)] -> [Span (Vec n Int)]
minimaliseRegions [] = []
minimaliseRegions [(Vec n Int, Vec n Int)]
xss = [(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)]
forall a. Eq a => [a] -> [a]
nub ([(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)])
-> ([(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)])
-> [(Vec n Int, Vec n Int)]
-> [(Vec n Int, Vec n Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)]
minimalise ([(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)])
-> [(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)]
forall a b. (a -> b) -> a -> b
$ [(Vec n Int, Vec n Int)]
xss
where localMin :: (Vec n Int, Vec n Int)
-> [(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)]
localMin (Vec n Int, Vec n Int)
x [(Vec n Int, Vec n Int)]
ys = (Vec n Int, Vec n Int)
-> ((Vec n Int, Vec n Int) -> Bool)
-> [(Vec n Int, Vec n Int)]
-> [(Vec n Int, Vec n Int)]
forall {a}. a -> (a -> Bool) -> [a] -> [a]
filter' (Vec n Int, Vec n Int)
x (\(Vec n Int, Vec n Int)
y -> (Vec n Int, Vec n Int) -> (Vec n Int, Vec n Int) -> Bool
forall (n :: Nat). Span (Vec n Int) -> Span (Vec n Int) -> Bool
containedWithin (Vec n Int, Vec n Int)
x (Vec n Int, Vec n Int)
y Bool -> Bool -> Bool
&& ((Vec n Int, Vec n Int)
x (Vec n Int, Vec n Int) -> (Vec n Int, Vec n Int) -> Bool
forall a. Eq a => a -> a -> Bool
/= (Vec n Int, Vec n Int)
y)) [(Vec n Int, Vec n Int)]
xss [(Vec n Int, Vec n Int)]
-> [(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)]
forall a. [a] -> [a] -> [a]
++ [(Vec n Int, Vec n Int)]
ys
minimalise :: [(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)]
minimalise = ((Vec n Int, Vec n Int)
-> [(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)])
-> [(Vec n Int, Vec n Int)]
-> [(Vec n Int, Vec n Int)]
-> [(Vec n Int, Vec n Int)]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Vec n Int, Vec n Int)
-> [(Vec n Int, Vec n Int)] -> [(Vec n Int, Vec n Int)]
localMin []
filter' :: a -> (a -> Bool) -> [a] -> [a]
filter' a
r a -> Bool
f [a]
xs = case (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
f [a]
xs of
[] -> [a
r]
[a]
ys -> [a]
ys
containedWithin :: Span (V.Vec n Int) -> Span (V.Vec n Int) -> Bool
containedWithin :: forall (n :: Nat). Span (Vec n Int) -> Span (Vec n Int) -> Bool
containedWithin (Vec n Int
V.Nil, Vec n Int
V.Nil) (Vec n Int
V.Nil, Vec n Int
V.Nil)
= Bool
True
containedWithin (V.Cons Int
l1 Vec n1 Int
ls1, V.Cons Int
u1 Vec n1 Int
us1) (V.Cons Int
l2 Vec n1 Int
ls2, V.Cons Int
u2 Vec n1 Int
us2)
= (Int
l2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
l1 Bool -> Bool -> Bool
&& Int
u1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
u2) Bool -> Bool -> Bool
&& Span (Vec n1 Int) -> Span (Vec n1 Int) -> Bool
forall (n :: Nat). Span (Vec n Int) -> Span (Vec n Int) -> Bool
containedWithin (Vec n1 Int
ls1, Vec n1 Int
Vec n1 Int
us1) (Vec n1 Int
Vec n1 Int
ls2, Vec n1 Int
Vec n1 Int
us2)