1 |
e2068500
|
Temesghen Kahsai
|
(********************************************************************)
|
2 |
|
|
(* *)
|
3 |
|
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4 |
|
|
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
|
5 |
|
|
(* *)
|
6 |
|
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7 |
|
|
(* under the terms of the GNU Lesser General Public License *)
|
8 |
|
|
(* version 2.1. *)
|
9 |
|
|
(* *)
|
10 |
|
|
(********************************************************************)
|
11 |
|
|
|
12 |
|
|
open Utils
|
13 |
|
|
open Format
|
14 |
|
|
open LustreSpec
|
15 |
|
|
open Corelang
|
16 |
|
|
|
17 |
|
|
let create_dest_dir () =
|
18 |
|
|
begin
|
19 |
|
|
if not (Sys.file_exists !Options.dest_dir) then
|
20 |
|
|
begin
|
21 |
|
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. creating destination directory@,");
|
22 |
|
|
Unix.mkdir !Options.dest_dir (Unix.stat ".").Unix.st_perm
|
23 |
|
|
end;
|
24 |
|
|
if (Unix.stat !Options.dest_dir).Unix.st_kind <> Unix.S_DIR then
|
25 |
|
|
begin
|
26 |
|
|
eprintf "Failure: destination %s is not a directory.@.@." !Options.dest_dir;
|
27 |
|
|
exit 1
|
28 |
|
|
end
|
29 |
|
|
end
|
30 |
|
|
|
31 |
|
|
(* Loading Lusi file and filling type tables with parsed
|
32 |
|
|
functions/nodes *)
|
33 |
|
|
let parse_header own filename =
|
34 |
|
|
Location.set_input filename;
|
35 |
|
|
let h_in = open_in filename in
|
36 |
|
|
let lexbuf = Lexing.from_channel h_in in
|
37 |
|
|
Location.init lexbuf filename;
|
38 |
|
|
(* Parsing *)
|
39 |
|
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. parsing header file %s@ " filename);
|
40 |
|
|
try
|
41 |
|
|
let header = Parse.header Parser_lustre.header Lexer_lustre.token lexbuf in
|
42 |
|
|
(*ignore (Modules.load_header ISet.empty header);*)
|
43 |
|
|
close_in h_in;
|
44 |
|
|
header
|
45 |
|
|
with
|
46 |
|
|
| (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc ->
|
47 |
|
|
Parse.report_error err;
|
48 |
|
|
raise exc
|
49 |
|
|
| Corelang.Error (loc, err) as exc -> (
|
50 |
|
|
eprintf "Parsing error: %a%a@."
|
51 |
|
|
Corelang.pp_error err
|
52 |
|
|
Location.pp_loc loc;
|
53 |
|
|
raise exc
|
54 |
|
|
)
|
55 |
|
|
|
56 |
|
|
let parse_source source_name =
|
57 |
|
|
(* Loading the input file *)
|
58 |
|
|
Location.set_input source_name;
|
59 |
|
|
let s_in = open_in source_name in
|
60 |
|
|
let lexbuf = Lexing.from_channel s_in in
|
61 |
|
|
Location.init lexbuf source_name;
|
62 |
|
|
|
63 |
|
|
(* Parsing *)
|
64 |
|
|
Log.report ~level:1
|
65 |
|
|
(fun fmt -> fprintf fmt ".. parsing source file %s@," source_name);
|
66 |
|
|
try
|
67 |
|
|
let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in
|
68 |
|
|
(*ignore (Modules.load_program ISet.empty prog);*)
|
69 |
|
|
close_in s_in;
|
70 |
|
|
prog
|
71 |
|
|
with
|
72 |
|
|
| (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc ->
|
73 |
|
|
Parse.report_error err;
|
74 |
|
|
raise exc
|
75 |
|
|
| Corelang.Error (loc, err) as exc ->
|
76 |
d50b0dc0
|
Temesghen Kahsai
|
eprintf "Parsing error: %a%a@."
|
77 |
e2068500
|
Temesghen Kahsai
|
Corelang.pp_error err
|
78 |
|
|
Location.pp_loc loc;
|
79 |
|
|
raise exc
|
80 |
|
|
|
81 |
|
|
let check_stateless_decls decls =
|
82 |
|
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking stateless/stateful status@ ");
|
83 |
|
|
try
|
84 |
|
|
Stateless.check_prog decls
|
85 |
|
|
with (Stateless.Error (loc, err)) as exc ->
|
86 |
d50b0dc0
|
Temesghen Kahsai
|
eprintf "Stateless status error: %a%a@."
|
87 |
e2068500
|
Temesghen Kahsai
|
Stateless.pp_error err
|
88 |
|
|
Location.pp_loc loc;
|
89 |
|
|
raise exc
|
90 |
|
|
|
91 |
|
|
let type_decls env decls =
|
92 |
|
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ ");
|
93 |
|
|
let new_env =
|
94 |
|
|
begin
|
95 |
|
|
try
|
96 |
|
|
Typing.type_prog env decls
|
97 |
|
|
with (Types.Error (loc,err)) as exc ->
|
98 |
d50b0dc0
|
Temesghen Kahsai
|
eprintf "Typing error: %a%a@."
|
99 |
e2068500
|
Temesghen Kahsai
|
Types.pp_error err
|
100 |
|
|
Location.pp_loc loc;
|
101 |
|
|
raise exc
|
102 |
|
|
end
|
103 |
|
|
in
|
104 |
|
|
if !Options.print_types then
|
105 |
|
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_type decls);
|
106 |
|
|
new_env
|
107 |
|
|
|
108 |
|
|
let clock_decls env decls =
|
109 |
|
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@ ");
|
110 |
|
|
let new_env =
|
111 |
|
|
begin
|
112 |
|
|
try
|
113 |
|
|
Clock_calculus.clock_prog env decls
|
114 |
|
|
with (Clocks.Error (loc,err)) as exc ->
|
115 |
d50b0dc0
|
Temesghen Kahsai
|
eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc;
|
116 |
e2068500
|
Temesghen Kahsai
|
raise exc
|
117 |
|
|
end
|
118 |
|
|
in
|
119 |
|
|
if !Options.print_clocks then
|
120 |
|
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_clock decls);
|
121 |
|
|
new_env
|
122 |
|
|
|
123 |
|
|
let check_top_decls header =
|
124 |
|
|
let new_tenv = type_decls Basic_library.type_env header in (* Typing *)
|
125 |
|
|
let new_cenv = clock_decls Basic_library.clock_env header in (* Clock calculus *)
|
126 |
|
|
header, new_tenv, new_cenv
|
127 |
|
|
|
128 |
|
|
let get_envs_from_const const_decl (ty_env, ck_env) =
|
129 |
|
|
(Env.add_value ty_env const_decl.const_id const_decl.const_type,
|
130 |
|
|
Env.add_value ck_env const_decl.const_id (Clocks.new_var true))
|
131 |
|
|
|
132 |
|
|
let get_envs_from_consts const_decls (ty_env, ck_env) =
|
133 |
|
|
List.fold_right get_envs_from_const const_decls (ty_env, ck_env)
|
134 |
|
|
|
135 |
|
|
let rec get_envs_from_top_decl (ty_env, ck_env) top_decl =
|
136 |
|
|
match top_decl.top_decl_desc with
|
137 |
|
|
| Node nd -> (Env.add_value ty_env nd.node_id nd.node_type,
|
138 |
|
|
Env.add_value ck_env nd.node_id nd.node_clock)
|
139 |
|
|
| ImportedNode ind -> (Env.add_value ty_env ind.nodei_id ind.nodei_type,
|
140 |
|
|
Env.add_value ck_env ind.nodei_id ind.nodei_clock)
|
141 |
|
|
| Const c -> get_envs_from_const c (ty_env, ck_env)
|
142 |
|
|
| TypeDef _ -> List.fold_left get_envs_from_top_decl (ty_env, ck_env) (consts_of_enum_type top_decl)
|
143 |
|
|
| Open _ -> (ty_env, ck_env)
|
144 |
|
|
|
145 |
|
|
(* get type and clock environments from a header *)
|
146 |
|
|
let get_envs_from_top_decls header =
|
147 |
|
|
List.fold_left get_envs_from_top_decl (Env.initial, Env.initial) header
|
148 |
|
|
|
149 |
|
|
(*
|
150 |
|
|
List.fold_right
|
151 |
|
|
(fun top_decl (ty_env, ck_env) ->
|
152 |
|
|
match top_decl.top_decl_desc with
|
153 |
|
|
| Node nd -> (Env.add_value ty_env nd.node_id nd.node_type,
|
154 |
|
|
Env.add_value ck_env nd.node_id nd.node_clock)
|
155 |
|
|
| ImportedNode ind -> (Env.add_value ty_env ind.nodei_id ind.nodei_type,
|
156 |
|
|
Env.add_value ck_env ind.nodei_id ind.nodei_clock)
|
157 |
|
|
| Const c -> get_envs_from_const c (ty_env, ck_env)
|
158 |
|
|
| TypeDef _ -> List.fold_left (fun envs top -> consts_of_enum_type top_decl
|
159 |
|
|
| Open _ -> (ty_env, ck_env))
|
160 |
|
|
header
|
161 |
|
|
(Env.initial, Env.initial)
|
162 |
|
|
*)
|
163 |
|
|
|
164 |
|
|
let check_compatibility (prog, computed_types_env, computed_clocks_env) (header, declared_types_env, declared_clocks_env) =
|
165 |
|
|
try
|
166 |
|
|
(* checking defined types are compatible with declared types*)
|
167 |
|
|
Typing.check_typedef_compat header;
|
168 |
|
|
|
169 |
|
|
(* checking type compatibility with computed types*)
|
170 |
|
|
Typing.check_env_compat header declared_types_env computed_types_env;
|
171 |
|
|
|
172 |
|
|
(* checking clocks compatibility with computed clocks*)
|
173 |
|
|
Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;
|
174 |
|
|
|
175 |
|
|
(* checking stateless status compatibility *)
|
176 |
|
|
Stateless.check_compat header
|
177 |
|
|
with
|
178 |
|
|
| (Types.Error (loc,err)) as exc ->
|
179 |
d50b0dc0
|
Temesghen Kahsai
|
eprintf "Type mismatch between computed type and declared type in lustre interface file: %a%a@."
|
180 |
|
|
Types.pp_error err
|
181 |
|
|
Location.pp_loc loc;
|
182 |
e2068500
|
Temesghen Kahsai
|
raise exc
|
183 |
|
|
| Clocks.Error (loc, err) as exc ->
|
184 |
d50b0dc0
|
Temesghen Kahsai
|
eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a%a@."
|
185 |
|
|
Clocks.pp_error err
|
186 |
|
|
Location.pp_loc loc;
|
187 |
e2068500
|
Temesghen Kahsai
|
raise exc
|
188 |
|
|
| Stateless.Error (loc, err) as exc ->
|
189 |
d50b0dc0
|
Temesghen Kahsai
|
eprintf "Stateless status mismatch between defined status and declared status in lustre interface file: %a%a@."
|
190 |
|
|
Stateless.pp_error err
|
191 |
|
|
Location.pp_loc loc;
|
192 |
e2068500
|
Temesghen Kahsai
|
raise exc
|
193 |
|
|
|
194 |
|
|
let is_stateful topdecl =
|
195 |
|
|
match topdecl.top_decl_desc with
|
196 |
|
|
| Node nd -> (match nd.node_stateless with Some b -> not b | None -> not nd.node_dec_stateless)
|
197 |
|
|
| ImportedNode nd -> not nd.nodei_stateless
|
198 |
|
|
| _ -> false
|
199 |
|
|
|
200 |
|
|
|
201 |
|
|
let import_dependencies prog =
|
202 |
|
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting dependencies@,");
|
203 |
|
|
let dependencies = Corelang.get_dependencies prog in
|
204 |
|
|
let deps =
|
205 |
|
|
List.fold_left
|
206 |
|
|
(fun (compilation_dep, type_env, clock_env) dep ->
|
207 |
|
|
let (local, s) = Corelang.dependency_of_top dep in
|
208 |
|
|
let basename = Modules.name_dependency (local, s) in
|
209 |
|
|
Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0>Library %s@," basename);
|
210 |
|
|
let lusic = Modules.import_dependency dep.top_decl_loc (local, s) in
|
211 |
|
|
Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]@ ");
|
212 |
|
|
let (lusi_type_env, lusi_clock_env) = get_envs_from_top_decls lusic.Lusic.contents in
|
213 |
|
|
let is_stateful = List.exists is_stateful lusic.Lusic.contents in
|
214 |
|
|
let new_dep = Dep (local, s, lusic.Lusic.contents, is_stateful ) in
|
215 |
|
|
new_dep::compilation_dep,
|
216 |
|
|
Env.overwrite type_env lusi_type_env,
|
217 |
|
|
Env.overwrite clock_env lusi_clock_env)
|
218 |
|
|
([], Basic_library.type_env, Basic_library.clock_env)
|
219 |
|
|
dependencies in
|
220 |
|
|
begin
|
221 |
|
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
|
222 |
|
|
deps
|
223 |
|
|
end
|