{-
   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.
-}

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams #-}

module Camfort.Specification.Stencils.CheckFrontend
  (
    -- * Stencil checking
    stencilChecking
    -- ** Validation Results
  , CheckResult
  , checkFailure
  , checkWarnings
    -- ** Helpers
  , existingStencils
  ) where

import           Prelude hiding (span)

import           Control.DeepSeq
import           Control.Monad.Reader (ReaderT, asks, runReaderT)
import           Control.Monad.State.Strict hiding (state)
import           Control.Monad.Writer.Lazy hiding (Product)
import           Data.Function (on)
import           Data.Generics.Uniplate.Operations
import           Data.List (intercalate, sort, union)
import           Data.Maybe

import           Camfort.Analysis
import           Camfort.Analysis.Annotations
import           Camfort.Analysis.CommentAnnotator
import           Camfort.Specification.Parser (SpecParseError)
import           Camfort.Specification.Stencils.Analysis (StencilsAnalysis)
import           Camfort.Specification.Stencils.Annotation (SA)
import qualified Camfort.Specification.Stencils.Annotation as SA
import           Camfort.Specification.Stencils.CheckBackend
import           Camfort.Specification.Stencils.Generate
import           Camfort.Specification.Stencils.Model
import qualified Camfort.Specification.Stencils.Parser as Parser
import           Camfort.Specification.Stencils.Parser.Types (reqRegions)
import           Camfort.Specification.Stencils.Syntax

import qualified Language.Fortran.AST as F
import qualified Language.Fortran.Analysis as FA
import qualified Language.Fortran.Analysis.BBlocks as FAB
import qualified Language.Fortran.Analysis.DataFlow as FAD
import qualified Language.Fortran.Util.Position as FU

-- TODO: Replace instances of this with logging of errors and warnings
newtype CheckResult = CheckResult [StencilResult]
instance NFData CheckResult where
  rnf :: CheckResult -> ()
rnf CheckResult
_ = ()
instance ExitCodeOfReport CheckResult where
  exitCodeOf :: CheckResult -> Int
exitCodeOf (CheckResult [StencilResult]
rs) = [StencilResult] -> Int
forall a. ExitCodeOfReport a => [a] -> Int
exitCodeOfSet [StencilResult]
rs

-- | Retrieve a list of 'StencilResult' from a 'CheckResult'.
--
-- Ensures correct ordering of results.
getCheckResult :: CheckResult -> [StencilResult]
getCheckResult :: CheckResult -> [StencilResult]
getCheckResult (CheckResult [StencilResult]
rs) = [StencilResult] -> [StencilResult]
forall a. Ord a => [a] -> [a]
sort [StencilResult]
rs

instance Eq CheckResult where
  == :: CheckResult -> CheckResult -> Bool
(==) = [StencilResult] -> [StencilResult] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([StencilResult] -> [StencilResult] -> Bool)
-> (CheckResult -> [StencilResult])
-> CheckResult
-> CheckResult
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CheckResult -> [StencilResult]
getCheckResult

-- | Represents only the check results for invalid stencils.
newtype CheckError  = CheckError { CheckError -> [StencilCheckError]
getCheckError :: [StencilCheckError] }

-- | Represents only the check results that resulted in warnings.
newtype CheckWarning = CheckWarning { CheckWarning -> [StencilCheckWarning]
getCheckWarning :: [StencilCheckWarning] }

-- | Retrieve the checks for invalid stencils from a 'CheckResult'. Result is
-- Nothing if there are no invalid checks.
checkFailure :: CheckResult -> Maybe CheckError
checkFailure :: CheckResult -> Maybe CheckError
checkFailure CheckResult
c = case [Maybe StencilCheckError] -> [StencilCheckError]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe StencilCheckError] -> [StencilCheckError])
-> [Maybe StencilCheckError] -> [StencilCheckError]
forall a b. (a -> b) -> a -> b
$ (StencilResult -> Maybe StencilCheckError)
-> [StencilResult] -> [Maybe StencilCheckError]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap StencilResult -> Maybe StencilCheckError
toFailure (CheckResult -> [StencilResult]
getCheckResult CheckResult
c) of
                 [] -> Maybe CheckError
forall a. Maybe a
Nothing
                 [StencilCheckError]
xs -> CheckError -> Maybe CheckError
forall a. a -> Maybe a
Just (CheckError -> Maybe CheckError) -> CheckError -> Maybe CheckError
forall a b. (a -> b) -> a -> b
$ [StencilCheckError] -> CheckError
CheckError [StencilCheckError]
xs
  where toFailure :: StencilResult -> Maybe StencilCheckError
toFailure (SCFail StencilCheckError
err) = StencilCheckError -> Maybe StencilCheckError
forall a. a -> Maybe a
Just StencilCheckError
err
        toFailure StencilResult
_            = Maybe StencilCheckError
forall a. Maybe a
Nothing

checkWarnings :: CheckResult -> Maybe CheckWarning
checkWarnings :: CheckResult -> Maybe CheckWarning
checkWarnings CheckResult
c = case [Maybe StencilCheckWarning] -> [StencilCheckWarning]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe StencilCheckWarning] -> [StencilCheckWarning])
-> [Maybe StencilCheckWarning] -> [StencilCheckWarning]
forall a b. (a -> b) -> a -> b
$ (StencilResult -> Maybe StencilCheckWarning)
-> [StencilResult] -> [Maybe StencilCheckWarning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap StencilResult -> Maybe StencilCheckWarning
toWarning (CheckResult -> [StencilResult]
getCheckResult CheckResult
c) of
                    [] -> Maybe CheckWarning
forall a. Maybe a
Nothing
                    [StencilCheckWarning]
xs -> CheckWarning -> Maybe CheckWarning
forall a. a -> Maybe a
Just (CheckWarning -> Maybe CheckWarning)
-> CheckWarning -> Maybe CheckWarning
forall a b. (a -> b) -> a -> b
$ [StencilCheckWarning] -> CheckWarning
CheckWarning [StencilCheckWarning]
xs
  where toWarning :: StencilResult -> Maybe StencilCheckWarning
toWarning (SCWarn StencilCheckWarning
warn) = StencilCheckWarning -> Maybe StencilCheckWarning
forall a. a -> Maybe a
Just StencilCheckWarning
warn
        toWarning StencilResult
_             = Maybe StencilCheckWarning
forall a. Maybe a
Nothing

-- | Result of stencil validation.
data StencilResult
  -- | No issues were identified with the stencil at the given position.
  = SCOkay { StencilResult -> SrcSpan
scSpan :: FU.SrcSpan
           , StencilResult -> Specification
scSpec :: Specification
           , StencilResult -> Variable
scVar  :: Variable
           , StencilResult -> SrcSpan
scBodySpan :: FU.SrcSpan
           }
  -- | Validation of stencil failed. See 'StencilCheckError' for information
  -- on the types of validation errors that can occur.
  | SCFail StencilCheckError
  -- | A warning which shouldn't interrupt other procedures.
  | SCWarn StencilCheckWarning
  deriving (StencilResult -> StencilResult -> Bool
(StencilResult -> StencilResult -> Bool)
-> (StencilResult -> StencilResult -> Bool) -> Eq StencilResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StencilResult -> StencilResult -> Bool
$c/= :: StencilResult -> StencilResult -> Bool
== :: StencilResult -> StencilResult -> Bool
$c== :: StencilResult -> StencilResult -> Bool
Eq)

instance ExitCodeOfReport StencilResult where
  exitCodeOf :: StencilResult -> Int
exitCodeOf (SCOkay {}) = Int
0
  exitCodeOf (SCFail StencilCheckError
_) = Int
1
  exitCodeOf (SCWarn StencilCheckWarning
_) = Int
0

class GetSpan a where
  getSpan :: a -> FU.SrcSpan

instance GetSpan StencilResult where
  getSpan :: StencilResult -> SrcSpan
getSpan SCOkay{scSpan :: StencilResult -> SrcSpan
scSpan = SrcSpan
srcSpan} = SrcSpan
srcSpan
  getSpan (SCFail StencilCheckError
err)             = StencilCheckError -> SrcSpan
forall a. GetSpan a => a -> SrcSpan
getSpan StencilCheckError
err
  getSpan (SCWarn StencilCheckWarning
warn)            = StencilCheckWarning -> SrcSpan
forall a. GetSpan a => a -> SrcSpan
getSpan StencilCheckWarning
warn

instance GetSpan StencilCheckError where
  getSpan :: StencilCheckError -> SrcSpan
getSpan (SynToAstError     SynToAstError
_ SrcSpan
srcSpan)      = SrcSpan
srcSpan
  getSpan (NotWellSpecified  (SrcSpan
srcSpan, SpecDecls
_) (SrcSpan, SpecDecls)
_) = SrcSpan
srcSpan
  getSpan (ParseError SrcSpan
srcSpan SpecParseError SpecParseError
_)             = SrcSpan
srcSpan
  getSpan (RegionExists SrcSpan
srcSpan Variable
_)           = SrcSpan
srcSpan

instance GetSpan StencilCheckWarning where
  getSpan :: StencilCheckWarning -> SrcSpan
getSpan (DuplicateSpecification SrcSpan
srcSpan) = SrcSpan
srcSpan
  getSpan (UnusedRegion SrcSpan
srcSpan Variable
_)         = SrcSpan
srcSpan

instance Ord StencilResult where
  compare :: StencilResult -> StencilResult -> Ordering
compare = SrcSpan -> SrcSpan -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SrcSpan -> SrcSpan -> Ordering)
-> (StencilResult -> SrcSpan)
-> StencilResult
-> StencilResult
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` StencilResult -> SrcSpan
forall a. GetSpan a => a -> SrcSpan
getSpan

instance Ord StencilCheckError where
  compare :: StencilCheckError -> StencilCheckError -> Ordering
compare = SrcSpan -> SrcSpan -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SrcSpan -> SrcSpan -> Ordering)
-> (StencilCheckError -> SrcSpan)
-> StencilCheckError
-> StencilCheckError
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` StencilCheckError -> SrcSpan
forall a. GetSpan a => a -> SrcSpan
getSpan

