{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DataKinds #-}

module Camfort.Specification.Stencils.DenotationalSemantics ( intervalsToRegions
                                                            , regionsToIntervals ) where

import Algebra.Lattice
import qualified Data.List.NonEmpty as NE
import qualified Data.Semigroup as SG

import qualified Camfort.Helpers.Vec as V
import Camfort.Specification.Stencils.Model
import Camfort.Specification.Stencils.Syntax

-- preconditions:
-- 1. If finite interval, all have "lower bound <= 0 <= upper bound";
-- 2. No dimensionality of 0; (insured by dep. type);
-- 3. All unioned interval lists are of equal length (insured by dep.  type).
intervalsToRegions :: UnionNF ('V.S n) (Interval 'Standard)
                   -> Either String Spatial
intervalsToRegions :: UnionNF ('S n) (Interval 'Standard) -> Either String Spatial
intervalsToRegions UnionNF ('S n) (Interval 'Standard)
as = do
    [RegionProd]
sums <- (Vec ('S n) (Interval 'Standard) -> Either String RegionProd)
-> [Vec ('S n) (Interval 'Standard)] -> Either String [RegionProd]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Vec ('S n) (Interval 'Standard) -> Either String RegionProd
forall (n :: Nat).
Vec n (Interval 'Standard) -> Either String RegionProd
toProd
          ([Vec ('S n) (Interval 'Standard)] -> Either String [RegionProd])
-> (UnionNF ('S n) (Interval 'Standard)
    -> [Vec ('S n) (Interval 'Standard)])
-> UnionNF ('S n) (Interval 'Standard)
-> Either String [RegionProd]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec ('S n) (Interval 'Standard)]
-> [Vec ('S n) (Interval 'Standard)]
forall (n :: Nat).
[Vec n (Interval 'Standard)] -> [Vec n (Interval 'Standard)]
maximas -- Final subsumption optimisation
          ([Vec ('S n) (Interval 'Standard)]
 -> [Vec ('S n) (Interval 'Standard)])
-> (UnionNF ('S n) (Interval 'Standard)
    -> [Vec ('S n) (Interval 'Standard)])
-> UnionNF ('S n) (Interval 'Standard)
-> [Vec ('S n) (Interval 'Standard)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionNF ('S n) (Interval 'Standard)
-> [Vec ('S n) (Interval 'Standard)]
forall a. NonEmpty a -> [a]
NE.toList
          (UnionNF ('S n) (Interval 'Standard)
 -> [Vec ('S n) (Interval 'Standard)])
-> (UnionNF ('S n) (Interval 'Standard)
    -> UnionNF ('S n) (Interval 'Standard))
-> UnionNF ('S n) (Interval 'Standard)
-> [Vec ('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. Semigroup a => NonEmpty a -> a
SG.sconcat
          (NonEmpty (UnionNF ('S n) (Interval 'Standard))
 -> UnionNF ('S n) (Interval 'Standard))
-> (UnionNF ('S n) (Interval 'Standard)
    -> NonEmpty (UnionNF ('S n) (Interval 'Standard)))
-> UnionNF ('S n) (Interval 'Standard)
-> 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))
-> UnionNF ('S n) (Interval 'Standard)
-> NonEmpty (UnionNF ('S n) (Interval 'Standard))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Vec ('S n) (Interval 'Standard)
-> UnionNF ('S n) (Interval 'Standard)
forall (n :: Nat) (a :: Bound).
Vec n (Interval a) -> UnionNF n (Interval a)
asymmetryElim
          (UnionNF ('S n) (Interval 'Standard) -> Either String [RegionProd])
-> UnionNF ('S n) (Interval 'Standard)
-> Either String [RegionProd]
forall a b. (a -> b) -> a -> b
$ UnionNF ('S n) (Interval 'Standard)
as
    Spatial -> Either String Spatial
forall (m :: * -> *) a. Monad m => a -> m a
return (Spatial -> Either String Spatial)
-> ([RegionProd] -> Spatial)
-> [RegionProd]
-> Either String Spatial
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RegionSum -> Spatial
Spatial (RegionSum -> Spatial)
-> ([RegionProd] -> RegionSum) -> [RegionProd] -> Spatial
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RegionProd] -> RegionSum
Sum ([RegionProd] -> Either String Spatial)
-> [RegionProd] -> Either String Spatial
forall a b. (a -> b) -> a -> b
$ [RegionProd]
sums
  where
    asymmetryElim :: V.Vec n (Interval a) -> UnionNF n (Interval a)
    asymmetryElim :: Vec n (Interval a) -> UnionNF n (Interval a)
asymmetryElim Vec n (Interval a)
ints
      | Just Int
ix <- Vec n (Interval a) -> Maybe Int
forall (n :: Nat) (a :: Bound). Vec n (Interval a) -> Maybe Int
findAsymmetry Vec n (Interval a)
ints =
        case Vec n (Interval a)
ints Vec n (Interval a) -> Int -> Interval a
forall (n :: Nat) a. Vec n a -> Int -> a
V.!! Int
ix of
          IntervHoled Int64
m Int64
n Bool
p ->
            Vec n (Interval 'Standard) -> UnionNF n (Interval 'Standard)
forall (n :: Nat) (a :: Bound).
Vec n (Interval a) -> UnionNF n (Interval a)
asymmetryElim (Int
-> Interval 'Standard
-> Vec n (Interval 'Standard)
-> Vec n (Interval 'Standard)
forall a (n :: Nat). Int -> a -> Vec n a -> Vec n a
V.replace Int
ix (Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled Int64
m Int64
0 Bool
p) Vec n (Interval a)
Vec n (Interval 'Standard)
ints) UnionNF n (Interval 'Standard)
-> UnionNF n (Interval 'Standard) -> UnionNF n (Interval 'Standard)
forall a. Semigroup a => a -> a -> a
SG.<>
            Vec n (Interval 'Standard) -> UnionNF n (Interval 'Standard)
forall (n :: Nat) (a :: Bound).
Vec n (Interval a) -> UnionNF n (Interval a)
asymmetryElim (Int
-> Interval 'Standard
-> Vec n (Interval 'Standard)
-> Vec n (Interval 'Standard)
forall a (n :: Nat). Int -> a -> Vec n a -> Vec n a
V.replace Int
ix (Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled Int64
0 Int64
n Bool
p) Vec n (Interval a)
Vec n (Interval 'Standard)
ints)
          Interval a
_ -> String -> UnionNF n (Interval a)
forall a. HasCallStack => String -> a
error String
"intervalsToRegions: asymmetryElim: case ints V.!! ix of ..."
      | Bool
otherwise = Vec n (Interval a) -> UnionNF n (Interval a)
forall (m :: * -> *) a. Monad m => a -> m a
return Vec n (Interval a)
ints
    findAsymmetry :: Vec n (Interval a) -> Maybe Int
findAsymmetry =
      (Interval a -> Bool) -> Vec n (Interval a) -> Maybe Int
forall a (n :: Nat). (a -> Bool) -> Vec n a -> Maybe Int
V.findIndex ((Interval a -> Bool) -> Vec n (Interval a) -> Maybe Int)
-> (Interval a -> Bool) -> Vec n (Interval a) -> Maybe Int
forall a b. (a -> b) -> a -> b
$ \case
        (IntervHoled Int64
m Int64
n Bool
_) -> Int64
m Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int64
0 Bool -> Bool -> Bool
&& Int64
n Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int64
0 Bool -> Bool -> Bool
&& Int64
m Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
/= -Int64
n
        Interval a
_ -> Bool
False

    toProd :: V.Vec n (Interval 'Standard) -> Either String RegionProd
    toProd :: Vec n (Interval 'Standard) -> Either String RegionProd
toProd Vec n (Interval 'Standard)
ints =
      ([Region] -> RegionProd)
-> Either String [Region] -> Either String RegionProd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Region] -> RegionProd
Product (Either String [Region] -> Either String RegionProd)
-> Either String [Region] -> Either String RegionProd
forall a b. (a -> b) -> a -> b
$ ((Interval 'Standard, Int) -> Either String Region)
-> [(Interval 'Standard, Int)] -> Either String [Region]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Interval 'Standard, Int) -> Either String Region
convert
                   ([(Interval 'Standard, Int)] -> Either String [Region])
-> ([(Interval 'Standard, Int)] -> [(Interval 'Standard, Int)])
-> [(Interval 'Standard, Int)]
-> Either String [Region]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Interval 'Standard, Int) -> Bool)
-> [(Interval 'Standard, Int)] -> [(Interval 'Standard, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Interval 'Standard -> Bool
isNonInf (Interval 'Standard -> Bool)
-> ((Interval 'Standard, Int) -> Interval 'Standard)
-> (Interval 'Standard, Int)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Interval 'Standard, Int) -> Interval 'Standard
forall a b. (a, b) -> a
fst)
                   ([(Interval 'Standard, Int)] -> Either String [Region])
-> [(Interval 'Standard, Int)] -> Either String [Region]
forall a b. (a -> b) -> a -> b
$ [Interval 'Standard] -> [Int] -> [(Interval 'Standard, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Vec n (Interval 'Standard) -> [Interval 'Standard]
forall (n :: Nat) a. Vec n a -> [a]
V.toList Vec n (Interval 'Standard)
ints) [Int
0..]

    isNonInf :: Interval 'Standard -> Bool
    isNonInf :: Interval 'Standard -> Bool
isNonInf Interval 'Standard
IntervInfinite = Bool
False
    isNonInf Interval 'Standard
_ = Bool
True

    convert :: (Interval 'Standard, Int) -> Either String Region
    convert :: (Interval 'Standard, Int) -> Either String Region
convert (IntervHoled Int64
0 Int64
0 Bool
False, Int
_) =
      String -> Either String Region
forall a b. a -> Either a b
Left String
"Empty set cannot be realised as a region."
    convert (IntervHoled Int64
0 Int64
0 Bool
True, Int
ix) = Region -> Either String Region
forall (m :: * -> *) a. Monad m => a -> m a
return (Region -> Either String Region) -> Region -> Either String Region
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Bool -> Region
Centered Int
0 (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Bool
True
    convert (IntervHoled Int64
0 Int64
m Bool
p, Int
ix) = Region -> Either String Region
forall (m :: * -> *) a. Monad m => a -> m a
return (Region -> Either String Region) -> Region -> Either String Region
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Bool -> Region
Forward (Int64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
m) (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Bool
p
    convert (IntervHoled Int64
m Int64
0 Bool
p, Int
ix) = Region -> Either String Region
forall (m :: * -> *) a. Monad m => a -> m a
return (Region -> Either String Region) -> Region -> Either String Region
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Bool -> Region
Backward (Int64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64 -> Int) -> Int64 -> Int
forall a b. (a -> b) -> a -> b
$ -Int64
m) (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Bool
p
    convert (IntervHoled Int64
m Int64
n Bool
p, Int
ix)
      | Int64
m Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== -Int64
n = Region -> Either String Region
forall (m :: * -> *) a. Monad m => a -> m a
return (Region -> Either String Region) -> Region -> Either String Region
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Bool -> Region
Centered (Int64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
n) (Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Bool
p
      | Bool
otherwise = String -> Either String Region
forall a b. a -> Either a b
Left (String -> Either String Region) -> String -> Either String Region
forall a b. (a -> b) -> a -> b
$
        String
"Impossible: the lower bound is not negation of upper bound. " String -> String -> String
forall a. [a] -> [a] -> [a]
++
        String
"Should have been separated before."
    convert (Interval 'Standard, Int)
_ = String -> Either String Region
forall a b. a -> Either a b
Left String
"Infinite interval cannot be realised as a region."

regionsToIntervals :: forall n .
                      V.Natural n
                   -> Spatial
                   -> Either String (UnionNF n (Interval 'Standard))
regionsToIntervals :: Natural n
-> Spatial -> Either String (UnionNF n (Interval 'Standard))
regionsToIntervals Natural n
nOfDims (Spatial (Sum [RegionProd]
prods))
    | [RegionProd] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RegionProd]
prods = String -> Either String (UnionNF n (Interval 'Standard))
forall a b. a -> Either a b
Left String
"Empty region sum"
    | Bool
otherwise =
      (NonEmpty (UnionNF n (Interval 'Standard))
 -> UnionNF n (Interval 'Standard))
-> Either String (NonEmpty (UnionNF n (Interval 'Standard)))
-> Either String (UnionNF n (Interval 'Standard))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty (UnionNF n (Interval 'Standard))
-> UnionNF n (Interval 'Standard)
forall a. Semigroup a => NonEmpty a -> a
SG.sconcat (Either String (NonEmpty (UnionNF n (Interval 'Standard)))
 -> Either String (UnionNF n (Interval 'Standard)))
-> ([RegionProd]
    -> Either String (NonEmpty (UnionNF n (Interval 'Standard))))
-> [RegionProd]
-> Either String (UnionNF n (Interval 'Standard))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (Either String (UnionNF n (Interval 'Standard)))
-> Either String (NonEmpty (UnionNF n (Interval 'Standard)))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (NonEmpty (Either String (UnionNF n (Interval 'Standard)))
 -> Either String (NonEmpty (UnionNF n (Interval 'Standard))))
-> ([RegionProd]
    -> NonEmpty (Either String (UnionNF n (Interval 'Standard))))
-> [RegionProd]
-> Either String (NonEmpty (UnionNF n (Interval 'Standard)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RegionProd -> Either String (UnionNF n (Interval 'Standard)))
-> NonEmpty RegionProd
-> NonEmpty (Either String (UnionNF n (Interval 'Standard)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RegionProd -> Either String (UnionNF n (Interval 'Standard))
convert (NonEmpty RegionProd
 -> NonEmpty (Either String (UnionNF n (Interval 'Standard))))
-> ([RegionProd] -> NonEmpty RegionProd)
-> [RegionProd]
-> NonEmpty (Either String (UnionNF n (Interval 'Standard)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RegionProd] -> NonEmpty RegionProd
forall a. [a] -> NonEmpty a
NE.fromList ([RegionProd] -> Either String (UnionNF n (Interval 'Standard)))
-> [RegionProd] -> Either String (UnionNF n (Interval 'Standard))
forall a b. (a -> b) -> a -> b
$ [RegionProd]
prods
  where
    convert :: RegionProd -> Either String (UnionNF n (Interval 'Standard))
    convert :: RegionProd -> Either String (UnionNF n (Interval 'Standard))
convert (Product [Region]
rs)
      | [Region] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Region]
rs = String -> Either String (UnionNF n (Interval 'Standard))
forall a b. a -> Either a b
Left String
"Empty region product"
      | Bool
otherwise = UnionNF n (Interval 'Standard)
-> Either String (UnionNF n (Interval 'Standard))
forall a b. b -> Either a b
Right (UnionNF n (Interval 'Standard)
 -> Either String (UnionNF n (Interval 'Standard)))
-> UnionNF n (Interval 'Standard)
-> Either String (UnionNF n (Interval 'Standard))
forall a b. (a -> b) -> a -> b
$ NonEmpty (UnionNF n (Interval 'Standard))
-> UnionNF n (Interval 'Standard)
forall a (f :: * -> *). (Lattice a, Foldable1 f) => f a -> a
meets1 (NonEmpty (UnionNF n (Interval 'Standard))
 -> UnionNF n (Interval 'Standard))
-> ([Region] -> NonEmpty (UnionNF n (Interval 'Standard)))
-> [Region]
-> UnionNF n (Interval 'Standard)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionNF n (Interval 'Standard)]
-> NonEmpty (UnionNF n (Interval 'Standard))
forall a. [a] -> NonEmpty a
NE.fromList ([UnionNF n (Interval 'Standard)]
 -> NonEmpty (UnionNF n (Interval 'Standard)))
-> ([Region] -> [UnionNF n (Interval 'Standard)])
-> [Region]
-> NonEmpty (UnionNF n (Interval 'Standard))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Region -> UnionNF n (Interval 'Standard))
-> [Region] -> [UnionNF n (Interval 'Standard)]
forall a b. (a -> b) -> [a] -> [b]
map Region -> UnionNF n (Interval 'Standard)
convert' ([Region] -> UnionNF n (Interval 'Standard))
-> [Region] -> UnionNF n (Interval 'Standard)
forall a b. (a -> b) -> a -> b
$ [Region]
rs

    convert' :: Region -> UnionNF n (Interval 'Standard)
convert' Region
r = Vec n (Interval 'Standard) -> UnionNF n (Interval 'Standard)
forall (m :: * -> *) a. Monad m => a -> m a
return (Vec n (Interval 'Standard) -> UnionNF n (Interval 'Standard))
-> Vec n (Interval 'Standard) -> UnionNF n (Interval 'Standard)
forall a b. (a -> b) -> a -> b
$ Natural n
-> (Int, Interval 'Standard) -> Vec n (Interval 'Standard)
forall (n' :: Nat).
Natural n'
-> (Int, Interval 'Standard) -> Vec n' (Interval 'Standard)
proto Natural n
nOfDims ((Int, Interval 'Standard) -> Vec n (Interval 'Standard))
-> (Int, Interval 'Standard) -> Vec n (Interval 'Standard)
forall a b. (a -> b) -> a -> b
$
      case Region
r of
        Forward  Int
dep Int
dim Bool
p -> (Int
dimInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1, Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled Int64
0 (Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
dep) Bool
p)
        Backward Int
dep Int
dim Bool
p -> (Int
dimInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1, Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled (- Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
dep) Int64
0 Bool
p)
        Centered Int
dep Int
dim Bool
p -> (Int
dimInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1, Int64 -> Int64 -> Bool -> Interval 'Standard
IntervHoled (- Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
dep) (Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
dep) Bool
p)

    proto :: forall n' .
             V.Natural n'
          -> (Int, Interval 'Standard)
          -> V.Vec n' (Interval 'Standard)
    proto :: Natural n'
-> (Int, Interval 'Standard) -> Vec n' (Interval 'Standard)
proto Natural n'
V.Zero (Int, Interval 'Standard)
_ = Vec n' (Interval 'Standard)
forall a. Vec 'Z a
V.Nil
    proto (V.Succ Natural n
n) (Int
i, Interval 'Standard
interv) = Interval 'Standard
-> Vec n (Interval 'Standard) -> Vec ('S n) (Interval 'Standard)
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
V.Cons
      (if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Interval 'Standard
interv else Interval 'Standard
IntervInfinite)
      (Natural n
-> (Int, Interval 'Standard) -> Vec n (Interval 'Standard)
forall (n' :: Nat).
Natural n'
-> (Int, Interval 'Standard) -> Vec n' (Interval 'Standard)
proto Natural n
n (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1, Interval 'Standard
interv))