Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lexerLustreSpec.mll @ 0038002e

History | View | Annotate | Download (3.44 KB)

1
{
2

    
3
  (* open ParserLustreSpec *)
4
  open Parser_lustre
5
  open Utils
6

    
7
  let str_buf = Buffer.create 1024
8

    
9
  exception Error of Location.t
10

    
11
(* As advised by Caml documentation. This way a single lexer rule is
12
   used to handle all the possible keywords. *)
13
let keyword_table =
14
  create_hashtable 20 [
15
  (* "true", TRUE; *)
16
  (* "false", FALSE; *)
17
  "stateless", STATELESS;
18
  "if", IF;
19
  "then", THEN;
20
  "else", ELSE;
21
  "merge", MERGE;
22
  "arrow", ARROW;
23
  "fby", FBY;
24
  "when", WHEN;
25
  "whennot", WHENNOT;
26
  "every", EVERY;
27
  "node", NODE;
28
  "let", LET;
29
  "tel", TEL;
30
  "returns", RETURNS;
31
  "var", VAR;
32
  "imported", IMPORTED;
33
  "wcet", WCET;
34
  "int", TINT;
35
  "bool", TBOOL;
36
  "float", TFLOAT;
37
  "real", TREAL;
38
  "clock", TCLOCK;
39
  "not", NOT;
40
  "tail", TAIL;
41
  "and", AND;
42
  "or", OR;
43
  "xor", OR;
44
  "mod", MOD;
45
  "pre", PRE;
46
  "div", DIV;
47
  "const", CONST;
48
  (* "include", INCLUDE; *)
49
  "assert", ASSERT;
50
  "ensures", ENSURES;
51
  "requires", REQUIRES;
52
  "observer", OBSERVER;
53
  "invariant", INVARIANT;
54
  "behavior", BEHAVIOR;
55
  "assumes", ASSUMES;
56
  "exists", EXISTS;
57
  "forall", FORALL;
58
  ]
59

    
60
}
61

    
62

    
63
let newline = ('\010' | '\013' | "\013\010")
64
let notnewline = [^ '\010' '\013']
65
let blank = [' ' '\009' '\012']
66

    
67
rule token = parse
68
  | "(*"
69
      { comment_line 0 lexbuf }
70
  | "--" notnewline* (newline|eof)
71
      { incr_line lexbuf;
72
      token lexbuf }
73
  | newline
74
      { incr_line lexbuf;
75
	token lexbuf }
76
  | blank +
77
      {token lexbuf}
78
  | '-'? ['0'-'9'] ['0'-'9']* '.' ['0'-'9']*
79
      {FLOAT (float_of_string (Lexing.lexeme lexbuf))}
80
  | '-'? ['0'-'9']+ 
81
      {INT (int_of_string (Lexing.lexeme lexbuf)) }
82
  | '-'? ['0'-'9']+ '.' ['0'-'9']+ ('E'|'e') ('+'|'-') ['0'-'9'] ['0'-'9'] as s {REAL s}
83
 (* | '/' (['_' 'A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '_' '0'-'9']* '/')+ as s
84
      {IDENT s}
85
 *)
86
  | ['_' 'A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '_' '0'-'9']*
87
      {let s = Lexing.lexeme lexbuf in
88
       try
89
	 Hashtbl.find keyword_table s
90
       with Not_found ->
91
	 IDENT s}
92
  | "->" {ARROW}
93
  | "=>" {IMPL}
94
  | "<=" {LTE}
95
  | ">=" {GTE}
96
  | "<>" {NEQ}
97
  | '<' {LT}
98
  | '>' {GT}
99
  | "!=" {NEQ}
100
  | '-' {MINUS}
101
  | '+' {PLUS}
102
  | '/' {DIV}
103
  | '*' {MULT}
104
  | '=' {EQ}
105
  | '(' {LPAR}
106
  | ')' {RPAR}
107
  | ';' {SCOL}
108
  | ':' {COL}
109
  | ',' {COMMA}
110
  | '=' {EQ}
111
  | '/' {DIV}
112
  | "&&" {AMPERAMPER}
113
  | "||" {BARBAR}
114
  | "::" {COLCOL}
115
  | "^" {POWER}
116
  | '"' { Buffer.clear str_buf; string_parse lexbuf }
117
  | eof { EOF }
118
  | _ { raise (Error (Location.curr lexbuf)) }
119
and comment_line n = parse
120
| eof
121
    { raise (Error (Location.curr lexbuf)) }
122
| "(*"
123
    { comment_line (n+1) lexbuf }
124
| "*)"
125
    { if n > 0 then comment_line (n-1) lexbuf else token lexbuf }
126
| newline
127
    { incr_line lexbuf;
128
      comment_line n lexbuf }
129
| _ { comment_line n lexbuf }
130
and string_parse = parse
131
  | "\\\"" as s { Buffer.add_string str_buf s; string_parse lexbuf}
132
  | '"' { STRING (Buffer.contents str_buf) }
133
  | _ as c  { Buffer.add_char str_buf c; string_parse lexbuf }
134

    
135
{
136

    
137
  let annot s =
138
    let lb = Lexing.from_string s in
139
   try
140
     Parser_lustre.lustre_annot(* ParserLustreSpec.lustre_annot *) token lb
141
   with Parsing.Parse_error as _e -> (
142
     Format.eprintf "Lexing error at position %a:@.unexpected token %s@.@?"
143
       (fun fmt p -> Format.fprintf fmt "%s l%i c%i" p.Lexing.pos_fname p.Lexing.pos_lnum p.Lexing.pos_cnum) lb.Lexing.lex_curr_p
144
       (Lexing.lexeme lb);
145
     raise Parsing.Parse_error)
146
     
147

    
148
  let spec s =
149
    let lb = Lexing.from_string s in
150
    Parser_lustre.lustre_spec (*ParserLustreSpec.lustre_spec*) token lb
151

    
152
}