-- | Represents a way in which validation of a stencil can fail.
data StencilCheckError
  -- | Error occurred during conversion from parsed representation to AST.
  = SynToAstError SynToAstError FU.SrcSpan
  -- | The existing stencil conflicts with an inferred stencil.
  | NotWellSpecified (FU.SrcSpan, SpecDecls) (FU.SrcSpan, SpecDecls)
  -- | The stencil could not be parsed correctly.
  | ParseError FU.SrcSpan (SpecParseError Parser.SpecParseError)
  -- | A definition for the region alias already exists.
  | RegionExists FU.SrcSpan Variable
  deriving (StencilCheckError -> StencilCheckError -> Bool
(StencilCheckError -> StencilCheckError -> Bool)
-> (StencilCheckError -> StencilCheckError -> Bool)
-> Eq StencilCheckError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StencilCheckError -> StencilCheckError -> Bool
$c/= :: StencilCheckError -> StencilCheckError -> Bool
== :: StencilCheckError -> StencilCheckError -> Bool
$c== :: StencilCheckError -> StencilCheckError -> Bool
Eq)

-- | Create a check result informating a user of a 'SynToAstError'.
synToAstError :: SynToAstError -> FU.SrcSpan -> StencilResult
synToAstError :: SynToAstError -> SrcSpan -> StencilResult
synToAstError SynToAstError
err SrcSpan
srcSpan = StencilCheckError -> StencilResult
SCFail (StencilCheckError -> StencilResult)
-> StencilCheckError -> StencilResult
forall a b. (a -> b) -> a -> b
$ SynToAstError -> SrcSpan -> StencilCheckError
SynToAstError SynToAstError
err SrcSpan
srcSpan

-- | Create a check result informating a user of a 'NotWellSpecified' error.
notWellSpecified :: (FU.SrcSpan, SpecDecls) -> (FU.SrcSpan, SpecDecls) -> StencilResult
notWellSpecified :: (SrcSpan, SpecDecls) -> (SrcSpan, SpecDecls) -> StencilResult
notWellSpecified (SrcSpan, SpecDecls)
got (SrcSpan, SpecDecls)
inferred = StencilCheckError -> StencilResult
SCFail (StencilCheckError -> StencilResult)
-> StencilCheckError -> StencilResult
forall a b. (a -> b) -> a -> b
$ (SrcSpan, SpecDecls) -> (SrcSpan, SpecDecls) -> StencilCheckError
NotWellSpecified (SrcSpan, SpecDecls)
got (SrcSpan, SpecDecls)
inferred

-- | Create a check result informating a user of a parse error.
parseError :: FU.SrcSpan -> SpecParseError Parser.SpecParseError -> StencilResult
parseError :: SrcSpan -> SpecParseError SpecParseError -> StencilResult
parseError SrcSpan
srcSpan SpecParseError SpecParseError
err = StencilCheckError -> StencilResult
SCFail (StencilCheckError -> StencilResult)
-> StencilCheckError -> StencilResult
forall a b. (a -> b) -> a -> b
$ SrcSpan -> SpecParseError SpecParseError -> StencilCheckError
ParseError SrcSpan
srcSpan SpecParseError SpecParseError
err

-- | Create a check result informating that a region already exists.
regionExistsError :: FU.SrcSpan -> Variable -> StencilResult
regionExistsError :: SrcSpan -> Variable -> StencilResult
regionExistsError SrcSpan
srcSpan Variable
r = StencilCheckError -> StencilResult
SCFail (StencilCheckError -> StencilResult)
-> StencilCheckError -> StencilResult
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Variable -> StencilCheckError
RegionExists SrcSpan
srcSpan Variable
r

-- | Represents a non-fatal validation warning.
data StencilCheckWarning
  -- | Specification is defined multiple times.
  = DuplicateSpecification FU.SrcSpan
  -- | Region is defined but not used.
  | UnusedRegion FU.SrcSpan Variable
  deriving (StencilCheckWarning -> StencilCheckWarning -> Bool
(StencilCheckWarning -> StencilCheckWarning -> Bool)
-> (StencilCheckWarning -> StencilCheckWarning -> Bool)
-> Eq StencilCheckWarning
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StencilCheckWarning -> StencilCheckWarning -> Bool
$c/= :: StencilCheckWarning -> StencilCheckWarning -> Bool
== :: StencilCheckWarning -> StencilCheckWarning -> Bool
$c== :: StencilCheckWarning -> StencilCheckWarning -> Bool
Eq)

-- | Create a check result informing a user of a duplicate specification.
duplicateSpecification :: FU.SrcSpan -> StencilResult
duplicateSpecification :: SrcSpan -> StencilResult
duplicateSpecification = StencilCheckWarning -> StencilResult
SCWarn (StencilCheckWarning -> StencilResult)
-> (SrcSpan -> StencilCheckWarning) -> SrcSpan -> StencilResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> StencilCheckWarning
DuplicateSpecification

-- | Create a check result informating an unused region.
unusedRegion :: FU.SrcSpan -> Variable -> StencilResult
unusedRegion :: SrcSpan -> Variable -> StencilResult
unusedRegion SrcSpan
srcSpan Variable
var = StencilCheckWarning -> StencilResult
SCWarn (StencilCheckWarning -> StencilResult)
-> StencilCheckWarning -> StencilResult
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Variable -> StencilCheckWarning
UnusedRegion SrcSpan
srcSpan Variable
var

