parse_env.ml 18 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
and (parse_list_var_tail2: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
95
    (* This function is introduced to allow lists to be ended by a `;'... *)
96
97
98
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser 
99
	  | [< 'Genlex.Kwd ";"; _ = (parse_list_var_tail3 (parse)) >] -> [] 
100
	  | [< 'Genlex.Kwd "," >] -> [] 
101
	  | [< 'Genlex.Kwd "." >] -> [] 
102
103
104
105
106
	  | [< a = parse ; tail = (parse_list_var_tail (parse)) >]
	    -> a :: tail  
	with e ->
	  print_err_msg tok_list "parse_list_var_tail2";
	  raise e
107
108
109
110
111
112
113
114
115
116
117
and (parse_list_var_tail3: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
    (* This function is also introduced to allow lists to be ended by a `;'... *)
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser 
	  | [< 'Genlex.Kwd "." >] -> [] 
	  | [< 'Genlex.Kwd "," >] -> [] 
	with e ->
	  print_err_msg tok_list "parse_list_var_tail3";
	  raise e
118

119

120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
(** 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
149

150
151
let rec (parse_automata: aut_token -> read_automata) = 
  fun tok -> 
152
    let tok_list = Stream.npeek 20 tok in
153
154
      try
	match tok with parser  
155
156
157
	    [< '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 ;
158
	       'Genlex.Ident "pre"; 'Genlex.Kwd "="; lpre = parse_list_prevar ;
159
	       'Genlex.Ident "start_node"; 'Genlex.Kwd "="; 'Genlex.Int node_id ; 
160
	       'Genlex.Kwd "," ;
161
162
163
164
	       'Genlex.Ident "arcs_nb"; 'Genlex.Kwd "="; 'Genlex.Int arcs_nb ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Ident "nodes_nb"; 'Genlex.Kwd "="; 'Genlex.Int nodes_nb ; 
	       'Genlex.Kwd "," ;
165
166
	       'Genlex.Ident "arcs"; 'Genlex.Kwd "="; la = parse_list_arc 
		      (List.append li (List.append lo (List.append ll lpre))) 
167
168
	    >]
            -> Automata(node_id, li, lo, ll, lpre, la)
169
170
171
172
	with e ->
	  print_err_msg tok_list "parse_automata";
	  raise e
	    
173

174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
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)
193
194
195
196
		| "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 *)
197
198
199
200
201
202
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	with e ->
	  print_err_msg tok_list "parse_var" ;
	  raise e

203
204
205
206
207
208
209
210
211
212
213
214
215
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  
216
217
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; pl = parse_pragma_list ;
	       'Genlex.Kwd ","; 'Genlex.Ident typ ;
218
219
220
221
222
223
224
225
226
227
228
229
230
	       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)
231
232
		  | "float" -> (var, FloatT(-.max_float /. 2., max_float /. 2.))
		  | "int" -> (var, IntT(min_int / 2, max_int / 2))
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
		  | 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
	    

264
and (parse_list_prevar: aut_token -> vnt list) = 
265
  fun tok -> 
266
267
    let tok_list = Stream.npeek 10 tok in
      try
268
	parse_list (parse_prevar) tok
269
      with e ->
270
	print_err_msg tok_list "parse_list_prevar" ;
271
	raise e
272
and (parse_prevar: aut_token -> vnt) = 
273
  fun tok -> 
274
275
276
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
277
278
279
280
	    [< '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 ")" >]
281
	    -> 
282
	      let pre_var = ("_pre" ^ (string_of_int i) ^ var) in
283
	      ( match typ with
284
		  "bool" -> (pre_var, BoolT)
285
286
		| "float" -> (pre_var, FloatT(-.max_float /. 2., max_float /. 2.))
		| "int" -> (pre_var, IntT(min_int / 2, max_int / 2))
287
288
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
289
	with e ->
290
	  print_err_msg tok_list "parse_prevar" ;
291
	  raise e
292

293
294
and (parse_list_arc: vnt list -> aut_token -> read_arc list) = 
  fun vars tok -> 
295
296
    let tok_list = Stream.npeek 10 tok in
      try
297
	parse_list (parse_arc vars) tok
298
299
300
      with e ->
	print_err_msg tok_list "parse_list_arc" ;
	raise e
301
302
and (parse_arc: vnt list -> aut_token -> read_arc) = 
  fun vars tok -> 
303
304
305
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
306
307
	    [< 'Genlex.Ident "From"; 'Genlex.Int node_from ; 
	       'Genlex.Ident "To"; 'Genlex.Int node_to ; 
308
309
	       'Genlex.Ident "With"; arc_info = parse_arc_info vars
	    >]
310
311
312
313
	    -> Arc(node_from, arc_info, node_to)
	with e ->
	  print_err_msg tok_list "parse_arc" ;
	  raise e
314
315
and (parse_arc_info: vnt list -> aut_token -> arc_info) = 
  fun vars tok -> 
316
317
318
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
319
320
321
322
	    [< weigth = (parse_weigth vars) ; 'Genlex.Ident ":"; 
	       expr = parse_formula_eps vars ; 'Genlex.Ident ":"; 
	       cpt_init = (parse_cpt_init vars)
	    >] 
323
324
325
326
	    -> (weigth, expr)
	with e ->
	  print_err_msg tok_list "parse_arc_info" ;
	  raise e
327
and (parse_weigth: vnt list -> aut_token -> weigth) = 
328
329
330
331
  fun vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
332
333
334
335
	    [< 'Genlex.Int w >] -> w (* W(w) *)
	  | [< 'Genlex.Ident "loop_body" >] -> 0 (* LoopBody  *)
	  | [< 'Genlex.Ident "loop_end"  >] -> 0 (* LoopEnd  *)
 	with e ->
336
337
338
339
340
341
342
343
344
345
	  print_err_msg tok_list "parse_weigth" ;
	  raise e

and (parse_cpt_init: vnt list -> aut_token -> 'a list) = 
  fun vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Ident "no_loop" >] -> []
	  | [< 'Genlex.Ident "loop" ; 'Genlex.Int i>] -> []
346
347
	  | [< 'Genlex.Ident "loop_inf" >] -> []
	  | [< 'Genlex.Ident "loop_between" ; 'Genlex.Int i ; 'Genlex.Int i>] -> [] 
348
349
350
351
352
353
	  | [< 'Genlex.Ident "loop_gauss" ; 'Genlex.Float i ; 'Genlex.Float i>] -> [] 
	with e ->
	  print_err_msg tok_list "parse_cpt_init" ;
	  raise e


354

355
356
and (parse_formula_eps: vnt list -> aut_token -> formula_eps) = 
  fun vars tok -> 
357
358
359
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser   
360
361
	  | [< 'Genlex.Ident "eps" >] -> Eps
	  | [< 'Genlex.Ident "("; 'Genlex.Ident "eps"; 'Genlex.Ident ")" >] -> Eps
362
	  | [< f = parse_formula vars >] -> Form(f)
363
364
365
366
	with e ->
	  print_err_msg tok_list "parse_formula_eps" ;
	  raise e
	    
367
368
and (parse_formula: vnt list -> aut_token -> formula) = 
  fun vars tok -> 
369
370
371
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
	    [< '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
387
388
389
390
391
392
393
394

	  | [< '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 ; 
395
396
	       f1 = parse_expr_or_bool_ident id vars; 
	       f = parse_more_formula f1 vars    >] -> f
397
398
	  | [< e1 = parse_expr vars ; f = parse_expr_right e1 vars 
	                                         >] -> f
399
400
401
	with e ->
	  print_err_msg tok_list "parse_formula" ;
	  raise e
402

403
404
and (parse_expr_or_bool_ident: string -> vnt list -> aut_token -> formula) = 
  fun id vars tok -> 
405
    let tok_list = Stream.npeek 10 tok in
406
    let (_, vt) = List.find (fun (vn,vt) -> vn = id) vars in
407
    let some_var =
408
      match vt with
409
410
411
	  BoolT -> None
	| IntT(_,_) -> Some(Ivar(id))
	| FloatT(_,_) -> Some(Fvar(id))
412
    in
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
      ( 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
	      )
      )
435

436
437
and (parse_more_formula: formula -> vnt list -> aut_token -> formula) = 
  fun f1 vars tok -> 
438
439
440
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
441
442
443
	    [< 'Genlex.Kwd "||"; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> Or(f1, f2)
	  | [< 'Genlex.Kwd "&&"; pl = parse_pragma_list ; 
444
445
446
	       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 *)
447
448
	  | [< 'Genlex.Kwd "="; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> Or(And(f1, f2), And(Not(f1), Not(f2))) 
449
450
451
452
	  | [< >] -> f1
	with e ->
	  print_err_msg tok_list "parse_more_formula" ;
	  raise e
453
454
and (parse_expr_right : expr -> vnt list -> aut_token -> formula) = 
  fun e1 vars tok -> 
455
456
457
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser
458
459
460
461
462
	    [< '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)
463
464
465
466
	with e ->
	  print_err_msg tok_list "parse_expr_rigth" ;
	  raise e
	    
467
468

(* 
469
470
471
 ** The following is copy-paste-adapted from sec 1.8 of the ocaml ref man 
 ** untitled ``pretty printing and parsing''.
 *)
472
473
and (parse_expr: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
474
    match tok with parser  
475
476
477
	[< 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 -> 
478
    match tok with parser  
479
480
	[< 'Genlex.Kwd "+"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
481
	   e = parse_more_adds (Sum(e1, e2)) vars >] -> e
482
483
      | [< 'Genlex.Kwd "-"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
484
	   e = parse_more_adds (Diff(e1, e2)) vars >] -> e
485
      | [<  >] -> e1
486
487
and (parse_mult: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
488
    match tok with parser  
489
490
491
	[< 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 -> 
492
    match tok with parser  
493
494
	[< 'Genlex.Kwd "*"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
495
	   e = parse_more_mults (Prod(e1, e2)) vars >] -> e
496
497
      | [< 'Genlex.Kwd "/"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
498
	   e = parse_more_mults (Quot(e1, e2)) vars >] -> e
499
500
      | [< 'Genlex.Kwd "mod"; pl = parse_pragma_list ; 
	   e2 = parse_simple vars; 
501
	   e = parse_more_mults (Mod(e1, e2)) vars >] -> e
502
      | [<  >] -> e1
503
504
and (parse_simple: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
505
    match tok with parser  
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
      
      | [< '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 >] -> 
521
522
523
	  let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in
	  let var =
	    match vt with
524
		BoolT -> assert false 
525
526
527
528
	      | IntT(_,_) -> Ivar(s)
	      | FloatT(_,_) -> Fvar(s)
	  in
	    var
529
530
  
      | [< 'Genlex.Int i;   pl = parse_pragma_list >] -> Ival(i)
531
532
533
534
      | [< 'Genlex.Float f; pl = parse_pragma_list >] -> Fval(f)
      | [< 'Genlex.Kwd "IfThenElseExpr";  pl = parse_pragma_list ; 
	   f1 = parse_formula vars; 
	   e2 = parse_expr vars; 
535
536
	   e3 = parse_expr vars >] -> Ite(f1, e2, e3) 
      | [< 'Genlex.Kwd "("; e = parse_expr vars; 'Genlex.Kwd ")" >] -> e
537