{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# 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.Fail
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, defaultSMTCfg)

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           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

--------------------------------------------------------------------------------
--  Data types
--------------------------------------------------------------------------------

data AnnotatedProgramUnit =
  AnnotatedProgramUnit
  { AnnotatedProgramUnit -> [PrimFormula InnerHA]
_apuPreconditions  :: [PrimFormula InnerHA]
  , AnnotatedProgramUnit -> [PrimFormula InnerHA]
_apuPostconditions :: [PrimFormula InnerHA]
  , AnnotatedProgramUnit -> [AuxDecl InnerHA]
_apuAuxDecls       :: [AuxDecl InnerHA]
  , AnnotatedProgramUnit -> ProgramUnit HA
_apuPU             :: F.ProgramUnit HA
  }

data AnnotationError
  = MissingWhileInvariant
  -- ^ The while block had no associated invariant
  | MissingSequenceAnn
  -- ^ A sequence annotation was required but not found

data HoareBackendError
  = VerifierError (VerifierError FortranVar)
  | TranslateErrorAnn TranslateError
  -- ^ Unit errors come from translating annotation formulae
  | TranslateErrorSrc TranslateError
  -- ^ HA errors come from translating actual source Fortran
  | InvalidSourceName SourceName
  -- ^ A program source name had no unique name
  | UnsupportedBlock (F.Block HA)
  -- ^ Found a block that we don't know how to deal with
  | UnexpectedBlock (F.Block HA)
  -- ^ Found a block in an illegal place
  | ArgWithoutDecl NamePair
  -- ^ Found an argument that didn't come with a variable declaration
  | AuxVarConflict F.Name
  -- ^ An auxiliary variable name conflicted with a program source name
  | AssignVarNotInScope NamePair
  -- ^ The variable was referenced in an assignment but not in scope
  | WrongAssignmentType Text SomeType
  -- ^ Expected array type but got the given type instead
  | NonLValueAssignment
  -- ^ Assigning to an expression that isn't an lvalue
  | UnsupportedAssignment Text
  -- ^ Tried to assign to something that's valid Fortran but unsupported
  | AnnotationError AnnotationError
  -- ^ There was a problem with the annotations

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 HA
_ -> Builder
"encountered unsupported block"
      UnexpectedBlock Block HA
_ -> 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
showList :: [HoareCheckResult] -> ShowS
$cshowList :: [HoareCheckResult] -> ShowS
show :: HoareCheckResult -> String
$cshow :: HoareCheckResult -> String
showsPrec :: Int -> HoareCheckResult -> ShowS
$cshowsPrec :: Int -> HoareCheckResult -> ShowS
Show)

instance ExitCodeOfReport HoareCheckResult where
  exitCodeOf :: HoareCheckResult -> Int
exitCodeOf (HoareCheckResult ProgramUnit HA
_ 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 HA
pu Bool
result) =
    Builder
"Program unit '" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ProgramUnitName -> Builder
describePuName (ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puSrcName ProgramUnit HA
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
    -- ^ The variables in scope. Associates unique names with name pairs and types.
  , CheckHoareEnv -> Map SourceName [UniqueName]
_heSourceToUnique :: Map SourceName [UniqueName]
    -- ^ The corresponding unique names for all the source names we have seen.
  , 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 HA
_hePU             :: F.ProgramUnit HA
  }

emptyEnv :: F.ProgramUnit HA -> PrimReprSpec -> CheckHoareEnv
emptyEnv :: ProgramUnit HA -> PrimReprSpec -> CheckHoareEnv
emptyEnv ProgramUnit HA
pu PrimReprSpec
spec = Bool
-> ScopeVars
-> Map SourceName [UniqueName]
-> (forall (p :: Precision) (k :: BasicType) a.
    Prim p k a -> PrimReprHandler a)
-> ProgramUnit HA
-> 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 HA
pu

makeLenses ''AnnotatedProgramUnit
makeLenses ''CheckHoareEnv

instance HasPrimReprHandlers CheckHoareEnv where
  primReprHandler :: 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.
Getter CheckHoareEnv (Prim p k a -> PrimReprHandler a)
heReprHandler

--------------------------------------------------------------------------------
--  Main function
--------------------------------------------------------------------------------

checkPU :: AnnotatedProgramUnit
        -> PrimReprSpec
        -> BackendAnalysis HoareCheckResult
checkPU :: AnnotatedProgramUnit
-> PrimReprSpec -> BackendAnalysis HoareCheckResult
checkPU AnnotatedProgramUnit
apu PrimReprSpec
symSpec = do

  let pu :: ProgramUnit HA
pu = AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
-> ProgramUnit HA
forall s a. s -> Getting a s a -> a
^. Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
Lens' AnnotatedProgramUnit (ProgramUnit HA)
apuPU

  -- The first part of the checking process has a mutable 'CheckHoareEnv' in
  -- 'StateT' as it collects information to add to the environment.
  (((Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
 [Block HA])
bodyTriple, [FortranAssignment]
initialAssignments), CheckHoareEnv
env) <- (StateT
   CheckHoareEnv
   BackendAnalysis
   ((Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
     [Block HA]),
    [FortranAssignment])
 -> CheckHoareEnv
 -> BackendAnalysis
      (((Prop (MetaExpr FortranVar) Bool,
         Prop (MetaExpr FortranVar) Bool, [Block HA]),
        [FortranAssignment]),
       CheckHoareEnv))
-> CheckHoareEnv
-> StateT
     CheckHoareEnv
     BackendAnalysis
     ((Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
       [Block HA]),
      [FortranAssignment])
-> BackendAnalysis
     (((Prop (MetaExpr FortranVar) Bool,
        Prop (MetaExpr FortranVar) Bool, [Block HA]),
       [FortranAssignment]),
      CheckHoareEnv)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  CheckHoareEnv
  BackendAnalysis
  ((Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
    [Block HA]),
   [FortranAssignment])
-> CheckHoareEnv
-> BackendAnalysis
     (((Prop (MetaExpr FortranVar) Bool,
        Prop (MetaExpr FortranVar) Bool, [Block HA]),
       [FortranAssignment]),
      CheckHoareEnv)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ProgramUnit HA -> PrimReprSpec -> CheckHoareEnv
emptyEnv ProgramUnit HA
pu PrimReprSpec
symSpec) (StateT
   CheckHoareEnv
   BackendAnalysis
   ((Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
     [Block HA]),
    [FortranAssignment])
 -> BackendAnalysis
      (((Prop (MetaExpr FortranVar) Bool,
         Prop (MetaExpr FortranVar) Bool, [Block HA]),
        [FortranAssignment]),
       CheckHoareEnv))
-> StateT
     CheckHoareEnv
     BackendAnalysis
     ((Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
       [Block HA]),
      [FortranAssignment])
-> BackendAnalysis
     (((Prop (MetaExpr FortranVar) Bool,
        Prop (MetaExpr FortranVar) Bool, [Block HA]),
       [FortranAssignment]),
      CheckHoareEnv)
