parse_env.ml 15.2 KB
Newer Older
1
(*pp camlp4o *)
2
(*-----------------------------------------------------------------------
3
** Copyright (C) 2001, 2002 - Verimag.
4
5
6
7
8
9
10
11
12
13
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
** File: parse_env.ml
** Main author: jahier@imag.fr
*)

open Formula

14
15

let debug_parsing = true
16
17
18
19
  
type read_arc = Arc of node * arc_info * node

type read_automata = Automata of 
20
  node        (* Initial node *)
21
22
23
  * vnt list  (* Input var list *)
  * vnt list  (* Output var list *)
  * vnt list  (* Local var list *)
24
  * vnt list  (* pre var list *)
25
26
27
  * read_arc list  (* Transition list *)

(* Keywords of the automata format *)
28
29
30
31
let lexer = Genlex.make_lexer ["("; ")"; ","; ";"; ".";
			       "&&"; "||"; "!"; "true"; "false"; 
			       "IfThenElseExpr";"IfThenElse";
			       "="; ">"; ">="; "<"; "<="; 
32
33
34
35
			       "+"; "-"; "*"; "/"; "mod"; "%"]

type aut_token = Genlex.token Stream.t

36
37
38
39
let print_genlex_token = 
  fun tok -> 
    let _ =
      match tok with
40
41
42
43
44
45
	  Genlex.Kwd(str)    -> print_string (str ^ " \t(Kwd)")
	| Genlex.Ident(str)  -> print_string (str ^ " \t(Ident)")
	| Genlex.Int(i)      -> print_int i; print_string " \t(Int)"
	| Genlex.Float(f)    -> print_float f; print_string " \t(Float)"
	| Genlex.String(str) -> print_string (str ^ " \t(String)")
	| Genlex.Char(c)     -> print_char c ; print_string " \t(Char)"
46
    in
47
      print_string "\n\t"
48

49
50
51
let print_err_msg tok_list func =
  if debug_parsing then
    begin
52
53
      print_string ("* Parse error in " ^ func ^ ". ");
      print_string ("The next 10 tokens are:\n\t");
54
      List.iter (print_genlex_token) tok_list ;
55
      print_string ("\n");
56
57
58
59
      flush stdout
    end 
  else ()
  
60
61
	

62
63

