blob: e1d4795b9b40d8bca3ad5e21c590600563c20505 (
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
74
75
76
77
78
79
80
81
82
83
|
{
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
| "interface" { INTERFACE }
| "datamodel" { DATAMODEL }
| "code" { CODE }
| "var" { VAR }
| "constructor" { CONSTRUCTOR }
| "method" { METHOD }
| "frame" { FRAME }
| "invariant" { INVARIANT }
| "returns" { RETURNS }
| "requires" { REQUIRES }
| "ensures" { ENSURES }
| "forall" { FORALL }
// Types
| "int" { INTTYPE }
| "bool" { BOOLTYPE }
| "seq" { SEQTYPE }
| "set" { SETTYPE }
// Operators
| "..." { DOTDOTDOT }
| ".." { DOTDOT }
| "." { DOT }
| "old" { OLD }
| "+" { 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 }
| "?" { QMARK }
// Numberic constants
| digit+ { INTEGER (System.Convert.ToInt32(lexeme lexbuf)) }
// identifiers
| idchar+ { ID (LexBuffer<char>.LexemeString lexbuf) }
// EOF
| eof { EOF }
| _ { printfn "Unrecognized input character: %s" (lexeme lexbuf) ; EOF }
|
