{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Camfort.Specification.Stencils.Consistency ( consistent
                                                  , ConsistencyResult(..) ) where

import qualified Camfort.Helpers.Vec as V
import Camfort.Specification.Stencils.DenotationalSemantics
import Camfort.Specification.Stencils.Model
import Camfort.Specification.Stencils.Syntax
import Camfort.Analysis (ExitCodeOfReport(..))

data ConsistencyResult =
    Consistent
  | Inconsistent String
  deriving (ConsistencyResult -> ConsistencyResult -> Bool
(ConsistencyResult -> ConsistencyResult -> Bool)
-> (ConsistencyResult -> ConsistencyResult -> Bool)
-> Eq ConsistencyResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConsistencyResult -> ConsistencyResult -> Bool
$c/= :: ConsistencyResult -> ConsistencyResult -> Bool
== :: ConsistencyResult -> ConsistencyResult -> Bool
$c== :: ConsistencyResult -> ConsistencyResult -> Bool
Eq, Int -> ConsistencyResult -> ShowS
[ConsistencyResult] -> ShowS
ConsistencyResult -> String
(Int -> ConsistencyResult -> ShowS)
-> (ConsistencyResult -> String)
-> ([ConsistencyResult] -> ShowS)
-> Show ConsistencyResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConsistencyResult] -> ShowS
$cshowList :: [ConsistencyResult] -> ShowS
show :: ConsistencyResult -> String
$cshow :: ConsistencyResult -> String
showsPrec :: Int -> ConsistencyResult -> ShowS
$cshowsPrec :: Int -> ConsistencyResult -> ShowS
Show)

instance ExitCodeOfReport ConsistencyResult where
  exitCodeOf :: ConsistencyResult -> Int
exitCodeOf ConsistencyResult
Consistent = Int
0
  exitCodeOf (Inconsistent String
_) = Int
1

-- | This function checks multiplicity consistency and then delegates the
-- spatial consistency to |consistent'| function.
consistent :: forall n .
              Specification
           -> Multiplicity (UnionNF n Offsets)
           -> ConsistencyResult
