{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE RankNTypes                 #-}

{-# OPTIONS_GHC -Wall #-}

{-|

This module is responsible for finding annotated program units, and running the
functionality in "Camfort.Specification.Hoare.CheckBackend" on each of them.

-}
module Camfort.Specification.Hoare.CheckFrontend
  (
    -- * Invariant Checking
    invariantChecking

    -- * Analysis Types
  , HoareAnalysis
  , HoareFrontendError(..)
  , HoareFrontendWarning(..)
  ) where

import           Control.Applicative                      (liftA2)
import           Control.Exception
import           Control.Lens
import           Control.Monad.Writer.Lazy                hiding (Product)
import           Data.Generics.Uniplate.Operations
import           Data.Map                                 (Map)
import qualified Data.Map                                 as Map
import           Data.Maybe                               (catMaybes)
import           Data.Void                                (absurd)

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

import           Camfort.Analysis
import qualified Camfort.Analysis.Annotations             as CA
import           Camfort.Analysis.CommentAnnotator
import           Camfort.Specification.Parser             (SpecParseError)

import           Language.Fortran.Model.Repr.Prim

import           Camfort.Specification.Hoare.Annotation
import           Camfort.Specification.Hoare.CheckBackend
import           Camfort.Specification.Hoare.Parser
import           Camfort.Specification.Hoare.Parser.Types (HoareParseError)
import           Camfort.Specification.Hoare.Syntax

import           Control.DeepSeq

--------------------------------------------------------------------------------
--  Invariant Checking
--------------------------------------------------------------------------------

{-|
Runs invariant checking on every annotated program unit in the given program
file. Expects the program file to have basic block and unique analysis
information.

The 'PrimReprSpec' argument controls how Fortran data types are treated
symbolically. See the documentation in "Language.Fortran.Mode.Repr.Prim" for a
detailed explanation.
-}
invariantChecking :: PrimReprSpec -> F.ProgramFile HA -> HoareAnalysis [HoareCheckResult]
invariantChecking :: PrimReprSpec -> ProgramFile HA -> HoareAnalysis [HoareCheckResult]
invariantChecking PrimReprSpec
primSpec ProgramFile HA
pf = do
  let parserWithAnns :: SpecParser HoareParseError (SpecOrDecl InnerHA)
parserWithAnns = SpecOrDecl A -> SpecOrDecl InnerHA
forall (b :: * -> *) a. Functor b => b a -> b (Analysis a)
F.initAnalysis (SpecOrDecl A -> SpecOrDecl InnerHA)
-> (SpecOrDecl () -> SpecOrDecl A)
-> SpecOrDecl ()
-> SpecOrDecl InnerHA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> A) -> SpecOrDecl () -> SpecOrDecl A
forall a b. (a -> b) -> SpecOrDecl a -> SpecOrDecl b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (A -> () -> A
forall a b. a -> b -> a
const A
CA.unitAnnotation) (SpecOrDecl () -> SpecOrDecl InnerHA)
-> SpecParser HoareParseError (SpecOrDecl ())
-> SpecParser HoareParseError (SpecOrDecl InnerHA)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecParser HoareParseError (SpecOrDecl ())
hoareParser

  ProgramFile HA
pf' <- SpecParser HoareParseError (SpecOrDecl InnerHA)
-> (SrcSpan
    -> SpecParseError HoareParseError
    -> AnalysisT HoareFrontendError HoareFrontendWarning IO ())
-> ProgramFile HA
-> AnalysisT
     HoareFrontendError HoareFrontendWarning IO (ProgramFile HA)
forall (m :: * -> *) e a ast.
(Monad m, Data a, Linkable a, ASTEmbeddable a ast) =>
SpecParser e ast
-> (SrcSpan -> SpecParseError e -> m ())
-> ProgramFile a
-> m (ProgramFile a)
annotateComments SpecParser HoareParseError (SpecOrDecl InnerHA)
parserWithAnns SrcSpan
-> SpecParseError HoareParseError
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
parseError ProgramFile HA
pf
  [AnnotatedProgramUnit]
annotatedPUs <- ProgramFile HA -> HoareAnalysis [AnnotatedProgramUnit]
findAnnotatedPUs ProgramFile HA
pf'

  let checkAndReport :: AnnotatedProgramUnit
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
checkAndReport AnnotatedProgramUnit
apu = do
        let nm :: ProgramUnitName
nm = ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
-> ProgramUnit HA
forall s a. s -> Getting a s a -> a
^. Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
Lens' AnnotatedProgramUnit (ProgramUnit HA)
apuPU)
            prettyName :: Text
