parse_env.ml 15.7 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
29
30
31
let lexer = Genlex.make_lexer ["("; ")"; ","; ";"; ".";
			       "&&"; "||"; "!"; "true"; "false"; 
			       "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
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
88
89
90
91
	  | [< 'Genlex.Kwd ";" ; a = parse ;
	       tail = (parse_list_var_tail (parse)) >]
	    -> a :: tail  
	with e ->
	  print_err_msg tok_list "parse_list_var_tail";
	  raise e
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
(** 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
123

124
125
let rec (parse_automata: aut_token -> read_automata) = 
  fun tok -> 
126
    let tok_list = Stream.npeek 20 tok in
127
128
      try
	match tok with parser  
129
130
131
	    [< '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 ;
132
	       'Genlex.Ident "pre"; 'Genlex.Kwd "="; lpre = parse_list_prevar ;
133
	       'Genlex.Ident "start_node"; 'Genlex.Kwd "="; 'Genlex.Int node_id ; 
134
	       'Genlex.Kwd "," ;
135
136
	       'Genlex.Ident "arcs"; 'Genlex.Kwd "="; la = parse_list_arc 
		      (List.append li (List.append lo (List.append ll lpre))) 
137
138
	    >]
            -> Automata(node_id, li, lo, ll, lpre, la)
139
140
141
142
	with e ->
	  print_err_msg tok_list "parse_automata";
	  raise e
	    
143

144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
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)
163
164
165
166
		| "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 *)
167
168
169
170
171
172
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	with e ->
	  print_err_msg tok_list "parse_var" ;
	  raise e

173
174
175
176
177
178
179
180
181
182
183
184
185
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  
186
187
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; pl = parse_pragma_list ;
	       'Genlex.Kwd ","; 'Genlex.Ident typ ;
188
189
190
191
192
193
194
195
196
197
198
199
200
	       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)
201
202
		  | "float" -> (var, FloatT(-.max_float /. 2., max_float /. 2.))
		  | "int" -> (var, IntT(min_int / 2, max_int / 2))
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
		  | 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
	    

234
and (parse_list_prevar: aut_token -> vnt list) = 
235
  fun tok -> 
236
237
    let tok_list = Stream.npeek 10 tok in
      try
238
	parse_list (parse_prevar) tok
239
      with e ->
240
	print_err_msg tok_list "parse_list_prevar" ;
241
	raise e
242
and (parse_prevar: aut_token -> vnt) = 
243
  fun tok -> 