(** Parsing lists *)
64
65
66
let rec
  (parse_list: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
67
68
69
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
70
71
	  | [< 'Genlex.Kwd "," >] -> [] (* empty list *)   
	  | [< 'Genlex.Kwd "." >] -> [] (* empty list *) 
72
	  | [< 'Genlex.Kwd "%" >] -> [] (* empty list *)  
73
          | [< vnt = parse ; tail = (parse_list_var_tail (parse)) >]
74
75
76
77
	    -> vnt :: tail  
	with e ->
	  print_err_msg tok_list "parse_list";
	  raise e
78
79
and (parse_list_var_tail: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
80
81
82
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser 
83
84
85
	  | [< 'Genlex.Kwd "," >] -> [] (* end of the list *)  
	  | [< 'Genlex.Kwd "." >] -> [] (* end of the list *)  
	  | [< 'Genlex.Kwd "%" >] -> [] (* end of the list *)  
86
87
88
89
90
91
	  | [< 'Genlex.Kwd ";" ; a = parse ;
	       tail = (parse_list_var_tail (parse)) >]
	    -> a :: tail  
	with e ->
	  print_err_msg tok_list "parse_list_var_tail";
	  raise e
92
93


94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
(** Parsing pragmas *)

type pragma = string * string

let rec (parse_pragma: aut_token -> pragma) =
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.String label ; 'Genlex.Ident ":"; 
	       'Genlex.String pragma  >] -> (label, pragma)
	with e ->
	  print_err_msg tok_list "parse_pragma" ;
	  raise e
and
  (parse_pragma_list: aut_token -> pragma list) =
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	( match (Stream.npeek 1 tok) with 
	      [Genlex.Kwd "%"] -> 
		( match tok with parser  
		      [< 'Genlex.Kwd "%" ; pl = (parse_list (parse_pragma)) >] -> pl
		)
	    | _ -> []
	)
      with e ->
	print_err_msg tok_list "parse_pragma_list" ;
	raise e
123

124
125
let rec (parse_automata: aut_token -> read_automata) = 
  fun tok -> 
126
    let tok_list = Stream.npeek 20 tok in
127
128
      try
	match tok with parser  
129
130
131
	    [< 'Genlex.Ident "inputs"; 'Genlex.Kwd "="; li = parse_list_var ;
	       'Genlex.Ident "outputs"; 'Genlex.Kwd "="; lo = parse_list_genvar ;
	       'Genlex.Ident "locals"; 'Genlex.Kwd "="; ll = parse_list_genvar ;
132
	       'Genlex.Ident "pre"; 'Genlex.Kwd "="; lpre = parse_list_prevar ;
133
	       'Genlex.Ident "start_node"; 'Genlex.Kwd "="; 'Genlex.Int node_id ; 
134
	       'Genlex.Kwd "," ;
135
136
	       'Genlex.Ident "arcs"; 'Genlex.Kwd "="; la = parse_list_arc 
		      (List.append li (List.append lo (List.append ll lpre))) 
137
138
	    >]
            -> Automata(node_id, li, lo, ll, lpre, la)
139
140
141
142
	with e ->
	  print_err_msg tok_list "parse_automata";
	  raise e
	    
143

144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
and (parse_list_var: aut_token -> vnt list) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_var) tok
      with e ->
	print_err_msg tok_list "parse_list_var" ;
	raise e
and (parse_var: aut_token -> vnt) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; 
	       prag_var = parse_pragma_list ; 
	       'Genlex.Kwd ",";  'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
	    -> 
	      ( match typ with
		  "bool" -> (var, BoolT)
		| "float" -> (var, FloatT(-.max_float, max_float))
		| "int" -> (var, IntT(min_int, max_int))
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	with e ->
	  print_err_msg tok_list "parse_var" ;
	  raise e

171
172
173
174
175
176
177
178
179
180
181
182
183
and (parse_list_genvar: aut_token -> vnt list) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_genvar) tok
      with e ->
	print_err_msg tok_list "parse_list_genvar" ;
	raise e
and (parse_genvar: aut_token -> vnt) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
184
185
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; pl = parse_pragma_list ;
	       'Genlex.Kwd ","; 'Genlex.Ident typ ;
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
	       vnt = parse_type var typ >]
	    -> vnt
	with e ->
	  print_err_msg tok_list "parse_genvar" ;
	  raise e
and (parse_type:  string -> string -> aut_token -> vnt) =
  fun var typ tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd ")" >] -> 
	      ( match typ with
		    "bool" -> (var, BoolT)
		  | "float" -> (var, FloatT(-.max_float, max_float))
		  | "int" -> (var, IntT(min_int, max_int))
		  | str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	  | [< 'Genlex.Kwd ","; vnt = parse_type_more var typ >] -> vnt
	with e ->
	  print_err_msg tok_list "parse_type" ;
	  raise e
	    
and (parse_type_more:  string -> string -> aut_token -> vnt) =
  fun var typ tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Int min; 'Genlex.Kwd ","; 'Genlex.Int max;  'Genlex.Kwd ")" >] -> 
	      ( match typ with
		    "bool" -> failwith ("*** int expected in .env" )
		  | "float" -> failwith ("*** int expected in .env " )
		  | "int" -> (var, IntT(min, max))
		  | str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	  | [< 'Genlex.Float min; 'Genlex.Kwd ","; 'Genlex.Float max;  'Genlex.Kwd ")" >] -> 
	      ( match typ with
		    "bool" -> failwith ("*** float expected in .env " )
		  | "float" -> (var, FloatT(min, max))
		  | "int" -> failwith ("*** float expected in .env " )
		  | str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	with e ->
	  print_err_msg tok_list "parse_type_more" ;
	  raise e
	    

232
and (parse_list_prevar: aut_token -> vnt list) = 
233
  fun tok -> 
234
235
    let tok_list = Stream.npeek 10 tok in
      try
236
	parse_list (parse_prevar) tok
237
      with e ->
238
	print_err_msg tok_list "parse_list_prevar" ;
239
	raise e
240
and (parse_prevar: aut_token -> vnt) = 
241
  fun tok -> 
242
243
244
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
245
246
247
248
	    [< 'Genlex.Kwd "("; 'Genlex.Ident "pre"; 'Genlex.Kwd "("; 
	       'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident var;  
	       'Genlex.Kwd ")"; pl = parse_pragma_list ; 
	       'Genlex.Kwd ","; 'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
249
	    -> 
250
	      let pre_var = ("_pre" ^ (string_of_int i) ^ var) in
251
	      ( match typ with
252
253
254
		  "bool" -> (pre_var, BoolT)
		| "float" -> (pre_var, FloatT(-.max_float, max_float))
		| "int" -> (pre_var, IntT(min_int, max_int))
255
256
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
257
	with e ->
258
	  print_err_msg tok_list "parse_prevar" ;
259
	  raise e
260

261
262
and (parse_list_arc: vnt list -> aut_token -> read_arc list) = 
  fun vars tok -> 
263
264
    let tok_list = Stream.npeek 10 tok in
      try
265
	parse_list (parse_arc vars) tok
266
267
268
      with e ->
	print_err_msg tok_list "parse_list_arc" ;
	raise e
269
270
and (parse_arc: vnt list -> aut_token -> read_arc) = 
  fun vars tok -> 
271
272
273
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
274
275
276
	    [< 'Genlex.Ident "From"; 'Genlex.Int node_from ; 
	       'Genlex.Ident "To"; 'Genlex.Int node_to ; 
	       'Genlex.Ident "With"; arc_info = parse_arc_info vars  >]
277
278
279
280
	    -> Arc(node_from, arc_info, node_to)
	with e ->
	  print_err_msg tok_list "parse_arc" ;
	  raise e
281
282
and (parse_arc_info: vnt list -> aut_token -> arc_info) = 
  fun vars tok -> 
283
284
285
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
286
	    [< 'Genlex.Int weigth ; 'Genlex.Ident ":"; expr = parse_formula_eps vars >] 
287
288
289
290
	    -> (weigth, expr)
	with e ->
	  print_err_msg tok_list "parse_arc_info" ;
	  raise e
291

292
293
and (parse_formula_eps: vnt list -> aut_token -> formula_eps) = 
  fun vars tok -> 
294
295
296
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser   
297
298
	  | [< 'Genlex.Ident "eps" >] -> Eps
	  | [< 'Genlex.Ident "("; 'Genlex.Ident "eps"; 'Genlex.Ident ")" >] -> Eps
299
	  | [< f = parse_formula vars >] -> Form(f)
300
301
302
303
	with e ->
	  print_err_msg tok_list "parse_formula_eps" ;
	  raise e
	    
304
305
and (parse_formula: vnt list -> aut_token -> formula) = 
  fun vars tok -> 
306
307
308
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
	    [< 'Genlex.Kwd "!"; pl = parse_pragma_list ;
	       f1 = parse_formula vars; 
	       f = parse_more_formula (Not(f1)) vars 
	                                         >] -> f  
	  | [< 'Genlex.Kwd "IfThenElse";  pl = parse_pragma_list ;
	       f1 = parse_formula vars; 
	       f2 = parse_formula vars; 
	       f3 = parse_formula vars           >] -> IteB(f1, f2, f3)
	  | [< 'Genlex.Kwd "("; 
	       f1 = parse_formula vars ; 'Genlex.Kwd ")" ; 
	       f = parse_more_formula f1 vars    >] -> f 
	  | [< 'Genlex.Kwd "true" ; pl = parse_pragma_list ;
	       f = parse_more_formula True vars  >] -> f
	  | [< 'Genlex.Kwd "false" ; pl = parse_pragma_list ;
	       f = parse_more_formula False vars >] -> f
324
325
326
327
328
329
330
331

	  | [< 'Genlex.Ident "pre"; 'Genlex.Kwd "("; 'Genlex.Int i ; 
	       'Genlex.Kwd "," ; 'Genlex.Ident id; 'Genlex.Kwd ")"; 
	       pl = parse_pragma_list ;  
	       f = parse_expr_or_bool_ident ("_pre" ^ (string_of_int i) ^ id) vars
	                                         >] -> f
	  | [< 'Genlex.Ident id ; 
	       pl = parse_pragma_list ; 
332
333
	       f1 = parse_expr_or_bool_ident id vars; 
	       f = parse_more_formula f1 vars    >] -> f
334
335
	  | [< e1 = parse_expr vars ; f = parse_expr_right e1 vars 
	                                         >] -> f
336
337
338
	with e ->
	  print_err_msg tok_list "parse_formula" ;
	  raise e
339

340
341
and (parse_expr_or_bool_ident: string -> vnt list -> aut_token -> formula) = 
  fun id vars tok -> 
342
    let tok_list = Stream.npeek 10 tok in
343
344
345
346
347
348
349
    let (_, vt) = List.find (fun (vn,vt) -> vn = id) vars in
    let var =
      match vt with
	  BoolT -> Ivar("XXX")
	| IntT(_,_) -> Ivar(id)
	| FloatT(_,_) -> Fvar(id)
    in
350
351
      try
	match tok with parser  
352
353
354
355
356
	    [< 'Genlex.Kwd "=";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Eq(var, e2) 
	  | [< 'Genlex.Kwd ">";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Sup(var, e2) 
	  | [< 'Genlex.Kwd ">="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> SupEq(var, e2)
	  | [< 'Genlex.Kwd "<";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Inf(var, e2) 
	  | [< 'Genlex.Kwd "<="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> InfEq(var, e2)
357
	  | [< f = parse_more_formula (Bvar(id)) vars >] -> f 
358
359
360
361
	with e ->
	  print_err_msg tok_list "parse_expr_or_bool_ident" ;
	  raise e

362
363
and (parse_more_formula: formula -> vnt list -> aut_token -> formula) = 
  fun f1 vars tok -> 
364
365
366
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
367
368
369
370
	    [< 'Genlex.Kwd "||"; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> Or(f1, f2)
	  | [< 'Genlex.Kwd "&&"; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> And(f1, f2) 
371
372
373
374
	  | [< >] -> f1
	with e ->
	  print_err_msg tok_list "parse_more_formula" ;
	  raise e
375
376
and (parse_expr_right : expr -> vnt list -> aut_token -> formula) = 
  fun e1 vars tok -> 
377
378
379
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser
380
381
382
383
384
	    [< 'Genlex.Kwd "=";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Eq(e1, e2) 
	  | [< 'Genlex.Kwd ">";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Sup(e1, e2) 
	  | [< 'Genlex.Kwd ">="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> SupEq(e1, e2)
	  | [< 'Genlex.Kwd "<";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Inf(e1, e2) 
	  | [< 'Genlex.Kwd "<="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> InfEq(e1, e2)
385
386
387
388
	with e ->
	  print_err_msg tok_list "parse_expr_rigth" ;
	  raise e
	    
389
390

(* 
391
392
393
 ** The following is copy-paste-adapted from sec 1.8 of the ocaml ref man 
 ** untitled ``pretty printing and parsing''.
 *)
394
395
and (parse_expr: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
396
    match tok with parser  
397
398
399
	[< e1 = parse_mult vars; e = parse_more_adds e1 vars >] -> e
and (parse_more_adds: expr -> vnt list -> aut_token -> expr) = 
  fun e1 vars tok -> 
400
    match tok with parser  
401
402
	[< 'Genlex.Kwd "+"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
403
	   e = parse_more_adds (Sum(e1, e2)) vars >] -> e
404
405
      | [< 'Genlex.Kwd "-"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
406
	   e = parse_more_adds (Diff(e1, e2)) vars >] -> e
407
      | [<  >] -> e1
408
409
and (parse_mult: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
410
    match tok with parser  
411
412
413
	[< e1 = parse_simple vars; e = parse_more_mults e1 vars >] -> e
and (parse_more_mults: expr -> vnt list -> aut_token -> expr) = 
  fun e1 vars tok -> 
414
    match tok with parser  
415
416
	[< 'Genlex.Kwd "*"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
417
	   e = parse_more_mults (Prod(e1, e2)) vars >] -> e
418
419
      | [< 'Genlex.Kwd "/"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
420
	   e = parse_more_mults (Quot(e1, e2)) vars >] -> e
421
422
      | [< 'Genlex.Kwd "mod"; pl = parse_pragma_list ; 
	   e2 = parse_simple vars; 
423
	   e = parse_more_mults (Mod(e1, e2)) vars >] -> e
424
      | [<  >] -> e1
425
426
and (parse_simple: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
427
    match tok with parser  
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
      
      | [< 'Genlex.Ident "pre"; 'Genlex.Kwd "(";  
	   'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident id;   
	   'Genlex.Kwd ")"; pl = parse_pragma_list  >] -> 
	  let s = ("_pre" ^ (string_of_int i) ^ id) in 
	  let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in 
	  let var = 
	    match vt with 
		BoolT -> assert false  
	      | IntT(_,_) -> Ivar(s) 
	      | FloatT(_,_) -> Fvar(s) 
	  in 
	    var 

      | [< 'Genlex.Ident s ; pl = parse_pragma_list >] -> 
443
444
445
	  let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in
	  let var =
	    match vt with
446
		BoolT -> assert false 
447
448
449
450
	      | IntT(_,_) -> Ivar(s)
	      | FloatT(_,_) -> Fvar(s)
	  in
	    var
451
452
  
      | [< 'Genlex.Int i;   pl = parse_pragma_list >] -> Ival(i)
453
454
455
456
      | [< 'Genlex.Float f; pl = parse_pragma_list >] -> Fval(f)
      | [< 'Genlex.Kwd "IfThenElseExpr";  pl = parse_pragma_list ; 
	   f1 = parse_formula vars; 
	   e2 = parse_expr vars; 
457
458
	   e3 = parse_expr vars >] -> Ite(f1, e2, e3) 
      | [< 'Genlex.Kwd "("; e = parse_expr vars; 'Genlex.Kwd ")" >] -> e
459