{-# LANGUAGE TupleSections #-}
{-
   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.
-}

module Camfort.Specification.Stencils
 (infer, check, synth) where

import           Camfort.Analysis
import           Camfort.Analysis.Annotations
import           Camfort.Specification.Stencils.Analysis (StencilsAnalysis)
import qualified Camfort.Specification.Stencils.Annotation as SA
import           Camfort.Specification.Stencils.CheckFrontend
import           Camfort.Specification.Stencils.InferenceFrontend
import           Control.DeepSeq
import           Data.Maybe (catMaybes)
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.Analysis.Renaming as FAR

-- | Helper for retrieving analysed blocks.
getBlocks :: F.ProgramFile A -> F.ProgramFile SA.SA
getBlocks :: ProgramFile A -> ProgramFile SA
getBlocks = ProgramFile SA -> ProgramFile SA
forall a.
Data a =>
ProgramFile (Analysis a) -> ProgramFile (Analysis a)
FAD.analyseConstExps (ProgramFile SA -> ProgramFile SA)
-> (ProgramFile A -> ProgramFile SA)
-> ProgramFile A
-> ProgramFile SA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramFile SA -> ProgramFile SA
forall a.
Data a =>
ProgramFile (Analysis a) -> ProgramFile (Analysis a)
FAB.analyseBBlocks (ProgramFile SA -> ProgramFile SA)
-> (ProgramFile A -> ProgramFile SA)
-> ProgramFile A
-> ProgramFile SA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramFile SA -> ProgramFile SA
forall a.
Data a =>
ProgramFile (Analysis a) -> ProgramFile (Analysis a)
FAR.analyseRenames (ProgramFile SA -> ProgramFile SA)
-> (ProgramFile A -> ProgramFile SA)
-> ProgramFile A
-> ProgramFile SA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramFile (StencilAnnotation A) -> ProgramFile SA
forall (b :: * -> *) a. Functor b => b a -> b (Analysis a)
FA.initAnalysis (ProgramFile (StencilAnnotation A) -> ProgramFile SA)
-> (ProgramFile A -> ProgramFile (StencilAnnotation A))
-> ProgramFile A
-> ProgramFile SA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (A -> StencilAnnotation A)
-> ProgramFile A -> ProgramFile (StencilAnnotation A)
forall a b. (a -> b) -> ProgramFile a -> ProgramFile b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap A -> StencilAnnotation A
forall a. a -> StencilAnnotation a
SA.mkStencilAnnotation

--------------------------------------------------
--         Stencil specification inference      --
--------------------------------------------------
-- Top-level of specification inference
infer :: Bool
      -> Char
      -> F.ProgramFile Annotation
      -> StencilsAnalysis StencilsReport
infer :: Bool -> Char -> ProgramFile A -> StencilsAnalysis StencilsReport
infer Bool
useEval Char
marker ProgramFile A
pf =
  (StencilsReport -> StencilsReport
forall a. NFData a => a -> a
force (StencilsReport -> StencilsReport)
-> ([LogLine] -> StencilsReport) -> [LogLine] -> StencilsReport
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [([Char], LogLine)] -> StencilsReport
StencilsReport ([([Char], LogLine)] -> StencilsReport)
-> ([LogLine] -> [([Char], LogLine)])
-> [LogLine]
-> StencilsReport
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LogLine -> ([Char], LogLine)) -> [LogLine] -> [([Char], LogLine)]
forall a b. (a -> b) -> [a] -> [b]
map (ProgramFile A -> [Char]
forall a. ProgramFile a -> [Char]
F.pfGetFilename ProgramFile A
pf,)) ([LogLine] -> StencilsReport)
-> AnalysisT () () Identity [LogLine]
-> StencilsAnalysis StencilsReport
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> Char -> ProgramFile SA -> AnalysisT () () Identity [LogLine]
stencilInference Bool
useEval Char
marker (ProgramFile A -> ProgramFile SA
getBlocks ProgramFile A
pf)

--------------------------------------------------
--         Stencil specification synthesis      --
--------------------------------------------------

-- Top-level of specification synthesis
synth :: Char
      -> [F.ProgramFile A]
      -> StencilsAnalysis [F.ProgramFile A]
synth :: Char -> [ProgramFile A] -> StencilsAnalysis [ProgramFile A]
synth Char
marker [ProgramFile A]
pfs = do
  ([([Char], [Char])], [Maybe (ProgramFile A)])
syntheses <- [(([Char], [Char]), Maybe (ProgramFile A))]
-> ([([Char], [Char])], [Maybe (ProgramFile A)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(([Char], [Char]), Maybe (ProgramFile A))]
 -> ([([Char], [Char])], [Maybe (ProgramFile A)]))
-> AnalysisT
     () () Identity [(([Char], [Char]), Maybe (ProgramFile A))]
