{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
module Camfort.Specification.Stencils.InferenceFrontend
(
stencilInference
, stencilSynthesis
, StencilsReport(..)
) where
import Camfort.Analysis
import Camfort.Analysis.Annotations
import Camfort.Analysis.CommentAnnotator
import Camfort.Helpers (descendReverseM, descendBiReverseM)
import Camfort.Specification.Stencils.Analysis (StencilsAnalysis)
import Camfort.Specification.Stencils.Annotation (SA)
import qualified Camfort.Specification.Stencils.Annotation as SA
import Camfort.Specification.Stencils.CheckFrontend
(CheckResult, existingStencils, stencilChecking)
import Camfort.Specification.Stencils.Generate
import qualified Camfort.Specification.Stencils.Parser as Parser
import Camfort.Specification.Stencils.Syntax
import qualified Camfort.Specification.Stencils.Synthesis as Synth
import Control.DeepSeq
import Control.Monad.RWS.Lazy hiding (state)
import Control.Monad.Writer.Lazy
import Data.Foldable
import Data.Generics.Uniplate.Operations
import qualified Data.Map as M
import Data.Maybe
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
import Prelude hiding (span, log)
data InferState = IS {
InferState -> InductionVarMapByASTBlock
_ivMap :: FAD.InductionVarMapByASTBlock
, InferState -> [Int]
visitedNodes :: [Int]}
data InferEnv = IE
{
InferEnv -> [(Specification, SrcSpan, Variable)]
ieExistingSpecs :: [(Specification, FU.SrcSpan, Variable)]
, InferEnv -> FlowsGraph (StencilAnnotation A)
ieFlowsGraph :: FAD.FlowsGraph (SA.StencilAnnotation A)
, InferEnv -> Bool
ieUseEval :: Bool
, InferEnv -> Bool
ieDoSynth :: Bool
, InferEnv -> Char
ieMarker :: Char
, InferEnv -> MetaInfo
ieMetaInfo :: F.MetaInfo
}
type LogLine = (FU.SrcSpan, Either [([Variable], Specification)] (String,Variable))
data StencilsReport = StencilsReport [(String, LogLine)]
instance NFData StencilsReport where
rnf :: StencilsReport -> ()
rnf StencilsReport
_ = ()
instance ExitCodeOfReport StencilsReport where
exitCodeOf :: StencilsReport -> Int
exitCodeOf StencilsReport
_ = Int
0
instance Show StencilsReport where
show :: StencilsReport -> Variable
show (StencilsReport [(Variable, LogLine)]
flogs) = [Variable] -> Variable
unlines ([Variable] -> Variable)
-> ([Variable] -> [Variable]) -> [Variable] -> Variable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Variable -> Bool) -> [Variable] -> [Variable]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Variable -> Bool) -> Variable -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable -> Bool
white) ([Variable] -> Variable) -> [Variable] -> Variable
forall a b. (a -> b) -> a -> b
$ [Variable]
output
where
output :: [Variable]
output = [ LogLine -> Variable
Synth.formatSpecNoComment LogLine
ll | (Variable
_, LogLine
ll) <- [(Variable, LogLine)]
flogs ]
white :: Variable -> Bool
white = (Char -> Bool) -> Variable -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Char
x -> (Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ') Bool -> Bool -> Bool
|| (Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\t'))
instance Describe StencilsReport
type Inferer = RWST InferEnv [LogLine] InferState StencilsAnalysis
getExistingSpecs :: Inferer [(Specification, FU.SrcSpan, Variable)]
getExistingSpecs :: Inferer [(Specification, SrcSpan, Variable)]
getExistingSpecs = (InferEnv -> [(Specification, SrcSpan, Variable)])
-> Inferer [(Specification, SrcSpan, Variable)]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> [(Specification, SrcSpan, Variable)]
ieExistingSpecs
getFlowsGraph :: Inferer (FAD.FlowsGraph (SA.StencilAnnotation A))
getFlowsGraph :: Inferer (FlowsGraph (StencilAnnotation A))
getFlowsGraph = (InferEnv -> FlowsGraph (StencilAnnotation A))
-> Inferer (FlowsGraph (StencilAnnotation A))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> FlowsGraph (StencilAnnotation A)
ieFlowsGraph
getMetaInfo :: Inferer F.MetaInfo
getMetaInfo :: Inferer MetaInfo
getMetaInfo = (InferEnv -> MetaInfo) -> Inferer MetaInfo
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> MetaInfo
ieMetaInfo
getMarker :: Inferer Char
getMarker :: Inferer Char
getMarker = (InferEnv -> Char) -> Inferer Char
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> Char
ieMarker
getUseEval :: Inferer Bool
getUseEval :: Inferer Bool
getUseEval = (InferEnv -> Bool) -> Inferer Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> Bool
ieUseEval
getDoSynth :: Inferer Bool
getDoSynth :: Inferer Bool
getDoSynth = (InferEnv -> Bool) -> Inferer Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> Bool
ieDoSynth
runInferer :: CheckResult
-> Bool
-> Bool
-> Char
-> F.MetaInfo
-> FAD.InductionVarMapByASTBlock
-> FAD.FlowsGraph (SA.StencilAnnotation A)
-> Inferer a
-> StencilsAnalysis (a, [LogLine])
runInferer :: CheckResult
-> Bool
-> Bool
-> Char
-> MetaInfo
-> InductionVarMapByASTBlock
-> FlowsGraph (StencilAnnotation A)
-> Inferer a
-> StencilsAnalysis (a, [LogLine])
runInferer CheckResult
cr Bool
useEval Bool
doSynth Char
marker MetaInfo
mi InductionVarMapByASTBlock
ivmap FlowsGraph (StencilAnnotation A)
flTo Inferer a
inferer = do
Inferer a
-> InferEnv -> InferState -> StencilsAnalysis (a, [LogLine])
forall (m :: * -> *) r w s a.
Monad m =>
RWST r w s m a -> r -> s -> m (a, w)
evalRWST Inferer a
inferer InferEnv
env (InductionVarMapByASTBlock -> [Int] -> InferState
IS InductionVarMapByASTBlock
ivmap [])
where env :: InferEnv
env = IE :: [(Specification, SrcSpan, Variable)]
-> FlowsGraph (StencilAnnotation A)
-> Bool
-> Bool
-> Char
-> MetaInfo
-> InferEnv
IE
{ ieExistingSpecs :: [(Specification, SrcSpan, Variable)]
ieExistingSpecs = CheckResult -> [(Specification, SrcSpan, Variable)]
existingStencils CheckResult
cr
, ieFlowsGraph :: FlowsGraph (StencilAnnotation A)
ieFlowsGraph = FlowsGraph (StencilAnnotation A)
flTo
, ieUseEval :: Bool
ieUseEval = Bool
useEval
, ieDoSynth :: Bool
ieDoSynth = Bool
doSynth
, ieMarker :: Char
ieMarker = Char
marker
, ieMetaInfo :: MetaInfo
ieMetaInfo = MetaInfo
mi
}
whenEval :: Inferer () -> Inferer ()
whenEval :: Inferer () -> Inferer ()
whenEval Inferer ()
i = Inferer Bool
getUseEval Inferer Bool -> (Bool -> Inferer ()) -> Inferer ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Bool -> Inferer () -> Inferer ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
`when` Inferer ()
i)
ifSynth :: Inferer a -> Inferer a -> Inferer a
ifSynth :: Inferer a -> Inferer a -> Inferer a
ifSynth Inferer a
t Inferer a
e = Inferer Bool
getDoSynth Inferer Bool -> (Bool -> Inferer a) -> Inferer a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Bool
doSynth -> if Bool
doSynth then Inferer a
t else Inferer a
e)
stencilInference :: Bool
-> Char
-> F.ProgramFile SA
-> StencilsAnalysis [LogLine]
stencilInference :: Bool -> Char -> ProgramFile SA -> StencilsAnalysis [LogLine]
stencilInference Bool
useEval Char
marker ProgramFile SA
pf = WriterT [LogLine] StencilsAnalysis (ProgramFile SA)
-> StencilsAnalysis [LogLine]
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT [LogLine] StencilsAnalysis (ProgramFile SA)
-> StencilsAnalysis [LogLine])
-> WriterT [LogLine] StencilsAnalysis (ProgramFile SA)
-> StencilsAnalysis [LogLine]
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool
-> Char
-> ProgramFile SA
-> WriterT [LogLine] StencilsAnalysis (ProgramFile SA)
stencilSynthesis' Bool
useEval Bool
False Char
marker ProgramFile SA
pf
stencilSynthesis :: Char
-> F.ProgramFile SA
-> StencilsAnalysis (F.ProgramFile SA, [LogLine])
stencilSynthesis :: Char
-> ProgramFile SA -> StencilsAnalysis (ProgramFile SA, [LogLine])
stencilSynthesis Char
marker ProgramFile SA
pf = do
let (ProgramFile SA
pf', Variable
_log0 :: String) = Writer Variable (ProgramFile SA) -> (ProgramFile SA, Variable)
forall w a. Writer w a -> (a, w)
runWriter (SpecParser SpecParseError Specification
-> (SrcSpan
-> SpecParseError SpecParseError -> WriterT Variable Identity ())
-> ProgramFile SA
-> Writer Variable (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 ((SpecParseError SpecParseError -> WriterT Variable Identity ())
-> SrcSpan
-> SpecParseError SpecParseError
-> WriterT Variable Identity ()
forall a b. a -> b -> a
const ((SpecParseError SpecParseError -> WriterT Variable Identity ())
-> SrcSpan
-> SpecParseError SpecParseError
-> WriterT Variable Identity ())
-> (()
-> SpecParseError SpecParseError -> WriterT Variable Identity ())
-> ()
-> SrcSpan
-> SpecParseError SpecParseError
-> WriterT Variable Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT Variable Identity ()
-> SpecParseError SpecParseError -> WriterT Variable Identity ()
forall a b. a -> b -> a
const (WriterT Variable Identity ()
-> SpecParseError SpecParseError -> WriterT Variable Identity ())
-> (() -> WriterT Variable Identity ())
-> ()
-> SpecParseError SpecParseError
-> WriterT Variable Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> WriterT Variable Identity ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure (()
-> SrcSpan
-> SpecParseError SpecParseError
-> WriterT Variable Identity ())
-> ()
-> SrcSpan
-> SpecParseError SpecParseError
-> WriterT Variable Identity ()
forall a b. (a -> b) -> a -> b
$ ()) ProgramFile SA
pf)
ProgramFile SA -> Text -> AnalysisT () () Identity ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logDebug' ProgramFile SA
pf (Text -> AnalysisT () () Identity ())
-> Text -> AnalysisT () () Identity ()
forall a b. (a -> b) -> a -> b
$ Variable -> Text
forall a. Describe a => a -> Text
describe Variable
_log0
WriterT [LogLine] StencilsAnalysis (ProgramFile SA)
-> StencilsAnalysis (ProgramFile SA, [LogLine])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT [LogLine] StencilsAnalysis (ProgramFile SA)
-> StencilsAnalysis (ProgramFile SA, [LogLine]))
-> WriterT [LogLine] StencilsAnalysis (ProgramFile SA)
-> StencilsAnalysis (ProgramFile SA, [LogLine])
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool
-> Char
-> ProgramFile SA
-> WriterT [LogLine] StencilsAnalysis (ProgramFile SA)
stencilSynthesis' Bool
False Bool
True Char
marker ProgramFile SA
pf'
stencilSynthesis' :: Bool
-> Bool
-> Char
-> F.ProgramFile SA
-> WriterT [LogLine] StencilsAnalysis
(F.ProgramFile SA)
stencilSynthesis' :: Bool
-> Bool
-> Char
-> ProgramFile SA
-> WriterT [LogLine] StencilsAnalysis (ProgramFile SA)
stencilSynthesis' Bool
useEval Bool
doSynth Char
marker pf :: ProgramFile SA
pf@(F.ProgramFile MetaInfo
mi [ProgramUnit SA]
pus) = do
CheckResult
checkRes <- AnalysisT () () Identity CheckResult
-> WriterT [LogLine] StencilsAnalysis CheckResult
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (AnalysisT () () Identity CheckResult
-> WriterT [LogLine] StencilsAnalysis CheckResult)
-> AnalysisT () () Identity CheckResult
-> WriterT [LogLine] StencilsAnalysis CheckResult
forall a b. (a -> b) -> a -> b
$ ProgramFile SA -> AnalysisT () () Identity CheckResult
stencilChecking ProgramFile SA
pf
let
bm :: BlockMap (StencilAnnotation A)
bm = ProgramFile SA -> BlockMap (StencilAnnotation A)
forall a. Data a => ProgramFile (Analysis a) -> BlockMap a
FAD.genBlockMap ProgramFile SA
pf
bbm :: BBlockMap SA
bbm = ProgramFile SA -> BBlockMap SA
forall a.
Data a =>
ProgramFile (Analysis a) -> BBlockMap (Analysis a)
FAB.genBBlockMap ProgramFile SA
pf
dm :: DefMap
dm = BlockMap (StencilAnnotation A) -> DefMap
forall a. Data a => BlockMap a -> DefMap
FAD.genDefMap BlockMap (StencilAnnotation A)
bm
perPU :: F.ProgramUnit SA
-> WriterT [LogLine] StencilsAnalysis (F.ProgramUnit SA)
perPU :: ProgramUnit SA
-> WriterT [LogLine] StencilsAnalysis (ProgramUnit SA)
perPU ProgramUnit SA
pu | Just BBGr SA
_ <- SA -> Maybe (BBGr SA)
forall a. Analysis a -> Maybe (BBGr (Analysis a))
FA.bBlocks (SA -> Maybe (BBGr SA)) -> SA -> Maybe (BBGr SA)
forall a b. (a -> b) -> a -> b
$ ProgramUnit SA -> SA
forall (f :: * -> *) a. Annotated f => f a -> a
F.getAnnotation ProgramUnit SA
pu = do
let
blocksM :: RWST InferEnv [LogLine] InferState StencilsAnalysis [Block SA]
blocksM = (Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA))
-> [Block SA]
-> RWST InferEnv [LogLine] InferState StencilsAnalysis [Block SA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
perBlockInfer (ProgramUnit SA -> [Block SA]
forall a. ProgramUnit a -> [Block a]
F.programUnitBody ProgramUnit SA
pu)
pum :: RWST
InferEnv [LogLine] InferState StencilsAnalysis (ProgramUnit SA)
pum = ProgramUnit SA -> [Block SA] -> ProgramUnit SA
forall a. ProgramUnit a -> [Block a] -> ProgramUnit a
F.updateProgramUnitBody ProgramUnit SA
pu ([Block SA] -> ProgramUnit SA)
-> RWST InferEnv [LogLine] InferState StencilsAnalysis [Block SA]
-> RWST
InferEnv [LogLine] InferState StencilsAnalysis (ProgramUnit SA)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RWST InferEnv [LogLine] InferState StencilsAnalysis [Block SA]
blocksM
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
Just BBGr SA
gr = ProgramUnitName -> BBlockMap SA -> Maybe (BBGr SA)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (ProgramUnit SA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
FA.puName ProgramUnit SA
pu) BBlockMap SA
bbm
flTo :: FlowsGraph (StencilAnnotation A)
flTo = 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
beMap :: BackEdgeMap
beMap = DomMap -> Gr [Block 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 [Block SA] () -> BackEdgeMap)
-> Gr [Block SA] () -> BackEdgeMap
forall a b. (a -> b) -> a -> b
$ BBGr SA -> Gr [Block 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
(ProgramUnit SA
pu', [LogLine]
log) <- AnalysisT () () Identity (ProgramUnit SA, [LogLine])
-> WriterT [LogLine] StencilsAnalysis (ProgramUnit SA, [LogLine])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (AnalysisT () () Identity (ProgramUnit SA, [LogLine])
-> WriterT [LogLine] StencilsAnalysis (ProgramUnit SA, [LogLine]))
-> AnalysisT () () Identity (ProgramUnit SA, [LogLine])
-> WriterT [LogLine] StencilsAnalysis (ProgramUnit SA, [LogLine])
forall a b. (a -> b) -> a -> b
$ CheckResult
-> Bool
-> Bool
-> Char
-> MetaInfo
-> InductionVarMapByASTBlock
-> FlowsGraph (StencilAnnotation A)
-> RWST
InferEnv [LogLine] InferState StencilsAnalysis (ProgramUnit SA)
-> AnalysisT () () Identity (ProgramUnit SA, [LogLine])
forall a.
CheckResult
-> Bool
-> Bool
-> Char
-> MetaInfo
-> InductionVarMapByASTBlock
-> FlowsGraph (StencilAnnotation A)
-> Inferer a
-> StencilsAnalysis (a, [LogLine])
runInferer CheckResult
checkRes Bool
useEval Bool
doSynth Char
marker MetaInfo
mi InductionVarMapByASTBlock
ivmap FlowsGraph (StencilAnnotation A)
flTo RWST
InferEnv [LogLine] InferState StencilsAnalysis (ProgramUnit SA)
pum
[LogLine] -> WriterT [LogLine] StencilsAnalysis ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [LogLine]
log
ProgramUnit SA
-> WriterT [LogLine] StencilsAnalysis (ProgramUnit SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProgramUnit SA
pu'
perPU ProgramUnit SA
pu = ProgramUnit SA
-> WriterT [LogLine] StencilsAnalysis (ProgramUnit SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProgramUnit SA
pu
[ProgramUnit SA]
pus' <- (ProgramUnit SA
-> WriterT [LogLine] StencilsAnalysis (ProgramUnit SA))
-> [ProgramUnit SA]
-> WriterT [LogLine] StencilsAnalysis [ProgramUnit SA]
forall (m :: * -> *) from to.
(Monad m, Applicative m, Biplate from to) =>
(to -> m to) -> from -> m from
transformBiM ProgramUnit SA
-> WriterT [LogLine] StencilsAnalysis (ProgramUnit SA)
perPU [ProgramUnit SA]
pus
ProgramFile SA
-> WriterT [LogLine] StencilsAnalysis (ProgramFile SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MetaInfo -> [ProgramUnit SA] -> ProgramFile SA
forall a. MetaInfo -> [ProgramUnit a] -> ProgramFile a
F.ProgramFile MetaInfo
mi [ProgramUnit SA]
pus')
genSpecsAndReport ::
FU.SrcSpan -> [Neighbour]
-> F.Block SA
-> Inferer [([Variable], Specification)]
genSpecsAndReport :: SrcSpan
-> [Neighbour] -> Block SA -> Inferer [([Variable], Specification)]
genSpecsAndReport SrcSpan
span [Neighbour]
lhsIxs Block SA
block = do
(IS InductionVarMapByASTBlock
ivmap [Int]
_) <- RWST InferEnv [LogLine] InferState StencilsAnalysis InferState
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
FlowsGraph (StencilAnnotation A)
flowsGraph <- Inferer (FlowsGraph (StencilAnnotation A))
getFlowsGraph
(([([Variable], Specification)]
specs, [Int]
visited), EvalLog
evalInfos) <- AnalysisT
() () Identity (([([Variable], Specification)], [Int]), EvalLog)
-> RWST
InferEnv
[LogLine]
InferState
StencilsAnalysis
(([([Variable], Specification)], [Int]), EvalLog)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (AnalysisT
() () Identity (([([Variable], Specification)], [Int]), EvalLog)
-> RWST
InferEnv
[LogLine]
InferState
StencilsAnalysis
(([([Variable], Specification)], [Int]), EvalLog))
-> AnalysisT
() () Identity (([([Variable], Specification)], [Int]), EvalLog)
-> RWST
InferEnv
[LogLine]
InferState
StencilsAnalysis
(([([Variable], Specification)], [Int]), EvalLog)
forall a b. (a -> b) -> a -> b
$ StencilInferer
(StencilAnnotation A) ([([Variable], Specification)], [Int])
-> [Variable]
-> FlowsGraph (StencilAnnotation A)
-> AnalysisT
() () Identity (([([Variable], Specification)], [Int]), EvalLog)
forall ann a.
StencilInferer ann a
-> [Variable] -> FlowsGraph ann -> StencilsAnalysis (a, EvalLog)
runStencilInferer ([Neighbour]
-> Block SA
-> StencilInferer
(StencilAnnotation A) ([([Variable], Specification)], [Int])
forall a.
(Data a, Show a, Eq a) =>
[Neighbour]
-> Block (Analysis a)
-> StencilInferer a ([([Variable], Specification)], [Int])
genSpecifications [Neighbour]
lhsIxs Block SA
block) [Variable]
ivs FlowsGraph (StencilAnnotation A)
flowsGraph
(InferState -> InferState) -> Inferer ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\InferState
state -> InferState
state { visitedNodes :: [Int]
visitedNodes = InferState -> [Int]
visitedNodes InferState
state [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
visited })
[LogLine] -> Inferer ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [ (SrcSpan
span, [([Variable], Specification)]
-> Either [([Variable], Specification)] (Variable, Variable)
forall a b. a -> Either a b
Left [([Variable], Specification)]
specs) ]
Inferer () -> Inferer ()
whenEval (Inferer () -> Inferer ()) -> Inferer () -> Inferer ()
forall a b. (a -> b) -> a -> b
$ do
[LogLine] -> Inferer ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [ (SrcSpan
span, (Variable, Variable)
-> Either [([Variable], Specification)] (Variable, Variable)
forall a b. b -> Either a b
Right (Variable
"EVALMODE: assign to relative array subscript\
\ (tag: tickAssign)",Variable
"")) ]
EvalLog -> ((Variable, Variable) -> Inferer ()) -> Inferer ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ EvalLog
evalInfos (((Variable, Variable) -> Inferer ()) -> Inferer ())
-> ((Variable, Variable) -> Inferer ()) -> Inferer ()
forall a b. (a -> b) -> a -> b
$ \(Variable, Variable)
evalInfo ->
[LogLine] -> Inferer ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [ (SrcSpan
span, (Variable, Variable)
-> Either [([Variable], Specification)] (Variable, Variable)
forall a b. b -> Either a b
Right (Variable, Variable)
evalInfo) ]
[([Variable], Specification)]
-> (([Variable], Specification) -> Inferer ()) -> Inferer ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [([Variable], Specification)]
specs ((([Variable], Specification) -> Inferer ()) -> Inferer ())
-> (([Variable], Specification) -> Inferer ()) -> Inferer ()
forall a b. (a -> b) -> a -> b
$ \([Variable], Specification)
spec ->
Bool -> Inferer () -> Inferer ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (([Variable], Specification) -> Variable
forall a. Show a => a -> Variable
show ([Variable], Specification)
spec Variable -> Variable -> Bool
forall a. Eq a => a -> a -> Bool
== Variable
"") (Inferer () -> Inferer ()) -> Inferer () -> Inferer ()
forall a b. (a -> b) -> a -> b
$
[LogLine] -> Inferer ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [ (SrcSpan
span, (Variable, Variable)
-> Either [([Variable], Specification)] (Variable, Variable)
forall a b. b -> Either a b
Right (Variable
"EVALMODE: Cannot make spec\
\ (tag: emptySpec)",Variable
"")) ]
[([Variable], Specification)]
-> Inferer [([Variable], Specification)]
forall (m :: * -> *) a. Monad m => a -> m a
return [([Variable], Specification)]
specs
perBlockInfer :: F.Block SA
-> Inferer (F.Block SA)
perBlockInfer :: Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
perBlockInfer = Bool
-> Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
perBlockInfer' Bool
False
perBlockInfer' :: Bool -> F.Block SA -> Inferer (F.Block SA)
perBlockInfer' :: Bool
-> Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
perBlockInfer' Bool
_ b :: Block SA
b@F.BlComment{} = Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Block SA
b
perBlockInfer' Bool
inDo b :: Block SA
b@(F.BlStatement SA
ann span :: SrcSpan
span@(FU.SrcSpan Position
lp Position
_) Maybe (Expression SA)
_ Statement SA
stmnt) = do
(IS InductionVarMapByASTBlock
ivmap [Int]
visitedStmts) <- RWST InferEnv [LogLine] InferState StencilsAnalysis InferState
forall s (m :: * -> *). MonadState s m => m s
get
let label :: Int
label = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (-Int
1) (SA -> Maybe Int
forall a. Analysis a -> Maybe Int
FA.insLabel SA
ann)
if Int
label Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
visitedStmts
then
Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall (m :: * -> *) a. Monad m => a -> m a
return Block SA
b
else do
[(Specification, SrcSpan, Variable)]
userSpecs <- Inferer [(Specification, SrcSpan, Variable)]
getExistingSpecs
let lhses :: [Expression SA]
lhses = [Expression SA
lhs | (F.StExpressionAssign SA
_ SrcSpan
_ Expression SA
lhs Expression SA
_)
<- Statement SA -> [Statement SA]
forall on. Uniplate on => on -> [on]
universe Statement SA
stmnt :: [F.Statement SA]]
[[([Variable], Specification)]]
specs <- (Expression SA -> Inferer [([Variable], Specification)])
-> [Expression SA]
-> RWST
InferEnv
[LogLine]
InferState
StencilsAnalysis
[[([Variable], Specification)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InductionVarMapByASTBlock
-> Expression SA -> Inferer [([Variable], Specification)]
genSpecsFor InductionVarMapByASTBlock
ivmap) [Expression SA]
lhses
Char
marker <- Inferer Char
getMarker
MetaInfo
mi <- Inferer MetaInfo
getMetaInfo
RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall a. Inferer a -> Inferer a -> Inferer a
ifSynth
(if Bool -> Bool
not ([[([Variable], Specification)]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[([Variable], Specification)]]
specs) Bool -> Bool -> Bool
&& [[([Variable], Specification)]]
specs [[([Variable], Specification)]]
-> [[([Variable], Specification)]] -> Bool
forall a. Eq a => a -> a -> Bool
/= [[]]
then
let specComment :: Variable
specComment = MetaInfo -> Int -> Char -> LogLine -> Variable
Synth.formatSpec MetaInfo
mi Int
tabs Char
marker (SrcSpan
span, [([Variable], Specification)]
-> Either [([Variable], Specification)] (Variable, Variable)
forall a b. a -> Either a b
Left [([Variable], Specification)]
specs')
specs' :: [([Variable], Specification)]
specs' = ([([Variable], Specification)] -> [([Variable], Specification)])
-> [[([Variable], Specification)]] -> [([Variable], Specification)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((([Variable], Specification) -> Maybe ([Variable], Specification))
-> [([Variable], Specification)] -> [([Variable], Specification)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([Variable], Specification) -> Maybe ([Variable], Specification)
noSpecAlready) [[([Variable], Specification)]]
specs
noSpecAlready :: ([Variable], Specification) -> Maybe ([Variable], Specification)
noSpecAlready ([Variable]
vars, Specification
spec) =
if [Variable] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Variable]
vars'
then Maybe ([Variable], Specification)
forall a. Maybe a
Nothing
else ([Variable], Specification) -> Maybe ([Variable], Specification)
forall a. a -> Maybe a
Just ([Variable]
vars', Specification
spec)
where vars' :: [Variable]
vars' = (Variable -> Bool) -> [Variable] -> [Variable]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Variable
v -> (Specification
spec, SrcSpan
span, Variable
v) (Specification, SrcSpan, Variable)
-> [(Specification, SrcSpan, Variable)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [(Specification, SrcSpan, Variable)]
userSpecs) [Variable]
vars
tabs :: Int
tabs = Position -> Int
FU.posColumn Position
lp Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
(FU.SrcSpan Position
loc Position
_) = SrcSpan
span
span' :: SrcSpan
span' = Position -> Position -> SrcSpan
FU.SrcSpan (Position
lp {posColumn :: Int
FU.posColumn = Int
1}) (Position
lp {posColumn :: Int
FU.posColumn = Int
1})
ann' :: SA
ann' = (A -> A) -> SA -> SA
SA.modifyBaseAnnotation (\A
ba -> A
ba { refactored :: Maybe Position
refactored = Position -> Maybe Position
forall a. a -> Maybe a
Just Position
loc }) SA
ann
in Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SA -> SrcSpan -> Comment SA -> Block SA
forall a. a -> SrcSpan -> Comment a -> Block a
F.BlComment SA
ann' SrcSpan
span' (Variable -> Comment SA
forall a. Variable -> Comment a
F.Comment Variable
specComment))
else Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Block SA
b)
(Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Block SA
b)
where
genSpecsFor :: FAD.InductionVarMapByASTBlock -> F.Expression SA -> Inferer [([Variable], Specification)]
genSpecsFor :: InductionVarMapByASTBlock
-> Expression SA -> Inferer [([Variable], Specification)]
genSpecsFor InductionVarMapByASTBlock
_ (F.ExpValue SA
_ SrcSpan
_ (F.ValVariable Variable
_)) | Bool
inDo = SrcSpan
-> [Neighbour] -> Block SA -> Inferer [([Variable], Specification)]
genSpecsAndReport SrcSpan
span [] Block SA
b
genSpecsFor InductionVarMapByASTBlock
ivmap Expression SA
lhs =
case Expression SA -> Maybe [Index SA]
forall a. Expression (Analysis a) -> Maybe [Index (Analysis a)]
isArraySubscript Expression SA
lhs of
Just [Index SA]
subs ->
case InductionVarMapByASTBlock -> [Index SA] -> Maybe [Neighbour]
forall a.
Data a =>
InductionVarMapByASTBlock
-> [Index (Analysis a)] -> Maybe [Neighbour]
neighbourIndex InductionVarMapByASTBlock
ivmap [Index SA]
subs of
Just [Neighbour]
lhs' -> SrcSpan
-> [Neighbour] -> Block SA -> Inferer [([Variable], Specification)]
genSpecsAndReport SrcSpan
span [Neighbour]
lhs' Block SA
b
Maybe [Neighbour]
Nothing -> do
Inferer () -> Inferer ()
whenEval (Inferer () -> Inferer ()) -> Inferer () -> Inferer ()
forall a b. (a -> b) -> a -> b
$
[LogLine] -> Inferer ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [(SrcSpan
span , (Variable, Variable)
-> Either [([Variable], Specification)] (Variable, Variable)
forall a b. b -> Either a b
Right (Variable
"EVALMODE: LHS is an array\
\ subscript we can't handle \
\(tag: LHSnotHandled)",Variable
""))]
[([Variable], Specification)]
-> Inferer [([Variable], Specification)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Maybe [Index SA]
_ -> [([Variable], Specification)]
-> Inferer [([Variable], Specification)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
perBlockInfer' Bool
_ (F.BlDo SA
ann SrcSpan
span Maybe (Expression SA)
lab Maybe Variable
cname Maybe (Expression SA)
lab' Maybe (DoSpecification SA)
mDoSpec [Block SA]
body Maybe (Expression SA)
tlab) = do
[Block SA]
body' <- (Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA))
-> [Block SA]
-> RWST InferEnv [LogLine] InferState StencilsAnalysis [Block SA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA))
-> Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall from to (m :: * -> *).
(Data from, Data to, Monad m, Biplate from to) =>
(to -> m to) -> from -> m from
descendBiReverseM (Bool
-> Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
perBlockInfer' Bool
True)) ([Block SA] -> [Block SA]
forall a. [a] -> [a]
reverse [Block SA]
body)
Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall (m :: * -> *) a. Monad m => a -> m a
return (Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA))
-> Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall a b. (a -> b) -> a -> b
$ SA
-> SrcSpan
-> Maybe (Expression SA)
-> Maybe Variable
-> Maybe (Expression SA)
-> Maybe (DoSpecification SA)
-> [Block SA]
-> Maybe (Expression SA)
-> Block SA
forall a.
a
-> SrcSpan
-> Maybe (Expression a)
-> Maybe Variable
-> Maybe (Expression a)
-> Maybe (DoSpecification a)
-> [Block a]
-> Maybe (Expression a)
-> Block a
F.BlDo SA
ann SrcSpan
span Maybe (Expression SA)
lab Maybe Variable
cname Maybe (Expression SA)
lab' Maybe (DoSpecification SA)
mDoSpec ([Block SA] -> [Block SA]
forall a. [a] -> [a]
reverse [Block SA]
body') Maybe (Expression SA)
tlab
perBlockInfer' Bool
inDo Block SA
b =
(Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA))
-> Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall on (m :: * -> *).
(Data on, Monad m, Uniplate on) =>
(on -> m on) -> on -> m on
descendReverseM ((Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA))
-> Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
forall from to (m :: * -> *).
(Data from, Data to, Monad m, Biplate from to) =>
(to -> m to) -> from -> m from
descendBiReverseM (Bool
-> Block SA
-> RWST InferEnv [LogLine] InferState StencilsAnalysis (Block SA)
perBlockInfer' Bool
inDo)) Block SA
b