parse_env.ml 13.6 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
132
133
	    [< '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 ;
	       'Genlex.Ident "pre"; 'Genlex.Kwd "="; lpre = parse_list_var ;
	       '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
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  
157
158
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; pl = parse_pragma_list ;
	       'Genlex.Kwd ","; 'Genlex.Ident typ ;
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
	       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)
		  | "float" -> (var, FloatT(-.max_float, max_float))
		  | "int" -> (var, IntT(min_int, max_int))
		  | 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
	    

205
206
and (parse_list_var: aut_token -> vnt list) = 
  fun tok -> 
207
208
209
210
211
212
    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
213
214
and (parse_var: aut_token -> vnt) = 
  fun tok -> 
215
216
217
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
218
219
220
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; 
	       prag_var = parse_pragma_list ; 
	       'Genlex.Kwd ",";  'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
221
222
	    -> 
	      ( match typ with
223
		  "bool" -> (var, BoolT)
224
		| "float" -> (var, FloatT(-.max_float, max_float))
225
		| "int" -> (var, IntT(min_int, max_int))
226
227
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
228
229
230
	with e ->
	  print_err_msg tok_list "parse_var" ;
	  raise e
231

232
233
and (parse_list_arc: vnt list -> aut_token -> read_arc list) = 
  fun vars tok -> 
234
235
    let tok_list = Stream.npeek 10 tok in
      try
236
	parse_list (parse_arc vars) tok
237
238
239
      with e ->
	print_err_msg tok_list "parse_list_arc" ;
	raise e
240
241
and (parse_arc: vnt list -> aut_token -> read_arc) = 
  fun vars tok -> 
242
243
244
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
245
246
247
	    [< 'Genlex.Ident "From"; 'Genlex.Int node_from ; 
	       'Genlex.Ident "To"; 'Genlex.Int node_to ; 
	       'Genlex.Ident "With"; arc_info = parse_arc_info vars  >]
248
249
250
251
	    -> Arc(node_from, arc_info, node_to)
	with e ->
	  print_err_msg tok_list "parse_arc" ;
	  raise e
252
253
and (parse_arc_info: vnt list -> aut_token -> arc_info) = 
  fun vars tok -> 
254
255
256
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
257
	    [< 'Genlex.Int weigth ; 'Genlex.Ident ":"; expr = parse_formula_eps vars >] 
258
259
260
261
	    -> (weigth, expr)
	with e ->
	  print_err_msg tok_list "parse_arc_info" ;
	  raise e
262

263
264
and (parse_formula_eps: vnt list -> aut_token -> formula_eps) = 
  fun vars tok -> 
265
266
267
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser   
268
269
	  | [< 'Genlex.Ident "eps" >] -> Eps
	  | [< 'Genlex.Ident "("; 'Genlex.Ident "eps"; 'Genlex.Ident ")" >] -> Eps
270
	  | [< f = parse_formula vars >] -> Form(f)
271
272
273
274
	with e ->
	  print_err_msg tok_list "parse_formula_eps" ;
	  raise e
	    
275
276
and (parse_formula: vnt list -> aut_token -> formula) = 
  fun vars tok -> 
277
278
279
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
	    [< '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
	  | [< 'Genlex.Ident id ; pl = parse_pragma_list ; 
	       f1 = parse_expr_or_bool_ident id vars; 
	       f = parse_more_formula f1 vars    >] -> f
298
	  | [< e1 = parse_expr vars ; f1 = parse_expr_right e1 vars ; 
299
	       f = parse_more_formula f1 vars    >] -> f
300
301
302
	with e ->
	  print_err_msg tok_list "parse_formula" ;
	  raise e
303

304
305
and (parse_expr_or_bool_ident: string -> vnt list -> aut_token -> formula) = 
  fun id vars tok -> 
306
    let tok_list = Stream.npeek 10 tok in
307
308
309
310
311
312
313
    let (_, vt) = List.find (fun (vn,vt) -> vn = id) vars in
    let var =
      match vt with
	  BoolT -> Ivar("XXX")
	| IntT(_,_) -> Ivar(id)
	| FloatT(_,_) -> Fvar(id)
    in
314
315
      try
	match tok with parser  
316
317
318
319
320
	    [< '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)
321
	  | [< f = parse_more_formula (Bvar(id)) vars >] -> f 
322
323
324
325
	with e ->
	  print_err_msg tok_list "parse_expr_or_bool_ident" ;
	  raise e

326
327
and (parse_more_formula: formula -> vnt list -> aut_token -> formula) = 
  fun f1 vars tok -> 
328
329
330
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
331
332
	    [< '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) 
333
334
335
336
	  | [< >] -> f1
	with e ->
	  print_err_msg tok_list "parse_more_formula" ;
	  raise e
337
338
and (parse_expr_right : expr -> vnt list -> aut_token -> formula) = 
  fun e1 vars tok -> 
339
340
341
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser
342
343
344
345
346
	    [< '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)
347
348
349
350
	with e ->
	  print_err_msg tok_list "parse_expr_rigth" ;
	  raise e
	    
351
352

(* 
353
354
355
 ** The following is copy-paste-adapted from sec 1.8 of the ocaml ref man 
 ** untitled ``pretty printing and parsing''.
 *)
356
357
and (parse_expr: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
358
    match tok with parser  
359
360
361
	[< 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 -> 
362
    match tok with parser  
363
364
	[< 'Genlex.Kwd "+"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
365
	   e = parse_more_adds (Sum(e1, e2)) vars >] -> e
366
367
      | [< 'Genlex.Kwd "-"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
368
	   e = parse_more_adds (Diff(e1, e2)) vars >] -> e
369
      | [<  >] -> e1
370
371
and (parse_mult: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
372
    match tok with parser  
373
374
375
	[< 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 -> 
376
    match tok with parser  
377
378
	[< 'Genlex.Kwd "*"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
379
	   e = parse_more_mults (Prod(e1, e2)) vars >] -> e
380
381
      | [< 'Genlex.Kwd "/"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
382
	   e = parse_more_mults (Quot(e1, e2)) vars >] -> e
383
384
      | [< 'Genlex.Kwd "mod"; pl = parse_pragma_list ; 
	   e2 = parse_simple vars; 
385
	   e = parse_more_mults (Mod(e1, e2)) vars >] -> e
386
      | [<  >] -> e1
387
388
and (parse_simple: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
389
    match tok with parser  
390
	[< 'Genlex.Ident s ; pl = parse_pragma_list >] -> 
391
392
393
	  let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in
	  let var =
	    match vt with
394
		BoolT -> assert false 
395
396
397
398
	      | IntT(_,_) -> Ivar(s)
	      | FloatT(_,_) -> Fvar(s)
	  in
	    var
399
400
401
402
403
      | [< 'Genlex.Int i; pl = parse_pragma_list >]   -> Ival(i)
      | [< 'Genlex.Float f; pl = parse_pragma_list >] -> Fval(f)
      | [< 'Genlex.Kwd "IfThenElseExpr";  pl = parse_pragma_list ; 
	   f1 = parse_formula vars; 
	   e2 = parse_expr vars; 
404
405
	   e3 = parse_expr vars >] -> Ite(f1, e2, e3) 
      | [< 'Genlex.Kwd "("; e = parse_expr vars; 'Genlex.Kwd ")" >] -> e
406