parse_env.ml 9.39 KB
Newer Older
1
(*pp camlp4o *)
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** 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

  
type read_arc = Arc of node * arc_info * node

type read_automata = Automata of 
18
  node        (* Initial node *)
19
20
21
  * vnt list  (* Input var list *)
  * vnt list  (* Output var list *)
  * vnt list  (* Local var list *)
22
23
  * vne list  (* pre var list of expression *)
  * vnf list  (* pre var list of formula *)
24
25
26
27
28
29
30
31
32
33
34
  * read_arc list  (* Transition list *)

(* Keywords of the automata format *)
let lexer = Genlex.make_lexer ["automata"; "["; "]"; "("; ")"; ","; ":"; ";";
			       "arc"; "eps"; "pre";
			       "And"; "Or"; "Not"; "true"; "false";
			       "="; ">"; ">=";
			       "+"; "-"; "*"; "/"; "mod"; "%"]

type aut_token = Genlex.token Stream.t

35
36
37
38
39
40
41
42
43
44
45
46
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_int i
	| Genlex.Float(f)    -> print_float f
	| Genlex.String(str) -> print_string str
	| Genlex.Char(c)     -> print_char c  
    in
      print_string " "
47

48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
let debug_parsing = false

let print_err_msg tok_list func =
  if debug_parsing then
    begin
      print_string ("* Parse error in " ^ func ^ ".\n\t\t\t\t");
      print_string ("The next 10 tokens are:\t``");
      List.iter (print_genlex_token) tok_list ;
      print_string ("''\n");
      flush stdout
    end 
  else ()
  

(** Parsing lists *)
63
64
65
let rec
  (parse_list: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
66
67
68
69
70
71
72
73
74
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
            [< vnt = parse ; tail = (parse_list_var_tail (parse)) >]
	    -> vnt :: tail  
	  | [< >] -> [] (* empty list *)
	with e ->
	  print_err_msg tok_list "parse_list";
	  raise e
75
76
and (parse_list_var_tail: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
77
78
79
80
81
82
83
84
85
86
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser 
	  | [< 'Genlex.Kwd ";" ; a = parse ;
	       tail = (parse_list_var_tail (parse)) >]
	    -> a :: tail  
	  | [< >] -> [] (* end of the list *)
	with e ->
	  print_err_msg tok_list "parse_list_var_tail";
	  raise e
87
88
89



90
91
let rec (parse_automata: aut_token -> read_automata) = 
  fun tok -> 
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "automata" ;
	       'Genlex.Kwd "(" ; 
	       'Genlex.Int node_id ; 'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; li = parse_list_var ; 'Genlex.Kwd "]" ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; lo = parse_list_var ; 'Genlex.Kwd "]" ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; ll = parse_list_var ; 'Genlex.Kwd "]" ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; lpe = parse_list_pre_expr ; 'Genlex.Kwd "]" ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; lpf = parse_list_pre_form ; 'Genlex.Kwd "]" ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; la = parse_list_arc ; 'Genlex.Kwd "]" ;
	       'Genlex.Kwd ")" >] 
            -> Automata(node_id, li, lo, ll, lpe, lpf, la)
	with e ->
	  print_err_msg tok_list "parse_automata";
	  raise e
	    
115

116
117
and (parse_list_var: aut_token -> vnt list) = 
  fun tok -> 
118
119
120
121
122
123
    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
124
125
and (parse_var: aut_token -> vnt) = 
  fun tok -> 
126
127
128
129
130
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; 'Genlex.Kwd ","; 
	       'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
131
132
133
134
135
136
137
138
	    -> 
	      ( match typ with
		  "boolean" -> (var, BoolT)
		    (* XXX Rajouter dans le format un moyen de prcised ces bornes *)
		| "float" -> (var, FloatT(-100., 100.))
		| "int" -> (var, IntT(-100, 100))
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
139
140
141
	with e ->
	  print_err_msg tok_list "parse_var" ;
	  raise e
142

143
and (parse_list_pre_expr: aut_token -> vne list) = 
144
  fun tok -> 
145
146
147
148
149
150
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_pre_expr) tok
      with e ->
	print_err_msg tok_list "parse_list_pre_expr" ;
	raise e
151
and (parse_pre_expr: aut_token -> vne) = 
152
  fun tok -> 
153
154
155
156
157
158
159
160
161
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; 'Genlex.Kwd ","; 
	       e = parse_expr ; 'Genlex.Kwd ","; init = parse_expr ; 'Genlex.Kwd ")" >]
	    -> (var, (e, init))
	with e ->
	  print_err_msg tok_list "parse_pre_expr" ;
	  raise e
162
163
164

and (parse_list_pre_form: aut_token -> vnf list) = 
  fun tok -> 
165
166
167
168
169
170
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_pre_form) tok
      with e ->
	  print_err_msg tok_list "parse_list_pre_form" ;
	raise e
171
172
and (parse_pre_form: aut_token -> vnf) = 
  fun tok -> 
173
174
175
176
177
178
179
180
181
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; 'Genlex.Kwd ","; 
	       f = parse_formula ; 'Genlex.Kwd ","; init = parse_formula; 'Genlex.Kwd ")" >]
	    -> (var, (f, init))
	with e ->
	  print_err_msg tok_list "parse_pre_form" ;
	  raise e
182
183
184
185


and (parse_list_arc: aut_token -> read_arc list) = 
  fun tok -> 
186
187
188
189
190
191
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_arc) tok
      with e ->
	print_err_msg tok_list "parse_list_arc" ;
	raise e
