{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE LambdaCase         #-}
{-# OPTIONS_GHC -Wall #-}

module Camfort.Specification.Hoare.Parser.Types where

import           Control.Monad.Except
import           Data.Data
import           Control.Exception
import           Data.List               ( intercalate )

import qualified Data.ByteString.Char8    as B

import qualified Language.Fortran.AST     as F
import           Language.Fortran.Version ( FortranVersion(..) )

-- for temporary definition defined in new fortran-src version, copied here
import           Language.Fortran.AST ( A0, Statement )
import           Language.Fortran.Parser ( Parser, makeParserFixed, makeParserFree )
import qualified Language.Fortran.Parser.Fixed.Fortran66  as F66
import qualified Language.Fortran.Parser.Fixed.Fortran77  as F77
import qualified Language.Fortran.Parser.Free.Fortran90   as F90
import qualified Language.Fortran.Parser.Free.Fortran95   as F95
import qualified Language.Fortran.Parser.Free.Fortran2003 as F2003

data HoareParseError
  = UnmatchedQuote
  | UnexpectedInput
  | MalformedExpression String
  | MalformedTypeSpec String
  | ParseError [Token]
  | LexError String
  deriving (HoareParseError -> HoareParseError -> Bool
(HoareParseError -> HoareParseError -> Bool)
-> (HoareParseError -> HoareParseError -> Bool)
-> Eq HoareParseError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HoareParseError -> HoareParseError -> Bool
== :: HoareParseError -> HoareParseError -> Bool
$c/= :: HoareParseError -> HoareParseError -> Bool
/= :: HoareParseError -> HoareParseError -> Bool
Eq, Eq HoareParseError
Eq HoareParseError
-> (HoareParseError -> HoareParseError -> Ordering)
-> (HoareParseError -> HoareParseError -> Bool)
-> (HoareParseError -> HoareParseError -> Bool)
-> (HoareParseError -> HoareParseError -> Bool)
-> (HoareParseError -> HoareParseError -> Bool)
-> (HoareParseError -> HoareParseError -> HoareParseError)
-> (HoareParseError -> HoareParseError -> HoareParseError)
-> Ord HoareParseError
HoareParseError -> HoareParseError -> Bool
HoareParseError -> HoareParseError -> Ordering
HoareParseError -> HoareParseError -> HoareParseError
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: HoareParseError -> HoareParseError -> Ordering
compare :: HoareParseError -> HoareParseError -> Ordering
$c< :: HoareParseError -> HoareParseError -> Bool
< :: HoareParseError -> HoareParseError -> Bool
$c<= :: HoareParseError -> HoareParseError -> Bool
<= :: HoareParseError -> HoareParseError -> Bool
$c> :: HoareParseError -> HoareParseError -> Bool
> :: HoareParseError -> HoareParseError -> Bool
$c>= :: HoareParseError -> HoareParseError -> Bool
>= :: HoareParseError -> HoareParseError -> Bool
$cmax :: HoareParseError -> HoareParseError -> HoareParseError
max :: HoareParseError -> HoareParseError -> HoareParseError
$cmin :: HoareParseError -> HoareParseError -> HoareParseError
min :: HoareParseError -> HoareParseError -> HoareParseError
Ord, Typeable, Typeable HoareParseError
Typeable HoareParseError
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> HoareParseError -> c HoareParseError)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HoareParseError)
-> (HoareParseError -> Constr)
-> (HoareParseError -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HoareParseError))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c HoareParseError))
-> ((forall b. Data b => b -> b)
    -> HoareParseError -> HoareParseError)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HoareParseError -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HoareParseError -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> HoareParseError -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> HoareParseError -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> HoareParseError -> m HoareParseError)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> HoareParseError -> m HoareParseError)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> HoareParseError -> m HoareParseError)
