Project

General

Profile

« Previous | Next » 

Revision 782742b6

Added by Pierre-Loïc Garoche about 5 years ago

Merged unstable with seahorn

View differences:

src/main_lustre_compiler.ml
49 49
    Log.report ~level:1
50 50
      (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension));
51 51
    Lusic.write_lusic true header destname lusic_ext;
52
    Lusic.print_lusic_to_h destname lusic_ext;
52
    generate_lusic_header destname lusic_ext;
53 53
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.")
54 54
  end
55 55

  
......
59 59
  let destname = !Options.dest_dir ^ "/" ^ basename in
60 60
  let lusic_ext = extension ^ "c" in
61 61
  let header_name = destname ^ lusic_ext in
62
  begin
62
  let do_generate_lusic, lusic_opt =
63 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
64
      true, None
69 65
    else
70 66
      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
67
      not lusic.Lusic.from_lusi, Some lusic
68
  in
69
  if do_generate_lusic then
70
    begin
71
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
72
      Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
73
      generate_lusic_header destname lusic_ext
74
    end
75
  else
76
    begin
77
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
78
      let lusic = desome lusic_opt in
79
      Modules.check_dependency lusic destname;
80
      let header = lusic.Lusic.contents in
81
      let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
82
      check_compatibility
83
	(prog, computed_types_env, computed_clocks_env)
84
	(header, declared_types_env, declared_clocks_env)
85
    end
86
      
87
      
88
      
89
      (* begin *)
90
      (* 	if not (Sys.file_exists header_name) then *)
91
      (* 	  begin *)
92
      (* 	    Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); *)
93
      (* 	    Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; *)
94
      (* 	    Lusic.print_lusic_to_h destname lusic_ext *)
95
      (* 	  end *)
96
      (* 	else *)
97
      (* 	  let lusic = Lusic.read_lusic destname lusic_ext in *)
98
      (* 	  if not lusic.Lusic.from_lusi then *)
99
      (* 	    begin *)
100
      (* 	      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); *)
101
      (*  	      Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; *)
102
      (* 	      (\*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*\) *)
103
      (* 	      Lusic.print_lusic_to_h destname lusic_ext *)
104
      (* 	    end *)
105
      (* 	  else *)
106
      (* 	    begin *)
107
      (* 	      Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name); *)
108
      (* 	      Modules.check_dependency lusic destname; *)
109
      (* 	      let header = lusic.Lusic.contents in *)
110
      (* 	      let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in *)
111
      (* 	      check_compatibility *)
112
      (* 		(prog, computed_types_env, computed_clocks_env) *)
113
      (* 		(header, declared_types_env, declared_clocks_env) *)
114
      (* 	    end *)
115
      (* end *)
89 116

  
90 117

  
91 118

  
......
215 242
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
216 243
  (* Special treatment of arrows in lustre backend. We want to keep them *)
217 244
  if !Options.output = "lustre" then
218
    Normalization.unfold_arrow_active := false;
245
    Normalization_common.unfold_arrow_active := false;
219 246
  let prog = Normalization.normalize_prog prog in
220 247
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
221 248

  

Also available in: Unified diff