{-
   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 DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ScopedTypeVariables #-}

{- | Defines the monad for the units-of-measure modules -}
module Camfort.Specification.Units.Monad
  ( UA, VV, UnitSolver, UnitOpts(..), unitOpts0, UnitState, UnitEnv(..), LiteralsOpt(..)
  , VarUnitMap, GivenVarSet, UnitAliasMap, TemplateMap, CallIdMap
  , NameParamMap, NameParamKey(..)
    -- ** State Helpers
  , freshId
    -- *** Getters
  , getConstraints
  , getNameParamMap
  , getProgramFile
  , getTemplateMap
  , getUnitAliasMap
  , getVarUnitMap
  , usCallIdRemap
  , usConstraints
  , usGivenVarSet
  , usNameParamMap
  , usProgramFile
  , usTemplateMap
  , usUnitAliasMap
  , usVarUnitMap
    -- *** Modifiers
  , modifyCallIdRemap
  , modifyCallIdRemapM
  , modifyConstraints
  , modifyGivenVarSet
  , modifyNameParamMap
  , modifyProgramFile
  , modifyProgramFileM
  , modifyTemplateMap
  , modifyUnitAliasMap
  , modifyVarUnitMap
    -- ** Runners
  , runUnitSolver
  , runUnitAnalysis
  ) where

import           Camfort.Analysis
import           Camfort.Specification.Units.Annotation (UA)
import           Camfort.Specification.Units.Environment (Constraints, VV)
import           Camfort.Specification.Units.MonadTypes
import           Control.Monad.Reader
import           Control.Monad.State.Strict
import qualified Language.Fortran.AST as F

unitOpts0 :: UnitOpts
unitOpts0 :: UnitOpts
unitOpts0 = LiteralsOpt -> UnitOpts
UnitOpts LiteralsOpt
LitMixed

--------------------------------------------------

unitState0 :: F.ProgramFile UA -> UnitState
unitState0 :: ProgramFile UA -> UnitState
unitState0 ProgramFile UA
pf = UnitState { usProgramFile :: ProgramFile UA
usProgramFile  = ProgramFile UA
pf
                          , usVarUnitMap :: VarUnitMap
usVarUnitMap   = VarUnitMap
forall a. Monoid a => a
mempty
                          , usGivenVarSet :: GivenVarSet
usGivenVarSet  = GivenVarSet
forall a. Monoid a => a
mempty
                          , usUnitAliasMap :: UnitAliasMap
usUnitAliasMap = UnitAliasMap
forall a. Monoid a => a
mempty
                          , usTemplateMap :: TemplateMap
usTemplateMap  = TemplateMap
forall a. Monoid a => a
mempty
                          , usNameParamMap :: NameParamMap
usNameParamMap = NameParamMap
forall a. Monoid a => a
mempty
                          , usNextUnique :: Int
usNextUnique   = Int
0
                          , usCallIdRemap :: CallIdMap
usCallIdRemap  = CallIdMap
forall a. Monoid a => a
mempty
                          , usConstraints :: Constraints
usConstraints  = [] }

-- helper functions

-- | Generate a number guaranteed to be unique in the current analysis.
freshId :: UnitSolver Int
freshId :: UnitSolver Int
freshId = do
  UnitState
s <- StateT UnitState UnitAnalysis UnitState
forall s (m :: * -> *). MonadState s m => m s
get
  let i :: Int
i = UnitState -> Int
usNextUnique UnitState
s
  UnitState -> StateT UnitState UnitAnalysis ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (UnitState -> StateT UnitState UnitAnalysis ())
-> UnitState -> StateT UnitState UnitAnalysis ()
forall a b. (a -> b) -> a -> b
$ UnitState
s { usNextUnique :: Int
usNextUnique = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 }
  Int -> UnitSolver Int
forall a. a -> StateT UnitState UnitAnalysis a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i

getConstraints :: UnitSolver Constraints
getConstraints :: UnitSolver Constraints
getConstraints = (UnitState -> Constraints) -> UnitSolver Constraints
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnitState -> Constraints
usConstraints

getNameParamMap :: UnitSolver NameParamMap
getNameParamMap :: UnitSolver NameParamMap
getNameParamMap = (UnitState -> NameParamMap) -> UnitSolver NameParamMap
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnitState -> NameParamMap
usNameParamMap

getProgramFile :: UnitSolver (F.ProgramFile UA)
getProgramFile :: UnitSolver (ProgramFile UA)
getProgramFile = (UnitState -> ProgramFile UA) -> UnitSolver (ProgramFile UA)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnitState -> ProgramFile UA
usProgramFile

getTemplateMap :: UnitSolver TemplateMap
getTemplateMap :: UnitSolver TemplateMap
getTemplateMap = (UnitState -> TemplateMap) -> UnitSolver TemplateMap
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnitState -> TemplateMap
usTemplateMap

getUnitAliasMap :: UnitSolver UnitAliasMap
getUnitAliasMap :: UnitSolver UnitAliasMap
getUnitAliasMap = (UnitState -> UnitAliasMap) -> UnitSolver UnitAliasMap
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnitState -> UnitAliasMap
usUnitAliasMap

getVarUnitMap :: UnitSolver VarUnitMap
getVarUnitMap :: UnitSolver VarUnitMap
getVarUnitMap = (UnitState -> VarUnitMap) -> UnitSolver VarUnitMap
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnitState -> VarUnitMap
usVarUnitMap

modifyVarUnitMap :: (VarUnitMap -> VarUnitMap) -> UnitSolver ()
modifyVarUnitMap :: (VarUnitMap -> VarUnitMap) -> StateT UnitState UnitAnalysis ()
modifyVarUnitMap VarUnitMap -> VarUnitMap
f = (UnitState -> UnitState) -> StateT UnitState UnitAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ UnitState
s -> UnitState
s { usVarUnitMap :: VarUnitMap
usVarUnitMap = VarUnitMap -> VarUnitMap
f (UnitState -> VarUnitMap
usVarUnitMap UnitState
s) })