prettyName = String -> Text
forall a. Describe a => a -> Text
describe (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ case ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puSrcName (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
-> ProgramUnit HA
forall s a. s -> Getting a s a -> a
^. Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
Lens' AnnotatedProgramUnit (ProgramUnit HA)
apuPU) of
              F.Named String
x -> String
x
              ProgramUnitName
_         -> ProgramUnitName -> String
forall a. Show a => a -> String
show ProgramUnitName
nm
        ProgramUnit HA -> Text -> AnalysisT HoareFrontendError w IO ()
forall a.
Spanned a =>
a -> Text -> AnalysisT HoareFrontendError w IO ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
-> ProgramUnit HA
forall s a. s -> Getting a s a -> a
^. Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
Lens' AnnotatedProgramUnit (ProgramUnit HA)
apuPU) (Text -> AnalysisT HoareFrontendError w IO ())
-> Text -> AnalysisT HoareFrontendError w IO ()
forall a b. (a -> b) -> a -> b
$ Text
"Verifying program unit: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
prettyName
        AnalysisT HoareFrontendError w IO HoareCheckResult
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
forall (m :: * -> *) w e a.
(Monad m, Describe w, Describe e) =>
AnalysisT e w m a -> AnalysisT e w m (Maybe a)
loggingAnalysisError (AnalysisT HoareFrontendError w IO HoareCheckResult
 -> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult))
-> (BackendAnalysis HoareCheckResult
    -> AnalysisT HoareFrontendError w IO HoareCheckResult)
-> BackendAnalysis HoareCheckResult
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HoareBackendError -> HoareFrontendError)
-> (HoareBackendWarning -> w)
-> BackendAnalysis HoareCheckResult
-> AnalysisT HoareFrontendError w IO HoareCheckResult
forall (m :: * -> *) e e' w w' a.
Monad m =>
(e -> e') -> (w -> w') -> AnalysisT e w m a -> AnalysisT e' w' m a
mapAnalysisT HoareBackendError -> HoareFrontendError
BackendError HoareBackendWarning -> w
forall a. HoareBackendWarning -> a
absurd (BackendAnalysis HoareCheckResult
 -> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult))
-> BackendAnalysis HoareCheckResult
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
forall a b. (a -> b) -> a -> b
$ AnnotatedProgramUnit
-> PrimReprSpec -> BackendAnalysis HoareCheckResult
checkPU AnnotatedProgramUnit
apu PrimReprSpec
primSpec

  [Maybe HoareCheckResult] -> [HoareCheckResult]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe HoareCheckResult] -> [HoareCheckResult])
-> AnalysisT
     HoareFrontendError HoareFrontendWarning IO [Maybe HoareCheckResult]
-> HoareAnalysis [HoareCheckResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AnnotatedProgramUnit
 -> AnalysisT
      HoareFrontendError
      HoareFrontendWarning
      IO
      (Maybe HoareCheckResult))
-> [AnnotatedProgramUnit]
-> AnalysisT
     HoareFrontendError HoareFrontendWarning IO [Maybe HoareCheckResult]
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 AnnotatedProgramUnit
-> AnalysisT
     HoareFrontendError HoareFrontendWarning IO (Maybe HoareCheckResult)
forall {w}.
Describe w =>
AnnotatedProgramUnit
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
checkAndReport [AnnotatedProgramUnit]
annotatedPUs