specOkay :: FU.SrcSpan -> Specification -> Variable -> FU.SrcSpan -> StencilResult
specOkay :: SrcSpan -> Specification -> Variable -> SrcSpan -> StencilResult
specOkay SrcSpan
spanSpec Specification
spec Variable
var SrcSpan
spanBody =
  SCOkay :: SrcSpan -> Specification -> Variable -> SrcSpan -> StencilResult
SCOkay { scSpan :: SrcSpan
scSpan      = SrcSpan
spanSpec
         , scSpec :: Specification
scSpec      = Specification
spec
         , scBodySpan :: SrcSpan
scBodySpan  = SrcSpan
spanBody
         , scVar :: Variable
scVar       = Variable
var
         }

-- | Pretty print a message with suitable spacing after the source position.
prettyWithSpan :: FU.SrcSpan -> String -> String
prettyWithSpan :: SrcSpan -> Variable -> Variable
prettyWithSpan SrcSpan
srcSpan Variable
s = SrcSpan -> Variable
forall a. Show a => a -> Variable
show SrcSpan
srcSpan Variable -> Variable -> Variable
forall a. [a] -> [a] -> [a]
++ Variable
"    " Variable -> Variable -> Variable
forall a. [a] -> [a] -> [a]
++ Variable
s

instance Show CheckResult where
  show :: CheckResult -> Variable
show = Variable -> [Variable] -> Variable
forall a. [a] -> [[a]] -> [a]
intercalate Variable
"\n" ([Variable] -> Variable)
-> (CheckResult -> [Variable]) -> CheckResult -> Variable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StencilResult -> Variable) -> [StencilResult] -> [Variable]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap StencilResult -> Variable
forall a. Show a => a -> Variable
show ([StencilResult] -> [Variable])
-> (CheckResult -> [StencilResult]) -> CheckResult -> [Variable]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckResult -> [StencilResult]
getCheckResult
instance Describe CheckResult

instance Show CheckError where
  show :: CheckError -> Variable
show = Variable -> [Variable] -> Variable
forall a. [a] -> [[a]] -> [a]
intercalate Variable
"\n" ([Variable] -> Variable)
-> (CheckError -> [Variable]) -> CheckError -> Variable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StencilCheckError -> Variable)
-> [StencilCheckError] -> [Variable]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap StencilCheckError -> Variable
forall a. Show a => a -> Variable
show ([StencilCheckError] -> [Variable])
-> (CheckError -> [StencilCheckError]) -> CheckError -> [Variable]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckError -> [StencilCheckError]
getCheckError

instance Show CheckWarning where
  show :: CheckWarning -> Variable
show = Variable -> [Variable] -> Variable
forall a. [a] -> [[a]] -> [a]
intercalate Variable
"\n" ([Variable] -> Variable)
-> (CheckWarning -> [Variable]) -> CheckWarning -> Variable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StencilCheckWarning -> Variable)
-> [StencilCheckWarning] -> [Variable]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap StencilCheckWarning -> Variable
forall a. Show a => a -> Variable
show ([StencilCheckWarning] -> [Variable])
-> (CheckWarning -> [StencilCheckWarning])
-> CheckWarning
-> [Variable]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckWarning -> [StencilCheckWarning]
getCheckWarning

instance Show StencilResult where
  show :: StencilResult -> Variable
show SCOkay{ scSpan :: StencilResult -> SrcSpan
scSpan = SrcSpan
span } = SrcSpan -> Variable -> Variable
prettyWithSpan SrcSpan
span Variable
"Correct."
  show (SCFail StencilCheckError
err)            = StencilCheckError -> Variable
forall a. Show a => a -> Variable
show StencilCheckError
err
  show (SCWarn StencilCheckWarning
warn)           = StencilCheckWarning -> Variable
forall a. Show a => a -> Variable
show StencilCheckWarning
warn

instance Show StencilCheckError where
  show :: StencilCheckError -> Variable
show (SynToAstError SynToAstError
err SrcSpan
srcSpan) = SrcSpan -> Variable -> Variable
prettyWithSpan SrcSpan
srcSpan (SynToAstError -> Variable
forall a. Show a => a -> Variable
show SynToAstError
err)
  show (NotWellSpecified (SrcSpan
spanActual, SpecDecls
stencilActual) (SrcSpan
spanInferred, SpecDecls
stencilInferred)) =
    [Variable] -> Variable
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Variable] -> Variable) -> [Variable] -> Variable
forall a b. (a -> b) -> a -> b
$ [SrcSpan -> Variable -> Variable
prettyWithSpan SrcSpan
spanActual Variable
"Not well specified.\n", Variable
sp,
             Variable
"Specification is:\n", Variable
sp, Variable
sp, SpecDecls -> Variable
pprintSpecDecls SpecDecls
stencilActual, Variable
"\n",
              Variable
sp, Variable
"but at ", SrcSpan -> Variable
forall a. Show a => a -> Variable
show SrcSpan
spanInferred] [Variable] -> [Variable] -> [Variable]
forall a. [a] -> [a] -> [a]
++ [Variable]
msg
    where
      sp :: Variable
sp = Int -> Char -> Variable
forall a. Int -> a -> [a]
replicate Int
8 Char
' '
      msg :: [Variable]
msg = case SpecDecls
stencilInferred of
              [] -> [Variable
" there is no specifiable array computation"]
              SpecDecls
_ ->  [Variable
" the code behaves as\n", Variable
sp, Variable
sp, SpecDecls -> Variable
pprintSpecDecls SpecDecls
stencilInferred]
  show (ParseError SrcSpan
srcSpan SpecParseError SpecParseError
err) = SrcSpan -> Variable -> Variable
prettyWithSpan SrcSpan
srcSpan (SpecParseError SpecParseError -> Variable
forall a. Show a => a -> Variable
show SpecParseError SpecParseError
err)
  show (RegionExists SrcSpan
srcSpan Variable
name) =
    SrcSpan -> Variable -> Variable
prettyWithSpan SrcSpan
srcSpan (Variable
"Region '" Variable -> Variable -> Variable
forall a. [a] -> [a] -> [a]
++ Variable
name Variable -> Variable -> Variable
forall a. [a] -> [a] -> [a]
++ Variable
"' already defined")

instance Show StencilCheckWarning where
  show :: StencilCheckWarning -> Variable
show (DuplicateSpecification SrcSpan
srcSpan) = SrcSpan -> Variable -> Variable
prettyWithSpan SrcSpan
srcSpan
    Variable
"Warning: Duplicate specification."
  show (UnusedRegion SrcSpan
srcSpan Variable
name)      = SrcSpan -> Variable -> Variable
prettyWithSpan SrcSpan
srcSpan (Variable -> Variable) -> Variable -> Variable
forall a b. (a -> b) -> a -> b
$
    Variable
"Warning: Unused region '" Variable -> Variable -> Variable
forall a. [a] -> [a] -> [a]
++ Variable
name Variable -> Variable -> Variable
forall a. [a] -> [a] -> [a]
++ Variable
"'"

-- Entry point
stencilChecking :: F.ProgramFile SA -> StencilsAnalysis CheckResult
stencilChecking :: ProgramFile SA -> StencilsAnalysis CheckResult
stencilChecking ProgramFile SA
pf = do
  (((), [StencilResult]) -> CheckResult)
-> AnalysisT () () Identity ((), [StencilResult])
-> StencilsAnalysis CheckResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([StencilResult] -> CheckResult
CheckResult ([StencilResult] -> CheckResult)
-> (((), [StencilResult]) -> [StencilResult])
-> ((), [StencilResult])
-> CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((), [StencilResult]) -> [StencilResult]
forall a b. (a, b) -> b
snd) (AnalysisT () () Identity ((), [StencilResult])
 -> StencilsAnalysis CheckResult)
