{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE CPP                        #-}

{-# OPTIONS_GHC -Wall #-}

module Camfort.Specification.Hoare.CheckBackend
  ( AnnotatedProgramUnit(..)
  , apuPreconditions
  , apuPostconditions
  , apuPU
  , apuAuxDecls
  , BackendAnalysis
  , HoareCheckResult(..)
  , HoareBackendError(..)
  , checkPU
  ) where

import           Control.Exception                      (Exception (..))
import           Control.Lens
import           Control.Monad.Reader
import           Control.Monad.State.Strict
import           Control.Monad.Writer.Lazy
import           Control.Monad.Trans.Maybe
import           Data.Data                              (Data)
import           Data.Foldable                          (foldlM)
import           Data.Generics.Uniplate.Operations      (childrenBi,
                                                         transformBi)
import           Data.Map                               (Map)
import qualified Data.Map                               as Map
import           Data.Maybe                             (isJust, maybeToList)
import           Data.Void                              (Void)

import           Data.SBV                               (SBool)

import qualified Language.Fortran.Analysis              as F
import qualified Language.Fortran.AST                   as F
import qualified Language.Fortran.LValue                as F
import qualified Language.Fortran.Util.Position         as F

import qualified Data.List.NonEmpty                     as NE

import           Camfort.Analysis
import           Camfort.Analysis.Logger                (Builder, Text)
import           Camfort.Helpers.TypeLevel
import           Camfort.Specification.Hoare.Annotation
import           Camfort.Specification.Hoare.Syntax
import           Camfort.Specification.Hoare.Translate
import           Language.Fortran.Model
import           Language.Fortran.Model.Repr.Prim
import           Language.Fortran.Model.Translate
import           Language.Fortran.Model.Vars

import           Language.Expression
import           Language.Expression.Choice
import           Language.Expression.Pretty
import           Language.Expression.Prop
import           Language.Verification
import           Language.Verification.Conditions

#if !MIN_VERSION_base(4,13,0)
-- Control.Monad.Fail import is redundant since GHC 8.8.1
import           Control.Monad.Fail
#endif

--------------------------------------------------------------------------------
--  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 (Analysis (HoareAnnotation A))
_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 (Analysis (HoareAnnotation A))
_ -> Builder
"encountered unsupported block"
      UnexpectedBlock Block (Analysis (HoareAnnotation A))
_ -> Builder
"a block was found in an illegal location"
      ArgWithoutDecl NamePair
nm ->
        Builder
"argument " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (NamePair -> String
forall a. Show a => a -> String
show NamePair
nm) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Builder
" doesn't have an associated type declaration"
      AuxVarConflict String
nm ->
        Builder
"auxiliary variable " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder String
nm Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Builder
" has the same name as a program variable; this is not allowed"
      AnnotationError AnnotationError
e -> AnnotationError -> Builder
forall a. Describe a => a -> Builder
describeBuilder AnnotationError
e
      AssignVarNotInScope NamePair
nm ->
        Builder
"variable " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (NamePair -> String
forall a. Pretty a => a -> String
pretty NamePair
nm) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Builder
" is being assigned to but is not in scope"
      WrongAssignmentType Text
message SomeType
gotType ->
        Builder
"unexpected variable type; expected " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Text -> Builder
forall a. Describe a => a -> Builder
describeBuilder Text
message Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Builder
"; got " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (SomeType -> String
forall a. Pretty a => a -> String
pretty SomeType
gotType)
      HoareBackendError
NonLValueAssignment ->
        Builder
"assignment an expression which is not a valid lvalue"
      UnsupportedAssignment Text
message ->
        Builder
"unsupported assignment; " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Text -> Builder
forall a. Describe a => a -> Builder
describeBuilder Text
message

type HoareBackendWarning = Void
type BackendAnalysis = AnalysisT HoareBackendError HoareBackendWarning IO

data HoareCheckResult = HoareCheckResult (F.ProgramUnit HA) Bool
  deriving (Int -> HoareCheckResult -> ShowS
[HoareCheckResult] -> ShowS
HoareCheckResult -> String
(Int -> HoareCheckResult -> ShowS)
-> (HoareCheckResult -> String)
-> ([HoareCheckResult] -> ShowS)
-> Show HoareCheckResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HoareCheckResult -> ShowS
showsPrec :: Int -> HoareCheckResult -> ShowS
$cshow :: HoareCheckResult -> String
show :: HoareCheckResult -> String
$cshowList :: [HoareCheckResult] -> ShowS
showList :: [HoareCheckResult] -> ShowS
Show)

instance ExitCodeOfReport HoareCheckResult where
  exitCodeOf :: HoareCheckResult -> Int
exitCodeOf (HoareCheckResult ProgramUnit (Analysis (HoareAnnotation A))
_ Bool
r) = if Bool
r then Int
0 else Int
1

describePuName :: F.ProgramUnitName -> Builder
describePuName :: ProgramUnitName -> Builder
describePuName (F.Named String
n)         = String -> Builder
forall a. Describe a => a -> Builder
describeBuilder String
n
describePuName ProgramUnitName
F.NamelessBlockData = Builder
"<nameless block data>"
describePuName ProgramUnitName
F.NamelessComment   = Builder
"<nameless comment>"
describePuName ProgramUnitName
F.NamelessMain      = Builder
"<nameless main>"

instance Describe HoareCheckResult where
  describeBuilder :: HoareCheckResult -> Builder
describeBuilder (HoareCheckResult ProgramUnit (Analysis (HoareAnnotation A))
pu Bool
result) =
    Builder
"Program unit '" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ProgramUnitName -> Builder
describePuName (ProgramUnit (Analysis (HoareAnnotation A)) -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puSrcName ProgramUnit (Analysis (HoareAnnotation A))
pu) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"': " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
    (if Bool
result then Builder
"verified!" else Builder
"unverifiable!")

type ScopeVars = Map UniqueName SomeVar

data CheckHoareEnv =
  CheckHoareEnv
  { CheckHoareEnv -> Bool
_heImplicitVars   :: Bool
  , CheckHoareEnv -> ScopeVars
_heVarsInScope    :: ScopeVars
    -- ^ 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 (Analysis (HoareAnnotation A))
_hePU             :: F.ProgramUnit HA
  }

emptyEnv :: F.ProgramUnit HA -> PrimReprSpec -> CheckHoareEnv
emptyEnv :: ProgramUnit (Analysis (HoareAnnotation A))
-> PrimReprSpec -> CheckHoareEnv
emptyEnv ProgramUnit (Analysis (HoareAnnotation A))
pu PrimReprSpec
spec = Bool
-> ScopeVars
-> Map SourceName [UniqueName]
-> (forall (p :: Precision) (k :: BasicType) a.
    Prim p k a -> PrimReprHandler a)
-> ProgramUnit (Analysis (HoareAnnotation A))
-> CheckHoareEnv
CheckHoareEnv Bool
True ScopeVars
forall a. Monoid a => a
mempty Map SourceName [UniqueName]
forall a. Monoid a => a
mempty (PrimReprSpec -> Prim p k a -> PrimReprHandler a
forall (p :: Precision) (k :: BasicType) a.
PrimReprSpec -> Prim p k a -> PrimReprHandler a
makeSymRepr PrimReprSpec
spec) ProgramUnit (Analysis (HoareAnnotation A))
pu

makeLenses ''AnnotatedProgramUnit
makeLenses ''CheckHoareEnv

instance HasPrimReprHandlers CheckHoareEnv where
  primReprHandler :: forall (p :: Precision) (k :: BasicType) a.
CheckHoareEnv -> Prim p k a -> PrimReprHandler a
primReprHandler = Getting
  (Prim p k a -> PrimReprHandler a)
  CheckHoareEnv
  (Prim p k a -> PrimReprHandler a)
-> CheckHoareEnv -> Prim p k a -> PrimReprHandler a
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Prim p k a -> PrimReprHandler a)
  CheckHoareEnv
  (Prim p k a -> PrimReprHandler a)
forall (p :: Precision) (k :: BasicType) a (f :: * -> *).
(Contravariant f, Functor f) =>
((Prim p k a -> PrimReprHandler a)
 -> f (Prim p k a -> PrimReprHandler a))
-> CheckHoareEnv -> f CheckHoareEnv
heReprHandler

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

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

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

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

    ([Block (Analysis (HoareAnnotation A))]
body, [FortranAssignment]
initialAssignments) <- CheckHoareMut
  ([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
initialSetup

    Bool
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([FortranAssignment] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FortranAssignment]
initialAssignments) (StateT CheckHoareEnv BackendAnalysis ()
 -> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$
      ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logDebug' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$
      Text
"Found " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
describeShow ([FortranAssignment] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FortranAssignment]
initialAssignments) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
      Text
" initial assignments: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [String] -> Text
forall a. Show a => a -> Text
describeShow ((FortranAssignment -> String) -> [FortranAssignment] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map FortranAssignment -> String
forall a. Pretty a => a -> String
pretty [FortranAssignment]
initialAssignments)

    AnnotatedProgramUnit -> StateT CheckHoareEnv BackendAnalysis ()
addAuxVariables AnnotatedProgramUnit
apu

    let translatePUFormulae :: [PrimFormula InnerHA]
-> StateT
     CheckHoareEnv
     BackendAnalysis
     [Prop (HFree' AllOps FortranVar) Bool]
translatePUFormulae =
            ReaderT
  CheckHoareEnv
  (StateT CheckHoareEnv BackendAnalysis)
  [Prop (HFree' AllOps FortranVar) Bool]
-> StateT
     CheckHoareEnv
     BackendAnalysis
     [Prop (HFree' AllOps FortranVar) Bool]
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState
          (ReaderT
   CheckHoareEnv
   (StateT CheckHoareEnv BackendAnalysis)
   [Prop (HFree' AllOps FortranVar) Bool]
 -> StateT
      CheckHoareEnv
      BackendAnalysis
      [Prop (HFree' AllOps FortranVar) Bool])
-> ([PrimFormula InnerHA]
    -> ReaderT
         CheckHoareEnv
         (StateT CheckHoareEnv BackendAnalysis)
         [Prop (HFree' AllOps FortranVar) Bool])
-> [PrimFormula InnerHA]
-> StateT
     CheckHoareEnv
     BackendAnalysis
     [Prop (HFree' AllOps FortranVar) Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula InnerHA
 -> ReaderT
      CheckHoareEnv
      (StateT CheckHoareEnv BackendAnalysis)
      (Prop (HFree' AllOps FortranVar) Bool))
-> [PrimFormula InnerHA]
-> ReaderT
     CheckHoareEnv
     (StateT CheckHoareEnv BackendAnalysis)
     [Prop (HFree' AllOps FortranVar) Bool]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (ProgramUnit (Analysis (HoareAnnotation A))
-> PrimFormula InnerHA
-> ReaderT
     CheckHoareEnv
     (StateT CheckHoareEnv BackendAnalysis)
     (Prop (HFree' AllOps FortranVar) Bool)
forall o ann (m :: * -> *) w.
(Spanned o, ReportAnn (Analysis ann), Data ann,
 MonadReader CheckHoareEnv m, MonadAnalysis HoareBackendError w m,
 MonadFail m) =>
o
-> PrimFormula (Analysis ann)
-> m (Prop (HFree' AllOps FortranVar) Bool)
tryTranslateFormula ProgramUnit (Analysis (HoareAnnotation A))
pu)

    [Prop (HFree' AllOps FortranVar) Bool]
preconds <- [PrimFormula InnerHA]
-> StateT
     CheckHoareEnv
     BackendAnalysis
     [Prop (HFree' AllOps FortranVar) Bool]
translatePUFormulae (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting
     [PrimFormula InnerHA] AnnotatedProgramUnit [PrimFormula InnerHA]
-> [PrimFormula InnerHA]
forall s a. s -> Getting a s a -> a
^. Getting
  [PrimFormula InnerHA] AnnotatedProgramUnit [PrimFormula InnerHA]
Lens' AnnotatedProgramUnit [PrimFormula InnerHA]
apuPreconditions)
    [Prop (HFree' AllOps FortranVar) Bool]
postconds <- [PrimFormula InnerHA]
-> StateT
     CheckHoareEnv
     BackendAnalysis
     [Prop (HFree' AllOps FortranVar) Bool]
translatePUFormulae (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting
     [PrimFormula InnerHA] AnnotatedProgramUnit [PrimFormula InnerHA]
-> [PrimFormula InnerHA]
forall s a. s -> Getting a s a -> a
^. Getting
  [PrimFormula InnerHA] AnnotatedProgramUnit [PrimFormula InnerHA]
Lens' AnnotatedProgramUnit [PrimFormula InnerHA]
apuPostconditions)

    ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Interpreting pre- and postconditions"

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

    ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Found preconditions: "  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. Describe a => a -> Text
describe (Prop (HFree' AllOps FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (HFree' AllOps FortranVar) Bool
precond)
    ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> StateT CheckHoareEnv BackendAnalysis ())
-> Text -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Found postconditions: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. Describe a => a -> Text
describe (Prop (HFree' AllOps FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (HFree' AllOps FortranVar) Bool
postcond)

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

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

  -- 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 (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> ReaderT CheckHoareEnv BackendAnalysis ())
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
" - Computing verification conditions"
    (()
_, [Prop (HFree' AllOps FortranVar) Bool]
vcs) <- GenM () -> CheckHoare ((), [Prop (HFree' AllOps FortranVar) Bool])
forall a.
GenM a -> CheckHoare (a, [Prop (HFree' AllOps FortranVar) Bool])
runGenM ([FortranAssignment]
-> (Prop (HFree' AllOps FortranVar) Bool,
    Prop (HFree' AllOps FortranVar) Bool,
    [Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody' [FortranAssignment]
initialAssignments (Prop (HFree' AllOps FortranVar) Bool,
 Prop (HFree' AllOps FortranVar) Bool,
 [Block (Analysis (HoareAnnotation A))])
bodyTriple)

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

    let checkVcs :: Int
-> [Prop (HFree' AllOps FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis Bool
checkVcs Int
_ [] = Bool -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall a. a -> ReaderT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        checkVcs Int
i (Prop (HFree' AllOps FortranVar) Bool
vc : [Prop (HFree' AllOps FortranVar) Bool]
rest) = do
          ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> ReaderT CheckHoareEnv BackendAnalysis ())
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
"   " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
describeShow Int
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. Describe a => a -> Text
describe (Prop (HFree' AllOps FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (HFree' AllOps FortranVar) Bool
vc)
          Bool
result <- (HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool)
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis Bool
verifyVc (ProgramUnit (Analysis (HoareAnnotation A))
-> HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' ProgramUnit (Analysis (HoareAnnotation A))
pu) Prop (HFree' AllOps FortranVar) Bool
vc
          if Bool
result
            then Int
-> [Prop (HFree' AllOps FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis Bool
checkVcs (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) [Prop (HFree' AllOps FortranVar) Bool]
rest
            else do
            ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu Text
"    - Failed!"
            (Int
 -> Prop (HFree' AllOps FortranVar) Bool
 -> ReaderT CheckHoareEnv BackendAnalysis ())
-> [Int]
-> [Prop (HFree' AllOps FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ Int
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis ()
printUnchecked [(Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i)..] [Prop (HFree' AllOps FortranVar) Bool]
vcs
            Bool -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall a. a -> ReaderT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

        printUnchecked :: Int
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis ()
printUnchecked Int
i Prop (HFree' AllOps FortranVar) Bool
vc = do
          ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu (Text -> ReaderT CheckHoareEnv BackendAnalysis ())
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ Text
"   " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
describeShow Int
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. Describe a => a -> Text
describe (Prop (HFree' AllOps FortranVar) Bool -> String
forall a. Pretty a => a -> String
pretty Prop (HFree' AllOps FortranVar) Bool
vc)
          ProgramUnit (Analysis (HoareAnnotation A))
-> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall a.
Spanned a =>
a -> Text -> ReaderT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' ProgramUnit (Analysis (HoareAnnotation A))
pu   Text
"    - Unchecked"

    ProgramUnit (Analysis (HoareAnnotation A))
-> Bool -> HoareCheckResult
HoareCheckResult ProgramUnit (Analysis (HoareAnnotation A))
pu (Bool -> HoareCheckResult)
-> ReaderT CheckHoareEnv BackendAnalysis Bool
-> ReaderT CheckHoareEnv BackendAnalysis HoareCheckResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> [Prop (HFree' AllOps FortranVar) Bool]
-> ReaderT CheckHoareEnv BackendAnalysis Bool
checkVcs (Int
1 :: Int) [Prop (HFree' AllOps FortranVar) Bool]
vcs

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

varOfType :: NamePair -> SomeType -> SomeVar
varOfType :: NamePair -> SomeType -> Some FortranVar
varOfType NamePair
names (Some D a
d) = FortranVar a -> Some FortranVar
forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some (D a -> NamePair -> FortranVar a
forall a. D a -> NamePair -> FortranVar a
FortranVar D a
d NamePair
names)


expNamePair :: F.Expression (F.Analysis a) -> NamePair
expNamePair :: forall a. Expression (Analysis a) -> NamePair
expNamePair = UniqueName -> SourceName -> NamePair
NamePair (UniqueName -> SourceName -> NamePair)
-> (Expression (Analysis a) -> UniqueName)
-> Expression (Analysis a)
-> SourceName
-> NamePair
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> UniqueName
UniqueName (String -> UniqueName)
-> (Expression (Analysis a) -> String)
-> Expression (Analysis a)
-> UniqueName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression (Analysis a) -> String
forall a. Expression (Analysis a) -> String
F.varName (Expression (Analysis a) -> SourceName -> NamePair)
-> (Expression (Analysis a) -> SourceName)
-> Expression (Analysis a)
-> NamePair
forall a b.
(Expression (Analysis a) -> a -> b)
-> (Expression (Analysis a) -> a) -> Expression (Analysis a) -> b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SourceName
SourceName (String -> SourceName)
-> (Expression (Analysis a) -> String)
-> Expression (Analysis a)
-> SourceName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression (Analysis a) -> String
forall a. Expression (Analysis a) -> String
F.srcName


functionNamePair :: F.ProgramUnit (F.Analysis a) -> NamePair
functionNamePair :: forall a. ProgramUnit (Analysis a) -> NamePair
functionNamePair =
  UniqueName -> SourceName -> NamePair
NamePair (UniqueName -> SourceName -> NamePair)
-> (ProgramUnit (Analysis a) -> UniqueName)
-> ProgramUnit (Analysis a)
-> SourceName
-> NamePair
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> UniqueName
UniqueName (String -> UniqueName)
-> (ProgramUnit (Analysis a) -> String)
-> ProgramUnit (Analysis a)
-> UniqueName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramUnitName -> String
fromPuName (ProgramUnitName -> String)
-> (ProgramUnit (Analysis a) -> ProgramUnitName)
-> ProgramUnit (Analysis a)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramUnit (Analysis a) -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName
           (ProgramUnit (Analysis a) -> SourceName -> NamePair)
-> (ProgramUnit (Analysis a) -> SourceName)
-> ProgramUnit (Analysis a)
-> NamePair
forall a b.
(ProgramUnit (Analysis a) -> a -> b)
-> (ProgramUnit (Analysis a) -> a) -> ProgramUnit (Analysis a) -> b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SourceName
SourceName (String -> SourceName)
-> (ProgramUnit (Analysis a) -> String)
-> ProgramUnit (Analysis a)
-> SourceName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramUnitName -> String
fromPuName (ProgramUnitName -> String)
-> (ProgramUnit (Analysis a) -> ProgramUnitName)
-> ProgramUnit (Analysis a)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramUnit (Analysis a) -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puSrcName
  where
    fromPuName :: ProgramUnitName -> String
fromPuName (F.Named String
n) = String
n
    fromPuName ProgramUnitName
_           = ShowS
forall a. HasCallStack => String -> a
error String
"impossible: function has no name"


-- 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 (Some FortranVar) -> Identity (Maybe (Some FortranVar)))
    -> ScopeVars -> Identity ScopeVars)
-> (Maybe (Some FortranVar) -> Identity (Maybe (Some FortranVar)))
-> CheckHoareEnv
-> Identity CheckHoareEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index ScopeVars -> Lens' ScopeVars (Maybe (IxValue ScopeVars))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index ScopeVars
UniqueName
uniq ((Maybe (Some FortranVar) -> Identity (Maybe (Some FortranVar)))
 -> CheckHoareEnv -> Identity CheckHoareEnv)
-> Maybe (Some FortranVar) -> CheckHoareEnv -> CheckHoareEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Some FortranVar -> Maybe (Some FortranVar)
forall a. a -> Maybe a
Just (NamePair -> SomeType -> Some FortranVar
varOfType NamePair
np SomeType
ty))
  (CheckHoareEnv -> CheckHoareEnv)
-> (CheckHoareEnv -> CheckHoareEnv)
-> CheckHoareEnv
-> CheckHoareEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Map SourceName [UniqueName]
 -> Identity (Map SourceName [UniqueName]))
-> CheckHoareEnv -> Identity CheckHoareEnv
Lens' CheckHoareEnv (Map SourceName [UniqueName])
heSourceToUnique ((Map SourceName [UniqueName]
  -> Identity (Map SourceName [UniqueName]))
 -> CheckHoareEnv -> Identity CheckHoareEnv)
-> ((Maybe [UniqueName] -> Identity (Maybe [UniqueName]))
    -> Map SourceName [UniqueName]
    -> Identity (Map SourceName [UniqueName]))
-> (Maybe [UniqueName] -> Identity (Maybe [UniqueName]))
-> CheckHoareEnv
-> Identity CheckHoareEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map SourceName [UniqueName])
-> Lens'
     (Map SourceName [UniqueName])
     (Maybe (IxValue (Map SourceName [UniqueName])))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map SourceName [UniqueName])
SourceName
src ((Maybe [UniqueName] -> Identity (Maybe [UniqueName]))
 -> CheckHoareEnv -> Identity CheckHoareEnv)
-> (Maybe [UniqueName] -> Maybe [UniqueName])
-> CheckHoareEnv
-> CheckHoareEnv
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ \case
        Maybe [UniqueName]
Nothing -> [UniqueName] -> Maybe [UniqueName]
forall a. a -> Maybe a
Just [UniqueName
uniq]
        Just [UniqueName]
xs -> [UniqueName] -> Maybe [UniqueName]
forall a. a -> Maybe a
Just (UniqueName
uniq UniqueName -> [UniqueName] -> [UniqueName]
forall a. a -> [a] -> [a]
: [UniqueName]
xs))


-- | 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 :: forall ann.
Data ann =>
Map SourceName [UniqueName]
-> PrimFormula (Analysis ann) -> PrimFormula (Analysis ann)
setFormulaUniqueNames Map SourceName [UniqueName]
nameMap = (Expression InnerHA -> Expression InnerHA)
-> PrimFormula (Analysis ann) -> PrimFormula (Analysis ann)
forall from to. Biplate from to => (to -> to) -> from -> from
transformBi Expression InnerHA -> Expression InnerHA
setExpUN
  where
    setExpUN :: F.Expression InnerHA -> F.Expression InnerHA
    setExpUN :: Expression InnerHA -> Expression InnerHA
setExpUN = do
      NamePair
np <- NamePair -> NamePair
realNamePair (NamePair -> NamePair)
-> (Expression InnerHA -> NamePair)
-> Expression InnerHA
-> NamePair
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression InnerHA -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair
      (InnerHA -> InnerHA) -> Expression InnerHA -> Expression InnerHA
forall a. (a -> a) -> Expression a -> Expression a
forall (f :: * -> *) a. Annotated f => (a -> a) -> f a -> f a
F.modifyAnnotation (String -> InnerHA -> InnerHA
forall {a}. String -> Analysis a -> Analysis a
setAnnUniq (NamePair
np NamePair -> Getting String NamePair String -> String
forall s a. s -> Getting a s a -> a
^. (UniqueName -> Const String UniqueName)
-> NamePair -> Const String NamePair
Lens' NamePair UniqueName
npUnique ((UniqueName -> Const String UniqueName)
 -> NamePair -> Const String NamePair)
-> ((String -> Const String String)
    -> UniqueName -> Const String UniqueName)
-> Getting String NamePair String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Const String String)
-> UniqueName -> Const String UniqueName
(Unwrapped UniqueName -> Const String (Unwrapped UniqueName))
-> UniqueName -> Const String UniqueName
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Iso
  UniqueName UniqueName (Unwrapped UniqueName) (Unwrapped UniqueName)
_Wrapped))

    realNamePair :: NamePair -> NamePair
realNamePair np :: NamePair
np@(NamePair UniqueName
_ SourceName
src) =
      -- 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)
Prism
  [UniqueName]
  [UniqueName]
  (UniqueName, [UniqueName])
  (UniqueName, [UniqueName])
_Cons (((UniqueName, [UniqueName])
  -> Const (First UniqueName) (UniqueName, [UniqueName]))
 -> [UniqueName] -> Const (First UniqueName) [UniqueName])
-> ((UniqueName -> Const (First UniqueName) UniqueName)
    -> (UniqueName, [UniqueName])
    -> Const (First UniqueName) (UniqueName, [UniqueName]))
-> (UniqueName -> Const (First UniqueName) UniqueName)
-> [UniqueName]
-> Const (First UniqueName) [UniqueName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UniqueName -> Const (First UniqueName) UniqueName)
-> (UniqueName, [UniqueName])
-> Const (First UniqueName) (UniqueName, [UniqueName])
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (UniqueName, [UniqueName])
  (UniqueName, [UniqueName])
  UniqueName
  UniqueName
_1 of
        Just UniqueName
uniq -> UniqueName -> SourceName -> NamePair
NamePair UniqueName
uniq SourceName
src
        Maybe UniqueName
Nothing   -> NamePair
np

    setAnnUniq :: String -> Analysis a -> Analysis a
setAnnUniq String
uniq Analysis a
a = Analysis a
a { uniqueName :: Maybe String
F.uniqueName = String -> Maybe String
forall a. a -> Maybe a
Just String
uniq }

--------------------------------------------------------------------------------
--  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 (Analysis (HoareAnnotation A))], [FortranAssignment])
initialSetup = do
  ProgramUnit (Analysis (HoareAnnotation A))
pu <- Getting
  (ProgramUnit (Analysis (HoareAnnotation A)))
  CheckHoareEnv
  (ProgramUnit (Analysis (HoareAnnotation A)))
-> StateT
     CheckHoareEnv
     BackendAnalysis
     (ProgramUnit (Analysis (HoareAnnotation A)))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
  (ProgramUnit (Analysis (HoareAnnotation A)))
  CheckHoareEnv
  (ProgramUnit (Analysis (HoareAnnotation A)))
Lens' CheckHoareEnv (ProgramUnit (Analysis (HoareAnnotation A)))
hePU
  let body :: [Block (Analysis (HoareAnnotation A))]
body = ProgramUnit (Analysis (HoareAnnotation A))
-> [Block (Analysis (HoareAnnotation A))]
forall from to. Biplate from to => from -> [to]
childrenBi ProgramUnit (Analysis (HoareAnnotation A))
pu :: [F.Block HA]

  -- 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 (Analysis (HoareAnnotation A))]
rawArgNames <- case ProgramUnit (Analysis (HoareAnnotation A))
pu of
    F.PUFunction Analysis (HoareAnnotation A)
_ SrcSpan
_ (Just TypeSpec (Analysis (HoareAnnotation A))
rettype) PrefixSuffix (Analysis (HoareAnnotation A))
_ String
_ Maybe (AList Expression (Analysis (HoareAnnotation A)))
funargs Maybe (Expression (Analysis (HoareAnnotation A)))
retvalue [Block (Analysis (HoareAnnotation A))]
_ Maybe [ProgramUnit (Analysis (HoareAnnotation A))]
_ -> do
      SomeType
rettype' <- ReaderT
  CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
-> StateT CheckHoareEnv BackendAnalysis SomeType
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState (ReaderT
   CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
 -> StateT CheckHoareEnv BackendAnalysis SomeType)
-> ReaderT
     CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
-> StateT CheckHoareEnv BackendAnalysis SomeType
forall a b. (a -> b) -> a -> b
$ TypeInfo (Analysis (HoareAnnotation A))
-> ReaderT
     CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
TypeInfo (Analysis ann) -> m SomeType
tryTranslateTypeInfo (TypeSpec (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall ann. TypeSpec ann -> TypeInfo ann
typeInfo TypeSpec (Analysis (HoareAnnotation A))
rettype)

      let retNames :: NamePair
retNames = case Maybe (Expression (Analysis (HoareAnnotation A)))
retvalue  of
            Just Expression (Analysis (HoareAnnotation A))
rv -> Expression (Analysis (HoareAnnotation A)) -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair Expression (Analysis (HoareAnnotation A))
rv
            Maybe (Expression (Analysis (HoareAnnotation A)))
Nothing -> ProgramUnit (Analysis (HoareAnnotation A)) -> NamePair
forall a. ProgramUnit (Analysis a) -> NamePair
functionNamePair ProgramUnit (Analysis (HoareAnnotation A))
pu

      (CheckHoareEnv -> CheckHoareEnv)
-> StateT CheckHoareEnv BackendAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CheckHoareEnv -> CheckHoareEnv)
 -> StateT CheckHoareEnv BackendAnalysis ())
-> (CheckHoareEnv -> CheckHoareEnv)
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ NamePair -> SomeType -> CheckHoareEnv -> CheckHoareEnv
newVar NamePair
retNames SomeType
rettype'

      [Expression (Analysis (HoareAnnotation A))]
-> StateT
     CheckHoareEnv
     BackendAnalysis
     [Expression (Analysis (HoareAnnotation A))]
forall a. a -> StateT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expression (Analysis (HoareAnnotation A))]
-> (AList Expression (Analysis (HoareAnnotation A))
    -> [Expression (Analysis (HoareAnnotation A))])
-> Maybe (AList Expression (Analysis (HoareAnnotation A)))
-> [Expression (Analysis (HoareAnnotation A))]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] AList Expression (Analysis (HoareAnnotation A))
-> [Expression (Analysis (HoareAnnotation A))]
forall (t :: * -> *) a. AList t a -> [t a]
F.aStrip Maybe (AList Expression (Analysis (HoareAnnotation A)))
funargs)

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

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

  ([Block (Analysis (HoareAnnotation A))]
restBody, [FortranAssignment]
initialAssignments) <- [Block (Analysis (HoareAnnotation A))]
-> CheckHoareMut
     ([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
readInitialBlocks [Block (Analysis (HoareAnnotation A))]
body

  -- 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 (Some FortranVar) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Some FortranVar) -> Bool)
-> StateT CheckHoareEnv BackendAnalysis (Maybe (Some FortranVar))
-> StateT CheckHoareEnv BackendAnalysis Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting
  (Maybe (Some FortranVar)) CheckHoareEnv (Maybe (Some FortranVar))
-> StateT CheckHoareEnv BackendAnalysis (Maybe (Some FortranVar))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
-> CheckHoareEnv -> Const (Maybe (Some FortranVar)) CheckHoareEnv
Lens' CheckHoareEnv ScopeVars
heVarsInScope ((ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
 -> CheckHoareEnv -> Const (Maybe (Some FortranVar)) CheckHoareEnv)
-> ((Maybe (Some FortranVar)
     -> Const (Maybe (Some FortranVar)) (Maybe (Some FortranVar)))
    -> ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
-> Getting
     (Maybe (Some FortranVar)) CheckHoareEnv (Maybe (Some FortranVar))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index ScopeVars -> Lens' ScopeVars (Maybe (IxValue ScopeVars))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at (NamePair
argName NamePair -> Getting UniqueName NamePair UniqueName -> UniqueName
forall s a. s -> Getting a s a -> a
^. Getting UniqueName NamePair UniqueName
Lens' NamePair UniqueName
npUnique))
    Bool
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
hasType (StateT CheckHoareEnv BackendAnalysis ()
 -> StateT CheckHoareEnv BackendAnalysis ())
-> StateT CheckHoareEnv BackendAnalysis ()
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ ProgramUnit (Analysis (HoareAnnotation A))
-> HoareBackendError -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' ProgramUnit (Analysis (HoareAnnotation A))
pu (NamePair -> HoareBackendError
ArgWithoutDecl NamePair
argName)

  ([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
-> CheckHoareMut
     ([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
forall a. a -> StateT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Block (Analysis (HoareAnnotation A))]
restBody, [FortranAssignment]
initialAssignments)


-- | 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 (f :: * -> *).
Functor f =>
(String -> f String) -> AuxDecl ann -> f (AuxDecl ann)
adName
    UniqueName
uniqNm <- String -> StateT CheckHoareEnv BackendAnalysis UniqueName
forall {m :: * -> *}.
MonadState CheckHoareEnv m =>
String -> m UniqueName
uniqueAux String
nm

    let srcNm :: SourceName
srcNm = String -> SourceName
SourceName String
nm
    Map SourceName [UniqueName]
sourceToUnique <- Getting
  (Map SourceName [UniqueName])
  CheckHoareEnv
  (Map SourceName [UniqueName])
-> StateT
     CheckHoareEnv BackendAnalysis (Map SourceName [UniqueName])
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
  (Map SourceName [UniqueName])
  CheckHoareEnv
  (Map SourceName [UniqueName])
Lens' CheckHoareEnv (Map SourceName [UniqueName])
heSourceToUnique

    -- 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 (Analysis (HoareAnnotation A))
-> HoareBackendError -> StateT CheckHoareEnv BackendAnalysis ()
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting
     (ProgramUnit (Analysis (HoareAnnotation A)))
     AnnotatedProgramUnit
     (ProgramUnit (Analysis (HoareAnnotation A)))
-> ProgramUnit (Analysis (HoareAnnotation A))
forall s a. s -> Getting a s a -> a
^. Getting
  (ProgramUnit (Analysis (HoareAnnotation A)))
  AnnotatedProgramUnit
  (ProgramUnit (Analysis (HoareAnnotation A)))
Lens'
  AnnotatedProgramUnit (ProgramUnit (Analysis (HoareAnnotation A)))
apuPU) (HoareBackendError -> StateT CheckHoareEnv BackendAnalysis ())
-> HoareBackendError -> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ String -> HoareBackendError
AuxVarConflict String
nm

    SomeType
ty <- ReaderT
  CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
-> StateT CheckHoareEnv BackendAnalysis SomeType
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState (ReaderT
   CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
 -> StateT CheckHoareEnv BackendAnalysis SomeType)
-> (TypeSpec InnerHA
    -> ReaderT
         CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType)
-> TypeSpec InnerHA
-> StateT CheckHoareEnv BackendAnalysis SomeType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeInfo InnerHA
-> ReaderT
     CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
TypeInfo (Analysis ann) -> m SomeType
tryTranslateTypeInfo (TypeInfo InnerHA
 -> ReaderT
      CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType)
-> (TypeSpec InnerHA -> TypeInfo InnerHA)
-> TypeSpec InnerHA
-> ReaderT
     CheckHoareEnv (StateT CheckHoareEnv BackendAnalysis) SomeType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSpec InnerHA -> TypeInfo InnerHA
forall ann. TypeSpec ann -> TypeInfo ann
typeInfo (TypeSpec InnerHA -> StateT CheckHoareEnv BackendAnalysis SomeType)
-> TypeSpec InnerHA
-> StateT CheckHoareEnv BackendAnalysis SomeType
forall a b. (a -> b) -> a -> b
$ AuxDecl InnerHA
auxDecl AuxDecl InnerHA
-> Getting (TypeSpec InnerHA) (AuxDecl InnerHA) (TypeSpec InnerHA)
-> TypeSpec InnerHA
forall s a. s -> Getting a s a -> a
^. Getting (TypeSpec InnerHA) (AuxDecl InnerHA) (TypeSpec InnerHA)
forall ann1 ann2 (f :: * -> *).
Functor f =>
(TypeSpec ann1 -> f (TypeSpec ann2))
-> AuxDecl ann1 -> f (AuxDecl ann2)
adTy
    (CheckHoareEnv -> CheckHoareEnv)
-> StateT CheckHoareEnv BackendAnalysis ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CheckHoareEnv -> CheckHoareEnv)
 -> StateT CheckHoareEnv BackendAnalysis ())
-> (CheckHoareEnv -> CheckHoareEnv)
-> StateT CheckHoareEnv BackendAnalysis ()
forall a b. (a -> b) -> a -> b
$ NamePair -> SomeType -> CheckHoareEnv -> CheckHoareEnv
newVar (UniqueName -> SourceName -> NamePair
NamePair UniqueName
uniqNm SourceName
srcNm) SomeType
ty
  where
    -- 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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UniqueName -> m UniqueName) -> UniqueName -> m UniqueName
forall a b. (a -> b) -> a -> b
$ String -> UniqueName
UniqueName
             (String -> UniqueName) -> ShowS -> String -> UniqueName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
forall a. HasCallStack => [a] -> a
head
             ([String] -> String) -> (String -> [String]) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile ((UniqueName -> ScopeVars -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` ScopeVars
varsInScope) (UniqueName -> Bool) -> (String -> UniqueName) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> UniqueName
UniqueName)
             ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> String -> [String]
forall a. (a -> a) -> a -> [a]
iterate (Char
' ' Char -> ShowS
forall a. a -> [a] -> [a]
:)
             (String -> UniqueName) -> String -> UniqueName
forall a b. (a -> b) -> a -> b
$ String
nm


-- | 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 (Analysis (HoareAnnotation A))]
-> CheckHoareMut
     ([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
readInitialBlocks = WriterT
  [FortranAssignment]
  (StateT CheckHoareEnv BackendAnalysis)
  [Block (Analysis (HoareAnnotation A))]
-> CheckHoareMut
     ([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT
   [FortranAssignment]
   (StateT CheckHoareEnv BackendAnalysis)
   [Block (Analysis (HoareAnnotation A))]
 -> CheckHoareMut
      ([Block (Analysis (HoareAnnotation A))], [FortranAssignment]))
-> ([Block (Analysis (HoareAnnotation A))]
    -> WriterT
         [FortranAssignment]
         (StateT CheckHoareEnv BackendAnalysis)
         [Block (Analysis (HoareAnnotation A))])
-> [Block (Analysis (HoareAnnotation A))]
-> CheckHoareMut
     ([Block (Analysis (HoareAnnotation A))], [FortranAssignment])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Block (Analysis (HoareAnnotation A))
 -> WriterT
      [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool)
-> [Block (Analysis (HoareAnnotation A))]
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     [Block (Analysis (HoareAnnotation A))]
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
(a -> m Bool) -> [a] -> m [a]
dropWhileM Block (Analysis (HoareAnnotation A))
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
readInitialBlock
  where
    -- 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 (Analysis (HoareAnnotation A))
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
readInitialBlock Block (Analysis (HoareAnnotation A))
bl = case Block (Analysis (HoareAnnotation A))
bl of
      F.BlStatement Analysis (HoareAnnotation A)
_ SrcSpan
_ Maybe (Expression (Analysis (HoareAnnotation A)))
_ Statement (Analysis (HoareAnnotation A))
st ->
        case Statement (Analysis (HoareAnnotation A))
st of
          F.StDeclaration Analysis (HoareAnnotation A)
_ SrcSpan
_ TypeSpec (Analysis (HoareAnnotation A))
astTypeSpec Maybe (AList Attribute (Analysis (HoareAnnotation A)))
attrs AList Declarator (Analysis (HoareAnnotation A))
decls -> do
            -- This is the part of the type info that applies to every variable
            -- in the declaration list.
            let topTypeInfo :: TypeInfo (Analysis (HoareAnnotation A))
topTypeInfo =
                  TypeSpec (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall ann. TypeSpec ann -> TypeInfo ann
typeInfo TypeSpec (Analysis (HoareAnnotation A))
astTypeSpec TypeInfo (Analysis (HoareAnnotation A))
-> (TypeInfo (Analysis (HoareAnnotation A))
    -> TypeInfo (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
forall a b. a -> (a -> b) -> b
&
                  (Maybe (AList Attribute (Analysis (HoareAnnotation A)))
 -> Identity
      (Maybe (AList Attribute (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A)))
forall ann (f :: * -> *).
Functor f =>
(Maybe (AList Attribute ann) -> f (Maybe (AList Attribute ann)))
-> TypeInfo ann -> f (TypeInfo ann)
tiAttributes ((Maybe (AList Attribute (Analysis (HoareAnnotation A)))
  -> Identity
       (Maybe (AList Attribute (Analysis (HoareAnnotation A)))))
 -> TypeInfo (Analysis (HoareAnnotation A))
 -> Identity (TypeInfo (Analysis (HoareAnnotation A))))
-> Maybe (AList Attribute (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (AList Attribute (Analysis (HoareAnnotation A)))
attrs

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

              F.Declarator Analysis (HoareAnnotation A)
_ SrcSpan
_ Expression (Analysis (HoareAnnotation A))
nameExp (F.ArrayDecl AList DimensionDeclarator (Analysis (HoareAnnotation A))
declDims) Maybe (Expression (Analysis (HoareAnnotation A)))
declLength Maybe (Expression (Analysis (HoareAnnotation A)))
mInitialValue -> do
                (Expression (Analysis (HoareAnnotation A)),
 TypeInfo (Analysis (HoareAnnotation A)),
 Maybe (Expression (Analysis (HoareAnnotation A))))
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     (Expression (Analysis (HoareAnnotation A)),
      TypeInfo (Analysis (HoareAnnotation A)),
      Maybe (Expression (Analysis (HoareAnnotation A))))
forall a.
a
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expression (Analysis (HoareAnnotation A))
nameExp,
                        TypeInfo (Analysis (HoareAnnotation A))
topTypeInfo
                        TypeInfo (Analysis (HoareAnnotation A))
-> (TypeInfo (Analysis (HoareAnnotation A))
    -> TypeInfo (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
forall a b. a -> (a -> b) -> b
& (Maybe (Expression (Analysis (HoareAnnotation A)))
 -> Identity (Maybe (Expression (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A)))
forall ann (f :: * -> *).
Functor f =>
(Maybe (Expression ann) -> f (Maybe (Expression ann)))
-> TypeInfo ann -> f (TypeInfo ann)
tiDeclaratorLength ((Maybe (Expression (Analysis (HoareAnnotation A)))
  -> Identity (Maybe (Expression (Analysis (HoareAnnotation A)))))
 -> TypeInfo (Analysis (HoareAnnotation A))
 -> Identity (TypeInfo (Analysis (HoareAnnotation A))))
-> Maybe (Expression (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (Expression (Analysis (HoareAnnotation A)))
declLength
                        TypeInfo (Analysis (HoareAnnotation A))
-> (TypeInfo (Analysis (HoareAnnotation A))
    -> TypeInfo (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
forall a b. a -> (a -> b) -> b
& (Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))
 -> Identity
      (Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))))
-> TypeInfo (Analysis (HoareAnnotation A))
-> Identity (TypeInfo (Analysis (HoareAnnotation A)))
forall ann (f :: * -> *).
Functor f =>
(Maybe (AList DimensionDeclarator ann)
 -> f (Maybe (AList DimensionDeclarator ann)))
-> TypeInfo ann -> f (TypeInfo ann)
tiDimensionDeclarators ((Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))
  -> Identity
       (Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))))
 -> TypeInfo (Analysis (HoareAnnotation A))
 -> Identity (TypeInfo (Analysis (HoareAnnotation A))))
-> Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))
-> TypeInfo (Analysis (HoareAnnotation A))
-> TypeInfo (Analysis (HoareAnnotation A))
forall s t a b. ASetter s t a b -> b -> s -> t
.~ AList DimensionDeclarator (Analysis (HoareAnnotation A))
-> Maybe (AList DimensionDeclarator (Analysis (HoareAnnotation A)))
forall a. a -> Maybe a
Just AList DimensionDeclarator (Analysis (HoareAnnotation A))
declDims,
                        Maybe (Expression (Analysis (HoareAnnotation A)))
mInitialValue)

            [(Expression (Analysis (HoareAnnotation A)),
  TypeInfo (Analysis (HoareAnnotation A)),
  Maybe (Expression (Analysis (HoareAnnotation A))))]
-> ((Expression (Analysis (HoareAnnotation A)),
     TypeInfo (Analysis (HoareAnnotation A)),
     Maybe (Expression (Analysis (HoareAnnotation A))))
    -> WriterT
         [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Expression (Analysis (HoareAnnotation A)),
  TypeInfo (Analysis (HoareAnnotation A)),
  Maybe (Expression (Analysis (HoareAnnotation A))))]
declVarsTis (((Expression (Analysis (HoareAnnotation A)),
   TypeInfo (Analysis (HoareAnnotation A)),
   Maybe (Expression (Analysis (HoareAnnotation A))))
  -> WriterT
       [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
 -> WriterT
      [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> ((Expression (Analysis (HoareAnnotation A)),
     TypeInfo (Analysis (HoareAnnotation A)),
     Maybe (Expression (Analysis (HoareAnnotation A))))
    -> WriterT
         [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ())
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) ()
forall a b. (a -> b) -> a -> b
$ \(Expression (Analysis (HoareAnnotation A))
varNameExp, TypeInfo (Analysis (HoareAnnotation A))
varTypeInfo, Maybe (Expression (Analysis (HoareAnnotation A)))
mInitialValue) -> do
              let varNames :: NamePair
varNames = Expression (Analysis (HoareAnnotation A)) -> NamePair
forall a. Expression (Analysis a) -> NamePair
expNamePair Expression (Analysis (HoareAnnotation A))
varNameExp

              SomeType
varType <- ReaderT
  CheckHoareEnv
  (WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
  SomeType
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) SomeType
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState (ReaderT
   CheckHoareEnv
   (WriterT
      [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
   SomeType
 -> WriterT
      [FortranAssignment]
      (StateT CheckHoareEnv BackendAnalysis)
      SomeType)
-> ReaderT
     CheckHoareEnv
     (WriterT
        [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
     SomeType
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) SomeType
forall a b. (a -> b) -> a -> b
$ TypeInfo (Analysis (HoareAnnotation A))
-> ReaderT
     CheckHoareEnv
     (WriterT
        [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
     SomeType
forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
TypeInfo (Analysis ann) -> m SomeType
tryTranslateTypeInfo TypeInfo (Analysis (HoareAnnotation A))
varTypeInfo

              -- 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 (Analysis (HoareAnnotation A))
 -> WriterT
      [FortranAssignment]
      (StateT CheckHoareEnv BackendAnalysis)
      FortranAssignment)
-> [Expression (Analysis (HoareAnnotation A))]
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     [FortranAssignment]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (ReaderT
  CheckHoareEnv
  (WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
  FortranAssignment
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     FortranAssignment
forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState (ReaderT
   CheckHoareEnv
   (WriterT
      [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
   FortranAssignment
 -> WriterT
      [FortranAssignment]
      (StateT CheckHoareEnv BackendAnalysis)
      FortranAssignment)
-> (Expression (Analysis (HoareAnnotation A))
    -> ReaderT
         CheckHoareEnv
         (WriterT
            [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
         FortranAssignment)
-> Expression (Analysis (HoareAnnotation A))
-> WriterT
     [FortranAssignment]
     (StateT CheckHoareEnv BackendAnalysis)
     FortranAssignment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamePair
-> Expression (Analysis (HoareAnnotation A))
-> ReaderT
     CheckHoareEnv
     (WriterT
        [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis))
     FortranAssignment
forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError Void m, MonadFail m) =>
NamePair -> Expression (Analysis ann) -> m FortranAssignment
simpleAssignment NamePair
varNames)
                          (Maybe (Expression (Analysis (HoareAnnotation A)))
-> [Expression (Analysis (HoareAnnotation A))]
forall a. Maybe a -> [a]
maybeToList Maybe (Expression (Analysis (HoareAnnotation A)))
mInitialValue)

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

          F.StImplicit Analysis (HoareAnnotation A)
_ SrcSpan
_ Maybe (AList ImpList (Analysis (HoareAnnotation A)))
Nothing -> do
            -- TODO: Deal with implicits properly
            Bool
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall a.
a
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
          F.StImplicit Analysis (HoareAnnotation A)
_ SrcSpan
_ (Just AList ImpList (Analysis (HoareAnnotation A))
_) -> Block (Analysis (HoareAnnotation A))
-> HoareBackendError
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block (Analysis (HoareAnnotation A))
bl (Block (Analysis (HoareAnnotation A)) -> HoareBackendError
UnsupportedBlock Block (Analysis (HoareAnnotation A))
bl)
          Statement (Analysis (HoareAnnotation A))
_ -> Bool
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall a.
a
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

      -- Skip comments that don't have sequence annotations
      F.BlComment{} | Maybe (PrimFormula InnerHA)
Nothing <- Block (Analysis (HoareAnnotation A)) -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation Block (Analysis (HoareAnnotation A))
bl -> Bool
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall a.
a
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
      Block (Analysis (HoareAnnotation A))
_ -> Bool
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) Bool
forall a.
a
-> WriterT
     [FortranAssignment] (StateT CheckHoareEnv BackendAnalysis) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False


verifyVc :: (HoareBackendError -> CheckHoare Bool) -> MetaFormula Bool -> CheckHoare Bool
verifyVc :: (HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool)
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT CheckHoareEnv BackendAnalysis Bool
verifyVc HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool
handle Prop (HFree' AllOps FortranVar) Bool
prop = do
  let getSrProp :: HighRepr Bool -> SBool
      getSrProp :: HighRepr Bool -> SBool
getSrProp (HRHigh SBool
x) = SBool
x
      getSrProp (HRCore CoreRepr Bool
_) = String -> SBool
forall a. HasCallStack => String -> a
error String
"absurd"

  let debug :: Bool
debug = Bool
False
      cfg :: SMTConfig
cfg | Bool
debug = SMTConfig
defaultSMTCfg { verbose :: Bool
verbose = Bool
True, transcript :: Maybe String
transcript = String -> Maybe String
forall a. a -> Maybe a
Just String
"transcript.smt2" }
          | Bool
otherwise = SMTConfig
defaultSMTCfg

  PrimReprHandlers
env <- (CheckHoareEnv -> PrimReprHandlers)
-> ReaderT CheckHoareEnv BackendAnalysis PrimReprHandlers
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckHoareEnv -> PrimReprHandlers
forall r. HasPrimReprHandlers r => r -> PrimReprHandlers
primReprHandlers

  let res :: Verifier FortranVar Bool
res = Query FortranVar SBool
-> VarEnv FortranVar -> Verifier FortranVar Bool
forall (v :: * -> *).
VerifiableVar v =>
Query v SBool -> VarEnv v -> Verifier v Bool
query (HighRepr Bool -> SBool
getSrProp (HighRepr Bool -> SBool)
-> Query FortranVar (HighRepr Bool) -> Query FortranVar SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr Bool)
-> PrimReprHandlers -> Query FortranVar (HighRepr Bool)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ((forall a.
 Query FortranVar a
 -> ReaderT PrimReprHandlers (Query FortranVar) a)
-> (forall a.
    VarSym FortranVar a
    -> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr a))
-> Prop (HFree' AllOps FortranVar) Bool
-> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr Bool)
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (m :: * -> *)
       (k :: * -> *) b.
(HMonad expr, HTraversable expr, VerifiableVar v,
 Exception (VerifierError v), HFoldableAt (Compose m k) expr,
 HFoldableAt (Compose m k) LogicOp, Monad m) =>
(forall a. Query v a -> m a)
-> (forall a. VarSym v a -> m (k a)) -> Prop (expr v) b -> m (k b)
evalProp' Query FortranVar a -> ReaderT PrimReprHandlers (Query FortranVar) a
forall a.
Query FortranVar a -> ReaderT PrimReprHandlers (Query FortranVar) a
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT PrimReprHandlers m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (HighRepr a
-> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr a)
forall a. a -> ReaderT PrimReprHandlers (Query FortranVar) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HighRepr a
 -> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr a))
-> (CoreRepr a -> HighRepr a)
-> CoreRepr a
-> ReaderT PrimReprHandlers (Query FortranVar) (HighRepr a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreRepr a -> HighRepr a
forall a. CoreRepr a -> HighRepr a
HRCore) Prop (HFree' AllOps FortranVar) Bool
prop) PrimReprHandlers
env) VarEnv FortranVar
PrimReprHandlers
env
  Either (VerifierError FortranVar) Bool
res' <- IO (Either (VerifierError FortranVar) Bool)
-> ReaderT
     CheckHoareEnv
     BackendAnalysis
     (Either (VerifierError FortranVar) Bool)
forall a. IO a -> ReaderT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either (VerifierError FortranVar) Bool)
 -> ReaderT
      CheckHoareEnv
      BackendAnalysis
      (Either (VerifierError FortranVar) Bool))
-> (Verifier FortranVar Bool
    -> IO (Either (VerifierError FortranVar) Bool))
-> Verifier FortranVar Bool
-> ReaderT
     CheckHoareEnv
     BackendAnalysis
     (Either (VerifierError FortranVar) Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig
-> Verifier FortranVar Bool
-> IO (Either (VerifierError FortranVar) Bool)
forall (v :: * -> *) a.
VerifiableVar v =>
SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)
runVerifierWith SMTConfig
cfg (Verifier FortranVar Bool
 -> ReaderT
      CheckHoareEnv
      BackendAnalysis
      (Either (VerifierError FortranVar) Bool))
-> Verifier FortranVar Bool
-> ReaderT
     CheckHoareEnv
     BackendAnalysis
     (Either (VerifierError FortranVar) Bool)
forall a b. (a -> b) -> a -> b
$ Verifier FortranVar Bool
res

  case Either (VerifierError FortranVar) Bool
res' of
    Right Bool
b -> Bool -> ReaderT CheckHoareEnv BackendAnalysis Bool
forall a. a -> ReaderT CheckHoareEnv BackendAnalysis a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
    Left VerifierError FortranVar
e  -> HoareBackendError -> ReaderT CheckHoareEnv BackendAnalysis Bool
handle (VerifierError FortranVar -> HoareBackendError
VerifierError VerifierError FortranVar
e)

--------------------------------------------------------------------------------
--  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
    ( (forall a b. (a -> b) -> GenM a -> GenM b)
-> (forall a b. a -> GenM b -> GenM a) -> Functor GenM
forall a b. a -> GenM b -> GenM a
forall a b. (a -> b) -> GenM a -> GenM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> GenM a -> GenM b
fmap :: forall a b. (a -> b) -> GenM a -> GenM b
$c<$ :: forall a b. a -> GenM b -> GenM a
<$ :: forall a b. a -> GenM b -> GenM a
Functor
    , Functor GenM
Functor GenM
-> (forall a. a -> GenM a)
-> (forall a b. GenM (a -> b) -> GenM a -> GenM b)
-> (forall a b c. (a -> b -> c) -> GenM a -> GenM b -> GenM c)
-> (forall a b. GenM a -> GenM b -> GenM b)
-> (forall a b. GenM a -> GenM b -> GenM a)
-> Applicative GenM
forall a. a -> GenM a
forall a b. GenM a -> GenM b -> GenM a
forall a b. GenM a -> GenM b -> GenM b
forall a b. GenM (a -> b) -> GenM a -> GenM b
forall a b c. (a -> b -> c) -> GenM a -> GenM b -> GenM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> GenM a
pure :: forall a. a -> GenM a
$c<*> :: forall a b. GenM (a -> b) -> GenM a -> GenM b
<*> :: forall a b. GenM (a -> b) -> GenM a -> GenM b
$cliftA2 :: forall a b c. (a -> b -> c) -> GenM a -> GenM b -> GenM c
liftA2 :: forall a b c. (a -> b -> c) -> GenM a -> GenM b -> GenM c
$c*> :: forall a b. GenM a -> GenM b -> GenM b
*> :: forall a b. GenM a -> GenM b -> GenM b
$c<* :: forall a b. GenM a -> GenM b -> GenM a
<* :: forall a b. GenM a -> GenM b -> GenM a
Applicative
    , Applicative GenM
Applicative GenM
-> (forall a b. GenM a -> (a -> GenM b) -> GenM b)
-> (forall a b. GenM a -> GenM b -> GenM b)
-> (forall a. a -> GenM a)
-> Monad GenM
forall a. a -> GenM a
forall a b. GenM a -> GenM b -> GenM b
forall a b. GenM a -> (a -> GenM b) -> GenM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. GenM a -> (a -> GenM b) -> GenM b
>>= :: forall a b. GenM a -> (a -> GenM b) -> GenM b
$c>> :: forall a b. GenM a -> GenM b -> GenM b
>> :: forall a b. GenM a -> GenM b -> GenM b
$creturn :: forall a. a -> GenM a
return :: forall a. a -> GenM a
Monad
    , MonadReader CheckHoareEnv
    , MonadWriter [MetaFormula Bool]
    , MonadLogger HoareBackendError HoareBackendWarning
    , MonadAnalysis HoareBackendError HoareBackendWarning
    , Monad GenM
Monad GenM -> (forall a. String -> GenM a) -> MonadFail GenM
forall a. String -> GenM a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
$cfail :: forall a. String -> GenM a
fail :: forall a. String -> GenM a
MonadFail
    )


runGenM :: GenM a -> CheckHoare (a, [MetaFormula Bool])
runGenM :: forall a.
GenM a -> CheckHoare (a, [Prop (HFree' AllOps FortranVar) Bool])
runGenM (GenM WriterT
  [Prop (HFree' AllOps FortranVar) Bool]
  (ReaderT CheckHoareEnv BackendAnalysis)
  a
action) = WriterT
  [Prop (HFree' AllOps FortranVar) Bool]
  (ReaderT CheckHoareEnv BackendAnalysis)
  a
-> ReaderT
     CheckHoareEnv
     BackendAnalysis
     (a, [Prop (HFree' AllOps FortranVar) Bool])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT WriterT
  [Prop (HFree' AllOps FortranVar) Bool]
  (ReaderT CheckHoareEnv BackendAnalysis)
  a
action


type FortranTriplet a = Triplet MetaExpr FortranVar a


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

  case AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
seqL AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> AnnSeq
     (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Maybe
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
`joinAnnSeq` AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
seqR of
    Just AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
x -> GenM [()] -> GenM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (GenM [()] -> GenM ()) -> GenM [()] -> GenM ()
forall a b. (a -> b) -> a -> b
$ (Triplet
   (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
 -> GenM ())
-> Triplet
     (HFree' AllOps)
     FortranVar
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> GenM [()]
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (m :: * -> *) cmd
       a.
(HMonad expr, MonadGenVCs expr v m, VerifiableVar v) =>
(Triplet expr v cmd -> m a)
-> Triplet expr v (AnnSeq expr v cmd) -> m [a]
sequenceVCs Triplet
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> GenM ()
genBlock (Prop (HFree' AllOps FortranVar) Bool
precond, Prop (HFree' AllOps FortranVar) Bool
postcond, AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
x)
    Maybe
  (AnnSeq
     (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
Nothing -> [Block (Analysis (HoareAnnotation A))]
-> HoareBackendError -> GenM ()
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' [Block (Analysis (HoareAnnotation A))]
body (HoareBackendError -> GenM ()) -> HoareBackendError -> GenM ()
forall a b. (a -> b) -> a -> b
$ AnnotationError -> HoareBackendError
AnnotationError AnnotationError
MissingSequenceAnn


genBody :: FortranTriplet [F.Block HA] -> GenM ()
genBody :: (Prop (HFree' AllOps FortranVar) Bool,
 Prop (HFree' AllOps FortranVar) Bool,
 [Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody = [FortranAssignment]
-> (Prop (HFree' AllOps FortranVar) Bool,
    Prop (HFree' AllOps FortranVar) Bool,
    [Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody' []


genBlock :: FortranTriplet (F.Block HA) -> GenM ()
genBlock :: Triplet
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> GenM ()
genBlock (Prop (HFree' AllOps FortranVar) Bool
precond, Prop (HFree' AllOps FortranVar) Bool
postcond, Block (Analysis (HoareAnnotation A))
bl) = do
  case Block (Analysis (HoareAnnotation A))
bl of
    F.BlIf Analysis (HoareAnnotation A)
_ SrcSpan
_ Maybe (Expression (Analysis (HoareAnnotation A)))
_ Maybe String
_ NonEmpty
  (Expression (Analysis (HoareAnnotation A)),
   [Block (Analysis (HoareAnnotation A))])
clauses Maybe [Block (Analysis (HoareAnnotation A))]
mElseBlock Maybe (Expression (Analysis (HoareAnnotation A)))
_ -> do
      NonEmpty
  (Maybe (MetaExpr FortranVar Bool),
   [Block (Analysis (HoareAnnotation A))])
clauses' <- (((Expression (Analysis (HoareAnnotation A)),
   [Block (Analysis (HoareAnnotation A))])
  -> GenM
       (Maybe (MetaExpr FortranVar Bool),
        [Block (Analysis (HoareAnnotation A))]))
 -> NonEmpty
      (Expression (Analysis (HoareAnnotation A)),
       [Block (Analysis (HoareAnnotation A))])
 -> GenM
      (NonEmpty
         (Maybe (MetaExpr FortranVar Bool),
          [Block (Analysis (HoareAnnotation A))])))
-> NonEmpty
     (Expression (Analysis (HoareAnnotation A)),
      [Block (Analysis (HoareAnnotation A))])
-> ((Expression (Analysis (HoareAnnotation A)),
     [Block (Analysis (HoareAnnotation A))])
    -> GenM
         (Maybe (MetaExpr FortranVar Bool),
          [Block (Analysis (HoareAnnotation A))]))
-> GenM
     (NonEmpty
        (Maybe (MetaExpr FortranVar Bool),
         [Block (Analysis (HoareAnnotation A))]))
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Expression (Analysis (HoareAnnotation A)),
  [Block (Analysis (HoareAnnotation A))])
 -> GenM
      (Maybe (MetaExpr FortranVar Bool),
       [Block (Analysis (HoareAnnotation A))]))
-> NonEmpty
     (Expression (Analysis (HoareAnnotation A)),
      [Block (Analysis (HoareAnnotation A))])
-> GenM
     (NonEmpty
        (Maybe (MetaExpr FortranVar Bool),
         [Block (Analysis (HoareAnnotation A))]))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse NonEmpty
  (Expression (Analysis (HoareAnnotation A)),
   [Block (Analysis (HoareAnnotation A))])
clauses (((Expression (Analysis (HoareAnnotation A)),
   [Block (Analysis (HoareAnnotation A))])
  -> GenM
       (Maybe (MetaExpr FortranVar Bool),
        [Block (Analysis (HoareAnnotation A))]))
 -> GenM
      (NonEmpty
         (Maybe (MetaExpr FortranVar Bool),
          [Block (Analysis (HoareAnnotation A))])))
-> ((Expression (Analysis (HoareAnnotation A)),
     [Block (Analysis (HoareAnnotation A))])
    -> GenM
         (Maybe (MetaExpr FortranVar Bool),
          [Block (Analysis (HoareAnnotation A))]))
-> GenM
     (NonEmpty
        (Maybe (MetaExpr FortranVar Bool),
         [Block (Analysis (HoareAnnotation A))]))
forall a b. (a -> b) -> a -> b
$ \(Expression (Analysis (HoareAnnotation A))
cond, [Block (Analysis (HoareAnnotation A))]
block) ->
          Expression (Analysis (HoareAnnotation A))
-> GenM (MetaExpr FortranVar Bool)
forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
Expression (Analysis ann) -> m (MetaExpr FortranVar Bool)
tryTranslateBoolExpr Expression (Analysis (HoareAnnotation A))
cond GenM (MetaExpr FortranVar Bool)
-> (MetaExpr FortranVar Bool
    -> GenM
         (Maybe (MetaExpr FortranVar Bool),
          [Block (Analysis (HoareAnnotation A))]))
-> GenM
     (Maybe (MetaExpr FortranVar Bool),
      [Block (Analysis (HoareAnnotation A))])
forall a b. GenM a -> (a -> GenM b) -> GenM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \MetaExpr FortranVar Bool
cond' -> (Maybe (MetaExpr FortranVar Bool),
 [Block (Analysis (HoareAnnotation A))])
-> GenM
     (Maybe (MetaExpr FortranVar Bool),
      [Block (Analysis (HoareAnnotation A))])
forall a. a -> GenM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MetaExpr FortranVar Bool -> Maybe (MetaExpr FortranVar Bool)
forall a. a -> Maybe a
Just MetaExpr FortranVar Bool
cond', [Block (Analysis (HoareAnnotation A))]
block)
      let clauses'' :: [(Maybe (MetaExpr FortranVar Bool),
  [Block (Analysis (HoareAnnotation A))])]
clauses'' = case Maybe [Block (Analysis (HoareAnnotation A))]
mElseBlock of
                        Maybe [Block (Analysis (HoareAnnotation A))]
Nothing ->
                          NonEmpty
  (Maybe (MetaExpr FortranVar Bool),
   [Block (Analysis (HoareAnnotation A))])
-> [(Maybe (MetaExpr FortranVar Bool),
     [Block (Analysis (HoareAnnotation A))])]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty
  (Maybe (MetaExpr FortranVar Bool),
   [Block (Analysis (HoareAnnotation A))])
clauses'
                        Just [Block (Analysis (HoareAnnotation A))]
elseBlock ->
                          NonEmpty
  (Maybe (MetaExpr FortranVar Bool),
   [Block (Analysis (HoareAnnotation A))])
-> [(Maybe (MetaExpr FortranVar Bool),
     [Block (Analysis (HoareAnnotation A))])]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty
  (Maybe (MetaExpr FortranVar Bool),
   [Block (Analysis (HoareAnnotation A))])
clauses' [(Maybe (MetaExpr FortranVar Bool),
  [Block (Analysis (HoareAnnotation A))])]
-> [(Maybe (MetaExpr FortranVar Bool),
     [Block (Analysis (HoareAnnotation A))])]
-> [(Maybe (MetaExpr FortranVar Bool),
     [Block (Analysis (HoareAnnotation A))])]
forall a. [a] -> [a] -> [a]
++ [(Maybe (MetaExpr FortranVar Bool)
forall a. Maybe a
Nothing, [Block (Analysis (HoareAnnotation A))]
elseBlock)]
      ((Prop (HFree' AllOps FortranVar) Bool,
  Prop (HFree' AllOps FortranVar) Bool,
  [Block (Analysis (HoareAnnotation A))])
 -> GenM ())
-> (MetaExpr FortranVar Bool
    -> Prop (HFree' AllOps FortranVar) Bool)
-> Triplet
     (HFree' AllOps)
     FortranVar
     [(Maybe (MetaExpr FortranVar Bool),
       [Block (Analysis (HoareAnnotation A))])]
-> GenM ()
forall (expr :: (* -> *) -> * -> *) (m :: * -> *) (v :: * -> *) cmd
       cond.
(HMonad expr, Monad m) =>
(Triplet expr v cmd -> m ())
-> (cond -> Prop (expr v) Bool)
-> Triplet expr v [(Maybe cond, cmd)]
-> m ()
multiIfVCs (Prop (HFree' AllOps FortranVar) Bool,
 Prop (HFree' AllOps FortranVar) Bool,
 [Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody MetaExpr FortranVar Bool -> Prop (HFree' AllOps FortranVar) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (Prop (HFree' AllOps FortranVar) Bool
precond, Prop (HFree' AllOps FortranVar) Bool
postcond, [(Maybe (MetaExpr FortranVar Bool),
  [Block (Analysis (HoareAnnotation A))])]
clauses'')

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

      Prop (HFree' AllOps FortranVar) Bool
invariant <- [Block (Analysis (HoareAnnotation A))]
-> PrimFormula InnerHA
-> GenM (Prop (HFree' AllOps FortranVar) Bool)
forall o ann (m :: * -> *) w.
(Spanned o, ReportAnn (Analysis ann), Data ann,
 MonadReader CheckHoareEnv m, MonadAnalysis HoareBackendError w m,
 MonadFail m) =>
o
-> PrimFormula (Analysis ann)
-> m (Prop (HFree' AllOps FortranVar) Bool)
tryTranslateFormula [Block (Analysis (HoareAnnotation A))]
body PrimFormula InnerHA
primInvariant
      MetaExpr FortranVar Bool
condExpr <- Expression (Analysis (HoareAnnotation A))
-> GenM (MetaExpr FortranVar Bool)
forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
Expression (Analysis ann) -> m (MetaExpr FortranVar Bool)
tryTranslateBoolExpr Expression (Analysis (HoareAnnotation A))
cond

      ((Prop (HFree' AllOps FortranVar) Bool,
  Prop (HFree' AllOps FortranVar) Bool,
  [Block (Analysis (HoareAnnotation A))])
 -> GenM ())
-> (MetaExpr FortranVar Bool
    -> Prop (HFree' AllOps FortranVar) Bool)
-> Prop (HFree' AllOps FortranVar) Bool
-> Triplet
     (HFree' AllOps)
     FortranVar
     (MetaExpr FortranVar Bool, [Block (Analysis (HoareAnnotation A))])
-> GenM ()
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (m :: * -> *) cmd
       cond.
(HMonad expr, MonadGenVCs expr v m) =>
(Triplet expr v cmd -> m ())
-> (cond -> Prop (expr v) Bool)
-> Prop (expr v) Bool
-> Triplet expr v (cond, cmd)
-> m ()
whileVCs (Prop (HFree' AllOps FortranVar) Bool,
 Prop (HFree' AllOps FortranVar) Bool,
 [Block (Analysis (HoareAnnotation A))])
-> GenM ()
genBody MetaExpr FortranVar Bool -> Prop (HFree' AllOps FortranVar) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr Prop (HFree' AllOps FortranVar) Bool
invariant (Prop (HFree' AllOps FortranVar) Bool
precond, Prop (HFree' AllOps FortranVar) Bool
postcond, (MetaExpr FortranVar Bool
condExpr, [Block (Analysis (HoareAnnotation A))]
body))

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


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


combineBlockSequence
  :: AnnSeq MetaExpr FortranVar (F.Block HA)
  -> F.Block HA
  -> GenM (AnnSeq MetaExpr FortranVar (F.Block HA))
combineBlockSequence :: AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Block (Analysis (HoareAnnotation A))
-> GenM
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
combineBlockSequence AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
prevSeq Block (Analysis (HoareAnnotation A))
bl = do
  AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
blSeq <- Block (Analysis (HoareAnnotation A))
-> GenM
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
blockToSequence Block (Analysis (HoareAnnotation A))
bl

  case AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
prevSeq AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> AnnSeq
     (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> Maybe
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
`joinAnnSeq` AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
blSeq of
    Just AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
r  -> AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
-> GenM
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a. a -> GenM a
forall (m :: * -> *) a. Monad m => a -> m a
return AnnSeq
  (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
r
    Maybe
  (AnnSeq
     (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
Nothing -> Block (Analysis (HoareAnnotation A))
-> HoareBackendError
-> GenM
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block (Analysis (HoareAnnotation A))
bl (HoareBackendError
 -> GenM
      (AnnSeq
         (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
-> HoareBackendError
-> GenM
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a b. (a -> b) -> a -> b
$ AnnotationError -> HoareBackendError
AnnotationError AnnotationError
MissingSequenceAnn


blockToSequence :: F.Block HA -> GenM (AnnSeq MetaExpr FortranVar (F.Block HA))
blockToSequence :: Block (Analysis (HoareAnnotation A))
-> GenM
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
blockToSequence Block (Analysis (HoareAnnotation A))
bl = do
  [GenM
   (Maybe
      (AnnSeq
         (HFree' AllOps)
         FortranVar
         (Block (Analysis (HoareAnnotation A)))))]
-> GenM
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a. [GenM (Maybe a)] -> GenM a
chooseFrom [GenM
  (Maybe
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
assignment, GenM
  (Maybe
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
sequenceSpec, GenM
  (Maybe
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
other]
  where
    assignment :: GenM
  (Maybe
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
assignment = (FortranAssignment
 -> AnnSeq
      (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> Maybe FortranAssignment
-> Maybe
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([FortranAssignment]
-> AnnSeq
     (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
[Assignment expr var] -> AnnSeq expr var cmd
JustAssign ([FortranAssignment]
 -> AnnSeq
      (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> (FortranAssignment -> [FortranAssignment])
-> FortranAssignment
-> AnnSeq
     (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FortranAssignment -> [FortranAssignment] -> [FortranAssignment]
forall a. a -> [a] -> [a]
: [])) (Maybe FortranAssignment
 -> Maybe
      (AnnSeq
         (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
-> GenM (Maybe FortranAssignment)
-> GenM
     (Maybe
        (AnnSeq
           (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Block (Analysis (HoareAnnotation A))
-> GenM (Maybe FortranAssignment)
forall (m :: * -> *).
(MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError Void m, MonadFail m) =>
Block (Analysis (HoareAnnotation A)) -> m (Maybe FortranAssignment)
tryBlockToAssignment Block (Analysis (HoareAnnotation A))
bl

    sequenceSpec :: GenM
  (Maybe
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
sequenceSpec =
      (PrimFormula InnerHA
 -> GenM
      (AnnSeq
         (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
-> Maybe (PrimFormula InnerHA)
-> GenM
     (Maybe
        (AnnSeq
           (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse
      ((Prop (HFree' AllOps FortranVar) Bool
 -> AnnSeq
      (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
-> GenM (Prop (HFree' AllOps FortranVar) Bool)
-> GenM
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall a b. (a -> b) -> GenM a -> GenM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop (HFree' AllOps FortranVar) Bool
-> AnnSeq
     (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
Prop (expr var) Bool -> AnnSeq expr var cmd
propAnnSeq (GenM (Prop (HFree' AllOps FortranVar) Bool)
 -> GenM
      (AnnSeq
         (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A)))))
-> (PrimFormula InnerHA
    -> GenM (Prop (HFree' AllOps FortranVar) Bool))
-> PrimFormula InnerHA
-> GenM
     (AnnSeq
        (HFree' AllOps) FortranVar (Block (Analysis (HoareAnnotation A))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block (Analysis (HoareAnnotation A))
-> PrimFormula InnerHA
-> GenM (Prop (HFree' AllOps FortranVar) Bool)
forall o ann (m :: * -> *) w.
(Spanned o, ReportAnn (Analysis ann), Data ann,
 MonadReader CheckHoareEnv m, MonadAnalysis HoareBackendError w m,
 MonadFail m) =>
o
-> PrimFormula (Analysis ann)
-> m (Prop (HFree' AllOps FortranVar) Bool)
tryTranslateFormula Block (Analysis (HoareAnnotation A))
bl)
      (Block (Analysis (HoareAnnotation A)) -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation Block (Analysis (HoareAnnotation A))
bl)

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

    -- Tries each action in the list, using the first that works and otherwise
    -- reporting an error.
    chooseFrom :: [GenM (Maybe a)] -> GenM a
    chooseFrom :: forall a. [GenM (Maybe a)] -> GenM a
chooseFrom =
      (GenM (Maybe a) -> (Maybe a -> GenM a) -> GenM a
forall a b. GenM a -> (a -> GenM b) -> GenM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GenM a -> Maybe a -> GenM a
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
m a -> Maybe a -> m a
fromMaybeM (Block (Analysis (HoareAnnotation A)) -> HoareBackendError -> GenM a
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Block (Analysis (HoareAnnotation A))
bl (HoareBackendError -> GenM a) -> HoareBackendError -> GenM a
forall a b. (a -> b) -> a -> b
$ AnnotationError -> HoareBackendError
AnnotationError AnnotationError
MissingSequenceAnn)) (GenM (Maybe a) -> GenM a)
-> ([GenM (Maybe a)] -> GenM (Maybe a))
-> [GenM (Maybe a)]
-> GenM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      MaybeT GenM a -> GenM (Maybe a)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT GenM a -> GenM (Maybe a))
-> ([GenM (Maybe a)] -> MaybeT GenM a)
-> [GenM (Maybe a)]
-> GenM (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [MaybeT GenM a] -> MaybeT GenM a
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([MaybeT GenM a] -> MaybeT GenM a)
-> ([GenM (Maybe a)] -> [MaybeT GenM a])
-> [GenM (Maybe a)]
-> MaybeT GenM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenM (Maybe a) -> MaybeT GenM a)
-> [GenM (Maybe a)] -> [MaybeT GenM a]
forall a b. (a -> b) -> [a] -> [b]
map GenM (Maybe a) -> MaybeT GenM a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT


getBlockSeqAnnotation :: F.Block HA -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation :: Block (Analysis (HoareAnnotation A)) -> Maybe (PrimFormula InnerHA)
getBlockSeqAnnotation = Getting
  (First (PrimFormula InnerHA))
  (Block (Analysis (HoareAnnotation A)))
  (PrimFormula InnerHA)
-> Block (Analysis (HoareAnnotation A))
-> Maybe (PrimFormula InnerHA)
forall s (m :: * -> *) a.
MonadReader s m =>
Getting (First a) s a -> m (Maybe a)
preview ((Block (Analysis (HoareAnnotation A))
 -> Analysis (HoareAnnotation A))
-> (Analysis (HoareAnnotation A)
    -> Const
         (First (PrimFormula InnerHA)) (Analysis (HoareAnnotation A)))
-> Block (Analysis (HoareAnnotation A))
-> Const
     (First (PrimFormula InnerHA))
     (Block (Analysis (HoareAnnotation A)))
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to Block (Analysis (HoareAnnotation A))
-> Analysis (HoareAnnotation A)
forall a. Block a -> a
forall (f :: * -> *) a. Annotated f => f a -> a
F.getAnnotation ((Analysis (HoareAnnotation A)
  -> Const
       (First (PrimFormula InnerHA)) (Analysis (HoareAnnotation A)))
 -> Block (Analysis (HoareAnnotation A))
 -> Const
      (First (PrimFormula InnerHA))
      (Block (Analysis (HoareAnnotation A))))
-> ((PrimFormula InnerHA
     -> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
    -> Analysis (HoareAnnotation A)
    -> Const
         (First (PrimFormula InnerHA)) (Analysis (HoareAnnotation A)))
-> Getting
     (First (PrimFormula InnerHA))
     (Block (Analysis (HoareAnnotation A)))
     (PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Analysis (HoareAnnotation A) -> Maybe (SpecOrDecl InnerHA))
-> Optic'
     (->)
     (Const (First (PrimFormula InnerHA)))
     (Analysis (HoareAnnotation A))
     (Maybe (SpecOrDecl InnerHA))
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to Analysis (HoareAnnotation A) -> Maybe (SpecOrDecl InnerHA)
getAnnSod Optic'
  (->)
  (Const (First (PrimFormula InnerHA)))
  (Analysis (HoareAnnotation A))
  (Maybe (SpecOrDecl InnerHA))
-> ((PrimFormula InnerHA
     -> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
    -> Maybe (SpecOrDecl InnerHA)
    -> Const
         (First (PrimFormula InnerHA)) (Maybe (SpecOrDecl InnerHA)))
-> (PrimFormula InnerHA
    -> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> Analysis (HoareAnnotation A)
-> Const
     (First (PrimFormula InnerHA)) (Analysis (HoareAnnotation A))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecOrDecl InnerHA
 -> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA))
-> Maybe (SpecOrDecl InnerHA)
-> Const (First (PrimFormula InnerHA)) (Maybe (SpecOrDecl InnerHA))
forall a b (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe b))
_Just ((SpecOrDecl InnerHA
  -> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA))
 -> Maybe (SpecOrDecl InnerHA)
 -> Const
      (First (PrimFormula InnerHA)) (Maybe (SpecOrDecl InnerHA)))
-> ((PrimFormula InnerHA
     -> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
    -> SpecOrDecl InnerHA
    -> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA))
-> (PrimFormula InnerHA
    -> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> Maybe (SpecOrDecl InnerHA)
-> Const (First (PrimFormula InnerHA)) (Maybe (SpecOrDecl InnerHA))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Specification (PrimFormula InnerHA)
 -> Const
      (First (PrimFormula InnerHA))
      (Specification (PrimFormula InnerHA)))
-> SpecOrDecl InnerHA
-> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA)
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (PrimSpec ann) (f (PrimSpec ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodSpec ((Specification (PrimFormula InnerHA)
  -> Const
       (First (PrimFormula InnerHA))
       (Specification (PrimFormula InnerHA)))
 -> SpecOrDecl InnerHA
 -> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA))
-> ((PrimFormula InnerHA
     -> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
    -> Specification (PrimFormula InnerHA)
    -> Const
         (First (PrimFormula InnerHA))
         (Specification (PrimFormula InnerHA)))
-> (PrimFormula InnerHA
    -> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> SpecOrDecl InnerHA
-> Const (First (PrimFormula InnerHA)) (SpecOrDecl InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula InnerHA
 -> Const (First (PrimFormula InnerHA)) (PrimFormula InnerHA))
-> Specification (PrimFormula InnerHA)
-> Const
     (First (PrimFormula InnerHA)) (Specification (PrimFormula InnerHA))
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f a) -> p (Specification a) (f (Specification a))
_SpecSeq)

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


tryBlockToAssignment
  :: ( MonadReader CheckHoareEnv m
     , MonadAnalysis HoareBackendError HoareBackendWarning m
     , MonadFail m
     )
  => F.Block HA -> m (Maybe FortranAssignment)
tryBlockToAssignment :: forall (m :: * -> *).
(MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError Void m, MonadFail m) =>
Block (Analysis (HoareAnnotation A)) -> m (Maybe FortranAssignment)
tryBlockToAssignment Block (Analysis (HoareAnnotation A))
bl = do
  case Block (Analysis (HoareAnnotation A))
bl of
    F.BlStatement Analysis (HoareAnnotation A)
_ SrcSpan
_ Maybe (Expression (Analysis (HoareAnnotation A)))
_ stAst :: Statement (Analysis (HoareAnnotation A))
stAst@(F.StExpressionAssign Analysis (HoareAnnotation A)
_ SrcSpan
_ Expression (Analysis (HoareAnnotation A))
lexp Expression (Analysis (HoareAnnotation A))
rvalue) ->
      FortranAssignment -> Maybe FortranAssignment
forall a. a -> Maybe a
Just (FortranAssignment -> Maybe FortranAssignment)
-> m FortranAssignment -> m (Maybe FortranAssignment)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        LValue (Analysis (HoareAnnotation A))
lvalue <- m (LValue (Analysis (HoareAnnotation A)))
-> Maybe (LValue (Analysis (HoareAnnotation A)))
-> m (LValue (Analysis (HoareAnnotation A)))
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
m a -> Maybe a -> m a
fromMaybeM (Expression (Analysis (HoareAnnotation A))
-> HoareBackendError -> m (LValue (Analysis (HoareAnnotation A)))
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis (HoareAnnotation A))
lexp HoareBackendError
NonLValueAssignment)
                  (Expression (Analysis (HoareAnnotation A))
-> Maybe (LValue (Analysis (HoareAnnotation A)))
forall a. Expression a -> Maybe (LValue a)
F.toLValue Expression (Analysis (HoareAnnotation A))
lexp)

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

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

              AList Index (Analysis (HoareAnnotation A))
_ -> AList Index (Analysis (HoareAnnotation A))
-> HoareBackendError -> m FortranAssignment
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' AList Index (Analysis (HoareAnnotation A))
ixs (HoareBackendError -> m FortranAssignment)
-> HoareBackendError -> m FortranAssignment
forall a b. (a -> b) -> a -> b
$
                   Text -> HoareBackendError
UnsupportedAssignment Text
"only simple indices are supported for now"
          LValue (Analysis (HoareAnnotation A))
_ -> Statement (Analysis (HoareAnnotation A))
-> HoareBackendError -> m FortranAssignment
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Statement (Analysis (HoareAnnotation A))
stAst (HoareBackendError -> m FortranAssignment)
-> HoareBackendError -> m FortranAssignment
forall a b. (a -> b) -> a -> b
$
               Text -> HoareBackendError
UnsupportedAssignment Text
"complex assignment"

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


-- | 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 :: forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError Void m, MonadFail m) =>
NamePair -> Expression (Analysis ann) -> m FortranAssignment
simpleAssignment NamePair
nm Expression (Analysis ann)
rvalAst = do
  Some varV :: FortranVar a
varV@(FortranVar D a
varD NamePair
_) <- Expression (Analysis ann) -> NamePair -> m (Some FortranVar)
forall a (m :: * -> *).
(Spanned a, MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError Void m, MonadFail m) =>
a -> NamePair -> m (Some FortranVar)
varFromScope Expression (Analysis ann)
rvalAst NamePair
nm

  case D a
varD of
    DPrim Prim p k a1
_ -> do
      MetaExpr FortranVar a
rvalExpr <- D a -> Expression (Analysis ann) -> m (MetaExpr FortranVar a)
forall ann (m :: * -> *) w a.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
D a -> Expression (Analysis ann) -> m (MetaExpr FortranVar a)
tryTranslateCoerceExpr D a
varD Expression (Analysis ann)
rvalAst
      FortranAssignment -> m FortranAssignment
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FortranVar a -> MetaExpr FortranVar a -> FortranAssignment
forall {k} (var :: k -> *) (a :: k) (expr :: (k -> *) -> k -> *).
var a -> expr var a -> Assignment expr var
Assignment FortranVar a
varV MetaExpr FortranVar a
rvalExpr)
    D a
_ -> Expression (Analysis ann)
-> HoareBackendError -> m FortranAssignment
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis ann)
rvalAst (HoareBackendError -> m FortranAssignment)
-> HoareBackendError -> m FortranAssignment
forall a b. (a -> b) -> a -> b
$
         Text -> SomeType -> HoareBackendError
WrongAssignmentType
         Text
"primitive value (others unsupported for now)"
         (D a -> SomeType
forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some D a
varD)

arrayAssignment
  :: ( ReportAnn (F.Analysis ann)
     , MonadReader CheckHoareEnv m
     , MonadAnalysis HoareBackendError HoareBackendWarning m
     , MonadFail m
     )
  => NamePair
  -> F.Expression (F.Analysis ann)
  -> F.Expression (F.Analysis ann)
  -> m FortranAssignment
arrayAssignment :: forall ann (m :: * -> *).
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError Void m, MonadFail m) =>
NamePair
-> Expression (Analysis ann)
-> Expression (Analysis ann)
-> m FortranAssignment
arrayAssignment NamePair
arrName Expression (Analysis ann)
ixAst Expression (Analysis ann)
rvalAst = do
  Some varV :: FortranVar a
varV@(FortranVar D a
varD NamePair
_) <- Expression (Analysis ann) -> NamePair -> m (Some FortranVar)
forall a (m :: * -> *).
(Spanned a, MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError Void m, MonadFail m) =>
a -> NamePair -> m (Some FortranVar)
varFromScope Expression (Analysis ann)
rvalAst NamePair
arrName

  case D a
varD of
    DArray Index i
ixIndex ArrValue a1
valAv -> do
      let ixD :: D i
ixD = Index i -> D i
forall i. Index i -> D i
dIndex Index i
ixIndex
          valD :: D a1
valD = ArrValue a1 -> D a1
forall a. ArrValue a -> D a
dArrValue ArrValue a1
valAv

      MetaExpr FortranVar i
ixExpr   <- HFree CoreOp FortranVar i -> MetaExpr FortranVar i
forall (op :: (* -> *) -> * -> *) (v :: * -> *) a.
(ChooseOp op AllOps, HTraversable op) =>
HFree op v a -> MetaExpr v a
intoMetaExpr (HFree CoreOp FortranVar i -> MetaExpr FortranVar i)
-> m (HFree CoreOp FortranVar i) -> m (MetaExpr FortranVar i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> D i -> Expression (Analysis ann) -> m (HFree CoreOp FortranVar i)
forall ann (m :: * -> *) w a.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
D a -> Expression (Analysis ann) -> m (FortranExpr a)
tryTranslateExpr D i
ixD Expression (Analysis ann)
ixAst
      MetaExpr FortranVar a1
rvalExpr <- HFree CoreOp FortranVar a1 -> MetaExpr FortranVar a1
forall (op :: (* -> *) -> * -> *) (v :: * -> *) a.
(ChooseOp op AllOps, HTraversable op) =>
HFree op v a -> MetaExpr v a
intoMetaExpr (HFree CoreOp FortranVar a1 -> MetaExpr FortranVar a1)
-> m (HFree CoreOp FortranVar a1) -> m (MetaExpr FortranVar a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> D a1 -> Expression (Analysis ann) -> m (HFree CoreOp FortranVar a1)
forall ann (m :: * -> *) w a.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
D a -> Expression (Analysis ann) -> m (FortranExpr a)
tryTranslateExpr D a1
valD Expression (Analysis ann)
rvalAst

      -- 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 a1)
arrExpr' = MetaOp (HFree' AllOps FortranVar) (Array i a1)
-> HFree' AllOps FortranVar (Array i a1)
forall (op :: (* -> *) -> * -> *) (ops :: [(* -> *) -> * -> *])
       (v :: * -> *) a.
(HFunctor op, HFunctor (OpChoice ops), ChooseOp op ops) =>
op (HFree' ops v) a -> HFree' ops v a
hwrap' (MetaOp (HFree' AllOps FortranVar) (Array i a1)
 -> HFree' AllOps FortranVar (Array i a1))
-> MetaOp (HFree' AllOps FortranVar) (Array i a1)
-> HFree' AllOps FortranVar (Array i a1)
forall a b. (a -> b) -> a -> b
$ D (Array i a1)
-> HFree' AllOps FortranVar (Array i a1)
-> MetaExpr FortranVar i
-> MetaExpr FortranVar a1
-> MetaOp (HFree' AllOps FortranVar) (Array i a1)
forall i v (t :: * -> *).
D (Array i v)
-> t (Array i v) -> t i -> t v -> MetaOp t (Array i v)
MopWriteArr D a
D (Array i a1)
varD HFree' AllOps FortranVar a
HFree' AllOps FortranVar (Array i a1)
arrExpr MetaExpr FortranVar i
ixExpr MetaExpr FortranVar a1
rvalExpr

      FortranAssignment -> m FortranAssignment
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FortranVar a -> HFree' AllOps FortranVar a -> FortranAssignment
forall {k} (var :: k -> *) (a :: k) (expr :: (k -> *) -> k -> *).
var a -> expr var a -> Assignment expr var
Assignment FortranVar a
varV HFree' AllOps FortranVar a
HFree' AllOps FortranVar (Array i a1)
arrExpr')

    D a
_ -> Expression (Analysis ann)
-> HoareBackendError -> m FortranAssignment
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis ann)
rvalAst (HoareBackendError -> m FortranAssignment)
-> HoareBackendError -> m FortranAssignment
forall a b. (a -> b) -> a -> b
$ Text -> SomeType -> HoareBackendError
WrongAssignmentType Text
"array type" (D a -> SomeType
forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some D a
varD)

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

varFromScope
  :: ( F.Spanned a
     , MonadReader CheckHoareEnv m
     , MonadAnalysis HoareBackendError HoareBackendWarning m
     , MonadFail m
     )
  => a -> NamePair -> m SomeVar
varFromScope :: forall a (m :: * -> *).
(Spanned a, MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError Void m, MonadFail m) =>
a -> NamePair -> m (Some FortranVar)
varFromScope a
loc NamePair
np = do
  let uniq :: UniqueName
uniq = NamePair
np NamePair -> Getting UniqueName NamePair UniqueName -> UniqueName
forall s a. s -> Getting a s a -> a
^. Getting UniqueName NamePair UniqueName
Lens' NamePair UniqueName
npUnique
  Maybe (Some FortranVar)
mscoped <- Getting
  (Maybe (Some FortranVar)) CheckHoareEnv (Maybe (Some FortranVar))
-> m (Maybe (Some FortranVar))
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
-> CheckHoareEnv -> Const (Maybe (Some FortranVar)) CheckHoareEnv
Lens' CheckHoareEnv ScopeVars
heVarsInScope ((ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
 -> CheckHoareEnv -> Const (Maybe (Some FortranVar)) CheckHoareEnv)
-> ((Maybe (Some FortranVar)
     -> Const (Maybe (Some FortranVar)) (Maybe (Some FortranVar)))
    -> ScopeVars -> Const (Maybe (Some FortranVar)) ScopeVars)
-> Getting
     (Maybe (Some FortranVar)) CheckHoareEnv (Maybe (Some FortranVar))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index ScopeVars -> Lens' ScopeVars (Maybe (IxValue ScopeVars))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index ScopeVars
UniqueName
uniq)
  case Maybe (Some FortranVar)
mscoped of
    Just Some FortranVar
v  -> Some FortranVar -> m (Some FortranVar)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Some FortranVar
v
    Maybe (Some FortranVar)
Nothing -> a -> HoareBackendError -> m (Some FortranVar)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' a
loc (HoareBackendError -> m (Some FortranVar))
-> HoareBackendError -> m (Some FortranVar)
forall a b. (a -> b) -> a -> b
$ NamePair -> HoareBackendError
AssignVarNotInScope NamePair
np

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

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

instance ReportAnn HA      where fromTranslateError :: forall (proxy :: * -> *).
proxy (Analysis (HoareAnnotation A))
-> TranslateError -> HoareBackendError
fromTranslateError proxy (Analysis (HoareAnnotation A))
_ = TranslateError -> HoareBackendError
TranslateErrorSrc
instance ReportAnn InnerHA where fromTranslateError :: forall (proxy :: * -> *).
proxy InnerHA -> TranslateError -> HoareBackendError
fromTranslateError proxy InnerHA
_ = TranslateError -> HoareBackendError
TranslateErrorAnn


doTranslate
  :: (MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m)
  => (HoareBackendError -> m a) -> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate :: forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate HoareBackendError -> m a
handle f ann -> TranslateT m a
trans f ann
ast = do
  TranslateEnv
env <- (CheckHoareEnv -> TranslateEnv) -> m TranslateEnv
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CheckHoareEnv -> TranslateEnv
toTranslateEnv
  Either TranslateError a
transResult <- TranslateT m a -> TranslateEnv -> m (Either TranslateError a)
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
TranslateT m a -> TranslateEnv -> m (Either TranslateError a)
runTranslateT (f ann -> TranslateT m a
trans f ann
ast) TranslateEnv
env
  case Either TranslateError a
transResult of
    Right a
x  -> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
    Left TranslateError
err -> HoareBackendError -> m a
handle (f ann -> TranslateError -> HoareBackendError
forall a (proxy :: * -> *).
ReportAnn a =>
proxy a -> TranslateError -> HoareBackendError
forall (proxy :: * -> *).
proxy ann -> TranslateError -> HoareBackendError
fromTranslateError f ann
ast TranslateError
err)


toTranslateEnv :: CheckHoareEnv -> TranslateEnv
toTranslateEnv :: CheckHoareEnv -> TranslateEnv
toTranslateEnv CheckHoareEnv
env =
  TranslateEnv
defaultTranslateEnv
    TranslateEnv -> (TranslateEnv -> TranslateEnv) -> TranslateEnv
forall a b. a -> (a -> b) -> b
& (Bool -> Identity Bool) -> TranslateEnv -> Identity TranslateEnv
Lens' TranslateEnv Bool
teImplicitVars ((Bool -> Identity Bool) -> TranslateEnv -> Identity TranslateEnv)
-> Bool -> TranslateEnv -> TranslateEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ CheckHoareEnv
env CheckHoareEnv -> Getting Bool CheckHoareEnv Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool CheckHoareEnv Bool
Lens' CheckHoareEnv Bool
heImplicitVars
    TranslateEnv -> (TranslateEnv -> TranslateEnv) -> TranslateEnv
forall a b. a -> (a -> b) -> b
& (ScopeVars -> Identity ScopeVars)
-> TranslateEnv -> Identity TranslateEnv
Lens' TranslateEnv ScopeVars
teVarsInScope ((ScopeVars -> Identity ScopeVars)
 -> TranslateEnv -> Identity TranslateEnv)
-> ScopeVars -> TranslateEnv -> TranslateEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ CheckHoareEnv
env CheckHoareEnv
-> Getting ScopeVars CheckHoareEnv ScopeVars -> ScopeVars
forall s a. s -> Getting a s a -> a
^. Getting ScopeVars CheckHoareEnv ScopeVars
Lens' CheckHoareEnv ScopeVars
heVarsInScope

--------------------------------------------------------------------------------
-- 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 :: forall ann (m :: * -> *) w a.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
D a -> Expression (Analysis ann) -> m (FortranExpr a)
tryTranslateExpr D a
d Expression (Analysis ann)
e = (HoareBackendError -> m (FortranExpr a))
-> (Expression (Analysis ann) -> TranslateT m (FortranExpr a))
-> Expression (Analysis ann)
-> m (FortranExpr a)
forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate (Expression (Analysis ann) -> HoareBackendError -> m (FortranExpr a)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis ann)
e) (D a -> Expression (Analysis ann) -> TranslateT m (FortranExpr a)
forall (m :: * -> *) a ann.
(Monad m, MonadFail m) =>
D a -> Expression (Analysis ann) -> TranslateT m (FortranExpr a)
translateExpression' D a
d) Expression (Analysis ann)
e

tryTranslateCoerceExpr
  :: ( ReportAnn (F.Analysis ann)
     , MonadReader CheckHoareEnv m
     , MonadAnalysis HoareBackendError w m
     , MonadFail m
     )
  => D a -> F.Expression (F.Analysis ann) -> m (MetaExpr FortranVar a)
tryTranslateCoerceExpr :: forall ann (m :: * -> *) w a.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
D a -> Expression (Analysis ann) -> m (MetaExpr FortranVar a)
tryTranslateCoerceExpr D a
d Expression (Analysis ann)
e =
  (HoareBackendError -> m (MetaExpr FortranVar a))
-> (Expression (Analysis ann)
    -> TranslateT m (MetaExpr FortranVar a))
-> Expression (Analysis ann)
-> m (MetaExpr FortranVar a)
forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate (Expression (Analysis ann)
-> HoareBackendError -> m (MetaExpr FortranVar a)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis ann)
e)
  ((HFree MetaOp (HFree CoreOp FortranVar) a -> MetaExpr FortranVar a)
-> TranslateT m (HFree MetaOp (HFree CoreOp FortranVar) a)
-> TranslateT m (MetaExpr FortranVar a)
forall a b. (a -> b) -> TranslateT m a -> TranslateT m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HFree MetaOp (HFree CoreOp FortranVar) a -> MetaExpr FortranVar a
forall (op1 :: (* -> *) -> * -> *) (op2 :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) (v :: * -> *) a.
(HFunctor op1, HFunctor op2, HFunctor (OpChoice ops),
 ChooseOp op1 ops, ChooseOp op2 ops) =>
HFree op1 (HFree op2 v) a -> HFree' ops v a
squashExpression (TranslateT m (HFree MetaOp (HFree CoreOp FortranVar) a)
 -> TranslateT m (MetaExpr FortranVar a))
-> (Expression (Analysis ann)
    -> TranslateT m (HFree MetaOp (HFree CoreOp FortranVar) a))
-> Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. D a
-> Expression (Analysis ann)
-> TranslateT m (HFree MetaOp (HFree CoreOp FortranVar) a)
forall (m :: * -> *) a ann.
(Monad m, MonadFail m) =>
D a
-> Expression (Analysis ann)
-> TranslateT m (HFree MetaOp (HFree CoreOp FortranVar) a)
translateCoerceExpression D a
d) Expression (Analysis ann)
e

tryTranslateTypeInfo
  :: ( ReportAnn (F.Analysis ann)
     , MonadReader CheckHoareEnv m
     , MonadAnalysis HoareBackendError w m
     , MonadFail m
     )
  => TypeInfo (F.Analysis ann) -> m SomeType
tryTranslateTypeInfo :: forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
TypeInfo (Analysis ann) -> m SomeType
tryTranslateTypeInfo TypeInfo (Analysis ann)
ti = (HoareBackendError -> m SomeType)
-> (TypeInfo (Analysis ann) -> TranslateT m SomeType)
-> TypeInfo (Analysis ann)
-> m SomeType
forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate (TypeInfo (Analysis ann) -> HoareBackendError -> m SomeType
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' TypeInfo (Analysis ann)
ti) TypeInfo (Analysis ann) -> TranslateT m SomeType
forall (m :: * -> *) ann.
(Monad m, MonadFail m, Show ann) =>
TypeInfo ann -> TranslateT m SomeType
translateTypeInfo TypeInfo (Analysis ann)
ti

tryTranslateBoolExpr
  :: ( ReportAnn (F.Analysis ann)
     , MonadReader CheckHoareEnv m
     , MonadAnalysis HoareBackendError w m
     , MonadFail m
     )
  => F.Expression (F.Analysis ann) -> m (MetaExpr FortranVar Bool)
tryTranslateBoolExpr :: forall ann (m :: * -> *) w.
(ReportAnn (Analysis ann), MonadReader CheckHoareEnv m,
 MonadAnalysis HoareBackendError w m, MonadFail m) =>
Expression (Analysis ann) -> m (MetaExpr FortranVar Bool)
tryTranslateBoolExpr Expression (Analysis ann)
e = (HoareBackendError -> m (MetaExpr FortranVar Bool))
-> (Expression (Analysis ann)
    -> TranslateT m (MetaExpr FortranVar Bool))
-> Expression (Analysis ann)
-> m (MetaExpr FortranVar Bool)
forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate (Expression (Analysis ann)
-> HoareBackendError -> m (MetaExpr FortranVar Bool)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' Expression (Analysis ann)
e) Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar Bool)
forall (m :: * -> *) ann.
(Monad m, MonadFail m) =>
Expression (Analysis ann)
-> TranslateT m (MetaExpr FortranVar Bool)
translateBoolExpression Expression (Analysis ann)
e

tryTranslateFormula
  :: ( F.Spanned o
     , ReportAnn (F.Analysis ann)
     , Data ann
     , MonadReader CheckHoareEnv m
     , MonadAnalysis HoareBackendError w m
     , MonadFail m
     )
  => o -> PrimFormula (F.Analysis ann) -> m (MetaFormula Bool)
tryTranslateFormula :: forall o ann (m :: * -> *) w.
(Spanned o, ReportAnn (Analysis ann), Data ann,
 MonadReader CheckHoareEnv m, MonadAnalysis HoareBackendError w m,
 MonadFail m) =>
o
-> PrimFormula (Analysis ann)
-> m (Prop (HFree' AllOps FortranVar) Bool)
tryTranslateFormula o
loc PrimFormula (Analysis ann)
formula = do
  Map SourceName [UniqueName]
sourceToUnique <- Getting
  (Map SourceName [UniqueName])
  CheckHoareEnv
  (Map SourceName [UniqueName])
-> m (Map SourceName [UniqueName])
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Map SourceName [UniqueName])
  CheckHoareEnv
  (Map SourceName [UniqueName])
Lens' CheckHoareEnv (Map SourceName [UniqueName])
heSourceToUnique
  -- 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 (HFree' AllOps FortranVar) Bool))
-> (PrimFormula (Analysis ann)
    -> TranslateT m (Prop (HFree' AllOps FortranVar) Bool))
-> PrimFormula (Analysis ann)
-> m (Prop (HFree' AllOps FortranVar) Bool)
forall (m :: * -> *) ann a (f :: * -> *).
(MonadReader CheckHoareEnv m, ReportAnn ann, MonadFail m) =>
(HoareBackendError -> m a)
-> (f ann -> TranslateT m a) -> f ann -> m a
doTranslate (o -> HoareBackendError -> m (Prop (HFree' AllOps FortranVar) Bool)
forall e w (m :: * -> *) o a.
(MonadAnalysis e w m, Spanned o) =>
o -> e -> m a
failAnalysis' o
loc) PrimFormula (Analysis ann)
-> TranslateT m (Prop (HFree' AllOps FortranVar) Bool)
forall (m :: * -> *) ann.
(Monad m, MonadFail m) =>
PrimFormula (Analysis ann)
-> TranslateT m (Prop (HFree' AllOps FortranVar) Bool)
translateFormula PrimFormula (Analysis ann)
formulaUN

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

dropWhileM :: (Monad m, MonadFail m) => (a -> m Bool) -> [a] -> m [a]
dropWhileM :: forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
(a -> m Bool) -> [a] -> m [a]
dropWhileM a -> m Bool
_ [] = [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
dropWhileM a -> m Bool
f (a
x : [a]
xs) = do
  Bool
continue <- a -> m Bool
f a
x
  if Bool
continue
    then (a -> m Bool) -> [a] -> m [a]
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
(a -> m Bool) -> [a] -> m [a]
dropWhileM a -> m Bool
f [a]
xs
    else [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs)


fromMaybeM :: (Monad m, MonadFail m) => m a -> Maybe a -> m a
fromMaybeM :: forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
m a -> Maybe a -> m a
fromMaybeM m a
e = m a -> (a -> m a) -> Maybe a -> m a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m a
e a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return


getAnnSod :: HA -> Maybe (SpecOrDecl InnerHA)
getAnnSod :: Analysis (HoareAnnotation A) -> Maybe (SpecOrDecl InnerHA)
getAnnSod = Getting
  (Maybe (SpecOrDecl InnerHA))
  (Analysis (HoareAnnotation A))
  (Maybe (SpecOrDecl InnerHA))
-> Analysis (HoareAnnotation A) -> Maybe (SpecOrDecl InnerHA)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((Analysis (HoareAnnotation A) -> HoareAnnotation A)
-> (HoareAnnotation A
    -> Const (Maybe (SpecOrDecl InnerHA)) (HoareAnnotation A))
-> Analysis (HoareAnnotation A)
-> Const
     (Maybe (SpecOrDecl InnerHA)) (Analysis (HoareAnnotation A))
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to Analysis (HoareAnnotation A) -> HoareAnnotation A
forall a. Analysis a -> a
F.prevAnnotation ((HoareAnnotation A
  -> Const (Maybe (SpecOrDecl InnerHA)) (HoareAnnotation A))
 -> Analysis (HoareAnnotation A)
 -> Const
      (Maybe (SpecOrDecl InnerHA)) (Analysis (HoareAnnotation A)))
-> ((Maybe (SpecOrDecl InnerHA)
     -> Const (Maybe (SpecOrDecl InnerHA)) (Maybe (SpecOrDecl InnerHA)))
    -> HoareAnnotation A
    -> Const (Maybe (SpecOrDecl InnerHA)) (HoareAnnotation A))
-> Getting
     (Maybe (SpecOrDecl InnerHA))
     (Analysis (HoareAnnotation A))
     (Maybe (SpecOrDecl InnerHA))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (SpecOrDecl InnerHA)
 -> Const (Maybe (SpecOrDecl InnerHA)) (Maybe (SpecOrDecl InnerHA)))
-> HoareAnnotation A
-> Const (Maybe (SpecOrDecl InnerHA)) (HoareAnnotation A)
forall a (f :: * -> *).
Functor f =>
(Maybe (SpecOrDecl InnerHA) -> f (Maybe (SpecOrDecl InnerHA)))
-> HoareAnnotation a -> f (HoareAnnotation a)
hoareSod)


lvVarNames :: F.LValue (F.Analysis x) -> NamePair
lvVarNames :: forall x. LValue (Analysis x) -> NamePair
lvVarNames LValue (Analysis x)
e =
  let uniqueName :: UniqueName
uniqueName = String -> UniqueName
UniqueName (String -> UniqueName) -> String -> UniqueName
forall a b. (a -> b) -> a -> b
$ LValue (Analysis x) -> String
forall a. LValue (Analysis a) -> String
F.lvVarName LValue (Analysis x)
e
      srcName :: SourceName
srcName = String -> SourceName
SourceName (String -> SourceName) -> String -> SourceName
forall a b. (a -> b) -> a -> b
$ LValue (Analysis x) -> String
forall a. LValue (Analysis a) -> String
F.lvSrcName LValue (Analysis x)
e
  in UniqueName -> SourceName -> NamePair
NamePair UniqueName
uniqueName SourceName
srcName


readerOfState :: (MonadState s m) => ReaderT s m a -> m a
readerOfState :: forall s (m :: * -> *) a. MonadState s m => ReaderT s m a -> m a
readerOfState ReaderT s m a
action = do
  s
st <- m s
forall s (m :: * -> *). MonadState s m => m s
get
  ReaderT s m a -> s -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT s m a
action s
st