{-# LANGUAGE TupleSections #-}
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
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap A -> StencilAnnotation A
forall a. a -> StencilAnnotation a
SA.mkStencilAnnotation
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
. [(String, LogLine)] -> StencilsReport
StencilsReport ([(String, LogLine)] -> StencilsReport)
-> ([LogLine] -> [(String, LogLine)])
-> [LogLine]
-> StencilsReport
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LogLine -> (String, LogLine)) -> [LogLine] -> [(String, LogLine)]
forall a b. (a -> b) -> [a] -> [b]
map (ProgramFile A -> String
forall a. ProgramFile a -> String
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)
synth :: Char
-> [F.ProgramFile A]
-> StencilsAnalysis [F.ProgramFile A]
synth :: Char -> [ProgramFile A] -> StencilsAnalysis [ProgramFile A]
synth Char
marker [ProgramFile A]
pfs = do
([(String, String)], [Maybe (ProgramFile A)])
syntheses <- [((String, String), Maybe (ProgramFile A))]
-> ([(String, String)], [Maybe (ProgramFile A)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((String, String), Maybe (ProgramFile A))]
-> ([(String, String)], [Maybe (ProgramFile A)]))
-> AnalysisT
() () Identity [((String, String), Maybe (ProgramFile A))]
-> AnalysisT
() () Identity ([(String, String)], [Maybe (ProgramFile A)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ProgramFile A
-> AnalysisT
() () Identity ((String, String), Maybe (ProgramFile A)))
-> [ProgramFile A]
-> AnalysisT
() () Identity [((String, String), Maybe (ProgramFile A))]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ProgramFile A
-> AnalysisT
() () Identity ((String, String), Maybe (ProgramFile A))
buildOutput [ProgramFile A]
pfs
[ProgramFile 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
$ String -> Text
forall a. Describe a => a -> Text
describe (String -> Text)
-> (([(String, String)], [Maybe (ProgramFile A)]) -> String)
-> ([(String, String)], [Maybe (ProgramFile A)])
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, String)] -> String
forall (t :: * -> *).
(Foldable t, Functor t) =>
t (String, String) -> String
normaliseMsg ([(String, String)] -> String)
-> (([(String, String)], [Maybe (ProgramFile A)])
-> [(String, String)])
-> ([(String, String)], [Maybe (ProgramFile A)])
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(String, String)], [Maybe (ProgramFile A)]) -> [(String, String)]
forall a b. (a, b) -> a
fst (([(String, String)], [Maybe (ProgramFile A)]) -> Text)
-> ([(String, String)], [Maybe (ProgramFile A)]) -> Text
forall a b. (a -> b) -> a -> b
$ ([(String, String)], [Maybe (ProgramFile A)])
syntheses
[ProgramFile A] -> StencilsAnalysis [ProgramFile 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
$ ([(String, String)], [Maybe (ProgramFile A)])
-> [Maybe (ProgramFile A)]
forall a b. (a, b) -> b
snd ([(String, String)], [Maybe (ProgramFile A)])
syntheses
where
buildOutput :: F.ProgramFile A -> StencilsAnalysis ((String, String), Maybe (F.ProgramFile Annotation))
buildOutput :: ProgramFile A
-> AnalysisT
() () Identity ((String, String), Maybe (ProgramFile A))
buildOutput ProgramFile A
pf = do
let f :: String
f = ProgramFile A -> String
forall a. ProgramFile a -> String
F.pfGetFilename ProgramFile A
pf
Either String (String, ProgramFile A)
result <- ProgramFile A
-> StencilsAnalysis (Either String (String, ProgramFile A))
synthWithCheck ProgramFile A
pf
((String, String), Maybe (ProgramFile A))
-> AnalysisT
() () Identity ((String, String), Maybe (ProgramFile A))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((String, String), Maybe (ProgramFile A))
-> AnalysisT
() () Identity ((String, String), Maybe (ProgramFile A)))
-> ((String, String), Maybe (ProgramFile A))
-> AnalysisT
() () Identity ((String, String), Maybe (ProgramFile A))
forall a b. (a -> b) -> a -> b
$ case Either String (String, ProgramFile A)
result of
Left String
err -> ((String -> String -> String
mkMsg String
f String
err, String
""), Maybe (ProgramFile A)
forall a. Maybe a
Nothing)
Right (String
warn,ProgramFile A
pf') -> ((String
"", String -> String -> String
mkMsg String
f String
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 String (String, 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SA -> A
SA.getBaseAnnotation ProgramFile SA
res
Either String (String, ProgramFile A)
-> StencilsAnalysis (Either String (String, ProgramFile A))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String (String, ProgramFile A)
-> StencilsAnalysis (Either String (String, ProgramFile A)))
-> Either String (String, ProgramFile A)
-> StencilsAnalysis (Either String (String, ProgramFile A))
forall a b. (a -> b) -> a -> b
$ (String, ProgramFile A) -> Either String (String, ProgramFile A)
forall a b. b -> Either a b
Right (String -> (CheckWarning -> String) -> Maybe CheckWarning -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" CheckWarning -> String
forall a. Show a => a -> String
show (CheckResult -> Maybe CheckWarning
checkWarnings CheckResult
checkRes), ProgramFile A
inference)
Just CheckError
err -> Either String (String, ProgramFile A)
-> StencilsAnalysis (Either String (String, ProgramFile A))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String (String, ProgramFile A)
-> StencilsAnalysis (Either String (String, ProgramFile A)))
-> (String -> Either String (String, ProgramFile A))
-> String
-> StencilsAnalysis (Either String (String, ProgramFile A))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String (String, ProgramFile A)
forall a b. a -> Either a b
Left (String
-> StencilsAnalysis (Either String (String, ProgramFile A)))
-> String
-> StencilsAnalysis (Either String (String, ProgramFile A))
forall a b. (a -> b) -> a -> b
$ CheckError -> String
forall a. Show a => a -> String
show CheckError
err
mkMsg :: String -> String -> String
mkMsg String
_ String
"" = String
""
mkMsg String
f String
e = String
"\nEncountered the following errors when checking\
\ stencil specs for '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'\n\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e
normaliseMsg :: t (String, String) -> String
normaliseMsg t (String, String)
outs =
let errors :: t String
errors = ((String, String) -> String) -> t (String, String) -> t String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String, String) -> String
forall a b. (a, b) -> a
fst t (String, String)
outs
fullMsg :: String
fullMsg = ((String, String) -> String) -> t (String, String) -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((String -> String -> String) -> (String, String) -> String
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> String -> String
forall a. [a] -> [a] -> [a]
(++)) t (String, String)
outs
in if (String -> Bool) -> t String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/=String
"") t String
errors then String
fullMsg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
errorTrailer else String
fullMsg
where errorTrailer :: String
errorTrailer = String
"\nPlease resolve these errors, and then\
\ run synthesis again."
check :: F.ProgramFile Annotation -> StencilsAnalysis CheckResult
check :: ProgramFile A -> StencilsAnalysis CheckResult
check = (CheckResult -> CheckResult)
-> StencilsAnalysis CheckResult -> StencilsAnalysis CheckResult
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