-> (WriterT [StencilResult] (AnalysisT () () Identity) ()
    -> AnalysisT () () Identity ((), [StencilResult]))
-> WriterT [StencilResult] (AnalysisT () () Identity) ()
-> StencilsAnalysis CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT [StencilResult] (AnalysisT () () Identity) ()
-> AnalysisT () () Identity ((), [StencilResult])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT [StencilResult] (AnalysisT () () Identity) ()
 -> StencilsAnalysis CheckResult)
-> WriterT [StencilResult] (AnalysisT () () Identity) ()
-> StencilsAnalysis CheckResult
forall a b. (a -> b) -> a -> b
$ do
    -- Attempt to parse comments to specifications
    ProgramFile SA
pf' <- SpecParser SpecParseError Specification
-> (SrcSpan
    -> SpecParseError SpecParseError
    -> WriterT [StencilResult] (AnalysisT () () Identity) ())
-> ProgramFile SA
-> WriterT
     [StencilResult] (AnalysisT () () Identity) (ProgramFile SA)
forall (m :: * -> *) e a ast.
(Monad m, Data a, Linkable a, ASTEmbeddable a ast) =>
SpecParser e ast
-> (SrcSpan -> SpecParseError e -> m ())
-> ProgramFile a
-> m (ProgramFile a)
annotateComments SpecParser SpecParseError Specification
Parser.specParser (\SrcSpan
srcSpan SpecParseError SpecParseError
err -> [StencilResult]
-> WriterT [StencilResult] (AnalysisT () () Identity) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [SrcSpan -> SpecParseError SpecParseError -> StencilResult
parseError SrcSpan
srcSpan SpecParseError SpecParseError
err]) ProgramFile SA
pf
    let -- get map of AST-Block-ID ==> corresponding AST-Block
        bm :: BlockMap (StencilAnnotation A)
bm         = ProgramFile SA -> BlockMap (StencilAnnotation A)
forall a. Data a => ProgramFile (Analysis a) -> BlockMap a
FAD.genBlockMap ProgramFile SA
pf'
        -- get map of program unit  ==> basic block graph
        bbm :: BBlockMap SA
bbm        = ProgramFile SA -> BBlockMap SA
forall a.
Data a =>
ProgramFile (Analysis a) -> BBlockMap (Analysis a)
FAB.genBBlockMap ProgramFile SA
pf'
        -- build the supergraph of global dependency
        sgr :: SuperBBGr SA
sgr        = BBlockMap SA -> SuperBBGr SA
forall a.
Data a =>
BBlockMap (Analysis a) -> SuperBBGr (Analysis a)
FAB.genSuperBBGr BBlockMap SA
bbm
        -- extract the supergraph itself
        gr :: BBGr SA
gr         = SuperBBGr SA -> BBGr SA
forall a. SuperBBGr a -> BBGr a
FAB.superBBGrGraph SuperBBGr SA
sgr
        -- get map of variable name ==> { defining AST-Block-IDs }
        dm :: DefMap
dm         = BlockMap (StencilAnnotation A) -> DefMap
forall a. Data a => BlockMap a -> DefMap
FAD.genDefMap BlockMap (StencilAnnotation A)
bm
        -- perform reaching definitions analysis
        rd :: InOutMap ASTBlockNodeSet
rd         = DefMap -> BBGr SA -> InOutMap ASTBlockNodeSet
forall a.
Data a =>
DefMap -> BBGr (Analysis a) -> InOutMap ASTBlockNodeSet
FAD.reachingDefinitions DefMap
dm BBGr SA
gr
        -- create graph of definition "flows"
        flowsGraph :: FlowsGraph (StencilAnnotation A)
flowsGraph =  BlockMap (StencilAnnotation A)
-> DefMap
-> BBGr SA
-> InOutMap ASTBlockNodeSet
-> FlowsGraph (StencilAnnotation A)
forall a.
Data a =>
BlockMap a
-> DefMap
-> BBGr (Analysis a)
-> InOutMap ASTBlockNodeSet
-> FlowsGraph a
FAD.genFlowsToGraph BlockMap (StencilAnnotation A)
bm DefMap
dm BBGr SA
gr InOutMap ASTBlockNodeSet
rd
        -- identify every loop by its back-edge
        beMap :: BackEdgeMap
beMap      = DomMap -> Gr (BB SA) () -> BackEdgeMap
forall (gr :: * -> * -> *) a b.
Graph gr =>
DomMap -> gr a b -> BackEdgeMap
FAD.genBackEdgeMap (BBGr SA -> DomMap
forall a. BBGr a -> DomMap
FAD.dominators BBGr SA
gr) (Gr (BB SA) () -> BackEdgeMap) -> Gr (BB SA) () -> BackEdgeMap
forall a b. (a -> b) -> a -> b
$ BBGr SA -> Gr (BB SA) ()
forall a. BBGr a -> Gr (BB a) ()
FA.bbgrGr BBGr SA
gr
        ivmap :: InductionVarMapByASTBlock
ivmap      = BackEdgeMap -> BBGr SA -> InductionVarMapByASTBlock
forall a.
Data a =>
BackEdgeMap -> BBGr (Analysis a) -> InductionVarMapByASTBlock
FAD.genInductionVarMapByASTBlock BackEdgeMap
beMap BBGr SA
gr
        -- results :: Checker (F.ProgramFile (F.ProgramFile (FA.Analysis A)))
        results :: ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  (ProgramFile SA)
results    = (ProgramUnit SA
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      (ProgramUnit SA))
-> ProgramFile SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (ProgramFile SA)
forall from to (m :: * -> *).
(Biplate from to, Applicative m) =>
(to -> m to) -> from -> m from
descendBiM ProgramUnit SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (ProgramUnit SA)
perProgramUnitCheck ProgramFile SA
pf'

    let addUnusedRegionsToResult :: ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  ()
addUnusedRegionsToResult = do
          [(SrcSpan, Variable)]
regions'     <- (CheckState -> [(SrcSpan, Variable)])
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     CheckState
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     [(SrcSpan, Variable)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CheckState -> [(SrcSpan, Variable)]
regions ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  CheckState
forall s (m :: * -> *). MonadState s m => m s
get
          [Variable]
usedRegions' <- (CheckState -> [Variable])
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     CheckState
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     [Variable]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CheckState -> [Variable]
usedRegions ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  CheckState
forall s (m :: * -> *). MonadState s m => m s
get
          let unused :: [(SrcSpan, Variable)]
unused = ((SrcSpan, Variable) -> Bool)
-> [(SrcSpan, Variable)] -> [(SrcSpan, Variable)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Variable -> [Variable] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Variable]
usedRegions') (Variable -> Bool)
-> ((SrcSpan, Variable) -> Variable) -> (SrcSpan, Variable) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SrcSpan, Variable) -> Variable
forall a b. (a, b) -> b
snd) [(SrcSpan, Variable)]
regions'
          ((SrcSpan, Variable)
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      ())
-> [(SrcSpan, Variable)]
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (StencilResult
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
addResult (StencilResult
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      ())
-> ((SrcSpan, Variable) -> StencilResult)
-> (SrcSpan, Variable)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SrcSpan -> Variable -> StencilResult)
-> (SrcSpan, Variable) -> StencilResult
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SrcSpan -> Variable -> StencilResult
unusedRegion) [(SrcSpan, Variable)]
unused

    [StencilResult]
output <- AnalysisT () () Identity [StencilResult]
-> WriterT
     [StencilResult] (AnalysisT () () Identity) [StencilResult]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (AnalysisT () () Identity [StencilResult]
 -> WriterT
      [StencilResult] (AnalysisT () () Identity) [StencilResult])
