parse_env.ml 23.8 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
15

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

19
20
type label_ce = (string * Control.expr) 

21
type read_automata = Automata of 
22
  node        (* Initial node *)
23
24
25
  * vnt list  (* Input var list *)
  * vnt list  (* Output var list *)
  * vnt list  (* Local var list *)
26
  * vnt list  (* pre var list *)
27
  * label_ce list  (* Definition of labels representing control expressions *)
28
29
30
  * read_arc list  (* Transition list *)

(* Keywords of the automata format *)
31
let lexer = Genlex.make_lexer ["("; ")"; ","; ";"; ".";
32
			       "&&"; "||"; "#"; "!"; "true"; "false"; 
33
			       "IfThenElseNum";"IfThenElse"; "==";
34
			       "="; ">"; ">="; "<"; "<="; 
35
			       "+"; "-"; "*"; "/"; "%"]
36
37
38

type aut_token = Genlex.token Stream.t

39
40
41
42
let print_genlex_token = 
  fun tok -> 
    let _ =
      match tok with
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)"
46
	| Genlex.Float(f)    -> Util.my_print_float f; print_string " \t(Float)"
47
48
	| Genlex.String(str) -> print_string (str ^ " \t(String)")
	| Genlex.Char(c)     -> print_char c ; print_string " \t(Char)"
49
    in
50
      print_string "\n\t"
51

52
let print_err_msg tok_list func =
53
54
55
56
57
58
59
  print_string ("* Parse error in " ^ func ^ ". ");
  print_string ("The next 10 tokens are:\n\t");
  List.iter (print_genlex_token) tok_list ;
  print_string ("\n");
  flush stdout
	
let print_debug msg =
60
  if debug_parsing then
61
62
    (
      print_string msg;
63
      flush stdout
64
    )
65

66
67

