Lexer.x

{
-- Ignore the slew of warnings from definitions generated by Alex.
-- NOTE: you should disable this line when working on this module to make sure
-- that you don't miss important warnings.
{-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-unused-binds #-}
{-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-name-shadowing #-}
{-# OPTIONS_GHC -fno-warn-unused-imports #-}

module Scyther.Theory.Lexer where

import Control.Applicative
import Control.Monad
import Data.Word (Word8)
import qualified Codec.Binary.UTF8.String as UTF8
}

$digit = [0-9]
$letter = [a-zA-Z]
$others = [\192-\214\216-\246\248-\255]

@integer    = $digit+
@identifierFirst = ($letter | $digit | $others)
@identifierAfter = ($letter | $digit | "_" | $others)
@identifier = @identifierFirst @identifierAfter*
@comment     = $printable | $white
@text        = $printable | $white
@lineComment = "//".*

tokens :-
  <0>        $white+            ;

  <0>        @lineComment       ;
  <0>        "(*"               { beginComment "(*" comment }
  <comment>  "(*"               { beginComment "(*" comment }
  <text>     "(*"               { beginComment "(*" comment }
  <comment>  "*)"               { endComment "(*" }
  <0>        "/*"               { beginComment "/*" comment }
  <comment>  "/*"               { beginComment "/*" comment }
  <text>     "/*"               { beginComment "/*" comment }
  <comment>  "*/"               { endComment "/*" }
  <comment>  @comment           { skip }

  <0>        "text{*"           { beginText "text" text }
  <0>        "section{*"        { beginText "section" text }
  <0>        "subsection{*"     { beginText "subsection" text }
  <text>     "*}"               { endText 0}
  <text>     @text              { scanString (TEXT . TextContent) }


  <0>        "∀"                { keyword FORALL }
  <0>        "∃"                { keyword EXISTS }
  <0>        "∧"                { keyword LAND }
  <0>        "∨"                { keyword LOR }
  <0>        "¬"                { keyword LNOT }
  <0>        "≈"                { keyword APPROX }

  <0>        ","                { keyword COMMA }
  <0>        "("                { keyword LPAREN }
  <0>        ")"                { keyword RPAREN }
  <0>        "["                { keyword LBRACKET }
  <0>        "]"                { keyword RBRACKET }
  <0>        "{"                { keyword LBRACE }
  <0>        "}"                { keyword RBRACE }
  <0>        "/"                { keyword SLASH }
  <0>        "\\"               { keyword BACKSLASH }
  <0>        "'"                { keyword SQUOTE }
  <0>        \"                 { keyword DQUOTE }
  <0>        "~"                { keyword TILDE }
  <0>        "^"                { keyword HAT }
  <0>        "="                { keyword EQUAL }
  <0>        ":"                { keyword COLON }
  <0>        "$"                { keyword DOLLAR }
  <0>        "@"                { keyword AT }
  <0>        "#"                { keyword SHARP }
  <0>        "*"                { keyword STAR }
  <0>        "<"                { keyword LESS }
  <0>        ">"                { keyword GREATER }
  <0>        "?"                { keyword QUESTIONMARK }
  <0>        "!"                { keyword BANG }
  <0>        "&"                { keyword AND }
  <0>        "|"                { keyword MID }
  <0>        "."                { keyword DOT }
  <0>        "_"                { keyword UNDERSCORE }
  <0>        "-"                { keyword MINUS }
  <0>        "+"                { keyword PLUS }
  <0>        "->"               { keyword RIGHTARROW }
  <0>        "<-"               { keyword LEFTARROW }
  <0>        "-->"              { keyword LONGRIGHTARROW }
  <0>        "<--"              { keyword LONGLEFTARROW }
  <0>        @identifier        { scanString IDENT}


{

-- | Lex a keyword
keyword :: Keyword -> AlexAction Keyword
keyword kw input len = return kw

-- | Wrap a string into a keyword
scanString :: (String -> Keyword) -> AlexAction Keyword
scanString kw (_,_,_,input) len = return $ kw (take len input)

{-
-- | Scan a string until EOF is encountered.
alexScanTokens :: String -> Either String [Keyword]
alexScanTokens inp = runAlex inp gather
  where
  gather = do
    t <- alexMonadScan
    case trace (show t) t of
      EOF -> return [EOF]
      _   -> (t:) `liftM` gather

-- | Scan a file.
scanFile f = do
   inp <- readFile f
   return $ alexScanTokens inp
-}

-- | Formal text types.
data TextType =
       TextBegin String
     | TextContent String
     | TextEnd
     deriving( Eq, Ord, Show )

-- | Lexable Keywords
data Keyword =
    IDENT String
  | TEXT TextType
  | SQUOTE
  | DQUOTE
  | RIGHTARROW
  | LEFTARROW
  | LONGRIGHTARROW
  | LONGLEFTARROW
  | COMMA
  | DOT
  | COLON
  | QUESTIONMARK
  | BANG
  | AND
  | MID
  | DOLLAR
  | AT
  | SHARP
  | LPAREN
  | RPAREN
  | LBRACKET
  | RBRACKET
  | LBRACE
  | RBRACE
  | SLASH
  | BACKSLASH
  | TILDE
  | HAT
  | STAR
  | UNDERSCORE
  | MINUS
  | PLUS
  | EQUAL
  | LESS
  | GREATER
  | EOF
  | FORALL
  | EXISTS
  | LAND
  | LOR
  | LNOT
  | APPROX
  -- dummy keyword to get rid of overlapping pattern matches
  | DUMMY_KEYWORD
  deriving( Eq )

instance Show Keyword where
  show kw = case kw of
      IDENT i -> identifier i
      TEXT t -> txt t
      SQUOTE -> symbol "'"
      DQUOTE -> symbol "\""
      RIGHTARROW -> symbol "->"
      LEFTARROW -> symbol "<-"
      LONGRIGHTARROW -> symbol "-->"
      LONGLEFTARROW -> symbol "<--"
      COMMA -> symbol ","
      DOT -> symbol "."
      COLON -> symbol ":"
      QUESTIONMARK -> symbol "?"
      BANG -> symbol "!"
      AND -> symbol "&"
      MID -> symbol "|"
      DOLLAR -> symbol "$"
      AT -> symbol "@"
      SHARP -> symbol "#"
      LPAREN -> symbol "("
      RPAREN -> symbol ")"
      LBRACKET -> symbol "["
      RBRACKET -> symbol "]"
      LBRACE  -> symbol "{"
      RBRACE -> symbol "}"
      SLASH -> symbol "/"
      BACKSLASH -> symbol "\\"
      TILDE -> symbol "~"
      HAT -> symbol "^"
      STAR -> symbol "*"
      UNDERSCORE -> symbol "_"
      MINUS -> symbol "-"
      PLUS -> symbol "+"
      EQUAL -> symbol "="
      LESS -> symbol "<"
      GREATER -> symbol ">"
      EOF -> "end of file"
      FORALL -> symbol   "∀"
      EXISTS -> symbol   "∃"
      LAND -> symbol     "∧"
      LOR -> symbol      "∨"
      LNOT -> symbol     "¬"
      APPROX -> symbol   "≈"
      DUMMY_KEYWORD -> "DUMMY_KEYWORD (this should not occur!)"
    where
      identifier i        = "identifier `" ++ i ++ "'"
      txt (TextBegin t)   = "start of `" ++ t ++ "'"
      txt (TextContent t) = "text `" ++ t ++ "'"
      txt (TextEnd)       = "start of text"
      symbol s            = "symbol `" ++ s ++ "'"
      keyword s           = "keyword `" ++ s ++ "'"

-- -----------------------------------------------------------------------------
-- Alex wrapper code.
--
-- This code is in the PUBLIC DOMAIN; you may copy it freely and use
-- it for any purpose whatsoever.

-- -----------------------------------------------------------------------------
-- The input type

type AlexInput = (AlexPosn,     -- current position,
                  Char,         -- previous char
                  [Word8],      -- remaining bytes of current char
                  String)       -- current input string

alexInputPrevChar :: AlexInput -> Char
alexInputPrevChar (p,c,bs,s) = c

alexGetByte :: AlexInput -> Maybe (Word8,AlexInput)
alexGetByte (p,c,(b:bs),s) = Just (b,(p,c,bs,s))
alexGetByte (p,c,[],[]) = Nothing
alexGetByte (p,_,[],(c:s))  = let p' = alexMove p c
                                  (b:bs) = UTF8.encodeChar c
                              in p' `seq`  Just (b, (p', c, bs, s))

-- -----------------------------------------------------------------------------
-- Token positions

-- `Posn' records the location of a token in the input text.  It has three
-- fields: the address (number of chacaters preceding the token), line number
-- and column of a token within the file. `start_pos' gives the position of the
-- start of the file and `eof_pos' a standard encoding for the end of file.
-- `move_pos' calculates the new position after traversing a given character,
-- assuming the usual eight character tab stops.

data AlexPosn = AlexPn !Int !Int !Int
        deriving (Eq)

instance Show AlexPosn where
  show (AlexPn _ l c) = "line "++show l++" column "++show c

alexStartPos :: AlexPosn
alexStartPos = AlexPn 0 1 1

alexMove :: AlexPosn -> Char -> AlexPosn
alexMove (AlexPn a l c) '\t' = AlexPn (a+1)  l     (((c+7) `div` 8)*8+1)
alexMove (AlexPn a l c) '\n' = AlexPn (a+1) (l+1)   1
alexMove (AlexPn a l c) _    = AlexPn (a+1)  l     (c+1)


-- -----------------------------------------------------------------------------
-- Default monad


data AlexState = AlexState {
        alex_pos :: !AlexPosn,  -- position at current input location
        alex_inp :: String,     -- the current input
        alex_chr :: !Char,      -- the character before the input
        alex_scd :: !Int,       -- the current startcode
        alex_ocd :: !Int,       -- the old startcode before the comment started
        alex_cmt :: [String]    -- stack of begin comment identifiers
    }

-- Compile with -funbox-strict-fields for best results!

runAlex :: String -> Alex a -> Either String a
runAlex input (Alex f)
   = case f (AlexState {alex_pos = alexStartPos,
                        alex_inp = input,
                        alex_chr = '\n',
                        alex_scd = 0,
                        alex_ocd = 0,
                        alex_cmt = []
             }) of
       Left msg -> Left msg
       Right ( _, a ) -> Right a

newtype Alex a = Alex { unAlex :: AlexState -> Either String (AlexState, a) }

instance Functor Alex where
  fmap = liftM

instance Applicative Alex where
  pure  = return
  (<*>) = ap

instance Monad Alex where
  m >>= k  = Alex $ \s -> case unAlex m s of
                                Left msg -> Left msg
                                Right (s',a) -> unAlex (k a) s'
  return a = Alex $ \s -> Right (s,a)

alexGetPos :: Alex AlexPosn
alexGetPos = Alex $ \s@AlexState{alex_pos=pos} -> Right (s, pos)

alexGetInput :: Alex AlexInput
alexGetInput
 = Alex $ \s@AlexState{alex_pos=pos,alex_chr=c,alex_inp=inp} ->
        Right (s, (pos,c,[],inp))

alexSetInput :: AlexInput -> Alex ()
alexSetInput (pos,c,_,inp)
 = Alex $ \s -> case s{alex_pos=pos,alex_chr=c,alex_inp=inp} of
                  s@(AlexState{}) -> Right (s, ())

alexError :: String -> Alex a
alexError message = Alex $ \s -> Left $ message ++ " in " ++ show (alex_pos s)

alexGetStartCode :: Alex Int
alexGetStartCode = Alex $ \s@AlexState{alex_scd=sc} -> Right (s, sc)

alexSetStartCode :: Int -> Alex ()
alexSetStartCode sc = Alex $ \s -> Right (s{alex_scd=sc}, ())

alexGetOldStartCode :: Alex Int
alexGetOldStartCode = Alex $ \s@AlexState{alex_ocd=sc} -> Right (s, sc)

alexSetOldStartCode :: Int -> Alex ()
alexSetOldStartCode sc = Alex $ \s -> Right (s{alex_ocd=sc}, ())

alexGetComments :: Alex [String]
alexGetComments = Alex $ \s -> Right (s, alex_cmt s)

alexSetComments :: [String] -> Alex ()
alexSetComments cmt = Alex $ \s -> Right (s{alex_cmt=cmt}, ())

alexMonadScan = do
  inp <- alexGetInput
  sc <- alexGetStartCode
  case alexScan inp sc of
    AlexEOF -> alexEOF
    AlexError inp' -> alexError "lexical error"
    AlexSkip  inp' len -> do
        alexSetInput inp'
        alexMonadScan
    AlexToken inp' len action -> do
        alexSetInput inp'
        action inp len

-- -----------------------------------------------------------------------------
-- Useful token actions

type AlexAction result = AlexInput -> Int -> Alex result

-- just ignore this token and scan another one
skip :: AlexAction Keyword
skip input len = alexMonadScan

-- ignore this token, but set the start code to a new value
begin :: Int -> AlexAction Keyword
begin code input len = do alexSetStartCode code; alexMonadScan

-- | Begin a text starting of the given type.
beginText :: String -> Int -> AlexAction Keyword
beginText ty code _ _ = do
  alexSetStartCode code
  return $ TEXT $ TextBegin ty

-- | End a text.
endText :: Int -> AlexAction Keyword
endText code _ _ = do
  alexSetStartCode code
  return $ TEXT TextEnd

-- | Begin a comment starting with the given sign.
beginComment :: String -> Int -> AlexAction Keyword
beginComment cmtBegin code input len = do
  cmts <- alexGetComments
  alexSetComments $ cmtBegin : cmts
  if null cmts
    then alexGetStartCode >>= alexSetOldStartCode
    else return ()
  alexSetStartCode code
  alexMonadScan

-- | End a comment that started with the given begin comment sign.
endComment :: String -> AlexAction Keyword
endComment cmtBegin input len = do
  cmts <- alexGetComments
  case cmts of
    [] -> alexError $ "comment ended but no beginning '"++cmtBegin++"' marked."
    (cmt:cmts') -> do
      if cmt == cmtBegin
        then do
          alexSetComments cmts'
          if null cmts'
            then alexGetOldStartCode >>= alexSetStartCode
            else return ()
        else return ()
      alexMonadScan

-- perform an action for this token, and set the start code to a new value
-- andBegin :: AlexAction result -> Int -> AlexAction result
(action `andBegin` code) input len = do alexSetStartCode code; action input len

alexEOF :: Alex Keyword
alexEOF = return EOF



}