{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wall #-}
module Camfort.Specification.Hoare.CheckBackend
( AnnotatedProgramUnit(..)
, apuPreconditions
, apuPostconditions
, apuPU
, apuAuxDecls
, BackendAnalysis
, HoareCheckResult(..)
, HoareBackendError(..)
, checkPU
) where
import Control.Exception (Exception (..))
import Control.Lens
import Control.Monad.Reader
import Control.Monad.State.Strict
import Control.Monad.Writer.Lazy
import Control.Monad.Trans.Maybe
import Data.Data (Data)
import Data.Foldable (foldlM)
import Data.Generics.Uniplate.Operations (childrenBi,
transformBi)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (isJust, maybeToList)
import Data.Void (Void)
import Data.SBV (SBool)
import qualified Language.Fortran.Analysis as F
import qualified Language.Fortran.AST as F
import qualified Language.Fortran.LValue as F
import qualified Language.Fortran.Util.Position as F
import qualified Data.List.NonEmpty as NE
import Camfort.Analysis
import Camfort.Analysis.Logger (Builder, Text)
import Camfort.Helpers.TypeLevel
import Camfort.Specification.Hoare.Annotation
import Camfort.Specification.Hoare.Syntax
import Camfort.Specification.Hoare.Translate
import Language.Fortran.Model
import Language.Fortran.Model.Repr.Prim
import Language.Fortran.Model.Translate
import Language.Fortran.Model.Vars
import Language.Expression
import Language.Expression.Choice
import Language.Expression.Pretty
import Language.Expression.Prop
import Language.Verification
import Language.Verification.Conditions
#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail
#endif
data AnnotatedProgramUnit =
AnnotatedProgramUnit
{ AnnotatedProgramUnit -> [PrimFormula InnerHA]
_apuPreconditions :: [PrimFormula InnerHA]
, AnnotatedProgramUnit -> [PrimFormula InnerHA]
_apuPostconditions :: [PrimFormula InnerHA]
, AnnotatedProgramUnit -> [AuxDecl InnerHA]
_apuAuxDecls :: [AuxDecl InnerHA]
, AnnotatedProgramUnit -> ProgramUnit (Analysis (HoareAnnotation A))
_apuPU :: F.ProgramUnit HA
}
data AnnotationError
= MissingWhileInvariant
| MissingSequenceAnn
data HoareBackendError
= VerifierError (VerifierError FortranVar)
| TranslateErrorAnn TranslateError
| TranslateErrorSrc TranslateError
| InvalidSourceName SourceName
| UnsupportedBlock (F.Block HA)
| UnexpectedBlock (F.Block HA)
| ArgWithoutDecl NamePair
| AuxVarConflict F.Name
| AssignVarNotInScope NamePair
| WrongAssignmentType Text SomeType
| NonLValueAssignment
| UnsupportedAssignment Text
| AnnotationError AnnotationError
instance Describe AnnotationError where
describeBuilder :: AnnotationError -> Builder
describeBuilder =
\case
AnnotationError
MissingSequenceAnn ->
Builder
"the program was insufficiently annotated; " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
"`seq` annotation required before this block"
AnnotationError
MissingWhileInvariant ->
Builder
"found a `do while` block with no invariant; " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
"invariant annotations must appear at the start of every `do while` loop"
instance Describe HoareBackendError where
describeBuilder :: HoareBackendError -> Builder
describeBuilder =
\case
VerifierError VerifierError FortranVar
e ->
Builder
"verifier error: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (VerifierError FortranVar -> String
forall e. Exception e => e -> String
displayException VerifierError FortranVar
e)
TranslateErrorAnn TranslateError
te ->
Builder
"translation error in logic annotation: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> TranslateError -> Builder
forall a. Describe a => a -> Builder
describeBuilder TranslateError
te
TranslateErrorSrc TranslateError
te ->
Builder
"translation error in source code: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> TranslateError -> Builder
forall a. Describe a => a -> Builder
describeBuilder TranslateError
te
InvalidSourceName SourceName
nm ->
Builder
"a program source name had no associated unique name: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (SourceName -> String
forall a. Pretty a => a -> String
pretty SourceName
nm)
UnsupportedBlock Block (Analysis (HoareAnnotation A))
_ -> Builder
"encountered unsupported block"
UnexpectedBlock Block (Analysis (HoareAnnotation A))
_ -> Builder
"a block was found in an illegal location"
ArgWithoutDecl NamePair
nm ->
Builder
"argument " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (NamePair -> String
forall a. Show a => a -> String
show NamePair
nm) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
" doesn't have an associated type declaration"
AuxVarConflict String
nm ->
Builder
"auxiliary variable " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder String
nm Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
" has the same name as a program variable; this is not allowed"
AnnotationError AnnotationError
e -> AnnotationError -> Builder
forall a. Describe a => a -> Builder
describeBuilder AnnotationError
e
AssignVarNotInScope NamePair
nm ->
Builder
"variable " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (NamePair -> String
forall a. Pretty a => a -> String
pretty NamePair
nm) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
" is being assigned to but is not in scope"
WrongAssignmentType Text
message SomeType
gotType ->
Builder
"unexpected variable type; expected " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Text -> Builder
forall a. Describe a => a -> Builder
describeBuilder Text
message Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
"; got " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (SomeType -> String
forall a. Pretty a => a -> String
pretty SomeType
gotType)
HoareBackendError
NonLValueAssignment ->
Builder
"assignment an expression which is not a valid lvalue"
UnsupportedAssignment Text
message ->
Builder
"unsupported assignment; " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Text -> Builder
forall a. Describe a => a -> Builder
describeBuilder Text
message
type HoareBackendWarning = Void
type BackendAnalysis = AnalysisT HoareBackendError HoareBackendWarning IO
data HoareCheckResult = HoareCheckResult (F.ProgramUnit HA) Bool
deriving (Int -> HoareCheckResult -> ShowS
[HoareCheckResult] -> ShowS
HoareCheckResult -> String
(Int -> HoareCheckResult -> ShowS)
-> (HoareCheckResult -> String)
-> ([HoareCheckResult] -> ShowS)
-> Show HoareCheckResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HoareCheckResult -> ShowS
showsPrec :: Int -> HoareCheckResult -> ShowS
$cshow :: HoareCheckResult -> String
show :: HoareCheckResult -> String
$cshowList :: [HoareCheckResult] -> ShowS
showList :: [HoareCheckResult] -> ShowS
Show)
instance ExitCodeOfReport HoareCheckResult where
exitCodeOf :: HoareCheckResult -> Int
exitCodeOf (HoareCheckResult ProgramUnit (Analysis (HoareAnnotation A))
_ Bool
r) = if Bool
r then Int
0 else Int
1
describePuName :: F.ProgramUnitName -> Builder
describePuName :: ProgramUnitName -> Builder
describePuName (F.Named String
n) = String -> Builder
forall a. Describe a => a -> Builder
describeBuilder String
n
describePuName ProgramUnitName
F.NamelessBlockData = Builder
"<nameless block data>"
describePuName ProgramUnitName
F.NamelessComment = Builder
"<nameless comment>"
describePuName ProgramUnitName
F.NamelessMain = Builder
"<nameless main>"
instance Describe HoareCheckResult where
describeBuilder :: HoareCheckResult -> Builder
describeBuilder (HoareCheckResult ProgramUnit (Analysis (HoareAnnotation A))
pu Bool
result) =
Builder
"Program unit '" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ProgramUnitName -> Builder
describePuName (ProgramUnit (Analysis (HoareAnnotation A)) -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puSrcName ProgramUnit (Analysis (HoareAnnotation A))
pu) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"': " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
(if Bool
result then Builder
"verified!" else Builder
"unverifiable!")
type ScopeVars = Map UniqueName SomeVar
data CheckHoareEnv =
CheckHoareEnv
{ CheckHoareEnv -> Bool
_heImplicitVars :: Bool
, CheckHoareEnv -> ScopeVars
_heVarsInScope :: ScopeVars
, CheckHoareEnv -> Map SourceName [UniqueName]
_heSourceToUnique :: Map SourceName [UniqueName]
, CheckHoareEnv
-> forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> PrimReprHandler a
_heReprHandler :: forall p k a. Prim p k a -> PrimReprHandler a
, CheckHoareEnv -> ProgramUnit (Analysis (HoareAnnotation A))
_hePU :: F.ProgramUnit HA
}
emptyEnv :: F.ProgramUnit HA -> PrimReprSpec -> CheckHoareEnv
emptyEnv :: ProgramUnit (Analysis (HoareAnnotation A))
-> PrimReprSpec -> CheckHoareEnv
emptyEnv ProgramUnit (Analysis (HoareAnnotation A))
pu PrimReprSpec
spec = Bool
-> ScopeVars
-> Map SourceName [UniqueName]
-> (forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> PrimReprHandler a)
-> ProgramUnit (Analysis (HoareAnnotation A))
-> CheckHoareEnv
CheckHoareEnv Bool
True ScopeVars
forall a. Monoid a => a
mempty Map SourceName [UniqueName]
forall a. Monoid a => a
mempty (PrimReprSpec -> Prim p k a -> PrimReprHandler a
forall (p :: Precision) (k :: BasicType) a.
PrimReprSpec -> Prim p k a -> PrimReprHandler a
makeSymRepr PrimReprSpec
spec) ProgramUnit (Analysis (HoareAnnotation A))
pu
makeLenses ''AnnotatedProgramUnit
makeLenses ''CheckHoareEnv
instance HasPrimReprHandlers CheckHoareEnv where
primReprHandler :: forall (p :: Precision) (k :: BasicType) a.
CheckHoareEnv -> Prim p k a -> PrimReprHandler a
primReprHandler = Getting
(Prim p k a -> PrimReprHandler a)
CheckHoareEnv
(Prim p k a -> PrimReprHandler a)
-> CheckHoareEnv -> Prim p k a -> PrimReprHandler a
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
(Prim p k a -> PrimReprHandler a)
CheckHoareEnv
(Prim p k a -> PrimReprHandler a)
forall (p :: Precision) (k :: BasicType) a (f :: * -> *).
(Contravariant f, Functor f) =>
((Prim p k a -> PrimReprHandler a)
-> f (Prim p k a -> PrimReprHandler a))
-> CheckHoareEnv -> f CheckHoareEnv
heReprHandler
checkPU :: AnnotatedProgramUnit
-> PrimReprSpec
-> BackendAnalysis HoareCheckResult
checkPU :: AnnotatedProgramUnit
-> PrimReprSpec -> BackendAnalysis HoareCheckResult
checkPU AnnotatedProgramUnit
apu PrimReprSpec
symSpec = do
let pu :: ProgramUnit (Analysis (HoareAnnotation A))
pu = AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting
(ProgramUnit (Analysis (HoareAnnotation A)))
AnnotatedProgramUnit
(ProgramUnit (Analysis (HoareAnnotation A)))
-> ProgramUnit (Analysis (HoareAnnotation A))
forall s a. s -> Getting a s a -> a
^. Getting
(ProgramUnit (Analysis (HoareAnnotation A)))
AnnotatedProgramUnit
(ProgramUnit (Analysis (HoareAnnotation A)))
Lens'
AnnotatedProgramUnit (ProgramUnit (Analysis (HoareAnnotation A)))
apuPU
(((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))])
bodyTriple, [FortranAssignment]
initialAssignments), CheckHoareEnv
env) <- (StateT
CheckHoareEnv
BackendAnalysis
((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment])
-> CheckHoareEnv
-> AnalysisT
HoareBackendError
Void
IO
(((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment]),
CheckHoareEnv))
-> CheckHoareEnv
-> StateT
CheckHoareEnv
BackendAnalysis
((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment])
-> AnalysisT
HoareBackendError
Void
IO
(((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment]),
CheckHoareEnv)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
CheckHoareEnv
BackendAnalysis
((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment])
-> CheckHoareEnv
-> AnalysisT
HoareBackendError
Void
IO
(((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment]),
CheckHoareEnv)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ProgramUnit (Analysis (HoareAnnotation A))
-> PrimReprSpec -> CheckHoareEnv
emptyEnv ProgramUnit (Analysis (HoareAnnotation A))
pu PrimReprSpec
symSpec) (StateT
CheckHoareEnv
BackendAnalysis
((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment])
-> AnalysisT
HoareBackendError
Void
IO
(((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment]),
CheckHoareEnv))
-> StateT
CheckHoareEnv
BackendAnalysis
((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment])
-> AnalysisT
HoareBackendError
Void
IO
(((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment]),
CheckHoareEnv)
forall a b. (a -> b) -> a -> b
$ do
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Setting up"
([Block (Analysis (HoareAnnotation A))]
body, [FortranAssignment]
initialAssignments) <- CheckHoareMut
([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
initialSetup
Bool
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([FortranAssignment] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FortranAssignment]
initialAssignments) (StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logDebug' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$
Text
"Found " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
describeShow ([FortranAssignment] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FortranAssignment]
initialAssignments) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
Text
" initial assignments: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [String] -> Text
forall a. Show a => a -> Text
describeShow ((FortranAssignment -> String) -> [FortranAssignment] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map FortranAssignment -> String
forall a. Pretty a => a -> String
pretty [FortranAssignment]
initialAssignments)
AnnotatedProgramUnit -> StateT CheckHoareEnv BackendAnalysis ()
addAuxVariables AnnotatedProgramUnit
apu
let translatePUFormulae :: [PrimFormula InnerHA]
-> StateT
CheckHoareEnv
BackendAnalysis
[Prop (HFree' AllOps FortranVar) Bool]
translatePUFormulae =
ReaderT
CheckHoareEnv
(StateT CheckHoareEnv BackendAnalysis)
[Prop (HFree' AllOps FortranVar) Bool]
-> StateT
CheckHoareEnv
BackendAnalysis
[Prop (HFree' AllOps FortranVar) Bool]
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState
(ReaderT
CheckHoareEnv
(StateT CheckHoareEnv BackendAnalysis)
[Prop (HFree' AllOps FortranVar) Bool]
-> StateT
CheckHoareEnv
BackendAnalysis
[Prop (HFree' AllOps FortranVar) Bool])
-> ([PrimFormula InnerHA]
-> ReaderT
CheckHoareEnv
(StateT CheckHoareEnv BackendAnalysis)
[Prop (HFree' AllOps FortranVar) Bool])
-> [PrimFormula InnerHA]
-> StateT
CheckHoareEnv
BackendAnalysis
[Prop (HFree' AllOps FortranVar) Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula InnerHA
-> ReaderT
CheckHoareEnv
(StateT CheckHoareEnv BackendAnalysis)
(Prop (HFree' AllOps FortranVar) Bool))
-> [PrimFormula InnerHA]
-> ReaderT
CheckHoareEnv
(StateT CheckHoareEnv BackendAnalysis)
[Prop (HFree' AllOps FortranVar) Bool]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (ProgramUnit (Analysis (HoareAnnotation A))
-> PrimFormula InnerHA
-> ReaderT
CheckHoareEnv
(StateT CheckHoareEnv BackendAnalysis)
(Prop (HFree' AllOps FortranVar) Bool)
forall o ann (m :: * -> *) w.
(Spanned o, ReportAnn (Analysis ann), Data ann,
MonadReader CheckHoareEnv m, MonadAnalysis HoareBackendError w m,
MonadFail m) =>
o
-> PrimFormula (Analysis ann)
-> m (Prop (HFree' AllOps FortranVar) Bool)
tryTranslateFormula ProgramUnit (Analysis (HoareAnnotation A))
pu)
[Prop (HFree' AllOps FortranVar) Bool]
preconds <- [PrimFormula InnerHA]
-> StateT
CheckHoareEnv
BackendAnalysis
[Prop (HFree' AllOps FortranVar) Bool]
translatePUFormulae (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting
[PrimFormula InnerHA] AnnotatedProgramUnit [PrimFormula InnerHA]
-> [PrimFormula InnerHA]
forall s a. s -> Getting a s a -> a
^. Getting
[PrimFormula InnerHA] AnnotatedProgramUnit [PrimFormula InnerHA]
Lens' AnnotatedProgramUnit [PrimFormula InnerHA]
apuPreconditions)
[Prop (HFree' AllOps FortranVar) Bool]
postconds <- [PrimFormula InnerHA]
-> StateT
CheckHoareEnv
BackendAnalysis
[Prop (HFree' AllOps FortranVar) Bool]
translatePUFormulae (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting
[PrimFormula InnerHA] AnnotatedProgramUnit [PrimFormula InnerHA]
-> [PrimFormula InnerHA]
forall s a. s -> Getting a s a -> a
^. Getting
[PrimFormula InnerHA] AnnotatedProgramUnit [PrimFormula InnerHA]
Lens' AnnotatedProgramUnit [PrimFormula InnerHA]
apuPostconditions)
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Interpreting pre- and postconditions"
let precond :: Prop (HFree' AllOps FortranVar) Bool
precond = [Prop (HFree' AllOps FortranVar) Bool]
-> Prop (HFree' AllOps FortranVar) Bool
forall (expr :: * -> *). [Prop expr Bool] -> Prop expr Bool
propAnd [Prop (HFree' AllOps FortranVar) Bool]
preconds
postcond :: Prop (HFree' AllOps FortranVar) Bool
postcond = [Prop (HFree' AllOps FortranVar) Bool]
-> Prop (HFree' AllOps FortranVar) Bool
forall (expr :: * -> *). [Prop expr Bool] -> Prop expr Bool
propAnd [Prop (HFree' AllOps FortranVar) Bool]
postconds
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Found preconditions: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. Describe a => a -> Text
describe (Prop (HFree' AllOps FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (HFree' AllOps FortranVar) Bool
precond)
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Found postconditions: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. Describe a => a -> Text
describe (Prop (HFree' AllOps FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (HFree' AllOps FortranVar) Bool
postcond)
let postcond' :: Prop (HFree' AllOps FortranVar) Bool
postcond' = Prop (HFree' AllOps FortranVar) Bool
-> [FortranAssignment] -> Prop (HFree' AllOps FortranVar) Bool
forall (expr :: (* -> *) -> * -> *) (v :: * -> *).
(HMonad expr, VerifiableVar v) =>
Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
chainSub Prop (HFree' AllOps FortranVar) Bool
postcond [FortranAssignment]
initialAssignments
((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment])
-> StateT
CheckHoareEnv
BackendAnalysis
((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))]),
[FortranAssignment])
forall a. a -> StateT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Prop (HFree' AllOps FortranVar) Bool
precond, Prop (HFree' AllOps FortranVar) Bool
postcond', [Block (Analysis (HoareAnnotation A))]
body), [FortranAssignment]
initialAssignments)
(ReaderT CheckHoareEnv BackendAnalysis HoareCheckResult
-> CheckHoareEnv -> BackendAnalysis HoareCheckResult)
-> CheckHoareEnv
-> ReaderT CheckHoareEnv BackendAnalysis HoareCheckResult
-> BackendAnalysis HoareCheckResult
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT CheckHoareEnv BackendAnalysis HoareCheckResult
-> CheckHoareEnv -> BackendAnalysis HoareCheckResult
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT CheckHoareEnv
env (ReaderT CheckHoareEnv BackendAnalysis HoareCheckResult
-> BackendAnalysis HoareCheckResult)
-> ReaderT CheckHoareEnv BackendAnalysis HoareCheckResult
-> BackendAnalysis HoareCheckResult
forall a b. (a -> b) -> a -> b
$ do
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> ReaderT CheckHoareEnv BackendAnalysis ())
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Computing verification conditions"
(()
_, [Prop (HFree' AllOps FortranVar) Bool]
vcs) <- GenM () -> CheckHoare ((), [Prop (HFree' AllOps FortranVar) Bool])
forall a.
GenM a -> CheckHoare (a, [Prop (HFree' AllOps FortranVar) Bool])
runGenM ([FortranAssignment]
-> (Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody' [FortranAssignment]
initialAssignments (Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))])
bodyTriple)
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> ReaderT CheckHoareEnv BackendAnalysis ())
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Verifying conditions:"
let checkVcs :: Int
-> [Prop (HFree' AllOps FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis Bool
checkVcs Int
_ [] = Bool -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall a. a -> ReaderT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkVcs Int
i (Prop (HFree' AllOps FortranVar) Bool
vc : [Prop (HFree' AllOps FortranVar) Bool]
rest) = do
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> ReaderT CheckHoareEnv BackendAnalysis ())
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
describeShow Int
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. Describe a => a -> Text
describe (Prop (HFree' AllOps FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (HFree' AllOps FortranVar) Bool
vc)
Bool
result <- (HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool)
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis Bool
verifyVc (ProgramUnit (Analysis (HoareAnnotation A))
-> HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' ProgramUnit (Analysis (HoareAnnotation A))
pu) Prop (HFree' AllOps FortranVar) Bool
vc
if Bool
result
then Int
-> [Prop (HFree' AllOps FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis Bool
checkVcs (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) [Prop (HFree' AllOps FortranVar) Bool]
rest
else do
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu Text
" - Failed!"
(Int
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis ())
-> [Int]
-> [Prop (HFree' AllOps FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ Int
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis ()
printUnchecked [(Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i)..] [Prop (HFree' AllOps FortranVar) Bool]
vcs
Bool -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall a. a -> ReaderT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
printUnchecked :: Int
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis ()
printUnchecked Int
i Prop (HFree' AllOps FortranVar) Bool
vc = do
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> ReaderT CheckHoareEnv BackendAnalysis ())
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
describeShow Int
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. Describe a => a -> Text
describe (Prop (HFree' AllOps FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (HFree' AllOps FortranVar) Bool
vc)
ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu Text
" - Unchecked"
ProgramUnit (Analysis (HoareAnnotation A))
-> Bool -> HoareCheckResult
HoareCheckResult ProgramUnit (Analysis (HoareAnnotation A))
pu (Bool -> HoareCheckResult)
-> ReaderT CheckHoareEnv BackendAnalysis Bool
-> ReaderT CheckHoareEnv BackendAnalysis HoareCheckResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> [Prop (HFree' AllOps FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis Bool
checkVcs (Int
1 :: Int) [Prop (HFree' AllOps FortranVar) Bool]
vcs
varOfType :: NamePair -> SomeType -> SomeVar
varOfType :: NamePair -> SomeType -> Some FortranVar
varOfType NamePair
names (Some D a
d) = FortranVar a -> Some FortranVar
forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some (D a -> NamePair -> FortranVar a
forall a. D a -> NamePair -> FortranVar a
FortranVar D a
d NamePair
names)
expNamePair :: F.Expression (F.Analysis a) -> NamePair
expNamePair :: forall a. Expression (Analysis a) -> NamePair
expNamePair = UniqueName -> SourceName -> NamePair
NamePair (UniqueName -> SourceName -> NamePair)
-> (Expression (Analysis a) -> UniqueName)
-> Expression (Analysis a)
-> SourceName
-> NamePair
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> UniqueName
UniqueName (String -> UniqueName)
-> (Expression (Analysis a) -> String)
-> Expression (Analysis a)
-> UniqueName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression (Analysis a) -> String
forall a. Expression (Analysis a) -> String
F.varName (Expression (Analysis a) -> SourceName -> NamePair)
-> (Expression (Analysis a) -> SourceName)
-> Expression (Analysis a)
-> NamePair
forall a b.
(Expression (Analysis a) -> a -> b)
-> (Expression (Analysis a) -> a) -> Expression (Analysis a) -> b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SourceName
SourceName (String -> SourceName)
-> (Expression (Analysis a) -> String)
-> Expression (Analysis a)
-> SourceName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression (Analysis a) -> String
forall a. Expression (Analysis a) -> String
F.srcName
functionNamePair :: F.ProgramUnit (F.Analysis a) -> NamePair
functionNamePair :: forall a. ProgramUnit (Analysis a) -> NamePair
functionNamePair =
UniqueName -> SourceName -> NamePair
NamePair (UniqueName -> SourceName -> NamePair)
-> (ProgramUnit (Analysis a) -> UniqueName)
-> ProgramUnit (Analysis a)
-> SourceName
-> NamePair
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> UniqueName
UniqueName (String -> UniqueName)
-> (ProgramUnit (Analysis a) -> String)
-> ProgramUnit (Analysis a)
-> UniqueName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramUnitName -> String
fromPuName (ProgramUnitName -> String)
-> (ProgramUnit (Analysis a) -> ProgramUnitName)
-> ProgramUnit (Analysis a)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramUnit (Analysis a) -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName
(ProgramUnit (Analysis a) -> SourceName -> NamePair)
-> (ProgramUnit (Analysis a) -> SourceName)
-> ProgramUnit (Analysis a)
-> NamePair
forall a b.
(ProgramUnit (Analysis a) -> a -> b)
-> (ProgramUnit (Analysis a) -> a) -> ProgramUnit (Analysis a) -> b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SourceName
SourceName (String -> SourceName)
-> (ProgramUnit (Analysis a) -> String)
-> ProgramUnit (Analysis a)
-> SourceName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramUnitName -> String
fromPuName (ProgramUnitName -> String)
-> (ProgramUnit (Analysis a) -> ProgramUnitName)
-> ProgramUnit (Analysis a)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramUnit (Analysis a) -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puSrcName
where
fromPuName :: ProgramUnitName -> String
fromPuName (F.Named String
n) = String
n
fromPuName ProgramUnitName
_ = ShowS
forall a. HasCallStack => String -> a
error String
"impossible: function has no name"
newVar :: NamePair -> SomeType -> CheckHoareEnv -> CheckHoareEnv
newVar :: NamePair -> SomeType -> CheckHoareEnv -> CheckHoareEnv
newVar np :: NamePair
np@(NamePair UniqueName
uniq SourceName
src) SomeType
ty
= ((ScopeVars -> Identity ScopeVars)
-> CheckHoareEnv -> Identity CheckHoareEnv
Lens' CheckHoareEnv ScopeVars
heVarsInScope ((ScopeVars -> Identity ScopeVars)
-> CheckHoareEnv -> Identity CheckHoareEnv)
-> ((Maybe (Some FortranVar) -> Identity (Maybe (Some FortranVar)))
-> ScopeVars -> Identity ScopeVars)
-> (Maybe (Some FortranVar) -> Identity (Maybe (Some FortranVar)))
-> CheckHoareEnv
-> Identity CheckHoareEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index ScopeVars -> Lens' ScopeVars (Maybe (IxValue ScopeVars))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index ScopeVars
UniqueName
uniq ((Maybe (Some FortranVar) -> Identity (Maybe (Some FortranVar)))
-> CheckHoareEnv -> Identity CheckHoareEnv)
-> Maybe (Some FortranVar) -> CheckHoareEnv -> CheckHoareEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Some FortranVar -> Maybe (Some FortranVar)
forall a. a -> Maybe a
Just (NamePair -> SomeType -> Some FortranVar
varOfType NamePair
np SomeType
ty))
(CheckHoareEnv -> CheckHoareEnv)
-> (CheckHoareEnv -> CheckHoareEnv)
-> CheckHoareEnv
-> CheckHoareEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Map SourceName [UniqueName]
-> Identity (Map SourceName [UniqueName]))
-> CheckHoareEnv -> Identity CheckHoareEnv
Lens' CheckHoareEnv (Map SourceName [UniqueName])
heSourceToUnique ((Map SourceName [UniqueName]
-> Identity (Map SourceName [UniqueName]))
-> CheckHoareEnv -> Identity CheckHoareEnv)
-> ((Maybe [UniqueName] -> Identity (Maybe [UniqueName]))
-> Map SourceName [UniqueName]
-> Identity (Map SourceName [UniqueName]))
-> (Maybe [UniqueName] -> Identity (Maybe [UniqueName]))
-> CheckHoareEnv
-> Identity CheckHoareEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map SourceName [UniqueName])
-> Lens'
(Map SourceName [UniqueName])
(Maybe (IxValue (Map SourceName [UniqueName])))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map SourceName [UniqueName])
SourceName
src ((Maybe [UniqueName] -> Identity (Maybe [UniqueName]))
-> CheckHoareEnv -> Identity CheckHoareEnv)
-> (Maybe [UniqueName] -> Maybe [UniqueName])
-> CheckHoareEnv
-> CheckHoareEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ \case
Maybe [UniqueName]
Nothing -> [UniqueName] -> Maybe [UniqueName]
forall a. a -> Maybe a
Just [UniqueName
uniq]
Just [UniqueName]
xs -> [UniqueName] -> Maybe [UniqueName]
forall a. a -> Maybe a
Just (UniqueName
uniq UniqueName -> [UniqueName] -> [UniqueName]
forall a. a -> [a] -> [a]
: [UniqueName]
xs))
setFormulaUniqueNames
:: (Data ann)
=> Map SourceName [UniqueName]
-> PrimFormula (F.Analysis ann)
-> PrimFormula (F.Analysis ann)
setFormulaUniqueNames :: forall ann.
Data ann =>
Map SourceName [UniqueName]
-> PrimFormula (Analysis ann) -> PrimFormula (Analysis ann)
setFormulaUniqueNames Map SourceName [UniqueName]
nameMap = (Expression InnerHA -> Expression InnerHA)
-> PrimFormula (Analysis ann) -> PrimFormula (Analysis ann)
forall from to. Biplate from to => (to -> to) -> from -> from
transformBi Expression InnerHA -> Expression InnerHA
setExpUN
where
setExpUN :: F.Expression InnerHA -> F.Expression InnerHA
setExpUN :: Expression InnerHA -> Expression InnerHA
setExpUN = do
NamePair
np <- NamePair -> NamePair
realNamePair (NamePair -> NamePair)
-> (Expression InnerHA -> NamePair)
-> Expression InnerHA
-> NamePair
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression InnerHA -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair
(InnerHA -> InnerHA) -> Expression InnerHA -> Expression InnerHA
forall a. (a -> a) -> Expression a -> Expression a
forall (f :: * -> *) a. Annotated f => (a -> a) -> f a -> f a
F.modifyAnnotation (String -> InnerHA -> InnerHA
forall {a}. String -> Analysis a -> Analysis a
setAnnUniq (NamePair
np NamePair -> Getting String NamePair String -> String
forall s a. s -> Getting a s a -> a
^. (UniqueName -> Const String UniqueName)
-> NamePair -> Const String NamePair
Lens' NamePair UniqueName
npUnique ((UniqueName -> Const String UniqueName)
-> NamePair -> Const String NamePair)
-> ((String -> Const String String)
-> UniqueName -> Const String UniqueName)
-> Getting String NamePair String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Const String String)
-> UniqueName -> Const String UniqueName
(Unwrapped UniqueName -> Const String (Unwrapped UniqueName))
-> UniqueName -> Const String UniqueName
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Iso
UniqueName UniqueName (Unwrapped UniqueName) (Unwrapped UniqueName)
_Wrapped))
realNamePair :: NamePair -> NamePair
realNamePair np :: NamePair
np@(NamePair UniqueName
_ SourceName
src) =
case Map SourceName [UniqueName]
nameMap Map SourceName [UniqueName]
-> Getting
(First UniqueName) (Map SourceName [UniqueName]) UniqueName
-> Maybe UniqueName
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index (Map SourceName [UniqueName])
-> Traversal'
(Map SourceName [UniqueName])
(IxValue (Map SourceName [UniqueName]))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map SourceName [UniqueName])
SourceName
src (([UniqueName] -> Const (First UniqueName) [UniqueName])
-> Map SourceName [UniqueName]
-> Const (First UniqueName) (Map SourceName [UniqueName]))
-> ((UniqueName -> Const (First UniqueName) UniqueName)
-> [UniqueName] -> Const (First UniqueName) [UniqueName])
-> Getting
(First UniqueName) (Map SourceName [UniqueName]) UniqueName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((UniqueName, [UniqueName])
-> Const (First UniqueName) (UniqueName, [UniqueName]))
-> [UniqueName] -> Const (First UniqueName) [UniqueName]
forall s t a b. Cons s t a b => Prism s t (a, s) (b, t)
Prism
[UniqueName]
[UniqueName]
(UniqueName, [UniqueName])
(UniqueName, [UniqueName])
_Cons (((UniqueName, [UniqueName])
-> Const (First UniqueName) (UniqueName, [UniqueName]))
-> [UniqueName] -> Const (First UniqueName) [UniqueName])
-> ((UniqueName -> Const (First UniqueName) UniqueName)
-> (UniqueName, [UniqueName])
-> Const (First UniqueName) (UniqueName, [UniqueName]))
-> (UniqueName -> Const (First UniqueName) UniqueName)
-> [UniqueName]
-> Const (First UniqueName) [UniqueName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UniqueName -> Const (First UniqueName) UniqueName)
-> (UniqueName, [UniqueName])
-> Const (First UniqueName) (UniqueName, [UniqueName])
forall s t a b. Field1 s t a b => Lens s t a b
Lens
(UniqueName, [UniqueName])
(UniqueName, [UniqueName])
UniqueName
UniqueName
_1 of
Just UniqueName
uniq -> UniqueName -> SourceName -> NamePair
NamePair UniqueName
uniq SourceName
src
Maybe UniqueName
Nothing -> NamePair
np
setAnnUniq :: String -> Analysis a -> Analysis a
setAnnUniq String
uniq Analysis a
a = Analysis a
a { uniqueName :: Maybe String
F.uniqueName = String -> Maybe String
forall a. a -> Maybe a
Just String
uniq }
type CheckHoareMut = StateT CheckHoareEnv BackendAnalysis
type CheckHoare = ReaderT CheckHoareEnv BackendAnalysis
type FortranAssignment = Assignment MetaExpr FortranVar
initialSetup :: CheckHoareMut ([F.Block HA], [FortranAssignment])
initialSetup :: CheckHoareMut
([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
initialSetup = do
ProgramUnit (Analysis (HoareAnnotation A))
pu <- Getting
(ProgramUnit (Analysis (HoareAnnotation A)))
CheckHoareEnv
(ProgramUnit (Analysis (HoareAnnotation A)))
-> StateT
CheckHoareEnv
BackendAnalysis
(ProgramUnit (Analysis (HoareAnnotation A)))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
(ProgramUnit (Analysis (HoareAnnotation A)))
CheckHoareEnv
(ProgramUnit (Analysis (HoareAnnotation A)))
Lens' CheckHoareEnv (ProgramUnit (Analysis (HoareAnnotation A)))
hePU
let body :: [Block (Analysis (HoareAnnotation A))]
body = ProgramUnit (Analysis (HoareAnnotation A))
-> [Block (Analysis (HoareAnnotation A))]
forall from to. Biplate from to => from -> [to]
childrenBi ProgramUnit (Analysis (HoareAnnotation A))
pu :: [F.Block HA]
[Expression (Analysis (HoareAnnotation A))]
rawArgNames <- case ProgramUnit (Analysis (HoareAnnotation A))
pu of
F.PUFunction Analysis (HoareAnnotation A)
_ SrcSpan
_ (Just TypeSpec (Analysis (HoareAnnotation A))
rettype) PrefixSuffix (Analysis (HoareAnnotation A))
_ String
_ Maybe (AList Expression (Analysis (HoareAnnotation A)))
funargs Maybe (Expression (Analysis (HoareAnnotation A)))
retvalue [Block (Analysis (HoareAnnotation A))]
_ Maybe [ProgramUnit (Analysis (HoareAnnotation A))]
_ -> do
SomeType
rettype' <- ReaderT
CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
-> StateT CheckHoareEnv BackendAnalysis SomeType
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState (ReaderT
CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
-> StateT CheckHoareEnv BackendAnalysis SomeType)
-> ReaderT
CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
-> StateT CheckHoareEnv BackendAnalysis SomeType
forall a b. (a -> b) -> a -> b
$ TypeInfo (Analysis (HoareAnnotation A))
-> ReaderT
CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
TypeInfo (Analysis ann) -> m SomeType
tryTranslateTypeInfo (TypeSpec (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall ann. TypeSpec ann -> TypeInfo ann
typeInfo TypeSpec (Analysis (HoareAnnotation A))
rettype)
let retNames :: NamePair
retNames = case Maybe (Expression (Analysis (HoareAnnotation A)))
retvalue of
Just Expression (Analysis (HoareAnnotation A))
rv -> Expression (Analysis (HoareAnnotation A)) -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair Expression (Analysis (HoareAnnotation A))
rv
Maybe (Expression (Analysis (HoareAnnotation A)))
Nothing -> ProgramUnit (Analysis (HoareAnnotation A)) -> NamePair
forall a. ProgramUnit (Analysis a) -> NamePair
functionNamePair ProgramUnit (Analysis (HoareAnnotation A))
pu
(CheckHoareEnv -> CheckHoareEnv)
-> StateT CheckHoareEnv BackendAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CheckHoareEnv -> CheckHoareEnv)
-> StateT CheckHoareEnv BackendAnalysis ())
-> (CheckHoareEnv -> CheckHoareEnv)
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ NamePair -> SomeType -> CheckHoareEnv -> CheckHoareEnv
newVar NamePair
retNames SomeType
rettype'
[Expression (Analysis (HoareAnnotation A))]
-> StateT
CheckHoareEnv
BackendAnalysis
[Expression (Analysis (HoareAnnotation A))]
forall a. a -> StateT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expression (Analysis (HoareAnnotation A))]
-> (AList Expression (Analysis (HoareAnnotation A))
-> [Expression (Analysis (HoareAnnotation A))])
-> Maybe (AList Expression (Analysis (HoareAnnotation A)))
-> [Expression (Analysis (HoareAnnotation A))]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] AList Expression (Analysis (HoareAnnotation A))
-> [Expression (Analysis (HoareAnnotation A))]
forall (t :: * -> *) a. AList t a -> [t a]
F.aStrip Maybe (AList Expression (Analysis (HoareAnnotation A)))
funargs)
F.PUSubroutine Analysis (HoareAnnotation A)
_ SrcSpan
_ PrefixSuffix (Analysis (HoareAnnotation A))
_ String
_ Maybe (AList Expression (Analysis (HoareAnnotation A)))
subargs [Block (Analysis (HoareAnnotation A))]
_ Maybe [ProgramUnit (Analysis (HoareAnnotation A))]
_ -> [Expression (Analysis (HoareAnnotation A))]
-> StateT
CheckHoareEnv
BackendAnalysis
[Expression (Analysis (HoareAnnotation A))]
forall a. a -> StateT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expression (Analysis (HoareAnnotation A))]
-> (AList Expression (Analysis (HoareAnnotation A))
-> [Expression (Analysis (HoareAnnotation A))])
-> Maybe (AList Expression (Analysis (HoareAnnotation A)))
-> [Expression (Analysis (HoareAnnotation A))]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] AList Expression (Analysis (HoareAnnotation A))
-> [Expression (Analysis (HoareAnnotation A))]
forall (t :: * -> *) a. AList t a -> [t a]
F.aStrip Maybe (AList Expression (Analysis (HoareAnnotation A)))
subargs)
ProgramUnit (Analysis (HoareAnnotation A))
_ -> [Expression (Analysis (HoareAnnotation A))]
-> StateT
CheckHoareEnv
BackendAnalysis
[Expression (Analysis (HoareAnnotation A))]
forall a. a -> StateT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return []
let argNames :: [NamePair]
argNames = (Expression (Analysis (HoareAnnotation A)) -> NamePair)
-> [Expression (Analysis (HoareAnnotation A))] -> [NamePair]
forall a b. (a -> b) -> [a] -> [b]
map Expression (Analysis (HoareAnnotation A)) -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair [Expression (Analysis (HoareAnnotation A))]
rawArgNames
([Block (Analysis (HoareAnnotation A))]
restBody, [FortranAssignment]
initialAssignments) <- [Block (Analysis (HoareAnnotation A))]
-> CheckHoareMut
([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
readInitialBlocks [Block (Analysis (HoareAnnotation A))]
body
[NamePair]
-> (NamePair -> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [NamePair]
argNames ((NamePair -> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ())
-> (NamePair -> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ \NamePair
argName -> do
Bool
hasType <- Maybe (Some FortranVar) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Some FortranVar) -> Bool)
-> StateT CheckHoareEnv BackendAnalysis (Maybe (Some FortranVar))
-> StateT CheckHoareEnv BackendAnalysis Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting
(Maybe (Some FortranVar)) CheckHoareEnv (Maybe (Some FortranVar))
-> StateT CheckHoareEnv BackendAnalysis (Maybe (Some FortranVar))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
-> CheckHoareEnv -> Const (Maybe (Some FortranVar)) CheckHoareEnv
Lens' CheckHoareEnv ScopeVars
heVarsInScope ((ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
-> CheckHoareEnv -> Const (Maybe (Some FortranVar)) CheckHoareEnv)
-> ((Maybe (Some FortranVar)
-> Const (Maybe (Some FortranVar)) (Maybe (Some FortranVar)))
-> ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
-> Getting
(Maybe (Some FortranVar)) CheckHoareEnv (Maybe (Some FortranVar))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index ScopeVars -> Lens' ScopeVars (Maybe (IxValue ScopeVars))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at (NamePair
argName NamePair -> Getting UniqueName NamePair UniqueName -> UniqueName
forall s a. s -> Getting a s a -> a
^. Getting UniqueName NamePair UniqueName
Lens' NamePair UniqueName
npUnique))
Bool
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
hasType (StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ ProgramUnit (Analysis (HoareAnnotation A))
-> HoareBackendError -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' ProgramUnit (Analysis (HoareAnnotation A))
pu (NamePair -> HoareBackendError
ArgWithoutDecl NamePair
argName)
([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
-> CheckHoareMut
([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
forall a. a -> StateT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Block (Analysis (HoareAnnotation A))]
restBody, [FortranAssignment]
initialAssignments)
addAuxVariables :: AnnotatedProgramUnit -> CheckHoareMut ()
addAuxVariables :: AnnotatedProgramUnit -> StateT CheckHoareEnv BackendAnalysis ()
addAuxVariables AnnotatedProgramUnit
apu =
[AuxDecl InnerHA]
-> (AuxDecl InnerHA -> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting [AuxDecl InnerHA] AnnotatedProgramUnit [AuxDecl InnerHA]
-> [AuxDecl InnerHA]
forall s a. s -> Getting a s a -> a
^. Getting [AuxDecl InnerHA] AnnotatedProgramUnit [AuxDecl InnerHA]
Lens' AnnotatedProgramUnit [AuxDecl InnerHA]
apuAuxDecls) ((AuxDecl InnerHA -> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ())
-> (AuxDecl InnerHA -> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ \AuxDecl InnerHA
auxDecl -> do
let nm :: String
nm = AuxDecl InnerHA
auxDecl AuxDecl InnerHA
-> Getting String (AuxDecl InnerHA) String -> String
forall s a. s -> Getting a s a -> a
^. Getting String (AuxDecl InnerHA) String
forall ann (f :: * -> *).
Functor f =>
(String -> f String) -> AuxDecl ann -> f (AuxDecl ann)
adName
UniqueName
uniqNm <- String -> StateT CheckHoareEnv BackendAnalysis UniqueName
forall {m :: * -> *}.
MonadState CheckHoareEnv m =>
String -> m UniqueName
uniqueAux String
nm
let srcNm :: SourceName
srcNm = String -> SourceName
SourceName String
nm
Map SourceName [UniqueName]
sourceToUnique <- Getting
(Map SourceName [UniqueName])
CheckHoareEnv
(Map SourceName [UniqueName])
-> StateT
CheckHoareEnv BackendAnalysis (Map SourceName [UniqueName])
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
(Map SourceName [UniqueName])
CheckHoareEnv
(Map SourceName [UniqueName])
Lens' CheckHoareEnv (Map SourceName [UniqueName])
heSourceToUnique
Bool
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SourceName
srcNm SourceName -> Map SourceName [UniqueName] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map SourceName [UniqueName]
sourceToUnique) (StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$
ProgramUnit (Analysis (HoareAnnotation A))
-> HoareBackendError -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting
(ProgramUnit (Analysis (HoareAnnotation A)))
AnnotatedProgramUnit
(ProgramUnit (Analysis (HoareAnnotation A)))
-> ProgramUnit (Analysis (HoareAnnotation A))
forall s a. s -> Getting a s a -> a
^. Getting
(ProgramUnit (Analysis (HoareAnnotation A)))
AnnotatedProgramUnit
(ProgramUnit (Analysis (HoareAnnotation A)))
Lens'
AnnotatedProgramUnit (ProgramUnit (Analysis (HoareAnnotation A)))
apuPU) (HoareBackendError -> StateT CheckHoareEnv BackendAnalysis ())
-> HoareBackendError -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ String -> HoareBackendError
AuxVarConflict String
nm
SomeType
ty <- ReaderT
CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
-> StateT CheckHoareEnv BackendAnalysis SomeType
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState (ReaderT
CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
-> StateT CheckHoareEnv BackendAnalysis SomeType)
-> (TypeSpec InnerHA
-> ReaderT
CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType)
-> TypeSpec InnerHA
-> StateT CheckHoareEnv BackendAnalysis SomeType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeInfo InnerHA
-> ReaderT
CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
TypeInfo (Analysis ann) -> m SomeType
tryTranslateTypeInfo (TypeInfo InnerHA
-> ReaderT
CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType)
-> (TypeSpec InnerHA -> TypeInfo InnerHA)
-> TypeSpec InnerHA
-> ReaderT
CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSpec InnerHA -> TypeInfo InnerHA
forall ann. TypeSpec ann -> TypeInfo ann
typeInfo (TypeSpec InnerHA -> StateT CheckHoareEnv BackendAnalysis SomeType)
-> TypeSpec InnerHA
-> StateT CheckHoareEnv BackendAnalysis SomeType
forall a b. (a -> b) -> a -> b
$ AuxDecl InnerHA
auxDecl AuxDecl InnerHA
-> Getting (TypeSpec InnerHA) (AuxDecl InnerHA) (TypeSpec InnerHA)
-> TypeSpec InnerHA
forall s a. s -> Getting a s a -> a
^. Getting (TypeSpec InnerHA) (AuxDecl InnerHA) (TypeSpec InnerHA)
forall ann1 ann2 (f :: * -> *).
Functor f =>
(TypeSpec ann1 -> f (TypeSpec ann2))
-> AuxDecl ann1 -> f (AuxDecl ann2)
adTy
(CheckHoareEnv -> CheckHoareEnv)
-> StateT CheckHoareEnv BackendAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CheckHoareEnv -> CheckHoareEnv)
-> StateT CheckHoareEnv BackendAnalysis ())
-> (CheckHoareEnv -> CheckHoareEnv)
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ NamePair -> SomeType -> CheckHoareEnv -> CheckHoareEnv
newVar (UniqueName -> SourceName -> NamePair
NamePair UniqueName
uniqNm SourceName
srcNm) SomeType
ty
where
uniqueAux :: String -> m UniqueName
uniqueAux String
nm = do
ScopeVars
varsInScope <- Getting ScopeVars CheckHoareEnv ScopeVars -> m ScopeVars
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting ScopeVars CheckHoareEnv ScopeVars
Lens' CheckHoareEnv ScopeVars
heVarsInScope
UniqueName -> m UniqueName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UniqueName -> m UniqueName) -> UniqueName -> m UniqueName
forall a b. (a -> b) -> a -> b
$ String -> UniqueName
UniqueName
(String -> UniqueName) -> ShowS -> String -> UniqueName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
forall a. HasCallStack => [a] -> a
head
([String] -> String) -> (String -> [String]) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile ((UniqueName -> ScopeVars -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` ScopeVars
varsInScope) (UniqueName -> Bool) -> (String -> UniqueName) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> UniqueName
UniqueName)
([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> String -> [String]
forall a. (a -> a) -> a -> [a]
iterate (Char
' ' Char -> ShowS
forall a. a -> [a] -> [a]
:)
(String -> UniqueName) -> String -> UniqueName
forall a b. (a -> b) -> a -> b
$ String
nm
readInitialBlocks :: [F.Block HA] -> CheckHoareMut ([F.Block HA], [FortranAssignment])
readInitialBlocks :: [Block (Analysis (HoareAnnotation A))]
-> CheckHoareMut
([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
readInitialBlocks = WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
[Block (Analysis (HoareAnnotation A))]
-> CheckHoareMut
([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
[Block (Analysis (HoareAnnotation A))]
-> CheckHoareMut
([Block (Analysis (HoareAnnotation A))], [FortranAssignment]))
-> ([Block (Analysis (HoareAnnotation A))]
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
[Block (Analysis (HoareAnnotation A))])
-> [Block (Analysis (HoareAnnotation A))]
-> CheckHoareMut
([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Block (Analysis (HoareAnnotation A))
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool)
-> [Block (Analysis (HoareAnnotation A))]
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
[Block (Analysis (HoareAnnotation A))]
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
(a -> m Bool) -> [a] -> m [a]
dropWhileM Block (Analysis (HoareAnnotation A))
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
readInitialBlock
where
readInitialBlock :: F.Block HA -> WriterT [FortranAssignment] CheckHoareMut Bool
readInitialBlock :: Block (Analysis (HoareAnnotation A))
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
readInitialBlock Block (Analysis (HoareAnnotation A))
bl = case Block (Analysis (HoareAnnotation A))
bl of
F.BlStatement Analysis (HoareAnnotation A)
_ SrcSpan
_ Maybe (Expression (Analysis (HoareAnnotation A)))
_ Statement (Analysis (HoareAnnotation A))
st ->
case Statement (Analysis (HoareAnnotation A))
st of
F.StDeclaration Analysis (HoareAnnotation A)
_ SrcSpan
_ TypeSpec (Analysis (HoareAnnotation A))
astTypeSpec Maybe (AList Attribute (Analysis (HoareAnnotation A)))
attrs AList Declarator (Analysis (HoareAnnotation A))
decls -> do
let topTypeInfo :: TypeInfo (Analysis (HoareAnnotation A))
topTypeInfo =
TypeSpec (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall ann. TypeSpec ann -> TypeInfo ann
typeInfo TypeSpec (Analysis (HoareAnnotation A))
astTypeSpec TypeInfo (Analysis (HoareAnnotation A))
-> (TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
forall a b. a -> (a -> b) -> b
&
(Maybe (AList Attribute (Analysis (HoareAnnotation A)))
-> Identity
(Maybe (AList Attribute (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A)))
forall ann (f :: * -> *).
Functor f =>
(Maybe (AList Attribute ann) -> f (Maybe (AList Attribute ann)))
-> TypeInfo ann -> f (TypeInfo ann)
tiAttributes ((Maybe (AList Attribute (Analysis (HoareAnnotation A)))
-> Identity
(Maybe (AList Attribute (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A))))
-> Maybe (AList Attribute (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (AList Attribute (Analysis (HoareAnnotation A)))
attrs
[(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))]
declVarsTis <- [Declarator (Analysis (HoareAnnotation A))]
-> (Declarator (Analysis (HoareAnnotation A))
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A)))))
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
[(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (AList Declarator (Analysis (HoareAnnotation A))
-> [Declarator (Analysis (HoareAnnotation A))]
forall (t :: * -> *) a. AList t a -> [t a]
F.aStrip AList Declarator (Analysis (HoareAnnotation A))
decls) ((Declarator (Analysis (HoareAnnotation A))
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A)))))
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
[(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))])
-> (Declarator (Analysis (HoareAnnotation A))
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A)))))
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
[(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))]
forall a b. (a -> b) -> a -> b
$ \case
F.Declarator Analysis (HoareAnnotation A)
_ SrcSpan
_ Expression (Analysis (HoareAnnotation A))
nameExp DeclaratorType (Analysis (HoareAnnotation A))
F.ScalarDecl Maybe (Expression (Analysis (HoareAnnotation A)))
declLength Maybe (Expression (Analysis (HoareAnnotation A)))
mInitialValue -> do
(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))
forall a.
a
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expression (Analysis (HoareAnnotation A))
nameExp,
TypeInfo (Analysis (HoareAnnotation A))
topTypeInfo
TypeInfo (Analysis (HoareAnnotation A))
-> (TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
forall a b. a -> (a -> b) -> b
& (Maybe (Expression (Analysis (HoareAnnotation A)))
-> Identity (Maybe (Expression (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A)))
forall ann (f :: * -> *).
Functor f =>
(Maybe (Expression ann) -> f (Maybe (Expression ann)))
-> TypeInfo ann -> f (TypeInfo ann)
tiDeclaratorLength ((Maybe (Expression (Analysis (HoareAnnotation A)))
-> Identity (Maybe (Expression (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A))))
-> Maybe (Expression (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (Expression (Analysis (HoareAnnotation A)))
declLength,
Maybe (Expression (Analysis (HoareAnnotation A)))
mInitialValue)
F.Declarator Analysis (HoareAnnotation A)
_ SrcSpan
_ Expression (Analysis (HoareAnnotation A))
nameExp (F.ArrayDecl AList DimensionDeclarator (Analysis (HoareAnnotation A))
declDims) Maybe (Expression (Analysis (HoareAnnotation A)))
declLength Maybe (Expression (Analysis (HoareAnnotation A)))
mInitialValue -> do
(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))
forall a.
a
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expression (Analysis (HoareAnnotation A))
nameExp,
TypeInfo (Analysis (HoareAnnotation A))
topTypeInfo
TypeInfo (Analysis (HoareAnnotation A))
-> (TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
forall a b. a -> (a -> b) -> b
& (Maybe (Expression (Analysis (HoareAnnotation A)))
-> Identity (Maybe (Expression (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A)))
forall ann (f :: * -> *).
Functor f =>
(Maybe (Expression ann) -> f (Maybe (Expression ann)))
-> TypeInfo ann -> f (TypeInfo ann)
tiDeclaratorLength ((Maybe (Expression (Analysis (HoareAnnotation A)))
-> Identity (Maybe (Expression (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A))))
-> Maybe (Expression (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (Expression (Analysis (HoareAnnotation A)))
declLength
TypeInfo (Analysis (HoareAnnotation A))
-> (TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
forall a b. a -> (a -> b) -> b
& (Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))
-> Identity
(Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A)))
forall ann (f :: * -> *).
Functor f =>
(Maybe (AList DimensionDeclarator ann)
-> f (Maybe (AList DimensionDeclarator ann)))
-> TypeInfo ann -> f (TypeInfo ann)
tiDimensionDeclarators ((Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))
-> Identity
(Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A))))
-> Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall s t a b. ASetter s t a b -> b -> s -> t
.~ AList DimensionDeclarator (Analysis (HoareAnnotation A))
-> Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))
forall a. a -> Maybe a
Just AList DimensionDeclarator (Analysis (HoareAnnotation A))
declDims,
Maybe (Expression (Analysis (HoareAnnotation A)))
mInitialValue)
[(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))]
-> ((Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))]
declVarsTis (((Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> ((Expression (Analysis (HoareAnnotation A)),
TypeInfo (Analysis (HoareAnnotation A)),
Maybe (Expression (Analysis (HoareAnnotation A))))
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ()
forall a b. (a -> b) -> a -> b
$ \(Expression (Analysis (HoareAnnotation A))
varNameExp, TypeInfo (Analysis (HoareAnnotation A))
varTypeInfo, Maybe (Expression (Analysis (HoareAnnotation A)))
mInitialValue) -> do
let varNames :: NamePair
varNames = Expression (Analysis (HoareAnnotation A)) -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair Expression (Analysis (HoareAnnotation A))
varNameExp
SomeType
varType <- ReaderT
CheckHoareEnv
(WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
SomeType
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) SomeType
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState (ReaderT
CheckHoareEnv
(WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
SomeType
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
SomeType)
-> ReaderT
CheckHoareEnv
(WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
SomeType
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) SomeType
forall a b. (a -> b) -> a -> b
$ TypeInfo (Analysis (HoareAnnotation A))
-> ReaderT
CheckHoareEnv
(WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
SomeType
forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
TypeInfo (Analysis ann) -> m SomeType
tryTranslateTypeInfo TypeInfo (Analysis (HoareAnnotation A))
varTypeInfo
(CheckHoareEnv -> CheckHoareEnv)
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CheckHoareEnv -> CheckHoareEnv)
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> (CheckHoareEnv -> CheckHoareEnv)
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ()
forall a b. (a -> b) -> a -> b
$ NamePair -> SomeType -> CheckHoareEnv -> CheckHoareEnv
newVar NamePair
varNames SomeType
varType
[FortranAssignment]
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ([FortranAssignment]
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
[FortranAssignment]
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expression (Analysis (HoareAnnotation A))
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
FortranAssignment)
-> [Expression (Analysis (HoareAnnotation A))]
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
[FortranAssignment]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (ReaderT
CheckHoareEnv
(WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
FortranAssignment
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
FortranAssignment
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState (ReaderT
CheckHoareEnv
(WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
FortranAssignment
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
FortranAssignment)
-> (Expression (Analysis (HoareAnnotation A))
-> ReaderT
CheckHoareEnv
(WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
FortranAssignment)
-> Expression (Analysis (HoareAnnotation A))
-> WriterT
[FortranAssignment]
(StateT CheckHoareEnv BackendAnalysis)
FortranAssignment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamePair
-> Expression (Analysis (HoareAnnotation A))
-> ReaderT
CheckHoareEnv
(WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
FortranAssignment
forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError Void m, MonadFail m) =>
NamePair -> Expression (Analysis ann) -> m FortranAssignment
simpleAssignment NamePair
varNames)
(Maybe (Expression (Analysis (HoareAnnotation A)))
-> [Expression (Analysis (HoareAnnotation A))]
forall a. Maybe a -> [a]
maybeToList Maybe (Expression (Analysis (HoareAnnotation A)))
mInitialValue)
Bool
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall a.
a
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
F.StImplicit Analysis (HoareAnnotation A)
_ SrcSpan
_ Maybe (AList ImpList (Analysis (HoareAnnotation A)))
Nothing -> do
Bool
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall a.
a
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
F.StImplicit Analysis (HoareAnnotation A)
_ SrcSpan
_ (Just AList ImpList (Analysis (HoareAnnotation A))
_) -> Block (Analysis (HoareAnnotation A))
-> HoareBackendError
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block (Analysis (HoareAnnotation A))
bl (Block (Analysis (HoareAnnotation A)) -> HoareBackendError
UnsupportedBlock Block (Analysis (HoareAnnotation A))
bl)
Statement (Analysis (HoareAnnotation A))
_ -> Bool
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall a.
a
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
F.BlComment{} | Maybe (PrimFormula InnerHA)
Nothing <- Block (Analysis (HoareAnnotation A)) -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation Block (Analysis (HoareAnnotation A))
bl -> Bool
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall a.
a
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Block (Analysis (HoareAnnotation A))
_ -> Bool
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall a.
a
-> WriterT
[FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
verifyVc :: (HoareBackendError -> CheckHoare Bool) -> MetaFormula Bool -> CheckHoare Bool
verifyVc :: (HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool)
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis Bool
verifyVc HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool
handle Prop (HFree' AllOps FortranVar) Bool
prop = do
let getSrProp :: HighRepr Bool -> SBool
getSrProp :: HighRepr Bool -> SBool
getSrProp (HRHigh SBool
x) = SBool
x
getSrProp (HRCore CoreRepr Bool
_) = String -> SBool
forall a. HasCallStack => String -> a
error String
"absurd"
let debug :: Bool
debug = Bool
False
cfg :: SMTConfig
cfg | Bool
debug = SMTConfig
defaultSMTCfg { verbose :: Bool
verbose = Bool
True, transcript :: Maybe String
transcript = String -> Maybe String
forall a. a -> Maybe a
Just String
"transcript.smt2" }
| Bool
otherwise = SMTConfig
defaultSMTCfg
PrimReprHandlers
env <- (CheckHoareEnv -> PrimReprHandlers)
-> ReaderT CheckHoareEnv BackendAnalysis PrimReprHandlers
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckHoareEnv -> PrimReprHandlers
forall r. HasPrimReprHandlers r => r -> PrimReprHandlers
primReprHandlers
let res :: Verifier FortranVar Bool
res = Query FortranVar SBool
-> VarEnv FortranVar -> Verifier FortranVar Bool
forall (v :: * -> *).
VerifiableVar v =>
Query v SBool -> VarEnv v -> Verifier v Bool
query (HighRepr Bool -> SBool
getSrProp (HighRepr Bool -> SBool)
-> Query FortranVar (HighRepr Bool) -> Query FortranVar SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr Bool)
-> PrimReprHandlers -> Query FortranVar (HighRepr Bool)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ((forall a.
Query FortranVar a
-> ReaderT PrimReprHandlers (Query FortranVar) a)
-> (forall a.
VarSym FortranVar a
-> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr a))
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr Bool)
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (m :: * -> *)
(k :: * -> *) b.
(HMonad expr, HTraversable expr, VerifiableVar v,
Exception (VerifierError v), HFoldableAt (Compose m k) expr,
HFoldableAt (Compose m k) LogicOp, Monad m) =>
(forall a. Query v a -> m a)
-> (forall a. VarSym v a -> m (k a)) -> Prop (expr v) b -> m (k b)
evalProp' Query FortranVar a -> ReaderT PrimReprHandlers (Query FortranVar) a
forall a.
Query FortranVar a -> ReaderT PrimReprHandlers (Query FortranVar) a
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT PrimReprHandlers m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (HighRepr a
-> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr a)
forall a. a -> ReaderT PrimReprHandlers (Query FortranVar) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HighRepr a
-> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr a))
-> (CoreRepr a -> HighRepr a)
-> CoreRepr a
-> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreRepr a -> HighRepr a
forall a. CoreRepr a -> HighRepr a
HRCore) Prop (HFree' AllOps FortranVar) Bool
prop) PrimReprHandlers
env) VarEnv FortranVar
PrimReprHandlers
env
Either (VerifierError FortranVar) Bool
res' <- IO (Either (VerifierError FortranVar) Bool)
-> ReaderT
CheckHoareEnv
BackendAnalysis
(Either (VerifierError FortranVar) Bool)
forall a. IO a -> ReaderT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either (VerifierError FortranVar) Bool)
-> ReaderT
CheckHoareEnv
BackendAnalysis
(Either (VerifierError FortranVar) Bool))
-> (Verifier FortranVar Bool
-> IO (Either (VerifierError FortranVar) Bool))
-> Verifier FortranVar Bool
-> ReaderT
CheckHoareEnv
BackendAnalysis
(Either (VerifierError FortranVar) Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig
-> Verifier FortranVar Bool
-> IO (Either (VerifierError FortranVar) Bool)
forall (v :: * -> *) a.
VerifiableVar v =>
SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)
runVerifierWith SMTConfig
cfg (Verifier FortranVar Bool
-> ReaderT
CheckHoareEnv
BackendAnalysis
(Either (VerifierError FortranVar) Bool))
-> Verifier FortranVar Bool
-> ReaderT
CheckHoareEnv
BackendAnalysis
(Either (VerifierError FortranVar) Bool)
forall a b. (a -> b) -> a -> b
$ Verifier FortranVar Bool
res
case Either (VerifierError FortranVar) Bool
res' of
Right Bool
b -> Bool -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall a. a -> ReaderT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
Left VerifierError FortranVar
e -> HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool
handle (VerifierError FortranVar -> HoareBackendError
VerifierError VerifierError FortranVar
e)
newtype GenM a = GenM (WriterT [MetaFormula Bool] CheckHoare a)
deriving
( (forall a b. (a -> b) -> GenM a -> GenM b)
-> (forall a b. a -> GenM b -> GenM a) -> Functor GenM
forall a b. a -> GenM b -> GenM a
forall a b. (a -> b) -> GenM a -> GenM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> GenM a -> GenM b
fmap :: forall a b. (a -> b) -> GenM a -> GenM b
$c<$ :: forall a b. a -> GenM b -> GenM a
<$ :: forall a b. a -> GenM b -> GenM a
Functor
, Functor GenM
Functor GenM
-> (forall a. a -> GenM a)
-> (forall a b. GenM (a -> b) -> GenM a -> GenM b)
-> (forall a b c. (a -> b -> c) -> GenM a -> GenM b -> GenM c)
-> (forall a b. GenM a -> GenM b -> GenM b)
-> (forall a b. GenM a -> GenM b -> GenM a)
-> Applicative GenM
forall a. a -> GenM a
forall a b. GenM a -> GenM b -> GenM a
forall a b. GenM a -> GenM b -> GenM b
forall a b. GenM (a -> b) -> GenM a -> GenM b
forall a b c. (a -> b -> c) -> GenM a -> GenM b -> GenM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> GenM a
pure :: forall a. a -> GenM a
$c<*> :: forall a b. GenM (a -> b) -> GenM a -> GenM b
<*> :: forall a b. GenM (a -> b) -> GenM a -> GenM b
$cliftA2 :: forall a b c. (a -> b -> c) -> GenM a -> GenM b -> GenM c
liftA2 :: forall a b c. (a -> b -> c) -> GenM a -> GenM b -> GenM c
$c*> :: forall a b. GenM a -> GenM b -> GenM b
*> :: forall a b. GenM a -> GenM b -> GenM b
$c<* :: forall a b. GenM a -> GenM b -> GenM a
<* :: forall a b. GenM a -> GenM b -> GenM a
Applicative
, Applicative GenM
Applicative GenM
-> (forall a b. GenM a -> (a -> GenM b) -> GenM b)
-> (forall a b. GenM a -> GenM b -> GenM b)
-> (forall a. a -> GenM a)
-> Monad GenM
forall a. a -> GenM a
forall a b. GenM a -> GenM b -> GenM b
forall a b. GenM a -> (a -> GenM b) -> GenM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. GenM a -> (a -> GenM b) -> GenM b
>>= :: forall a b. GenM a -> (a -> GenM b) -> GenM b
$c>> :: forall a b. GenM a -> GenM b -> GenM b
>> :: forall a b. GenM a -> GenM b -> GenM b
$creturn :: forall a. a -> GenM a
return :: forall a. a -> GenM a
Monad
, MonadReader CheckHoareEnv
, MonadWriter [MetaFormula Bool]
, MonadLogger HoareBackendError HoareBackendWarning
, MonadAnalysis HoareBackendError HoareBackendWarning
, Monad GenM
Monad GenM -> (forall a. String -> GenM a) -> MonadFail GenM
forall a. String -> GenM a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
$cfail :: forall a. String -> GenM a
fail :: forall a. String -> GenM a
MonadFail
)
runGenM :: GenM a -> CheckHoare (a, [MetaFormula Bool])
runGenM :: forall a.
GenM a -> CheckHoare (a, [Prop (HFree' AllOps FortranVar) Bool])
runGenM (GenM WriterT
[Prop (HFree' AllOps FortranVar) Bool]
(ReaderT CheckHoareEnv BackendAnalysis)
a
action) = WriterT
[Prop (HFree' AllOps FortranVar) Bool]
(ReaderT CheckHoareEnv BackendAnalysis)
a
-> ReaderT
CheckHoareEnv
BackendAnalysis
(a, [Prop (HFree' AllOps FortranVar) Bool])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT WriterT
[Prop (HFree' AllOps FortranVar) Bool]
(ReaderT CheckHoareEnv BackendAnalysis)
a
action
type FortranTriplet a = Triplet MetaExpr FortranVar a
genBody' :: [FortranAssignment] -> FortranTriplet [F.Block HA] -> GenM ()
genBody' :: [FortranAssignment]
-> (Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody' [FortranAssignment]
as (Prop (HFree' AllOps FortranVar) Bool
precond, Prop (HFree' AllOps FortranVar) Bool
postcond, [Block (Analysis (HoareAnnotation A))]
body) = do
let seqL :: AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
seqL = [FortranAssignment]
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
[Assignment expr var] -> AnnSeq expr var cmd
JustAssign [FortranAssignment]
as
AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
seqR <- [Block (Analysis (HoareAnnotation A))]
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
bodyToSequence [Block (Analysis (HoareAnnotation A))]
body
case AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
seqL AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
`joinAnnSeq` AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
seqR of
Just AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
x -> GenM [()] -> GenM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (GenM [()] -> GenM ()) -> GenM [()] -> GenM ()
forall a b. (a -> b) -> a -> b
$ (Triplet
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> GenM ())
-> Triplet
(HFree' AllOps)
FortranVar
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> GenM [()]
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (m :: * -> *) cmd
a.
(HMonad expr, MonadGenVCs expr v m, VerifiableVar v) =>
(Triplet expr v cmd -> m a)
-> Triplet expr v (AnnSeq expr v cmd) -> m [a]
sequenceVCs Triplet
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> GenM ()
genBlock (Prop (HFree' AllOps FortranVar) Bool
precond, Prop (HFree' AllOps FortranVar) Bool
postcond, AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
x)
Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
Nothing -> [Block (Analysis (HoareAnnotation A))]
-> HoareBackendError -> GenM ()
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' [Block (Analysis (HoareAnnotation A))]
body (HoareBackendError -> GenM ()) -> HoareBackendError -> GenM ()
forall a b. (a -> b) -> a -> b
$ AnnotationError -> HoareBackendError
AnnotationError AnnotationError
MissingSequenceAnn
genBody :: FortranTriplet [F.Block HA] -> GenM ()
genBody :: (Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody = [FortranAssignment]
-> (Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody' []
genBlock :: FortranTriplet (F.Block HA) -> GenM ()
genBlock :: Triplet
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> GenM ()
genBlock (Prop (HFree' AllOps FortranVar) Bool
precond, Prop (HFree' AllOps FortranVar) Bool
postcond, Block (Analysis (HoareAnnotation A))
bl) = do
case Block (Analysis (HoareAnnotation A))
bl of
F.BlIf Analysis (HoareAnnotation A)
_ SrcSpan
_ Maybe (Expression (Analysis (HoareAnnotation A)))
_ Maybe String
_ NonEmpty
(Expression (Analysis (HoareAnnotation A)),
[Block (Analysis (HoareAnnotation A))])
clauses Maybe [Block (Analysis (HoareAnnotation A))]
mElseBlock Maybe (Expression (Analysis (HoareAnnotation A)))
_ -> do
NonEmpty
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])
clauses' <- (((Expression (Analysis (HoareAnnotation A)),
[Block (Analysis (HoareAnnotation A))])
-> GenM
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))]))
-> NonEmpty
(Expression (Analysis (HoareAnnotation A)),
[Block (Analysis (HoareAnnotation A))])
-> GenM
(NonEmpty
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])))
-> NonEmpty
(Expression (Analysis (HoareAnnotation A)),
[Block (Analysis (HoareAnnotation A))])
-> ((Expression (Analysis (HoareAnnotation A)),
[Block (Analysis (HoareAnnotation A))])
-> GenM
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))]))
-> GenM
(NonEmpty
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))]))
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Expression (Analysis (HoareAnnotation A)),
[Block (Analysis (HoareAnnotation A))])
-> GenM
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))]))
-> NonEmpty
(Expression (Analysis (HoareAnnotation A)),
[Block (Analysis (HoareAnnotation A))])
-> GenM
(NonEmpty
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))]))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse NonEmpty
(Expression (Analysis (HoareAnnotation A)),
[Block (Analysis (HoareAnnotation A))])
clauses (((Expression (Analysis (HoareAnnotation A)),
[Block (Analysis (HoareAnnotation A))])
-> GenM
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))]))
-> GenM
(NonEmpty
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])))
-> ((Expression (Analysis (HoareAnnotation A)),
[Block (Analysis (HoareAnnotation A))])
-> GenM
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))]))
-> GenM
(NonEmpty
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))]))
forall a b. (a -> b) -> a -> b
$ \(Expression (Analysis (HoareAnnotation A))
cond, [Block (Analysis (HoareAnnotation A))]
block) ->
Expression (Analysis (HoareAnnotation A))
-> GenM (MetaExpr FortranVar Bool)
forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
Expression (Analysis ann) -> m (MetaExpr FortranVar Bool)
tryTranslateBoolExpr Expression (Analysis (HoareAnnotation A))
cond GenM (MetaExpr FortranVar Bool)
-> (MetaExpr FortranVar Bool
-> GenM
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))]))
-> GenM
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])
forall a b. GenM a -> (a -> GenM b) -> GenM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \MetaExpr FortranVar Bool
cond' -> (Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])
-> GenM
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])
forall a. a -> GenM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MetaExpr FortranVar Bool -> Maybe (MetaExpr FortranVar Bool)
forall a. a -> Maybe a
Just MetaExpr FortranVar Bool
cond', [Block (Analysis (HoareAnnotation A))]
block)
let clauses'' :: [(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])]
clauses'' = case Maybe [Block (Analysis (HoareAnnotation A))]
mElseBlock of
Maybe [Block (Analysis (HoareAnnotation A))]
Nothing ->
NonEmpty
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])
-> [(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])
clauses'
Just [Block (Analysis (HoareAnnotation A))]
elseBlock ->
NonEmpty
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])
-> [(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty
(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])
clauses' [(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])]
-> [(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])]
-> [(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])]
forall a. [a] -> [a] -> [a]
++ [(Maybe (MetaExpr FortranVar Bool)
forall a. Maybe a
Nothing, [Block (Analysis (HoareAnnotation A))]
elseBlock)]
((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))])
-> GenM ())
-> (MetaExpr FortranVar Bool
-> Prop (HFree' AllOps FortranVar) Bool)
-> Triplet
(HFree' AllOps)
FortranVar
[(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])]
-> GenM ()
forall (expr :: (* -> *) -> * -> *) (m :: * -> *) (v :: * -> *) cmd
cond.
(HMonad expr, Monad m) =>
(Triplet expr v cmd -> m ())
-> (cond -> Prop (expr v) Bool)
-> Triplet expr v [(Maybe cond, cmd)]
-> m ()
multiIfVCs (Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody MetaExpr FortranVar Bool -> Prop (HFree' AllOps FortranVar) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (Prop (HFree' AllOps FortranVar) Bool
precond, Prop (HFree' AllOps FortranVar) Bool
postcond, [(Maybe (MetaExpr FortranVar Bool),
[Block (Analysis (HoareAnnotation A))])]
clauses'')
F.BlDoWhile Analysis (HoareAnnotation A)
_ SrcSpan
_ Maybe (Expression (Analysis (HoareAnnotation A)))
_ Maybe String
_ Maybe (Expression (Analysis (HoareAnnotation A)))
_ Expression (Analysis (HoareAnnotation A))
cond [Block (Analysis (HoareAnnotation A))]
body Maybe (Expression (Analysis (HoareAnnotation A)))
_ -> do
PrimFormula InnerHA
primInvariant <-
case [Block (Analysis (HoareAnnotation A))]
body of
Block (Analysis (HoareAnnotation A))
b : [Block (Analysis (HoareAnnotation A))]
_ | Just (SodSpec (Specification SpecKind
SpecInvariant PrimFormula InnerHA
f))
<- Analysis (HoareAnnotation A) -> Maybe (SpecOrDecl InnerHA)
getAnnSod (Block (Analysis (HoareAnnotation A))
-> Analysis (HoareAnnotation A)
forall a. Block a -> a
forall (f :: * -> *) a. Annotated f => f a -> a
F.getAnnotation Block (Analysis (HoareAnnotation A))
b)
-> PrimFormula InnerHA -> GenM (PrimFormula InnerHA)
forall a. a -> GenM a
forall (m :: * -> *) a. Monad m => a -> m a
return PrimFormula InnerHA
f
[Block (Analysis (HoareAnnotation A))]
_ -> Block (Analysis (HoareAnnotation A))
-> HoareBackendError -> GenM (PrimFormula InnerHA)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block (Analysis (HoareAnnotation A))
bl (HoareBackendError -> GenM (PrimFormula InnerHA))
-> HoareBackendError -> GenM (PrimFormula InnerHA)
forall a b. (a -> b) -> a -> b
$ AnnotationError -> HoareBackendError
AnnotationError AnnotationError
MissingWhileInvariant
Prop (HFree' AllOps FortranVar) Bool
invariant <- [Block (Analysis (HoareAnnotation A))]
-> PrimFormula InnerHA
-> GenM (Prop (HFree' AllOps FortranVar) Bool)
forall o ann (m :: * -> *) w.
(Spanned o, ReportAnn (Analysis ann), Data ann,
MonadReader CheckHoareEnv m, MonadAnalysis HoareBackendError w m,
MonadFail m) =>
o
-> PrimFormula (Analysis ann)
-> m (Prop (HFree' AllOps FortranVar) Bool)
tryTranslateFormula [Block (Analysis (HoareAnnotation A))]
body PrimFormula InnerHA
primInvariant
MetaExpr FortranVar Bool
condExpr <- Expression (Analysis (HoareAnnotation A))
-> GenM (MetaExpr FortranVar Bool)
forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
Expression (Analysis ann) -> m (MetaExpr FortranVar Bool)
tryTranslateBoolExpr Expression (Analysis (HoareAnnotation A))
cond
((Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))])
-> GenM ())
-> (MetaExpr FortranVar Bool
-> Prop (HFree' AllOps FortranVar) Bool)
-> Prop (HFree' AllOps FortranVar) Bool
-> Triplet
(HFree' AllOps)
FortranVar
(MetaExpr FortranVar Bool, [Block (Analysis (HoareAnnotation A))])
-> GenM ()
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (m :: * -> *) cmd
cond.
(HMonad expr, MonadGenVCs expr v m) =>
(Triplet expr v cmd -> m ())
-> (cond -> Prop (expr v) Bool)
-> Prop (expr v) Bool
-> Triplet expr v (cond, cmd)
-> m ()
whileVCs (Prop (HFree' AllOps FortranVar) Bool,
Prop (HFree' AllOps FortranVar) Bool,
[Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody MetaExpr FortranVar Bool -> Prop (HFree' AllOps FortranVar) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr Prop (HFree' AllOps FortranVar) Bool
invariant (Prop (HFree' AllOps FortranVar) Bool
precond, Prop (HFree' AllOps FortranVar) Bool
postcond, (MetaExpr FortranVar Bool
condExpr, [Block (Analysis (HoareAnnotation A))]
body))
F.BlComment Analysis (HoareAnnotation A)
_ SrcSpan
_ Comment (Analysis (HoareAnnotation A))
_ -> () -> GenM ()
forall a. a -> GenM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Block (Analysis (HoareAnnotation A))
_ -> Block (Analysis (HoareAnnotation A))
-> HoareBackendError -> GenM ()
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block (Analysis (HoareAnnotation A))
bl (HoareBackendError -> GenM ()) -> HoareBackendError -> GenM ()
forall a b. (a -> b) -> a -> b
$ Block (Analysis (HoareAnnotation A)) -> HoareBackendError
UnsupportedBlock Block (Analysis (HoareAnnotation A))
bl
bodyToSequence :: [F.Block HA] -> GenM (AnnSeq MetaExpr FortranVar (F.Block HA))
bodyToSequence :: [Block (Analysis (HoareAnnotation A))]
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
bodyToSequence [Block (Analysis (HoareAnnotation A))]
blocks = do
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Block (Analysis (HoareAnnotation A))
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> [Block (Analysis (HoareAnnotation A))]
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Block (Analysis (HoareAnnotation A))
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
combineBlockSequence AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
emptyAnnSeq [Block (Analysis (HoareAnnotation A))]
blocks
combineBlockSequence
:: AnnSeq MetaExpr FortranVar (F.Block HA)
-> F.Block HA
-> GenM (AnnSeq MetaExpr FortranVar (F.Block HA))
combineBlockSequence :: AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Block (Analysis (HoareAnnotation A))
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
combineBlockSequence AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
prevSeq Block (Analysis (HoareAnnotation A))
bl = do
AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
blSeq <- Block (Analysis (HoareAnnotation A))
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
blockToSequence Block (Analysis (HoareAnnotation A))
bl
case AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
prevSeq AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
`joinAnnSeq` AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
blSeq of
Just AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
r -> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a. a -> GenM a
forall (m :: * -> *) a. Monad m => a -> m a
return AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
r
Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
Nothing -> Block (Analysis (HoareAnnotation A))
-> HoareBackendError
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block (Analysis (HoareAnnotation A))
bl (HoareBackendError
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
-> HoareBackendError
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a b. (a -> b) -> a -> b
$ AnnotationError -> HoareBackendError
AnnotationError AnnotationError
MissingSequenceAnn
blockToSequence :: F.Block HA -> GenM (AnnSeq MetaExpr FortranVar (F.Block HA))
blockToSequence :: Block (Analysis (HoareAnnotation A))
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
blockToSequence Block (Analysis (HoareAnnotation A))
bl = do
[GenM
(Maybe
(AnnSeq
(HFree' AllOps)
FortranVar
(Block (Analysis (HoareAnnotation A)))))]
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a. [GenM (Maybe a)] -> GenM a
chooseFrom [GenM
(Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
assignment, GenM
(Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
sequenceSpec, GenM
(Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
other]
where
assignment :: GenM
(Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
assignment = (FortranAssignment
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> Maybe FortranAssignment
-> Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([FortranAssignment]
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
[Assignment expr var] -> AnnSeq expr var cmd
JustAssign ([FortranAssignment]
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> (FortranAssignment -> [FortranAssignment])
-> FortranAssignment
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FortranAssignment -> [FortranAssignment] -> [FortranAssignment]
forall a. a -> [a] -> [a]
: [])) (Maybe FortranAssignment
-> Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
-> GenM (Maybe FortranAssignment)
-> GenM
(Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Block (Analysis (HoareAnnotation A))
-> GenM (Maybe FortranAssignment)
forall (m :: * -> *).
(MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError Void m, MonadFail m) =>
Block (Analysis (HoareAnnotation A)) -> m (Maybe FortranAssignment)
tryBlockToAssignment Block (Analysis (HoareAnnotation A))
bl
sequenceSpec :: GenM
(Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
sequenceSpec =
(PrimFormula InnerHA
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
-> Maybe (PrimFormula InnerHA)
-> GenM
(Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse
((Prop (HFree' AllOps FortranVar) Bool
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> GenM (Prop (HFree' AllOps FortranVar) Bool)
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a b. (a -> b) -> GenM a -> GenM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop (HFree' AllOps FortranVar) Bool
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
Prop (expr var) Bool -> AnnSeq expr var cmd
propAnnSeq (GenM (Prop (HFree' AllOps FortranVar) Bool)
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
-> (PrimFormula InnerHA
-> GenM (Prop (HFree' AllOps FortranVar) Bool))
-> PrimFormula InnerHA
-> GenM
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block (Analysis (HoareAnnotation A))
-> PrimFormula InnerHA
-> GenM (Prop (HFree' AllOps FortranVar) Bool)
forall o ann (m :: * -> *) w.
(Spanned o, ReportAnn (Analysis ann), Data ann,
MonadReader CheckHoareEnv m, MonadAnalysis HoareBackendError w m,
MonadFail m) =>
o
-> PrimFormula (Analysis ann)
-> m (Prop (HFree' AllOps FortranVar) Bool)
tryTranslateFormula Block (Analysis (HoareAnnotation A))
bl)
(Block (Analysis (HoareAnnotation A)) -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation Block (Analysis (HoareAnnotation A))
bl)
other :: GenM
(Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
other = Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> GenM
(Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
forall a. a -> GenM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> GenM
(Maybe
(AnnSeq
(HFree' AllOps)
FortranVar
(Block (Analysis (HoareAnnotation A))))))
-> Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> GenM
(Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
forall a b. (a -> b) -> a -> b
$ case Block (Analysis (HoareAnnotation A))
bl of
F.BlComment{} -> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a. a -> Maybe a
Just AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
emptyAnnSeq
Block (Analysis (HoareAnnotation A))
_ -> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a. a -> Maybe a
Just (AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Maybe
(AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a b. (a -> b) -> a -> b
$ Block (Analysis (HoareAnnotation A))
-> AnnSeq
(HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
forall cmd (expr :: (* -> *) -> * -> *) (var :: * -> *).
cmd -> AnnSeq expr var cmd
cmdAnnSeq Block (Analysis (HoareAnnotation A))
bl
chooseFrom :: [GenM (Maybe a)] -> GenM a
chooseFrom :: forall a. [GenM (Maybe a)] -> GenM a
chooseFrom =
(GenM (Maybe a) -> (Maybe a -> GenM a) -> GenM a
forall a b. GenM a -> (a -> GenM b) -> GenM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GenM a -> Maybe a -> GenM a
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
m a -> Maybe a -> m a
fromMaybeM (Block (Analysis (HoareAnnotation A)) -> HoareBackendError -> GenM a
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block (Analysis (HoareAnnotation A))
bl (HoareBackendError -> GenM a) -> HoareBackendError -> GenM a
forall a b. (a -> b) -> a -> b
$ AnnotationError -> HoareBackendError
AnnotationError AnnotationError
MissingSequenceAnn)) (GenM (Maybe a) -> GenM a)
-> ([GenM (Maybe a)] -> GenM (Maybe a))
-> [GenM (Maybe a)]
-> GenM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
MaybeT GenM a -> GenM (Maybe a)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT GenM a -> GenM (Maybe a))
-> ([GenM (Maybe a)] -> MaybeT GenM a)
-> [GenM (Maybe a)]
-> GenM (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [MaybeT GenM a] -> MaybeT GenM a
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([MaybeT GenM a] -> MaybeT GenM a)
-> ([GenM (Maybe a)] -> [MaybeT GenM a])
-> [GenM (Maybe a)]
-> MaybeT GenM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenM (Maybe a) -> MaybeT GenM a)
-> [GenM (Maybe a)] -> [MaybeT GenM a]
forall a b. (a -> b) -> [a] -> [b]
map GenM (Maybe a) -> MaybeT GenM a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT
getBlockSeqAnnotation :: F.Block HA -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation :: Block (Analysis (HoareAnnotation A)) -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation = Getting
(First (PrimFormula InnerHA))
(Block (Analysis (HoareAnnotation A)))
(PrimFormula InnerHA)
-> Block (Analysis (HoareAnnotation A))
-> Maybe (PrimFormula InnerHA)
forall s (m :: * -> *) a.
MonadReader s m =>
Getting (First a) s a -> m (Maybe a)
preview ((Block (Analysis (HoareAnnotation A))
-> Analysis (HoareAnnotation A))
-> (Analysis (HoareAnnotation A)
-> Const
(First (PrimFormula InnerHA)) (Analysis (HoareAnnotation A)))
-> Block (Analysis (HoareAnnotation A))
-> Const
(First (PrimFormula InnerHA))
(Block (Analysis (HoareAnnotation A)))
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to Block (Analysis (HoareAnnotation A))
-> Analysis (HoareAnnotation A)
forall a. Block a -> a
forall (f :: * -> *) a. Annotated f => f a -> a
F.getAnnotation ((Analysis (HoareAnnotation A)
-> Const
(First (PrimFormula InnerHA)) (Analysis (HoareAnnotation A)))
-> Block (Analysis (HoareAnnotation A))
-> Const
(First (PrimFormula InnerHA))
(Block (Analysis (HoareAnnotation A))))
-> ((PrimFormula InnerHA
-> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> Analysis (HoareAnnotation A)
-> Const
(First (PrimFormula InnerHA)) (Analysis (HoareAnnotation A)))
-> Getting
(First (PrimFormula InnerHA))
(Block (Analysis (HoareAnnotation A)))
(PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Analysis (HoareAnnotation A) -> Maybe (SpecOrDecl InnerHA))
-> Optic'
(->)
(Const (First (PrimFormula InnerHA)))
(Analysis (HoareAnnotation A))
(Maybe (SpecOrDecl InnerHA))
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to Analysis (HoareAnnotation A) -> Maybe (SpecOrDecl InnerHA)
getAnnSod Optic'
(->)
(Const (First (PrimFormula InnerHA)))
(Analysis (HoareAnnotation A))
(Maybe (SpecOrDecl InnerHA))
-> ((PrimFormula InnerHA
-> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> Maybe (SpecOrDecl InnerHA)
-> Const
(First (PrimFormula InnerHA)) (Maybe (SpecOrDecl InnerHA)))
-> (PrimFormula InnerHA
-> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> Analysis (HoareAnnotation A)
-> Const
(First (PrimFormula InnerHA)) (Analysis (HoareAnnotation A))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecOrDecl InnerHA
-> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA))
-> Maybe (SpecOrDecl InnerHA)
-> Const (First (PrimFormula InnerHA)) (Maybe (SpecOrDecl InnerHA))
forall a b (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe b))
_Just ((SpecOrDecl InnerHA
-> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA))
-> Maybe (SpecOrDecl InnerHA)
-> Const
(First (PrimFormula InnerHA)) (Maybe (SpecOrDecl InnerHA)))
-> ((PrimFormula InnerHA
-> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> SpecOrDecl InnerHA
-> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA))
-> (PrimFormula InnerHA
-> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> Maybe (SpecOrDecl InnerHA)
-> Const (First (PrimFormula InnerHA)) (Maybe (SpecOrDecl InnerHA))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Specification (PrimFormula InnerHA)
-> Const
(First (PrimFormula InnerHA))
(Specification (PrimFormula InnerHA)))
-> SpecOrDecl InnerHA
-> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA)
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (PrimSpec ann) (f (PrimSpec ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodSpec ((Specification (PrimFormula InnerHA)
-> Const
(First (PrimFormula InnerHA))
(Specification (PrimFormula InnerHA)))
-> SpecOrDecl InnerHA
-> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA))
-> ((PrimFormula InnerHA
-> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> Specification (PrimFormula InnerHA)
-> Const
(First (PrimFormula InnerHA))
(Specification (PrimFormula InnerHA)))
-> (PrimFormula InnerHA
-> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> SpecOrDecl InnerHA
-> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula InnerHA
-> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> Specification (PrimFormula InnerHA)
-> Const
(First (PrimFormula InnerHA)) (Specification (PrimFormula InnerHA))
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f a) -> p (Specification a) (f (Specification a))
_SpecSeq)
tryBlockToAssignment
:: ( MonadReader CheckHoareEnv m
, MonadAnalysis HoareBackendError HoareBackendWarning m
, MonadFail m
)
=> F.Block HA -> m (Maybe FortranAssignment)
tryBlockToAssignment :: forall (m :: * -> *).
(MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError Void m, MonadFail m) =>
Block (Analysis (HoareAnnotation A)) -> m (Maybe FortranAssignment)
tryBlockToAssignment Block (Analysis (HoareAnnotation A))
bl = do
case Block (Analysis (HoareAnnotation A))
bl of
F.BlStatement Analysis (HoareAnnotation A)
_ SrcSpan
_ Maybe (Expression (Analysis (HoareAnnotation A)))
_ stAst :: Statement (Analysis (HoareAnnotation A))
stAst@(F.StExpressionAssign Analysis (HoareAnnotation A)
_ SrcSpan
_ Expression (Analysis (HoareAnnotation A))
lexp Expression (Analysis (HoareAnnotation A))
rvalue) ->
FortranAssignment -> Maybe FortranAssignment
forall a. a -> Maybe a
Just (FortranAssignment -> Maybe FortranAssignment)
-> m FortranAssignment -> m (Maybe FortranAssignment)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
LValue (Analysis (HoareAnnotation A))
lvalue <- m (LValue (Analysis (HoareAnnotation A)))
-> Maybe (LValue (Analysis (HoareAnnotation A)))
-> m (LValue (Analysis (HoareAnnotation A)))
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
m a -> Maybe a -> m a
fromMaybeM (Expression (Analysis (HoareAnnotation A))
-> HoareBackendError -> m (LValue (Analysis (HoareAnnotation A)))
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis (HoareAnnotation A))
lexp HoareBackendError
NonLValueAssignment)
(Expression (Analysis (HoareAnnotation A))
-> Maybe (LValue (Analysis (HoareAnnotation A)))
forall a. Expression a -> Maybe (LValue a)
F.toLValue Expression (Analysis (HoareAnnotation A))
lexp)
case LValue (Analysis (HoareAnnotation A))
lvalue of
F.LvSimpleVar {} -> NamePair
-> Expression (Analysis (HoareAnnotation A)) -> m FortranAssignment
forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError Void m, MonadFail m) =>
NamePair -> Expression (Analysis ann) -> m FortranAssignment
simpleAssignment (Expression (Analysis (HoareAnnotation A)) -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair Expression (Analysis (HoareAnnotation A))
lexp) Expression (Analysis (HoareAnnotation A))
rvalue
F.LvSubscript Analysis (HoareAnnotation A)
_ SrcSpan
_ lvar :: LValue (Analysis (HoareAnnotation A))
lvar@(F.LvSimpleVar {}) AList Index (Analysis (HoareAnnotation A))
ixs ->
case AList Index (Analysis (HoareAnnotation A))
ixs of
F.AList Analysis (HoareAnnotation A)
_ SrcSpan
_ [F.IxSingle Analysis (HoareAnnotation A)
_ SrcSpan
_ Maybe String
_ Expression (Analysis (HoareAnnotation A))
ixExpr] ->
NamePair
-> Expression (Analysis (HoareAnnotation A))
-> Expression (Analysis (HoareAnnotation A))
-> m FortranAssignment
forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError Void m, MonadFail m) =>
NamePair
-> Expression (Analysis ann)
-> Expression (Analysis ann)
-> m FortranAssignment
arrayAssignment (LValue (Analysis (HoareAnnotation A)) -> NamePair
forall x. LValue (Analysis x) -> NamePair
lvVarNames LValue (Analysis (HoareAnnotation A))
lvar) Expression (Analysis (HoareAnnotation A))
ixExpr Expression (Analysis (HoareAnnotation A))
rvalue
AList Index (Analysis (HoareAnnotation A))
_ -> AList Index (Analysis (HoareAnnotation A))
-> HoareBackendError -> m FortranAssignment
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' AList Index (Analysis (HoareAnnotation A))
ixs (HoareBackendError -> m FortranAssignment)
-> HoareBackendError -> m FortranAssignment
forall a b. (a -> b) -> a -> b
$
Text -> HoareBackendError
UnsupportedAssignment Text
"only simple indices are supported for now"
LValue (Analysis (HoareAnnotation A))
_ -> Statement (Analysis (HoareAnnotation A))
-> HoareBackendError -> m FortranAssignment
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Statement (Analysis (HoareAnnotation A))
stAst (HoareBackendError -> m FortranAssignment)
-> HoareBackendError -> m FortranAssignment
forall a b. (a -> b) -> a -> b
$
Text -> HoareBackendError
UnsupportedAssignment Text
"complex assignment"
Block (Analysis (HoareAnnotation A))
_ -> Maybe FortranAssignment -> m (Maybe FortranAssignment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FortranAssignment
forall a. Maybe a
Nothing
simpleAssignment
:: ( ReportAnn (F.Analysis ann)
, MonadReader CheckHoareEnv m
, MonadAnalysis HoareBackendError HoareBackendWarning m
, MonadFail m
)
=> NamePair
-> F.Expression (F.Analysis ann)
-> m FortranAssignment
simpleAssignment :: forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError Void m, MonadFail m) =>
NamePair -> Expression (Analysis ann) -> m FortranAssignment
simpleAssignment NamePair
nm Expression (Analysis ann)
rvalAst = do
Some varV :: FortranVar a
varV@(FortranVar D a
varD NamePair
_) <- Expression (Analysis ann) -> NamePair -> m (Some FortranVar)
forall a (m :: * -> *).
(Spanned a, MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError Void m, MonadFail m) =>
a -> NamePair -> m (Some FortranVar)
varFromScope Expression (Analysis ann)
rvalAst NamePair
nm
case D a
varD of
DPrim Prim p k a1
_ -> do
MetaExpr FortranVar a
rvalExpr <- D a -> Expression (Analysis ann) -> m (MetaExpr FortranVar a)
forall ann (m :: * -> *) w a.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
D a -> Expression (Analysis ann) -> m (MetaExpr FortranVar a)
tryTranslateCoerceExpr D a
varD Expression (Analysis ann)
rvalAst
FortranAssignment -> m FortranAssignment
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FortranVar a -> MetaExpr FortranVar a -> FortranAssignment
forall {k} (var :: k -> *) (a :: k) (expr :: (k -> *) -> k -> *).
var a -> expr var a -> Assignment expr var
Assignment FortranVar a
varV MetaExpr FortranVar a
rvalExpr)
D a
_ -> Expression (Analysis ann)
-> HoareBackendError -> m FortranAssignment
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis ann)
rvalAst (HoareBackendError -> m FortranAssignment)
-> HoareBackendError -> m FortranAssignment
forall a b. (a -> b) -> a -> b
$
Text -> SomeType -> HoareBackendError
WrongAssignmentType
Text
"primitive value (others unsupported for now)"
(D a -> SomeType
forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some D a
varD)
arrayAssignment
:: ( ReportAnn (F.Analysis ann)
, MonadReader CheckHoareEnv m
, MonadAnalysis HoareBackendError HoareBackendWarning m
, MonadFail m
)
=> NamePair
-> F.Expression (F.Analysis ann)
-> F.Expression (F.Analysis ann)
-> m FortranAssignment
arrayAssignment :: forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError Void m, MonadFail m) =>
NamePair
-> Expression (Analysis ann)
-> Expression (Analysis ann)
-> m FortranAssignment
arrayAssignment NamePair
arrName Expression (Analysis ann)
ixAst Expression (Analysis ann)
rvalAst = do
Some varV :: FortranVar a
varV@(FortranVar D a
varD NamePair
_) <- Expression (Analysis ann) -> NamePair -> m (Some FortranVar)
forall a (m :: * -> *).
(Spanned a, MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError Void m, MonadFail m) =>
a -> NamePair -> m (Some FortranVar)
varFromScope Expression (Analysis ann)
rvalAst NamePair
arrName
case D a
varD of
DArray Index i
ixIndex ArrValue a1
valAv -> do
let ixD :: D i
ixD = Index i -> D i
forall i. Index i -> D i
dIndex Index i
ixIndex
valD :: D a1
valD = ArrValue a1 -> D a1
forall a. ArrValue a -> D a
dArrValue ArrValue a1
valAv
MetaExpr FortranVar i
ixExpr <- HFree CoreOp FortranVar i -> MetaExpr FortranVar i
forall (op :: (* -> *) -> * -> *) (v :: * -> *) a.
(ChooseOp op AllOps, HTraversable op) =>
HFree op v a -> MetaExpr v a
intoMetaExpr (HFree CoreOp FortranVar i -> MetaExpr FortranVar i)
-> m (HFree CoreOp FortranVar i) -> m (MetaExpr FortranVar i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> D i -> Expression (Analysis ann) -> m (HFree CoreOp FortranVar i)
forall ann (m :: * -> *) w a.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
D a -> Expression (Analysis ann) -> m (FortranExpr a)
tryTranslateExpr D i
ixD Expression (Analysis ann)
ixAst
MetaExpr FortranVar a1
rvalExpr <- HFree CoreOp FortranVar a1 -> MetaExpr FortranVar a1
forall (op :: (* -> *) -> * -> *) (v :: * -> *) a.
(ChooseOp op AllOps, HTraversable op) =>
HFree op v a -> MetaExpr v a
intoMetaExpr (HFree CoreOp FortranVar a1 -> MetaExpr FortranVar a1)
-> m (HFree CoreOp FortranVar a1) -> m (MetaExpr FortranVar a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> D a1 -> Expression (Analysis ann) -> m (HFree CoreOp FortranVar a1)
forall ann (m :: * -> *) w a.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
D a -> Expression (Analysis ann) -> m (FortranExpr a)
tryTranslateExpr D a1
valD Expression (Analysis ann)
rvalAst
let arrExpr :: HFree' AllOps FortranVar a
arrExpr = HFree (OpChoice AllOps) FortranVar a -> HFree' AllOps FortranVar a
forall (ops :: [(* -> *) -> * -> *]) (v :: * -> *) a.
HFree (OpChoice ops) v a -> HFree' ops v a
HFree' (HFree (OpChoice AllOps) FortranVar a
-> HFree' AllOps FortranVar a)
-> HFree (OpChoice AllOps) FortranVar a
-> HFree' AllOps FortranVar a
forall a b. (a -> b) -> a -> b
$ FortranVar a -> HFree (OpChoice AllOps) FortranVar a
forall {k} (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
t a -> HFree h t a
HPure FortranVar a
varV
arrExpr' :: HFree' AllOps FortranVar (Array i a1)
arrExpr' = MetaOp (HFree' AllOps FortranVar) (Array i a1)
-> HFree' AllOps FortranVar (Array i a1)
forall (op :: (* -> *) -> * -> *) (ops :: [(* -> *) -> * -> *])
(v :: * -> *) a.
(HFunctor op, HFunctor (OpChoice ops), ChooseOp op ops) =>
op (HFree' ops v) a -> HFree' ops v a
hwrap' (MetaOp (HFree' AllOps FortranVar) (Array i a1)
-> HFree' AllOps FortranVar (Array i a1))
-> MetaOp (HFree' AllOps FortranVar) (Array i a1)
-> HFree' AllOps FortranVar (Array i a1)
forall a b. (a -> b) -> a -> b
$ D (Array i a1)
-> HFree' AllOps FortranVar (Array i a1)
-> MetaExpr FortranVar i
-> MetaExpr FortranVar a1
-> MetaOp (HFree' AllOps FortranVar) (Array i a1)
forall i v (t :: * -> *).
D (Array i v)
-> t (Array i v) -> t i -> t v -> MetaOp t (Array i v)
MopWriteArr D a
D (Array i a1)
varD HFree' AllOps FortranVar a
HFree' AllOps FortranVar (Array i a1)
arrExpr MetaExpr FortranVar i
ixExpr MetaExpr FortranVar a1
rvalExpr
FortranAssignment -> m FortranAssignment
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FortranVar a -> HFree' AllOps FortranVar a -> FortranAssignment
forall {k} (var :: k -> *) (a :: k) (expr :: (k -> *) -> k -> *).
var a -> expr var a -> Assignment expr var
Assignment FortranVar a
varV HFree' AllOps FortranVar a
HFree' AllOps FortranVar (Array i a1)
arrExpr')
D a
_ -> Expression (Analysis ann)
-> HoareBackendError -> m FortranAssignment
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis ann)
rvalAst (HoareBackendError -> m FortranAssignment)
-> HoareBackendError -> m FortranAssignment
forall a b. (a -> b) -> a -> b
$ Text -> SomeType -> HoareBackendError
WrongAssignmentType Text
"array type" (D a -> SomeType
forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some D a
varD)
varFromScope
:: ( F.Spanned a
, MonadReader CheckHoareEnv m
, MonadAnalysis HoareBackendError HoareBackendWarning m
, MonadFail m
)
=> a -> NamePair -> m SomeVar
varFromScope :: forall a (m :: * -> *).
(Spanned a, MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError Void m, MonadFail m) =>
a -> NamePair -> m (Some FortranVar)
varFromScope a
loc NamePair
np = do
let uniq :: UniqueName
uniq = NamePair
np NamePair -> Getting UniqueName NamePair UniqueName -> UniqueName
forall s a. s -> Getting a s a -> a
^. Getting UniqueName NamePair UniqueName
Lens' NamePair UniqueName
npUnique
Maybe (Some FortranVar)
mscoped <- Getting
(Maybe (Some FortranVar)) CheckHoareEnv (Maybe (Some FortranVar))
-> m (Maybe (Some FortranVar))
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
-> CheckHoareEnv -> Const (Maybe (Some FortranVar)) CheckHoareEnv
Lens' CheckHoareEnv ScopeVars
heVarsInScope ((ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
-> CheckHoareEnv -> Const (Maybe (Some FortranVar)) CheckHoareEnv)
-> ((Maybe (Some FortranVar)
-> Const (Maybe (Some FortranVar)) (Maybe (Some FortranVar)))
-> ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
-> Getting
(Maybe (Some FortranVar)) CheckHoareEnv (Maybe (Some FortranVar))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index ScopeVars -> Lens' ScopeVars (Maybe (IxValue ScopeVars))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index ScopeVars
UniqueName
uniq)
case Maybe (Some FortranVar)
mscoped of
Just Some FortranVar
v -> Some FortranVar -> m (Some FortranVar)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Some FortranVar
v
Maybe (Some FortranVar)
Nothing -> a -> HoareBackendError -> m (Some FortranVar)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' a
loc (HoareBackendError -> m (Some FortranVar))
-> HoareBackendError -> m (Some FortranVar)
forall a b. (a -> b) -> a -> b
$ NamePair -> HoareBackendError
AssignVarNotInScope NamePair
np
class Show a => ReportAnn a where
fromTranslateError :: proxy a -> TranslateError -> HoareBackendError
instance ReportAnn HA where fromTranslateError :: forall (proxy :: * -> *).
proxy (Analysis (HoareAnnotation A))
-> TranslateError -> HoareBackendError
fromTranslateError proxy (Analysis (HoareAnnotation A))
_ = TranslateError -> HoareBackendError
TranslateErrorSrc
instance ReportAnn InnerHA where fromTranslateError :: forall (proxy :: * -> *).
proxy InnerHA -> TranslateError -> HoareBackendError
fromTranslateError proxy InnerHA
_ = TranslateError -> HoareBackendError
TranslateErrorAnn
doTranslate
:: (MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m)
=> (HoareBackendError -> m a) -> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate :: forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate HoareBackendError -> m a
handle f ann -> TranslateT m a
trans f ann
ast = do
TranslateEnv
env <- (CheckHoareEnv -> TranslateEnv) -> m TranslateEnv
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckHoareEnv -> TranslateEnv
toTranslateEnv
Either TranslateError a
transResult <- TranslateT m a -> TranslateEnv -> m (Either TranslateError a)
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
TranslateT m a -> TranslateEnv -> m (Either TranslateError a)
runTranslateT (f ann -> TranslateT m a
trans f ann
ast) TranslateEnv
env
case Either TranslateError a
transResult of
Right a
x -> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
Left TranslateError
err -> HoareBackendError -> m a
handle (f ann -> TranslateError -> HoareBackendError
forall a (proxy :: * -> *).
ReportAnn a =>
proxy a -> TranslateError -> HoareBackendError
forall (proxy :: * -> *).
proxy ann -> TranslateError -> HoareBackendError
fromTranslateError f ann
ast TranslateError
err)
toTranslateEnv :: CheckHoareEnv -> TranslateEnv
toTranslateEnv :: CheckHoareEnv -> TranslateEnv
toTranslateEnv CheckHoareEnv
env =
TranslateEnv
defaultTranslateEnv
TranslateEnv -> (TranslateEnv -> TranslateEnv) -> TranslateEnv
forall a b. a -> (a -> b) -> b
& (Bool -> Identity Bool) -> TranslateEnv -> Identity TranslateEnv
Lens' TranslateEnv Bool
teImplicitVars ((Bool -> Identity Bool) -> TranslateEnv -> Identity TranslateEnv)
-> Bool -> TranslateEnv -> TranslateEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ CheckHoareEnv
env CheckHoareEnv -> Getting Bool CheckHoareEnv Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool CheckHoareEnv Bool
Lens' CheckHoareEnv Bool
heImplicitVars
TranslateEnv -> (TranslateEnv -> TranslateEnv) -> TranslateEnv
forall a b. a -> (a -> b) -> b
& (ScopeVars -> Identity ScopeVars)
-> TranslateEnv -> Identity TranslateEnv
Lens' TranslateEnv ScopeVars
teVarsInScope ((ScopeVars -> Identity ScopeVars)
-> TranslateEnv -> Identity TranslateEnv)
-> ScopeVars -> TranslateEnv -> TranslateEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ CheckHoareEnv
env CheckHoareEnv
-> Getting ScopeVars CheckHoareEnv ScopeVars -> ScopeVars
forall s a. s -> Getting a s a -> a
^. Getting ScopeVars CheckHoareEnv ScopeVars
Lens' CheckHoareEnv ScopeVars
heVarsInScope
tryTranslateExpr
:: ( ReportAnn (F.Analysis ann)
, MonadReader CheckHoareEnv m
, MonadAnalysis HoareBackendError w m
, MonadFail m
)
=> D a -> F.Expression (F.Analysis ann) -> m (FortranExpr a)
tryTranslateExpr :: forall ann (m :: * -> *) w a.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
D a -> Expression (Analysis ann) -> m (FortranExpr a)
tryTranslateExpr D a
d Expression (Analysis ann)
e = (HoareBackendError -> m (FortranExpr a))
-> (Expression (Analysis ann) -> TranslateT m (FortranExpr a))
-> Expression (Analysis ann)
-> m (FortranExpr a)
forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate (Expression (Analysis ann) -> HoareBackendError -> m (FortranExpr a)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis ann)
e) (D a -> Expression (Analysis ann) -> TranslateT m (FortranExpr a)
forall (m :: * -> *) a ann.
(Monad m, MonadFail m) =>
D a -> Expression (Analysis ann) -> TranslateT m (FortranExpr a)
translateExpression' D a
d) Expression (Analysis ann)
e
tryTranslateCoerceExpr
:: ( ReportAnn (F.Analysis ann)
, MonadReader CheckHoareEnv m
, MonadAnalysis HoareBackendError w m
, MonadFail m
)
=> D a -> F.Expression (F.Analysis ann) -> m (MetaExpr FortranVar a)
tryTranslateCoerceExpr :: forall ann (m :: * -> *) w a.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
D a -> Expression (Analysis ann) -> m (MetaExpr FortranVar a)
tryTranslateCoerceExpr D a
d Expression (Analysis ann)
e =
(HoareBackendError -> m (MetaExpr FortranVar a))
-> (Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar a))
-> Expression (Analysis ann)
-> m (MetaExpr FortranVar a)
forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate (Expression (Analysis ann)
-> HoareBackendError -> m (MetaExpr FortranVar a)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis ann)
e)
((HFree MetaOp (HFree CoreOp FortranVar) a -> MetaExpr FortranVar a)
-> TranslateT m (HFree MetaOp (HFree CoreOp FortranVar) a)
-> TranslateT m (MetaExpr FortranVar a)
forall a b. (a -> b) -> TranslateT m a -> TranslateT m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HFree MetaOp (HFree CoreOp FortranVar) a -> MetaExpr FortranVar a
forall (op1 :: (* -> *) -> * -> *) (op2 :: (* -> *) -> * -> *)
(ops :: [(* -> *) -> * -> *]) (v :: * -> *) a.
(HFunctor op1, HFunctor op2, HFunctor (OpChoice ops),
ChooseOp op1 ops, ChooseOp op2 ops) =>
HFree op1 (HFree op2 v) a -> HFree' ops v a
squashExpression (TranslateT m (HFree MetaOp (HFree CoreOp FortranVar) a)
-> TranslateT m (MetaExpr FortranVar a))
-> (Expression (Analysis ann)
-> TranslateT m (HFree MetaOp (HFree CoreOp FortranVar) a))
-> Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. D a
-> Expression (Analysis ann)
-> TranslateT m (HFree MetaOp (HFree CoreOp FortranVar) a)
forall (m :: * -> *) a ann.
(Monad m, MonadFail m) =>
D a
-> Expression (Analysis ann)
-> TranslateT m (HFree MetaOp (HFree CoreOp FortranVar) a)
translateCoerceExpression D a
d) Expression (Analysis ann)
e
tryTranslateTypeInfo
:: ( ReportAnn (F.Analysis ann)
, MonadReader CheckHoareEnv m
, MonadAnalysis HoareBackendError w m
, MonadFail m
)
=> TypeInfo (F.Analysis ann) -> m SomeType
tryTranslateTypeInfo :: forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
TypeInfo (Analysis ann) -> m SomeType
tryTranslateTypeInfo TypeInfo (Analysis ann)
ti = (HoareBackendError -> m SomeType)
-> (TypeInfo (Analysis ann) -> TranslateT m SomeType)
-> TypeInfo (Analysis ann)
-> m SomeType
forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate (TypeInfo (Analysis ann) -> HoareBackendError -> m SomeType
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' TypeInfo (Analysis ann)
ti) TypeInfo (Analysis ann) -> TranslateT m SomeType
forall (m :: * -> *) ann.
(Monad m, MonadFail m, Show ann) =>
TypeInfo ann -> TranslateT m SomeType
translateTypeInfo TypeInfo (Analysis ann)
ti
tryTranslateBoolExpr
:: ( ReportAnn (F.Analysis ann)
, MonadReader CheckHoareEnv m
, MonadAnalysis HoareBackendError w m
, MonadFail m
)
=> F.Expression (F.Analysis ann) -> m (MetaExpr FortranVar Bool)
tryTranslateBoolExpr :: forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
MonadAnalysis HoareBackendError w m, MonadFail m) =>
Expression (Analysis ann) -> m (MetaExpr FortranVar Bool)
tryTranslateBoolExpr Expression (Analysis ann)
e = (HoareBackendError -> m (MetaExpr FortranVar Bool))
-> (Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar Bool))
-> Expression (Analysis ann)
-> m (MetaExpr FortranVar Bool)
forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate (Expression (Analysis ann)
-> HoareBackendError -> m (MetaExpr FortranVar Bool)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis ann)
e) Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar Bool)
forall (m :: * -> *) ann.
(Monad m, MonadFail m) =>
Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar Bool)
translateBoolExpression Expression (Analysis ann)
e
tryTranslateFormula
:: ( F.Spanned o
, ReportAnn (F.Analysis ann)
, Data ann
, MonadReader CheckHoareEnv m
, MonadAnalysis HoareBackendError w m
, MonadFail m
)
=> o -> PrimFormula (F.Analysis ann) -> m (MetaFormula Bool)
tryTranslateFormula :: forall o ann (m :: * -> *) w.
(Spanned o, ReportAnn (Analysis ann), Data ann,
MonadReader CheckHoareEnv m, MonadAnalysis HoareBackendError w m,
MonadFail m) =>
o
-> PrimFormula (Analysis ann)
-> m (Prop (HFree' AllOps FortranVar) Bool)
tryTranslateFormula o
loc PrimFormula (Analysis ann)
formula = do
Map SourceName [UniqueName]
sourceToUnique <- Getting
(Map SourceName [UniqueName])
CheckHoareEnv
(Map SourceName [UniqueName])
-> m (Map SourceName [UniqueName])
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
(Map SourceName [UniqueName])
CheckHoareEnv
(Map SourceName [UniqueName])
Lens' CheckHoareEnv (Map SourceName [UniqueName])
heSourceToUnique
let formulaUN :: PrimFormula (Analysis ann)
formulaUN = Map SourceName [UniqueName]
-> PrimFormula (Analysis ann) -> PrimFormula (Analysis ann)
forall ann.
Data ann =>
Map SourceName [UniqueName]
-> PrimFormula (Analysis ann) -> PrimFormula (Analysis ann)
setFormulaUniqueNames Map SourceName [UniqueName]
sourceToUnique PrimFormula (Analysis ann)
formula
(HoareBackendError -> m (Prop (HFree' AllOps FortranVar) Bool))
-> (PrimFormula (Analysis ann)
-> TranslateT m (Prop (HFree' AllOps FortranVar) Bool))
-> PrimFormula (Analysis ann)
-> m (Prop (HFree' AllOps FortranVar) Bool)
forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate (o -> HoareBackendError -> m (Prop (HFree' AllOps FortranVar) Bool)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' o
loc) PrimFormula (Analysis ann)
-> TranslateT m (Prop (HFree' AllOps FortranVar) Bool)
forall (m :: * -> *) ann.
(Monad m, MonadFail m) =>
PrimFormula (Analysis ann)
-> TranslateT m (Prop (HFree' AllOps FortranVar) Bool)
translateFormula PrimFormula (Analysis ann)
formulaUN
dropWhileM :: (Monad m, MonadFail m) => (a -> m Bool) -> [a] -> m [a]
dropWhileM :: forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
(a -> m Bool) -> [a] -> m [a]
dropWhileM a -> m Bool
_ [] = [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
dropWhileM a -> m Bool
f (a
x : [a]
xs) = do
Bool
continue <- a -> m Bool
f a
x
if Bool
continue
then (a -> m Bool) -> [a] -> m [a]
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
(a -> m Bool) -> [a] -> m [a]
dropWhileM a -> m Bool
f [a]
xs
else [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs)
fromMaybeM :: (Monad m, MonadFail m) => m a -> Maybe a -> m a
fromMaybeM :: forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
m a -> Maybe a -> m a
fromMaybeM m a
e = m a -> (a -> m a) -> Maybe a -> m a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m a
e a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
getAnnSod :: HA -> Maybe (SpecOrDecl InnerHA)
getAnnSod :: Analysis (HoareAnnotation A) -> Maybe (SpecOrDecl InnerHA)
getAnnSod = Getting
(Maybe (SpecOrDecl InnerHA))
(Analysis (HoareAnnotation A))
(Maybe (SpecOrDecl InnerHA))
-> Analysis (HoareAnnotation A) -> Maybe (SpecOrDecl InnerHA)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((Analysis (HoareAnnotation A) -> HoareAnnotation A)
-> (HoareAnnotation A
-> Const (Maybe (SpecOrDecl InnerHA)) (HoareAnnotation A))
-> Analysis (HoareAnnotation A)
-> Const
(Maybe (SpecOrDecl InnerHA)) (Analysis (HoareAnnotation A))
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to Analysis (HoareAnnotation A) -> HoareAnnotation A
forall a. Analysis a -> a
F.prevAnnotation ((HoareAnnotation A
-> Const (Maybe (SpecOrDecl InnerHA)) (HoareAnnotation A))
-> Analysis (HoareAnnotation A)
-> Const
(Maybe (SpecOrDecl InnerHA)) (Analysis (HoareAnnotation A)))
-> ((Maybe (SpecOrDecl InnerHA)
-> Const (Maybe (SpecOrDecl InnerHA)) (Maybe (SpecOrDecl InnerHA)))
-> HoareAnnotation A
-> Const (Maybe (SpecOrDecl InnerHA)) (HoareAnnotation A))
-> Getting
(Maybe (SpecOrDecl InnerHA))
(Analysis (HoareAnnotation A))
(Maybe (SpecOrDecl InnerHA))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (SpecOrDecl InnerHA)
-> Const (Maybe (SpecOrDecl InnerHA)) (Maybe (SpecOrDecl InnerHA)))
-> HoareAnnotation A
-> Const (Maybe (SpecOrDecl InnerHA)) (HoareAnnotation A)
forall a (f :: * -> *).
Functor f =>
(Maybe (SpecOrDecl InnerHA) -> f (Maybe (SpecOrDecl InnerHA)))
-> HoareAnnotation a -> f (HoareAnnotation a)
hoareSod)
lvVarNames :: F.LValue (F.Analysis x) -> NamePair
lvVarNames :: forall x. LValue (Analysis x) -> NamePair
lvVarNames LValue (Analysis x)
e =
let uniqueName :: UniqueName
uniqueName = String -> UniqueName
UniqueName (String -> UniqueName) -> String -> UniqueName
forall a b. (a -> b) -> a -> b
$ LValue (Analysis x) -> String
forall a. LValue (Analysis a) -> String
F.lvVarName LValue (Analysis x)
e
srcName :: SourceName
srcName = String -> SourceName
SourceName (String -> SourceName) -> String -> SourceName
forall a b. (a -> b) -> a -> b
$ LValue (Analysis x) -> String
forall a. LValue (Analysis a) -> String
F.lvSrcName LValue (Analysis x)
e
in UniqueName -> SourceName -> NamePair
NamePair UniqueName
uniqueName SourceName
srcName
readerOfState :: (MonadState s m) => ReaderT s m a -> m a
readerOfState :: forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState ReaderT s m a
action = do
s
st <- m s
forall s (m :: * -> *). MonadState s m => m s
get
ReaderT s m a -> s -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT s m a
action s
st