forall a b. (a -> b) -> a -> b
$ do
    ProgramUnit HA -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit HA
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Setting up"

    ([Block HA]
body, [FortranAssignment]
initialAssignments) <- CheckHoareMut ([Block HA], [FortranAssignment])
initialSetup

    Bool
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([FortranAssignment] -> 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 HA -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logDebug' ProgramUnit HA
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 (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 (MetaExpr FortranVar) Bool]
translatePUFormulae =
            ReaderT
  CheckHoareEnv
  (StateT CheckHoareEnv BackendAnalysis)
  [Prop (MetaExpr FortranVar) Bool]
-> StateT
     CheckHoareEnv BackendAnalysis [Prop (MetaExpr FortranVar) Bool]
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState
          (ReaderT
   CheckHoareEnv
   (StateT CheckHoareEnv BackendAnalysis)
   [Prop (MetaExpr FortranVar) Bool]
 -> StateT
      CheckHoareEnv BackendAnalysis [Prop (MetaExpr FortranVar) Bool])
-> ([PrimFormula InnerHA]
    -> ReaderT
         CheckHoareEnv
         (StateT CheckHoareEnv BackendAnalysis)
         [Prop (MetaExpr FortranVar) Bool])
-> [PrimFormula InnerHA]
-> StateT
     CheckHoareEnv BackendAnalysis [Prop (MetaExpr FortranVar) Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula InnerHA
 -> ReaderT
      CheckHoareEnv
      (StateT CheckHoareEnv BackendAnalysis)
      (Prop (MetaExpr FortranVar) Bool))
-> [PrimFormula InnerHA]
-> ReaderT
     CheckHoareEnv
     (StateT CheckHoareEnv BackendAnalysis)
     [Prop (MetaExpr FortranVar) Bool]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (ProgramUnit HA
-> PrimFormula InnerHA
-> ReaderT
     CheckHoareEnv
     (StateT CheckHoareEnv BackendAnalysis)
     (Prop (MetaExpr 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 (MetaExpr FortranVar) Bool)
tryTranslateFormula ProgramUnit HA
pu)

    [Prop (MetaExpr FortranVar) Bool]
preconds <- [PrimFormula InnerHA]
-> StateT
     CheckHoareEnv BackendAnalysis [Prop (MetaExpr 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 (MetaExpr FortranVar) Bool]
postconds <- [PrimFormula InnerHA]
-> StateT
     CheckHoareEnv BackendAnalysis [Prop (MetaExpr 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 HA -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit HA
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Interpreting pre- and postconditions"

    let precond :: Prop (MetaExpr FortranVar) Bool
precond = [Prop (MetaExpr FortranVar) Bool]
-> Prop (MetaExpr FortranVar) Bool
forall (expr :: * -> *). [Prop expr Bool] -> Prop expr Bool
propAnd [Prop (MetaExpr FortranVar) Bool]
preconds
        postcond :: Prop (MetaExpr FortranVar) Bool
postcond = [Prop (MetaExpr FortranVar) Bool]
-> Prop (MetaExpr FortranVar) Bool
forall (expr :: * -> *). [Prop expr Bool] -> Prop expr Bool
propAnd [Prop (MetaExpr FortranVar) Bool]
postconds

    ProgramUnit HA -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit HA
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 (MetaExpr FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (MetaExpr FortranVar) Bool
precond)
    ProgramUnit HA -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit HA
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 (MetaExpr FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (MetaExpr FortranVar) Bool
postcond)

    -- Modify the postcondition by substituting in variable values from the
    -- initial assignments
    let postcond' :: Prop (MetaExpr FortranVar) Bool
postcond' = Prop (MetaExpr FortranVar) Bool
-> [FortranAssignment] -> Prop (MetaExpr FortranVar) Bool
forall (expr :: (* -> *) -> * -> *) (v :: * -> *).
(HMonad expr, VerifiableVar v) =>
Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
chainSub Prop (MetaExpr FortranVar) Bool
postcond [FortranAssignment]
initialAssignments

    ((Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
  [Block HA]),
 [FortranAssignment])
-> StateT
     CheckHoareEnv
     BackendAnalysis
     ((Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
       [Block HA]),
      [FortranAssignment])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Prop (MetaExpr FortranVar) Bool
precond, Prop (MetaExpr FortranVar) Bool
postcond', [Block HA]
body), [FortranAssignment]
initialAssignments)

  -- The second part has an immutable 'CheckHoareEnv' in 'ReaderT'.
  (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 HA -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit HA
pu (Text -> ReaderT CheckHoareEnv BackendAnalysis ())
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Computing verification conditions"
    (()
_, [Prop (MetaExpr FortranVar) Bool]
vcs) <- GenM () -> CheckHoare ((), [Prop (MetaExpr FortranVar) Bool])
forall a.
GenM a -> CheckHoare (a, [Prop (MetaExpr FortranVar) Bool])
runGenM ([FortranAssignment]
-> (Prop (MetaExpr FortranVar) Bool,
    Prop (MetaExpr FortranVar) Bool, [Block HA])
-> GenM ()
genBody' [FortranAssignment]
initialAssignments (Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
 [Block HA])
bodyTriple)

    ProgramUnit HA -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit HA
pu (Text -> ReaderT CheckHoareEnv BackendAnalysis ())
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Verifying conditions:"

    let checkVcs :: Int
-> [Prop (MetaExpr FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis Bool
checkVcs Int
_ [] = Bool -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        checkVcs Int
i (Prop (MetaExpr FortranVar) Bool
vc : [Prop (MetaExpr FortranVar) Bool]
rest) = do
          ProgramUnit HA -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit HA
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 (MetaExpr FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (MetaExpr FortranVar) Bool
vc)
          Bool
result <- (HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool)
-> Prop (MetaExpr FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis Bool
verifyVc (ProgramUnit HA
-> HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' ProgramUnit HA
pu) Prop (MetaExpr FortranVar) Bool
vc
          if Bool
result
            then Int
-> [Prop (MetaExpr FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis Bool
checkVcs (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) [Prop (MetaExpr FortranVar) Bool]
rest
            else do
            ProgramUnit HA -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit HA
pu Text
"    - Failed!"
            (Int
 -> Prop (MetaExpr FortranVar) Bool
 -> ReaderT CheckHoareEnv BackendAnalysis ())
-> [Int]
-> [Prop (MetaExpr FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ Int
-> Prop (MetaExpr FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis ()
printUnchecked [(Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i)..] [Prop (MetaExpr FortranVar) Bool]
vcs
            Bool -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

        printUnchecked :: Int
-> Prop (MetaExpr FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis ()
printUnchecked Int
i Prop (MetaExpr FortranVar) Bool
vc = do
          ProgramUnit HA -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit HA
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 (MetaExpr FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (MetaExpr FortranVar) Bool
vc)
          ProgramUnit HA -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit HA
pu   Text
"    - Unchecked"

    ProgramUnit HA -> Bool -> HoareCheckResult
HoareCheckResult ProgramUnit HA
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 (MetaExpr FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis Bool
checkVcs (Int
1 :: Int) [Prop (MetaExpr FortranVar) Bool]
vcs

--------------------------------------------------------------------------------
--  Variables and names
--------------------------------------------------------------------------------

varOfType :: NamePair -> SomeType -> SomeVar
varOfType :: NamePair -> SomeType -> SomeVar
varOfType NamePair
names (Some D a
d) = FortranVar a -> SomeVar
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 :: 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 (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 :: 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 (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"


-- TODO: Consider reporting a warning when two variables have the same source
-- name.

-- | Create a variable in scope with the given name and type.
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 SomeVar -> Identity (Maybe SomeVar))
    -> ScopeVars -> Identity ScopeVars)
-> (Maybe SomeVar -> Identity (Maybe SomeVar))
-> 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 SomeVar -> Identity (Maybe SomeVar))
 -> CheckHoareEnv -> Identity CheckHoareEnv)
-> Maybe SomeVar -> CheckHoareEnv -> CheckHoareEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ SomeVar -> Maybe SomeVar
forall a. a -> Maybe a
Just (NamePair -> SomeType -> SomeVar
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))


-- | In specifications attached to program units (pre- and post-conditions), the
-- @fortran-src@ renamer doesn't have access to a renaming environment so it
-- doesn't assign the right unique names. Once we have access to unique names
-- from inside the program unit, this function assigns those names to variables
-- in the PU specifications.
setFormulaUniqueNames
  :: (Data ann)
  => Map SourceName [UniqueName]
  -> PrimFormula (F.Analysis ann)
  -> PrimFormula (F.Analysis ann)
setFormulaUniqueNames :: 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 (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
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped))

    realNamePair :: NamePair -> NamePair
realNamePair np :: NamePair
np@(NamePair UniqueName
_ SourceName
src) =
      -- TODO: How sound is it to take the first available? Should I throw
      -- warnings?
      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)
_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
_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 }

--------------------------------------------------------------------------------
--  Check Monad
--------------------------------------------------------------------------------

type CheckHoareMut = StateT CheckHoareEnv BackendAnalysis
type CheckHoare = ReaderT CheckHoareEnv BackendAnalysis

type FortranAssignment = Assignment MetaExpr FortranVar

-- | Sets up the environment for checking the program unit, including reading
-- past variable declarations. Returns the assignments made in variable
-- declarations, and blocks after the variable declarations.
initialSetup :: CheckHoareMut ([F.Block HA], [FortranAssignment])
initialSetup :: CheckHoareMut ([Block HA], [FortranAssignment])
initialSetup = do
  ProgramUnit HA
pu <- Getting (ProgramUnit HA) CheckHoareEnv (ProgramUnit HA)
-> StateT CheckHoareEnv BackendAnalysis (ProgramUnit HA)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (ProgramUnit HA) CheckHoareEnv (ProgramUnit HA)
Lens' CheckHoareEnv (ProgramUnit HA)
hePU
  let body :: [Block HA]
body = ProgramUnit HA -> [Block HA]
forall from to. Biplate from to => from -> [to]
childrenBi ProgramUnit HA
pu :: [F.Block HA]

  -- If the program unit is a function, we might need to treat its name as a
  -- variable with its return type.

  -- If the program is a function or subroutine, it might have arguments that we
  -- need to treat as variables.
  [Expression HA]
rawArgNames <- case ProgramUnit HA
pu of
    F.PUFunction HA
_ SrcSpan
_ (Just TypeSpec HA
rettype) PrefixSuffix HA
_ String
_ Maybe (AList Expression HA)
funargs Maybe (Expression HA)
retvalue [Block HA]
_ Maybe [ProgramUnit HA]
_ -> 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 HA
-> 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 HA -> TypeInfo HA
forall ann. TypeSpec ann -> TypeInfo ann
typeInfo TypeSpec HA
rettype)

      let retNames :: NamePair
retNames = case Maybe (Expression HA)
retvalue  of
            Just Expression HA
rv -> Expression HA -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair Expression HA
rv
            Maybe (Expression HA)
Nothing -> ProgramUnit HA -> NamePair
forall a. ProgramUnit (Analysis a) -> NamePair
functionNamePair ProgramUnit HA
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 HA]
-> StateT CheckHoareEnv BackendAnalysis [Expression HA]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expression HA]
-> (AList Expression HA -> [Expression HA])
-> Maybe (AList Expression HA)
-> [Expression HA]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] AList Expression HA -> [Expression HA]
forall (t :: * -> *) a. AList t a -> [t a]
F.aStrip Maybe (AList Expression HA)
funargs)

    F.PUSubroutine HA
_ SrcSpan
_ PrefixSuffix HA
_ String
_ Maybe (AList Expression HA)
subargs [Block HA]
_ Maybe [ProgramUnit HA]
_ -> [Expression HA]
-> StateT CheckHoareEnv BackendAnalysis [Expression HA]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expression HA]
-> (AList Expression HA -> [Expression HA])
-> Maybe (AList Expression HA)
-> [Expression HA]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] AList Expression HA -> [Expression HA]
forall (t :: * -> *) a. AList t a -> [t a]
F.aStrip Maybe (AList Expression HA)
subargs)
    ProgramUnit HA