244
245
246
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
247
248
249
250
	    [< '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 ")" >]
251
	    -> 
252
	      let pre_var = ("_pre" ^ (string_of_int i) ^ var) in
253
	      ( match typ with
254
		  "bool" -> (pre_var, BoolT)
255
256
		| "float" -> (pre_var, FloatT(-.max_float /. 2., max_float /. 2.))
		| "int" -> (pre_var, IntT(min_int / 2, max_int / 2))
257
258
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
259
	with e ->
260
	  print_err_msg tok_list "parse_prevar" ;
261
	  raise e
262

263
264
and (parse_list_arc: vnt list -> aut_token -> read_arc list) = 
  fun vars tok -> 
265
266
    let tok_list = Stream.npeek 10 tok in
      try
267
	parse_list (parse_arc vars) tok
268
269
270
      with e ->
	print_err_msg tok_list "parse_list_arc" ;
	raise e
271
272
and (parse_arc: vnt list -> aut_token -> read_arc) = 
  fun vars tok -> 
273
274
275
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
276
277
278
	    [< 'Genlex.Ident "From"; 'Genlex.Int node_from ; 
	       'Genlex.Ident "To"; 'Genlex.Int node_to ; 
	       'Genlex.Ident "With"; arc_info = parse_arc_info vars  >]
279
280
281
282
	    -> Arc(node_from, arc_info, node_to)
	with e ->
	  print_err_msg tok_list "parse_arc" ;
	  raise e
283
284
and (parse_arc_info: vnt list -> aut_token -> arc_info) = 
  fun vars tok -> 
285
286
287
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
288
	    [< 'Genlex.Int weigth ; 'Genlex.Ident ":"; expr = parse_formula_eps vars >] 
289
290
291
292
	    -> (weigth, expr)
	with e ->
	  print_err_msg tok_list "parse_arc_info" ;
	  raise e
293

294
295
and (parse_formula_eps: vnt list -> aut_token -> formula_eps) = 
  fun vars tok -> 
296
297
298
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser   
299
300
	  | [< 'Genlex.Ident "eps" >] -> Eps
	  | [< 'Genlex.Ident "("; 'Genlex.Ident "eps"; 'Genlex.Ident ")" >] -> Eps
301
	  | [< f = parse_formula vars >] -> Form(f)
302
303
304
305
	with e ->
	  print_err_msg tok_list "parse_formula_eps" ;
	  raise e
	    
306
307
and (parse_formula: vnt list -> aut_token -> formula) = 
  fun vars tok -> 
308
309
310
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
	    [< '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
326
327
328
329
330
331
332
333

	  | [< '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 ; 
334
335
	       f1 = parse_expr_or_bool_ident id vars; 
	       f = parse_more_formula f1 vars    >] -> f
336
337
	  | [< e1 = parse_expr vars ; f = parse_expr_right e1 vars 
	                                         >] -> f
338
339
340
	with e ->
	  print_err_msg tok_list "parse_formula" ;
	  raise e
341

342
343
and (parse_expr_or_bool_ident: string -> vnt list -> aut_token -> formula) = 
  fun id vars tok -> 
344
    let tok_list = Stream.npeek 10 tok in
345
    let (_, vt) = List.find (fun (vn,vt) -> vn = id) vars in
346
    let some_var =
347
      match vt with
348
349
350
	  BoolT -> None
	| IntT(_,_) -> Some(Ivar(id))
	| FloatT(_,_) -> Some(Fvar(id))
351
    in
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
      ( 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
	      )
      )
374

375
376
and (parse_more_formula: formula -> vnt list -> aut_token -> formula) = 
  fun f1 vars tok -> 
377
378
379
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
380
381
382
383
	    [< 'Genlex.Kwd "||"; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> Or(f1, f2)
	  | [< 'Genlex.Kwd "&&"; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> And(f1, f2) 
384
385
	  | [< 'Genlex.Kwd "="; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> Or(And(f1, f2), And(Not(f1), Not(f2))) 
386
387
388
389
	  | [< >] -> f1
	with e ->
	  print_err_msg tok_list "parse_more_formula" ;
	  raise e
390
391
and (parse_expr_right : expr -> vnt list -> aut_token -> formula) = 
  fun e1 vars tok -> 
392
393
394
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser
395
396
397
398
399
	    [< '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)
400
401
402
403
	with e ->
	  print_err_msg tok_list "parse_expr_rigth" ;
	  raise e
	    
404
405

(* 
406
407
408
 ** The following is copy-paste-adapted from sec 1.8 of the ocaml ref man 
 ** untitled ``pretty printing and parsing''.
 *)
409
410
and (parse_expr: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
411
    match tok with parser  
412
413
414
	[< 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 -> 
415
    match tok with parser  
416
417
	[< 'Genlex.Kwd "+"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
418
	   e = parse_more_adds (Sum(e1, e2)) vars >] -> e
419
420
      | [< 'Genlex.Kwd "-"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
421
	   e = parse_more_adds (Diff(e1, e2)) vars >] -> e
422
      | [<  >] -> e1
423
424
and (parse_mult: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
425
    match tok with parser  
426
427
428
	[< 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 -> 
429
    match tok with parser  
430
431
	[< 'Genlex.Kwd "*"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
432
	   e = parse_more_mults (Prod(e1, e2)) vars >] -> e
433
434
      | [< 'Genlex.Kwd "/"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
435
	   e = parse_more_mults (Quot(e1, e2)) vars >] -> e
436
437
      | [< 'Genlex.Kwd "mod"; pl = parse_pragma_list ; 
	   e2 = parse_simple vars; 
438
	   e = parse_more_mults (Mod(e1, e2)) vars >] -> e
439
      | [<  >] -> e1
440
441
and (parse_simple: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
442
    match tok with parser  
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
      
      | [< '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 >] -> 
458
459
460
	  let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in
	  let var =
	    match vt with
461
		BoolT -> assert false 
462
463
464
465
	      | IntT(_,_) -> Ivar(s)
	      | FloatT(_,_) -> Fvar(s)
	  in
	    var
466
467
  
      | [< 'Genlex.Int i;   pl = parse_pragma_list >] -> Ival(i)
468
469
470
471
      | [< 'Genlex.Float f; pl = parse_pragma_list >] -> Fval(f)
      | [< 'Genlex.Kwd "IfThenElseExpr";  pl = parse_pragma_list ; 
	   f1 = parse_formula vars; 
	   e2 = parse_expr vars; 
472
473
	   e3 = parse_expr vars >] -> Ite(f1, e2, e3) 
      | [< 'Genlex.Kwd "("; e = parse_expr vars; 'Genlex.Kwd ")" >] -> e
474