summaryrefslogtreecommitdiff
path: root/Jennisys/Lexer.fsl
blob: 9a1cc623b77786b2cac9efb40d75ce3de06fc04a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
{
module Lexer
open System
open Parser
open Microsoft.FSharp.Text.Lexing

let lexeme lexbuf =
    LexBuffer<char>.LexemeString lexbuf
}

// These are some regular expression definitions
let digit = ['0'-'9']
let nondigit = [ 'a'-'z' 'A'-'Z' '_' ]
let idchar = (nondigit | digit)
let whitespace = [' ' '\t' ]
let newline = ('\n' | '\r' '\n')

rule tokenize = parse
| whitespace  { tokenize lexbuf }
| newline     { lexbuf.EndPos <- lexbuf.EndPos.NextLine; tokenize lexbuf }
// TODO:  | "//"[-newline]* { tokenize lexbuf }
// keywords
| "class"    { CLASS }
| "model"    { MODEL }
| "code"     { CODE }
| "var"          { VAR }
| "constructor"  { CONSTRUCTOR }
| "method"       { METHOD }
| "frame"        { FRAME }
| "invariant"    { INVARIANT }
| "returns"      { RETURNS }
| "requires"     { REQUIRES }
| "forall"       { FORALL }
// Operators
| "."      { DOT }
| "+"      { PLUS }
| "-"      { MINUS }
| "*"      { STAR }
| "div"    { DIV }
| "mod"    { MOD }
| "&&"     { AND }
| "||"     { OR }
| "!"      { NOT }
| "==>"    { IMPLIES }
| "<==>"   { IFF }
| "<"      { LESS }
| "<="     { ATMOST }
| "="      { EQ }
| "!="     { NEQ }
| ">="     { ATLEAST }
| ">"      { GREATER }
| "in"     { IN }
| "!in"    { NOTIN }
// Misc
| ":="     { GETS }
| "("      { LPAREN }
| ")"      { RPAREN }
| "["      { LBRACKET }
| "]"      { RBRACKET }
| "{"      { LCURLY }
| "}"      { RCURLY }
| "|"      { VERTBAR }
| ":"      { COLON }
| "::"     { COLONCOLON }
| ","      { COMMA }
// Numberic constants
| digit+        { INTEGER (System.Numerics.BigInteger.Parse(lexeme lexbuf)) }
// identifiers
| idchar+       { ID (LexBuffer<char>.LexemeString lexbuf) }
// EOF
| eof   { EOF }
| _ { printfn "Unrecognized input character: %s" (lexeme lexbuf) ; EOF }