Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

parse_env.ml 32.8 KB
Newer Older
1
(*pp camlp4o *)
2
(*-----------------------------------------------------------------------
3
** Copyright (C) 2001 - 2003 - 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
type label_ce = (string * Control.expr) 
20
type formula_def = (string * formula) 
21

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

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

type aut_token = Genlex.token Stream.t

41

42
43
44
let default_max_float = 1000.
let default_max_int = 1000
let default_min_int = -1000
45

46
47
48
49
50
51
52
53
54
55
56
let print_err_msg ic tok tok_list func msg msg2 =

  (* Try to guess the char number from the tok number. *)
  let n = Stream.count tok in
  let print_genlex_token = 
    fun tok -> 
      let _ =
	match tok with
	    Genlex.Kwd(str)    -> print_string ("`" ^ str ^ "' ")
	  | Genlex.Ident(str)  -> print_string ("`" ^ str ^ "' ")
	  | Genlex.Int(i)      -> print_string "`"; print_int i; print_string "' "
57
58
	  | Genlex.Float(f)    -> 
	      print_string "`"; print_float f; print_string "' "
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
	  | Genlex.String(str) -> print_string ("`" ^ str ^ "' ")
	  | Genlex.Char(c)     -> print_string "`"; print_char c ; print_string "' "
      in
	print_string " "
  in

  let  remove_sep str =
    let blank_str = "[\010\|\013\|\009\|\026\|\012\|\"\| ]" in
    let blank_reg =  Str.regexp blank_str in
      Str.global_replace blank_reg "" str
  in
  let add_quotes str =
    let str2 = ("`" ^ (Str.global_replace (Str.regexp "[ ]") "' `" str) ^ "'") in
    let str3 = Str.global_replace (Str.regexp "[\n]") "'\n" str2 in
    let str4 = Str.global_replace (Str.regexp "[\t]") "\t`" str3 in
      str4
 (*     let str5 =  Str.global_replace (Str.regexp "`<") "<" str4 in *)
(*       Str.global_replace (Str.regexp ">'") ">" str5 *)
  in  
  let string_of_genlex_token = 
    fun tok -> 
80
      match tok with
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
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
136
137
138
139
	  Genlex.Kwd(str)    -> str
	| Genlex.Ident(str)  -> str
	| Genlex.Int(i)      -> string_of_int i
	| Genlex.Float(f)    -> string_of_float f
	| Genlex.String(str) -> remove_sep str
	| Genlex.Char(c)     -> Char.escaped c
  in
  let rec skip_n_non_sep_char n s =
    if n = 0
    then 
      try
	let c = Stream.next s in
	  ( match c with
		('\"' | ' ' | '\010' | '\013' | '\009' | '\026' | '\012') -> 
		  skip_n_non_sep_char n s
	      | _ -> 
		  ()
	  );
      with _ -> ()
    else
      try
	let c = Stream.next s in
	  ( match c with
		('\"' | ' ' | '\010' | '\013' | '\009' | '\026' | '\012') -> 
		  skip_n_non_sep_char n s
	      | _ -> 
		  skip_n_non_sep_char (n-1) s
	  );
      with _ -> ()
  in
  let _ = seek_in ic 0 in
  let new_tok = lexer (Stream.of_channel ic) in
  let first_n_toks = Stream.npeek n new_tok in
  let str = String.concat "" (List.map (string_of_genlex_token) first_n_toks) in
  let s = String.length str in
  let _ = seek_in ic 0 in
  let char_stream = Stream.of_channel ic in
  let char_pos =
    skip_n_non_sep_char s char_stream;
    (Stream.count char_stream) 
  in

    print_string ("\n*** Parse error (" ^ func ^ ") ");
    print_string ("around character " ^ (string_of_int char_pos) ^ ". ");
    print_string ("\n*** The next 10 tokens are: ");
    List.iter (print_genlex_token) tok_list ;
    print_string ("\n" ^ 
		  (if msg = "" 
		   then "" 
		   else ("*** whereas either one of the following token(s) was (were) expected:\n\t" ^ 
			 (add_quotes msg) ^ " \n")) ^
		  (if msg2 = "" 
		   then "" 
		   else ("*** " ^ msg2) 
		  )
		 );
    flush stdout
		 	
let print_debug ic msg =
140
  if debug_parsing then
141
    (
142
      print_string (string_of_int (pos_in ic) ^ ": " ^ msg);
143
      flush stdout
144
    )
145

146
147

(** Parsing lists *)
148
let rec
149
150
151
  (parse_list: in_channel -> (in_channel -> aut_token -> 'a) -> aut_token -> 'a list) = 
  fun ic parse tok -> 
    let _ = print_debug ic ("parse_list \n") in
152
153
154
155
156
157
158
159
160
161
162
163
    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
164
		  | [< vnt = parse ic; tail = (parse_list_var_tail ic (parse)) >]
165
166
167
		    -> vnt :: tail  
	      )
	)
168
169
170
171
172
173
174
      with 
	  Failure _ -> failwith "" 
	| e ->
	    print_err_msg ic tok tok_list "parse_list" ",\n\t; .\n\t; ,\n\t.\n\t)\n\t%" "";
	    failwith "" 