-> AnalysisT () () Identity [StencilResult]
-> WriterT
     [StencilResult] (AnalysisT () () Identity) [StencilResult]
forall a b. (a -> b) -> a -> b
$ CheckState -> [StencilResult]
checkResult (CheckState -> [StencilResult])
-> (((), CheckState) -> CheckState)
-> ((), CheckState)
-> [StencilResult]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((), CheckState) -> CheckState
forall a b. (a, b) -> b
snd (((), CheckState) -> [StencilResult])
-> AnalysisT () () Identity ((), CheckState)
-> AnalysisT () () Identity [StencilResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  ()
-> FlowsGraph (StencilAnnotation A)
-> CheckState
-> AnalysisT () () Identity ((), CheckState)
forall a.
Checker a
-> FlowsGraph (StencilAnnotation A)
-> CheckState
-> StencilsAnalysis (a, CheckState)
runChecker (ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  (ProgramFile SA)
results ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  (ProgramFile SA)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  ()
addUnusedRegionsToResult) FlowsGraph (StencilAnnotation A)
flowsGraph (InductionVarMapByASTBlock -> CheckState
startState InductionVarMapByASTBlock
ivmap)

    [StencilResult]
-> WriterT [StencilResult] (AnalysisT () () Identity) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [StencilResult]
output


data CheckState = CheckState
  { CheckState -> RegionEnv
regionEnv     :: RegionEnv
  , CheckState -> [StencilResult]
checkResult   :: [StencilResult]
  , CheckState -> Maybe ProgramUnitName
prog          :: Maybe F.ProgramUnitName
  , CheckState -> InductionVarMapByASTBlock
ivMap         :: FAD.InductionVarMapByASTBlock
  , CheckState -> [(SrcSpan, Variable)]
regions       :: [(FU.SrcSpan, Variable)]
  , CheckState -> [Variable]
usedRegions   :: [Variable]
  }

addResult :: StencilResult -> Checker ()
addResult :: StencilResult
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
addResult StencilResult
r = (CheckState -> CheckState)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\CheckState
s -> CheckState
s { checkResult :: [StencilResult]
checkResult = StencilResult
r StencilResult -> [StencilResult] -> [StencilResult]
forall a. a -> [a] -> [a]
: CheckState -> [StencilResult]
checkResult CheckState
s })

-- | Remove the given regions variables from the tracked unused regions.
informRegionsUsed :: [Variable] -> Checker ()
informRegionsUsed :: [Variable]
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
informRegionsUsed [Variable]
rs = (CheckState -> CheckState)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify
  (\CheckState
s -> CheckState
s { usedRegions :: [Variable]
usedRegions = CheckState -> [Variable]
usedRegions CheckState
s [Variable] -> [Variable] -> [Variable]
forall a. Eq a => [a] -> [a] -> [a]
`union` [Variable]
rs })

-- | Start tracking a region.
addRegionToTracked :: FU.SrcSpan -> Variable -> Checker ()
addRegionToTracked :: SrcSpan
-> Variable
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
addRegionToTracked SrcSpan
srcSpan Variable
r =
  (CheckState -> CheckState)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\CheckState
s -> CheckState
s { regions :: [(SrcSpan, Variable)]
regions = (SrcSpan
srcSpan, Variable
r) (SrcSpan, Variable)
-> [(SrcSpan, Variable)] -> [(SrcSpan, Variable)]
forall a. a -> [a] -> [a]
: CheckState -> [(SrcSpan, Variable)]
regions CheckState
s })

-- | True if the region name is already tracked.
regionExists :: Variable -> Checker Bool
regionExists :: Variable -> Checker Bool
regionExists Variable
reg = do
  [Variable]
knownNames <- (CheckState -> [Variable])
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     CheckState
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     [Variable]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((SrcSpan, Variable) -> Variable)
-> [(SrcSpan, Variable)] -> [Variable]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SrcSpan, Variable) -> Variable
forall a b. (a, b) -> b
snd ([(SrcSpan, Variable)] -> [Variable])
-> (CheckState -> [(SrcSpan, Variable)])
-> CheckState
-> [Variable]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckState -> [(SrcSpan, Variable)]
regions) ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  CheckState
forall s (m :: * -> *). MonadState s m => m s
get
  Bool -> Checker Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Checker Bool) -> Bool -> Checker Bool
forall a b. (a -> b) -> a -> b
$ Variable
reg Variable -> [Variable] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Variable]
knownNames

startState :: FAD.InductionVarMapByASTBlock -> CheckState
startState :: InductionVarMapByASTBlock -> CheckState
startState InductionVarMapByASTBlock
ivmap =
  CheckState :: RegionEnv
-> [StencilResult]
-> Maybe ProgramUnitName
-> InductionVarMapByASTBlock
-> [(SrcSpan, Variable)]
-> [Variable]
-> CheckState
CheckState { regionEnv :: RegionEnv
regionEnv     = []
             , checkResult :: [StencilResult]
checkResult   = []
             , prog :: Maybe ProgramUnitName
prog          = Maybe ProgramUnitName
forall a. Maybe a
Nothing
             , ivMap :: InductionVarMapByASTBlock
ivMap         = InductionVarMapByASTBlock
ivmap
             , regions :: [(SrcSpan, Variable)]
regions       = []
             , usedRegions :: [Variable]
usedRegions   = []
             }


type CheckerEnv = FAD.FlowsGraph (SA.StencilAnnotation A)
type Checker = ReaderT CheckerEnv (StateT CheckState StencilsAnalysis)


runChecker
  :: Checker a
  -> FAD.FlowsGraph (SA.StencilAnnotation A) -> CheckState
  -> StencilsAnalysis (a, CheckState)
runChecker :: Checker a
-> FlowsGraph (StencilAnnotation A)
-> CheckState
-> StencilsAnalysis (a, CheckState)
runChecker Checker a
c FlowsGraph (StencilAnnotation A)
flows CheckState
state = do
  let env :: FlowsGraph (StencilAnnotation A)
env = FlowsGraph (StencilAnnotation A)
flows
  StateT CheckState (AnalysisT () () Identity) a
-> CheckState -> StencilsAnalysis (a, CheckState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Checker a
-> FlowsGraph (StencilAnnotation A)
-> StateT CheckState (AnalysisT () () Identity) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Checker a
c FlowsGraph (StencilAnnotation A)
env) CheckState
state


getFlowsGraph :: Checker (FAD.FlowsGraph (SA.StencilAnnotation A))
getFlowsGraph :: Checker (FlowsGraph (StencilAnnotation A))
getFlowsGraph = (FlowsGraph (StencilAnnotation A)
 -> FlowsGraph (StencilAnnotation A))
-> Checker (FlowsGraph (StencilAnnotation A))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks FlowsGraph (StencilAnnotation A)
-> FlowsGraph (StencilAnnotation A)
forall a. a -> a
id

-- If the annotation contains an unconverted stencil specification syntax tree
-- then convert it and return an updated annotation containing the AST
parseCommentToAST :: SA -> FU.SrcSpan -> Checker (Either SynToAstError SA)
parseCommentToAST :: SA -> SrcSpan -> Checker (Either SynToAstError SA)
parseCommentToAST SA
ann SrcSpan
span =
  case SA -> Maybe Specification
SA.getParseSpec SA
ann of
    Just Specification
stencilComment -> do
         [Variable]
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
informRegionsUsed (Specification -> [Variable]
reqRegions Specification
stencilComment)
         RegionEnv
renv <- (CheckState -> RegionEnv)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     CheckState
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     RegionEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CheckState -> RegionEnv
regionEnv ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  CheckState
forall s (m :: * -> *). MonadState s m => m s
get
         let ?renv = renv
         case Specification
