{-# LANGUAGE PatternGuards, DoAndIfThenElse, ConstraintKinds, ScopedTypeVariables #-}
module Camfort.Specification.Units.Synthesis
(runSynthesis)
where
import Camfort.Analysis.Annotations
import Camfort.Specification.Units.Analysis (puName, puSrcName)
import Camfort.Specification.Units.Annotation (UA)
import qualified Camfort.Specification.Units.Annotation as UA
import Camfort.Specification.Units.Environment
import Camfort.Specification.Units.Monad
import Control.Monad.State.Strict hiding (gets)
import Data.Generics.Uniplate.Operations
import Data.Maybe
import qualified Data.Set as S
import qualified Language.Fortran.AST as F
import qualified Language.Fortran.Analysis as FA
import qualified Language.Fortran.Util.Position as FU
runSynthesis :: Char -> [(VV, UnitInfo)] -> UnitSolver [(VV, UnitInfo)]
runSynthesis :: Char -> [(VV, UnitInfo)] -> UnitSolver [(VV, UnitInfo)]
runSynthesis Char
marker [(VV, UnitInfo)]
vars = do
(ProgramFile UA -> UnitSolver (ProgramFile UA)) -> UnitSolver ()
modifyProgramFileM ((ProgramFile UA -> UnitSolver (ProgramFile UA)) -> UnitSolver ())
-> (ProgramFile UA -> UnitSolver (ProgramFile UA)) -> UnitSolver ()
forall a b. (a -> b) -> a -> b
$ ([ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> ProgramFile UA -> UnitSolver (ProgramFile UA)
forall from to (m :: * -> *).
(Biplate from to, Applicative m) =>
(to -> m to) -> from -> m from
descendBiM (Char
-> [(VV, UnitInfo)]
-> [ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
synthProgramUnits Char
marker [(VV, UnitInfo)]
vars) (ProgramFile UA -> UnitSolver (ProgramFile UA))
-> (ProgramFile UA -> UnitSolver (ProgramFile UA))
-> ProgramFile UA
-> UnitSolver (ProgramFile UA)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ([Block UA] -> StateT UnitState UnitAnalysis [Block UA])
-> ProgramFile UA -> UnitSolver (ProgramFile UA)
forall from to (m :: * -> *).
(Biplate from to, Applicative m) =>
(to -> m to) -> from -> m from
descendBiM (Char
-> [(VV, UnitInfo)]
-> [Block UA]
-> StateT UnitState UnitAnalysis [Block UA]
synthBlocks Char
marker [(VV, UnitInfo)]
vars)
[(VV, UnitInfo)] -> UnitSolver [(VV, UnitInfo)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(VV, UnitInfo)]
vars
synthBlocks :: Char -> [(VV, UnitInfo)] -> [F.Block UA] -> UnitSolver [F.Block UA]
synthBlocks :: Char
-> [(VV, UnitInfo)]
-> [Block UA]
-> StateT UnitState UnitAnalysis [Block UA]
synthBlocks Char
marker [(VV, UnitInfo)]
vars = ([Block UA] -> [Block UA])
-> StateT UnitState UnitAnalysis [Block UA]
-> StateT UnitState UnitAnalysis [Block UA]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Block UA] -> [Block UA]
forall a. [a] -> [a]
reverse (StateT UnitState UnitAnalysis [Block UA]
-> StateT UnitState UnitAnalysis [Block UA])
-> ([Block UA] -> StateT UnitState UnitAnalysis [Block UA])
-> [Block UA]
-> StateT UnitState UnitAnalysis [Block UA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Block UA]
-> Block UA -> StateT UnitState UnitAnalysis [Block UA])
-> [Block UA]
-> [Block UA]
-> StateT UnitState UnitAnalysis [Block UA]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Char
-> [(VV, UnitInfo)]
-> [Block UA]
-> Block UA
-> StateT UnitState UnitAnalysis [Block UA]
synthBlock Char
marker [(VV, UnitInfo)]
vars) []
synthBlock :: Char -> [(VV, UnitInfo)] -> [F.Block UA] -> F.Block UA -> UnitSolver [F.Block UA]
synthBlock :: Char
-> [(VV, UnitInfo)]
-> [Block UA]
-> Block UA
-> StateT UnitState UnitAnalysis [Block UA]
synthBlock Char
marker [(VV, UnitInfo)]
vars [Block UA]
bs b :: Block UA
b@(F.BlStatement UA
a (FU.SrcSpan Position
lp Position
_) Maybe (Expression UA)
_ (F.StDeclaration UA
_ SrcSpan
_ TypeSpec UA
_ Maybe (AList Attribute UA)
_ AList Declarator UA
decls)) = do
ProgramFile UA
pf <- UnitState -> ProgramFile UA
usProgramFile (UnitState -> ProgramFile UA)
-> StateT UnitState UnitAnalysis UnitState
-> UnitSolver (ProgramFile UA)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` StateT UnitState UnitAnalysis UnitState
forall s (m :: * -> *). MonadState s m => m s
get
GivenVarSet
gvSet <- UnitState -> GivenVarSet
usGivenVarSet (UnitState -> GivenVarSet)
-> StateT UnitState UnitAnalysis UnitState
-> StateT UnitState UnitAnalysis GivenVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` StateT UnitState UnitAnalysis UnitState
forall s (m :: * -> *). MonadState s m => m s
get
[Block UA]
newBs <- ([Maybe (Block UA)] -> [Block UA])
-> StateT UnitState UnitAnalysis [Maybe (Block UA)]
-> StateT UnitState UnitAnalysis [Block UA]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe (Block UA)] -> [Block UA]
forall a. [Maybe a] -> [a]
catMaybes (StateT UnitState UnitAnalysis [Maybe (Block UA)]
-> StateT UnitState UnitAnalysis [Block UA])
-> ((Expression UA
-> StateT UnitState UnitAnalysis (Maybe (Block UA)))
-> StateT UnitState UnitAnalysis [Maybe (Block UA)])
-> (Expression UA
-> StateT UnitState UnitAnalysis (Maybe (Block UA)))
-> StateT UnitState UnitAnalysis [Block UA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expression UA]
-> (Expression UA
-> StateT UnitState UnitAnalysis (Maybe (Block UA)))
-> StateT UnitState UnitAnalysis [Maybe (Block UA)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (AList Declarator UA -> [Expression UA]
forall from to. Biplate from to => from -> [to]
universeBi AList Declarator UA
decls) ((Expression UA
-> StateT UnitState UnitAnalysis (Maybe (Block UA)))
-> StateT UnitState UnitAnalysis [Block UA])
-> (Expression UA
-> StateT UnitState UnitAnalysis (Maybe (Block UA)))
-> StateT UnitState UnitAnalysis [Block UA]
forall a b. (a -> b) -> a -> b
$ \ Expression UA
e -> case Expression UA
e of
(F.ExpValue UA
_ SrcSpan
_ (F.ValVariable Name
_))
| Name
vname Name -> GivenVarSet -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` GivenVarSet
gvSet
, Just UnitInfo
u <- VV -> [(VV, UnitInfo)] -> Maybe UnitInfo
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Name
vname, Name
sname) [(VV, UnitInfo)]
vars -> do
let newA :: UA
newA = UA
a { prevAnnotation :: UnitAnnotation A
FA.prevAnnotation = (UA -> UnitAnnotation A
forall a. Analysis a -> a
FA.prevAnnotation UA
a) {
prevAnnotation :: A
UA.prevAnnotation = (UnitAnnotation A -> A
forall a. UnitAnnotation a -> a
UA.prevAnnotation (UA -> UnitAnnotation A
forall a. Analysis a -> a
FA.prevAnnotation UA
a)) {
refactored :: Maybe Position
refactored = Position -> Maybe Position
forall a. a -> Maybe a
Just Position
lp } } }
newSS :: SrcSpan
newSS = Position -> Position -> SrcSpan
FU.SrcSpan (Position
lp {posColumn :: Int
FU.posColumn = Int
0}) (Position
lp {posColumn :: Int
FU.posColumn = Int
0})
txt :: Name
txt = Char
markerChar -> Name -> Name
forall a. a -> [a] -> [a]
:Name
" " Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ (Name, UnitInfo) -> Name
showUnitDecl (Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.srcName Expression UA
e, UnitInfo
u)
space :: Int
space = Position -> Int
FU.posColumn Position
lp Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
(F.ProgramFile MetaInfo
mi [ProgramUnit UA]
_) = ProgramFile UA
pf
newB :: Block UA
newB = UA -> SrcSpan -> Comment UA -> Block UA
forall a. a -> SrcSpan -> Comment a -> Block a
F.BlComment UA
newA SrcSpan
newSS (Comment UA -> Block UA)
-> (Name -> Comment UA) -> Name -> Block UA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Comment UA
forall a. Name -> Comment a
F.Comment (Name -> Block UA) -> Name -> Block UA
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Int -> Name -> Name
buildCommentText MetaInfo
mi Int
space Name
txt
Maybe (Block UA)
-> StateT UnitState UnitAnalysis (Maybe (Block UA))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Block UA)
-> StateT UnitState UnitAnalysis (Maybe (Block UA)))
-> Maybe (Block UA)
-> StateT UnitState UnitAnalysis (Maybe (Block UA))
forall a b. (a -> b) -> a -> b
$ Block UA -> Maybe (Block UA)
forall a. a -> Maybe a
Just Block UA
newB
where
vname :: Name
vname = Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.varName Expression UA
e
sname :: Name
sname = Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.srcName Expression UA
e
(Expression UA
_ :: F.Expression UA) -> Maybe (Block UA)
-> StateT UnitState UnitAnalysis (Maybe (Block UA))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Block UA)
forall a. Maybe a
Nothing
[Block UA] -> StateT UnitState UnitAnalysis [Block UA]
forall (m :: * -> *) a. Monad m => a -> m a
return (Block UA
bBlock UA -> [Block UA] -> [Block UA]
forall a. a -> [a] -> [a]
:[Block UA] -> [Block UA]
forall a. [a] -> [a]
reverse [Block UA]
newBs [Block UA] -> [Block UA] -> [Block UA]
forall a. [a] -> [a] -> [a]
++ [Block UA]
bs)
synthBlock Char
_ [(VV, UnitInfo)]
_ [Block UA]
bs Block UA
b = [Block UA] -> StateT UnitState UnitAnalysis [Block UA]
forall (m :: * -> *) a. Monad m => a -> m a
return (Block UA
bBlock UA -> [Block UA] -> [Block UA]
forall a. a -> [a] -> [a]
:[Block UA]
bs)
synthProgramUnits :: Char -> [(VV, UnitInfo)] -> [F.ProgramUnit UA] -> UnitSolver [F.ProgramUnit UA]
synthProgramUnits :: Char
-> [(VV, UnitInfo)]
-> [ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
synthProgramUnits Char
marker [(VV, UnitInfo)]
vars [ProgramUnit UA]
pus = do
([ProgramUnit UA] -> [ProgramUnit UA])
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [ProgramUnit UA] -> [ProgramUnit UA]
forall a. [a] -> [a]
reverse (StateT UnitState UnitAnalysis [ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> ([ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> [ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ProgramUnit UA]
-> ProgramUnit UA
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> [ProgramUnit UA]
-> [ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Char
-> [(VV, UnitInfo)]
-> [ProgramUnit UA]
-> ProgramUnit UA
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
synthProgramUnit Char
marker [(VV, UnitInfo)]
vars) [] ([ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> [ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
forall a b. (a -> b) -> a -> b
$ [ProgramUnit UA]
pus
synthProgramUnit :: Char -> [(VV, UnitInfo)] -> [F.ProgramUnit UA] -> F.ProgramUnit UA -> UnitSolver [F.ProgramUnit UA]
synthProgramUnit :: Char
-> [(VV, UnitInfo)]
-> [ProgramUnit UA]
-> ProgramUnit UA
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
synthProgramUnit Char
marker [(VV, UnitInfo)]
vars [ProgramUnit UA]
pus pu :: ProgramUnit UA
pu@(F.PUFunction UA
a (FU.SrcSpan Position
lp Position
_) Maybe (TypeSpec UA)
_ PrefixSuffix UA
_ Name
_ Maybe (AList Expression UA)
_ Maybe (Expression UA)
mret [Block UA]
_ Maybe [ProgramUnit UA]
_) = do
ProgramFile UA
pf <- UnitState -> ProgramFile UA
usProgramFile (UnitState -> ProgramFile UA)
-> StateT UnitState UnitAnalysis UnitState
-> UnitSolver (ProgramFile UA)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` StateT UnitState UnitAnalysis UnitState
forall s (m :: * -> *). MonadState s m => m s
get
GivenVarSet
gvSet <- UnitState -> GivenVarSet
usGivenVarSet (UnitState -> GivenVarSet)
-> StateT UnitState UnitAnalysis UnitState
-> StateT UnitState UnitAnalysis GivenVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` StateT UnitState UnitAnalysis UnitState
forall s (m :: * -> *). MonadState s m => m s
get
let (Name
vname, Name
sname) = case Maybe (Expression UA)
mret of Just Expression UA
e -> (Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.varName Expression UA
e, Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.srcName Expression UA
e)
Maybe (Expression UA)
Nothing -> (ProgramUnit UA -> Name
puName ProgramUnit UA
pu, ProgramUnit UA -> Name
puSrcName ProgramUnit UA
pu)
case VV -> [(VV, UnitInfo)] -> Maybe UnitInfo
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Name
vname, Name
sname) [(VV, UnitInfo)]
vars of
Just UnitInfo
u | Name
vname Name -> GivenVarSet -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` GivenVarSet
gvSet -> do
let newA :: UA
newA = UA
a { prevAnnotation :: UnitAnnotation A
FA.prevAnnotation = (UA -> UnitAnnotation A
forall a. Analysis a -> a
FA.prevAnnotation UA
a) {
prevAnnotation :: A
UA.prevAnnotation = (UnitAnnotation A -> A
forall a. UnitAnnotation a -> a
UA.prevAnnotation (UA -> UnitAnnotation A
forall a. Analysis a -> a
FA.prevAnnotation UA
a)) {
refactored :: Maybe Position
refactored = Position -> Maybe Position
forall a. a -> Maybe a
Just Position
lp } } }
let newSS :: SrcSpan
newSS = Position -> Position -> SrcSpan
FU.SrcSpan (Position
lp {posColumn :: Int
FU.posColumn = Int
0}) (Position
lp {posColumn :: Int
FU.posColumn = Int
0})
txt :: Name
txt = Char
markerChar -> Name -> Name
forall a. a -> [a] -> [a]
:Name
" " Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ (Name, UnitInfo) -> Name
showUnitDecl (Name
sname, UnitInfo
u)
space :: Int
space = Position -> Int
FU.posColumn Position
lp Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
(F.ProgramFile MetaInfo
mi [ProgramUnit UA]
_) = ProgramFile UA
pf
newPU :: ProgramUnit UA
newPU = UA -> SrcSpan -> Comment UA -> ProgramUnit UA
forall a. a -> SrcSpan -> Comment a -> ProgramUnit a
F.PUComment UA
newA SrcSpan
newSS (Comment UA -> ProgramUnit UA)
-> (Name -> Comment UA) -> Name -> ProgramUnit UA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Comment UA
forall a. Name -> Comment a
F.Comment (Name -> ProgramUnit UA) -> Name -> ProgramUnit UA
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Int -> Name -> Name
buildCommentText MetaInfo
mi Int
space Name
txt
(ProgramUnit UA -> [ProgramUnit UA])
-> StateT UnitState UnitAnalysis (ProgramUnit UA)
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProgramUnit UA -> [ProgramUnit UA] -> [ProgramUnit UA]
forall a. a -> [a] -> [a]
:ProgramUnit UA
newPUProgramUnit UA -> [ProgramUnit UA] -> [ProgramUnit UA]
forall a. a -> [a] -> [a]
:[ProgramUnit UA]
pus) (StateT UnitState UnitAnalysis (ProgramUnit UA)
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> StateT UnitState UnitAnalysis (ProgramUnit UA)
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
forall a b. (a -> b) -> a -> b
$ ([ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> ProgramUnit UA -> StateT UnitState UnitAnalysis (ProgramUnit UA)
forall from to (m :: * -> *).
(Biplate from to, Applicative m) =>
(to -> m to) -> from -> m from
descendBiM (Char
-> [(VV, UnitInfo)]
-> [ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
synthProgramUnits Char
marker [(VV, UnitInfo)]
vars) ProgramUnit UA
pu
Maybe UnitInfo
_ -> (ProgramUnit UA -> [ProgramUnit UA])
-> StateT UnitState UnitAnalysis (ProgramUnit UA)
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProgramUnit UA -> [ProgramUnit UA] -> [ProgramUnit UA]
forall a. a -> [a] -> [a]
:[ProgramUnit UA]
pus) (StateT UnitState UnitAnalysis (ProgramUnit UA)
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> StateT UnitState UnitAnalysis (ProgramUnit UA)
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
forall a b. (a -> b) -> a -> b
$ ([ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> ProgramUnit UA -> StateT UnitState UnitAnalysis (ProgramUnit UA)
forall from to (m :: * -> *).
(Biplate from to, Applicative m) =>
(to -> m to) -> from -> m from
descendBiM (Char
-> [(VV, UnitInfo)]
-> [ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
synthProgramUnits Char
marker [(VV, UnitInfo)]
vars) ProgramUnit UA
pu
synthProgramUnit Char
marker [(VV, UnitInfo)]
vars [ProgramUnit UA]
pus ProgramUnit UA
pu = (ProgramUnit UA -> [ProgramUnit UA])
-> StateT UnitState UnitAnalysis (ProgramUnit UA)
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProgramUnit UA -> [ProgramUnit UA] -> [ProgramUnit UA]
forall a. a -> [a] -> [a]
:[ProgramUnit UA]
pus) (StateT UnitState UnitAnalysis (ProgramUnit UA)
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> StateT UnitState UnitAnalysis (ProgramUnit UA)
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
forall a b. (a -> b) -> a -> b
$ ([ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA])
-> ProgramUnit UA -> StateT UnitState UnitAnalysis (ProgramUnit UA)
forall from to (m :: * -> *).
(Biplate from to, Applicative m) =>
(to -> m to) -> from -> m from
descendBiM (Char
-> [(VV, UnitInfo)]
-> [ProgramUnit UA]
-> StateT UnitState UnitAnalysis [ProgramUnit UA]
synthProgramUnits Char
marker [(VV, UnitInfo)]
vars) ProgramUnit UA
pu
showUnitDecl :: ([Char], UnitInfo) -> [Char]
showUnitDecl :: (Name, UnitInfo) -> Name
showUnitDecl (Name
sname, UnitInfo
u) = Name
"unit(" Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ UnitInfo -> Name
forall a. Show a => a -> Name
show UnitInfo
u Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
") :: " Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
sname