and (parse_list_var_tail: in_channel -> (in_channel -> aut_token -> 'a) -> aut_token -> 'a list) = 
  fun ic parse tok -> 
175
    let _ = print_debug ic ("parse_list_var_tail \n") in
176
177
178
179
180
181
182
183
184
185
186
187
    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
188
		    [< 'Genlex.Kwd ";" ;  tail = (parse_list_var_tail2 ic (parse)) >]
189
190
191
		    -> tail  
	      )
	)
192
193
194
195
196
197
198
199
200
      with Failure 
	  _ -> failwith "" 
	| e ->
	    print_err_msg ic tok tok_list "parse_list_var_tail" ",\n\t; .\n\t; ,\n\t.\n\t)\n\t%" "";
	    failwith ""

and (parse_list_var_tail2: in_channel -> (in_channel -> aut_token -> 'a) -> aut_token -> 'a list) = 
  fun ic parse tok -> 
    let _ = print_debug ic ("parse_list_var_tail2 \n") in
201
    (* This function is introduced to allow lists to be ended by a `;'... *)
202
203
    let tok_list = Stream.npeek 10 tok in
      try
204
205
	(
	  match tok with parser 
206
	    | [< 'Genlex.Kwd ";"; _ = (parse_list_var_tail3 ic (parse)) >] -> [] 
207
208
	    | [< 'Genlex.Kwd "," >] -> [] 
	    | [< 'Genlex.Kwd "." >] -> [] 
209
	    | [< a = parse ic ; tail = (parse_list_var_tail ic (parse)) >]
210
211
	      -> a :: tail  
	)
212
213
214
215
216
217
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_list_var_tail2" "" "";
	failwith ""
and (parse_list_var_tail3: in_channel -> (in_channel -> aut_token -> 'a) -> aut_token -> 'a list) = 
  fun ic parse tok -> 
    let _ = print_debug ic ("parse_list_var_tail3 \n") in
218
219
220
    (* This function is also introduced to allow lists to be ended by a `;'... *)
    let tok_list = Stream.npeek 10 tok in
      try
221
222
223
224
225
	(
	  match tok with parser 
	    | [< 'Genlex.Kwd "." >] -> [] 
	    | [< 'Genlex.Kwd "," >] -> []
	)
226
227
228
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_list_var_tail3" "" "";
	failwith ""
229

230

231
232
233
234
(** Parsing pragmas *)

type pragma = string * string

235
236
237
let rec (parse_pragma: in_channel -> aut_token -> pragma) =
  fun ic tok -> 
    let _ = print_debug ic ("parse_pragma \n") in
238
239
    let tok_list = Stream.npeek 10 tok in
      try
240
241
242
243
244
	(
	  match tok with parser  
	      [< 'Genlex.String label ; 'Genlex.Ident ":"; 
		 'Genlex.String pragma  >] -> (label, pragma)
	)
245
246
247
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_pragma"  "<string>" "";
	failwith ""
248
and
249
250
251
  (parse_pragma_list: in_channel -> aut_token -> pragma list) =
  fun ic tok -> 
    let _ = print_debug ic ("parse_pragma_list \n") in
252
253
254
255
256
    let tok_list = Stream.npeek 10 tok in
      try
	( match (Stream.npeek 1 tok) with 
	      [Genlex.Kwd "%"] -> 
		( match tok with parser  
257
		      [< 'Genlex.Kwd "%" ; 
258
			 pl = (parse_list ic (parse_pragma));
259
260
261
			 'Genlex.Kwd "%" 
		      >] 
		      -> pl
262
263
264
		)
	    | _ -> []
	)
265
266
267
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_pragma_list"  "" "";
	failwith ""
268

269
270
271
let rec (parse_automata: in_channel -> aut_token -> read_automata) = 
  fun ic tok -> 
    let _ = print_debug ic ("parse_automata \n") in
272
    let tok_list = Stream.npeek 20 tok in
273
      try
274
275
	(
	  match tok with parser  
276
277
278
279
280
281
282
283
284
285
286
287
288
289
	      [< 
		li = parse_list_inputs_opt ic;
		lo = parse_list_outputs_opt ic;
		ll = parse_list_locals_opt ic;
		lpre = parse_list_pre_opt ic;
		llabel_ce = parse_list_label_ce_opt ic ;
		fdl = parse_list_formula_def_opt ic (li @ lo @ ll @ lpre) ;
		'Genlex.Ident "start_node"; 'Genlex.Kwd "="; 'Genlex.Int node_id; 'Genlex.Kwd "," ;
		arcs_nb = parse_list_arcs_nb_opt ic;
		nodes_nb = parse_list_nodes_nb_opt ic;
		'Genlex.Ident "arcs"; 'Genlex.Kwd "="; la = parse_list_arc  ic (li @ lo @ ll @ lpre) ;
		'Genlex.Kwd ".";
	      >]
              -> Automata(node_id, li, lo, ll, lpre, llabel_ce, fdl, la)
290
	)
291
292
293
294
295
296
297
298
299
      with Failure 
	  _ -> failwith "" 
	| e ->
	    print_err_msg ic tok tok_list "parse_automata" 
	    ("inputs = <var list> ,\n\t" ^ 
	     "outputs = <var list> ,\n\t" ^
	     "locals = <var list> ,\n\t" ^
	     "pre = <pre var list> ,\n\t" ^
	     "ctrl_expr = <ctrl expr list> ,\n\t" ^
300
	     "formula = <formula def list> ,\n\t" ^
301
302
303
304
305
306
	     "start_node = <int> ,\n\t" ^
	     "arc_nb = <int> ,\n\t" ^
	     "node_nb = <int> ,\n\t" ^
	     "arcs = <arc list> .") "" ;
	    failwith ""
	      
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
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
352
353
354
355
356
357
358
359
360
and parse_list_inputs_opt ic tok =
  match tok with parser  
      [<'Genlex.Ident "inputs"; 'Genlex.Kwd "="; l = parse_list_var ic ;'Genlex.Kwd "," 
      >] -> l
    | [< >]  -> []

and parse_list_outputs_opt ic tok =
  match tok with parser  
      [<'Genlex.Ident "outputs"; 'Genlex.Kwd "="; l = parse_list_genvar ic ;'Genlex.Kwd "," 
      >] -> l
    | [< >]  -> []

and parse_list_locals_opt ic tok =
  match tok with parser  
      [<'Genlex.Ident "locals"; 'Genlex.Kwd "="; l = parse_list_genvar ic ;'Genlex.Kwd "," 
      >] -> l
    | [< >]  -> []

and parse_list_pre_opt ic tok =
  match tok with parser  
      [<'Genlex.Ident "pre"; 'Genlex.Kwd "="; l = parse_list_prevar ic ;'Genlex.Kwd "," 
      >] -> l
    | [< >]  -> []


and parse_list_arcs_nb_opt ic tok =
  match tok with parser  
      [< 'Genlex.Ident "arcs_nb"; 'Genlex.Kwd "="; 'Genlex.Int arcs_nb  ; 'Genlex.Kwd "," 
      >] -> arcs_nb
    | [< >]  -> 0

and parse_list_nodes_nb_opt ic tok =
  match tok with parser  
      [< 'Genlex.Ident "nodes_nb"; 'Genlex.Kwd "="; 'Genlex.Int nodes_nb  ; 'Genlex.Kwd "," 
      >] -> nodes_nb
    | [< >]  -> 0


and parse_list_label_ce_opt ic tok =
  match tok with parser  
      [< 'Genlex.Ident "ctrl_expr"; 'Genlex.Kwd "="; 
	 llabel_ce = parse_list_label_ce ic ;'Genlex.Kwd "," 
      >] -> llabel_ce
    | [< >]  -> []
	

and parse_list_formula_def_opt ic vars tok =
  match tok with parser  
      [< 'Genlex.Ident "formula"; 'Genlex.Kwd "="; 
	 fdl = parse_list_formula_def ic vars ; 'Genlex.Kwd ","
      >] -> fdl
    | [< >]  -> []


361
362
363
364

and (parse_list_var: in_channel -> aut_token -> vnt list) = 
  fun ic tok -> 
    let _ = print_debug ic ("parse_list_var \n") in
365
366
    let tok_list = Stream.npeek 10 tok in
      try
367
368
369
370
371
372
	parse_list ic (parse_var) tok
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_list_var"  "" "" ;
	failwith ""
and (parse_var: in_channel -> aut_token -> vnt) = 
  fun ic tok -> 
373
374
    let tok_list = Stream.npeek 10 tok in
      try
375
376
377
378
	(
	  match tok with parser  
	      [< 'Genlex.Kwd "("; 
		 'Genlex.Ident var; 
379
		 prag_var = parse_pragma_list ic; 
380
381
382
383
384
385
		 'Genlex.Kwd ",";  
		 'Genlex.Ident typ ; 
		 'Genlex.Kwd ")" >]
	      -> 
		( match typ with
		      "bool" -> (var, BoolT)
386
		    | "float" -> (var, FloatT(-.default_max_float, default_max_float))
387
		    | "int" -> (var, IntT(default_min_int / 2, default_max_int / 2))
388
			(* We divide by 2 so that domains are always smaller 
389
			   than max_int *)
390
391
392
		    | str -> 
			print_err_msg ic tok tok_list "parse_var" "" (str ^ " is not a valid type" );
			failwith ""
393
394
		)
	)
395
396
397
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_var"  "( <ident> , <type> )" "";
	failwith ""
398

399
400
and (parse_list_genvar: in_channel -> aut_token -> vnt list) = 
  fun ic tok -> 
401
402
    let tok_list = Stream.npeek 10 tok in
      try
403
404
405
406
407
408
	parse_list ic (parse_genvar) tok
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_list_genvar"  "" "";
	failwith ""
and (parse_genvar: in_channel -> aut_token -> vnt) = 
  fun ic tok -> 
409
410
    let tok_list = Stream.npeek 10 tok in
      try
411
412
	(
	  match tok with parser  
413
	      [< 'Genlex.Kwd "("; 'Genlex.Ident var; pl = parse_pragma_list ic;
414
		 'Genlex.Kwd ","; 'Genlex.Ident typ ;
415
		 vnt = parse_type ic var typ >]
416
417
	      -> vnt
	)
418
419
420
421
422
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_genvar"  "( or ," "";
	failwith ""
and (parse_type: in_channel ->  string -> string -> aut_token -> vnt) =
  fun ic var typ tok -> 
423
424
    let tok_list = Stream.npeek 10 tok in
      try
425
426
427
428
429
	(
	  match tok with parser  
	      [< 'Genlex.Kwd ")" >] -> 
		( match typ with
		      "bool" -> (var, BoolT)
430
		    | "float" -> (var, FloatT(-.default_max_float, default_max_float))
431
		    | "int" -> (var, IntT(min_int / 2, max_int / 2))
432
433
434
		    | str -> 
			print_err_msg ic tok tok_list "parse_type" "" (str ^ " is not a valid type");
			failwith ""
435
		)
436
	    | [< 'Genlex.Kwd ","; vnt = parse_type_more ic var typ >] -> vnt
437
	)
438
439
440
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_type"  "<bool> \n\t<float> \n\t<int>" "";
	failwith ""
441
	    
442
443
and (parse_type_more: in_channel ->  string -> string -> aut_token -> vnt) =
  fun ic var typ tok -> 
444
445
    let tok_list = Stream.npeek 10 tok in
      try
446
447
448
449
	(
	  match tok with parser  
	      [< 'Genlex.Int min; 'Genlex.Kwd ","; 'Genlex.Int max;  'Genlex.Kwd ")" >] -> 
		( match typ with
450
451
452
453
454
455
		      "bool" -> 
			print_err_msg ic tok tok_list "parse_type_more" "" ("*** int expected" );
			failwith ""
		    | "float" -> 
			print_err_msg ic tok tok_list "parse_type_more" "" ("*** int expected " );
			failwith ""
456
		    | "int" -> (var, IntT(min, max))
457
458
459
		    | str -> 
			print_err_msg ic tok tok_list "parse_type_more" "" (str ^ " is not a valid type");
			failwith ""
460
461
462
		)
	    | [< 'Genlex.Float min; 'Genlex.Kwd ","; 'Genlex.Float max;  'Genlex.Kwd ")" >] -> 
		( match typ with
463
464
465
		      "bool" -> 
			print_err_msg ic tok tok_list "parse_type_more" "" ("*** float expected in .luc " );
			failwith ""
466
		    | "float" -> (var, FloatT(min, max))
467
468
469
470
471
472
		    | "int" -> 
			print_err_msg ic tok tok_list "parse_type_more" "" ("*** float expected in .luc " );
			failwith ""
		    | str -> 
			print_err_msg ic tok tok_list "parse_type_more" "" (str ^ " is not a valid type" );
			failwith ""
473
474
		)
	)
475
476
477
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_type_more"  "<bool> \n\t<float> \n\t<int>" "";
	failwith ""
478
479
	    

480
481
and (parse_list_prevar: in_channel -> aut_token -> vnt list) = 
  fun ic tok -> 
482
483
    let tok_list = Stream.npeek 10 tok in
      try
484
485
486
487
488
489
490
	parse_list ic (parse_prevar) tok
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_list_prevar"  "" "";
	failwith ""
and (parse_prevar: in_channel -> aut_token -> vnt) = 
  fun ic tok -> 
    let _ = print_debug ic ("parse_prevar \n") in
491
    let tok_list = Stream.npeek 10 tok in
492
      try (
493
	match tok with parser  
494
495
	    [< 'Genlex.Kwd "("; 'Genlex.Ident "pre"; 'Genlex.Kwd "("; 
	       'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident var;  
496
	       'Genlex.Kwd ")"; pl = parse_pragma_list ic ; 
497
	       'Genlex.Kwd ","; 'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
498
	    -> 
499
	      let pre_var = Prevar.create_prevar_name i var in
500
	      ( match typ with
501
		  "bool" -> (pre_var, BoolT)
502
		| "float" -> (pre_var, FloatT(-.default_max_float, default_max_float))
503
		| "int" -> (pre_var, IntT(min_int / 2, max_int / 2))
504
505
506
		| str -> 
		    print_err_msg ic tok tok_list "" "" (str ^ " is not a valid type" );
		    failwith ""
507
	      )
508
      )
509
510
511
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_prevar"  "" "";
	failwith ""
512

513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544


and (parse_list_formula_def: in_channel -> vnt list -> aut_token 
       -> (string * formula) list) =
  fun ic vars tok -> 
    let _ = print_debug ic ("parse_list_formula_def \n") in
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list ic (fun ic -> parse_formula_def ic vars) tok
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_list_formula_def"  "" "";
	failwith ""
and (parse_formula_def: in_channel -> vnt list -> aut_token -> string * formula) = 
  fun ic vars tok -> 
    let _ = print_debug ic ("parse_formula_def \n") in
    let tok_list = Stream.npeek 10 tok in
      try (
	match tok with parser  
	    [< 'Genlex.Kwd "(" ; 
	       'Genlex.Ident label ;	 
	       'Genlex.Kwd "," ; 
	       f = parse_formula ic vars ; 
	       'Genlex.Kwd ")" 
	    >]
	    -> 
	      (label, f)
      )
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_formula_def"  "" "";
	failwith ""


545
546
547
and (parse_list_label_ce: in_channel -> aut_token -> label_ce list) =
  fun ic tok -> 
    let _ = print_debug ic ("parse_list_label_ce \n") in
548
549
    let tok_list = Stream.npeek 10 tok in
      try
550
551
552
553
554
555
556
	parse_list ic (parse_ce) tok
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_list_label_ce"  "" "";
	failwith ""
and (parse_ce: in_channel -> aut_token -> label_ce) = 
  fun ic tok -> 
    let _ = print_debug ic ("parse_ce \n") in
557
    let tok_list = Stream.npeek 10 tok in
558
      try (
559
560
561
562
	match tok with parser  
	    [< 'Genlex.Kwd "(" ; 
	       'Genlex.Ident label ;	 
	       'Genlex.Kwd "," ; 
563
	       expr = parse_list_ctrl_expr ic  ; 
564
565
566
567
	       'Genlex.Kwd ")" 
	    >]
	    -> 
	      (label, expr)
568
      )
569
570
571
572
573
574
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_ce"  "" "";
	failwith ""
and (parse_list_ctrl_expr : in_channel -> aut_token -> Control.expr) =
  fun ic tok -> 
    let _ = print_debug ic ("parse_list_ctrl_expr  \n") in
575
576
577
    let tok_list = Stream.npeek 10 tok in
    let ce_list =
      try
578
579
580
581
	parse_list ic (parse_ctrl_expr) tok
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_list_ctrl_expr"  "" "";
	failwith ""
582
    in
583
584
585
586
587
588
      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)
589
590
591
and (parse_ctrl_expr: in_channel -> aut_token -> Control.expr) = 
  fun ic tok -> 
    let _ = print_debug ic ("parse_ctrl_expr \n") in
592
    let tok_list = Stream.npeek 10 tok in
593
      try (
594
595
596
597
	match tok with parser  
	    [< 'Genlex.Ident "Set" ; 'Genlex.Ident varname ; 'Genlex.Int i 
	    >] ->
	      (Control.set varname i)
598
599
600
601
	  | [< 'Genlex.Ident "Set_between" ; 'Genlex.Ident varname ;
	       'Genlex.Int i ; 'Genlex.Int min ; 'Genlex.Int max 
	    >] -> 
	      (Control.set_between varname i min max)
602
603
604
605
	  | [< 'Genlex.Ident "Draw_between" ; 'Genlex.Ident varname ;
	       'Genlex.Int min ; 'Genlex.Int max 
	    >] -> 
	      (Control.draw_between varname min max)
606
	  | [< 'Genlex.Ident "Draw_gauss" ; 'Genlex.Ident varname ; 
607
	       m = parse_float ic  ; dev = parse_float ic  
608
609
610
611
612
	    >] -> 
	      (Control.draw_gauss varname m dev)
	  | [< 'Genlex.Ident "Dec" ; 'Genlex.Ident varname 
	    >] -> 
	      (Control.dec varname)
613
	  | [< 'Genlex.Kwd "IfThenElse" ; test = parse_test_expr ic  ; 
614
	       'Genlex.Kwd "(" ;  
615
	       cel_then = parse_list_ctrl_expr ic  ; 
616
617
	       'Genlex.Kwd ")" ;  
	       'Genlex.Kwd "(" ;  
618
	       cel_else = parse_list_ctrl_expr ic  ; 
619
620
621
	       'Genlex.Kwd ")" 
	    >] ->  
	      Control.ite test cel_then cel_else
622
      )
623
      with Failure _ -> failwith "" | e ->
624
625
	print_err_msg ic tok tok_list "parse_ctrl_expr"  
	"Set\n\tSet_between\n\tDraw_gauss\n\tDec\n\tIfThenElse ( <ctrl expr> ) ( <ctrl expr> )" "";
626
	failwith ""
627

628
629
630
and (parse_float: in_channel -> aut_token -> float) =
  fun ic tok -> 
    let _ = print_debug ic ("parse_float \n") in
631
    let tok_list = Stream.npeek 10 tok in
632
      try (
633
634
635
	match tok with parser  
	    [< 'Genlex.Float f >] -> f
	  | [< 'Genlex.Int i >] -> (float_of_int i)
636
      )
637
638
639
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_float"  "<int> or <float>" "";
	failwith ""
640
641


642
643
644
and (parse_int_or_var: in_channel -> aut_token -> Control.number) =
  fun ic tok -> 
    let _ = print_debug ic ("parse_int_or_var \n") in
645
    let tok_list = Stream.npeek 10 tok in
646
      try (
647
648
649
	match tok with parser  
	    [< 'Genlex.Int i >] -> Control.IntExpr(i)
	  | [< 'Genlex.Ident id >] -> Control.VarExpr(id)
650
      )
651
652
653
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_int_or_var"  "<int> or <ident>" "";
	failwith ""
654
	    
655
656
657
and (parse_test_expr: in_channel -> aut_token -> Control.test) =
  fun ic tok -> 
    let _ = print_debug ic ("parse_test_expr \n") in
658
    let tok_list = Stream.npeek 10 tok in
659
      try (
660
	match tok with parser
661
	    [< 'Genlex.Kwd "(" ; ct = parse_test_expr ic  ; 'Genlex.Kwd ")" >]
662
663
664
	    ->
	      ct
	  |
665
	    [< 'Genlex.Kwd op ; n1 = parse_int_or_var ic ; n2 = parse_int_or_var ic>]
666
667
668
669
670
671
672
	    -> 
	      match op with
		| "<"  -> Control.GtExpr(n2, n1)
		| "<=" -> Control.GeExpr(n2, n1)
		| ">"  -> Control.GtExpr(n1, n2)
		| ">=" -> Control.GeExpr(n1, n2)
		| "="  -> Control.EqExpr(n1, n2)
673
		| "=="  -> Control.EqExpr(n1, n2)
674
		| _ -> assert false
675
      )
676
677
678
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_test_expr"  ">\n\t<\n\t<=\n\t>=\n\t=\n\t==" "";
	failwith ""
679
680
	    

681
682
683
and (parse_list_arc: in_channel -> vnt list -> aut_token -> read_arc list) = 
  fun ic vars tok -> 
    let _ = print_debug ic ("parse_list_arc \n") in
684
685
    let tok_list = Stream.npeek 10 tok in
      try
686
687
688
689
690
691
692
	parse_list ic (fun ic -> parse_arc ic vars) tok
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_list_arc"  "" "";
	failwith ""
and (parse_arc: in_channel -> vnt list -> aut_token -> read_arc) = 
  fun ic vars tok -> 
    let _ = print_debug ic ("parse_arc \n") in
693
    let tok_list = Stream.npeek 10 tok in
694
      try (
695
	match tok with parser  
696
697
698
699
700
	    [< 'Genlex.Ident "From"; 
	       'Genlex.Int node_from ; 
	       'Genlex.Ident "To"; 
	       'Genlex.Int node_to ; 
	       'Genlex.Ident "With"; 
701
	       arc_info = parse_arc_info ic vars
702
	    >]
703
	    -> Arc(node_from, arc_info, node_to)
704
      ) 
705
706
707
708
709
710
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_arc" "From <int> To <int> With <arc_label>"  "";
	failwith ""
and (parse_arc_info: in_channel -> vnt list -> aut_token -> arc_info) = 
  fun ic vars tok -> 
    let _ = print_debug ic ("parse_arc_info \n") in
711
    let tok_list = Stream.npeek 10 tok in
712
      try (
713
	match tok with parser  
714
	    [< weight = (parse_weight ic vars) ; 
715
	       'Genlex.Ident ":"; 
716
717
	       expr = parse_formula_eps ic vars ; 
	       pc = parse_post_cond_id ic
718
	    >] 
719
	    -> (weight, expr, pc)
720
      ) 
721
722
723
724
725
726
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_arc_info" "<weigth> :" "";
	failwith ""
and (parse_post_cond_id: in_channel -> aut_token -> string) =
  fun ic tok -> 
    let _ = print_debug ic ("parse_post_cond_id \n") in
727
     let tok_list = Stream.npeek 10 tok in
728
      try (
729
730
731
732
733
734
	match (Stream.npeek 2 tok) with
	    [ Genlex.Ident ":"; Genlex.Ident label ] -> 
	      Stream.junk tok;
	      Stream.junk tok;
	      label
	  | _ -> "identity"
735
      )
736
737
738
739
740
741
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_post_cond_id"  "" "";
	failwith ""
and (parse_weight: in_channel -> vnt list -> aut_token -> weight) = 
  fun ic vars tok -> 
    let _ = print_debug ic ("parse_weight \n") in
742
    let tok_list = Stream.npeek 10 tok in
743
      try (
744
	match tok with parser  
745
746
747
748
749
	    [< 'Genlex.Int w >] -> Wint(w)
	  | [< 'Genlex.Kwd "!" ; 
	       'Genlex.Ident lbl >] 
	    -> Wident_not_sig(lbl)
	  | [< 'Genlex.Ident lbl >] -> Wident(lbl)
750
      )
751
752
753
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_weight"  "[!] <weigth_ident> or <int>" "";
	failwith ""
754
755


756
757
and (parse_formula_eps: in_channel -> vnt list -> aut_token -> formula_eps) = 
  fun ic vars tok -> 
758
    let tok_list = Stream.npeek 10 tok in
759
      try (
760
	match tok with parser   
761
762
763
	  | 
	    [< 'Genlex.Ident "eps" >] -> Eps
	  | 
764
	    [< 'Genlex.Ident "("; fe = parse_formula_eps ic vars ; 
765
766
767
768
	       'Genlex.Ident ")" 
	    >] 
	    -> fe
	  | 
769
	    [< f = parse_formula ic vars >] -> Form(f)
770
      )
771
772
773
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_formula_eps"  "eps or (" "";
	failwith ""
774
	    
775
776
and (parse_formula: in_channel -> vnt list -> aut_token -> formula) = 
  fun ic vars tok -> 
777
778
    let tok_list = Stream.npeek 10 tok in
      try
779
	(
780
	match tok with parser  
781
782
	    [< 'Genlex.Kwd "!"; pl = parse_pragma_list ic  ;
	       f = parse_formula ic vars
783
	    >] -> Not(f)
784
	  | 
785
786
787
788
	    [< 'Genlex.Kwd "IfThenElse";  pl = parse_pragma_list ic  ;
	       f1 = parse_formula ic vars; 
	       f2 = parse_formula ic vars; 
	       f3 = parse_formula ic vars           
789
790
791
	    >] 
	    -> IteB(f1, f2, f3)
	  | 
792
793
794
	    [< 'Genlex.Kwd "==";  pl = parse_pragma_list ic  ;
	       f1 = parse_formula ic vars; 
	       f2 = parse_formula ic vars
795
	    >] 
796
797
798
	    -> 
	      EqB(f1, f2) 
(* 	      Or(And(f1, f2), And(Not(f1), Not(f2)))  *)
799
	  | 
800
	    [< 'Genlex.Kwd "true" ; pl = parse_pragma_list ic 
801
	    >] 
802
	    -> True
803
	  | 
804
	    [< 'Genlex.Kwd "false" ; pl = parse_pragma_list ic 
805
	    >] 
806
	    -> False
807
	  | 
808
	    [< 'Genlex.Kwd "("; f = parse_formula ic vars ; 'Genlex.Kwd ")"
809
810
811
	    >]
	    -> f 
	  |  
812
813
814
	    [< 'Genlex.Kwd "||"; pl = parse_pragma_list ic  ;
	       f1 = parse_formula ic vars ;
	       f2 = parse_formula ic vars 
815
	    >] 
816
	    -> Or(f1, f2)
817
	  | 
818
819
820
	    [< 'Genlex.Kwd "&&"; pl = parse_pragma_list ic  ;
	       f1 = parse_formula ic vars ; 
	       f2 = parse_formula ic vars 
821
	    >] 
822
823
	    -> 
	      And(f1, f2)
824
	  | 
825
826
827
	    [< 'Genlex.Kwd "#"; pl = parse_pragma_list ic  ; 
	       f1 = parse_formula ic vars ;
	       f2 = parse_formula ic vars 
828
	    >] 
829
	    -> And(Or(f1, f2), Not(And(f1, f2))) (* xor *)
830

831
	  | 
832
833
	    [< 'Genlex.Kwd "=";  pl = parse_pragma_list ic  ; 
	       e1 = parse_expr ic vars ; e2 = parse_expr ic vars 
834
835
	    >] 
	    -> Eq(e1, e2) 
836
	  | 
837
838
	    [< 'Genlex.Kwd "<>";  pl = parse_pragma_list ic  ; 
	       e1 = parse_expr ic vars ; e2 = parse_expr ic vars 
839
	    >] 
840
	    -> Not(Eq(e1, e2))
841
	  | 
842
843
	    [< 'Genlex.Kwd ">";  pl = parse_pragma_list ic  ; 
	       e1 = parse_expr ic vars ;e2 = parse_expr ic vars 
844
845
846
	    >] 
	    -> Sup(e1, e2) 
	  | 
847
848
	    [< 'Genlex.Kwd ">="; pl = parse_pragma_list ic  ; 
	       e1 = parse_expr ic vars ;e2 = parse_expr ic vars 
849
850
851
	    >] 
	    -> SupEq(e1, e2)
	  | 
852
853
	    [< 'Genlex.Kwd "<";  pl = parse_pragma_list ic  ; 
	       e1 = parse_expr ic vars ; e2 = parse_expr ic vars 
854
855
856
	    >] 
	    -> Inf(e1, e2) 
	  | 
857
858
	    [< 'Genlex.Kwd "<="; pl = parse_pragma_list ic  ; 
	       e1 = parse_expr ic vars ;e2 = parse_expr ic vars 
859
860
861
862
863
	    >] 
	    -> InfEq(e1, e2)
	  | 
	    [< 'Genlex.Ident "pre"; 'Genlex.Kwd "("; 'Genlex.Int i ; 
	       'Genlex.Kwd "," ; 'Genlex.Ident id; 'Genlex.Kwd ")"; 
864
	       pl = parse_pragma_list ic 
865
866
	    >]
	    ->
867
	      let pre_id = Prevar.create_prevar_name  i id in
868
869
870
871
872
	      (* Ditto *)
	      let (_, vt) = List.find (fun (vn,vt) -> vn = pre_id) vars in
		( match vt with
		    BoolT -> Bvar(pre_id)
		  | _  -> 
873
874
875
876
		      print_err_msg ic tok tok_list "parse_formula" "" 
		      (pre_id ^ " is declared as a" ^
		       " boolean and is used as a numeric. ");
		      failwith ""
877
878
		)
	  | 
879
	    [< 'Genlex.Ident id ; pl = parse_pragma_list ic  >] 
880
881
882
883
884
885
	    -> 
	      (* 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)
		  | _  -> 
886
887
888
889
		      print_err_msg  ic tok tok_list "parse_formula" "" 
		       (id ^ " is declared as a" ^
				" boolean and is used as a numeric.\n ");
		      failwith ""
890
891
		)
	)
892
893
894
895
896
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_formula"  
	("!\n\tIfThenElse\n\t==\n\ttrue\n\tfalse\n\t(\n\t||\n\t&&\n\t#\n\t=\n\t<>\n\t<\n\t>\n\t" ^
	 "<=\n\t>=\n\tpre") "";
	failwith ""
897
	    
898

899

900
(* 
901
902
903
 ** The following is copy-paste-adapted from sec 1.8 of the ocaml ref man 
 ** untitled ``pretty printing and parsing''.
 *)
904
905
906
and (parse_expr: in_channel -> vnt list -> aut_token -> expr) = 
  fun ic vars tok -> 
    let _ = print_debug ic ("parse_expr ic \n") in
907
    let tok_list = Stream.npeek 10 tok in
908
      try (
909
	match tok with parser  
910
	    [< e1 = parse_mult ic vars; e = parse_more_adds ic e1 vars >] -> e
911
      )
912
913
914
915
916
917
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_expr"  "" "";
	failwith ""
and (parse_more_adds: in_channel -> expr -> vnt list -> aut_token -> expr) = 
  fun ic e1 vars tok -> 
    let _ = print_debug ic ("parse_more_adds \n") in
918
    let tok_list = Stream.npeek 10 tok in
919
      try (
920
921
	match tok with parser  
	    [< 'Genlex.Kwd "+"; 
922
923
924
	       pl = parse_pragma_list ic  ;
	       e2 = parse_mult ic vars; 
	       e = parse_more_adds ic (Sum(e1, e2)) vars 
925
926
927
	    >] 
	    -> e
	  | [< 'Genlex.Kwd "-"; 
928
929
930
	       pl = parse_pragma_list ic  ;
	       e2 = parse_mult ic vars; 
	       e = parse_more_adds ic (Diff(e1, e2)) vars 
931
932
933
934
	    >] 
	    -> e
	  | [< >] 
	    -> e1
935
      )
936
937
938
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_more_adds"  "+ or -" "";
	failwith ""
939

940
941
942
and (parse_mult: in_channel -> vnt list -> aut_token -> expr) = 
  fun ic vars tok -> 
    let _ = print_debug ic ("parse_mult \n") in
943
    let tok_list = Stream.npeek 10 tok in
944
      try (
945
	match tok with parser  
946
	    [< e1 = parse_simple ic vars; e = parse_more_mults ic e1 vars >] -> e
947
      )
948
949
950
951
952
953
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_more_adds"  "" "";
	failwith ""
and (parse_more_mults: in_channel -> expr -> vnt list -> aut_token -> expr) = 
  fun ic e1 vars tok -> 
    let _ = print_debug ic ("parse_more_mults \n") in
954
    let tok_list = Stream.npeek 10 tok in
955
      try (
956
957
	match tok with parser  
	    [< 'Genlex.Kwd "*"; 
958
959
960
	       pl = parse_pragma_list ic  ;  
	       e2 = parse_simple ic vars; 
	       e = parse_more_mults ic (Prod(e1, e2)) vars 
961
962
963
	    >] 
	    -> e
	  | [< 'Genlex.Kwd "/"; 
964
965
966
	       pl = parse_pragma_list ic  ;  
	       e2 = parse_simple ic vars; 
	       e = parse_more_mults ic (Quot(e1, e2)) vars 
967
968
969
	    >] 
	    -> e
	  | [< 'Genlex.Ident "mod"; 
970
971
972
	       pl = parse_pragma_list ic  ; 
	       e2 = parse_simple ic vars; 
	       e = parse_more_mults ic (Mod(e1, e2)) vars 
973
974
975
976
	    >] 
	    -> e
	  | [<  >] 
	    -> e1
977
      )
978
979
980
981
982
983
      with Failure _ -> failwith "" | e ->
	print_err_msg ic tok tok_list "parse_more_mults"  "*\n\t/\n\t mod" "";
	failwith ""
and (parse_simple: in_channel -> vnt list -> aut_token -> expr) = 
  fun ic vars tok -> 
    let _ = print_debug ic ("parse_simple \n") in
984
    let tok_list = Stream.npeek 10 tok in
985
      try (
986
987
988
989
	match tok with parser  
	    
	  | [< 'Genlex.Ident "pre"; 'Genlex.Kwd "(";  
	       'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident id;   
990
	       'Genlex.Kwd ")"; pl = parse_pragma_list ic   >] -> 
991
	      let s = Prevar.create_prevar_name i id in 
992
993
994
995
996
997
998
999
1000
	      let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in 
	      let var = 
		match vt with 
		    BoolT -> assert false  
		  |<