-> Data HoareParseError
HoareParseError -> Constr
HoareParseError -> DataType
(forall b. Data b => b -> b) -> HoareParseError -> HoareParseError
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> HoareParseError -> u
forall u. (forall d. Data d => d -> u) -> HoareParseError -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HoareParseError -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HoareParseError -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> HoareParseError -> m HoareParseError
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> HoareParseError -> m HoareParseError
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HoareParseError
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HoareParseError -> c HoareParseError
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HoareParseError)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HoareParseError)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HoareParseError -> c HoareParseError
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HoareParseError -> c HoareParseError
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HoareParseError
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HoareParseError
$ctoConstr :: HoareParseError -> Constr
toConstr :: HoareParseError -> Constr
$cdataTypeOf :: HoareParseError -> DataType
dataTypeOf :: HoareParseError -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HoareParseError)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HoareParseError)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HoareParseError)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HoareParseError)
$cgmapT :: (forall b. Data b => b -> b) -> HoareParseError -> HoareParseError
gmapT :: (forall b. Data b => b -> b) -> HoareParseError -> HoareParseError
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HoareParseError -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HoareParseError -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HoareParseError -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HoareParseError -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> HoareParseError -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> HoareParseError -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> HoareParseError -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> HoareParseError -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> HoareParseError -> m HoareParseError
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> HoareParseError -> m HoareParseError
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> HoareParseError -> m HoareParseError
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> HoareParseError -> m HoareParseError
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> HoareParseError -> m HoareParseError
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> HoareParseError -> m HoareParseError
Data)

instance Show HoareParseError where
  show :: HoareParseError -> [Char]
show HoareParseError
UnmatchedQuote = [Char]
"unmatched quote"
  show HoareParseError
UnexpectedInput = [Char]
"unexpected characters in input"
  show (MalformedExpression [Char]
expr) = [Char]
"couldn't parse expression: \"" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
expr [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\""
  show (MalformedTypeSpec [Char]
ts) = [Char]
"couldn't parse type spec: \"" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
ts [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\""
  show (ParseError [Token]
tokens) = [Char]
"unable to parse input: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Token] -> [Char]
prettyTokens [Token]
tokens
  show (LexError [Char]
xs) = [Char]
"unable to lex input: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
xs

instance Exception HoareParseError where

prettyTokens :: [Token] -> String
prettyTokens :: [Token] -> [Char]
prettyTokens = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" " ([[Char]] -> [Char]) -> ([Token] -> [[Char]]) -> [Token] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token -> [Char]) -> [Token] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Token -> [Char]
prettyToken
  where
    prettyToken :: Token -> [Char]
prettyToken = \case
      TQuoted [Char]
qv -> [Char]
"\"" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
qv [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\""
      Token
TStaticAssert -> [Char]
"static_assert"
      Token
TPre -> [Char]
"pre"
      Token
TPost -> [Char]
"post"
      Token
TInvariant -> [Char]
"invariant"
      Token
TSeq -> [Char]
"seq"
      Token
TRParen -> [Char]
")"
      Token
TLParen -> [Char]
"("
      Token
TAnd -> [Char]
"&"
      Token
TOr -> [Char]
"|"
      Token
TImpl -> [Char]
"->"
      Token
TEquiv -> [Char]
"<->"
      Token
TNot -> [Char]
"!"
      Token
TTrue -> [Char]
"T"
      Token
TFalse -> [Char]
"F"
      Token
TDeclAux -> [Char]
"decl_aux"
      TName [Char]
nm -> [Char]
nm
      Token
TDColon -> [Char]
"::"

type HoareSpecParser = Either HoareParseError

data Token =

  -- Quoted Fortran --
    TQuoted String

  -- Static Assertions --
  | TStaticAssert
  | TPre
  | TPost
  | TInvariant
  | TSeq
  | TRParen
  | TLParen
  | TAnd
  | TOr
  | TImpl
  | TEquiv
  | TNot
  | TTrue
  | TFalse

  -- Auxiliary variable declarations --
  | TDeclAux
  | TName String
  | TDColon
  deriving (Int -> Token -> ShowS
[Token] -> ShowS
Token -> [Char]
(Int -> Token -> ShowS)
-> (Token -> [Char]) -> ([Token] -> ShowS) -> Show Token
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Token -> ShowS
showsPrec :: Int -> Token -> ShowS
$cshow :: Token -> [Char]
show :: Token -> [Char]
$cshowList :: [Token] -> ShowS
showList :: [Token] -> ShowS
Show, Token -> Token -> Bool
(Token -> Token -> Bool) -> (Token -> Token -> Bool) -> Eq Token
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Token -> Token -> Bool
== :: Token -> Token -> Bool
$c/= :: Token -> Token -> Bool
/= :: Token -> Token -> Bool
Eq, Eq Token
Eq Token
-> (Token -> Token -> Ordering)
-> (Token -> Token -> Bool)
-> (Token -> Token -> Bool)
-> (Token -> Token -> Bool)
-> (Token -> Token -> Bool)
-> (Token -> Token -> Token)
-> (Token -> Token -> Token)
-> Ord Token
Token -> Token -> Bool
Token -> Token -> Ordering
Token -> Token -> Token
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Token -> Token -> Ordering
compare :: Token -> Token -> Ordering
$c< :: Token -> Token -> Bool
< :: Token -> Token -> Bool
$c<= :: Token -> Token -> Bool
<= :: Token -> Token -> Bool
$c> :: Token -> Token -> Bool
> :: Token -> Token -> Bool
$c>= :: Token -> Token -> Bool
>= :: Token -> Token -> Bool
$cmax :: Token -> Token -> Token
max :: Token -> Token -> Token
$cmin :: Token -> Token -> Token
min :: Token -> Token -> Token
Ord, Typeable, Typeable Token
Typeable Token
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Token -> c Token)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Token)
-> (Token -> Constr)
-> (Token -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Token))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Token))
-> ((forall b. Data b => b -> b) -> Token -> Token)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Token -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Token -> r)
-> (forall u. (forall d. Data d => d -> u) -> Token -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Token -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Token -> m Token)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Token -> m Token)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Token -> m Token)
-> Data Token
Token -> Constr
Token -> DataType
(forall b. Data b => b -> b) -> Token -> Token
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Token -> u
forall u. (forall d. Data d => d -> u) -> Token -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Token -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Token -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Token -> m Token
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Token -> m Token
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Token
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Token -> c Token
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Token)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Token)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Token -> c Token
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Token -> c Token
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Token
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Token
$ctoConstr :: Token -> Constr
toConstr :: Token -> Constr
$cdataTypeOf :: Token -> DataType
dataTypeOf :: Token -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Token)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Token)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Token)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Token)
$cgmapT :: (forall b. Data b => b -> b) -> Token -> Token
gmapT :: (forall b. Data b => b -> b) -> Token -> Token
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Token -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Token -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Token -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Token -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Token -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Token -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Token -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Token -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Token -> m Token
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Token -> m Token
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Token -> m Token
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Token -> m Token
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Token -> m Token
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Token -> m Token
Data)