modifyCallIdRemap :: (CallIdMap -> CallIdMap) -> UnitSolver ()
modifyCallIdRemap :: (CallIdMap -> CallIdMap) -> StateT UnitState UnitAnalysis ()
modifyCallIdRemap CallIdMap -> CallIdMap
f = (UnitState -> UnitState) -> StateT UnitState UnitAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ UnitState
s -> UnitState
s { usCallIdRemap :: CallIdMap
usCallIdRemap = CallIdMap -> CallIdMap
f (UnitState -> CallIdMap
usCallIdRemap UnitState
s) })

modifyConstraints :: (Constraints -> Constraints) -> UnitSolver ()
modifyConstraints :: (Constraints -> Constraints) -> StateT UnitState UnitAnalysis ()
modifyConstraints Constraints -> Constraints
f = (UnitState -> UnitState) -> StateT UnitState UnitAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ UnitState
s -> UnitState
s { usConstraints :: Constraints
usConstraints = Constraints -> Constraints
f (UnitState -> Constraints
usConstraints UnitState
s) })

modifyGivenVarSet :: (GivenVarSet -> GivenVarSet) -> UnitSolver ()
modifyGivenVarSet :: (GivenVarSet -> GivenVarSet) -> StateT UnitState UnitAnalysis ()
modifyGivenVarSet GivenVarSet -> GivenVarSet
f = (UnitState -> UnitState) -> StateT UnitState UnitAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ UnitState
s -> UnitState
s { usGivenVarSet :: GivenVarSet
usGivenVarSet = GivenVarSet -> GivenVarSet
f (UnitState -> GivenVarSet
usGivenVarSet UnitState
s) })

modifyUnitAliasMap :: (UnitAliasMap -> UnitAliasMap) -> UnitSolver ()
modifyUnitAliasMap :: (UnitAliasMap -> UnitAliasMap) -> StateT UnitState UnitAnalysis ()
modifyUnitAliasMap UnitAliasMap -> UnitAliasMap
f = (UnitState -> UnitState) -> StateT UnitState UnitAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ UnitState
s -> UnitState
s { usUnitAliasMap :: UnitAliasMap
usUnitAliasMap = UnitAliasMap -> UnitAliasMap
f (UnitState -> UnitAliasMap
usUnitAliasMap UnitState
s) })

modifyTemplateMap :: (TemplateMap -> TemplateMap) -> UnitSolver ()
modifyTemplateMap :: (TemplateMap -> TemplateMap) -> StateT UnitState UnitAnalysis ()
modifyTemplateMap TemplateMap -> TemplateMap
f = (UnitState -> UnitState) -> StateT UnitState UnitAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ UnitState
s -> UnitState
s { usTemplateMap :: TemplateMap
usTemplateMap = TemplateMap -> TemplateMap
f (UnitState -> TemplateMap
usTemplateMap UnitState
s) })