(** Parsing lists *)
68
69
70
let rec
  (parse_list: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
    let _ = print_debug ("parse_list \n") in
    let tok_list = Stream.npeek 10 tok in
      try
	(
	  match tok_list with  
	    | (Genlex.Kwd ";")::(Genlex.Kwd ",")::_ ->  Stream.junk tok; [] (* empty list *)   
	    | (Genlex.Kwd ";")::(Genlex.Kwd ".")::_ ->  Stream.junk tok; [] (* empty list *)   
	    | (Genlex.Kwd "," )::_ -> [] (* empty list *)   
	    | (Genlex.Kwd "." )::_ -> [] (* empty list *) 
	    | (Genlex.Kwd "%" )::_ -> [] (* empty list *)  
	    | (Genlex.Kwd ")" )::_ -> [] (* empty list *)  
	    | _ -> (
		match tok with parser
		  | [< vnt = parse ; tail = (parse_list_var_tail (parse)) >]
		    -> vnt :: tail  
	      )
	)
      with e ->
	print_err_msg tok_list "parse_list";
	raise e
91
92
and (parse_list_var_tail: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
    let _ = print_debug ("parse_list_var_t \n") in
    let tok_list = Stream.npeek 10 tok in
      try
	(
	  match tok_list with 
	    | (Genlex.Kwd ";")::(Genlex.Kwd ",")::_ ->  Stream.junk tok; [] (* end of the list *)
	    | (Genlex.Kwd ";")::(Genlex.Kwd ".")::_ ->  Stream.junk tok; [] (* end of the list *)
	    | (Genlex.Kwd "," )::_ -> [] (* end of the list *)  
	    | (Genlex.Kwd "." )::_ -> [] (* end of the list *)  
	    | (Genlex.Kwd "%" )::_ -> [] (* end of the list *)  
	    | (Genlex.Kwd ")" )::_ -> [] (* end of the list *)  
	    | _ -> (
		match tok with parser
		    [< 'Genlex.Kwd ";" ;  tail = (parse_list_var_tail2 (parse)) >]
		    -> tail  
	      )
	)
      with e ->
	print_err_msg tok_list "parse_list_var_tail";
	raise e
113

114
115
and (parse_list_var_tail2: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
116
    let _ = print_debug ("parse_list_var_tail2 \n") in
117
    (* This function is introduced to allow lists to be ended by a `;'... *)
118
119
    let tok_list = Stream.npeek 10 tok in
      try
120
121
122
123
124
125
126
127
128
129
130
	(
	  match tok with parser 
	    | [< 'Genlex.Kwd ";"; _ = (parse_list_var_tail3 (parse)) >] -> [] 
	    | [< 'Genlex.Kwd "," >] -> [] 
	    | [< '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
131
132
and (parse_list_var_tail3: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
133
    let _ = print_debug ("parse_list_var_tail3 \n") in
134
135
136
    (* This function is also introduced to allow lists to be ended by a `;'... *)
    let tok_list = Stream.npeek 10 tok in
      try
137
138
139
140
141
142
143
144
	(
	  match tok with parser 
	    | [< 'Genlex.Kwd "." >] -> [] 
	    | [< 'Genlex.Kwd "," >] -> []
	)
      with e ->
	print_err_msg tok_list "parse_list_var_tail3";
	raise e
145

146

147
148
149
150
151
152
(** Parsing pragmas *)

type pragma = string * string

let rec (parse_pragma: aut_token -> pragma) =
  fun tok -> 
153
    let _ = print_debug ("parse_pragma \n") in
154
155
    let tok_list = Stream.npeek 10 tok in
      try
156
157
158
159
160
161
162
163
	(
	  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
164
165
166
and
  (parse_pragma_list: aut_token -> pragma list) =
  fun tok -> 
167
    let _ = print_debug ("parse_pragma_list \n") in
168
169
170
171
172
    let tok_list = Stream.npeek 10 tok in
      try
	( match (Stream.npeek 1 tok) with 
	      [Genlex.Kwd "%"] -> 
		( match tok with parser  
173
174
175
176
177
		      [< 'Genlex.Kwd "%" ; 
			 pl = (parse_list (parse_pragma));
			 'Genlex.Kwd "%" 
		      >] 
		      -> pl
178
179
180
181
182
183
		)
	    | _ -> []
	)
      with e ->
	print_err_msg tok_list "parse_pragma_list" ;
	raise e
184

185
186
let rec (parse_automata: aut_token -> read_automata) = 
  fun tok -> 
187
    let _ = print_debug ("parse_automata \n") in
188
    let tok_list = Stream.npeek 20 tok in
189
      try
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
	(
	  match tok with parser  
	      [< 'Genlex.Ident "inputs"; 'Genlex.Kwd "="; li = parse_list_var ; 
		 'Genlex.Kwd ",";
		 'Genlex.Ident "outputs"; 'Genlex.Kwd "="; lo = parse_list_genvar ;
		 'Genlex.Kwd ",";
		 'Genlex.Ident "locals"; 'Genlex.Kwd "="; ll = parse_list_genvar ;
		 'Genlex.Kwd ",";
		 'Genlex.Ident "pre"; 'Genlex.Kwd "="; lpre = parse_list_prevar ;
		 'Genlex.Kwd ",";
		 'Genlex.Ident "ctrl_expr"; 'Genlex.Kwd "="; llabel_ce = parse_list_label_ce ;
		 'Genlex.Kwd ",";
		 'Genlex.Ident "start_node"; 'Genlex.Kwd "="; 'Genlex.Int node_id ; 
		 'Genlex.Kwd "," ;
		 'Genlex.Ident "arcs_nb"; 'Genlex.Kwd "="; 'Genlex.Int arcs_nb ; 
		 'Genlex.Kwd "," ;
		 'Genlex.Ident "nodes_nb"; 'Genlex.Kwd "="; 'Genlex.Int nodes_nb ; 
		 'Genlex.Kwd "," ;
		 'Genlex.Ident "arcs"; 'Genlex.Kwd "="; la = parse_list_arc 
							       (List.append li (List.append lo (List.append ll lpre))) ;
		 'Genlex.Kwd ".";
211
	    >]
212
            -> Automata(node_id, li, lo, ll, lpre, llabel_ce, la)
213
214
215
216
	)
      with e ->
	print_err_msg tok_list "parse_automata";
	raise e
217
	    
218

219
220
and (parse_list_var: aut_token -> vnt list) = 
  fun tok -> 
221
    let _ = print_debug ("parse_list_var \n") in
222
223
224
225
226
227
228
229
230
231
    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
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
	(
	  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 /. 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 *)
		    | str -> failwith ("*** Bad type in .luc: " ^ str )
		)
	)
      with e ->
	print_err_msg tok_list "parse_var" ;
	raise e
253

254
255
256
257
258
259
260
261
262
263
264
265
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
266
267
268
269
270
271
272
273
274
275
	(
	  match tok with parser  
	      [< 'Genlex.Kwd "("; 'Genlex.Ident var; pl = parse_pragma_list ;
		 'Genlex.Kwd ","; 'Genlex.Ident typ ;
		 vnt = parse_type var typ >]
	      -> vnt
	)
      with e ->
	print_err_msg tok_list "parse_genvar" ;
	raise e
276
277
278
279
and (parse_type:  string -> string -> aut_token -> vnt) =
  fun var typ tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
280
281
282
283
284
285
286
287
288
289
290
291
292
293
	(
	  match tok with parser  
	      [< 'Genlex.Kwd ")" >] -> 
		( match typ with
		      "bool" -> (var, BoolT)
		    | "float" -> (var, FloatT(-.max_float /. 2., max_float /. 2.))
		    | "int" -> (var, IntT(min_int / 2, max_int / 2))
		    | str -> failwith ("*** Bad type in .luc: " ^ str )
		)
	    | [< 'Genlex.Kwd ","; vnt = parse_type_more var typ >] -> vnt
	)
      with e ->
	print_err_msg tok_list "parse_type" ;
	raise e
294
295
296
297
298
	    
and (parse_type_more:  string -> string -> aut_token -> vnt) =
  fun var typ tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
	(
	  match tok with parser  
	      [< 'Genlex.Int min; 'Genlex.Kwd ","; 'Genlex.Int max;  'Genlex.Kwd ")" >] -> 
		( match typ with
		      "bool" -> failwith ("*** int expected in .luc" )
		    | "float" -> failwith ("*** int expected in .luc " )
		    | "int" -> (var, IntT(min, max))
		    | str -> failwith ("*** Bad type in .luc: " ^ str )
		)
	    | [< 'Genlex.Float min; 'Genlex.Kwd ","; 'Genlex.Float max;  'Genlex.Kwd ")" >] -> 
		( match typ with
		      "bool" -> failwith ("*** float expected in .luc " )
		    | "float" -> (var, FloatT(min, max))
		    | "int" -> failwith ("*** float expected in .luc " )
		    | str -> failwith ("*** Bad type in .luc: " ^ str )
		)
	)
      with e ->
	print_err_msg tok_list "parse_type_more" ;
	raise e
319
320
	    

321
and (parse_list_prevar: aut_token -> vnt list) = 
322
  fun tok -> 
323
324
    let tok_list = Stream.npeek 10 tok in
      try
325
	parse_list (parse_prevar) tok
326
      with e ->
327
	print_err_msg tok_list "parse_list_prevar" ;
328
	raise e
329
and (parse_prevar: aut_token -> vnt) = 
330
  fun tok -> 
331
    let _ = print_debug ("parse_prevar \n") in
332
    let tok_list = Stream.npeek 10 tok in
333
      try (
334
	match tok with parser  
335
336
337
338
	    [< '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 ")" >]
339
	    -> 
340
	      let pre_var = ("_pre" ^ (string_of_int i) ^ var) in
341
	      ( match typ with
342
		  "bool" -> (pre_var, BoolT)
343
344
		| "float" -> (pre_var, FloatT(-.max_float /. 2., max_float /. 2.))
		| "int" -> (pre_var, IntT(min_int / 2, max_int / 2))
345
		| str -> failwith ("*** Bad type in .luc: " ^ str )
346
	      )
347
348
349
350
      )
      with e ->
	print_err_msg tok_list "parse_prevar" ;
	raise e
351

352
353
and (parse_list_label_ce: aut_token -> label_ce list) =
  fun tok -> 
354
    let _ = print_debug ("parse_list_label_ce \n") in
355
356
357
358
359
360
361
362
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_ce) tok
      with e ->
	print_err_msg tok_list "parse_list_label_ce" ;
	raise e
and (parse_ce: aut_token -> label_ce) = 
  fun tok -> 
363
    let _ = print_debug ("parse_ce \n") in
364
    let tok_list = Stream.npeek 10 tok in
365
      try (
366
367
368
369
370
371
372
373
374
	match tok with parser  
	    [< 'Genlex.Kwd "(" ; 
	       'Genlex.Ident label ;	 
	       'Genlex.Kwd "," ; 
	       expr = parse_list_ctrl_expr ; 
	       'Genlex.Kwd ")" 
	    >]
	    -> 
	      (label, expr)
375
376
377
378
      )
      with e ->
	print_err_msg tok_list "parse_ce" ;
	raise e
379
380
and (parse_list_ctrl_expr : aut_token -> Control.expr) =
  fun tok -> 
381
    let _ = print_debug ("parse_list_ctrl_expr  \n") in
382
383
384
385
386
387
388
389
    let tok_list = Stream.npeek 10 tok in
    let ce_list =
      try
	parse_list (parse_ctrl_expr) tok
      with e ->
	print_err_msg tok_list "parse_list_ctrl_expr" ;
	raise e
    in
390
391
392
393
394
395
      if ce_list = [] then (fun x -> x)
      else
	List.fold_left 
	  (fun ce1 ce2 -> (fun st -> ce2 (ce1 st)))
	  (List.hd ce_list) 
	  (List.tl ce_list)
396
397
and (parse_ctrl_expr: aut_token -> Control.expr) = 
  fun tok -> 
398
    let _ = print_debug ("parse_ctrl_expr \n") in
399
    let tok_list = Stream.npeek 10 tok in
400
      try (
401
402
403
404
	match tok with parser  
	    [< 'Genlex.Ident "Set" ; 'Genlex.Ident varname ; 'Genlex.Int i 
	    >] ->
	      (Control.set varname i)
405
406
407
408
	  | [< 'Genlex.Ident "Set_between" ; 'Genlex.Ident varname ;
	       'Genlex.Int i ; 'Genlex.Int min ; 'Genlex.Int max 
	    >] -> 
	      (Control.set_between varname i min max)
409
410
411
412
	  | [< 'Genlex.Ident "Draw_between" ; 'Genlex.Ident varname ;
	       'Genlex.Int min ; 'Genlex.Int max 
	    >] -> 
	      (Control.draw_between varname min max)
413
414
	  | [< 'Genlex.Ident "Draw_gauss" ; 'Genlex.Ident varname ; 
	       m = parse_float ; dev = parse_float 
415
416
417
418
419
420
421
422
423
424
425
426
427
428
	    >] -> 
	      (Control.draw_gauss varname m dev)
	  | [< 'Genlex.Ident "Dec" ; 'Genlex.Ident varname 
	    >] -> 
	      (Control.dec varname)
	  | [< 'Genlex.Kwd "IfThenElse" ; test = parse_test_expr ; 
	       'Genlex.Kwd "(" ;  
	       cel_then = parse_list_ctrl_expr ; 
	       'Genlex.Kwd ")" ;  
	       'Genlex.Kwd "(" ;  
	       cel_else = parse_list_ctrl_expr ; 
	       'Genlex.Kwd ")" 
	    >] ->  
	      Control.ite test cel_then cel_else
429
430
431
432
      )
      with e ->
	print_err_msg tok_list "parse_ctrl_expr" ;
	raise e
433

434
435
and (parse_float: aut_token -> float) =
  fun tok -> 
436
    let _ = print_debug ("parse_float \n") in
437
    let tok_list = Stream.npeek 10 tok in
438
      try (
439
440
441
	match tok with parser  
	    [< 'Genlex.Float f >] -> f
	  | [< 'Genlex.Int i >] -> (float_of_int i)
442
443
444
445
      )
      with e ->
	print_err_msg tok_list "parse_float" ;
	raise e
446
447


448
449
and (parse_int_or_var: aut_token -> Control.number) =
  fun tok -> 
450
    let _ = print_debug ("parse_int_or_var \n") in
451
    let tok_list = Stream.npeek 10 tok in
452
      try (
453
454
455
	match tok with parser  
	    [< 'Genlex.Int i >] -> Control.IntExpr(i)
	  | [< 'Genlex.Ident id >] -> Control.VarExpr(id)
456
457
458
459
      )
      with e ->
	print_err_msg tok_list "parse_int_or_var" ;
	raise e
460
461
462
	    
and (parse_test_expr: aut_token -> Control.test) =
  fun tok -> 
463
    let _ = print_debug ("parse_test_expr \n") in
464
    let tok_list = Stream.npeek 10 tok in
465
      try (
466
	match tok with parser
467
468
469
470
471
	    [< 'Genlex.Kwd "(" ; ct = parse_test_expr ; 'Genlex.Kwd ")" >]
	    ->
	      ct
	  |
	    [< 'Genlex.Kwd op ; n1 = parse_int_or_var ; n2 = parse_int_or_var>]
472
473
474
475
476
477
478
	    -> 
	      match op with
		| "<"  -> Control.GtExpr(n2, n1)
		| "<=" -> Control.GeExpr(n2, n1)
		| ">"  -> Control.GtExpr(n1, n2)
		| ">=" -> Control.GeExpr(n1, n2)
		| "="  -> Control.EqExpr(n1, n2)
479
		| "=="  -> Control.EqExpr(n1, n2)
480
		| _ -> assert false
481
482
483
484
      )
      with e ->
	print_err_msg tok_list "parse_test_expr" ;
	raise e
485
486
	    

487
488
and (parse_list_arc: vnt list -> aut_token -> read_arc list) = 
  fun vars tok -> 
489
    let _ = print_debug ("parse_list_arc \n") in
490
491
    let tok_list = Stream.npeek 10 tok in
      try
492
	parse_list (parse_arc vars) tok
493
494
495
      with e ->
	print_err_msg tok_list "parse_list_arc" ;
	raise e
496
497
and (parse_arc: vnt list -> aut_token -> read_arc) = 
  fun vars tok -> 
498
    let _ = print_debug ("parse_arc \n") in
499
    let tok_list = Stream.npeek 10 tok in
500
      try (
501
	match tok with parser  
502
503
504
505
506
507
	    [< 'Genlex.Ident "From"; 
	       'Genlex.Int node_from ; 
	       'Genlex.Ident "To"; 
	       'Genlex.Int node_to ; 
	       'Genlex.Ident "With"; 
	       arc_info = parse_arc_info vars
508
	    >]
509
	    -> Arc(node_from, arc_info, node_to)
510
511
512
513
      ) 
      with e ->
	print_err_msg tok_list "parse_arc" ;
	raise e
514
515
and (parse_arc_info: vnt list -> aut_token -> arc_info) = 
  fun vars tok -> 
516
    let _ = print_debug ("parse_arc_info \n") in
517
    let tok_list = Stream.npeek 10 tok in
518
      try (
519
	match tok with parser  
520
521
522
523
	    [< weight = (parse_weight vars) ; 
	       'Genlex.Ident ":"; 
	       expr = parse_formula_eps vars ; 
	       pc = parse_post_cond_id
524
	    >] 
525
	    -> (weight, expr, pc)
526
527
528
529
      ) 
      with e ->
	print_err_msg tok_list "parse_arc_info" ;
	raise e
530
531
and (parse_post_cond_id: aut_token -> string) =
  fun tok -> 
532
    let _ = print_debug ("parse_post_cond_id \n") in
533
     let tok_list = Stream.npeek 10 tok in
534
      try (
535
536
537
538
539
540
	match (Stream.npeek 2 tok) with
	    [ Genlex.Ident ":"; Genlex.Ident label ] -> 
	      Stream.junk tok;
	      Stream.junk tok;
	      label
	  | _ -> "identity"
541
542
543
544
      )
      with e ->
	print_err_msg tok_list "parse_post_cond_id" ;
	raise e
545
and (parse_weight: vnt list -> aut_token -> weight) = 
546
  fun vars tok -> 
547
    let _ = print_debug ("parse_weight \n") in
548
    let tok_list = Stream.npeek 10 tok in
549
      try (
550
	match tok with parser  
551
552
553
554
555
	    [< 'Genlex.Int w >] -> Wint(w)
	  | [< 'Genlex.Kwd "!" ; 
	       'Genlex.Ident lbl >] 
	    -> Wident_not_sig(lbl)
	  | [< 'Genlex.Ident lbl >] -> Wident(lbl)
556
557
558
559
      )
      with e ->
	print_err_msg tok_list "parse_weight" ;
	raise e
560
561


562
563
and (parse_formula_eps: vnt list -> aut_token -> formula_eps) = 
  fun vars tok -> 
564
    let tok_list = Stream.npeek 10 tok in
565
      try (
566
	match tok with parser   
567
568
569
570
571
572
573
574
575
576
577
578
579
	  | 
	    [< 'Genlex.Ident "eps" >] -> Eps
	  | 
	    [< 'Genlex.Ident "("; fe = parse_formula_eps vars ; 
	       'Genlex.Ident ")" 
	    >] 
	    -> fe
	  | 
	    [< f = parse_formula vars >] -> Form(f)
      )
      with e ->
	print_err_msg tok_list "parse_formula_eps" ;
	raise e
580
	    
581
582
and (parse_formula: vnt list -> aut_token -> formula) = 
  fun vars tok -> 
583
584
    let tok_list = Stream.npeek 10 tok in
      try
585
	(
586
	match tok with parser  
587
	    [< 'Genlex.Kwd "!"; pl = parse_pragma_list ;
588
589
	       f = parse_formula vars
	    >] -> Not(f)
590
591
	  | 
	    [< 'Genlex.Kwd "IfThenElse";  pl = parse_pragma_list ;
592
593
	       f1 = parse_formula vars; 
	       f2 = parse_formula vars; 
594
595
596
597
	       f3 = parse_formula vars           
	    >] 
	    -> IteB(f1, f2, f3)
	  | 
598
599
600
	    [< 'Genlex.Kwd "==";  pl = parse_pragma_list ;
	       f1 = parse_formula vars; 
	       f2 = parse_formula vars
601
	    >] 
602
	    -> Or(And(f1, f2), And(Not(f1), Not(f2))) 
603
	  | 
604
	    [< 'Genlex.Kwd "true" ; pl = parse_pragma_list
605
	    >] 
606
	    -> True
607
	  | 
608
	    [< 'Genlex.Kwd "false" ; pl = parse_pragma_list
609
	    >] 
610
	    -> False
611
	  | 
612
613
614
615
616
617
618
	    [< 'Genlex.Kwd "("; f = parse_formula vars ; 'Genlex.Kwd ")"
	    >]
	    -> f 
	  |  
	    [< 'Genlex.Kwd "||"; pl = parse_pragma_list ;
	       f1 = parse_formula vars ;
	       f2 = parse_formula vars 
619
	    >] 
620
	    -> Or(f1, f2)
621
	  | 
622
623
624
	    [< 'Genlex.Kwd "&&"; pl = parse_pragma_list ;
	       f1 = parse_formula vars ; 
	       f2 = parse_formula vars 
625
	    >] 
626
627
	    -> 
	      And(f1, f2)
628
	  | 
629
630
631
	    [< 'Genlex.Kwd "#"; pl = parse_pragma_list ; 
	       f1 = parse_formula vars ;
	       f2 = parse_formula vars 
632
	    >] 
633
	    -> And(Or(f1, f2), Not(And(f1, f2))) (* xor *)
634

635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
	  | 
	    [< 'Genlex.Kwd "=";  pl = parse_pragma_list ; 
	       e1 = parse_expr vars ; e2 = parse_expr vars 
	    >] 
	    -> Eq(e1, e2) 
	  | 
	    [< 'Genlex.Kwd ">";  pl = parse_pragma_list ; 
	       e1 = parse_expr vars ;e2 = parse_expr vars 
	    >] 
	    -> Sup(e1, e2) 
	  | 
	    [< 'Genlex.Kwd ">="; pl = parse_pragma_list ; 
	       e1 = parse_expr vars ;e2 = parse_expr vars 
	    >] 
	    -> SupEq(e1, e2)
	  | 
	    [< 'Genlex.Kwd "<";  pl = parse_pragma_list ; 
	       e1 = parse_expr vars ; e2 = parse_expr vars 
	    >] 
	    -> Inf(e1, e2) 
	  | 
	    [< 'Genlex.Kwd "<="; pl = parse_pragma_list ; 
	       e1 = parse_expr vars ;e2 = parse_expr vars 
	    >] 
	    -> InfEq(e1, e2)
	  | 
	    [< 'Genlex.Ident "pre"; 'Genlex.Kwd "("; 'Genlex.Int i ; 
	       'Genlex.Kwd "," ; 'Genlex.Ident id; 'Genlex.Kwd ")"; 
	       pl = parse_pragma_list
	    >]
	    ->
	      let pre_id = ("_pre" ^ (string_of_int i) ^ id) in
	      (* Ditto *)
	      let (_, vt) = List.find (fun (vn,vt) -> vn = pre_id) vars in
		( match vt with
		    BoolT -> Bvar(pre_id)
		  | _  -> 
		      failwith ("* Parse error: " ^ pre_id ^ " is declared as a" ^
				" boolean and is used as a numeric.\n ")
		)
	  | 
	    [< 'Genlex.Ident id ; pl = parse_pragma_list >] 
	    -> 
	      (* When an ident is encountered, it can be a numeric one *)
	      let (_, vt) = List.find (fun (vn,vt) -> vn = id) vars in
		( match vt with
		    BoolT -> Bvar(id)
		  | _  -> 
		      failwith ("* Parse error: " ^ id ^ " is declared as a" ^
				" boolean and is used as a numeric.\n ")
		)
	)
      with e ->
	print_err_msg tok_list "parse_formula" ;
	raise e
690
	    
691

692

693
(* 
694
695
696
 ** The following is copy-paste-adapted from sec 1.8 of the ocaml ref man 
 ** untitled ``pretty printing and parsing''.
 *)
697
698
and (parse_expr: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
699
    let _ = print_debug ("parse_expr \n") in
700
    let tok_list = Stream.npeek 10 tok in
701
      try (
702
703
	match tok with parser  
	    [< e1 = parse_mult vars; e = parse_more_adds e1 vars >] -> e
704
705
706
707
      )
      with e ->
	print_err_msg tok_list "parse_expr" ;
	raise e
708
709
and (parse_more_adds: expr -> vnt list -> aut_token -> expr) = 
  fun e1 vars tok -> 
710
    let _ = print_debug ("parse_more_adds \n") in
711
    let tok_list = Stream.npeek 10 tok in
712
      try (
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
	match tok with parser  
	    [< 'Genlex.Kwd "+"; 
	       pl = parse_pragma_list ;
	       e2 = parse_mult vars; 
	       e = parse_more_adds (Sum(e1, e2)) vars 
	    >] 
	    -> e
	  | [< 'Genlex.Kwd "-"; 
	       pl = parse_pragma_list ;
	       e2 = parse_mult vars; 
	       e = parse_more_adds (Diff(e1, e2)) vars 
	    >] 
	    -> e
	  | [< >] 
	    -> e1
728
729
730
731
      )
      with e ->
	print_err_msg tok_list "parse_more_adds" ;
	raise e
732

733
734
and (parse_mult: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
735
    let _ = print_debug ("parse_mult \n") in
736
    let tok_list = Stream.npeek 10 tok in
737
      try (
738
739
	match tok with parser  
	    [< e1 = parse_simple vars; e = parse_more_mults e1 vars >] -> e
740
741
742
743
      )
      with e ->
	print_err_msg tok_list "parse_more_adds" ;
	raise e
744
745
and (parse_more_mults: expr -> vnt list -> aut_token -> expr) = 
  fun e1 vars tok -> 
746
    let _ = print_debug ("parse_more_mults \n") in
747
    let tok_list = Stream.npeek 10 tok in
748
      try (
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
	match tok with parser  
	    [< 'Genlex.Kwd "*"; 
	       pl = parse_pragma_list ;  
	       e2 = parse_simple vars; 
	       e = parse_more_mults (Prod(e1, e2)) vars 
	    >] 
	    -> e
	  | [< 'Genlex.Kwd "/"; 
	       pl = parse_pragma_list ;  
	       e2 = parse_simple vars; 
	       e = parse_more_mults (Quot(e1, e2)) vars 
	    >] 
	    -> e
	  | [< 'Genlex.Ident "mod"; 
	       pl = parse_pragma_list ; 
	       e2 = parse_simple vars; 
	       e = parse_more_mults (Mod(e1, e2)) vars 
	    >] 
	    -> e
	  | [<  >] 
	    -> e1
770
771
772
773
      )
      with e ->
	print_err_msg tok_list "parse_more_mults" ;
	raise e
774
775
and (parse_simple: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
776
    let _ = print_debug ("parse_simple \n") in
777
    let tok_list = Stream.npeek 10 tok in
778
      try (
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
	match tok with parser  
	    
	  | [< '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 >] -> 
	      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.Kwd "-"; e = parse_minus_int_or_float vars >] -> e
	  | [< 'Genlex.Int i;   pl = parse_pragma_list >] -> Ival(i)
	  | [< 'Genlex.Float f; pl = parse_pragma_list >] -> Fval(f)

	  | [< 'Genlex.Kwd "IfThenElseNum";  pl = parse_pragma_list ; 
	       f1 = parse_formula vars; 
	       e2 = parse_expr vars; 
	       e3 = parse_expr vars >] -> Ite(f1, e2, e3) 
	  | [< 'Genlex.Kwd "("; e = parse_expr vars; 'Genlex.Kwd ")" >] -> e
813

814
815
816
817
      )
      with e ->
	print_err_msg tok_list "parse_simple" ;
	raise e
818
819
and (parse_minus_int_or_float: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
820
    let _ = print_debug ("parse_minus_int_or_float \n") in
821
    let tok_list = Stream.npeek 10 tok in
822
      try (
823
824
825
	match tok with parser  
	    [< 'Genlex.Int i;   pl = parse_pragma_list >] -> Ival(-i)
	  | [< 'Genlex.Float f; pl = parse_pragma_list >] -> Fval(-.f)
826
827
828
829
      )
      with e ->
	print_err_msg tok_list "parse_minus_int_or_float" ;
	raise e