Project

General

Profile

« Previous | Next » 

Revision 7291cb80

Added by Xavier Thirioux over 9 years ago

- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@171 041b043f-8d7c-46b2-b46e-ef0dd855326e

View differences:

src/main_lustre_compiler.ml
36 36 
    begin
37 37 
      try
38 38 
	Typing.type_prog env decls
39 
    (*Typing.uneval_prog_generics prog*)
40 39 
      with (Types.Error (loc,err)) as exc ->
41 40 
	Format.eprintf "Typing error at loc %a: %a@]@."
42 41 
	  Location.pp_loc loc
......
72 71 
  Location.init lexbuf filename;
73 72 
  (* Parsing *)
74 73 
  report ~level:1 (fun fmt -> fprintf fmt "@[<v>.. parsing header file %s@,@?" filename);
75 
  let header =
76 
    try
77 
      Parse.prog Parser_lustre.header Lexer_lustre.token lexbuf
78 
    with (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc ->
79 
      Parse.report_error err;
80 
      raise exc
81 
  in
74 
  try
75 
    Parse.prog Parser_lustre.header Lexer_lustre.token lexbuf
76 
  with (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc ->
77 
    Parse.report_error err;
78 
    raise exc
79 

  		




  
  80
  
    
let check_lusi header =


  		




  82
  81
  
    
  let new_tenv = type_decls Basic_library.type_env header in   (* Typing *)


  		




  83
  82
  
    
  let new_cenv: Clocks.clock_expr Utils.IMap.t = clock_decls Basic_library.clock_env header in   (* Clock calculus *)


  		




  84
  83
  
    
  header, new_tenv, new_cenv


  		




  85
  
  
    
  


  		




  86
  84
  
    
    


  		




  87
  85
  
    
let rec compile basename extension =


  		




  88
  86
  
    
  (* Loading the input file *)


  		




  ......




  114
  112
  
    
      try


  		




  115
  113
  
    
	let basename = s ^ ".lusi" in 


  		




  116
  114
  
    
	report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>Library %s@ " s);


  		




  117
  
  
    
	let _, lusi_type_env, lusi_clock_env = load_lusi basename in 


  		




  
  115
  
    
	let _, lusi_type_env, lusi_clock_env = check_lusi (load_lusi basename) in 


  		




  118
  116
  
    
	report ~level:1 (fun fmt -> fprintf fmt "@]@,@?");


  		




  119
  117
  
    
	Env.overwrite type_env lusi_type_env,


  		




  120
  118
  
    
	Env.overwrite clock_env lusi_clock_env      


  		




  ......




  172
  170
  
    
    raise exc


  		




  173
  171
  
    
    end;


  		




  174
  172
  
    
  *)


  		




  
  173
  
    

  		




  
  174
  
    
  (* Checking the existence of a lusi (Lustre Interface file) *)


  		




  
  175
  
    
  let lusi_name = basename ^ ".lusi" in


  		




  
  176
  
    
  let _ = 


  		




  
  177
  
    
    try 


  		




  
  178
  
    
      let _ = open_in lusi_name in


  		




  
  179
  
    
      let header = load_lusi lusi_name in


  		




  
  180
  
    
      let _, declared_types_env, declared_clocks_env = check_lusi header in


  		




  
  181
  
    
      (* checking type compatibility with computed types*)


  		




  
  182
  
    
      Typing.check_env_compat header declared_types_env computed_types_env;


  		




  
  183
  
    
      (* checking clocks compatibilty with computed clocks*)


  		




  
  184
  
    
      Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;


  		




  
  185
  
    
      Typing.uneval_prog_generics prog


  		




  
  186
  
    
    with Sys_error _ -> ( 


  		




  
  187
  
    
      (* Printing lusi file is necessary *)


  		




  
  188
  
    
      report ~level:1 


  		




  
  189
  
    
	(fun fmt -> 


  		




  
  190
  
    
	  fprintf fmt 


  		




  
  191
  
    
	    ".. generating lustre interface file %s@,@?" lusi_name);


  		




  
  192
  
    
      let lusi_out = open_out lusi_name in


  		




  
  193
  
    
      let lusi_fmt = formatter_of_out_channel lusi_out in


  		




  
  194
  
    
      Typing.uneval_prog_generics prog;


  		




  
  195
  
    
      Printers.pp_lusi_header lusi_fmt source_name prog


  		




  
  196
  
    
    )


  		




  
  197
  
    
    | (Types.Error (loc,err)) as exc ->


  		




  
  198
  
    
      Format.eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@]@."


  		




  
  199
  
    
	Types.pp_error err;


  		




  
  200
  
    
      raise exc


  		




  
  201
  
    
  in


  		




  
  202
  
    

  		




  175
  203
  
    
  (* Computes and stores generic calls for each node,


  		




  176
  204
  
    
     only useful for ANSI C90 compliant generic node compilation *)


  		




  177
  205
  
    
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;


  		




  ......




  180
  208
  
    
  (* Normalization phase *)


  		




  181
  209
  
    
  report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,@?");


  		




  182
  210
  
    
  let normalized_prog = Normalization.normalize_prog prog in


  		




  183
  
  
    
  Typing.uneval_prog_generics normalized_prog;


  		




  
  211
  
    
  (*Typing.uneval_prog_generics normalized_prog;*)


  		




  184
  212
  
    
  report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Printers.pp_prog normalized_prog);


  		




  185
  213
  
    
  (* Checking array accesses *)


  		




  186
  214
  
    
  if !Options.check then


  		




  ......




  196
  224
  
    
    (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)


  		




  197
  225
  
    
    machine_code);


  		




  198
  226
  
    

  		




  199
  
  
    
  (* Checking the existence of a lusi (Lustre Interface file) *)


  		




  200
  
  
    
  let lusi_name = basename ^ ".lusi" in


  		




  201
  
  
    
  let _ = 


  		




  202
  
  
    
    try 


  		




  203
  
  
    
      let _ = open_in lusi_name in


  		




  204
  
  
    
      let _, declared_types_env, declared_clocks_env = load_lusi lusi_name in


  		




  205
  
  
    
      (* checking type compatibilty with computed types*)


  		




  206
  
  
    
      Typing.check_env_compat declared_types_env computed_types_env;


  		




  207
  
  
    
      (* checking clocks compatibilty with computed clocks*)


  		




  208
  
  
    
      Clock_calculus.check_env_compat declared_clocks_env computed_clocks_env;


  		




  209
  
  
    
      


  		




  210
  
  
    
    with Sys_error _ -> ( 


  		




  211
  
  
    
      (* Printing lusi file is necessary *)


  		




  212
  
  
    
      report ~level:1 


  		




  213
  
  
    
	(fun fmt -> 


  		




  214
  
  
    
	  fprintf fmt 


  		




  215
  
  
    
	    ".. generating lustre interface file %s@,@?" lusi_name);


  		




  216
  
  
    
      let lusi_out = open_out lusi_name in


  		




  217
  
  
    
      let lusi_fmt = formatter_of_out_channel lusi_out in


  		




  218
  
  
    
      Printers.pp_lusi_header lusi_fmt source_name normalized_prog


  		




  219
  
  
    
    )


  		




  220
  
  
    
    | (Types.Error (loc,err)) as exc ->


  		




  221
  
  
    
      Format.eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@]@."


  		




  222
  
  
    
	Types.pp_error err;


  		




  223
  
  
    
      raise exc


  		




  224
  
  
    
  in


  		




  225
  
  
    

  		




  226
  227
  
    
  (* Printing code *)


  		




  227
  
  
    
  let basename    = Filename.basename basename in


  		




  
  228
  
    
  let basename    =  Filename.basename basename in


  		




  228
  229
  
    
  let _ = match !Options.output with


  		




  229
  230
  
    
      "C" -> 


  		




  230
  231
  
    
	begin


  		




  231
  
  
    
	  let header_file = basename ^ ".h" in (* Could be changed *)


  		




  232
  
  
    
	  let source_file = basename ^ ".c" in (* Could be changed *)


  		




  233
  
  
    
	  let makefile_file = basename ^ ".makefile" in (* Could be changed *)


  		




  
  232
  
    
	  let destname = !Options.dest_dir ^ "/" ^ basename in


  		




  
  233
  
    
	  let header_file = destname ^ ".h" in (* Could be changed *)


  		




  
  234
  
    
	  let source_file = destname ^ ".c" in (* Could be changed *)


  		




  
  235
  
    
	  let makefile_file = destname ^ ".makefile" in (* Could be changed *)


  		




  234
  236
  
    
	  let spec_file_opt = if !Options.c_spec then 


  		




  235
  237
  
    
	      (


  		




  236
  238
  
    
		let spec_file = basename ^ "_spec.c" in


  		




  ......




  252
  254
  
    
	    | Some f -> Some (formatter_of_out_channel (open_out f))


  		




  253
  255
  
    
	  in


  		




  254
  256
  
    
	  report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,@?");


  		




  255
  
  
    
	  C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code;


  		




  
  257
  
    
	  C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code


  		




  256
  258
  
    
	end


  		




  257
  
  
    
    | "java" -> begin


  		




  258
  
  
    
      failwith "Sorry, but not yet supported !"


  		




  
  259
  
    
    | "java" ->


  		




  
  260
  
    
      begin


  		




  
  261
  
    
	failwith "Sorry, but not yet supported !"


  		




  259
  262
  
    
    (*let source_file = basename ^ ".java" in


  		




  260
  263
  
    
      report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);


  		




  261
  264
  
    
      let source_out = open_out source_file in


  		




  262
  265
  
    
      let source_fmt = formatter_of_out_channel source_out in


  		




  263
  266
  
    
      report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");


  		




  264
  267
  
    
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)


  		




  265
  
  
    
    end


  		




  266
  
  
    
    | "horn" -> begin


  		




  267
  
  
    
      let source_file = basename ^ ".smt2" in (* Could be changed *)


  		




  268
  
  
    
      let source_out = open_out source_file in


  		




  269
  
  
    
      let fmt = formatter_of_out_channel source_out in


  		




  270
  
  
    
      Horn_backend.translate fmt basename normalized_prog machine_code


  		




  271
  
  
    
    end


  		




  
  268
  
    
      end


  		




  
  269
  
    
    | "horn" ->


  		




  
  270
  
    
      begin


  		




  
  271
  
    
	let source_file = basename ^ ".smt2" in (* Could be changed *)


  		




  
  272
  
    
	let source_out = open_out source_file in


  		




  
  273
  
    
	let fmt = formatter_of_out_channel source_out in


  		




  
  274
  
    
	Horn_backend.translate fmt basename normalized_prog machine_code


  		




  
  275
  
    
      end


  		




  272
  276
  
    
    | _ -> assert false


  		




  273
  277
  
    
  in


  		




  274
  278
  
    
  report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");


  		












Also available in:  Unified diff