--------------------------------------------------------------------------------
--  Results and errors
--------------------------------------------------------------------------------

type HoareAnalysis = AnalysisT HoareFrontendError HoareFrontendWarning IO

data HoareFrontendError
  = ParseError (SpecParseError HoareParseError)
  | InvalidPUConditions F.ProgramUnitName [SpecOrDecl InnerHA]
  | BackendError HoareBackendError

instance NFData HoareFrontendError where
  rnf :: HoareFrontendError -> ()
rnf HoareFrontendError
_ = ()

data HoareFrontendWarning
  = OrphanDecls F.ProgramUnitName

instance NFData HoareFrontendWarning where
  rnf :: HoareFrontendWarning -> ()
rnf HoareFrontendWarning
_ = ()

instance Describe HoareFrontendError where
  describeBuilder :: HoareFrontendError -> Builder
describeBuilder = \case
    ParseError SpecParseError HoareParseError
spe -> Builder
"parse error: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (SpecParseError HoareParseError -> String
forall e. Exception e => e -> String
displayException SpecParseError HoareParseError
spe)
    InvalidPUConditions ProgramUnitName
nm [SpecOrDecl InnerHA]
conds ->
      Builder
"invalid specification types attached to PU with name " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (ProgramUnitName -> String
forall a. Show a => a -> String
show ProgramUnitName
nm) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
": " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
      String -> Builder
forall a. Describe a => a -> Builder
describeBuilder ([SpecOrDecl InnerHA] -> String
forall a. Show a => a -> String
show [SpecOrDecl InnerHA]
conds)
    BackendError HoareBackendError
e -> HoareBackendError -> Builder
forall a. Describe a => a -> Builder
describeBuilder HoareBackendError
e

instance Describe HoareFrontendWarning where
  describeBuilder :: HoareFrontendWarning -> Builder
describeBuilder = \case
    OrphanDecls ProgramUnitName
nm ->
      Builder
"auxiliary variable declared for a program unit with no annotations with name " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
      String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (ProgramUnitName -> String
forall a. Show a => a -> String
show ProgramUnitName
nm) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"; skipping invariant checking for this program unit"

--------------------------------------------------------------------------------
--  Internal
--------------------------------------------------------------------------------

parseError :: F.SrcSpan -> SpecParseError HoareParseError -> HoareAnalysis ()
parseError :: SrcSpan
-> SpecParseError HoareParseError
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
parseError SrcSpan
sp SpecParseError HoareParseError
err = SrcSpan
-> HoareFrontendError
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall a.
Spanned a =>
a
-> HoareFrontendError
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> e -> m ()
logError' SrcSpan
sp (SpecParseError HoareParseError -> HoareFrontendError
ParseError SpecParseError HoareParseError
err)

-- | Finds all annotated program units in the given program file. Throws errors
-- for program units that are incorrectly annotated. Returns a list of program
-- units which are correctly annotated at the top level.
findAnnotatedPUs :: F.ProgramFile HA -> HoareAnalysis [AnnotatedProgramUnit]
findAnnotatedPUs :: ProgramFile HA -> HoareAnalysis [AnnotatedProgramUnit]
findAnnotatedPUs ProgramFile HA
pf =
  let pusByName :: Map F.ProgramUnitName (F.ProgramUnit HA)
      pusByName :: Map ProgramUnitName (ProgramUnit HA)
pusByName = [(ProgramUnitName, ProgramUnit HA)]
-> Map ProgramUnitName (ProgramUnit HA)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName ProgramUnit HA
pu, ProgramUnit HA
pu) | ProgramUnit HA
pu <- ProgramFile HA -> [ProgramUnit HA]
forall from to. Biplate from to => from -> [to]
universeBi ProgramFile HA
pf]

      -- Each annotation may get linked with one program unit. However, for this
      -- analysis we want to collect all of the annotations that are associated
      -- with the same program unit. For this we need to do some extra work
      -- because the comment annotator can't directly deal with this situation.
      sodsByPU :: Map F.ProgramUnitName [SpecOrDecl InnerHA]
      sodsByPU :: Map ProgramUnitName [SpecOrDecl InnerHA]