modifyNameParamMap :: (NameParamMap -> NameParamMap) -> UnitSolver ()
modifyNameParamMap :: (NameParamMap -> NameParamMap) -> StateT UnitState UnitAnalysis ()
modifyNameParamMap NameParamMap -> NameParamMap
f = (UnitState -> UnitState) -> StateT UnitState UnitAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ UnitState
s -> UnitState
s { usNameParamMap :: NameParamMap
usNameParamMap = NameParamMap -> NameParamMap
f (UnitState -> NameParamMap
usNameParamMap UnitState
s) })

modifyProgramFile :: (F.ProgramFile UA -> F.ProgramFile UA) -> UnitSolver ()
modifyProgramFile :: (ProgramFile UA -> ProgramFile UA)
-> StateT UnitState UnitAnalysis ()
modifyProgramFile ProgramFile UA -> ProgramFile UA
f = (UnitState -> UnitState) -> StateT UnitState UnitAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ UnitState
s -> UnitState
s { usProgramFile :: ProgramFile UA
usProgramFile = ProgramFile UA -> ProgramFile UA
f (UnitState -> ProgramFile UA
usProgramFile UnitState
s) })

modifyProgramFileM :: (F.ProgramFile UA -> UnitSolver (F.ProgramFile UA)) -> UnitSolver ()
modifyProgramFileM :: (ProgramFile UA -> UnitSolver (ProgramFile UA))
-> StateT UnitState UnitAnalysis ()
modifyProgramFileM ProgramFile UA -> UnitSolver (ProgramFile UA)
f = do
  ProgramFile UA
pf <- (UnitState -> ProgramFile UA)
-> StateT UnitState UnitAnalysis UnitState
-> UnitSolver (ProgramFile UA)
forall a b.
(a -> b)
-> StateT UnitState UnitAnalysis a
-> StateT UnitState UnitAnalysis b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UnitState -> ProgramFile UA
usProgramFile StateT UnitState UnitAnalysis UnitState
forall s (m :: * -> *). MonadState s m => m s
get
  ProgramFile UA
pf' <- ProgramFile UA -> UnitSolver (ProgramFile UA)
f ProgramFile UA
pf
  (UnitState -> UnitState) -> StateT UnitState UnitAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ UnitState
s -> UnitState
s { usProgramFile :: ProgramFile UA
usProgramFile = ProgramFile UA
pf' })

modifyCallIdRemapM :: (CallIdMap -> UnitSolver (a, CallIdMap)) -> UnitSolver a
modifyCallIdRemapM :: forall a. (CallIdMap -> UnitSolver (a, CallIdMap)) -> UnitSolver a
modifyCallIdRemapM CallIdMap -> UnitSolver (a, CallIdMap)
f = do
  CallIdMap
idMap <- (UnitState -> CallIdMap) -> StateT UnitState UnitAnalysis CallIdMap
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnitState -> CallIdMap
usCallIdRemap
  (a
x, CallIdMap
idMap') <- CallIdMap -> UnitSolver (a, CallIdMap)
f CallIdMap
idMap
  (CallIdMap -> CallIdMap) -> StateT UnitState UnitAnalysis ()
modifyCallIdRemap (CallIdMap -> CallIdMap -> CallIdMap
forall a b. a -> b -> a
const CallIdMap
idMap')
  a -> UnitSolver a
forall a. a -> StateT UnitState UnitAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

--------------------------------------------------

-- | Runs the stateful part of the unit solver.
runUnitSolver :: F.ProgramFile UA -> UnitSolver a -> UnitAnalysis (a, UnitState)
runUnitSolver :: forall a.
ProgramFile UA -> UnitSolver a -> UnitAnalysis (a, UnitState)
runUnitSolver ProgramFile UA
pf UnitSolver a
solver = do
  UnitSolver a -> UnitState -> UnitAnalysis (a, UnitState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT UnitSolver a
solver (ProgramFile UA -> UnitState
unitState0 ProgramFile UA
pf)

runUnitAnalysis :: UnitEnv -> UnitAnalysis a -> AnalysisT () () IO a
runUnitAnalysis :: forall a. UnitEnv -> UnitAnalysis a -> AnalysisT () () IO a
runUnitAnalysis UnitEnv
env = (UnitAnalysis a -> UnitEnv -> AnalysisT () () IO a)
-> UnitEnv -> UnitAnalysis a -> AnalysisT () () IO a
forall a b c. (a -> b -> c) -> b -> a -> c
flip UnitAnalysis a -> UnitEnv -> AnalysisT () () IO a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT UnitEnv
env