_ -> [Expression HA]
-> StateT CheckHoareEnv BackendAnalysis [Expression HA]
forall (m :: * -> *) a. Monad m => a -> m a
return []

  let argNames :: [NamePair]
argNames = (Expression HA -> NamePair) -> [Expression HA] -> [NamePair]
forall a b. (a -> b) -> [a] -> [b]
map Expression HA -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair [Expression HA]
rawArgNames

  ([Block HA]
restBody, [FortranAssignment]
initialAssignments) <- [Block HA] -> CheckHoareMut ([Block HA], [FortranAssignment])
readInitialBlocks [Block HA]
body

  -- Verify that all argument names have types associated with them.
  [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 SomeVar -> Bool
forall a. Maybe a -> Bool
isJust (Maybe SomeVar -> Bool)
-> StateT CheckHoareEnv BackendAnalysis (Maybe SomeVar)
-> StateT CheckHoareEnv BackendAnalysis Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting (Maybe SomeVar) CheckHoareEnv (Maybe SomeVar)
-> StateT CheckHoareEnv BackendAnalysis (Maybe SomeVar)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((ScopeVars -> Const (Maybe SomeVar) ScopeVars)
-> CheckHoareEnv -> Const (Maybe SomeVar) CheckHoareEnv
Lens' CheckHoareEnv ScopeVars
heVarsInScope ((ScopeVars -> Const (Maybe SomeVar) ScopeVars)
 -> CheckHoareEnv -> Const (Maybe SomeVar) CheckHoareEnv)
-> ((Maybe SomeVar -> Const (Maybe SomeVar) (Maybe SomeVar))
    -> ScopeVars -> Const (Maybe SomeVar) ScopeVars)
-> Getting (Maybe SomeVar) CheckHoareEnv (Maybe SomeVar)
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 HA
-> HoareBackendError -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' ProgramUnit HA
pu (NamePair -> HoareBackendError
ArgWithoutDecl NamePair
argName)

  ([Block HA], [FortranAssignment])
-> CheckHoareMut ([Block HA], [FortranAssignment])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Block HA]
restBody, [FortranAssignment]
initialAssignments)


-- | Uses the auxiliary variable declaration annotations to add auxiliary
-- variables into scope.
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. Lens' (AuxDecl ann) String
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

    -- Make sure auxiliary variable source names don't conflict with other
    -- variables (including other auxiliary variables).
    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 HA