sodsByPU = ([SpecOrDecl InnerHA]
 -> [SpecOrDecl InnerHA] -> [SpecOrDecl InnerHA])
-> [(ProgramUnitName, [SpecOrDecl InnerHA])]
-> Map ProgramUnitName [SpecOrDecl InnerHA]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [SpecOrDecl InnerHA]
-> [SpecOrDecl InnerHA] -> [SpecOrDecl InnerHA]
forall a. [a] -> [a] -> [a]
(++)
        [ (ProgramUnitName
nm, [SpecOrDecl InnerHA
sod])
        | HA
ann <- ProgramFile HA -> [HA]
forall from to. Biplate from to => from -> [to]
universeBi ProgramFile HA
pf :: [HA]
        , ProgramUnitName
nm  <- HA -> HoareAnnotation A
forall a. Analysis a -> a
F.prevAnnotation HA
ann HoareAnnotation A
-> Getting
     (Endo [ProgramUnitName]) (HoareAnnotation A) ProgramUnitName
-> [ProgramUnitName]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (Maybe ProgramUnitName
 -> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName))
-> HoareAnnotation A
-> Const (Endo [ProgramUnitName]) (HoareAnnotation A)
forall a (f :: * -> *).
Functor f =>
(Maybe ProgramUnitName -> f (Maybe ProgramUnitName))
-> HoareAnnotation a -> f (HoareAnnotation a)
hoarePUName ((Maybe ProgramUnitName
  -> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName))
 -> HoareAnnotation A
 -> Const (Endo [ProgramUnitName]) (HoareAnnotation A))
-> ((ProgramUnitName
     -> Const (Endo [ProgramUnitName]) ProgramUnitName)
    -> Maybe ProgramUnitName
    -> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName))
-> Getting
     (Endo [ProgramUnitName]) (HoareAnnotation A) ProgramUnitName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProgramUnitName -> Const (Endo [ProgramUnitName]) ProgramUnitName)
-> Maybe ProgramUnitName
-> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName)
forall a b (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe b))
_Just
        , SpecOrDecl InnerHA
sod <- HA -> HoareAnnotation A
forall a. Analysis a -> a
F.prevAnnotation HA
ann HoareAnnotation A
-> Getting
     (Endo [SpecOrDecl InnerHA])
     (HoareAnnotation A)
     (SpecOrDecl InnerHA)
-> [SpecOrDecl InnerHA]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (Maybe (SpecOrDecl InnerHA)
 -> Const (Endo [SpecOrDecl InnerHA]) (Maybe (SpecOrDecl InnerHA)))
-> HoareAnnotation A
-> Const (Endo [SpecOrDecl InnerHA]) (HoareAnnotation A)
forall a (f :: * -> *).
Functor f =>
(Maybe (SpecOrDecl InnerHA) -> f (Maybe (SpecOrDecl InnerHA)))
-> HoareAnnotation a -> f (HoareAnnotation a)
hoareSod    ((Maybe (SpecOrDecl InnerHA)
  -> Const (Endo [SpecOrDecl InnerHA]) (Maybe (SpecOrDecl InnerHA)))
 -> HoareAnnotation A
 -> Const (Endo [SpecOrDecl InnerHA]) (HoareAnnotation A))
-> ((SpecOrDecl InnerHA
     -> Const (Endo [SpecOrDecl InnerHA]) (SpecOrDecl InnerHA))
    -> Maybe (SpecOrDecl InnerHA)
    -> Const (Endo [SpecOrDecl InnerHA]) (Maybe (SpecOrDecl InnerHA)))