-> Either SynToAstError (Either (Variable, RegionSum) SpecDecl)
forall s t.
(SynToAst s t, ?renv::RegionEnv) =>
s -> Either SynToAstError t
synToAst Specification
stencilComment of
           Right Either (Variable, RegionSum) SpecDecl
ast -> do
             SA -> SA
pfun <- ((Variable, RegionSum)
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      (SA -> SA))
-> (SpecDecl
    -> ReaderT
         (FlowsGraph (StencilAnnotation A))
         (StateT CheckState (AnalysisT () () Identity))
         (SA -> SA))
-> Either (Variable, RegionSum) SpecDecl
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (SA -> SA)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\reg :: (Variable, RegionSum)
reg@(Variable
var,RegionSum
_) -> do
                        Bool
exists <- Variable -> Checker Bool
regionExists Variable
var
                        if Bool
exists
                          then StencilResult
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
addResult (SrcSpan -> Variable -> StencilResult
regionExistsError SrcSpan
span Variable
var)
                               ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  ()
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (SA -> SA)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (SA -> SA)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (SA -> SA)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (SA -> SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SA -> SA
forall a. a -> a
id
                          else SrcSpan
-> Variable
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
addRegionToTracked SrcSpan
span Variable
var
                               ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  ()
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (SA -> SA)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (SA -> SA)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (SA -> SA)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (SA -> SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Variable, RegionSum) -> SA -> SA
SA.giveRegionSpec (Variable, RegionSum)
reg))
                     ((SA -> SA)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (SA -> SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((SA -> SA)
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      (SA -> SA))
-> (SpecDecl -> SA -> SA)
-> SpecDecl
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (SA -> SA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecDecls -> SA -> SA
SA.giveAstSpec (SpecDecls -> SA -> SA)
-> (SpecDecl -> SpecDecls) -> SpecDecl -> SA -> SA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecDecl -> SpecDecls
forall (f :: * -> *) a. Applicative f => a -> f a
pure) Either (Variable, RegionSum) SpecDecl
ast
             Either SynToAstError SA -> Checker (Either SynToAstError SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either SynToAstError SA -> Checker (Either SynToAstError SA))
-> (SA -> Either SynToAstError SA)
-> SA
-> Checker (Either SynToAstError SA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SA -> Either SynToAstError SA
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SA -> Checker (Either SynToAstError SA))
-> SA -> Checker (Either SynToAstError SA)
forall a b. (a -> b) -> a -> b
$ SA -> SA
pfun SA
ann
           Left SynToAstError
err  -> Either SynToAstError SA -> Checker (Either SynToAstError SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either SynToAstError SA -> Checker (Either SynToAstError SA))
-> (SynToAstError -> Either SynToAstError SA)
-> SynToAstError
-> Checker (Either SynToAstError SA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynToAstError -> Either SynToAstError SA
forall a b. a -> Either a b
Left (SynToAstError -> Checker (Either SynToAstError SA))
-> SynToAstError -> Checker (Either SynToAstError SA)
forall a b. (a -> b) -> a -> b
$ SynToAstError
err

    Maybe Specification
_ -> Either SynToAstError SA -> Checker (Either SynToAstError SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either SynToAstError SA -> Checker (Either SynToAstError SA))
-> (SA -> Either SynToAstError SA)
-> SA
-> Checker (Either SynToAstError SA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SA -> Either SynToAstError SA
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SA -> Checker (Either SynToAstError SA))
-> SA -> Checker (Either SynToAstError SA)
forall a b. (a -> b) -> a -> b
$ SA
ann

-- If the annotation contains an encapsulated region environment, extract it
-- and add it to current region environment in scope
updateRegionEnv :: SA -> Checker ()
updateRegionEnv :: SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
updateRegionEnv SA
ann =
  case SA -> Maybe (Variable, RegionSum)
SA.getRegionSpec SA
ann of
    Just (Variable, RegionSum)
renv -> (CheckState -> CheckState)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\CheckState
s -> CheckState
s { regionEnv :: RegionEnv
regionEnv = (Variable, RegionSum)
renv (Variable, RegionSum) -> RegionEnv -> RegionEnv
forall a. a -> [a] -> [a]
: CheckState -> RegionEnv
regionEnv CheckState
s })
    Maybe (Variable, RegionSum)
_         -> ()
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- Go into the program units first and record the module name when
-- entering into a module
perProgramUnitCheck ::
   F.ProgramUnit SA -> Checker (F.ProgramUnit SA)

perProgramUnitCheck :: ProgramUnit SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (ProgramUnit SA)
perProgramUnitCheck p :: ProgramUnit SA
p@F.PUModule{} = do
    (CheckState -> CheckState)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\CheckState
s -> CheckState
s { prog :: Maybe ProgramUnitName
prog = ProgramUnitName -> Maybe ProgramUnitName
forall a. a -> Maybe a
Just (ProgramUnitName -> Maybe ProgramUnitName)
-> ProgramUnitName -> Maybe ProgramUnitName
forall a b. (a -> b) -> a -> b
$ ProgramUnit SA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
FA.puName ProgramUnit SA
p })
    (Block SA
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      (Block SA))
-> ProgramUnit SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (ProgramUnit SA)
forall from to (m :: * -> *).
(Biplate from to, Applicative m) =>
(to -> m to) -> from -> m from
descendBiM Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
perBlockCheck ProgramUnit SA
p
perProgramUnitCheck ProgramUnit SA
p = (Block SA
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      (Block SA))
-> ProgramUnit SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (ProgramUnit SA)
forall from to (m :: * -> *).
(Biplate from to, Applicative m) =>
(to -> m to) -> from -> m from
descendBiM Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
perBlockCheck ProgramUnit SA
p

perBlockCheck :: F.Block SA -> Checker (F.Block SA)

perBlockCheck :: Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
perBlockCheck b :: Block SA
b@(F.BlComment SA
ann SrcSpan
span Comment SA
_) = do
  Either SynToAstError SA
ast       <- SA -> SrcSpan -> Checker (Either SynToAstError SA)
parseCommentToAST SA
ann SrcSpan
span
  case Either SynToAstError SA
ast of
    Left SynToAstError
err -> StencilResult
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
addResult (SynToAstError -> SrcSpan -> StencilResult
synToAstError SynToAstError
err SrcSpan
span) ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  ()
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Block SA
b
    Right SA
ann' -> do
      SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
updateRegionEnv SA
ann'
      let b' :: Block SA
b' = SA -> Block SA -> Block SA
forall (f :: * -> *) a. Annotated f => a -> f a -> f a
F.setAnnotation SA
ann' Block SA
b
      case (SA -> Maybe SpecDecls
SA.getAstSpec SA
ann', SA -> Maybe (Block SA)
SA.getStencilBlock SA
ann') of
        -- Comment contains a specification and an Associated block
        (Just SpecDecls
specDecls, Just Block SA
block) ->
         case Block SA
block of
          s :: Block SA
s@(F.BlStatement SA
_ SrcSpan
span' Maybe (Expression SA)
_ (F.StExpressionAssign SA
_ SrcSpan
_ Expression SA
lhs Expression SA
_)) -> do
             Block SA
-> SpecDecls
-> SrcSpan
-> Maybe [Index SA]
-> SrcSpan
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
checkStencil Block SA
s SpecDecls
specDecls SrcSpan
span' (Expression SA -> Maybe [Index SA]
forall a. Expression (Analysis a) -> Maybe [Index (Analysis a)]
isArraySubscript Expression SA
lhs) SrcSpan
span
             Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
forall (m :: * -> *) a. Monad m => a -> m a
return Block SA
b'

          -- Stub, maybe collect stencils inside 'do' block
          F.BlDo{} -> Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
forall (m :: * -> *) a. Monad m => a -> m a
return Block SA
b'
          Block SA
_ -> Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
forall (m :: * -> *) a. Monad m => a -> m a
return Block SA
b'
        (Maybe SpecDecls, Maybe (Block SA))
_ -> Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
forall (m :: * -> *) a. Monad m => a -> m a
return Block SA
b'

perBlockCheck b :: Block SA
b@(F.BlDo SA
_ SrcSpan
_ Maybe (Expression SA)
_ Maybe Variable
_ Maybe (Expression SA)
_ Maybe (DoSpecification SA)
_ BB SA
body Maybe (Expression SA)
_) = do
   -- descend into the body of the do-statement
   (Block SA
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      (Block SA))
-> BB SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Block SA
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      (Block SA))
-> Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
forall from to (m :: * -> *).
(Biplate from to, Applicative m) =>
(to -> m to) -> from -> m from
descendBiM Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
perBlockCheck) BB SA
body
   -- Remove any induction variable from the state
   Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
