rzk-0.8.0: src/Language/Rzk/Syntax/Lex.x
-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6.2).
-- Lexer definition for use with Alex 3
{
{-# OPTIONS -Wno-incomplete-patterns #-}
{-# OPTIONS_GHC -w #-}
{-# LANGUAGE PatternSynonyms #-}
module Language.Rzk.Syntax.Lex where
import Prelude
import qualified Data.Text
import qualified Data.Bits
import Data.Char (ord)
import Data.Function (on)
import Data.Word (Word8)
}
-- Predefined character classes
$c = [A-Z\192-\222] # [\215] -- capital isolatin1 letter (215 = \times)
$s = [a-z\223-\255] # [\247] -- small isolatin1 letter (247 = \div )
$l = [$c $s] -- letter
$d = [0-9] -- digit
$i = [$l $d _ '] -- identifier character
$u = [. \n] -- universal: any character
-- Symbols and non-identifier-like reserved words
@rsyms = \ᵒ \ᵖ | "inv" \ᵒ \ᵖ | "uninv" \ᵒ \ᵖ | "flip" \ᵒ \ᵖ | "unflip" \ᵒ \ᵖ | \Σ | \π \₁ | \π \₂ | \# "lang" | \; | "rzk" \- "1" | \# "set" \- "option" | \= | \# "unset" \- "option" | \# "check" | \: | \# "compute" | \# "compute" \- "whnf" | \# "compute" \- "nf" | \# "postulate" | \# "assume" | \# "variable" | \# "variables" | \# "section" | \# "end" | \# "define" | \: \= | \# "def" | \( | \) | \, | \| | \{ | \} | \↦ | \♭ | \_ "b" | \♯ | \_ \# | \_ "op" | \_ "id" | \/ | "1" | \* \₁ | "2" | "0" \₂ | "1" \₂ | \× | \⊤ | \⊥ | \≡ | \≤ | \∧ | \∨ | \→ | \= \_ \{ | \[ | \] | \< | \> | \\ | \< \| | \| \> | \$ "extract" \$ | "refl" \_ \{ | \* | \* \_ "1" | "0" \_ "2" | "1" \_ "2" | \= \= \= | \< \= | \/ \\ | \\ \/ | \- \> | \| \- \> | \∑
:-
-- Line comment "--"
"--" [.]* ;
-- Block comment "{-" "-}"
\{ \- [$u # \-]* \- ([$u # [\- \}]] [$u # \-]* \- | \-)* \} ;
-- Whitespace (skipped)
$white+ ;
-- Symbols
@rsyms
{ tok (eitherResIdent TV) }
-- token VarIdentToken
[$u # [\t \n \r \ \! \" \# \( \) \, \- \. \; \< \> \? \[ \\ \] \{ \| \}]] [$u # [\t \n \r \ \" \# \( \) \, \; \< \> \[ \\ \] \{ \| \}]] *
{ tok (eitherResIdent T_VarIdentToken) }
-- token HoleIdentToken
\?
{ tok (eitherResIdent T_HoleIdentToken) }
-- Keywords and Ident
$l $i*
{ tok (eitherResIdent TV) }
-- String
\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | r | f)))* \"
{ tok (TL . unescapeInitTail) }
{
-- | Create a token with position.
tok :: (Data.Text.Text -> Tok) -> (Posn -> Data.Text.Text -> Token)
tok f p = PT p . f
-- | Token without position.
data Tok
= TK {-# UNPACK #-} !TokSymbol -- ^ Reserved word or symbol.
| TL !Data.Text.Text -- ^ String literal.
| TI !Data.Text.Text -- ^ Integer literal.
| TV !Data.Text.Text -- ^ Identifier.
| TD !Data.Text.Text -- ^ Float literal.
| TC !Data.Text.Text -- ^ Character literal.
| T_VarIdentToken !Data.Text.Text
| T_HoleIdentToken !Data.Text.Text
deriving (Eq, Show, Ord)
-- | Smart constructor for 'Tok' for the sake of backwards compatibility.
pattern TS :: Data.Text.Text -> Int -> Tok
pattern TS t i = TK (TokSymbol t i)
-- | Keyword or symbol tokens have a unique ID.
data TokSymbol = TokSymbol
{ tsText :: Data.Text.Text
-- ^ Keyword or symbol text.
, tsID :: !Int
-- ^ Unique ID.
} deriving (Show)
-- | Keyword/symbol equality is determined by the unique ID.
instance Eq TokSymbol where (==) = (==) `on` tsID
-- | Keyword/symbol ordering is determined by the unique ID.
instance Ord TokSymbol where compare = compare `on` tsID
-- | Token with position.
data Token
= PT Posn Tok
| Err Posn
deriving (Eq, Show, Ord)
-- | Pretty print a position.
printPosn :: Posn -> String
printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c
-- | Pretty print the position of the first token in the list.
tokenPos :: [Token] -> String
tokenPos (t:_) = printPosn (tokenPosn t)
tokenPos [] = "end of file"
-- | Get the position of a token.
tokenPosn :: Token -> Posn
tokenPosn (PT p _) = p
tokenPosn (Err p) = p
-- | Get line and column of a token.
tokenLineCol :: Token -> (Int, Int)
tokenLineCol = posLineCol . tokenPosn
-- | Get line and column of a position.
posLineCol :: Posn -> (Int, Int)
posLineCol (Pn _ l c) = (l,c)
-- | Convert a token into "position token" form.
mkPosToken :: Token -> ((Int, Int), Data.Text.Text)
mkPosToken t = (tokenLineCol t, tokenText t)
-- | Convert a token to its text.
tokenText :: Token -> Data.Text.Text
tokenText t = case t of
PT _ (TS s _) -> s
PT _ (TL s) -> Data.Text.pack (show s)
PT _ (TI s) -> s
PT _ (TV s) -> s
PT _ (TD s) -> s
PT _ (TC s) -> s
Err _ -> Data.Text.pack "#error"
PT _ (T_VarIdentToken s) -> s
PT _ (T_HoleIdentToken s) -> s
-- | Convert a token to a string.
prToken :: Token -> String
prToken t = Data.Text.unpack (tokenText t)
-- | Finite map from text to token organized as binary search tree.
data BTree
= N -- ^ Nil (leaf).
| B Data.Text.Text Tok BTree BTree
-- ^ Binary node.
deriving (Show)
-- | Convert potential keyword into token or use fallback conversion.
eitherResIdent :: (Data.Text.Text -> Tok) -> Data.Text.Text -> Tok
eitherResIdent tv s = treeFind resWords
where
treeFind N = tv s
treeFind (B a t left right) =
case compare s a of
LT -> treeFind left
GT -> treeFind right
EQ -> t
-- | The keywords and symbols of the language organized as binary search tree.
resWords :: BTree
resWords =
b "\\" 50
(b "/\\" 25
(b "#unset-option" 13
(b "#define" 7
(b "#compute-nf" 4
(b "#check" 2 (b "#assume" 1 N N) (b "#compute" 3 N N))
(b "#def" 6 (b "#compute-whnf" 5 N N) N))
(b "#postulate" 10
(b "#lang" 9 (b "#end" 8 N N) N)
(b "#set-option" 12 (b "#section" 11 N N) N)))
(b "*" 19
(b "$extract$" 16
(b "#variables" 15 (b "#variable" 14 N N) N)
(b ")" 18 (b "(" 17 N N) N))
(b "," 22
(b "*\8321" 21 (b "*_1" 20 N N) N) (b "/" 24 (b "->" 23 N N) N))))
(b "=" 38
(b ":" 32
(b "1_2" 29
(b "0\8322" 27 (b "0_2" 26 N N) (b "1" 28 N N))
(b "2" 31 (b "1\8322" 30 N N) N))
(b "<" 35
(b ";" 34 (b ":=" 33 N N) N) (b "<|" 37 (b "<=" 36 N N) N)))
(b "Sigma" 44
(b ">" 41
(b "=_{" 40 (b "===" 39 N N) N) (b "CUBE" 43 (b "BOT" 42 N N) N))
(b "U" 47
(b "TOPE" 46 (b "TOP" 45 N N) N) (b "[" 49 (b "Unit" 48 N N) N)))))
(b "uninv_op" 75
(b "inv_op" 63
(b "as" 57
(b "_b" 54
(b "]" 52 (b "\\/" 51 N N) (b "_#" 53 N N))
(b "_op" 56 (b "_id" 55 N N) N))
(b "flip\7506\7510" 60
(b "flip_op" 59 (b "first" 58 N N) N)
(b "in" 62 (b "idJ" 61 N N) N)))
(b "refl" 69
(b "mod" 66
(b "let" 65 (b "inv\7506\7510" 64 N N) N)
(b "recOR" 68 (b "recBOT" 67 N N) N))
(b "second" 72
(b "rzk-1" 71 (b "refl_{" 70 N N) N)
(b "unflip\7506\7510" 74 (b "unflip_op" 73 N N) N))))
(b "\7506\7510" 88
(b "|>" 82
(b "{" 79
(b "unit" 77 (b "uninv\7506\7510" 76 N N) (b "uses" 78 N N))
(b "|->" 81 (b "|" 80 N N) N))
(b "\931" 85
(b "\215" 84 (b "}" 83 N N) N)
(b "\960\8322" 87 (b "\960\8321" 86 N N) N)))
(b "\8801" 94
(b "\8721" 91
(b "\8614" 90 (b "\8594" 89 N N) N)
(b "\8744" 93 (b "\8743" 92 N N) N))
(b "\8869" 97
(b "\8868" 96 (b "\8804" 95 N N) N)
(b "\9839" 99 (b "\9837" 98 N N) N)))))
where
b s n = B bs (TS bs n)
where
bs = Data.Text.pack s
-- | Unquote string literal.
unescapeInitTail :: Data.Text.Text -> Data.Text.Text
unescapeInitTail = Data.Text.pack . unesc . tail . Data.Text.unpack
where
unesc s = case s of
'\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs
'\\':'n':cs -> '\n' : unesc cs
'\\':'t':cs -> '\t' : unesc cs
'\\':'r':cs -> '\r' : unesc cs
'\\':'f':cs -> '\f' : unesc cs
'"':[] -> []
c:cs -> c : unesc cs
_ -> []
-------------------------------------------------------------------
-- Alex wrapper code.
-- A modified "posn" wrapper.
-------------------------------------------------------------------
data Posn = Pn !Int !Int !Int
deriving (Eq, Show, Ord)
alexStartPos :: Posn
alexStartPos = Pn 0 1 1
alexMove :: Posn -> Char -> Posn
alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1)
alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1
alexMove (Pn a l c) _ = Pn (a+1) l (c+1)
type Byte = Word8
type AlexInput = (Posn, -- current position,
Char, -- previous char
[Byte], -- pending bytes on the current char
Data.Text.Text) -- current input string
tokens :: Data.Text.Text -> [Token]
tokens str = go (alexStartPos, '\n', [], str)
where
go :: AlexInput -> [Token]
go inp@(pos, _, _, str) =
case alexScan inp 0 of
AlexEOF -> []
AlexError (pos, _, _, _) -> [Err pos]
AlexSkip inp' len -> go inp'
AlexToken inp' len act -> act pos (Data.Text.take len str) : (go inp')
alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)
alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))
alexGetByte (p, _, [], s) =
case Data.Text.uncons s of
Nothing -> Nothing
Just (c,s) ->
let p' = alexMove p c
(b:bs) = utf8Encode c
in p' `seq` Just (b, (p', c, bs, s))
alexInputPrevChar :: AlexInput -> Char
alexInputPrevChar (p, c, bs, s) = c
-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
utf8Encode :: Char -> [Word8]
utf8Encode = map fromIntegral . go . ord
where
go oc
| oc <= 0x7f = [oc]
| oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6)
, 0x80 + oc Data.Bits..&. 0x3f
]
| oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12)
, 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
, 0x80 + oc Data.Bits..&. 0x3f
]
| otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18)
, 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)
, 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
, 0x80 + oc Data.Bits..&. 0x3f
]
}