Lexer.x

{
{-# OPTIONS_GHC -w #-}
module HyLo.InputFile.Lexer (lexify, Token(..),
                             FilePos, line, col)

where

import Debug.Trace ( trace )

import Data.Char ( isSpace )

import HyLo.Signature.String ( PropSymbol(..),
                               NomSymbol(..),
                               RelSymbol(..), inv
                                )
}

%wrapper "posn"

$digit = [0-9]                  -- digits
$alpha = [a-zA-Z]               -- alphabetic characters
$alphaNum = [$alpha$digit]
$alphaNumDotDash = [$alpha$digit\+\/\.\-\_]
$alphaNumDotDashSlash = [$alpha$digit\+\.\-\_\\\/]

@int = \-?$digit+
@rel = [Rr]@int

hyloTokens :-
  $white+                   ;       -- strip whitspaces
  \%.*                      ;       -- strip comments

  signature                  { discardValue TokenSignature -- SIGNATURE }
  propositions               { discardValue TokenPropositions }
  nominals                   { discardValue TokenNominals }

  relations                  { discardValue TokenRelations }
  subsetof                   { discardValue TokenSubsetOf }
  equals                     { discardValue TokenEquals }
  inverseof                  { discardValue TokenInverseOf }
  tclosureof                 { discardValue TokenTClosureOf }
  trclosureof                { discardValue TokenTRClosureOf }

  reflexive                  { discardValue TokenReflexive }
  universal                  { discardValue TokenUniversal }
  difference                 { discardValue TokenDifference }
  transitive                 { discardValue TokenTransitive }
  symmetric                  { discardValue TokenSymmetric }
  functional                 { discardValue TokenFunctional }

  automatic                  { discardValue TokenAutomatic }

  proverparameters           { discardValue TokenProverParameters }
  prover                     { discardValue TokenProver }

  query                      { discardValue TokenQuery }
  theory                     { discardValue TokenTheory }
  valid\?                    { discardValue TokenValid }
  satisfiable\?              { discardValue TokenSatisfiable }
  retrieve                   { discardValue TokenRetrieve }

  true                       { discardValue TokenTrue  }
  false                      { discardValue TokenFalse }
  [Pp]@int                   { storeValue (TokenProp . PropSymbol) }
  [Nn]@int                   { storeValue (TokenNom . NomSymbol) }

  \<$white*@rel?$white*\>    { storeValue (TokenDia . rel . dropEnds) }
  dia                        { discardValue (TokenDia defaultRel)     }

  \<$white*\-@rel?$white*\>  { storeValue (TokenDia . relI . tail . dropEnds) }

  \[$white*@rel?$white*\]    { storeValue (TokenBox . rel . dropEnds) }
  box                        { discardValue (TokenBox defaultRel)     }

  \[$white*\-@rel?$white*\]  { storeValue (TokenBox . relI . tail . dropEnds) }

  \:                         { discardValue TokenColon  }

  A                          { discardValue TokenUBox }
  E                          { discardValue TokenUDia }

  D                          { discardValue TokenDDia }
  B                          { discardValue TokenDBox }

  down                       { discardValue TokenDown }

  [v\|]                      { discardValue TokenOr   }
  [&\^]                      { discardValue TokenAnd  }
  [\!\-\~]                   { discardValue TokenNeg  }
  "<-->"                     { discardValue TokenDimp }
  "-->"                      { discardValue TokenImp  }
  "->"                       { discardValue TokenImp  }

  "("                        { discardValue TokenOB }
  ")"                        { discardValue TokenCB }
  "{"                        { discardValue TokenOC }
  "}"                        { discardValue TokenCC }
  "<"                        { discardValue TokenODia }
  ">"                        { discardValue TokenCDia }
  "["                        { discardValue TokenOBox }
  "]"                        { discardValue TokenCBox }

  \=                         { discardValue TokenEqual}
  \.                         { discardValue TokenDot }
  \;                         { discardValue TokenSC }
  \,                         { discardValue TokenComma }
  $alphaNum$alphaNumDotDash*    { storeValue TokenVariable }
  $alphaNum$alphaNumDotDash+          { storeValue TokenLabel }
  \"$alphaNumDotDashSlash*\" { storeValue (TokenFile . dropEnds) }
{
data Token = TokenSignature
           | TokenPropositions | TokenNominals
           | TokenRelations
             | TokenSubsetOf | TokenEquals | TokenInverseOf
             | TokenTClosureOf | TokenTRClosureOf
             | TokenReflexive |TokenTransitive | TokenSymmetric
             | TokenFunctional
             | TokenUniversal | TokenDifference
           | TokenAutomatic
           | TokenProverParameters | TokenProver
           | TokenTheory | TokenQuery | TokenValid | TokenSatisfiable | TokenRetrieve
           | TokenOC | TokenCC
           | TokenEqual
           | TokenVariable String
           | TokenLabel String
           | TokenFile String
           | TokenBegin           | TokenEnd
           | TokenTrue            | TokenFalse
           | TokenProp PropSymbol | TokenNom NomSymbol
           | TokenNeg             | TokenAnd            | TokenOr
           | TokenDown
           | TokenBox  RelSymbol  | TokenDia  RelSymbol
           | TokenImp             | TokenDimp
           | TokenUBox            | TokenUDia
           | TokenDBox            | TokenDDia
           | TokenOB              | TokenCB
           | TokenODia | TokenCDia | TokenOBox | TokenCBox
           | TokenDot             | TokenSC             | TokenColon | TokenComma
  deriving (Eq, Show)

data FilePos = FP{line :: Int, col :: Int} deriving (Eq, Show)

makeFilePos (AlexPn _ l c) = FP{line = l, col = c}

lexify :: String -> [(Token, FilePos)]
lexify str = go (alexStartPos,'\n',str)
    where go inp@(pos,_,str) = case alexScan inp 0 of
                                    AlexEOF                       -> []
                                    AlexError (AlexPn _ l c, _,_) -> error $ concat ["Unknown token at line: ", show l, " col: ", show c]
                                    AlexSkip  inp' len            -> go inp'
                                    AlexToken inp' len act        -> act pos (take len str) : go inp'

-- for building tokens which hold a value
storeValue     mkToken alexPos v = (mkToken v, makeFilePos alexPos)

-- for building tokens which discard the parsed string
discardValue   token alexPos _ = (token, makeFilePos alexPos)

dropEnds = init . tail

rel  r
  | null r    = defaultRel
  | otherwise =  RelSymbol r
relI   = inv . rel
defaultRel = RelSymbol "R1"
}