Project

General

Profile

« Previous | Next » 

Revision 9c4624e4

Added by Teme Kahsai about 9 years ago

do not use lusi for horn, and some logging for horn

View differences:

src/main_lustre_compiler.ml
149 149
    raise exc
150 150
    end;
151 151
  *)
152
  
152

  
153 153
  (* Creating destination directory if needed *)
154 154
  create_dest_dir ();
155 155

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

  
161 166
  Typing.uneval_prog_generics prog;
162 167
  Clock_calculus.uneval_prog_generics prog;
......
170 175
      let _ = Clock_calculus.clock_prog clock_env orig in
171 176
      Typing.uneval_prog_generics orig;
172 177
      Clock_calculus.uneval_prog_generics orig;
173
      Inliner.witness 
178
      Inliner.witness
174 179
	basename
175 180
	!Options.main_node
176 181
	orig prog type_env clock_env
......
234 239
      machine_code
235 240
  in
236 241

  
237
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
242
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
238 243
  (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
239 244
  machine_code);
240 245

  
......
259 264
      machine_code
260 265
  in
261 266

  
267

  
262 268
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
263 269
  (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
264 270
  machine_code);
......
289 295
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
290 296
      end
291 297
    | "horn" ->
292
      begin
298
       begin
293 299
	let source_file = destname ^ ".smt2" in (* Could be changed *)
294 300
	let source_out = open_out source_file in
295 301
	let fmt = formatter_of_out_channel source_out in

Also available in: Unified diff