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/

luc_exe.ml 12.5 KB
Newer Older
1
(*-----------------------------------------------------------------------
2
3
4
5
6
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
7
** File: luc_exe.ml
8
9
** Author: jahier@imag.fr
*)
10
11
12
13
14

(*------------------------------------------------------------------------*)

open Util
open Formula
15
open Value
16
17
open Env_state
open List
18
open Command_line_luc_exe
19
20
21
22

(*------------------------------------------------------------------------*)


23
let (options:Command_line_luc_exe.optionsT) = {
24
  show_automata = false ;
25
  user_seed = 0 ;
26
  boot = false 
27
28
29
30
31
32
33
}

(*------------------------------------------------------------------------*)

type rif_token = Genlex.token 
type rif_stream = Genlex.token Stream.t

34
let rec (parse_luc_files : rif_stream -> string list list -> string list list) =
35
36
37
  fun stream sll -> 
    try (
      match (Stream.next stream) with
38
	  (Genlex.String str) -> parse_luc_files stream ([str]::sll)
39
40
41
	| (Genlex.Kwd "x")    -> 
	    ( match (sll, (Stream.next stream)) with
		  ((sl::tail), (Genlex.String str2)) -> 
42
		    parse_luc_files stream ((append sl [str2])::tail)  
43
44
45
		| _ -> 
		    failwith "### parse error.\n" 
	    )
46
47
	| _  -> failwith ("### parse error. A string (wrapped with double" ^
			  "quotes) or `x' was expected. \n")
48
49
50
51
52
53
54
    )
    with Stream.Failure -> 
      sll

(* Dynamically change the current env automata *)
let (replace_env_dynamically: rif_stream -> unit) =
  fun stream -> 
55
    let luc_files = parse_luc_files stream [] in
56
      Env_state.clear_all ();
57
      output_string stderr "loading ";
58
      List.iter (fun x -> output_string stderr (x ^ " ")) (List.flatten luc_files);
59
      output_string stderr "  ...\n  ";
60
      Env_state.read_env_state luc_files;
61
62
      output_string stderr "  ...  ok\n";      
      Env_state.set_output_var_names (Env_state.out_env_unsorted ()) ;
63

64
      if options.show_automata then (
65
	Show_env.luc_to_dot (flatten (Env_state.current_nodes ())) [] 
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
		("automata" ^ (string_of_int (Hashtbl.hash Sys.argv))) 
		(Env_state.graph ()) ;
      ) ;

      print_string "#inputs ";
      List.iter 
	(fun (vn,vt) -> 
	   print_string (vn ^ ":" ^ (var_type_to_string2 vt) ^ " ")
	) 
	(Env_state.out_env_unsorted ());
      print_string "\n";

      flush stdout;
      flush stderr
	

(*------------------------------------------------------------------------*)
(* RIF parsing *)

85
let lexer = Genlex.make_lexer ["q"; "#"; "x"; "load_luc"; "#@"; "@#"]
86
87
88
89
90
let rif_pragmas = ["inputs"]

(* Which pragmas should be defined ? *)
(* let rif_pragmas = ["outs";"outputs";"program";"inputs";"step";"reset"] *)

91
92
let rec (read_rif_input : vnt list -> env_in) =
  fun vntl -> 
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
    (** Reads the environment input values on stdin. It should
      follow the rif format. *)
    let tbl = Hashtbl.create (List.length vntl) in
      if vntl = []
      then tbl
      else 
	let line = read_line () in
	let stream = lexer(Stream.of_string line) in
	  parse_rif_stream vntl stream tbl
	    
and (parse_rif_stream : vnt list -> rif_stream -> env_in -> env_in) =
  fun vntl stream tbl -> 
    if vntl = []
    then tbl
    else 
      let tok_list = Stream.npeek 2 stream in
109
	match tok_list with
