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

where

import Debug.Trace ( trace )

import Data.Char ( isSpace )

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

%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 }
  injective                  { discardValue TokenInjective }

  automatic                  { discardValue TokenAutomatic }

  proverparameters           { discardValue TokenProverParameters }
  prover                     { discardValue TokenProver }

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

  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 (TokenIDia . rel . tail . dropEnds) }

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

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

  \:                         { discardValue TokenColon  }

  A                          { discardValue TokenUBox }
  E                          { discardValue TokenUDia }

  D                          { discardValue TokenDDia }
  B                          { discardValue TokenDBox }

  down                       { discardValue TokenDown }

  ">="                       { discardValue TokenGE }
  "<="                       { discardValue TokenLE }
  ">."                        { discardValue TokenG }
  "<."                        { discardValue TokenL }
  "="                        { discardValue TokenE }
  "/="                       { discardValue TokenNE }

  [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 }
  $digit+                    { storeValue (TokenInteger . read) }
  $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 | TokenInjective
             | TokenUniversal | TokenDifference
           | TokenAutomatic
           | TokenProverParameters | TokenProver
           | TokenTheory | TokenQuery | TokenValid | TokenSatisfiable | TokenRetrieve | TokenCount
           | TokenOC | TokenCC
           | TokenEqual
           | TokenInteger Int
           | TokenVariable String
           | TokenLabel String
           | TokenFile String
           | TokenBegin           | TokenEnd
           | TokenTrue            | TokenFalse
           | TokenProp PropSymbol | TokenNom NomSymbol
           | TokenNeg             | TokenAnd            | TokenOr
           | TokenDown
           | TokenGE              | TokenLE
           | TokenG               | TokenL
           | TokenE               | TokenNE
           | TokenBox  RelSymbol  | TokenDia  RelSymbol
           | TokenIBox RelSymbol  | TokenIDia 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}

-- 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
defaultRel = RelSymbol "R1"
}