Project

General

Profile

Revision 01d48bb0 src/main_lustre_compiler.ml

View differences:

src/main_lustre_compiler.ml
76 76
      else
77 77
	begin
78 78
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
79
	  Lusic.check_lusic lusic destname;
79 80
	  let header = lusic.Lusic.contents in
80 81
	  let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
81 82
	  check_compatibility
......
104 105
  (* Sorting nodes *)
105 106
  let prog = SortProg.sort prog in
106 107

  
108
  (* Perform inlining before any analysis *)
109
  let orig, prog =
110
    if !Options.global_inline && !Options.main_node <> "" then
111
      (if !Options.witnesses then prog else []),
112
      Inliner.global_inline basename prog type_env clock_env
113
    else (* if !Option.has_local_inline *)
114
      [],
115
      Inliner.local_inline basename prog type_env clock_env
116
  in
117

  
118
  (* Checking stateless/stateful status *)
119
  check_stateless_decls prog;
120

  
107 121
  (* Typing *)
108 122
  let computed_types_env = type_decls type_env prog in
109 123

  
110 124
  (* Clock calculus *)
111 125
  let computed_clocks_env = clock_decls clock_env prog in
112 126

  
113
  (* Checking stateless/stateful status *)
114
  check_stateless_decls prog;
115

  
116 127
  (* Generating a .lusi header file only *)
117 128
  if !Options.lusi then
118 129
    begin
......
150 161
  Typing.uneval_prog_generics prog;
151 162
  Clock_calculus.uneval_prog_generics prog;
152 163

  
153
  (* Perform global inlining *)
154
  let prog =
155
    if !Options.global_inline &&
156
      (match !Options.main_node with | "" -> false | _ -> true) then
157
      Inliner.global_inline basename prog type_env clock_env
158
    else (* if !Option.has_local_inline *)
159
      Inliner.local_inline basename prog type_env clock_env
160
  in
164
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
165
    begin
166
      let orig = Corelang.copy_prog orig in
167
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file !@,");
168
      check_stateless_decls orig;
169
      let _ = Typing.type_prog type_env orig in
170
      let _ = Clock_calculus.clock_prog clock_env orig in
171
      Typing.uneval_prog_generics orig;
172
      Clock_calculus.uneval_prog_generics orig;
173
      Inliner.witness 
174
	basename
175
	!Options.main_node
176
	orig prog type_env clock_env;
177
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@,");
178
    end;
179

  
161 180
(*Format.eprintf "Inliner.global_inline<<@.%a@.>>@." Printers.pp_prog prog;*)
162 181
  (* Computes and stores generic calls for each node,
163 182
     only useful for ANSI C90 compliant generic node compilation *)
......
194 213
 *)
195 214
  let prog =
196 215
    if !Options.optimization >= 4 then
197
      Optimize_prog.prog_unfold_consts prog
216
      begin
217
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. constants elimination@,");
218
	Optimize_prog.prog_unfold_consts prog
219
      end
198 220
    else
199 221
      prog
200 222
  in
......
221 243
      end
222 244
    else
223 245
      machine_code
224
 in
246
  in
225 247
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
226 248
  (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
227 249
  machine_code);
......
230 252
  let basename    =  Filename.basename basename in
231 253
  let destname = !Options.dest_dir ^ "/" ^ basename in
232 254
  let _ = match !Options.output with
233
      "C" ->
234
	begin
255
    | "C" ->
256
      begin
235 257
	  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
236 258
	  let source_lib_file = destname ^ ".c" in (* Could be changed *)
237 259
	  let source_main_file = destname ^ "_main.c" in (* Could be changed *)

Also available in: Unified diff