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

open Formula

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

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

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

type aut_token = Genlex.token Stream.t

35
36
37
38
let print_genlex_token = 
  fun tok -> 
    let _ =
      match tok with
39
40
41
42
43
44
	  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)"
45
    in
46
      print_string "\n\t"
47

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

61
62

(** Parsing lists *)
63
64
65
let rec
  (parse_list: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
66
67
68
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
69
	  | [< 'Genlex.Kwd ";"; 'Genlex.Kwd "," >] -> [] (* empty list *)   
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
	  | [< 'Genlex.Kwd ";" ;  tail = (parse_list_var_tail2 (parse)) >]
	    -> tail  
88
89
90
	with e ->
	  print_err_msg tok_list "parse_list_var_tail";
	  raise e
91

92
93
and (parse_list_var_tail2: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
94
    (* This function is introduced to allow lists to be ended by a `;'... *)
95
96
97
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser 
98
	  | [< 'Genlex.Kwd ";"; _ = (parse_list_var_tail3 (parse)) >] -> [] 
99
	  | [< 'Genlex.Kwd "," >] -> [] 
100
	  | [< 'Genlex.Kwd "." >] -> [] 
101
102
103
104
105
	  | [< 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
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
117

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
(** 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
148

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

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

202
203
204
205
206
207
208
209
210
211
212
213
214
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  
215
216
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; pl = parse_pragma_list ;
	       'Genlex.Kwd ","; 'Genlex.Ident typ ;
217
218
219
220
221
222
223
224
225
226
227
228
229
	       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)
230
231
		  | "float" -> (var, FloatT(-.max_float /. 2., max_float /. 2.))
		  | "int" -> (var, IntT(min_int / 2, max_int / 2))
232
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
		  | 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
	    

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

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

338
and (parse_cpt_init: vnt list -> aut_token -> cpt_init) = 
339
340
341
342
  fun vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
343
344
345
346
347
	    [< 'Genlex.Ident "no_loop" >] -> NoLoop
	  | [< 'Genlex.Ident "loop" ; 'Genlex.Int i>] -> Loop(i)
	  | [< 'Genlex.Ident "loop_inf" >] -> LoopInf
	  | [< 'Genlex.Ident "loop_between" ; 'Genlex.Int min ; 'Genlex.Int max
	    >] -> LoopBetween(min, max) 
348
349
	  | [< 'Genlex.Ident "loop_gauss" ; 'Genlex.Float mean ; 'Genlex.Float var
	    >] -> LoopGauss(mean, var)
350
351
352
353
354
	with e ->
	  print_err_msg tok_list "parse_cpt_init" ;
	  raise e


355

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

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

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

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

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