-> AnalysisT
     () () Identity ([([Char], [Char])], [Maybe (ProgramFile A)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ProgramFile A
 -> AnalysisT
      () () Identity (([Char], [Char]), Maybe (ProgramFile A)))
-> [ProgramFile A]
-> AnalysisT
     () () Identity [(([Char], [Char]), Maybe (ProgramFile A))]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ProgramFile A
-> AnalysisT
     () () Identity (([Char], [Char]), Maybe (ProgramFile A))
buildOutput [ProgramFile A]
pfs
  [ProgramFile A] -> Text -> AnalysisT () () Identity ()
forall a. Spanned a => a -> Text -> AnalysisT () () Identity ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' [ProgramFile A]
pfs (Text -> AnalysisT () () Identity ())
-> Text -> AnalysisT () () Identity ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
forall a. Describe a => a -> Text
describe ([Char] -> Text)
-> (([([Char], [Char])], [Maybe (ProgramFile A)]) -> [Char])
-> ([([Char], [Char])], [Maybe (ProgramFile A)])
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [([Char], [Char])] -> [Char]
forall {t :: * -> *}.
(Foldable t, Functor t) =>
t ([Char], [Char]) -> [Char]
normaliseMsg ([([Char], [Char])] -> [Char])
-> (([([Char], [Char])], [Maybe (ProgramFile A)])
    -> [([Char], [Char])])
-> ([([Char], [Char])], [Maybe (ProgramFile A)])
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([([Char], [Char])], [Maybe (ProgramFile A)]) -> [([Char], [Char])]
forall a b. (a, b) -> a
fst (([([Char], [Char])], [Maybe (ProgramFile A)]) -> Text)
-> ([([Char], [Char])], [Maybe (ProgramFile A)]) -> Text
forall a b. (a -> b) -> a -> b
$ ([([Char], [Char])], [Maybe (ProgramFile A)])
syntheses
  [ProgramFile A] -> StencilsAnalysis [ProgramFile A]
forall a. a -> AnalysisT () () Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ProgramFile A] -> StencilsAnalysis [ProgramFile A])
-> ([Maybe (ProgramFile A)] -> [ProgramFile A])
-> [Maybe (ProgramFile A)]
-> StencilsAnalysis [ProgramFile A]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (ProgramFile A)] -> [ProgramFile A]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (ProgramFile A)] -> StencilsAnalysis [ProgramFile A])
-> [Maybe (ProgramFile A)] -> StencilsAnalysis [ProgramFile A]
forall a b. (a -> b) -> a -> b
$ ([([Char], [Char])], [Maybe (ProgramFile A)])
-> [Maybe (ProgramFile A)]
forall a b. (a, b) -> b
snd ([([Char], [Char])], [Maybe (ProgramFile A)])
syntheses
  where
    buildOutput :: F.ProgramFile A -> StencilsAnalysis ((String, String), Maybe (F.ProgramFile Annotation))
    buildOutput :: ProgramFile A
-> AnalysisT
     () () Identity (([Char], [Char]), Maybe (ProgramFile A))
buildOutput ProgramFile A
pf = do
      let f :: [Char]
f = ProgramFile A -> [Char]
forall a. ProgramFile a -> [Char]
F.pfGetFilename ProgramFile A
pf
      Either [Char] ([Char], ProgramFile A)
result <- ProgramFile A
-> StencilsAnalysis (Either [Char] ([Char], ProgramFile A))
synthWithCheck ProgramFile A
pf
      (([Char], [Char]), Maybe (ProgramFile A))
-> AnalysisT
     () () Identity (([Char], [Char]), Maybe (ProgramFile A))
forall a. a -> AnalysisT () () Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((([Char], [Char]), Maybe (ProgramFile A))
 -> AnalysisT
      () () Identity (([Char], [Char]), Maybe (ProgramFile A)))
-> (([Char], [Char]), Maybe (ProgramFile A))
-> AnalysisT
     () () Identity (([Char], [Char]), Maybe (ProgramFile A))
forall a b. (a -> b) -> a -> b
$ case Either [Char] ([Char], ProgramFile A)
result of
               Left [Char]
err         -> (([Char] -> [Char] -> [Char]
mkMsg [Char]
f [Char]
err, [Char]
""), Maybe (ProgramFile A)
forall a. Maybe a
Nothing)
               Right ([Char]
warn,ProgramFile A
pf') -> (([Char]
"", [Char] -> [Char] -> [Char]
mkMsg [Char]
f [Char]
warn), ProgramFile A -> Maybe (ProgramFile A)
forall a. a -> Maybe a
Just ProgramFile A
pf')
    synthWithCheck :: F.ProgramFile A -> StencilsAnalysis (Either String (String, F.ProgramFile Annotation))
    synthWithCheck :: ProgramFile A
-> StencilsAnalysis (Either [Char] ([Char], ProgramFile A))
synthWithCheck ProgramFile A
pf = do
      let blocks :: ProgramFile SA
blocks = ProgramFile A -> ProgramFile SA
getBlocks ProgramFile A
pf
      CheckResult
checkRes <- ProgramFile SA -> StencilsAnalysis CheckResult
stencilChecking ProgramFile SA
blocks
      case CheckResult -> Maybe CheckError