-- TODO: Make this report errors and deal with source position better
parseExpression :: FortranVersion -> String -> HoareSpecParser (F.Expression ())
parseExpression :: FortranVersion -> [Char] -> HoareSpecParser (Expression ())
parseExpression FortranVersion
v [Char]
strExpr =
  case FortranVersion -> Parser (Statement ())
byVerStmt FortranVersion
v [Char]
"<unknown>" ByteString
paddedBsExpr of
    Right (F.StExpressionAssign ()
_ SrcSpan
_ Expression ()
_ Expression ()
e) -> Expression () -> HoareSpecParser (Expression ())
forall a. a -> Either HoareParseError a
forall (m :: * -> *) a. Monad m => a -> m a
return Expression ()
e
    Either ParseErrorSimple (Statement ())
_ -> HoareParseError -> HoareSpecParser (Expression ())
forall a. HoareParseError -> Either HoareParseError a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([Char] -> HoareParseError
MalformedExpression [Char]
strExpr)
  where
    paddedBsExpr :: ByteString
paddedBsExpr = [Char] -> ByteString
B.pack ([Char] -> ByteString) -> [Char] -> ByteString
forall a b. (a -> b) -> a -> b
$ [Char]
"      a = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
strExpr


-- TODO: Make this report errors and deal with source position better
parseTypeSpec :: FortranVersion -> String -> HoareSpecParser (F.TypeSpec ())
parseTypeSpec :: FortranVersion -> [Char] -> HoareSpecParser (TypeSpec ())
parseTypeSpec FortranVersion
v [Char]
strTs =
  case FortranVersion -> Parser (Statement ())
byVerStmt FortranVersion
v [Char]
"<unknown>" ByteString
paddedBsTs of
    Right (F.StDeclaration ()
_ SrcSpan
_ TypeSpec ()
s Maybe (AList Attribute ())
_ AList Declarator ()
_) -> TypeSpec () -> HoareSpecParser (TypeSpec ())
forall a. a -> Either HoareParseError a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeSpec ()
s
    Either ParseErrorSimple (Statement ())
