Project

General

Profile

Revision 7ecfca04 src/main_lustre_compiler.ml

View differences:

src/main_lustre_compiler.ml
22 22

  
23 23
let extensions = [".ec"; ".lus"; ".lusi"]
24 24

  
25
let check_stateless_decls decls =
26
  report ~level:1 (fun fmt -> fprintf fmt ".. checking stateless/stateful status@,@?");
27
  try
28
    Stateless.check_prog decls
29
  with (Stateless.Error (loc, err)) as exc ->
30
    Format.eprintf "Stateless status error at loc %a: %a@]@."
31
      Location.pp_loc loc
32
      Stateless.pp_error err;
33
    raise exc
25
(* print a .lusi header file from a source prog *)
26
let print_lusi prog dirname basename extension =
27
  let header = Lusic.extract_header dirname basename prog in
28
  let header_name = dirname ^ "/" ^ basename ^ extension in
29
  let h_out = open_out header_name in
30
  let h_fmt = formatter_of_out_channel h_out in
31
  begin
32
    Typing.uneval_prog_generics header;
33
    Clock_calculus.uneval_prog_generics header;
34
    Printers.pp_lusi_header h_fmt basename header;
35
    close_out h_out
36
  end
37

  
38
(* compile a .lusi header file *)
39
let compile_header dirname  basename extension =
40
  let destname = !Options.dest_dir ^ "/" ^ basename in
41
  let header_name = basename ^ extension in
42
  let lusic_ext = extension ^ "c" in
43
  begin
44
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
45
    let header = parse_header true (dirname ^ "/" ^ header_name) in
46
    ignore (Modules.load_header ISet.empty header);
47
    ignore (check_top_decls header);
48
    create_dest_dir ();
49
    Log.report ~level:1
50
      (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension));
51
    Lusic.write_lusic true header destname lusic_ext;
52
    Lusic.print_lusic_to_h destname lusic_ext;
53
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.")
54
  end
55

  
56
(* check whether a source file has a compiled header,
57
   if not, generate the compiled header *)
58
let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
59
  let destname = !Options.dest_dir ^ "/" ^ basename in
60
  let lusic_ext = extension ^ "c" in
61
  let header_name = destname ^ lusic_ext in
62
  begin
63
    if not (Sys.file_exists header_name) then
64
      begin
65
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
66
	Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
67
	Lusic.print_lusic_to_h destname lusic_ext
68
      end
69
    else
70
      let lusic = Lusic.read_lusic destname lusic_ext in
71
      if not lusic.Lusic.from_lusi then
72
	begin
73
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
74
       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
75
	  (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
76
	  Lusic.print_lusic_to_h destname lusic_ext
77
	end
78
      else
79
	begin
80
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
81
	  Modules.check_dependency lusic destname;
82
	  let header = lusic.Lusic.contents in
83
	  let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
84
	  check_compatibility
85
	    (prog, computed_types_env, computed_clocks_env)
86
	    (header, declared_types_env, declared_clocks_env)
87
	end
88
  end
89

  
90

  
91
let functional_backend () = 
92
  match !Options.output with
93
  | "horn" | "lustre" | "acsl" -> true
94
  | _ -> false
95

  
96
(* From prog to prog *)
97
let stage1 prog dirname basename =
98
  (* Removing automata *) 
99
  let prog = expand_automata prog in
100

  
101
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);
102

  
103
  (* Importing source *)
104
  let _ = Modules.load_program ISet.empty prog in
34 105

  
35
let type_decls env decls =  
36
  report ~level:1 (fun fmt -> fprintf fmt ".. typing@,@?");
37
  let new_env = 
38
    begin
39
      try
40
	Typing.type_prog env decls
41
      with (Types.Error (loc,err)) as exc ->
42
	Format.eprintf "Typing error at loc %a: %a@]@."
43
	  Location.pp_loc loc
44
	  Types.pp_error err;
45
	raise exc
46
    end 
47
  in
48
  if !Options.print_types then
49
    report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Corelang.pp_prog_type decls);
50
  new_env
51
      
52
let clock_decls env decls = 
53
  report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@,@?");
54
  let new_env =
55
    begin
56
      try
57
	Clock_calculus.clock_prog env decls
58
      with (Clocks.Error (loc,err)) as exc ->
59
	Location.print loc;
60
	eprintf "Clock calculus error at loc %a: %a@]@." Location.pp_loc loc Clocks.pp_error err;
61
	raise exc
62
    end
63
  in
64
  if !Options.print_clocks then
65
    report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Corelang.pp_prog_clock decls);
66
  new_env
67

  
68
(* Loading Lusi file and filling type tables with parsed
69
   functions/nodes *)
70
let load_lusi own filename =
71
  Location.input_name := filename;
72
  let lexbuf = Lexing.from_channel (open_in filename) in
73
  Location.init lexbuf filename;
74
  (* Parsing *)
75
  report ~level:1 (fun fmt -> fprintf fmt "@[<v>.. parsing header file %s@,@?" filename);
76
  try
77
    Parse.header own Parser_lustre.header Lexer_lustre.token lexbuf
78
  with
79
  | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> 
80
    Parse.report_error err;
81
    raise exc
82
  | Corelang.Error (loc, err) as exc ->
83
     Format.eprintf "Parsing error at loc %a: %a@]@."
84
       Location.pp_loc loc
85
       Corelang.pp_error err;
86
     raise exc
87

  
88
let check_lusi header =
89
  let new_tenv = type_decls Basic_library.type_env header in   (* Typing *)
90
  let new_cenv = clock_decls Basic_library.clock_env header in   (* Clock calculus *)
91
  header, new_tenv, new_cenv
92
    
93
let rec compile basename extension =
94
  (* Loading the input file *)
95
  let source_name = basename^extension in
96
  Location.input_name := source_name;
97
  let lexbuf = Lexing.from_channel (open_in source_name) in
98
  Location.init lexbuf source_name;
99
  (* Parsing *)
100
  report ~level:1 
101
    (fun fmt -> fprintf fmt "@[<v>.. parsing file %s@,@?" source_name);
102
  let prog =
103
    try
104
      Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf
105
    with
106
    | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> 
107
      Parse.report_error err;
108
      raise exc
109
    | Corelang.Error (loc, err) as exc ->
110
      Format.eprintf "Parsing error at loc %a: %a@]@."
111
	Location.pp_loc loc
112
	Corelang.pp_error err;
113
      raise exc
114
  in
115 106
  (* Extracting dependencies *)
116 107
  let dependencies, type_env, clock_env = import_dependencies prog in
117 108

  

Also available in: Unified diff