checkFailure CheckResult
checkRes of
        Maybe CheckError
Nothing  -> do
          ProgramFile SA
res <- (ProgramFile SA, [LogLine]) -> ProgramFile SA
forall a b. (a, b) -> a
fst ((ProgramFile SA, [LogLine]) -> ProgramFile SA)
-> AnalysisT () () Identity (ProgramFile SA, [LogLine])
-> AnalysisT () () Identity (ProgramFile SA)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Char
-> ProgramFile SA
-> AnalysisT () () Identity (ProgramFile SA, [LogLine])
stencilSynthesis Char
marker ProgramFile SA
blocks
          let inference :: ProgramFile A
inference = (SA -> A) -> ProgramFile SA -> ProgramFile A
forall a b. (a -> b) -> ProgramFile a -> ProgramFile b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SA -> A
SA.getBaseAnnotation ProgramFile SA
res
          Either [Char] ([Char], ProgramFile A)
-> StencilsAnalysis (Either [Char] ([Char], ProgramFile A))
forall a. a -> AnalysisT () () Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [Char] ([Char], ProgramFile A)
 -> StencilsAnalysis (Either [Char] ([Char], ProgramFile A)))
-> Either [Char] ([Char], ProgramFile A)
-> StencilsAnalysis (Either [Char] ([Char], ProgramFile A))
forall a b. (a -> b) -> a -> b
$ ([Char], ProgramFile A) -> Either [Char] ([Char], ProgramFile A)
forall a b. b -> Either a b
Right ([Char] -> (CheckWarning -> [Char]) -> Maybe CheckWarning -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"" CheckWarning -> [Char]
forall a. Show a => a -> [Char]
show (CheckResult -> Maybe CheckWarning
checkWarnings CheckResult
checkRes), ProgramFile A
inference)
        Just CheckError
err -> Either [Char] ([Char], ProgramFile A)
-> StencilsAnalysis (Either [Char] ([Char], ProgramFile A))
forall a. a -> AnalysisT () () Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [Char] ([Char], ProgramFile A)
 -> StencilsAnalysis (Either [Char] ([Char], ProgramFile A)))
-> ([Char] -> Either [Char] ([Char], ProgramFile A))
-> [Char]
-> StencilsAnalysis (Either [Char] ([Char], ProgramFile A))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Either [Char] ([Char], ProgramFile A)
forall a b. a -> Either a b
Left ([Char]
 -> StencilsAnalysis (Either [Char] ([Char], ProgramFile A)))
-> [Char]
-> StencilsAnalysis (Either [Char] ([Char], ProgramFile A))
forall a b. (a -> b) -> a -> b
$ CheckError -> [Char]
forall a. Show a => a -> [Char]
show CheckError
err

    mkMsg :: [Char] -> [Char] -> [Char]
mkMsg [Char]
_ [Char]
"" = [Char]
""
    mkMsg [Char]
f [Char]
e  = [Char]
"\nEncountered the following errors when checking\
                 \ stencil specs for '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'\n\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
e

    normaliseMsg :: t ([Char], [Char]) -> [Char]
normaliseMsg t ([Char], [Char])
outs =
      let errors :: t [Char]
errors = (([Char], [Char]) -> [Char]) -> t ([Char], [Char]) -> t [Char]
forall a b. (a -> b) -> t a -> t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], [Char]) -> [Char]
forall a b. (a, b) -> a
fst t ([Char], [Char])
outs
          fullMsg :: [Char]
fullMsg = (([Char], [Char]) -> [Char]) -> t ([Char], [Char]) -> [Char]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (([Char] -> [Char] -> [Char]) -> ([Char], [Char]) -> [Char]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
(++)) t ([Char], [Char])
outs
      in if ([Char] -> Bool) -> t [Char] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/=[Char]
"") t [Char]
errors then [Char]
fullMsg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
errorTrailer else [Char]
fullMsg
      where errorTrailer :: [Char]
errorTrailer = [Char]
"\nPlease resolve these errors, and then\
                           \ run synthesis again."


--------------------------------------------------
--         Stencil specification checking       --
--------------------------------------------------

check :: F.ProgramFile Annotation -> StencilsAnalysis CheckResult
check :: ProgramFile A -> StencilsAnalysis CheckResult
check = (CheckResult -> CheckResult)
-> StencilsAnalysis CheckResult -> StencilsAnalysis CheckResult
forall a b.
(a -> b)
-> AnalysisT () () Identity a -> AnalysisT () () Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CheckResult -> CheckResult
forall a. NFData a => a -> a
force (StencilsAnalysis CheckResult -> StencilsAnalysis CheckResult)
-> (ProgramFile A -> StencilsAnalysis CheckResult)
-> ProgramFile A
-> StencilsAnalysis CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramFile SA -> StencilsAnalysis CheckResult
stencilChecking (ProgramFile SA -> StencilsAnalysis CheckResult)
-> (ProgramFile A -> ProgramFile SA)
-> ProgramFile A
-> StencilsAnalysis CheckResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramFile A -> ProgramFile SA
getBlocks

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