{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wall #-}

module Camfort.Specification.Hoare.Lexer (lexer) where

import Data.Monoid (Alt(..))
import Data.Coerce
import qualified Data.Char as Char

import Control.Monad.State
import Control.Monad.Except

import Camfort.Specification.Hoare.Parser.Types


-- | Lex an invariant annotation.
lexer :: String -> HoareSpecParser [Token]
lexer :: String -> HoareSpecParser [Token]
lexer [] = [Token] -> HoareSpecParser [Token]
forall (m :: * -> *) a. Monad m => a -> m a
return []
lexer (Char
' ' : String
xs) = String -> HoareSpecParser [Token]
lexer String
xs
lexer (Char
'\t' : String
xs) = String -> HoareSpecParser [Token]
lexer String
xs
lexer String
xs
  | Just (Token
tok, String
rest) <- String -> Maybe (Token, String)
lexSymbol String
xs
  = Token -> String -> HoareSpecParser [Token]
addToTokens Token
tok String
rest
lexer (Char
'"' : String
xs) = do
  (Token
tok, String
rest) <- String -> HoareSpecParser (Token, String)
lexQuoted String
xs
  Token -> String -> HoareSpecParser [Token]
addToTokens Token
tok String
rest
lexer String
xs = do
  Maybe (Token, String)
mname <- String -> HoareSpecParser (Maybe (Token, String))
lexName String
xs
  case Maybe (Token, String)
mname of
    Just (Token
tok, String
rest) -> Token -> String -> HoareSpecParser [Token]
addToTokens Token
tok String
rest
    Maybe (Token, String)
Nothing -> HoareParseError -> HoareSpecParser [Token]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> HoareParseError
LexError String
xs)


addToTokens :: Token -> String -> HoareSpecParser [Token]
addToTokens :: Token -> String -> HoareSpecParser [Token]
addToTokens Token
tok String
rest = do
 [Token]
tokens <- String -> HoareSpecParser [Token]
lexer String
rest
 [Token] -> HoareSpecParser [Token]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token] -> HoareSpecParser [Token])
-> [Token] -> HoareSpecParser [Token]
forall a b. (a -> b) -> a -> b
$ Token
tok Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
tokens

lexSymbol :: String -> Maybe (Token, String)
lexSymbol :: String -> Maybe (Token, String)
lexSymbol String
xs =
  let symbols :: [(String, Token)]
symbols =
        [ (String
"static_assert", Token
TStaticAssert)
        , (String
"decl_aux", Token
TDeclAux)
        , (String
"invariant", Token
TInvariant)
        , (String
"post", Token
TPost)
        , (String
"pre", Token
TPre)
        , (String
"seq", Token
TSeq)
        , (String
"&", Token
TAnd)
        , (String
"|", Token
TOr)
        , (String
"<->", Token
TEquiv)
        , (String
"->", Token
TImpl)
        , (String
"!", Token
TNot)
        , (String
"t", Token
TTrue)
        , (String
"f", Token
TFalse)
        , (String
"(", Token
TLParen)
        , (String
")", Token
TRParen)
        , (String
"::", Token
TDColon)
        ]

      tryMatch :: (String, t) -> Maybe (t, String)
tryMatch (String
symbol, t
tok) = (t
tok,) (String -> (t, String)) -> Maybe String -> Maybe (t, String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
symbol String
xs

      firstMatch :: [Maybe (Token, String)] -> Maybe (Token, String)
firstMatch = Alt Maybe (Token, String) -> Maybe (Token, String)
forall k (f :: k -> *) (a :: k). Alt f a -> f a
getAlt (Alt Maybe (Token, String) -> Maybe (Token, String))
-> ([Maybe (Token, String)] -> Alt Maybe (Token, String))
-> [Maybe (Token, String)]
-> Maybe (Token, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Alt Maybe (Token, String)] -> Alt Maybe (Token, String)
forall a. Monoid a => [a] -> a
mconcat ([Alt Maybe (Token, String)] -> Alt Maybe (Token, String))
-> ([Maybe (Token, String)] -> [Alt Maybe (Token, String)])
-> [Maybe (Token, String)]
-> Alt Maybe (Token, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (Token, String)] -> [Alt Maybe (Token, String)]
coerce

  in [Maybe (Token, String)] -> Maybe (Token, String)
firstMatch ((String, Token) -> Maybe (Token, String)
forall t. (String, t) -> Maybe (t, String)
tryMatch ((String, Token) -> Maybe (Token, String))
-> [(String, Token)] -> [Maybe (Token, String)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, Token)]
symbols)


lexQuoted :: String -> HoareSpecParser (Token, String)
lexQuoted :: String -> HoareSpecParser (Token, String)
lexQuoted String
input = do
  let
    go :: String -> StateT String HoareSpecParser String
    go :: String -> StateT String HoareSpecParser String
go (Char
'"' : String
xs) = String -> StateT String HoareSpecParser String
forall (m :: * -> *) a. Monad m => a -> m a
return String
xs
    go [] = HoareParseError -> StateT String HoareSpecParser String
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError HoareParseError
UnmatchedQuote
    go (Char
c : String
xs) = do
      (String -> String) -> StateT String HoareSpecParser ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Char
c Char -> String -> String
forall a. a -> [a] -> [a]
:)
      String -> StateT String HoareSpecParser String
go String
xs

  (String
rest, String
expr) <- StateT String HoareSpecParser String
-> String -> HoareSpecParser (String, String)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (String -> StateT String HoareSpecParser String
go String
input) []
  (Token, String) -> HoareSpecParser (Token, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Token
TQuoted (String -> String
forall a. [a] -> [a]
reverse String
expr), String
rest)


isNameStartChar :: Char -> Bool
isNameStartChar :: Char -> Bool
isNameStartChar Char
c = Char -> Bool
Char.isLetter Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'

isNameChar :: Char -> Bool
isNameChar :: Char -> Bool
isNameChar Char
c =
  Char -> Bool
Char.isLetter Char
c Bool -> Bool -> Bool
||
  Char -> Bool
Char.isNumber Char
c Bool -> Bool -> Bool
||
  Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'

lexName :: String -> HoareSpecParser (Maybe (Token, String))
lexName :: String -> HoareSpecParser (Maybe (Token, String))
lexName String
xs =
  let (String
nm, String
rest) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isNameChar String
xs
  in case String
nm of
    (Char
n1 : String
_) | Char -> Bool
isNameStartChar Char
n1 -> Maybe (Token, String) -> HoareSpecParser (Maybe (Token, String))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Token, String) -> Maybe (Token, String)
forall a. a -> Maybe a
Just (String -> Token
TName String
nm, String
rest))
    String
_ -> Maybe (Token, String) -> HoareSpecParser (Maybe (Token, String))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Token, String)
forall a. Maybe a
Nothing


stripPrefix :: (Eq a) => [a] -> [a] -> Maybe [a]
stripPrefix :: [a] -> [a] -> Maybe [a]
stripPrefix (a
p : [a]
refix) (a
s : [a]
tring)
  | a
p a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
s = [a] -> [a] -> Maybe [a]
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix [a]
refix [a]
tring
  | Bool
otherwise = Maybe [a]
forall a. Maybe a
Nothing
stripPrefix [] [a]
string = [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a]
string
stripPrefix [a]
_ [] = Maybe [a]
forall a. Maybe a
Nothing