110
111
112
113
114
115
	  | [Genlex.Kwd "#"; Genlex.Ident id] ->
	      if List.mem id rif_pragmas
	      then 
		(
		  Stream.junk stream ;
		  Stream.junk stream ; 
116
		  parse_rif_stream vntl (lexer (Stream.of_string (read_line ()))) tbl
117
118
119
120
121
122
		)
	      else
		(* We skip everything that occurs after a [#] not followed by a
		   member of [rif_pragmas], until the next eol. *)
		(
		  Stream.junk stream ; 
123
124
		  parse_rif_stream 
		    vntl (lexer (Stream.of_string (read_line ()))) tbl
125
126
		)

127
	  | [Genlex.Kwd "#" ; Genlex.Kwd "load_luc"]
128
129
130
131
132
133
	      (* dynamically change the environment *)
	    ->
	      (
		Stream.junk stream ; 
		Stream.junk stream ; 
		replace_env_dynamically stream;
134
135
136
		parse_rif_stream 
		  (Env_state.in_env_unsorted ()) 
		  (lexer (Stream.of_string (read_line ()))) tbl
137
138
	      )

139
140
141
142
143
144
	  | (Genlex.Kwd "#")::_ 
	      (* Ditto *)
	    ->
	      Stream.junk stream ; 
	      parse_rif_stream vntl (lexer (Stream.of_string (read_line ()))) tbl
		
145
146
147
148
149
150
	  | (Genlex.Kwd "q")::_ 
	      (* Ditto *)
	    ->
	      print_string "bye!\n";
	      exit 0
		
151
152
153
154
155
156
157
158
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
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
	  | (Genlex.Kwd "#@")::_ ->
	      (* Beginning of multi-line comment. Note that here,
		 unlike the rif format, we ignore multi line pragmas;
		 namely, we handle them as a lusti-line comment. *)
	      (
		Stream.junk stream ;
		ignore_toks_until_end_of_pragmas vntl stream tbl
	      ) 

	  | (Genlex.Float f)::_ ->
	      (
		Stream.junk stream ;
		Hashtbl.add tbl (fst (hd vntl)) (N(F(f))) ;
		parse_rif_stream (tl vntl) stream tbl
	      )

	  | (Genlex.Int i)::_ ->
	      (
		Stream.junk stream ;
		if ((var_type_to_string (snd (hd vntl))) = "bool")
		then 
		  if i = 0 
		  then Hashtbl.add tbl (fst (hd vntl)) (B(false))
		  else Hashtbl.add tbl (fst (hd vntl)) (B(true))
		else Hashtbl.add tbl (fst (hd vntl)) (N(I(i))) ;
		parse_rif_stream (tl vntl) stream tbl
	      )
	      
	  | (Genlex.Ident b)::_ ->
	      (
		Stream.junk stream ;
		if mem b ["f"; "F";"false"]
		then Hashtbl.add tbl (fst (hd vntl)) (B(false))
		else if  mem b ["t"; "T";"true"]
		    then Hashtbl.add tbl (fst (hd vntl)) (B(true))
		else 
		  failwith ("### parse error. " ^ b ^ " is unknown \n") ;
		
		parse_rif_stream (tl vntl) stream tbl
	      )
	      
	  | [] -> 
	      (* Eol is is reached; proceed with the next one *)
	      parse_rif_stream vntl (lexer (Stream.of_string (read_line ()))) tbl

	  | _ -> failwith ("### parse error.\n")
	      
and (ignore_toks_until_end_of_pragmas : vnt list -> rif_stream -> env_in 
       -> env_in) =
  fun vntl stream tbl -> 
    (* ignore all tokens until "@#" is reached *)
    let tok_opt = Stream.peek stream in
      match tok_opt  with
	| Some(Genlex.Kwd "@#") ->
	    (
	      Stream.junk stream ;
	      parse_rif_stream vntl stream tbl
	    )
	| Some(_) ->
	    (
	      Stream.junk stream ;
	      ignore_toks_until_end_of_pragmas vntl stream tbl 
	    )
	| None -> 
	    (* Eol is is reached; proceed with the next one *)
	    ignore_toks_until_end_of_pragmas vntl 
	    (lexer (Stream.of_string (read_line ()))) tbl
	    
    
220
221
222
223

let (write_rif_output : vnt list -> env_out -> unit) =
  fun vntl output -> 
    let ae_l = List.map (fun (vn, _) -> List.assoc vn output) vntl in
224
      List.iter (Value.print stdout) ae_l
225
226
227
228
229
230
231
232
233
234
235
236


(*------------------------------------------------------------------------*)

let arg_nb = (Array.length Sys.argv) 

external random_seed: unit -> int = "sys_random_seed";;

let rec (main : unit -> 'a) =
  fun _ ->
    try
      if (arg_nb < 2) 
237
      then output_string stderr usage 
238
239
240
      else
	main2 ()
    with 
241
	Failure(errmsg) -> output_string stderr errmsg
242
      | e ->  
243
(* 	  Env_state.dump_env_state_stat (); *)
244
(* 	  print_string  Command_line_luc_exe.usage ; *)
245
	  raise e	
246
247

and 
248
  (get_luc_exe_options: int -> int) =
249
250
251
  fun n -> 
    try 
      begin
252
	let opt = List.assoc Sys.argv.(n) Command_line_luc_exe.string_to_option in
253
	  match opt with
254
255
256
	      ShowAut -> options.show_automata <- true ; (n+1)
	    | NoShowAut -> options.show_automata <- false ; (n+1)
	    | Boot -> options.boot <- true ; (n+1)
257
	    | Verbose  -> Env_state.set_verbose true ; (n+1)
258
259
	    | Inside    -> Env_state.set_draw_mode  Env_state.Inside ; (n+1)
	    | Edges    -> Env_state.set_draw_mode  Env_state.Edges ; (n+1)
260
	    | Vertices -> Env_state.set_draw_mode  Env_state.Vertices ; (n+1)
261
262
263
264
265
266
267
	    | Precision ->
		let str = (Sys.argv.(n+1)) in
		  Util.precision := (cmd_line_string_to_int str
		    ("*** Error when calling lurette: an " ^
		     "integer is expected after the " ^
		     "option --precision\n")) ;
		  n+2
268
269
270
	    | Seed ->
		let str = (Sys.argv.(n+1)) in
		  options.user_seed <- cmd_line_string_to_int str 
271
		    ("*** Error when calling luc_exe: an " ^
272
273
274
275
276
277
278
279
280
		     "integer is expected after the " ^
		     "option --with-seed\n") ;
		  n+2
      end
    with Not_found -> n
and
  (get_env_from_args: int -> string list list -> string list list) =
  fun n file_ll -> 
    (** Returns the environment file names given at top-level into a
281
      list of list.  E.g., if the call [luc_exe env1 x env2 x env3
282
283
284
285
286
287
      env4] is done, then [get_env_from_args 10 []] (where 10 is the
      arg nb) returns [[["env1"; "env2"; "env3"]; ["env4"]]].

      Also set the command line options if any.  *)
    if (n = arg_nb) then file_ll
    else
288
      let m = get_luc_exe_options n in
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
	(* m > n iff Sys.argv.(n) is an option *)
	if 
	  (m > n) 
	then 
	  get_env_from_args m file_ll
	else
	  let arg = Sys.argv.(m) in
	    if 
	      (arg = "x") 
	    then
	      match file_ll with
		  sl::sll -> 
		    let env = Sys.argv.(n+1) in
                      get_env_from_args (n+2) ((env::sl)::sll)
		| []  -> assert false
	    else 
	      get_env_from_args (n+1) ([arg]::file_ll)
and
  (main2 : unit -> 'a) =
  fun _ -> 
309
310

    (* Clean up tables as non-reg assert stuff migth have filled them *)
311
    let _ = Env_state.clear_all () in
312

313
314
    (* Initialisation of `Env_state.env_state' *)
    let env_llist = (get_env_from_args 1 []) in
315
    let () = Env_state.read_env_state env_llist in
316
           
317
318
319
320
321
322
323
    (* Initialisation of the random engine *)
    let seed = 
      if (options.user_seed = 0)
      then (random_seed ())
      else  options.user_seed
    in
      Random.init seed ;
324
325
326
327
      output_string stderr "#The random engine was initialized with the seed ";
      output_string stderr (string_of_int seed);
      output_string stderr  "\n ";
      flush stderr ;      
328
329


330
      if options.show_automata then (
331
	Show_env.luc_to_dot (flatten (Env_state.current_nodes ())) [] 
332
333
		("automata" ^ (string_of_int (Hashtbl.hash Sys.argv))) 
		(Env_state.graph ()) ;
334
335
336
	Util.gv ("automata" ^ (string_of_int (Hashtbl.hash Sys.argv)) ^ ".ps")
      ) ;

337

338
      Env_state.set_output_var_names (Env_state.out_env_unsorted ()) ;
339
340

      (* Initializing the solution number table *)
341
342
343
344
      Env_state.set_sol_number 
	(Bdd.dtrue (Env_state.bdd_manager ())) (Util.one_sol, Util.zero_sol);
      Env_state.set_sol_number 
	(Bdd.dfalse (Env_state.bdd_manager ())) (Util.zero_sol, Util.one_sol);
345
346
347
348
349
350
351
352
353
354
355
356

      print_string "#inputs ";
      List.iter 
	(fun (vn,vt) -> 
	   print_string (vn ^ ":" ^ (var_type_to_string2 vt) ^ " ")
	) 
	(Env_state.out_env_unsorted ());
      print_string "\n";
      flush stdout;

      if options.boot 
      then
357
358
359
360
	let nll_call_out_loc_list = Env.env_try 1 1 (Hashtbl.create 0) in
	let (nll, call, out, loc) = 
	  match nll_call_out_loc_list with
	      [(nll, call, out, loc)] -> (nll, call, out, loc)
361
362
	    | _ -> assert false
	in
363
	  Env.env_step nll call out loc ;
364
	  Env.update_pre 
365
366
367
	    (Env_state.input ()) 
	    (Env_state.output ()) 
	    (Env_state.local ()) ;
368
369
370
371
372
373
374
375
376
	  write_rif_output (Env_state.out_env_unsorted ()) out ;
      else ();  

      main_loop 1 ;
      flush stdout

and
  main_loop t = 

377
  let previous_nodes = (Env_state.current_nodes ()) in
378
379
  let nl = List.flatten previous_nodes in
  let _ = 
380

381
    if Env_state.verbose () then
382
383
      (
	List.iter  
384
385
	 (fun n -> 
	    output_string stderr ("current nodes:" ^ (string_of_int n) ^ "\n "))  
386
	 nl; 
387
	Control.print_state (Env_state.ctrl_state ());
388
389
	flush stderr
      ) ;
390

391
    print_string ("\n# step " ^ (string_of_int t)) ;
392
    if Env_state.verbose () then
393
      (
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
	print_string "(";
	if (List.length nl)  > 1
	then 
	  (
	    print_string "current nodes are ";
	    List.iter 
	      (fun n -> print_string ((string_of_int n) ^ " ")) 
	      nl
	  )
	else 
	  (
	    print_string "current node is ";
	    print_string (string_of_int (List.hd nl))
	  );
	print_string ("):")
      ) ;
    print_string ("\n");
411
412
    flush stdout 
  in
413
  let input = read_rif_input (Env_state.in_env_unsorted ()) in
414
  let nll_call_out_loc_list = Env.env_try 1 1 input in
415

416
417
418
  let (nll, call, out, loc) = 
    match nll_call_out_loc_list with
	[(nll, call, out, loc)] -> (nll, call, out, loc)
419
420
      | _ -> assert false
  in
421
422
    
    Env.env_step nll call out loc ;
423
    
424
425
426
427
428
    Env.update_pre 
      (Env_state.input ()) 
      (Env_state.output ()) 
      (Env_state.local ()) ;
    
429
    write_rif_output (Env_state.out_env_unsorted ()) out ;
430
    if options.show_automata then (
431
      if (previous_nodes <> Env_state.current_nodes ()) then 
432
433
434
	  Show_env.luc_to_dot (flatten (Env_state.current_nodes ()))
          (flatten previous_nodes) 
	    ("automata" ^ (string_of_int (Hashtbl.hash Sys.argv))) 
435
436
	  (Env_state.graph ())
    );
437
438
439
440

    (* Clean-up cached info that depend on pre or inputs *)
    Env_state.clear_step () ;

441
442
443
444
445
    main_loop (t+1) 
;;
      


446
447
448
449
450
451
452
	

try main ()
with e ->
  print_string ((Printexc.to_string e) ^ "\n");
  flush stdout
;;   
453
454