-> 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 HA) AnnotatedProgramUnit (ProgramUnit HA)
-> ProgramUnit HA
forall s a. s -> Getting a s a -> a
^. Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
Lens' AnnotatedProgramUnit (ProgramUnit HA)
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 ann ann2.
Lens (AuxDecl ann) (AuxDecl ann2) (TypeSpec ann) (TypeSpec 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
    -- This a bit of a hack: keep prepending underscores until we arrive at a
    -- unique name that hasn't been used yet.
    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 (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. [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


-- | As part of the initial setup, reads setup blocks like declarations and
-- implicit statements. Updates the environment accordingly. Returns the rest of
-- the blocks, after the setup blocks.
readInitialBlocks :: [F.Block HA] -> CheckHoareMut ([F.Block HA], [FortranAssignment])
readInitialBlocks :: [Block HA] -> CheckHoareMut ([Block HA], [FortranAssignment])
readInitialBlocks = WriterT
  [FortranAssignment]
  (StateT CheckHoareEnv BackendAnalysis)
  [Block HA]
-> CheckHoareMut ([Block HA], [FortranAssignment])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT
   [FortranAssignment]
   (StateT CheckHoareEnv BackendAnalysis)
   [Block HA]
 -> CheckHoareMut ([Block HA], [FortranAssignment]))
-> ([Block HA]
    -> WriterT
         [FortranAssignment]
         (StateT CheckHoareEnv BackendAnalysis)
         [Block HA])
-> [Block HA]
-> CheckHoareMut ([Block HA], [FortranAssignment])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Block HA
 -> WriterT
      [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool)
-> [Block HA]
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     [Block HA]
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
(a -> m Bool) -> [a] -> m [a]
dropWhileM Block HA
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
readInitialBlock
  where
    -- This function returns 'True' if the block may be part of the setup, and
    -- 'False' otherwise.
    readInitialBlock :: F.Block HA -> WriterT [FortranAssignment] CheckHoareMut Bool
    readInitialBlock :: Block HA
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
readInitialBlock Block HA
bl = case Block HA
bl of
      F.BlStatement HA
_ SrcSpan
_ Maybe (Expression HA)
_ Statement HA
st ->
        case Statement HA
st of
          F.StDeclaration HA
_ SrcSpan
_ TypeSpec HA
astTypeSpec Maybe (AList Attribute HA)
attrs AList Declarator HA
decls -> do
            -- This is the part of the type info that applies to every variable
            -- in the declaration list.
            let topTypeInfo :: TypeInfo HA
topTypeInfo =
                  TypeSpec HA -> TypeInfo HA
forall ann. TypeSpec ann -> TypeInfo ann
typeInfo TypeSpec HA
astTypeSpec TypeInfo HA -> (TypeInfo HA -> TypeInfo HA) -> TypeInfo HA
forall a b. a -> (a -> b) -> b
&
                  (Maybe (AList Attribute HA)
 -> Identity (Maybe (AList Attribute HA)))
-> TypeInfo HA -> Identity (TypeInfo HA)
forall ann. Lens' (TypeInfo ann) (Maybe (AList Attribute ann))
tiAttributes ((Maybe (AList Attribute HA)
  -> Identity (Maybe (AList Attribute HA)))
 -> TypeInfo HA -> Identity (TypeInfo HA))
-> Maybe (AList Attribute HA) -> TypeInfo HA -> TypeInfo HA
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (AList Attribute HA)
attrs

            -- Each variable may have extra information that modifies its type info
            [(Expression HA, TypeInfo HA, Maybe (Expression HA))]
declVarsTis <- [Declarator HA]
-> (Declarator HA
    -> WriterT
         [FortranAssignment]
         (StateT CheckHoareEnv BackendAnalysis)
         (Expression HA, TypeInfo HA, Maybe (Expression HA)))
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     [(Expression HA, TypeInfo HA, Maybe (Expression HA))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (AList Declarator HA -> [Declarator HA]
forall (t :: * -> *) a. AList t a -> [t a]
F.aStrip AList Declarator HA
decls) ((Declarator HA
  -> WriterT
       [FortranAssignment]
       (StateT CheckHoareEnv BackendAnalysis)
       (Expression HA, TypeInfo HA, Maybe (Expression HA)))
 -> WriterT
      [FortranAssignment]
      (StateT CheckHoareEnv BackendAnalysis)
      [(Expression HA, TypeInfo HA, Maybe (Expression HA))])
-> (Declarator HA
    -> WriterT
         [FortranAssignment]
         (StateT CheckHoareEnv BackendAnalysis)
         (Expression HA, TypeInfo HA, Maybe (Expression HA)))
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     [(Expression HA, TypeInfo HA, Maybe (Expression HA))]
forall a b. (a -> b) -> a -> b
$ \case
              F.DeclVariable HA
_ SrcSpan
_ Expression HA
nameExp Maybe (Expression HA)
declLength Maybe (Expression HA)
mInitialValue -> do
                (Expression HA, TypeInfo HA, Maybe (Expression HA))
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     (Expression HA, TypeInfo HA, Maybe (Expression HA))
forall (m :: * -> *) a. Monad m => a -> m a
return (Expression HA
nameExp,
                        TypeInfo HA
topTypeInfo
                        TypeInfo HA -> (TypeInfo HA -> TypeInfo HA) -> TypeInfo HA
forall a b. a -> (a -> b) -> b
& (Maybe (Expression HA) -> Identity (Maybe (Expression HA)))
-> TypeInfo HA -> Identity (TypeInfo HA)
forall ann. Lens' (TypeInfo ann) (Maybe (Expression ann))
tiDeclaratorLength ((Maybe (Expression HA) -> Identity (Maybe (Expression HA)))
 -> TypeInfo HA -> Identity (TypeInfo HA))
-> Maybe (Expression HA) -> TypeInfo HA -> TypeInfo HA
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (Expression HA)
declLength,
                        Maybe (Expression HA)
mInitialValue)

              F.DeclArray HA
_ SrcSpan
_ Expression HA
nameExp AList DimensionDeclarator HA
declDims Maybe (Expression HA)
declLength Maybe (Expression HA)
mInitialValue ->
                (Expression HA, TypeInfo HA, Maybe (Expression HA))
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     (Expression HA, TypeInfo HA, Maybe (Expression HA))
forall (m :: * -> *) a. Monad m => a -> m a
return (Expression HA
nameExp,
                        TypeInfo HA
topTypeInfo
                        TypeInfo HA -> (TypeInfo HA -> TypeInfo HA) -> TypeInfo HA
forall a b. a -> (a -> b) -> b
& (Maybe (Expression HA) -> Identity (Maybe (Expression HA)))
-> TypeInfo HA -> Identity (TypeInfo HA)
forall ann. Lens' (TypeInfo ann) (Maybe (Expression ann))
tiDeclaratorLength ((Maybe (Expression HA) -> Identity (Maybe (Expression HA)))
 -> TypeInfo HA -> Identity (TypeInfo HA))
-> Maybe (Expression HA) -> TypeInfo HA -> TypeInfo HA
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (Expression HA)
declLength
                        TypeInfo HA -> (TypeInfo HA -> TypeInfo HA) -> TypeInfo HA
forall a b. a -> (a -> b) -> b
& (Maybe (AList DimensionDeclarator HA)
 -> Identity (Maybe (AList DimensionDeclarator HA)))
-> TypeInfo HA -> Identity (TypeInfo HA)
forall ann.
Lens' (TypeInfo ann) (Maybe (AList DimensionDeclarator ann))
tiDimensionDeclarators ((Maybe (AList DimensionDeclarator HA)
  -> Identity (Maybe (AList DimensionDeclarator HA)))
 -> TypeInfo HA -> Identity (TypeInfo HA))
-> Maybe (AList DimensionDeclarator HA)
-> TypeInfo HA
-> TypeInfo HA
forall s t a b. ASetter s t a b -> b -> s -> t
.~ AList DimensionDeclarator HA
-> Maybe (AList DimensionDeclarator HA)
forall a. a -> Maybe a
Just AList DimensionDeclarator HA
declDims,
                        Maybe (Expression HA)
mInitialValue)

            [(Expression HA, TypeInfo HA, Maybe (Expression HA))]
-> ((Expression HA, TypeInfo HA, Maybe (Expression HA))
    -> 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 HA, TypeInfo HA, Maybe (Expression HA))]
declVarsTis (((Expression HA, TypeInfo HA, Maybe (Expression HA))
  -> WriterT
       [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
 -> WriterT
      [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> ((Expression HA, TypeInfo HA, Maybe (Expression HA))
    -> WriterT
         [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ()
forall a b. (a -> b) -> a -> b
$ \(Expression HA
varNameExp, TypeInfo HA
varTypeInfo, Maybe (Expression HA)
mInitialValue) -> do
              let varNames :: NamePair
varNames = Expression HA -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair Expression HA
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 HA
-> 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 HA
varTypeInfo

              -- Put the new variable in scope
              (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

              -- Record the assignment if there is one. NB this must be done
              -- after putting the variable in scope, because making an
              -- assignment checks that it is in scope.
              [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 HA
 -> WriterT
      [FortranAssignment]
      (StateT CheckHoareEnv BackendAnalysis)
      FortranAssignment)
-> [Expression HA]
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     [FortranAssignment]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t 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 HA
    -> ReaderT
         CheckHoareEnv
         (WriterT
            [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
         FortranAssignment)
-> Expression HA
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     FortranAssignment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamePair
-> Expression HA
-> ReaderT
     CheckHoareEnv
     (WriterT
        [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
     FortranAssignment
forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError HoareBackendWarning m,
 MonadFail m) =>
NamePair -> Expression (Analysis ann) -> m FortranAssignment
simpleAssignment NamePair
varNames)
                          (Maybe (Expression HA) -> [Expression HA]
forall a. Maybe a -> [a]
maybeToList Maybe (Expression HA)
mInitialValue)

            Bool
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

          F.StImplicit HA
_ SrcSpan
_ Maybe (AList ImpList HA)
Nothing -> do
            -- TODO: Deal with implicits properly
            Bool
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
          F.StImplicit HA
_ SrcSpan
_ (Just AList ImpList HA
_) -> Block HA
-> 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 HA
bl (Block HA -> HoareBackendError
UnsupportedBlock Block HA
bl)
          Statement HA
_ -> Bool
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

      -- Skip comments that don't have sequence annotations
      F.BlComment{} | Maybe (PrimFormula InnerHA)
Nothing <- Block HA -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation Block HA
bl -> Bool
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
      Block HA
_ -> Bool
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
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 (MetaExpr FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis Bool
verifyVc HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool
handle Prop (MetaExpr 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 (MetaExpr 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' forall a.
Query FortranVar a -> ReaderT PrimReprHandlers (Query FortranVar) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (HighRepr a
-> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr 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 (MetaExpr 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 (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 (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)

--------------------------------------------------------------------------------
--  Generation Monad
--------------------------------------------------------------------------------

-- | The verification condition generation monad. A writer of meta-formulae with
-- an immutable 'CheckHoareEnv'.
newtype GenM a = GenM (WriterT [MetaFormula Bool] CheckHoare a)
  deriving
    ( a -> GenM b -> GenM a
(a -> b) -> GenM a -> GenM b
(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
<$ :: a -> GenM b -> GenM a
$c<$ :: forall a b. a -> GenM b -> GenM a
fmap :: (a -> b) -> GenM a -> GenM b
$cfmap :: forall a b. (a -> b) -> GenM a -> GenM b
Functor
    , Functor GenM
a -> GenM a
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
GenM a -> GenM b -> GenM b
GenM a -> GenM b -> GenM a
GenM (a -> b) -> GenM a -> GenM b
(a -> b -> c) -> GenM a -> GenM b -> GenM c
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
<* :: GenM a -> GenM b -> GenM a
$c<* :: forall a b. GenM a -> GenM b -> GenM a
*> :: GenM a -> GenM b -> GenM b
$c*> :: forall a b. GenM a -> GenM b -> GenM b
liftA2 :: (a -> b -> c) -> GenM a -> GenM b -> GenM c
$cliftA2 :: forall a b c. (a -> b -> c) -> GenM a -> GenM b -> GenM c
<*> :: GenM (a -> b) -> GenM a -> GenM b
$c<*> :: forall a b. GenM (a -> b) -> GenM a -> GenM b
pure :: a -> GenM a
$cpure :: forall a. a -> GenM a
$cp1Applicative :: Functor GenM
Applicative
    , Applicative GenM
a -> GenM a
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
GenM a -> (a -> GenM b) -> GenM b
GenM a -> GenM b -> GenM b
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
return :: a -> GenM a
$creturn :: forall a. a -> GenM a
>> :: GenM a -> GenM b -> GenM b
$c>> :: forall a b. GenM a -> GenM b -> GenM b
>>= :: GenM a -> (a -> GenM b) -> GenM b
$c>>= :: forall a b. GenM a -> (a -> GenM b) -> GenM b
$cp1Monad :: Applicative GenM
Monad
    , MonadReader CheckHoareEnv
    , MonadWriter [MetaFormula Bool]
    , MonadLogger HoareBackendError HoareBackendWarning
    , MonadAnalysis HoareBackendError HoareBackendWarning
    , Monad GenM
Monad GenM -> (forall a. String -> GenM a) -> MonadFail GenM
String -> GenM a
forall a. String -> GenM a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
fail :: String -> GenM a
$cfail :: forall a. String -> GenM a
$cp1MonadFail :: Monad GenM
MonadFail
    )


runGenM :: GenM a -> CheckHoare (a, [MetaFormula Bool])
runGenM :: GenM a -> CheckHoare (a, [Prop (MetaExpr FortranVar) Bool])
runGenM (GenM WriterT [Prop (MetaExpr FortranVar) Bool] CheckHoare a
action) = WriterT [Prop (MetaExpr FortranVar) Bool] CheckHoare a
-> CheckHoare (a, [Prop (MetaExpr FortranVar) Bool])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT WriterT [Prop (MetaExpr FortranVar) Bool] CheckHoare a
action


type FortranTriplet a = Triplet MetaExpr FortranVar a


genBody' :: [FortranAssignment] -> FortranTriplet [F.Block HA] -> GenM ()
genBody' :: [FortranAssignment]
-> (Prop (MetaExpr FortranVar) Bool,
    Prop (MetaExpr FortranVar) Bool, [Block HA])
-> GenM ()
genBody' [FortranAssignment]
as (Prop (MetaExpr FortranVar) Bool
precond, Prop (MetaExpr FortranVar) Bool
postcond, [Block HA]
body) = do
  let seqL :: AnnSeq MetaExpr FortranVar (Block HA)
seqL = [FortranAssignment] -> AnnSeq MetaExpr FortranVar (Block HA)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
[Assignment expr var] -> AnnSeq expr var cmd
JustAssign [FortranAssignment]
as
  AnnSeq MetaExpr FortranVar (Block HA)
seqR <- [Block HA] -> GenM (AnnSeq MetaExpr FortranVar (Block HA))
bodyToSequence [Block HA]
body

  case AnnSeq MetaExpr FortranVar (Block HA)
seqL AnnSeq MetaExpr FortranVar (Block HA)
-> AnnSeq MetaExpr FortranVar (Block HA)
-> Maybe (AnnSeq MetaExpr FortranVar (Block HA))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
`joinAnnSeq` AnnSeq MetaExpr FortranVar (Block HA)
seqR of
    Just AnnSeq MetaExpr FortranVar (Block HA)
x -> GenM [()] -> GenM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (GenM [()] -> GenM ()) -> GenM [()] -> GenM ()
forall a b. (a -> b) -> a -> b
$ (Triplet MetaExpr FortranVar (Block HA) -> GenM ())
-> Triplet
     MetaExpr FortranVar (AnnSeq MetaExpr FortranVar (Block HA))
-> 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 MetaExpr FortranVar (Block HA) -> GenM ()
genBlock (Prop (MetaExpr FortranVar) Bool
precond, Prop (MetaExpr FortranVar) Bool
postcond, AnnSeq MetaExpr FortranVar (Block HA)
x)
    Maybe (AnnSeq MetaExpr FortranVar (Block HA))
Nothing -> [Block HA] -> HoareBackendError -> GenM ()
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' [Block HA]
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 (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
 [Block HA])
-> GenM ()
genBody = [FortranAssignment]
-> (Prop (MetaExpr FortranVar) Bool,
    Prop (MetaExpr FortranVar) Bool, [Block HA])
-> GenM ()
genBody' []


genBlock :: FortranTriplet (F.Block HA) -> GenM ()
genBlock :: Triplet MetaExpr FortranVar (Block HA) -> GenM ()
genBlock (Prop (MetaExpr FortranVar) Bool
precond, Prop (MetaExpr FortranVar) Bool
postcond, Block HA
bl) = do
  case Block HA
bl of
    F.BlIf HA
_ SrcSpan
_ Maybe (Expression HA)
_ Maybe String
_ [Maybe (Expression HA)]
conds [[Block HA]]
bodies Maybe (Expression HA)
_ -> do
      [Maybe (MetaExpr FortranVar Bool)]
condsExprs <- (Maybe (Expression HA) -> GenM (Maybe (MetaExpr FortranVar Bool)))
-> [Maybe (Expression HA)]
-> GenM [Maybe (MetaExpr FortranVar Bool)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Expression HA -> GenM (MetaExpr FortranVar Bool))
-> Maybe (Expression HA) -> GenM (Maybe (MetaExpr FortranVar Bool))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expression HA -> 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) [Maybe (Expression HA)]
conds
      ((Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
  [Block HA])
 -> GenM ())
-> (MetaExpr FortranVar Bool -> Prop (MetaExpr FortranVar) Bool)
-> Triplet
     MetaExpr
     FortranVar
     [(Maybe (MetaExpr FortranVar Bool), [Block HA])]
-> 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 (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
 [Block HA])
-> GenM ()
genBody MetaExpr FortranVar Bool -> Prop (MetaExpr FortranVar) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (Prop (MetaExpr FortranVar) Bool
precond, Prop (MetaExpr FortranVar) Bool
postcond, ([Maybe (MetaExpr FortranVar Bool)]
-> [[Block HA]] -> [(Maybe (MetaExpr FortranVar Bool), [Block HA])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe (MetaExpr FortranVar Bool)]
condsExprs [[Block HA]]
bodies))

    F.BlDoWhile HA
_ SrcSpan
_ Maybe (Expression HA)
_ Maybe String
_ Maybe (Expression HA)
_ Expression HA
cond [Block HA]
body Maybe (Expression HA)
_ -> do
      PrimFormula InnerHA
primInvariant <-
        case [Block HA]
body of
         Block HA
b : [Block HA]
_ | Just (SodSpec (Specification SpecKind
SpecInvariant PrimFormula InnerHA
f))
                 <- HA -> Maybe (SpecOrDecl InnerHA)
getAnnSod (Block HA -> HA
forall (f :: * -> *) a. Annotated f => f a -> a
F.getAnnotation Block HA
b)
                 -> PrimFormula InnerHA -> GenM (PrimFormula InnerHA)
forall (m :: * -> *) a. Monad m => a -> m a
return PrimFormula InnerHA
f
         [Block HA]
_ -> Block HA -> HoareBackendError -> GenM (PrimFormula InnerHA)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block HA
bl (HoareBackendError -> GenM (PrimFormula InnerHA))
-> HoareBackendError -> GenM (PrimFormula InnerHA)
forall a b. (a -> b) -> a -> b
$ AnnotationError -> HoareBackendError
AnnotationError AnnotationError
MissingWhileInvariant

      Prop (MetaExpr FortranVar) Bool
invariant <- [Block HA]
-> PrimFormula InnerHA -> GenM (Prop (MetaExpr 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 (MetaExpr FortranVar) Bool)
tryTranslateFormula [Block HA]
body PrimFormula InnerHA
primInvariant
      MetaExpr FortranVar Bool
condExpr <- Expression HA -> 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 HA
cond

      ((Prop (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
  [Block HA])
 -> GenM ())
-> (MetaExpr FortranVar Bool -> Prop (MetaExpr FortranVar) Bool)
-> Prop (MetaExpr FortranVar) Bool
-> Triplet
     MetaExpr FortranVar (MetaExpr FortranVar Bool, [Block HA])
-> 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 (MetaExpr FortranVar) Bool, Prop (MetaExpr FortranVar) Bool,
 [Block HA])
-> GenM ()
genBody MetaExpr FortranVar Bool -> Prop (MetaExpr FortranVar) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr Prop (MetaExpr FortranVar) Bool
invariant (Prop (MetaExpr FortranVar) Bool
precond, Prop (MetaExpr FortranVar) Bool
postcond, (MetaExpr FortranVar Bool
condExpr, [Block HA]
body))

    F.BlComment HA
_ SrcSpan
_ Comment HA
_ -> () -> GenM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Block HA
_ -> Block HA -> HoareBackendError -> GenM ()
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block HA
bl (HoareBackendError -> GenM ()) -> HoareBackendError -> GenM ()
forall a b. (a -> b) -> a -> b
$ Block HA -> HoareBackendError
UnsupportedBlock Block HA
bl


bodyToSequence :: [F.Block HA] -> GenM (AnnSeq MetaExpr FortranVar (F.Block HA))
bodyToSequence :: [Block HA] -> GenM (AnnSeq MetaExpr FortranVar (Block HA))
bodyToSequence [Block HA]
blocks = do
  (AnnSeq MetaExpr FortranVar (Block HA)
 -> Block HA -> GenM (AnnSeq MetaExpr FortranVar (Block HA)))
-> AnnSeq MetaExpr FortranVar (Block HA)
-> [Block HA]
-> GenM (AnnSeq MetaExpr FortranVar (Block HA))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM AnnSeq MetaExpr FortranVar (Block HA)
-> Block HA -> GenM (AnnSeq MetaExpr FortranVar (Block HA))
combineBlockSequence AnnSeq MetaExpr FortranVar (Block HA)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
emptyAnnSeq [Block HA]
blocks


combineBlockSequence
  :: AnnSeq MetaExpr FortranVar (F.Block HA)
  -> F.Block HA
  -> GenM (AnnSeq MetaExpr FortranVar (F.Block HA))
combineBlockSequence :: AnnSeq MetaExpr FortranVar (Block HA)
-> Block HA -> GenM (AnnSeq MetaExpr FortranVar (Block HA))
combineBlockSequence AnnSeq MetaExpr FortranVar (Block HA)
prevSeq Block HA
bl = do
  AnnSeq MetaExpr FortranVar (Block HA)
blSeq <- Block HA -> GenM (AnnSeq MetaExpr FortranVar (Block HA))
blockToSequence Block HA
bl

  case AnnSeq MetaExpr FortranVar (Block HA)
prevSeq AnnSeq MetaExpr FortranVar (Block HA)
-> AnnSeq MetaExpr FortranVar (Block HA)
-> Maybe (AnnSeq MetaExpr FortranVar (Block HA))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
`joinAnnSeq` AnnSeq MetaExpr FortranVar (Block HA)
blSeq of
    Just AnnSeq MetaExpr FortranVar (Block HA)
r  -> AnnSeq MetaExpr FortranVar (Block HA)
-> GenM (AnnSeq MetaExpr FortranVar (Block HA))
forall (m :: * -> *) a. Monad m => a -> m a
return AnnSeq MetaExpr FortranVar (Block HA)
r
    Maybe (AnnSeq MetaExpr FortranVar (Block HA))
Nothing -> Block HA
-> HoareBackendError
-> GenM (AnnSeq MetaExpr FortranVar (Block HA))
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block HA
bl (HoareBackendError -> GenM (AnnSeq MetaExpr FortranVar (Block HA)))
-> HoareBackendError
-> GenM (AnnSeq MetaExpr FortranVar (Block HA))
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 HA -> GenM (AnnSeq MetaExpr FortranVar (Block HA))
blockToSequence Block HA
bl = do
  [GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))]
-> GenM (AnnSeq MetaExpr FortranVar (Block HA))
forall a. [GenM (Maybe a)] -> GenM a
chooseFrom [GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
assignment, GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
sequenceSpec, GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
other]
  where
    assignment :: GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
assignment = (FortranAssignment -> AnnSeq MetaExpr FortranVar (Block HA))
-> Maybe FortranAssignment
-> Maybe (AnnSeq MetaExpr FortranVar (Block HA))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([FortranAssignment] -> AnnSeq MetaExpr FortranVar (Block HA)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
[Assignment expr var] -> AnnSeq expr var cmd
JustAssign ([FortranAssignment] -> AnnSeq MetaExpr FortranVar (Block HA))
-> (FortranAssignment -> [FortranAssignment])
-> FortranAssignment
-> AnnSeq MetaExpr FortranVar (Block HA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FortranAssignment -> [FortranAssignment] -> [FortranAssignment]
forall a. a -> [a] -> [a]
: [])) (Maybe FortranAssignment
 -> Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
-> GenM (Maybe FortranAssignment)
-> GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Block HA -> GenM (Maybe FortranAssignment)
forall (m :: * -> *).
(MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError HoareBackendWarning m,
 MonadFail m) =>
Block HA -> m (Maybe FortranAssignment)
tryBlockToAssignment Block HA
bl

    sequenceSpec :: GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
sequenceSpec =
      (PrimFormula InnerHA
 -> GenM (AnnSeq MetaExpr FortranVar (Block HA)))
-> Maybe (PrimFormula InnerHA)
-> GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse
      ((Prop (MetaExpr FortranVar) Bool
 -> AnnSeq MetaExpr FortranVar (Block HA))
-> GenM (Prop (MetaExpr FortranVar) Bool)
-> GenM (AnnSeq MetaExpr FortranVar (Block HA))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop (MetaExpr FortranVar) Bool
-> AnnSeq MetaExpr FortranVar (Block HA)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
Prop (expr var) Bool -> AnnSeq expr var cmd
propAnnSeq (GenM (Prop (MetaExpr FortranVar) Bool)
 -> GenM (AnnSeq MetaExpr FortranVar (Block HA)))
-> (PrimFormula InnerHA -> GenM (Prop (MetaExpr FortranVar) Bool))
-> PrimFormula InnerHA
-> GenM (AnnSeq MetaExpr FortranVar (Block HA))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block HA
-> PrimFormula InnerHA -> GenM (Prop (MetaExpr 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 (MetaExpr FortranVar) Bool)
tryTranslateFormula Block HA
bl)
      (Block HA -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation Block HA
bl)

    other :: GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
other = Maybe (AnnSeq MetaExpr FortranVar (Block HA))
-> GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (AnnSeq MetaExpr FortranVar (Block HA))
 -> GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA))))
-> Maybe (AnnSeq MetaExpr FortranVar (Block HA))
-> GenM (Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
forall a b. (a -> b) -> a -> b
$ case Block HA
bl of
      F.BlComment{} -> AnnSeq MetaExpr FortranVar (Block HA)
-> Maybe (AnnSeq MetaExpr FortranVar (Block HA))
forall a. a -> Maybe a
Just AnnSeq MetaExpr FortranVar (Block HA)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
emptyAnnSeq
      Block HA
_             -> AnnSeq MetaExpr FortranVar (Block HA)
-> Maybe (AnnSeq MetaExpr FortranVar (Block HA))
forall a. a -> Maybe a
Just (AnnSeq MetaExpr FortranVar (Block HA)
 -> Maybe (AnnSeq MetaExpr FortranVar (Block HA)))
-> AnnSeq MetaExpr FortranVar (Block HA)
-> Maybe (AnnSeq MetaExpr FortranVar (Block HA))
forall a b. (a -> b) -> a -> b
$ Block HA -> AnnSeq MetaExpr FortranVar (Block HA)
forall cmd (expr :: (* -> *) -> * -> *) (var :: * -> *).
cmd -> AnnSeq expr var cmd
cmdAnnSeq Block HA
bl

    -- Tries each action in the list, using the first that works and otherwise
    -- reporting an error.
    chooseFrom :: [GenM (Maybe a)] -> GenM a
    chooseFrom :: [GenM (Maybe a)] -> GenM a
chooseFrom =
      (GenM (Maybe a) -> (Maybe a -> GenM a) -> GenM a
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 HA -> HoareBackendError -> GenM a
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block HA
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 HA -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation = Getting
  (First (PrimFormula InnerHA)) (Block HA) (PrimFormula InnerHA)
-> Block HA -> Maybe (PrimFormula InnerHA)
forall s (m :: * -> *) a.
MonadReader s m =>
Getting (First a) s a -> m (Maybe a)
preview ((Block HA -> HA)
-> Optic' (->) (Const (First (PrimFormula InnerHA))) (Block HA) HA
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to Block HA -> HA
forall (f :: * -> *) a. Annotated f => f a -> a
F.getAnnotation Optic' (->) (Const (First (PrimFormula InnerHA))) (Block HA) HA
-> ((PrimFormula InnerHA
     -> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
    -> HA -> Const (First (PrimFormula InnerHA)) HA)
-> Getting
     (First (PrimFormula InnerHA)) (Block HA) (PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HA -> Maybe (SpecOrDecl InnerHA))
-> Optic'
     (->)
     (Const (First (PrimFormula InnerHA)))
     HA
     (Maybe (SpecOrDecl InnerHA))
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to HA -> Maybe (SpecOrDecl InnerHA)
getAnnSod Optic'
  (->)
  (Const (First (PrimFormula InnerHA)))
  HA
  (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))
-> HA
-> Const (First (PrimFormula InnerHA)) HA
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. Prism (Maybe a) (Maybe b) a 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. Prism' (SpecOrDecl ann) (PrimSpec 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. Prism' (Specification a) a
_SpecSeq)

--------------------------------------------------------------------------------
-- Handling assignments


tryBlockToAssignment
  :: ( MonadReader CheckHoareEnv m
     , MonadAnalysis HoareBackendError HoareBackendWarning m
     , MonadFail m
     )
  => F.Block HA -> m (Maybe FortranAssignment)
tryBlockToAssignment :: Block HA -> m (Maybe FortranAssignment)
tryBlockToAssignment Block HA
bl = do
  case Block HA
bl of
    F.BlStatement HA
_ SrcSpan
_ Maybe (Expression HA)
_ stAst :: Statement HA
stAst@(F.StExpressionAssign HA
_ SrcSpan
_ Expression HA
lexp Expression HA
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 HA
lvalue <- m (LValue HA) -> Maybe (LValue HA) -> m (LValue HA)
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
m a -> Maybe a -> m a
fromMaybeM (Expression HA -> HoareBackendError -> m (LValue HA)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression HA
lexp HoareBackendError
NonLValueAssignment)
                  (Expression HA -> Maybe (LValue HA)
forall a. Expression a -> Maybe (LValue a)
F.toLValue Expression HA
lexp)

        case LValue HA
lvalue of
          F.LvSimpleVar {} -> NamePair -> Expression HA -> m FortranAssignment
forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError HoareBackendWarning m,
 MonadFail m) =>
NamePair -> Expression (Analysis ann) -> m FortranAssignment
simpleAssignment (Expression HA -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair Expression HA
lexp) Expression HA
rvalue

          F.LvSubscript HA
_ SrcSpan
_ lvar :: LValue HA
lvar@(F.LvSimpleVar {}) AList Index HA
ixs ->
            case AList Index HA
ixs of
              F.AList HA
_ SrcSpan
_ [F.IxSingle HA
_ SrcSpan
_ Maybe String
_ Expression HA
ixExpr] ->
                NamePair -> Expression HA -> Expression HA -> m FortranAssignment
forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError HoareBackendWarning m,
 MonadFail m) =>
NamePair
-> Expression (Analysis ann)
-> Expression (Analysis ann)
-> m FortranAssignment
arrayAssignment (LValue HA -> NamePair
forall x. LValue (Analysis x) -> NamePair
lvVarNames LValue HA
lvar) Expression HA
ixExpr Expression HA
rvalue

              AList Index HA
_ -> AList Index HA -> HoareBackendError -> m FortranAssignment
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' AList Index HA
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 HA
_ -> Statement HA -> HoareBackendError -> m FortranAssignment
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Statement HA
stAst (HoareBackendError -> m FortranAssignment)
-> HoareBackendError -> m FortranAssignment
forall a b. (a -> b) -> a -> b
$
               Text -> HoareBackendError
UnsupportedAssignment Text
"complex assignment"

    Block HA
_ -> Maybe FortranAssignment -> m (Maybe FortranAssignment)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FortranAssignment
forall a. Maybe a
Nothing


-- | Create an assignment where the whole value is written to. TODO: this
-- currently only supports primitive values.
simpleAssignment
  :: ( ReportAnn (F.Analysis ann)
     , MonadReader CheckHoareEnv m
     , MonadAnalysis HoareBackendError HoareBackendWarning m
     , MonadFail m
     )
  => NamePair
  -> F.Expression (F.Analysis ann)
  -> m FortranAssignment
simpleAssignment :: 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 SomeVar
forall a (m :: * -> *).
(Spanned a, MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError HoareBackendWarning m,
 MonadFail m) =>
a -> NamePair -> m SomeVar
varFromScope Expression (Analysis ann)
rvalAst NamePair
nm

  case D a
varD of
    DPrim Prim p k a
_ -> 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 (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 :: 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 SomeVar
forall a (m :: * -> *).
(Spanned a, MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError HoareBackendWarning m,
 MonadFail m) =>
a -> NamePair -> m SomeVar
varFromScope Expression (Analysis ann)
rvalAst NamePair
arrName

  case D a
varD of
    DArray Index i
ixIndex ArrValue a
valAv -> do
      let ixD :: D i
ixD = Index i -> D i
forall i. Index i -> D i
dIndex Index i
ixIndex
          valD :: D a
valD = ArrValue a -> D a
forall a. ArrValue a -> D a
dArrValue ArrValue a
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 a
rvalExpr <- HFree CoreOp FortranVar a -> MetaExpr FortranVar a
forall (op :: (* -> *) -> * -> *) (v :: * -> *) a.
(ChooseOp op AllOps, HTraversable op) =>
HFree op v a -> MetaExpr v a
intoMetaExpr (HFree CoreOp FortranVar a -> MetaExpr FortranVar a)
-> m (HFree CoreOp FortranVar a) -> m (MetaExpr FortranVar a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> D a -> Expression (Analysis ann) -> m (HFree CoreOp 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 (FortranExpr a)
tryTranslateExpr D a
valD Expression (Analysis ann)
rvalAst

      -- Replace instances of the array variable with the same array, but with
      -- the new value written at the given index.
      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 a)
arrExpr' = MetaOp (MetaExpr FortranVar) (Array i a)
-> HFree' AllOps FortranVar (Array i a)
forall (op :: (* -> *) -> * -> *) (ops :: [(* -> *) -> * -> *])
       (v :: * -> *) a.
(HFunctor op, HFunctor (OpChoice ops), ChooseOp op ops) =>
op (HFree' ops v) a -> HFree' ops v a
hwrap' (MetaOp (MetaExpr FortranVar) (Array i a)
 -> HFree' AllOps FortranVar (Array i a))
-> MetaOp (MetaExpr FortranVar) (Array i a)
-> HFree' AllOps FortranVar (Array i a)
forall a b. (a -> b) -> a -> b
$ D (Array i a)
-> HFree' AllOps FortranVar (Array i a)
-> MetaExpr FortranVar i
-> MetaExpr FortranVar a
-> MetaOp (MetaExpr FortranVar) (Array i a)
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 a)
varD HFree' AllOps FortranVar a
HFree' AllOps FortranVar (Array i a)
arrExpr MetaExpr FortranVar i
ixExpr MetaExpr FortranVar a
rvalExpr

      FortranAssignment -> m FortranAssignment
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 a)
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 :: a -> NamePair -> m SomeVar
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 SomeVar
mscoped <- Getting (Maybe SomeVar) CheckHoareEnv (Maybe SomeVar)
-> m (Maybe SomeVar)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ScopeVars -> Const (Maybe SomeVar) ScopeVars)
-> CheckHoareEnv -> Const (Maybe SomeVar) CheckHoareEnv
Lens' CheckHoareEnv ScopeVars
heVarsInScope ((ScopeVars -> Const (Maybe SomeVar) ScopeVars)
 -> CheckHoareEnv -> Const (Maybe SomeVar) CheckHoareEnv)
-> ((Maybe SomeVar -> Const (Maybe SomeVar) (Maybe SomeVar))
    -> ScopeVars -> Const (Maybe SomeVar) ScopeVars)
-> Getting (Maybe SomeVar) CheckHoareEnv (Maybe SomeVar)
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 SomeVar
mscoped of
    Just SomeVar
v  -> SomeVar -> m SomeVar
forall (m :: * -> *) a. Monad m => a -> m a
return SomeVar
v
    Maybe SomeVar
Nothing -> a -> HoareBackendError -> m SomeVar
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' a
loc (HoareBackendError -> m SomeVar) -> HoareBackendError -> m SomeVar
forall a b. (a -> b) -> a -> b
$ NamePair -> HoareBackendError
AssignVarNotInScope NamePair
np

--------------------------------------------------------------------------------
--  Translation
--------------------------------------------------------------------------------

class Show a => ReportAnn a where
  fromTranslateError :: proxy a -> TranslateError -> HoareBackendError

instance ReportAnn HA      where fromTranslateError :: proxy HA -> TranslateError -> HoareBackendError
fromTranslateError proxy HA
_ = TranslateError -> HoareBackendError
TranslateErrorSrc
instance ReportAnn InnerHA where fromTranslateError :: 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 :: (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 (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
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

--------------------------------------------------------------------------------
-- Shorthands for translating expressions and failing the analysis if the
-- translation fails

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 :: 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 :: 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 (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 :: 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 :: 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 :: o
-> PrimFormula (Analysis ann)
-> m (Prop (MetaExpr 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
  -- TODO: Instead of setting unique names before translation, can we get the
  -- renamer to work inside annotations? I've tried to make this work but ran
  -- into some problems:
  -- - We have to run the renamer before calling 'annotateComments' or it
  --   doesn't find any comments (why?).
  -- - When the renamer is run /after/ calling 'annotateComemnts' it doesn't do
  --   any renaming inside annotations (why?)
  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 (MetaExpr FortranVar) Bool))
-> (PrimFormula (Analysis ann)
    -> TranslateT m (Prop (MetaExpr FortranVar) Bool))
-> PrimFormula (Analysis ann)
-> m (Prop (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 (o -> HoareBackendError -> m (Prop (MetaExpr 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 (MetaExpr FortranVar) Bool)
forall (m :: * -> *) ann.
(Monad m, MonadFail m) =>
PrimFormula (Analysis ann)
-> TranslateT m (Prop (MetaExpr FortranVar) Bool)
translateFormula PrimFormula (Analysis ann)
formulaUN

--------------------------------------------------------------------------------
--  Utility functions
--------------------------------------------------------------------------------

dropWhileM :: (Monad m, MonadFail m) => (a -> m Bool) -> [a] -> m [a]
dropWhileM :: (a -> m Bool) -> [a] -> m [a]
dropWhileM a -> m Bool
_ [] = [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 (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 :: 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 (m :: * -> *) a. Monad m => a -> m a
return


getAnnSod :: HA -> Maybe (SpecOrDecl InnerHA)
getAnnSod :: HA -> Maybe (SpecOrDecl InnerHA)
getAnnSod = Getting
  (Maybe (SpecOrDecl InnerHA)) HA (Maybe (SpecOrDecl InnerHA))
-> HA -> Maybe (SpecOrDecl InnerHA)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((HA -> HoareAnnotation A)
-> Optic'
     (->) (Const (Maybe (SpecOrDecl InnerHA))) HA (HoareAnnotation A)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to HA -> HoareAnnotation A
forall a. Analysis a -> a
F.prevAnnotation Optic'
  (->) (Const (Maybe (SpecOrDecl InnerHA))) HA (HoareAnnotation A)
-> ((Maybe (SpecOrDecl InnerHA)
     -> Const (Maybe (SpecOrDecl InnerHA)) (Maybe (SpecOrDecl InnerHA)))
    -> HoareAnnotation A
    -> Const (Maybe (SpecOrDecl InnerHA)) (HoareAnnotation A))
-> Getting
     (Maybe (SpecOrDecl InnerHA)) HA (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. Lens' (HoareAnnotation a) (Maybe (SpecOrDecl InnerHA))
hoareSod)


lvVarNames :: F.LValue (F.Analysis x) -> NamePair
lvVarNames :: 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 :: 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