{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
module Camfort.Specification.Units.Analysis.Infer
( InferenceReport(..)
, InferenceResult(..)
, getInferred
, inferUnits
) where
import Camfort.Analysis (ExitCodeOfReport(..), Describe(..))
import Camfort.Specification.Units.Analysis
(UnitAnalysis, puName, puSrcName, runInference)
import Camfort.Specification.Units.Analysis.Consistent
(ConsistencyError, ConsistencyReport(..), checkUnits)
import Camfort.Specification.Units.Environment
import Camfort.Specification.Units.InferenceBackend (inferVariables, chooseImplicitNames)
import Camfort.Specification.Units.Monad
import Control.DeepSeq
import Data.Data (Data)
import Data.Generics.Uniplate.Operations (universeBi)
import Data.List (sort)
import qualified Data.Map.Strict as M
import Data.Maybe (mapMaybe, maybeToList)
import GHC.Generics (Generic)
import qualified Language.Fortran.AST as F
import qualified Language.Fortran.Analysis as FA
import qualified Language.Fortran.Util.Position as FU
data ExpInfo = ExpInfo
{ ExpInfo -> SrcSpan
eiSrcSpan :: FU.SrcSpan
, ExpInfo -> Name
eiVName :: F.Name
, ExpInfo -> Name
eiSName :: F.Name
} deriving (Int -> ExpInfo -> ShowS
[ExpInfo] -> ShowS
ExpInfo -> Name
(Int -> ExpInfo -> ShowS)
-> (ExpInfo -> Name) -> ([ExpInfo] -> ShowS) -> Show ExpInfo
forall a.
(Int -> a -> ShowS) -> (a -> Name) -> ([a] -> ShowS) -> Show a
showList :: [ExpInfo] -> ShowS
$cshowList :: [ExpInfo] -> ShowS
show :: ExpInfo -> Name
$cshow :: ExpInfo -> Name
showsPrec :: Int -> ExpInfo -> ShowS
$cshowsPrec :: Int -> ExpInfo -> ShowS
Show, ExpInfo -> ExpInfo -> Bool
(ExpInfo -> ExpInfo -> Bool)
-> (ExpInfo -> ExpInfo -> Bool) -> Eq ExpInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExpInfo -> ExpInfo -> Bool
$c/= :: ExpInfo -> ExpInfo -> Bool
== :: ExpInfo -> ExpInfo -> Bool
$c== :: ExpInfo -> ExpInfo -> Bool
Eq, Eq ExpInfo
Eq ExpInfo
-> (ExpInfo -> ExpInfo -> Ordering)
-> (ExpInfo -> ExpInfo -> Bool)
-> (ExpInfo -> ExpInfo -> Bool)
-> (ExpInfo -> ExpInfo -> Bool)
-> (ExpInfo -> ExpInfo -> Bool)
-> (ExpInfo -> ExpInfo -> ExpInfo)
-> (ExpInfo -> ExpInfo -> ExpInfo)
-> Ord ExpInfo
ExpInfo -> ExpInfo -> Bool
ExpInfo -> ExpInfo -> Ordering
ExpInfo -> ExpInfo -> ExpInfo
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ExpInfo -> ExpInfo -> ExpInfo
$cmin :: ExpInfo -> ExpInfo -> ExpInfo
max :: ExpInfo -> ExpInfo -> ExpInfo
$cmax :: ExpInfo -> ExpInfo -> ExpInfo
>= :: ExpInfo -> ExpInfo -> Bool
$c>= :: ExpInfo -> ExpInfo -> Bool
> :: ExpInfo -> ExpInfo -> Bool
$c> :: ExpInfo -> ExpInfo -> Bool
<= :: ExpInfo -> ExpInfo -> Bool
$c<= :: ExpInfo -> ExpInfo -> Bool
< :: ExpInfo -> ExpInfo -> Bool
$c< :: ExpInfo -> ExpInfo -> Bool
compare :: ExpInfo -> ExpInfo -> Ordering
$ccompare :: ExpInfo -> ExpInfo -> Ordering
$cp1Ord :: Eq ExpInfo
Ord, Typeable, Typeable ExpInfo
DataType
Constr
Typeable ExpInfo
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExpInfo -> c ExpInfo)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExpInfo)
-> (ExpInfo -> Constr)
-> (ExpInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ExpInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpInfo))
-> ((forall b. Data b => b -> b) -> ExpInfo -> ExpInfo)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExpInfo -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExpInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> ExpInfo -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> ExpInfo -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo)
-> Data ExpInfo
ExpInfo -> DataType
ExpInfo -> Constr
(forall b. Data b => b -> b) -> ExpInfo -> ExpInfo
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExpInfo -> c ExpInfo
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExpInfo
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ExpInfo -> u
forall u. (forall d. Data d => d -> u) -> ExpInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExpInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExpInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExpInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExpInfo -> c ExpInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ExpInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpInfo)
$cExpInfo :: Constr
$tExpInfo :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo
gmapMp :: (forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo
gmapM :: (forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ExpInfo -> m ExpInfo
gmapQi :: Int -> (forall d. Data d => d -> u) -> ExpInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ExpInfo -> u
gmapQ :: (forall d. Data d => d -> u) -> ExpInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ExpInfo -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExpInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExpInfo -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExpInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExpInfo -> r
gmapT :: (forall b. Data b => b -> b) -> ExpInfo -> ExpInfo
$cgmapT :: (forall b. Data b => b -> b) -> ExpInfo -> ExpInfo
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpInfo)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ExpInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ExpInfo)
dataTypeOf :: ExpInfo -> DataType
$cdataTypeOf :: ExpInfo -> DataType
toConstr :: ExpInfo -> Constr
$ctoConstr :: ExpInfo -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExpInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExpInfo
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExpInfo -> c ExpInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExpInfo -> c ExpInfo
$cp1Data :: Typeable ExpInfo
Data, (forall x. ExpInfo -> Rep ExpInfo x)
-> (forall x. Rep ExpInfo x -> ExpInfo) -> Generic ExpInfo
forall x. Rep ExpInfo x -> ExpInfo
forall x. ExpInfo -> Rep ExpInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ExpInfo x -> ExpInfo
$cfrom :: forall x. ExpInfo -> Rep ExpInfo x
Generic)
data InferenceReport
= InferenceReport (F.ProgramFile UA) [(VV, UnitInfo)]
instance NFData InferenceReport where
rnf :: InferenceReport -> ()
rnf InferenceReport
_ = ()
data InferenceResult
= Inferred InferenceReport
| InfInconsistent ConsistencyError
instance NFData InferenceResult where
rnf :: InferenceResult -> ()
rnf InferenceResult
_ = ()
instance ExitCodeOfReport InferenceResult where
exitCodeOf :: InferenceResult -> Int
exitCodeOf (Inferred InferenceReport
_) = Int
0
exitCodeOf (InfInconsistent ConsistencyError
_) = Int
1
instance Show InferenceReport where
show :: InferenceReport -> Name
show (InferenceReport ProgramFile UA
pf [(VV, UnitInfo)]
vars) =
[Name] -> Name
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Name
"\n", Name
fname, Name
":\n", [Name] -> Name
unlines [ (ExpInfo, UnitInfo) -> Name
forall a. Show a => (ExpInfo, a) -> Name
expReport (ExpInfo, UnitInfo)
ei | (ExpInfo, UnitInfo)
ei <- [(ExpInfo, UnitInfo)]
expInfo ]]
where
expReport :: (ExpInfo, a) -> Name
expReport (ExpInfo
ei, a
u) = Name
" " Name -> ShowS
forall a. [a] -> [a] -> [a]
++ SrcSpan -> Name
showSrcSpan (ExpInfo -> SrcSpan
eiSrcSpan ExpInfo
ei) Name -> ShowS
forall a. [a] -> [a] -> [a]
++ Name
" unit " Name -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> Name
forall a. Show a => a -> Name
show a
u Name -> ShowS
forall a. [a] -> [a] -> [a]
++ Name
" :: " Name -> ShowS
forall a. [a] -> [a] -> [a]
++ ExpInfo -> Name
eiSName ExpInfo
ei
showSrcSpan :: FU.SrcSpan -> String
showSrcSpan :: SrcSpan -> Name
showSrcSpan (FU.SrcSpan Position
l Position
_) = Position -> Name
forall a. Show a => a -> Name
show Position
l
fname :: Name
fname = ProgramFile UA -> Name
forall a. ProgramFile a -> Name
F.pfGetFilename ProgramFile UA
pf
expInfo :: [(ExpInfo, UnitInfo)]
expInfo = [ (ExpInfo
ei, UnitInfo
u) | ExpInfo
ei <- [ExpInfo]
declVariableNames
, UnitInfo
u <- Maybe UnitInfo -> [UnitInfo]
forall a. Maybe a -> [a]
maybeToList ((ExpInfo -> Name
eiVName ExpInfo
ei, ExpInfo -> Name
eiSName ExpInfo
ei) VV -> [(VV, UnitInfo)] -> Maybe UnitInfo
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(VV, UnitInfo)]
vars) ]
declVariableNames :: [ExpInfo]
declVariableNames :: [ExpInfo]
declVariableNames = [ExpInfo] -> [ExpInfo]
forall a. Ord a => [a] -> [a]
sort ([ExpInfo] -> [ExpInfo])
-> (Map Name ExpInfo -> [ExpInfo]) -> Map Name ExpInfo -> [ExpInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name ExpInfo -> [ExpInfo]
forall k a. Map k a -> [a]
M.elems (Map Name ExpInfo -> [ExpInfo]) -> Map Name ExpInfo -> [ExpInfo]
forall a b. (a -> b) -> a -> b
$ (ExpInfo -> ExpInfo -> ExpInfo)
-> Map Name ExpInfo -> Map Name ExpInfo -> Map Name ExpInfo
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (((ExpInfo, ExpInfo) -> ExpInfo) -> ExpInfo -> ExpInfo -> ExpInfo
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (ExpInfo, ExpInfo) -> ExpInfo
forall a b. (a, b) -> a
fst) Map Name ExpInfo
declInfo Map Name ExpInfo
puInfo
where
declInfo :: Map Name ExpInfo
declInfo = [(Name, ExpInfo)] -> Map Name ExpInfo
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (ExpInfo -> Name
eiVName ExpInfo
ei, ExpInfo
ei) | ExpInfo
ei <- [ExpInfo]
declVariableNamesDecl ]
puInfo :: Map Name ExpInfo
puInfo = [(Name, ExpInfo)] -> Map Name ExpInfo
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (ExpInfo -> Name
eiVName ExpInfo
ei, ExpInfo
ei) | ExpInfo
ei <- [ExpInfo]
declVariableNamesPU ]
declVariableNamesDecl :: [ExpInfo]
declVariableNamesDecl :: [ExpInfo]
declVariableNamesDecl = ((Declarator UA -> Maybe ExpInfo) -> [Declarator UA] -> [ExpInfo])
-> [Declarator UA] -> (Declarator UA -> Maybe ExpInfo) -> [ExpInfo]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Declarator UA -> Maybe ExpInfo) -> [Declarator UA] -> [ExpInfo]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (ProgramFile UA -> [Declarator UA]
forall from to. Biplate from to => from -> [to]
universeBi ProgramFile UA
pf :: [F.Declarator UA]) ((Declarator UA -> Maybe ExpInfo) -> [ExpInfo])
-> (Declarator UA -> Maybe ExpInfo) -> [ExpInfo]
forall a b. (a -> b) -> a -> b
$ \ Declarator UA
d -> case Declarator UA
d of
F.DeclVariable UA
_ SrcSpan
ss v :: Expression UA
v@(F.ExpValue UA
_ SrcSpan
_ (F.ValVariable Name
_)) Maybe (Expression UA)
_ Maybe (Expression UA)
_ -> ExpInfo -> Maybe ExpInfo
forall a. a -> Maybe a
Just (SrcSpan -> Name -> Name -> ExpInfo
ExpInfo SrcSpan
ss (Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.varName Expression UA
v) (Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.srcName Expression UA
v))
F.DeclArray UA
_ SrcSpan
ss v :: Expression UA
v@(F.ExpValue UA
_ SrcSpan
_ (F.ValVariable Name
_)) AList DimensionDeclarator UA
_ Maybe (Expression UA)
_ Maybe (Expression UA)
_ -> ExpInfo -> Maybe ExpInfo
forall a. a -> Maybe a
Just (SrcSpan -> Name -> Name -> ExpInfo
ExpInfo SrcSpan
ss (Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.varName Expression UA
v) (Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.srcName Expression UA
v))
Declarator UA
_ -> Maybe ExpInfo
forall a. Maybe a
Nothing
declVariableNamesPU :: [ExpInfo]
declVariableNamesPU :: [ExpInfo]
declVariableNamesPU = ((ProgramUnit UA -> Maybe ExpInfo)
-> [ProgramUnit UA] -> [ExpInfo])
-> [ProgramUnit UA]
-> (ProgramUnit UA -> Maybe ExpInfo)
-> [ExpInfo]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ProgramUnit UA -> Maybe ExpInfo) -> [ProgramUnit UA] -> [ExpInfo]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (ProgramFile UA -> [ProgramUnit UA]
forall from to. Biplate from to => from -> [to]
universeBi ProgramFile UA
pf :: [F.ProgramUnit UA]) ((ProgramUnit UA -> Maybe ExpInfo) -> [ExpInfo])
-> (ProgramUnit UA -> Maybe ExpInfo) -> [ExpInfo]
forall a b. (a -> b) -> a -> b
$ \ ProgramUnit UA
pu -> case ProgramUnit UA
pu of
F.PUFunction UA
_ SrcSpan
ss Maybe (TypeSpec UA)
_ PrefixSuffix UA
_ Name
_ Maybe (AList Expression UA)
_ (Just v :: Expression UA
v@(F.ExpValue UA
_ SrcSpan
_ (F.ValVariable Name
_))) [Block UA]
_ Maybe [ProgramUnit UA]
_ -> ExpInfo -> Maybe ExpInfo
forall a. a -> Maybe a
Just (SrcSpan -> Name -> Name -> ExpInfo
ExpInfo SrcSpan
ss (Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.varName Expression UA
v) (Expression UA -> Name
forall a. Expression (Analysis a) -> Name
FA.srcName Expression UA
v))
F.PUFunction UA
_ SrcSpan
ss Maybe (TypeSpec UA)
_ PrefixSuffix UA
_ Name
_ Maybe (AList Expression UA)
_ Maybe (Expression UA)
Nothing [Block UA]
_ Maybe [ProgramUnit UA]
_ -> ExpInfo -> Maybe ExpInfo
forall a. a -> Maybe a
Just (SrcSpan -> Name -> Name -> ExpInfo
ExpInfo SrcSpan
ss (ProgramUnit UA -> Name
puName ProgramUnit UA
pu) (ProgramUnit UA -> Name
puSrcName ProgramUnit UA
pu))
ProgramUnit UA
_ -> Maybe ExpInfo
forall a. Maybe a
Nothing
instance Show InferenceResult where
show :: InferenceResult -> Name
show (Inferred InferenceReport
report) = InferenceReport -> Name
forall a. Show a => a -> Name
show InferenceReport
report
show (InfInconsistent ConsistencyError
err) = ConsistencyError -> Name
forall a. Show a => a -> Name
show ConsistencyError
err
instance Describe InferenceReport
instance Describe InferenceResult
getInferred :: InferenceReport -> [(VV, UnitInfo)]
getInferred :: InferenceReport -> [(VV, UnitInfo)]
getInferred (InferenceReport ProgramFile UA
_ [(VV, UnitInfo)]
vars) = [(VV, UnitInfo)]
vars
inferUnits :: UnitAnalysis InferenceResult
inferUnits :: UnitAnalysis InferenceResult
inferUnits = do
([(VV, UnitInfo)]
eVars, UnitState
state) <- UnitSolver [(VV, UnitInfo)]
-> UnitAnalysis ([(VV, UnitInfo)], UnitState)
forall a. UnitSolver a -> UnitAnalysis (a, UnitState)
runInference ([(VV, UnitInfo)] -> [(VV, UnitInfo)]
chooseImplicitNames ([(VV, UnitInfo)] -> [(VV, UnitInfo)])
-> UnitSolver [(VV, UnitInfo)] -> UnitSolver [(VV, UnitInfo)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnitSolver [(VV, UnitInfo)]
runInferVariables)
let pfUA :: ProgramFile UA
pfUA = UnitState -> ProgramFile UA
usProgramFile UnitState
state
case [(VV, UnitInfo)]
eVars of
[] -> do
ConsistencyReport
consistency <- UnitAnalysis ConsistencyReport
checkUnits
InferenceResult -> UnitAnalysis InferenceResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (InferenceResult -> UnitAnalysis InferenceResult)
-> InferenceResult -> UnitAnalysis InferenceResult
forall a b. NFData a => (a -> b) -> a -> b
$!! case ConsistencyReport
consistency of
Consistent{} -> InferenceReport -> InferenceResult
Inferred (ProgramFile UA -> [(VV, UnitInfo)] -> InferenceReport
InferenceReport ProgramFile UA
pfUA [(VV, UnitInfo)]
eVars)
Inconsistent ConsistencyError
err -> ConsistencyError -> InferenceResult
InfInconsistent ConsistencyError
err
[(VV, UnitInfo)]
_ -> InferenceResult -> UnitAnalysis InferenceResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (InferenceResult -> UnitAnalysis InferenceResult)
-> (InferenceReport -> InferenceResult)
-> InferenceReport
-> UnitAnalysis InferenceResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InferenceReport -> InferenceResult
Inferred (InferenceReport -> UnitAnalysis InferenceResult)
-> InferenceReport -> UnitAnalysis InferenceResult
forall a b. NFData a => (a -> b) -> a -> b
$!! ProgramFile UA -> [(VV, UnitInfo)] -> InferenceReport
InferenceReport ProgramFile UA
pfUA [(VV, UnitInfo)]
eVars
runInferVariables :: UnitSolver [(VV, UnitInfo)]
runInferVariables :: UnitSolver [(VV, UnitInfo)]
runInferVariables = Constraints -> [(VV, UnitInfo)]
inferVariables (Constraints -> [(VV, UnitInfo)])
-> StateT UnitState UnitAnalysis Constraints
-> UnitSolver [(VV, UnitInfo)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT UnitState UnitAnalysis Constraints
getConstraints