forall (m :: * -> *) a. Monad m => a -> m a
return Block SA
b

perBlockCheck Block SA
b = do
  SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
updateRegionEnv (SA
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      ())
-> (Block SA -> SA)
-> Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block SA -> SA
forall (f :: * -> *) a. Annotated f => f a -> a
F.getAnnotation (Block SA
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      ())
-> Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall a b. (a -> b) -> a -> b
$ Block SA
b
  -- Go inside child blocks
  (Block SA
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      (Block SA))
-> BB SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Block SA
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      (Block SA))
-> Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
forall from to (m :: * -> *).
(Biplate from to, Applicative m) =>
(to -> m to) -> from -> m from
descendBiM Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
perBlockCheck) (BB SA
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      ())
-> BB SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall a b. (a -> b) -> a -> b
$ Block SA -> BB SA
forall on. Uniplate on => on -> [on]
children Block SA
b
  Block SA
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     (Block SA)
forall (m :: * -> *) a. Monad m => a -> m a
return Block SA
b

-- | Validate the stencil and log an appropriate result.
checkStencil :: F.Block SA -> SpecDecls
  -> FU.SrcSpan -> Maybe [F.Index SA] -> FU.SrcSpan -> Checker ()
checkStencil :: Block SA
-> SpecDecls
-> SrcSpan
-> Maybe [Index SA]
-> SrcSpan
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
checkStencil Block SA
block SpecDecls
specDecls SrcSpan
spanInferred Maybe [Index SA]
maybeSubs SrcSpan
span = do
  -- Work out whether this is a stencil (non empty LHS indices) or not
  let ([Index SA]
subs, Bool
isStencil) = case Maybe [Index SA]
maybeSubs of
                             Maybe [Index SA]
Nothing -> ([], Bool
False)
                             Just [Index SA]
subs' -> ([Index SA]
subs', Bool
True)

  -- Get the induction variables relative to the current block
  InductionVarMapByASTBlock
ivmap <- (CheckState -> InductionVarMapByASTBlock)
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     CheckState
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     InductionVarMapByASTBlock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CheckState -> InductionVarMapByASTBlock
ivMap ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  CheckState
forall s (m :: * -> *). MonadState s m => m s
get
  let ivs :: [Variable]
ivs = InductionVarMapByASTBlock -> Block SA -> [Variable]
forall (ast :: * -> *) a.
(Spanned (ast (Analysis a)), Annotated ast) =>
InductionVarMapByASTBlock -> ast (Analysis a) -> [Variable]
extractRelevantIVS InductionVarMapByASTBlock
ivmap Block SA
block

  -- Do analysis; create list of relative indices
  FlowsGraph (StencilAnnotation A)
flowsGraph <- Checker (FlowsGraph (StencilAnnotation A))
getFlowsGraph
  let lhsN :: [Neighbour]
lhsN         = [Neighbour] -> Maybe [Neighbour] -> [Neighbour]
forall a. a -> Maybe a -> a
fromMaybe [] (InductionVarMapByASTBlock -> [Index SA] -> Maybe [Neighbour]
forall a.
Data a =>
InductionVarMapByASTBlock
-> [Index (Analysis a)] -> Maybe [Neighbour]
neighbourIndex InductionVarMapByASTBlock
ivmap [Index SA]
subs)

  [(Variable, (Bool, [[Int]]))]
relOffsets <- StateT
  CheckState (AnalysisT () () Identity) [(Variable, (Bool, [[Int]]))]
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     [(Variable, (Bool, [[Int]]))]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT
   CheckState (AnalysisT () () Identity) [(Variable, (Bool, [[Int]]))]
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      [(Variable, (Bool, [[Int]]))])
-> (AnalysisT () () Identity [(Variable, (Bool, [[Int]]))]
    -> StateT
         CheckState
         (AnalysisT () () Identity)
         [(Variable, (Bool, [[Int]]))])
-> AnalysisT () () Identity [(Variable, (Bool, [[Int]]))]
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     [(Variable, (Bool, [[Int]]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnalysisT () () Identity [(Variable, (Bool, [[Int]]))]
-> StateT
     CheckState (AnalysisT () () Identity) [(Variable, (Bool, [[Int]]))]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (AnalysisT () () Identity [(Variable, (Bool, [[Int]]))]
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      [(Variable, (Bool, [[Int]]))])
-> AnalysisT () () Identity [(Variable, (Bool, [[Int]]))]
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     [(Variable, (Bool, [[Int]]))]
forall a b. (a -> b) -> a -> b
$ ([(Variable, (Bool, [[Int]]))], EvalLog)
-> [(Variable, (Bool, [[Int]]))]
forall a b. (a, b) -> a
fst (([(Variable, (Bool, [[Int]]))], EvalLog)
 -> [(Variable, (Bool, [[Int]]))])
-> AnalysisT
     () () Identity ([(Variable, (Bool, [[Int]]))], EvalLog)
-> AnalysisT () () Identity [(Variable, (Bool, [[Int]]))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StencilInferer (StencilAnnotation A) [(Variable, (Bool, [[Int]]))]
-> [Variable]
-> FlowsGraph (StencilAnnotation A)
-> AnalysisT
     () () Identity ([(Variable, (Bool, [[Int]]))], EvalLog)
forall ann a.
StencilInferer ann a
-> [Variable] -> FlowsGraph ann -> StencilsAnalysis (a, EvalLog)
runStencilInferer ([Neighbour]
-> BB SA
-> StencilInferer
     (StencilAnnotation A) [(Variable, (Bool, [[Int]]))]
forall a.
(Data a, Show a, Eq a) =>
[Neighbour]
-> [Block (Analysis a)]
-> StencilInferer a [(Variable, (Bool, [[Int]]))]
genOffsets [Neighbour]
lhsN [Block SA
block]) [Variable]
ivs FlowsGraph (StencilAnnotation A)
flowsGraph

  let multOffsets :: [(Variable, Multiplicity [[Int]])]
multOffsets = ((Variable, (Bool, [[Int]])) -> (Variable, Multiplicity [[Int]]))
-> [(Variable, (Bool, [[Int]]))]
-> [(Variable, Multiplicity [[Int]])]
forall a b. (a -> b) -> [a] -> [b]
map (\(Variable, (Bool, [[Int]]))
relOffset ->
          case (Variable, (Bool, [[Int]]))
relOffset of
          (Variable
var, (Bool
True, [[Int]]
offsets)) -> (Variable
var, [[Int]] -> Multiplicity [[Int]]
forall a. a -> Multiplicity a
Mult [[Int]]
offsets)
          (Variable
var, (Bool
False, [[Int]]
offsets)) -> (Variable
var, [[Int]] -> Multiplicity [[Int]]
forall a. a -> Multiplicity a
Once [[Int]]
offsets)) [(Variable, (Bool, [[Int]]))]
relOffsets
      expandedDecls :: [(Variable, Specification)]
expandedDecls =
          (SpecDecl -> [(Variable, Specification)])
-> SpecDecls -> [(Variable, Specification)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\([Variable]
vars,Specification
spec) -> (Variable -> (Variable, Specification))
-> [Variable] -> [(Variable, Specification)]
forall a b. (a -> b) -> [a] -> [b]
map ((Variable -> Specification -> (Variable, Specification))
-> Specification -> Variable -> (Variable, Specification)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) Specification
spec) [Variable]
vars) SpecDecls
specDecls

  let userDefinedIsStencils :: [Bool]
userDefinedIsStencils = (SpecDecl -> Bool) -> SpecDecls -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\([Variable]
_, Specification Multiplicity (Approximation Spatial)
_ Bool
b) -> Bool
b) SpecDecls
specDecls
  -- Model and compare the current and specified stencil specs
  if (Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool
isStencil Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
==) [Bool]
userDefinedIsStencils Bool -> Bool -> Bool
&& [(Variable, Multiplicity [[Int]])]
-> [(Variable, Specification)] -> Bool
checkOffsetsAgainstSpec [(Variable, Multiplicity [[Int]])]
multOffsets [(Variable, Specification)]
expandedDecls
    then ((Variable, Specification)
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      ())
-> [(Variable, Specification)]
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\spec :: (Variable, Specification)
spec@(Variable
v,Specification
s) -> do
                   Bool
specExists <- (Variable, Specification) -> Checker Bool
seenBefore (Variable, Specification)
spec
                   if Bool
specExists then StencilResult
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
addResult (SrcSpan -> StencilResult
duplicateSpecification SrcSpan
span)
                     else StencilResult
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
addResult (SrcSpan -> Specification -> Variable -> SrcSpan -> StencilResult
specOkay SrcSpan
span Specification
s Variable
v SrcSpan
spanInferred)) [(Variable, Specification)]
expandedDecls
    else do
    SpecDecls
inferred <- StateT CheckState (AnalysisT () () Identity) SpecDecls
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     SpecDecls
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT CheckState (AnalysisT () () Identity) SpecDecls
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      SpecDecls)
-> (AnalysisT () () Identity SpecDecls
    -> StateT CheckState (AnalysisT () () Identity) SpecDecls)
