parse_env.ml 17.8 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
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
and (parse_weigth: vnt list -> aut_token -> int) = 
  fun vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Int w >] -> w
	  | [< 'Genlex.Ident "dyn" >] -> -1
	with e ->
	  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>] -> []
	  | [< 'Genlex.Ident "loop_betwenn" ; 'Genlex.Int i ; 'Genlex.Int i>] -> [] 
	  | [< 'Genlex.Ident "loop_gauss" ; 'Genlex.Float i ; 'Genlex.Float i>] -> [] 
	with e ->
	  print_err_msg tok_list "parse_cpt_init" ;
	  raise e


352

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

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

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

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

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