192
193
and (parse_arc: aut_token -> read_arc) = 
  fun tok -> 
194
195
196
197
198
199
200
201
202
203
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "arc"; 'Genlex.Kwd "("; 'Genlex.Int node_from ; 
	       'Genlex.Kwd ","; arc_info = parse_arc_info ; 
	       'Genlex.Kwd "," ; 'Genlex.Int node_to ; 'Genlex.Kwd ")";  >]
	    -> Arc(node_from, arc_info, node_to)
	with e ->
	  print_err_msg tok_list "parse_arc" ;
	  raise e
204
205
and (parse_arc_info: aut_token -> arc_info) = 
  fun tok -> 
206
207
208
209
210
211
212
213
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Int weigth ; 'Genlex.Kwd ":"; expr = parse_formula_eps >] 
	    -> (weigth, expr)
	with e ->
	  print_err_msg tok_list "parse_arc_info" ;
	  raise e
214
215
216

and (parse_formula_eps: aut_token -> formula_eps) = 
  fun tok -> 
217
218
219
220
221
222
223
224
225
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser   
	    [< 'Genlex.Kwd "eps" >] -> Eps
	  | [< f = parse_formula >] -> Form(f)
	with e ->
	  print_err_msg tok_list "parse_formula_eps" ;
	  raise e
	    
226
227
and (parse_formula: aut_token -> formula) = 
  fun tok -> 
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "Not"; f1 = parse_formula ; 
	       f = parse_more_formula (Not(f1)) >] -> f  
	  | [< 'Genlex.Kwd "("; f1 = parse_formula; 'Genlex.Kwd ")" ; 
	       f = parse_more_formula f1 >] -> f 
	  | [< 'Genlex.Kwd "true" ; f = parse_more_formula True >] -> f
	  | [< 'Genlex.Kwd "false" ; f = parse_more_formula False >] -> f
	  | [< 'Genlex.Ident b ; f = parse_more_formula (Bvar(b)) >] -> f
	  | [< e1 = parse_expr; f1 = parse_expr_right e1 ; 
	       f = parse_more_formula f1 >] -> f
	with e ->
	  print_err_msg tok_list "parse_formula" ;
	  raise e
243
244
245

and (parse_more_formula: formula -> aut_token -> formula) = 
  fun f1 tok -> 
246
247
248
249
250
251
252
253
254
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "Or";  f2 = parse_formula >] -> Or(f1, f2)
	  | [< 'Genlex.Kwd "And"; f2 = parse_formula >] -> And(f1, f2) 
	  | [< >] -> f1
	with e ->
	  print_err_msg tok_list "parse_more_formula" ;
	  raise e
255
256
and (parse_expr_right : expr -> aut_token -> formula) = 
  fun e1 tok -> 
257
258
259
260
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser
	    [< 'Genlex.Kwd "=";  e2 = parse_expr >] -> Eq(e1, e2) 
261
262
263
264
	  | [< 'Genlex.Kwd ">";  e2 = parse_expr >] -> Sup(e1, e2) 
	  | [< 'Genlex.Kwd ">="; e2 = parse_expr >] -> SupEq(e1, e2)
	  | [< 'Genlex.Kwd "<";  e2 = parse_expr >] -> Inf(e1, e2) 
	  | [< 'Genlex.Kwd "<="; e2 = parse_expr >] -> InfEq(e1, e2)
265
266
267
268
	with e ->
	  print_err_msg tok_list "parse_expr_rigth" ;
	  raise e
	    
269
270

(* 
271
272
273
 ** The following is copy-paste-adapted from sec 1.8 of the ocaml ref man 
 ** untitled ``pretty printing and parsing''.
 *)
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
and (parse_expr: aut_token -> expr) = 
  fun tok -> 
    match tok with parser  
	[< e1 = parse_mult; e = parse_more_adds e1 >] -> e
and (parse_more_adds: expr -> aut_token -> expr) = 
  fun e1 tok -> 
    match tok with parser  
	[< 'Genlex.Kwd "+"; e2 = parse_mult; 
	   e = parse_more_adds (Sum(e1, e2)) >] -> e
      | [< 'Genlex.Kwd "-"; e2 = parse_mult; 
	   e = parse_more_adds (Diff(e1, e2)) >] -> e
      | [<  >] -> e1
and (parse_mult: aut_token -> expr) = 
  fun tok -> 
    match tok with parser  
	[< e1 = parse_simple; e = parse_more_mults e1 >] -> e
and (parse_more_mults: expr -> aut_token -> expr) = 
  fun e1 tok -> 
    match tok with parser  
	[< 'Genlex.Kwd "*";   e2 = parse_simple; 
	   e = parse_more_mults (Prod(e1, e2)) >] -> e
      | [< 'Genlex.Kwd "/";   e2 = parse_simple; 
	   e = parse_more_mults (Quot(e1, e2)) >] -> e
      | [< 'Genlex.Kwd "mod"; e2 = parse_simple; 
	   e = parse_more_mults (Mod(e1, e2)) >] -> e
      | [<  >] -> e1
and (parse_simple: aut_token -> expr) = 
  fun tok -> 
    match tok with parser  
303
304
305
	[< 'Genlex.Ident s >] -> Nvar(s)
      | [< 'Genlex.Int i >]   -> Ival(i)
      | [< 'Genlex.Float f >] -> Fval(f)
306
307
      | [< 'Genlex.Kwd "("; e = parse_expr; 'Genlex.Kwd ")" >] -> e