Project

General

Profile

Revision 843bc20f

View differences:

Makefile.in
47 47
	install -m 0755 $(LOCAL_BINDIR)/* ${bindir}
48 48
	mkdir -p ${includedir}/lustrec
49 49
	cp include/* ${includedir}/lustrec
50
	mkdir -p ${datadir}
50 51
	install -m 0655 share/FindLustre.cmake ${datadir}
51 52

  
52 53
.PHONY: compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean
src/backends/Horn/horn_backend.ml
522 522

  
523 523

  
524 524
let translate fmt basename prog machines =
525
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification");
526 525
  List.iter (print_machine machines fmt) (List.rev machines);
527 526
  main_print machines fmt
528 527

  
src/log.ml
11 11

  
12 12
let report ~level:level p =
13 13
if !Options.verbose_level >= level then
14
  Format.eprintf "%t" p
14
  begin
15
    Format.eprintf "%t" p;
16
    Format.pp_print_flush Format.err_formatter ()
17
  end
15 18

  
16 19
(* Local Variables: *)
17 20
(* compile-command:"make -C .." *)
src/main_lustre_compiler.ml
70 70
	begin
71 71
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
72 72
       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
73
(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
73
	  (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
74 74
	  Lusic.print_lusic_to_h destname lusic_ext
75 75
	end
76 76
      else
......
85 85
	end
86 86
  end
87 87

  
88

  
89

  
88 90
(* compile a .lus source file *)
89 91
let rec compile_source dirname basename extension =
90 92

  
......
155 157

  
156 158
  (* Compatibility with Lusi *)
157 159
  (* Checking the existence of a lusi (Lustre Interface file) *)
158
  match !Options.output with
160
  (match !Options.output with
159 161
    "C" ->
160 162
      begin
161 163
        let extension = ".lusi" in
162 164
        compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
163 165
      end
164
   |_ -> ();
166
   |_ -> ());
165 167

  
166 168
  Typing.uneval_prog_generics prog;
167 169
  Clock_calculus.uneval_prog_generics prog;
......
299 301
	let source_file = destname ^ ".smt2" in (* Could be changed *)
300 302
	let source_out = open_out source_file in
301 303
	let fmt = formatter_of_out_channel source_out in
302
	Horn_backend.translate fmt basename prog machine_code;
304
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
305
        Horn_backend.translate fmt basename prog machine_code;
303 306
	(* Tracability file if option is activated *)
304 307
	if !Options.traces then (
305 308
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
306 309
	let traces_out = open_out traces_file in
307 310
	let fmt = formatter_of_out_channel traces_out in
311
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
308 312
	Horn_backend.traces_file fmt basename prog machine_code;
309 313
	)
310 314
      end
......
321 325
    | _ -> assert false
322 326
  in
323 327
  begin
324
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
328
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
325 329
  (* We stop the process here *)
326 330
    exit 0
327 331
  end
src/normalization.ml
379 379
	  annots = List.map (fun v ->
380 380
	    let eq =
381 381
	      try
382
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs
382
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs) 
383 383
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
384
	    let expr = substitute_expr diff_vars defs eq.eq_rhs in
384
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
385 385
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
386 386
	    (["traceability"], pair)
387 387
	  ) diff_vars;
src/parser_lustre.mly
43 43
let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false
44 44
let get_current_node () = try List.hd !node_stack with _ -> assert false
45 45

  
46
let rec fby expr n init =
47
  if n<=1 then
48
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr)))
49
  else
50
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init))))
51
  
46 52
%}
47 53

  
48 54
%token <int> INT
......
403 409
| node_ident LPAR expr RPAR EVERY expr
404 410
    {mkexpr (Expr_appl ($1, $3, Some $6))}
405 411
| node_ident LPAR tuple_expr RPAR
406
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
412
    {
413
      let id=$1 in
414
      let args=List.rev $3 in
415
      match id, args with
416
      | "fbyn", [expr;n;init] ->
417
	let n = match n.expr_desc with
418
	  | Expr_const (Const_int n) -> n
419
	  | _ -> assert false
420
	in
421
	fby expr n init
422
      | _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None))
423
    }
407 424
| node_ident LPAR tuple_expr RPAR EVERY expr
408
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some $6)) }
425
    {
426
      let id=$1 in
427
      let args=List.rev $3 in
428
      let clock=$6 in
429
      if id="fby" then
430
	assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
431
      else
432
	mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) 
433
    }
409 434

  
410 435
/* Boolean expr */
411 436
| expr AND expr 
test/test-compile.sh
5 5
declare c i w h a v
6 6
declare -a files
7 7

  
8
SRC_PREFIX="../.."
9
#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
8
#SRC_PREFIX="../.."
9
SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
10 10
NOW=`date "+%y%m%d%H%M"`
11 11
report=`pwd`/report-$NOW
12 12
#LUSTREC="../../_build/src/lustrec"

Also available in: Unified diff