-> Getting
     (Endo [SpecOrDecl InnerHA])
     (HoareAnnotation A)
     (SpecOrDecl InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecOrDecl InnerHA
 -> Const (Endo [SpecOrDecl InnerHA]) (SpecOrDecl InnerHA))
-> Maybe (SpecOrDecl InnerHA)
-> Const (Endo [SpecOrDecl InnerHA]) (Maybe (SpecOrDecl InnerHA))
forall a b (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe b))
_Just
        ]

      -- For a given program unit and list of associated specifications, create
      -- an annotated program unit, and report an error if something is wrong.
      collectUnit
        :: F.ProgramUnit HA -> [SpecOrDecl InnerHA]
        -> HoareAnalysis (Maybe AnnotatedProgramUnit)
      collectUnit :: ProgramUnit HA
-> [SpecOrDecl InnerHA]
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
collectUnit ProgramUnit HA
pu [SpecOrDecl InnerHA]
sods = do
        let pres :: [PrimFormula InnerHA]
pres  = [SpecOrDecl InnerHA]
sods [SpecOrDecl InnerHA]
-> Getting
     (Endo [PrimFormula InnerHA])
     [SpecOrDecl InnerHA]
     (PrimFormula InnerHA)
-> [PrimFormula InnerHA]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (SpecOrDecl InnerHA
 -> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> [SpecOrDecl InnerHA]
-> Const (Endo [PrimFormula InnerHA]) [SpecOrDecl InnerHA]
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 ((SpecOrDecl InnerHA
  -> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
 -> [SpecOrDecl InnerHA]
 -> Const (Endo [PrimFormula InnerHA]) [SpecOrDecl InnerHA])
-> ((PrimFormula InnerHA
     -> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
    -> SpecOrDecl InnerHA
    -> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> Getting
     (Endo [PrimFormula InnerHA])
     [SpecOrDecl InnerHA]
     (PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimSpec InnerHA
 -> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [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 ((PrimSpec InnerHA
  -> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
 -> SpecOrDecl InnerHA
 -> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> ((PrimFormula InnerHA
     -> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
    -> PrimSpec InnerHA
    -> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
-> (PrimFormula InnerHA
    -> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula InnerHA
 -> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> PrimSpec InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA)
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f a) -> p (Specification a) (f (Specification a))
_SpecPre
            posts :: [PrimFormula InnerHA]
posts = [SpecOrDecl InnerHA]
sods [SpecOrDecl InnerHA]
-> Getting
     (Endo [PrimFormula InnerHA])
     [SpecOrDecl InnerHA]
     (PrimFormula InnerHA)
-> [PrimFormula InnerHA]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (SpecOrDecl InnerHA
 -> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> [SpecOrDecl InnerHA]
-> Const (Endo [PrimFormula InnerHA]) [SpecOrDecl InnerHA]
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 ((SpecOrDecl InnerHA
  -> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
 -> [SpecOrDecl InnerHA]
 -> Const (Endo [PrimFormula InnerHA]) [SpecOrDecl InnerHA])
-> ((PrimFormula InnerHA
     -> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
    -> SpecOrDecl InnerHA
    -> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> Getting
     (Endo [PrimFormula InnerHA])
     [SpecOrDecl InnerHA]
     (PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimSpec InnerHA
 -> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [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 ((PrimSpec InnerHA
  -> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
 -> SpecOrDecl InnerHA
 -> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> ((PrimFormula InnerHA
     -> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
    -> PrimSpec InnerHA
    -> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
-> (PrimFormula InnerHA
    -> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula InnerHA
 -> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> PrimSpec InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA)
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f a) -> p (Specification a) (f (Specification a))
_SpecPost
            decls :: [AuxDecl InnerHA]
decls = [SpecOrDecl InnerHA]
sods [SpecOrDecl InnerHA]
-> Getting
     (Endo [AuxDecl InnerHA]) [SpecOrDecl InnerHA] (AuxDecl InnerHA)
-> [AuxDecl InnerHA]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (SpecOrDecl InnerHA
 -> Const (Endo [AuxDecl InnerHA]) (SpecOrDecl InnerHA))
-> [SpecOrDecl InnerHA]
-> Const (Endo [AuxDecl InnerHA]) [SpecOrDecl InnerHA]
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 ((SpecOrDecl InnerHA
  -> Const (Endo [AuxDecl InnerHA]) (SpecOrDecl InnerHA))
 -> [SpecOrDecl InnerHA]
 -> Const (Endo [AuxDecl InnerHA]) [SpecOrDecl InnerHA])
-> ((AuxDecl InnerHA
     -> Const (Endo [AuxDecl InnerHA]) (AuxDecl InnerHA))
    -> SpecOrDecl InnerHA
    -> Const (Endo [AuxDecl InnerHA]) (SpecOrDecl InnerHA))
-> Getting
     (Endo [AuxDecl InnerHA]) [SpecOrDecl InnerHA] (AuxDecl InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AuxDecl InnerHA
 -> Const (Endo [AuxDecl InnerHA]) (AuxDecl InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [AuxDecl InnerHA]) (SpecOrDecl InnerHA)
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (AuxDecl ann) (f (AuxDecl ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodDecl

            errors :: [SpecOrDecl InnerHA]
errors = (SpecOrDecl InnerHA -> Bool)
-> [SpecOrDecl InnerHA] -> [SpecOrDecl InnerHA]
forall a. (a -> Bool) -> [a] -> [a]
filter (APrism
  (SpecOrDecl InnerHA)
  (SpecOrDecl InnerHA)
  (PrimFormula InnerHA)
  (PrimFormula InnerHA)
-> SpecOrDecl InnerHA -> Bool
forall s t a b. APrism s t a b -> s -> Bool
isn't (Market
  (PrimFormula InnerHA)
  (PrimFormula InnerHA)
  (PrimSpec InnerHA)
  (Identity (PrimSpec InnerHA))
-> Market
     (PrimFormula InnerHA)
     (PrimFormula InnerHA)
     (SpecOrDecl InnerHA)
     (Identity (SpecOrDecl InnerHA))
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (PrimSpec ann) (f (PrimSpec ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodSpec (Market
   (PrimFormula InnerHA)
   (PrimFormula InnerHA)
   (PrimSpec InnerHA)
   (Identity (PrimSpec InnerHA))
 -> Market
      (PrimFormula InnerHA)
      (PrimFormula InnerHA)
      (SpecOrDecl InnerHA)
      (Identity (SpecOrDecl InnerHA)))
-> (Market
      (PrimFormula InnerHA)
      (PrimFormula InnerHA)
      (PrimFormula InnerHA)
      (Identity (PrimFormula InnerHA))
    -> Market
         (PrimFormula InnerHA)
         (PrimFormula InnerHA)
         (PrimSpec InnerHA)
         (Identity (PrimSpec InnerHA)))
-> APrism
     (SpecOrDecl InnerHA)
     (SpecOrDecl InnerHA)
     (PrimFormula InnerHA)
     (PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Market
  (PrimFormula InnerHA)
  (PrimFormula InnerHA)
  (PrimFormula InnerHA)
  (Identity (PrimFormula InnerHA))
-> Market
     (PrimFormula InnerHA)
     (PrimFormula InnerHA)
     (PrimSpec InnerHA)
     (Identity (PrimSpec InnerHA))
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f a) -> p (Specification a) (f (Specification a))
_SpecPre ) (SpecOrDecl InnerHA -> Bool)
-> (SpecOrDecl InnerHA -> Bool) -> SpecOrDecl InnerHA -> Bool
.&&
                             APrism
  (SpecOrDecl InnerHA)
  (SpecOrDecl InnerHA)
  (PrimFormula InnerHA)
  (PrimFormula InnerHA)
-> SpecOrDecl InnerHA -> Bool
forall s t a b. APrism s t a b -> s -> Bool
isn't (Market
  (PrimFormula InnerHA)
  (PrimFormula InnerHA)
  (PrimSpec InnerHA)
  (Identity (PrimSpec InnerHA))
-> Market
     (PrimFormula InnerHA)
     (PrimFormula InnerHA)
     (SpecOrDecl InnerHA)
     (Identity (SpecOrDecl InnerHA))
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (PrimSpec ann) (f (PrimSpec ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodSpec (Market
   (PrimFormula InnerHA)
   (PrimFormula InnerHA)
   (PrimSpec InnerHA)
   (Identity (PrimSpec InnerHA))
 -> Market
      (PrimFormula InnerHA)
      (PrimFormula InnerHA)
      (SpecOrDecl InnerHA)
      (Identity (SpecOrDecl InnerHA)))
-> (Market
      (PrimFormula InnerHA)
      (PrimFormula InnerHA)
      (PrimFormula InnerHA)
      (Identity (PrimFormula InnerHA))
    -> Market
         (PrimFormula InnerHA)
         (PrimFormula InnerHA)
         (PrimSpec InnerHA)
         (Identity (PrimSpec InnerHA)))
-> APrism
     (SpecOrDecl InnerHA)
     (SpecOrDecl InnerHA)
     (PrimFormula InnerHA)
     (PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Market
  (PrimFormula InnerHA)
  (PrimFormula InnerHA)
  (PrimFormula InnerHA)
  (Identity (PrimFormula InnerHA))
-> Market
     (PrimFormula InnerHA)
     (PrimFormula InnerHA)
     (PrimSpec InnerHA)
     (Identity (PrimSpec InnerHA))
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f a) -> p (Specification a) (f (Specification a))
_SpecPost) (SpecOrDecl InnerHA -> Bool)
-> (SpecOrDecl InnerHA -> Bool) -> SpecOrDecl InnerHA -> Bool
.&&
                             APrism
  (SpecOrDecl InnerHA)
  (SpecOrDecl InnerHA)
  (AuxDecl InnerHA)
  (AuxDecl InnerHA)
-> SpecOrDecl InnerHA -> Bool
forall s t a b. APrism s t a b -> s -> Bool
isn't APrism
  (SpecOrDecl InnerHA)
  (SpecOrDecl InnerHA)
  (AuxDecl InnerHA)
  (AuxDecl InnerHA)
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (AuxDecl ann) (f (AuxDecl ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodDecl)
                     [SpecOrDecl InnerHA]
sods
              where .&& :: (SpecOrDecl InnerHA -> Bool)
-> (SpecOrDecl InnerHA -> Bool) -> SpecOrDecl InnerHA -> Bool
(.&&) = (Bool -> Bool -> Bool)
-> (SpecOrDecl InnerHA -> Bool)
-> (SpecOrDecl InnerHA -> Bool)
-> SpecOrDecl InnerHA
-> Bool
forall a b c.
(a -> b -> c)
-> (SpecOrDecl InnerHA -> a)
-> (SpecOrDecl InnerHA -> b)
-> SpecOrDecl InnerHA
-> c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&)

            result :: AnnotatedProgramUnit
result = [PrimFormula InnerHA]
-> [PrimFormula InnerHA]
-> [AuxDecl InnerHA]
-> ProgramUnit HA
-> AnnotatedProgramUnit
AnnotatedProgramUnit [PrimFormula InnerHA]
pres [PrimFormula InnerHA]
posts [AuxDecl InnerHA]
decls ProgramUnit HA
pu

        Bool
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([SpecOrDecl InnerHA] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SpecOrDecl InnerHA]
errors) (AnalysisT HoareFrontendError HoareFrontendWarning IO ()
 -> AnalysisT HoareFrontendError HoareFrontendWarning IO ())
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall a b. (a -> b) -> a -> b
$ ProgramUnit HA
-> HoareFrontendError
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall a.
Spanned a =>
a
-> HoareFrontendError
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> e -> m ()
logError' ProgramUnit HA
pu (ProgramUnitName -> [SpecOrDecl InnerHA] -> HoareFrontendError
InvalidPUConditions (ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName ProgramUnit HA
pu) [SpecOrDecl InnerHA]
errors)

        if [PrimFormula InnerHA] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PrimFormula InnerHA]
pres Bool -> Bool -> Bool
&& [PrimFormula InnerHA] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PrimFormula InnerHA]
posts
          then do
            Bool
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([AuxDecl InnerHA] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AuxDecl InnerHA]
decls) (AnalysisT HoareFrontendError HoareFrontendWarning IO ()
 -> AnalysisT HoareFrontendError HoareFrontendWarning IO ())
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall a b. (a -> b) -> a -> b
$ ProgramUnit HA
-> HoareFrontendWarning
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall a.
Spanned a =>
a
-> HoareFrontendWarning
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> w -> m ()
logWarn' ProgramUnit HA
pu (ProgramUnitName -> HoareFrontendWarning
OrphanDecls (ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName ProgramUnit HA
pu))
            Maybe AnnotatedProgramUnit
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
forall a.
a -> AnalysisT HoareFrontendError HoareFrontendWarning IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe AnnotatedProgramUnit
forall a. Maybe a
Nothing
          else Maybe AnnotatedProgramUnit
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
forall a.
a -> AnalysisT HoareFrontendError HoareFrontendWarning IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe AnnotatedProgramUnit
 -> HoareAnalysis (Maybe AnnotatedProgramUnit))
-> Maybe AnnotatedProgramUnit
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
forall a b. (a -> b) -> a -> b
$ AnnotatedProgramUnit -> Maybe AnnotatedProgramUnit
forall a. a -> Maybe a
Just AnnotatedProgramUnit
result

      apus :: [HoareAnalysis (Maybe AnnotatedProgramUnit)]
      apus :: [HoareAnalysis (Maybe AnnotatedProgramUnit)]
apus = ((ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))
 -> HoareAnalysis (Maybe AnnotatedProgramUnit))
-> [(ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))]
-> [HoareAnalysis (Maybe AnnotatedProgramUnit)]
forall a b. (a -> b) -> [a] -> [b]
map (ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
forall a b. (a, b) -> b
snd ([(ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))]
 -> [HoareAnalysis (Maybe AnnotatedProgramUnit)])
-> (Map
      ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
    -> [(ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))])
-> Map ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
-> [HoareAnalysis (Maybe AnnotatedProgramUnit)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
-> [(ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))]
forall k a. Map k a -> [(k, a)]
Map.toList (Map ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
 -> [HoareAnalysis (Maybe AnnotatedProgramUnit)])
-> Map ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
-> [HoareAnalysis (Maybe AnnotatedProgramUnit)]
forall a b. (a -> b) -> a -> b
$ (ProgramUnit HA
 -> [SpecOrDecl InnerHA]
 -> HoareAnalysis (Maybe AnnotatedProgramUnit))
-> Map ProgramUnitName (ProgramUnit HA)
-> Map ProgramUnitName [SpecOrDecl InnerHA]
-> Map ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith ProgramUnit HA
-> [SpecOrDecl InnerHA]
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
collectUnit Map ProgramUnitName (ProgramUnit HA)
pusByName Map ProgramUnitName [SpecOrDecl InnerHA]
sodsByPU

  in [Maybe AnnotatedProgramUnit] -> [AnnotatedProgramUnit]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe AnnotatedProgramUnit] -> [AnnotatedProgramUnit])
-> AnalysisT
     HoareFrontendError
     HoareFrontendWarning
     IO
     [Maybe AnnotatedProgramUnit]
-> HoareAnalysis [AnnotatedProgramUnit]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HoareAnalysis (Maybe AnnotatedProgramUnit)]
-> AnalysisT
     HoareFrontendError
     HoareFrontendWarning
     IO
     [Maybe AnnotatedProgramUnit]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [HoareAnalysis (Maybe AnnotatedProgramUnit)]
apus