Project

General

Profile

« Previous | Next » 

Revision ed736b69

Added by Pierre-Loïc Garoche over 8 years ago

Merge of last trunk commits
Added fbyn(expr, n, init) to encode
init -> pre (init -> pre (init -> ... pre expr))
with n occurences of init

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