content: {-# LANGUAGE OverloadedStrings #-}
  
  {-|
  
  Hoare-logic-based invariant annotation and automated checking for Fortran.
  
  = Annotations
  
  Programs must be annotation in order to check them. Annotations are of the form
  
  == Static assertions
  
  @
  != static_assert <keyword> (<logic_expression>)
  @
  
  The possible keywords are
  
    [@pre@] program unit preconditions.
  
    [@post@] program unit postconditions.
  
    [@seq@] invariants between program statements.
  
    [@invariant@] loop invariant annotations.
  
  == Logical Expressions
  
  A logical expression is an expression formed from quoted Fortran expressions
  combined with an arbitrary combination of the logical operators
  
    [ @&@ ] conjunction
  
    [ @|@ ] disjunction
  
    [ @->@ ] implication
  
    [ @\<-\>@ ] bi-implication, equivalence
  
    [ @!@ ] negation
  
  For example,
  
  @
  "x >= 3" & ("y = 7" | "y = z")
  @
  
  is a valid logical expression.
  
  == Variables
  
  In logical expressions, you may use any Fortran variables that are declared in
  the associated program unit, and you may use an annotated function's return
  variable as long as it has a declared type (i.e. the function's name unless
  otherwise specified). In addition, you may declare auxiliary variables using the
  syntax
  
  @
  != decl_aux("\<type spec\>" :: \<name\>)
  @
  
    [@\<type spec\>@] an arbitrary Fortran type specification, such as
      @integer@ or @real(kind=8,dimensions=(3,4))@
  
    [@\<name\>@] any string (case-insensitive) that is a valid Fortran
      identifier, such as @my_var123@.
  
  Using any undeclared variables will result in an error.
  
  == Necessary Annotations
  
  Annotations are required at the following program points:
  
  * Between any two statements @S1@ and @S2@, where @S2@ is not an assignment.
  * On the line after @do ...@.
  
  == Unsupported Program Constructs
  
  Many parts of Fortran are currently unsupported. You will receive a helpful
  error message if you try to use something that's unsupported. Notable
  unsupported constructs are:
  
  * Standard @do@ loops (@do while@ loops /are/ supported)
  * Multi-dimensional arrays
  * User-defined data types
  * Program sub-units
  * Intrinsic functions
  * @write@, @read@, etc
  * Subroutine and function calls
  
  == Example
  
  Here's an example of a properly annotated Fortran program:
  
  @
  != decl_aux("integer" :: x_)
  != decl_aux("integer" :: y_)
  != static_assert pre("x == x_" & "y == y_")
  != static_assert post("multiply == x_ * y_")
  integer function multiply(x, y)
    implicit none
  
    integer :: x, y
    integer :: r, n
  
    if (x < 0) then
       x = -x
       y = -y
    end if
  
    r = 0
    n = 0
    != static_assert seq("x * y == x_ * y_" & "n == 0" & "r == 0" & "n <= x")
    do while (n < x)
       != static_assert invariant("x * y == x_ * y_" & "r == n * y" & "n <= x")
       r = r + y
       n = n + 1
    end do
  
    multiply = r
  end function multiply
  @
  
  -}
  module Camfort.Specification.Hoare (check, HoareCheckResults(..), PrimReprOption(..)) where
  
  import           Camfort.Analysis
  import           Camfort.Analysis.Annotations
  import           Camfort.Specification.Hoare.Annotation
  import           Camfort.Specification.Hoare.CheckBackend
  import           Camfort.Specification.Hoare.CheckFrontend
  import           Control.DeepSeq
  import           Data.List                                 (intersperse)
  import qualified Language.Fortran.AST                      as F
  import qualified Language.Fortran.Analysis                 as FA
  import qualified Language.Fortran.Analysis.BBlocks         as FAB
  import qualified Language.Fortran.Analysis.Renaming        as FAR
  import           Language.Fortran.Model.Repr.Prim
  
  
  --------------------------------------------------------------------------------
  --  Types
  --------------------------------------------------------------------------------
  
  newtype HoareCheckResults = HoareCheckResults [HoareCheckResult]
  
  instance NFData HoareCheckResults where
    rnf _ = ()
  
  instance ExitCodeOfReport HoareCheckResults where
    exitCodeOf (HoareCheckResults rs) = exitCodeOfSet rs
  
  instance Describe HoareCheckResults where
    describeBuilder (HoareCheckResults rs) =
      mconcat . intersperse "\n" . map describeBuilder $ rs
  
  -- TODO: Give more control here
  data PrimReprOption = PROIdealized | PROPrecise
  
  --------------------------------------------------------------------------------
  --  Checking
  --------------------------------------------------------------------------------
  
  {-|
  The main entry point for the invariant checking analysis. Runs invariant
  checking on every annotated program unit in the given program file.
  
  The 'PrimReprOption' argument controls how Fortran data types are treated
  symbolically. See the documentation in "Language.Fortran.Model.Repr.Prim" for a
  detailed explanation.
  -}
  check :: PrimReprOption
        -> F.ProgramFile Annotation
        -> HoareAnalysis HoareCheckResults
  check pro = fmap HoareCheckResults . invariantChecking (fromPrimReprOption pro) . getBlocks
  
  --------------------------------------------------------------------------------
  --  Internal
  --------------------------------------------------------------------------------
  
  getBlocks :: F.ProgramFile A -> F.ProgramFile (FA.Analysis (HoareAnnotation A))
  getBlocks =
    FAB.analyseBBlocks . FAR.analyseRenames .
    FA.initAnalysis . fmap hoareAnn0
  
  -- defaultSymSpec :: PrimReprSpec
  -- defaultSymSpec = prsIdealized
  
  fromPrimReprOption :: PrimReprOption -> PrimReprSpec
  fromPrimReprOption PROIdealized = prsIdealized
  fromPrimReprOption PROPrecise = prsPrecise
  
  --------------------------------------------------------------------------------
  --  Testsing
  --------------------------------------------------------------------------------
  
  -- testOn :: FilePath -> IO ()
  -- testOn fp = do
  --   (mfs, pfsSources) <- loadModAndProgramFiles Nothing simpleCompiler () fp fp []
  --   describePerFileAnalysis
  --     "invariant checking"
  --     (check PROIdealized)
  --     (logOutputStd True)
  --     LogDebug
  --     False
  --     mfs
  --     pfsSources
  --   return ()
  
  -- testHoare = do
  --   testOn "camfort/samples/invariants/arrays.f90"
  --   testOn "camfort/samples/invariants/invariants.f90"
  