_ -> HoareParseError -> HoareSpecParser (TypeSpec ())
forall a. HoareParseError -> Either HoareParseError a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([Char] -> HoareParseError
MalformedTypeSpec [Char]
strTs)
  where
    paddedBsTs :: ByteString
paddedBsTs = [Char] -> ByteString
B.pack ([Char] -> ByteString) -> [Char] -> ByteString
forall a b. (a -> b) -> a -> b
$ [Char]
strTs [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" :: dummy"

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

f66StmtNoTransform, f77StmtNoTransform, f77eStmtNoTransform, f77lStmtNoTransform,
  f90StmtNoTransform, f95StmtNoTransform, f2003StmtNoTransform
    :: Parser (Statement A0)
f66StmtNoTransform :: Parser (Statement ())
f66StmtNoTransform   = ParserMaker AlexInput Token (Statement ())
forall a. ParserMaker AlexInput Token a
makeParserFixed LexAction (Statement ())
F66.statementParser   FortranVersion
Fortran66
f77StmtNoTransform :: Parser (Statement ())
f77StmtNoTransform   = ParserMaker AlexInput Token (Statement ())
forall a. ParserMaker AlexInput Token a
makeParserFixed LexAction (Statement ())
F77.statementParser   FortranVersion
Fortran77
f77eStmtNoTransform :: Parser (Statement ())
f77eStmtNoTransform  = ParserMaker AlexInput Token (Statement ())
forall a. ParserMaker AlexInput Token a
makeParserFixed LexAction (Statement ())
F77.statementParser   FortranVersion
Fortran77Extended
f77lStmtNoTransform :: Parser (Statement ())
f77lStmtNoTransform  = ParserMaker AlexInput Token (Statement ())
forall a. ParserMaker AlexInput Token a
makeParserFixed LexAction (Statement ())
F77.statementParser   FortranVersion
Fortran77Legacy
f90StmtNoTransform :: Parser (Statement ())
f90StmtNoTransform   = ParserMaker AlexInput Token (Statement ())
forall a. ParserMaker AlexInput Token a
makeParserFree  LexAction (Statement ())
F90.statementParser   FortranVersion
Fortran90
f95StmtNoTransform :: Parser (Statement ())
f95StmtNoTransform   = ParserMaker AlexInput Token (Statement ())
forall a. ParserMaker AlexInput Token a
makeParserFree  LexAction (Statement ())
F95.statementParser   FortranVersion
Fortran95
f2003StmtNoTransform :: Parser (Statement ())
f2003StmtNoTransform = ParserMaker AlexInput Token (Statement ())
forall a. ParserMaker AlexInput Token a
makeParserFree  LexAction (Statement ())
F2003.statementParser FortranVersion
Fortran2003

byVerStmt :: FortranVersion -> Parser (Statement A0)
byVerStmt :: FortranVersion -> Parser (Statement ())
byVerStmt = \case
  FortranVersion
Fortran66         -> Parser (Statement ())
f66StmtNoTransform
  FortranVersion
Fortran77         -> Parser (Statement ())
f77StmtNoTransform
  FortranVersion
Fortran77Extended -> Parser (Statement ())
f77eStmtNoTransform
  FortranVersion
Fortran77Legacy   -> Parser (Statement ())
f77lStmtNoTransform
  FortranVersion
Fortran90         -> Parser (Statement ())
f90StmtNoTransform
  FortranVersion
Fortran95         -> Parser (Statement ())
f95StmtNoTransform
  FortranVersion
Fortran2003       -> Parser (Statement ())
f2003StmtNoTransform
  FortranVersion
v                 -> [Char] -> Parser (Statement ())
forall a. HasCallStack => [Char] -> a
error ([Char] -> Parser (Statement ()))
-> [Char] -> Parser (Statement ())
forall a b. (a -> b) -> a -> b
$  [Char]
"Language.Fortran.Parser.byVerStmt: "
                             [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"no parser available for requested version: "
                             [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> FortranVersion -> [Char]
forall a. Show a => a -> [Char]
show FortranVersion
v