-> AnalysisT () () Identity SpecDecls
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     SpecDecls
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnalysisT () () Identity SpecDecls
-> StateT CheckState (AnalysisT () () Identity) SpecDecls
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (AnalysisT () () Identity SpecDecls
 -> ReaderT
      (FlowsGraph (StencilAnnotation A))
      (StateT CheckState (AnalysisT () () Identity))
      SpecDecls)
-> AnalysisT () () Identity SpecDecls
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     SpecDecls
forall a b. (a -> b) -> a -> b
$ (SpecDecls, [Int]) -> SpecDecls
forall a b. (a, b) -> a
fst ((SpecDecls, [Int]) -> SpecDecls)
-> (((SpecDecls, [Int]), EvalLog) -> (SpecDecls, [Int]))
-> ((SpecDecls, [Int]), EvalLog)
-> SpecDecls
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SpecDecls, [Int]), EvalLog) -> (SpecDecls, [Int])
forall a b. (a, b) -> a
fst (((SpecDecls, [Int]), EvalLog) -> SpecDecls)
-> AnalysisT () () Identity ((SpecDecls, [Int]), EvalLog)
-> AnalysisT () () Identity SpecDecls
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StencilInferer (StencilAnnotation A) (SpecDecls, [Int])
-> [Variable]
-> FlowsGraph (StencilAnnotation A)
-> AnalysisT () () Identity ((SpecDecls, [Int]), EvalLog)
forall ann a.
StencilInferer ann a
-> [Variable] -> FlowsGraph ann -> StencilsAnalysis (a, EvalLog)
runStencilInferer ([Neighbour]
-> Block SA
-> StencilInferer (StencilAnnotation A) (SpecDecls, [Int])
forall a.
(Data a, Show a, Eq a) =>
[Neighbour]
-> Block (Analysis a) -> StencilInferer a (SpecDecls, [Int])
genSpecifications [Neighbour]
lhsN Block SA
block) [Variable]
ivs FlowsGraph (StencilAnnotation A)
flowsGraph
    StencilResult
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     ()
addResult ((SrcSpan, SpecDecls) -> (SrcSpan, SpecDecls) -> StencilResult
notWellSpecified (SrcSpan
span, SpecDecls
specDecls) (SrcSpan
spanInferred, SpecDecls
inferred))
  where
    seenBefore :: (Variable, Specification) -> Checker Bool
    seenBefore :: (Variable, Specification) -> Checker Bool
seenBefore (Variable
v,Specification
spec) = do
          [StencilResult]
checkLog <- (CheckState -> [StencilResult])
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     CheckState
-> ReaderT
     (FlowsGraph (StencilAnnotation A))
     (StateT CheckState (AnalysisT () () Identity))
     [StencilResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CheckState -> [StencilResult]
checkResult ReaderT
  (FlowsGraph (StencilAnnotation A))
  (StateT CheckState (AnalysisT () () Identity))
  CheckState
forall s (m :: * -> *). MonadState s m => m s
get
          Bool -> Checker Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Checker Bool) -> Bool -> Checker Bool
forall a b. (a -> b) -> a -> b
$ (StencilResult -> Bool) -> [StencilResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\StencilResult
x -> case StencilResult
x of
                              SCOkay{ scSpec :: StencilResult -> Specification
scSpec=Specification
spec'
                                    , scBodySpan :: StencilResult -> SrcSpan
scBodySpan=SrcSpan
bspan
                                    , scVar :: StencilResult -> Variable
scVar = Variable
var}
                                -> Specification
spec' Specification -> Specification -> Bool
forall a. Eq a => a -> a -> Bool
== Specification
spec Bool -> Bool -> Bool
&& SrcSpan
bspan SrcSpan -> SrcSpan -> Bool
forall a. Eq a => a -> a -> Bool
== SrcSpan
spanInferred Bool -> Bool -> Bool
&& Variable
v Variable -> Variable -> Bool
forall a. Eq a => a -> a -> Bool
== Variable
var
                              StencilResult
_ -> Bool
False) [StencilResult]
checkLog

existingStencils :: CheckResult -> [(Specification, FU.SrcSpan, Variable)]
existingStencils :: CheckResult -> [(Specification, SrcSpan, Variable)]
existingStencils = (StencilResult -> Maybe (Specification, SrcSpan, Variable))
-> [StencilResult] -> [(Specification, SrcSpan, Variable)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe StencilResult -> Maybe (Specification, SrcSpan, Variable)
getExistingStencil ([StencilResult] -> [(Specification, SrcSpan, Variable)])
-> (CheckResult -> [StencilResult])
-> CheckResult
-> [(Specification, SrcSpan, Variable)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckResult -> [StencilResult]
getCheckResult
  where getExistingStencil :: StencilResult -> Maybe (Specification, SrcSpan, Variable)
getExistingStencil (SCOkay SrcSpan
_ Specification
spec Variable
var SrcSpan
bodySpan) = (Specification, SrcSpan, Variable)
-> Maybe (Specification, SrcSpan, Variable)
forall a. a -> Maybe a
Just (Specification
spec, SrcSpan
bodySpan, Variable
var)
        getExistingStencil StencilResult
_                            = Maybe (Specification, SrcSpan, Variable)
forall a. Maybe a
Nothing

-- Local variables:
-- mode: haskell
-- haskell-program-name: "cabal repl"
-- End: