{-# 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 qualified Language.Fortran.Lexer.FreeForm   as F
import qualified Language.Fortran.Parser.Fortran90 as F
import qualified Language.Fortran.ParserMonad      as F


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
/= :: HoareParseError -> HoareParseError -> Bool
$c/= :: HoareParseError -> HoareParseError -> Bool
== :: HoareParseError -> HoareParseError -> Bool
$c== :: 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
min :: HoareParseError -> HoareParseError -> HoareParseError
$cmin :: HoareParseError -> HoareParseError -> HoareParseError
max :: HoareParseError -> HoareParseError -> HoareParseError
$cmax :: HoareParseError -> HoareParseError -> HoareParseError
>= :: HoareParseError -> HoareParseError -> Bool
$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
compare :: HoareParseError -> HoareParseError -> Ordering
$ccompare :: HoareParseError -> HoareParseError -> Ordering
$cp1Ord :: Eq HoareParseError
Ord, Typeable, Typeable HoareParseError
DataType
Constr
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 -> DataType
HoareParseError -> Constr
(forall b. Data b => b -> b) -> HoareParseError -> HoareParseError
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HoareParseError -> c HoareParseError
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cLexError :: Constr
$cParseError :: Constr
$cMalformedTypeSpec :: Constr
$cMalformedExpression :: Constr
$cUnexpectedInput :: Constr
$cUnmatchedQuote :: Constr
$tHoareParseError :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d)
-> HoareParseError -> m HoareParseError
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> HoareParseError -> m HoareParseError
gmapQi :: Int -> (forall d. Data d => d -> u) -> HoareParseError -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> HoareParseError -> u
gmapQ :: (forall d. Data d => d -> u) -> HoareParseError -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> HoareParseError -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HoareParseError -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HoareParseError -> r
gmapT :: (forall b. Data b => b -> b) -> HoareParseError -> HoareParseError
$cgmapT :: (forall b. Data b => b -> b) -> HoareParseError -> HoareParseError
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HoareParseError)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c HoareParseError)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c HoareParseError)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HoareParseError)
dataTypeOf :: HoareParseError -> DataType
$cdataTypeOf :: HoareParseError -> DataType
toConstr :: HoareParseError -> Constr
$ctoConstr :: HoareParseError -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HoareParseError
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HoareParseError
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HoareParseError -> c HoareParseError
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HoareParseError -> c HoareParseError
$cp1Data :: Typeable HoareParseError
Data)

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

instance Exception HoareParseError where

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

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 -> String
(Int -> Token -> ShowS)
-> (Token -> String) -> ([Token] -> ShowS) -> Show Token
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Token] -> ShowS
$cshowList :: [Token] -> ShowS
show :: Token -> String
$cshow :: Token -> String
showsPrec :: Int -> Token -> ShowS
$cshowsPrec :: Int -> Token -> ShowS
Show, Token -> Token -> Bool
(Token -> Token -> Bool) -> (Token -> Token -> Bool) -> Eq Token
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Token -> Token -> Bool
$c/= :: Token -> Token -> Bool
== :: Token -> Token -> Bool
$c== :: 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
min :: Token -> Token -> Token
$cmin :: Token -> Token -> Token
max :: Token -> Token -> Token
$cmax :: Token -> Token -> Token
>= :: Token -> Token -> Bool
$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
compare :: Token -> Token -> Ordering
$ccompare :: Token -> Token -> Ordering
$cp1Ord :: Eq Token
Ord, Typeable, Typeable Token
DataType
Constr
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 -> DataType
Token -> Constr
(forall b. Data b => b -> b) -> Token -> Token
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Token -> c Token
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cTDColon :: Constr
$cTName :: Constr
$cTDeclAux :: Constr
$cTFalse :: Constr
$cTTrue :: Constr
$cTNot :: Constr
$cTEquiv :: Constr
$cTImpl :: Constr
$cTOr :: Constr
$cTAnd :: Constr
$cTLParen :: Constr
$cTRParen :: Constr
$cTSeq :: Constr
$cTInvariant :: Constr
$cTPost :: Constr
$cTPre :: Constr
$cTStaticAssert :: Constr
$cTQuoted :: Constr
$tToken :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> Token -> m Token
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Token -> m Token
gmapQi :: Int -> (forall d. Data d => d -> u) -> Token -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Token -> u
gmapQ :: (forall d. Data d => d -> u) -> Token -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Token -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Token -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Token -> r
gmapT :: (forall b. Data b => b -> b) -> Token -> Token
$cgmapT :: (forall b. Data b => b -> b) -> Token -> Token
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Token)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Token)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Token)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Token)
dataTypeOf :: Token -> DataType
$cdataTypeOf :: Token -> DataType
toConstr :: Token -> Constr
$ctoConstr :: Token -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Token
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Token
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Token -> c Token
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Token -> c Token
$cp1Data :: Typeable Token
Data)

-- TODO: Make this report errors and deal with source position better
parseExpression :: String -> HoareSpecParser (F.Expression ())
parseExpression :: String -> HoareSpecParser (Expression ())
parseExpression String
expr =
  case Parse AlexInput Token (Statement ())
-> ParseState AlexInput
-> ParseResult AlexInput Token (Statement ())
forall b c a.
(Loc b, LastToken b c, Show c) =>
Parse b c a -> ParseState b -> ParseResult b c a
F.runParse Parse AlexInput Token (Statement ())
F.statementParser ParseState AlexInput
parseState of
    F.ParseOk (F.StExpressionAssign ()
_ SrcSpan
_ Expression ()
_ Expression ()
e) ParseState AlexInput
_ -> Expression () -> HoareSpecParser (Expression ())
forall (m :: * -> *) a. Monad m => a -> m a
return Expression ()
e
    ParseResult AlexInput Token (Statement ())
_ -> HoareParseError -> HoareSpecParser (Expression ())
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> HoareParseError
MalformedExpression String
expr)
  where
    paddedExpr :: ByteString
paddedExpr = String -> ByteString
B.pack (String -> ByteString) -> String -> ByteString
forall a b. (a -> b) -> a -> b
$ String
"      a = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
expr
    parseState :: ParseState AlexInput
parseState = ByteString -> FortranVersion -> String -> ParseState AlexInput
F.initParseState ByteString
paddedExpr FortranVersion
F.Fortran90 String
"<unknown>"


-- TODO: Make this report errors and deal with source position better
parseTypeSpec :: String -> HoareSpecParser (F.TypeSpec ())
parseTypeSpec :: String -> HoareSpecParser (TypeSpec ())
parseTypeSpec String
ts =
  case Parse AlexInput Token (Statement ())
-> ParseState AlexInput
-> ParseResult AlexInput Token (Statement ())
forall b c a.
(Loc b, LastToken b c, Show c) =>
Parse b c a -> ParseState b -> ParseResult b c a
F.runParse Parse AlexInput Token (Statement ())
F.statementParser ParseState AlexInput
parseState of
    F.ParseOk (F.StDeclaration ()
_ SrcSpan
_ TypeSpec ()
s Maybe (AList Attribute ())
_ AList Declarator ()
_) ParseState AlexInput
_ -> TypeSpec () -> HoareSpecParser (TypeSpec ())
forall (m :: * -> *) a. Monad m => a -> m a
return TypeSpec ()
s
    ParseResult AlexInput Token (Statement ())
_ -> HoareParseError -> HoareSpecParser (TypeSpec ())
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> HoareParseError
MalformedTypeSpec String
ts)
  where
    paddedTS :: ByteString
paddedTS = String -> ByteString
B.pack (String -> ByteString) -> String -> ByteString
forall a b. (a -> b) -> a -> b
$ String
ts String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: dummy"
    parseState :: ParseState AlexInput
parseState = ByteString -> FortranVersion -> String -> ParseState AlexInput
F.initParseState ByteString
paddedTS FortranVersion
F.Fortran90 String
"<unknown>"