1 2 3(****************************************************************************** 4Simple lexer for PSL/Sugar properties 5(based on examples/lexyacc in mosml distribution) 6 ******************************************************************************) 7 8 9{ 10 open Lexing Parser; 11 12 exception LexicalError of string * int * int (* (message, loc1, loc2) *) 13 14 fun lexerError lexbuf s = 15 raise LexicalError (s, getLexemeStart lexbuf, getLexemeEnd lexbuf); 16 17 val commentStart = ref 0; (* Start of outermost comment being scanned *) 18 19 fun commentNotClosed lexbuf = 20 raise LexicalError ("Comment not terminated", 21 !commentStart, getLexemeEnd lexbuf); 22 23 val commentDepth = ref 0; (* Current comment nesting *) 24 25 (* Scan keywords as identifiers and use this function to distinguish them. *) 26 (* If the set of keywords is large, use an auxiliary hashtable. *) 27 28 fun keyword s = 29 case s of 30 "A" => A 31 | "AF" => AF 32 | "AG" => AG 33 | "AX" => AX 34 | "abort" => ABORT 35 | "always" => ALWAYS 36 | "before" => BEFORE 37 | "E" => E 38 | "EF" => EF 39 | "EG" => EG 40 | "EX" => EX 41 | "forall" => FORALL 42 | "G" => G 43 | "inf" => INF 44 | "never" => NEVER 45 | "next" => NEXT 46 | "U" => U 47 | "X" => X 48 | "abort" => ABORT 49 | "until" => UNTIL 50 | "W" => W 51 | "whilenot" => WHILENOT 52 | "within" => WITHIN 53 | _ => Name s; 54 55 } 56 57rule Token = parse 58 "(*" { commentStart := getLexemeStart lexbuf; 59 commentDepth := 1; 60 SkipComment lexbuf; Token lexbuf } 61 | `@` { AT } 62 | `;` { SEMICOLON } 63 | "[*" { LBRKTSTAR } 64 | "[=" { LBRKTEQ } 65 | "[->" { LBRKTLEFTARROW } 66 | "[*]" { LBRKTSTARRBRKT } 67 | "[+]" { LBRKTPLUSRBRKT } 68 | `,` { COMMA } 69 | `:` { COLON } 70 | `|` { BAR } 71 | "||" { BARBAR } 72 | `&` { AMPERSAND } 73 | "&&" { AMPERSANDAMPERSAND } 74 | "->" { LEFTARROW } 75 | "<->" { LEFTRIGHTARROW } 76 | "|->" { BARLEFTARROW } 77 | "|=>" { BAREQLEFTARROW } 78 | "|=" { BAREQUAL } 79 | `!` { EXCLAIM } 80 | `*` { STAR } 81 | `(` { LPAR } 82 | `)` { RPAR } 83 | `[` { LBRKT } 84 | `]` { RBRKT } 85 | `{` { LBRACE } 86 | `}` { RBRACE } 87 | "before!" { BEFOREX } 88 | "before!_" { BEFOREXU } 89 | "before_" { BEFOREU } 90 | "whilenot!_" { WHILENOTXU } 91 | "eventually!" { EVENTUALLYX } 92 | "next!" { NEXTX } 93 | "next_a" { NEXTA } 94 | "next_a!" { NEXTAX } 95 | "next_e" { NEXTE } 96 | "next_e!" { NEXTEX } 97 | "next_event" { NEXTEVENT } 98 | "next_event!" { NEXTEVENTX } 99 | "next_event_a!" { NEXTEVENTAX } 100 | "next_event_e!" { NEXTEVENTEX } 101 | "until!" { UNTILX } 102 | "until!_" { UNTILXU } 103 | "until_" { UNTILU } 104 | "whilenot!" { WHILENOTX } 105 | "whilenot!_" { WHILENOTXU } 106 | "whilenot_" { WHILENOTU } 107 | "within!" { WITHINX } 108 | "within!_" { WITHINXU } 109 | "within_" { WITHINU } 110 | "X!" { XX } 111 | eof { EOF } 112 | [` ` `\t` `\n` `\r`]{ Token lexbuf } 113 | [`0`-`9`]+ { case Int.fromString (getLexeme lexbuf) of 114 NONE => lexerError lexbuf "internal error" 115 | SOME i => Number i} 116 | [`_``a`-`z``A`-`Z`][`_``a`-`z``A`-`Z``0`-`9`]* 117 { keyword (getLexeme lexbuf) } 118 119 | _ { lexerError lexbuf "Illegal symbol in input" } 120 121and SkipComment = parse 122 "*)" { commentDepth := !commentDepth - 1; 123 if !commentDepth = 0 then () 124 else SkipComment lexbuf } 125 | "(*" { commentDepth := !commentDepth + 1; 126 SkipComment lexbuf } 127 | (eof | `\^Z`) { commentNotClosed lexbuf } 128 | _ { SkipComment lexbuf } 129; 130