{-# 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 :: [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)
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 (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 (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 (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. [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 (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 :: [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 :: 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 :: Vec n Int -> Span (Vec n Int)
mkTrivialSpan Vec n Int
V.Nil = (Vec n Int
forall a. Vec 'Z a
V.Nil, Vec n Int
forall a. Vec 'Z a
V.Nil)
mkTrivialSpan (V.Cons Int
x Vec n Int
xs) =
if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
absoluteRep
then (Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons (-Int
absoluteRep) Vec n Int
ys, Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons Int
absoluteRep Vec n Int
zs)
else (Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons Int
x Vec n Int
ys, Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons Int
x Vec n Int
zs)
where
(Vec n Int
ys, Vec n Int
zs) = Vec n Int -> (Vec n Int, Vec n Int)
forall (n :: Nat). Vec n Int -> Span (Vec n Int)
mkTrivialSpan Vec n 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 :: [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. [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 ('S m) Int] -> [Span (Vec ('S m) Int)])
-> [Vec ('S m) Int]
-> Either String (Approximation Spatial)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec ('S m) Int] -> [Span (Vec ('S m) Int)]
forall (n :: Nat). [Vec n Int] -> [Span (Vec n Int)]
inferMinimalVectorRegions ([Vec ('S m) Int] -> Either String (Approximation Spatial))
-> [Vec ('S m) Int] -> Either String (Approximation Spatial)
forall a b. (a -> b) -> a -> b
$ [Vec n Int]
[Vec ('S m) 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 :: [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 :: [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 :: [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 :: 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) = (Vec 'Z Int, Vec 'Z Int) -> Maybe (Vec 'Z Int, Vec 'Z Int)
forall a. a -> Maybe a
Just (Vec 'Z Int
forall a. Vec 'Z a
V.Nil, 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 n Int
ls1, V.Cons Int
u1 Vec n Int
us1) (V.Cons Int
l2 Vec n Int
ls2, V.Cons Int
u2 Vec n 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 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 (Vec n Int
ls1, Vec n Int
Vec n Int
us1) (Vec n Int
Vec n Int
ls2, Vec n Int
Vec n Int
us2) of
Just (Vec n Int
l, Vec n Int
u) -> (Vec ('S n) Int, Vec ('S n) Int)
-> Maybe (Vec ('S n) Int, Vec ('S n) Int)
forall a. a -> Maybe a
Just (Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons Int
l1 Vec n Int
l, Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons Int
u1 Vec n Int
u)
Maybe (Span (Vec n 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 n Int
us1 Vec n Int -> Vec n Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vec n Int
Vec n Int
us2) Bool -> Bool -> Bool
&& (Vec n Int
ls1 Vec n Int -> Vec n Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vec n Int
Vec n Int
ls2)
= (Vec ('S n) Int, Vec ('S n) Int)
-> Maybe (Vec ('S n) Int, Vec ('S n) Int)
forall a. a -> Maybe a
Just (Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons Int
l1 Vec n Int
ls1, Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons Int
u2 Vec n 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 n Int
us1 Vec n Int -> Vec n Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vec n Int
Vec n Int
us2) Bool -> Bool -> Bool
&& (Vec n Int
ls1 Vec n Int -> Vec n Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vec n Int
Vec n Int
ls2)
= (Vec ('S n) Int, Vec ('S n) Int)
-> Maybe (Vec ('S n) Int, Vec ('S n) Int)
forall a. a -> Maybe a
Just (Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons Int
l2 Vec n Int
ls2, Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons Int
u1 Vec n 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 :: [Span (Vec n Int)] -> [Span (Vec n Int)]
minimaliseRegions [] = []
minimaliseRegions [Span (Vec n Int)]
xss = [Span (Vec n Int)] -> [Span (Vec n Int)]
forall a. Eq a => [a] -> [a]
nub ([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)]
minimalise ([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)]
xss
where localMin :: Span (Vec n Int) -> [Span (Vec n Int)] -> [Span (Vec n Int)]
localMin Span (Vec n Int)
x [Span (Vec n Int)]
ys = Span (Vec n Int)
-> (Span (Vec n Int) -> Bool)
-> [Span (Vec n Int)]
-> [Span (Vec n Int)]
forall a. a -> (a -> Bool) -> [a] -> [a]
filter' Span (Vec n Int)
x (\Span (Vec n Int)
y -> Span (Vec n Int) -> Span (Vec n Int) -> Bool
forall (n :: Nat). Span (Vec n Int) -> Span (Vec n Int) -> Bool
containedWithin Span (Vec n Int)
x Span (Vec n Int)
y Bool -> Bool -> Bool
&& (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)) [Span (Vec n Int)]
xss [Span (Vec n Int)] -> [Span (Vec n Int)] -> [Span (Vec n Int)]
forall a. [a] -> [a] -> [a]
++ [Span (Vec n Int)]
ys
minimalise :: [Span (Vec n Int)] -> [Span (Vec n Int)]
minimalise = (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 (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Span (Vec n Int) -> [Span (Vec n Int)] -> [Span (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 :: 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 n Int
ls1, V.Cons Int
u1 Vec n Int
us1) (V.Cons Int
l2 Vec n Int
ls2, V.Cons Int
u2 Vec n 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 n Int) -> Span (Vec n Int) -> Bool
forall (n :: Nat). Span (Vec n Int) -> Span (Vec n Int) -> Bool
containedWithin (Vec n Int
ls1, Vec n Int
Vec n Int
us1) (Vec n Int
Vec n Int
ls2, Vec n Int
Vec n Int
us2)