consistent :: Specification
-> Multiplicity (UnionNF n Offsets) -> ConsistencyResult
consistent (Specification Multiplicity (Approximation Spatial)
mult Bool
_) Multiplicity (UnionNF n Offsets)
observedIxs =
    -- First do the linearity check
    case (Multiplicity (Approximation (UnionNF n (Interval 'Standard)))
specModel, Multiplicity (UnionNF n Offsets)
observedIxs) of
      (Mult Approximation (UnionNF n (Interval 'Standard))
a, Mult UnionNF n Offsets
b) -> Approximation (UnionNF n (Interval 'Standard))
a Approximation (UnionNF n (Interval 'Standard))
-> UnionNF n Offsets -> ConsistencyResult
forall (n :: Nat).
Approximation (UnionNF n (Interval 'Standard))
-> UnionNF n Offsets -> ConsistencyResult
`consistent'` UnionNF n Offsets
b
      (Once Approximation (UnionNF n (Interval 'Standard))
a, Once UnionNF n Offsets
b) -> Approximation (UnionNF n (Interval 'Standard))
a Approximation (UnionNF n (Interval 'Standard))
-> UnionNF n Offsets -> ConsistencyResult
forall (n :: Nat).
Approximation (UnionNF n (Interval 'Standard))
-> UnionNF n Offsets -> ConsistencyResult
`consistent'` UnionNF n Offsets
b
      (Once Approximation (UnionNF n (Interval 'Standard))
_, Mult UnionNF n Offsets
_) ->String -> ConsistencyResult
Inconsistent
        String
"Specification is readOnce, but there are repeated indices."
      (Mult Approximation (UnionNF n (Interval 'Standard))
_, Once UnionNF n Offsets
_) -> String -> ConsistencyResult
Inconsistent
        String
"Specification lacks readOnce, but the indices are unique."
  where
    specModel :: Multiplicity (Approximation (UnionNF n (Interval 'Standard)))
    specModel :: Multiplicity (Approximation (UnionNF n (Interval 'Standard)))
specModel =
      case Multiplicity
  (Either String (Approximation (UnionNF n (Interval 'Standard))))
-> Either
     String
     (Multiplicity (Approximation (UnionNF n (Interval 'Standard))))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Multiplicity
   (Either String (Approximation (UnionNF n (Interval 'Standard))))
 -> Either
      String
      (Multiplicity (Approximation (UnionNF n (Interval 'Standard)))))
-> Multiplicity
     (Either String (Approximation (UnionNF n (Interval 'Standard))))
-> Either
     String
     (Multiplicity (Approximation (UnionNF n (Interval 'Standard))))
forall a b. (a -> b) -> a -> b
$ (Approximation (Either String (UnionNF n (Interval 'Standard)))
-> Either String (Approximation (UnionNF n (Interval 'Standard)))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Approximation (Either String (UnionNF n (Interval 'Standard)))
 -> Either String (Approximation (UnionNF n (Interval 'Standard))))
-> (Approximation Spatial
    -> Approximation (Either String (UnionNF n (Interval 'Standard))))
-> Approximation Spatial
-> Either String (Approximation (UnionNF n (Interval 'Standard)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Spatial -> Either String (UnionNF n (Interval 'Standard)))
-> Approximation Spatial
-> Approximation (Either String (UnionNF n (Interval 'Standard)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Natural n
-> Spatial -> Either String (UnionNF n (Interval 'Standard))
forall (n :: Nat).
Natural n
-> Spatial -> Either String (UnionNF n (Interval 'Standard))
regionsToIntervals Natural n
nOfDims)) (Approximation Spatial
 -> Either String (Approximation (UnionNF n (Interval 'Standard))))
-> Multiplicity (Approximation Spatial)
-> Multiplicity
     (Either String (Approximation (UnionNF n (Interval 'Standard))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Multiplicity (Approximation Spatial)
mult of
        Right Multiplicity (Approximation (UnionNF n (Interval 'Standard)))
model -> Multiplicity (Approximation (UnionNF n (Interval 'Standard)))
model
        Left String
msg -> String
-> Multiplicity (Approximation (UnionNF n (Interval 'Standard)))
forall a. HasCallStack => String -> a
error String
msg

    nOfDims :: V.Natural n
    nOfDims :: Natural n
nOfDims = UnionNF n Offsets -> Natural n
forall (n :: Nat) a. UnionNF n a -> Natural n
vecLength (UnionNF n Offsets -> Natural n)
-> (Multiplicity (UnionNF n Offsets) -> UnionNF n Offsets)
-> Multiplicity (UnionNF n Offsets)
-> Natural n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Multiplicity (UnionNF n Offsets) -> UnionNF n Offsets
forall a. Peelable a => a -> CoreTyp a
peel (Multiplicity (UnionNF n Offsets) -> Natural n)
-> Multiplicity (UnionNF n Offsets) -> Natural n
forall a b. (a -> b) -> a -> b
$ Multiplicity (UnionNF n Offsets)
observedIxs

-- | This is the actual consistency check using set comparison supplied in
-- the model.
consistent' :: Approximation (UnionNF n (Interval 'Standard))
            -> UnionNF n Offsets
            -> ConsistencyResult
consistent' :: Approximation (UnionNF n (Interval 'Standard))
-> UnionNF n Offsets -> ConsistencyResult
consistent' (Exact UnionNF n (Interval 'Standard)
unf) UnionNF n Offsets
ixs =
  case UnionNF n (Interval 'Standard) -> UnionNF n Offsets -> Ordering
forall a b (n :: Nat).
(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 (Interval 'Standard)
unf UnionNF n Offsets
ixs of
    Ordering
EQ -> ConsistencyResult
Consistent
    Ordering
LT ->
      String -> ConsistencyResult
Inconsistent String
"The specification covers a smaller area than the indices."
    Ordering
GT ->
      String -> ConsistencyResult
Inconsistent String
"The specification covers a larger area than the indices."
consistent' (Bound (Just UnionNF n (Interval 'Standard)
unf) Maybe (UnionNF n (Interval 'Standard))
Nothing) UnionNF n Offsets
ixs =
  case UnionNF n (Interval 'Standard) -> UnionNF n Offsets -> Ordering
forall a b (n :: Nat).
(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 (Interval 'Standard)
unf UnionNF n Offsets
ixs of
    Ordering
EQ -> ConsistencyResult
Consistent
    Ordering
LT -> ConsistencyResult
Consistent
    Ordering
GT -> String -> ConsistencyResult
Inconsistent (String -> ConsistencyResult) -> String -> ConsistencyResult
forall a b. (a -> b) -> a -> b
$
      String
"There are indices covered by the lower bound specification, but " String -> ShowS
forall a. [a] -> [a] -> [a]
++
      String
"could not observed in the indices."
consistent' (Bound Maybe (UnionNF n (Interval 'Standard))
Nothing (Just UnionNF n (Interval 'Standard)
unf)) UnionNF n Offsets
ixs =
  case UnionNF n (Interval 'Standard) -> UnionNF n Offsets -> Ordering
forall a b (n :: Nat).
(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 (Interval 'Standard)
unf UnionNF n Offsets
ixs of
    Ordering
EQ -> ConsistencyResult
Consistent
    Ordering
GT -> ConsistencyResult
Consistent
    Ordering
LT -> String -> ConsistencyResult
Inconsistent
      String
"There are indices outside the upper bound specification."
consistent' (Bound Maybe (UnionNF n (Interval 'Standard))
lb Maybe (UnionNF n (Interval 'Standard))
ub) UnionNF n Offsets
ixs =
  case (ConsistencyResult
cLower, ConsistencyResult
cUpper) of
    (ConsistencyResult
Consistent, ConsistencyResult
Consistent) -> ConsistencyResult
Consistent
    (ConsistencyResult
Consistent, ConsistencyResult
inconsistent) -> ConsistencyResult
inconsistent
    (ConsistencyResult
inconsistent, ConsistencyResult
Consistent) -> ConsistencyResult
inconsistent
    (Inconsistent{}, Inconsistent{}) -> String -> ConsistencyResult
Inconsistent
      String
"Neither the lower nor ther upper bound conform with the indices."
  where
    cLower :: ConsistencyResult
cLower = Maybe (UnionNF n (Interval 'Standard))
-> Maybe (UnionNF n (Interval 'Standard))
-> Approximation (UnionNF n (Interval 'Standard))
forall a. Maybe a -> Maybe a -> Approximation a
Bound Maybe (UnionNF n (Interval 'Standard))
lb Maybe (UnionNF n (Interval 'Standard))
forall a. Maybe a
Nothing Approximation (UnionNF n (Interval 'Standard))
-> UnionNF n Offsets -> ConsistencyResult
forall (n :: Nat).
Approximation (UnionNF n (Interval 'Standard))
-> UnionNF n Offsets -> ConsistencyResult
`consistent'` UnionNF n Offsets
ixs
    cUpper :: ConsistencyResult
cUpper = Maybe (UnionNF n (Interval 'Standard))
-> Maybe (UnionNF n (Interval 'Standard))
-> Approximation (UnionNF n (Interval 'Standard))
forall a. Maybe a -> Maybe a -> Approximation a
Bound Maybe (UnionNF n (Interval 'Standard))
forall a. Maybe a
Nothing Maybe (UnionNF n (Interval 'Standard))
ub Approximation (UnionNF n (Interval 'Standard))
-> UnionNF n Offsets -> ConsistencyResult
forall (n :: Nat).
Approximation (UnionNF n (Interval 'Standard))
-> UnionNF n Offsets -> ConsistencyResult
`consistent'` UnionNF n Offsets
ixs