parse_env.ml 16.5 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
let lexer = Genlex.make_lexer ["("; ")"; ","; ";"; ".";
29
			       "&&"; "||"; "#"; "!"; "true"; "false"; 
30
31
			       "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
	  | [< 'Genlex.Kwd ";"; 'Genlex.Kwd "," >] -> [] (* empty list *)   
71
72
	  | [< 'Genlex.Kwd "," >] -> [] (* empty list *)   
	  | [< 'Genlex.Kwd "." >] -> [] (* empty list *) 
73
	  | [< 'Genlex.Kwd "%" >] -> [] (* empty list *)  
74
          | [< vnt = parse ; tail = (parse_list_var_tail (parse)) >]
75
76
77
78
	    -> vnt :: tail  
	with e ->
	  print_err_msg tok_list "parse_list";
	  raise e
79
80
and (parse_list_var_tail: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
81
82
83
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser 
84
85
86
	  | [< 'Genlex.Kwd "," >] -> [] (* end of the list *)  
	  | [< 'Genlex.Kwd "." >] -> [] (* end of the list *)  
	  | [< 'Genlex.Kwd "%" >] -> [] (* end of the list *)  
87
88
	  | [< 'Genlex.Kwd ";" ;  tail = (parse_list_var_tail2 (parse)) >]
	    -> tail  
89
90
91
	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
and (parse_list_var_tail2: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
    (* This function is introduced to allow lists to be ended by a `;' *)
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser 
	  | [< 'Genlex.Kwd "," >] -> [] 
	  | [< a = parse ; tail = (parse_list_var_tail (parse)) >]
	    -> a :: tail  
	with e ->
	  print_err_msg tok_list "parse_list_var_tail2";
	  raise e

106

107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
(** 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
136

137
138
let rec (parse_automata: aut_token -> read_automata) = 
  fun tok -> 
139
    let tok_list = Stream.npeek 20 tok in
140
141
      try
	match tok with parser  
142
143
144
	    [< '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 ;
145
	       'Genlex.Ident "pre"; 'Genlex.Kwd "="; lpre = parse_list_prevar ;
146
	       'Genlex.Ident "start_node"; 'Genlex.Kwd "="; 'Genlex.Int node_id ; 
147
	       'Genlex.Kwd "," ;
148
149
150
151
	       'Genlex.Ident "arcs_nb"; 'Genlex.Kwd "="; 'Genlex.Int arcs_nb ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Ident "nodes_nb"; 'Genlex.Kwd "="; 'Genlex.Int nodes_nb ; 
	       'Genlex.Kwd "," ;
152
153
	       'Genlex.Ident "arcs"; 'Genlex.Kwd "="; la = parse_list_arc 
		      (List.append li (List.append lo (List.append ll lpre))) 
154
155
	    >]
            -> Automata(node_id, li, lo, ll, lpre, la)
156
157
158
159
	with e ->
	  print_err_msg tok_list "parse_automata";
	  raise e
	    
160

161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
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)
180
181
182
183
		| "float" -> (var, FloatT(-.max_float /. 2., max_float /. 2.))
		| "int" -> (var, IntT(min_int / 2, max_int / 2))
		    (* We divide by 2 so that domains are always smaller 
		       than max_int resp max_float *)
184
185
186
187
188
189
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	with e ->
	  print_err_msg tok_list "parse_var" ;
	  raise e

190
191
192
193
194
195
196
197
198
199
200
201
202
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  
203
204
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; pl = parse_pragma_list ;
	       'Genlex.Kwd ","; 'Genlex.Ident typ ;
205
206
207
208
209
210
211
212
213
214
215
216
217
	       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)
218
219
		  | "float" -> (var, FloatT(-.max_float /. 2., max_float /. 2.))
		  | "int" -> (var, IntT(min_int / 2, max_int / 2))
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
		  | 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
	    

251
and (parse_list_prevar: aut_token -> vnt list) = 
252
  fun tok -> 
253
254
    let tok_list = Stream.npeek 10 tok in
      try
255
	parse_list (parse_prevar) tok
256
      with e ->
257
	print_err_msg tok_list "parse_list_prevar" ;
258
	raise e
259
and (parse_prevar: aut_token -> vnt) = 
260
  fun tok -> 
261
262
263
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
264
265
266
267
	    [< '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 ")" >]
268
	    -> 
269
	      let pre_var = ("_pre" ^ (string_of_int i) ^ var) in
270
	      ( match typ with
271
		  "bool" -> (pre_var, BoolT)
272
273
		| "float" -> (pre_var, FloatT(-.max_float /. 2., max_float /. 2.))
		| "int" -> (pre_var, IntT(min_int / 2, max_int / 2))
274
275
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
276
	with e ->
277
	  print_err_msg tok_list "parse_prevar" ;
278
	  raise e
279

280
281
and (parse_list_arc: vnt list -> aut_token -> read_arc list) = 
  fun vars tok -> 
282
283
    let tok_list = Stream.npeek 10 tok in
      try
284
	parse_list (parse_arc vars) tok
285
286
287
      with e ->
	print_err_msg tok_list "parse_list_arc" ;
	raise e
288
289
and (parse_arc: vnt list -> aut_token -> read_arc) = 
  fun vars tok -> 
290
291
292
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
293
294
295
	    [< 'Genlex.Ident "From"; 'Genlex.Int node_from ; 
	       'Genlex.Ident "To"; 'Genlex.Int node_to ; 
	       'Genlex.Ident "With"; arc_info = parse_arc_info vars  >]
296
297
298
299
	    -> Arc(node_from, arc_info, node_to)
	with e ->
	  print_err_msg tok_list "parse_arc" ;
	  raise e
300
301
and (parse_arc_info: vnt list -> aut_token -> arc_info) = 
  fun vars tok -> 
302
303
304
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
305
	    [< 'Genlex.Int weigth ; 'Genlex.Ident ":"; expr = parse_formula_eps vars >] 
306
307
308
309
	    -> (weigth, expr)
	with e ->
	  print_err_msg tok_list "parse_arc_info" ;
	  raise e
310

311
312
and (parse_formula_eps: vnt list -> aut_token -> formula_eps) = 
  fun vars tok -> 
313
314
315
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser   
316
317
	  | [< 'Genlex.Ident "eps" >] -> Eps
	  | [< 'Genlex.Ident "("; 'Genlex.Ident "eps"; 'Genlex.Ident ")" >] -> Eps
318
	  | [< f = parse_formula vars >] -> Form(f)
319
320
321
322
	with e ->
	  print_err_msg tok_list "parse_formula_eps" ;
	  raise e
	    
323
324
and (parse_formula: vnt list -> aut_token -> formula) = 
  fun vars tok -> 
325
326
327
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
	    [< '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
343
344
345
346
347
348
349
350

	  | [< '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 ; 
351
352
	       f1 = parse_expr_or_bool_ident id vars; 
	       f = parse_more_formula f1 vars    >] -> f
353
354
	  | [< e1 = parse_expr vars ; f = parse_expr_right e1 vars 
	                                         >] -> f
355
356
357
	with e ->
	  print_err_msg tok_list "parse_formula" ;
	  raise e
358

359
360
and (parse_expr_or_bool_ident: string -> vnt list -> aut_token -> formula) = 
  fun id vars tok -> 
361
    let tok_list = Stream.npeek 10 tok in
362
    let (_, vt) = List.find (fun (vn,vt) -> vn = id) vars in
363
    let some_var =
364
      match vt with
365
366
367
	  BoolT -> None
	| IntT(_,_) -> Some(Ivar(id))
	| FloatT(_,_) -> Some(Fvar(id))
368
    in
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
      ( match some_var with
	    None -> 
	      ( try
		 match tok with parser
		      [< f = parse_more_formula (Bvar(id)) vars >] -> f 
		 with e ->
		   print_err_msg tok_list "parse_expr_or_bool_ident" ;
		   raise e
	      )
	  | Some(var) -> 
	      ( try
		  match tok with parser  
		      [< '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)
	      with e ->
		print_err_msg tok_list "parse_expr_or_bool_ident" ;
		raise e
	      )
      )
391

392
393
and (parse_more_formula: formula -> vnt list -> aut_token -> formula) = 
  fun f1 vars tok -> 
394
395
396
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
397
398
399
	    [< 'Genlex.Kwd "||"; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> Or(f1, f2)
	  | [< 'Genlex.Kwd "&&"; pl = parse_pragma_list ; 
400
401
402
	       f2 = parse_formula vars >] -> And(f1, f2)
	  | [< 'Genlex.Kwd "#"; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> And(Or(f1, f2), Not(And(f1, f2))) (* xor *)
403
404
	  | [< 'Genlex.Kwd "="; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> Or(And(f1, f2), And(Not(f1), Not(f2))) 
405
406
407
408
	  | [< >] -> f1
	with e ->
	  print_err_msg tok_list "parse_more_formula" ;
	  raise e
409
410
and (parse_expr_right : expr -> vnt list -> aut_token -> formula) = 
  fun e1 vars tok -> 
411
412
413
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser
414
415
416
417
418
	    [< '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)
419
420
421
422
	with e ->
	  print_err_msg tok_list "parse_expr_rigth" ;
	  raise e
	    
423
424

(* 
425
426
427
 ** The following is copy-paste-adapted from sec 1.8 of the ocaml ref man 
 ** untitled ``pretty printing and parsing''.
 *)
428
429
and (parse_expr: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
430
    match tok with parser  
431
432
433
	[< 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 -> 
434
    match tok with parser  
435
436
	[< 'Genlex.Kwd "+"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
437
	   e = parse_more_adds (Sum(e1, e2)) vars >] -> e
438
439
      | [< 'Genlex.Kwd "-"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
440
	   e = parse_more_adds (Diff(e1, e2)) vars >] -> e
441
      | [<  >] -> e1
442
443
and (parse_mult: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
444
    match tok with parser  
445
446
447
	[< 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 -> 
448
    match tok with parser  
449
450
	[< 'Genlex.Kwd "*"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
451
	   e = parse_more_mults (Prod(e1, e2)) vars >] -> e
452
453
      | [< 'Genlex.Kwd "/"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
454
	   e = parse_more_mults (Quot(e1, e2)) vars >] -> e
455
456
      | [< 'Genlex.Kwd "mod"; pl = parse_pragma_list ; 
	   e2 = parse_simple vars; 
457
	   e = parse_more_mults (Mod(e1, e2)) vars >] -> e
458
      | [<  >] -> e1
459
460
and (parse_simple: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
461
    match tok with parser  
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
      
      | [< '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 >] -> 
477
478
479
	  let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in
	  let var =
	    match vt with
480
		BoolT -> assert false 
481
482
483
484
	      | IntT(_,_) -> Ivar(s)
	      | FloatT(_,_) -> Fvar(s)
	  in
	    var
485
486
  
      | [< 'Genlex.Int i;   pl = parse_pragma_list >] -> Ival(i)
487
488
489
490
      | [< 'Genlex.Float f; pl = parse_pragma_list >] -> Fval(f)
      | [< 'Genlex.Kwd "IfThenElseExpr";  pl = parse_pragma_list ; 
	   f1 = parse_formula vars; 
	   e2 = parse_expr vars; 
491
492
	   e3 = parse_expr vars >] -> Ite(f1, e2, e3) 
      | [< 'Genlex.Kwd "("; e = parse_expr vars; 'Genlex.Kwd ")" >] -> e
493