Revision 01d48bb0
src/automata.ml | ||
---|---|---|
24 | 24 |
actual_s : var_decl |
25 | 25 |
} |
26 | 26 |
|
27 |
let cpvar_decl var_decl = |
|
28 |
mkvar_decl var_decl.var_loc ~orig:var_decl.var_orig (var_decl.var_id, var_decl.var_dec_type, var_decl.var_dec_clock, var_decl.var_dec_const, var_decl.var_dec_value) |
|
29 |
|
|
27 | 30 |
let as_clock var_decl = |
28 | 31 |
let tydec = var_decl.var_dec_type in |
29 | 32 |
{ var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } } |
... | ... | |
99 | 102 |
let actual_r = mk_new_name used (id ^ "__restart_act") in |
100 | 103 |
let actual_s = mk_new_name used (id ^ "__state_act") in |
101 | 104 |
{ |
102 |
incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false); |
|
103 |
incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false); |
|
104 |
incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false); |
|
105 |
incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false); |
|
106 |
actual_r = mkvar_decl loc (actual_r , tydec_bool, ckdec_any, false); |
|
107 |
actual_s = mkvar_decl loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false) |
|
105 |
incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None);
|
|
106 |
incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None);
|
|
107 |
incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None);
|
|
108 |
incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None);
|
|
109 |
actual_r = mkvar_decl loc (actual_r , tydec_bool, ckdec_any, false, None);
|
|
110 |
actual_s = mkvar_decl loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false, None)
|
|
108 | 111 |
} |
109 | 112 |
|
110 | 113 |
let vars_of_aut_state aut_state = |
... | ... | |
123 | 126 |
node_id = node_id; |
124 | 127 |
node_type = Types.new_var (); |
125 | 128 |
node_clock = Clocks.new_var true; |
126 |
node_inputs = var_inputs; |
|
127 |
node_outputs = var_outputs; |
|
129 |
node_inputs = List.map cpvar_decl var_inputs;
|
|
130 |
node_outputs = List.map cpvar_decl var_outputs;
|
|
128 | 131 |
node_locals = []; |
129 | 132 |
node_gencalls = []; |
130 | 133 |
node_checks = []; |
... | ... | |
173 | 176 |
node_id = node_id; |
174 | 177 |
node_type = Types.new_var (); |
175 | 178 |
node_clock = Clocks.new_var true; |
176 |
node_inputs = var_inputs; |
|
177 |
node_outputs = aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs;
|
|
178 |
node_locals = new_var_locals @ handler.hand_locals;
|
|
179 |
node_inputs = List.map cpvar_decl var_inputs;
|
|
180 |
node_outputs = List.map cpvar_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
|
|
181 |
node_locals = List.map cpvar_decl (new_var_locals @ handler.hand_locals);
|
|
179 | 182 |
node_gencalls = []; |
180 | 183 |
node_checks = []; |
181 | 184 |
node_asserts = handler.hand_asserts; |
src/backends/C/c_backend.ml | ||
---|---|---|
26 | 26 |
*) |
27 | 27 |
|
28 | 28 |
let gen_files funs basename prog machines dependencies header_file source_lib_file source_main_file makefile_file machines = |
29 |
|
|
29 | 30 |
let header_out = open_out header_file in |
30 | 31 |
let header_fmt = formatter_of_out_channel header_out in |
31 | 32 |
let source_lib_out = open_out source_lib_file in |
32 | 33 |
let source_lib_fmt = formatter_of_out_channel source_lib_out in |
33 |
|
|
34 |
|
|
34 | 35 |
let print_header, print_lib_c, print_main_c, print_makefile = funs in |
35 | 36 |
(* Generating H file *) |
36 | 37 |
print_header header_fmt basename prog machines dependencies; |
37 |
|
|
38 |
|
|
38 | 39 |
(* Generating Lib C file *) |
39 | 40 |
print_lib_c source_lib_fmt basename prog machines dependencies; |
40 |
|
|
41 |
|
|
41 | 42 |
close_out header_out; |
42 | 43 |
close_out source_lib_out; |
43 | 44 |
|
... | ... | |
64 | 65 |
end |
65 | 66 |
) |
66 | 67 |
|
67 |
let translate_to_c header source_lib source_main makefile basename prog machines dependencies = |
|
68 |
|
|
68 |
let translate_to_c header source_lib source_main makefile basename prog machines dependencies = |
|
69 | 69 |
match !Options.spec with |
70 | 70 |
| "no" -> begin |
71 | 71 |
let module HeaderMod = C_backend_header.EmptyMod in |
... | ... | |
77 | 77 |
let module Source = C_backend_src.Main (SourceMod) in |
78 | 78 |
let module SourceMain = C_backend_main.Main (SourceMainMod) in |
79 | 79 |
let module Makefile = C_backend_makefile.Main (MakefileMod) in |
80 |
|
|
80 |
|
|
81 | 81 |
let funs = |
82 | 82 |
Header.print_alloc_header, |
83 | 83 |
Source.print_lib_c, |
... | ... | |
100 | 100 |
let module Source = C_backend_src.Main (SourceMod) in |
101 | 101 |
let module SourceMain = C_backend_main.Main (SourceMainMod) in |
102 | 102 |
let module Makefile = C_backend_makefile.Main (MakefileMod) in |
103 |
|
|
103 |
|
|
104 | 104 |
let funs = |
105 | 105 |
Header.print_alloc_header, |
106 | 106 |
Source.print_lib_c, |
src/backends/C/c_backend_common.ml | ||
---|---|---|
51 | 51 |
var_dec_type = mktyp Location.dummy_loc Tydec_any; |
52 | 52 |
var_dec_clock = mkclock Location.dummy_loc Ckdec_any; |
53 | 53 |
var_dec_const = false; |
54 |
var_dec_value = None; |
|
54 | 55 |
var_type = Type_predef.type_arrow (Types.new_var ()) (Types.new_var ()); |
55 | 56 |
var_clock = Clocks.new_var true; |
56 | 57 |
var_loc = loc } |
... | ... | |
133 | 134 |
(Utils.duplicate 0 (Dimension.size_const_dimension d)) |
134 | 135 |
| _ -> assert false |
135 | 136 |
|
137 |
|
|
138 |
let pp_c_tag fmt t = |
|
139 |
pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t) |
|
140 |
|
|
141 |
(* Prints a constant value *) |
|
142 |
let rec pp_c_const fmt c = |
|
143 |
match c with |
|
144 |
| Const_int i -> pp_print_int fmt i |
|
145 |
| Const_real r -> pp_print_string fmt r |
|
146 |
| Const_float r -> pp_print_float fmt r |
|
147 |
| Const_tag t -> pp_c_tag fmt t |
|
148 |
| Const_array ca -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca |
|
149 |
| Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl |
|
150 |
| Const_string _ -> assert false (* string occurs in annotations not in C *) |
|
151 |
|
|
152 |
(* Prints a value expression [v], with internal function calls only. |
|
153 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
|
154 |
but an offset suffix may be added for array variables |
|
155 |
*) |
|
156 |
let rec pp_c_val self pp_var fmt v = |
|
157 |
match v with |
|
158 |
| Cst c -> pp_c_const fmt c |
|
159 |
| Array vl -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl |
|
160 |
| Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i |
|
161 |
| Power (v, n) -> assert false |
|
162 |
| LocalVar v -> pp_var fmt v |
|
163 |
| StateVar v -> |
|
164 |
(* array memory vars are represented by an indirection to a local var with the right type, |
|
165 |
in order to avoid casting everywhere. *) |
|
166 |
if Types.is_array_type v.var_type |
|
167 |
then fprintf fmt "%a" pp_var v |
|
168 |
else fprintf fmt "%s->_reg.%a" self pp_var v |
|
169 |
| Fun (n, vl) -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl |
|
170 |
|
|
171 |
(* Access to the value of a variable: |
|
172 |
- if it's not a scalar output, then its name is enough |
|
173 |
- otherwise, dereference it (it has been declared as a pointer, |
|
174 |
despite its scalar Lustre type) |
|
175 |
- moreover, dereference memory array variables. |
|
176 |
*) |
|
177 |
let pp_c_var_read m fmt id = |
|
178 |
if Types.is_address_type id.var_type |
|
179 |
then |
|
180 |
if is_memory m id |
|
181 |
then fprintf fmt "(*%s)" id.var_id |
|
182 |
else fprintf fmt "%s" id.var_id |
|
183 |
else |
|
184 |
if is_output m id |
|
185 |
then fprintf fmt "*%s" id.var_id |
|
186 |
else fprintf fmt "%s" id.var_id |
|
187 |
|
|
188 |
(* Addressable value of a variable, the one that is passed around in calls: |
|
189 |
- if it's not a scalar non-output, then its name is enough |
|
190 |
- otherwise, reference it (it must be passed as a pointer, |
|
191 |
despite its scalar Lustre type) |
|
192 |
*) |
|
193 |
let pp_c_var_write m fmt id = |
|
194 |
if Types.is_address_type id.var_type |
|
195 |
then |
|
196 |
fprintf fmt "%s" id.var_id |
|
197 |
else |
|
198 |
if is_output m id |
|
199 |
then |
|
200 |
fprintf fmt "%s" id.var_id |
|
201 |
else |
|
202 |
fprintf fmt "&%s" id.var_id |
|
203 |
|
|
136 | 204 |
(* Declaration of an input variable: |
137 | 205 |
- if its type is array/matrix/etc, then declare it as a mere pointer, |
138 | 206 |
in order to cope with unknown/parametric array dimensions, |
... | ... | |
159 | 227 |
known in order to statically allocate memory, |
160 | 228 |
so we print the full type |
161 | 229 |
*) |
162 |
let pp_c_decl_local_var fmt id = |
|
163 |
pp_c_type id.var_id fmt id.var_type |
|
230 |
let pp_c_decl_local_var m fmt id = |
|
231 |
if id.var_dec_const |
|
232 |
then |
|
233 |
Format.fprintf fmt "%a = %a" |
|
234 |
(pp_c_type id.var_id) id.var_type |
|
235 |
(pp_c_val "" (pp_c_var_read m)) (get_const_assign m id) |
|
236 |
else |
|
237 |
Format.fprintf fmt "%a" |
|
238 |
(pp_c_type id.var_id) id.var_type |
|
164 | 239 |
|
165 | 240 |
let pp_c_decl_array_mem self fmt id = |
166 | 241 |
fprintf fmt "%a = (%a) (%s->_reg.%s)" |
... | ... | |
177 | 252 |
then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type) |
178 | 253 |
else pp_c_type id.var_id fmt id.var_type |
179 | 254 |
|
180 |
(* Access to the value of a variable: |
|
181 |
- if it's not a scalar output, then its name is enough |
|
182 |
- otherwise, dereference it (it has been declared as a pointer, |
|
183 |
despite its scalar Lustre type) |
|
184 |
- moreover, dereference memory array variables. |
|
185 |
*) |
|
186 |
let pp_c_var_read m fmt id = |
|
187 |
if Types.is_address_type id.var_type |
|
188 |
then |
|
189 |
if is_memory m id |
|
190 |
then fprintf fmt "(*%s)" id.var_id |
|
191 |
else fprintf fmt "%s" id.var_id |
|
192 |
else |
|
193 |
if is_output m id |
|
194 |
then fprintf fmt "*%s" id.var_id |
|
195 |
else fprintf fmt "%s" id.var_id |
|
196 |
|
|
197 |
(* Addressable value of a variable, the one that is passed around in calls: |
|
198 |
- if it's not a scalar non-output, then its name is enough |
|
199 |
- otherwise, reference it (it must be passed as a pointer, |
|
200 |
despite its scalar Lustre type) |
|
201 |
*) |
|
202 |
let pp_c_var_write m fmt id = |
|
203 |
if Types.is_address_type id.var_type |
|
204 |
then |
|
205 |
fprintf fmt "%s" id.var_id |
|
206 |
else |
|
207 |
if is_output m id |
|
208 |
then |
|
209 |
fprintf fmt "%s" id.var_id |
|
210 |
else |
|
211 |
fprintf fmt "&%s" id.var_id |
|
212 |
|
|
213 | 255 |
let pp_c_decl_instance_var fmt (name, (node, static)) = |
214 | 256 |
fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name |
215 | 257 |
|
216 |
let pp_c_tag fmt t = |
|
217 |
pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t) |
|
218 |
|
|
219 |
(* Prints a constant value *) |
|
220 |
let rec pp_c_const fmt c = |
|
221 |
match c with |
|
222 |
| Const_int i -> pp_print_int fmt i |
|
223 |
| Const_real r -> pp_print_string fmt r |
|
224 |
| Const_float r -> pp_print_float fmt r |
|
225 |
| Const_tag t -> pp_c_tag fmt t |
|
226 |
| Const_array ca -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca |
|
227 |
| Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl |
|
228 |
| Const_string _ -> assert false (* string occurs in annotations not in C *) |
|
229 |
|
|
230 |
(* Prints a value expression [v], with internal function calls only. |
|
231 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
|
232 |
but an offset suffix may be added for array variables |
|
233 |
*) |
|
234 |
let rec pp_c_val self pp_var fmt v = |
|
235 |
match v with |
|
236 |
| Cst c -> pp_c_const fmt c |
|
237 |
| Array vl -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl |
|
238 |
| Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i |
|
239 |
| Power (v, n) -> assert false |
|
240 |
| LocalVar v -> pp_var fmt v |
|
241 |
| StateVar v -> |
|
242 |
(* array memory vars are represented by an indirection to a local var with the right type, |
|
243 |
in order to avoid casting everywhere. *) |
|
244 |
if Types.is_array_type v.var_type |
|
245 |
then fprintf fmt "%a" pp_var v |
|
246 |
else fprintf fmt "%s->_reg.%a" self pp_var v |
|
247 |
| Fun (n, vl) -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl |
|
248 |
|
|
249 | 258 |
let pp_c_checks self fmt m = |
250 | 259 |
Utils.fprintf_list ~sep:"" |
251 | 260 |
(fun fmt (loc, check) -> |
src/backends/C/c_backend_header.ml | ||
---|---|---|
36 | 36 |
let print_import_standard fmt = |
37 | 37 |
fprintf fmt "#include \"%s/arrow.h\"@.@." Version.include_path |
38 | 38 |
|
39 |
let print_static_declare_instance attr fmt (i, (m, static)) = |
|
39 |
let rec print_static_val pp_var fmt v = |
|
40 |
match v with |
|
41 |
| Cst c -> pp_c_const fmt c |
|
42 |
| LocalVar v -> pp_var fmt v |
|
43 |
| Fun (n, vl) -> Basic_library.pp_c n (print_static_val pp_var) fmt vl |
|
44 |
| _ -> (Format.eprintf "Internal error: C_backend_header.print_static_val"; assert false) |
|
45 |
|
|
46 |
let print_constant m pp_var fmt v = |
|
47 |
Format.fprintf fmt "inst ## %s = %a" |
|
48 |
v.var_id |
|
49 |
(print_static_val pp_var) (Machine_code.get_const_assign m v) |
|
50 |
|
|
51 |
let print_static_constant (m, attr, inst) fmt const_locals = |
|
52 |
let pp_var fmt v = |
|
53 |
if List.mem v const_locals |
|
54 |
then |
|
55 |
Format.fprintf fmt "%s ## %s" inst v.var_id |
|
56 |
else |
|
57 |
Format.fprintf fmt "%s" v.var_id in |
|
58 |
Format.fprintf fmt "%a%t" |
|
59 |
(Utils.fprintf_list ~sep:";\\@," (print_constant m pp_var)) const_locals |
|
60 |
(Utils.pp_final_char_if_non_empty ";\\@," const_locals) |
|
61 |
|
|
62 |
let print_static_declare_instance (m, attr, inst) const_locals fmt (i, (n, static)) = |
|
63 |
let pp_var fmt v = |
|
64 |
if List.mem v const_locals |
|
65 |
then |
|
66 |
Format.fprintf fmt "%s ## %s" inst v.var_id |
|
67 |
else |
|
68 |
Format.fprintf fmt "%s" v.var_id in |
|
69 |
let values = List.map (Machine_code.value_of_dimension m) static in |
|
40 | 70 |
fprintf fmt "%a(%s, %a%t%s)" |
41 |
pp_machine_static_declare_name (node_name m)
|
|
71 |
pp_machine_static_declare_name (node_name n)
|
|
42 | 72 |
attr |
43 |
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
|
|
73 |
(Utils.fprintf_list ~sep:", " (print_static_val pp_var)) values
|
|
44 | 74 |
(Utils.pp_final_char_if_non_empty ", " static) |
45 | 75 |
i |
46 | 76 |
|
47 |
let print_static_declare_macro fmt m = |
|
77 |
let print_static_declare_macro fmt (m, attr, inst) = |
|
78 |
let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in |
|
48 | 79 |
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
49 |
let inst = mk_instance m in |
|
50 |
let attr = mk_attribute m in |
|
51 |
fprintf fmt "@[<v 2>#define %a(%s, %a%t%s)\\@,%s %a %s;\\@,%a%t%a;@,@]" |
|
80 |
fprintf fmt "@[<v 2>#define %a(%s, %a%t%s)\\@,%a%s %a %s;\\@,%a%t%a;@,@]" |
|
52 | 81 |
pp_machine_static_declare_name m.mname.node_id |
53 | 82 |
attr |
54 | 83 |
(Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic |
55 | 84 |
(Utils.pp_final_char_if_non_empty ", " m.mstatic) |
56 | 85 |
inst |
86 |
(* constants *) |
|
87 |
(print_static_constant (m, attr, inst)) const_locals |
|
57 | 88 |
attr |
58 | 89 |
pp_machine_memtype_name m.mname.node_id |
59 | 90 |
inst |
60 |
(Utils.fprintf_list ~sep:";\\@," pp_c_decl_local_var) array_mem
|
|
91 |
(Utils.fprintf_list ~sep:";\\@," (pp_c_decl_local_var m)) array_mem
|
|
61 | 92 |
(Utils.pp_final_char_if_non_empty ";\\@," array_mem) |
62 | 93 |
(Utils.fprintf_list ~sep:";\\@," |
63 | 94 |
(fun fmt (i',m') -> |
64 |
let path = sprintf "inst ## _%s" i' in
|
|
95 |
let path = sprintf "%s ## _%s" inst i' in
|
|
65 | 96 |
fprintf fmt "%a" |
66 |
(print_static_declare_instance attr) (path,m')
|
|
97 |
(print_static_declare_instance (m, attr, inst) const_locals) (path, m')
|
|
67 | 98 |
)) m.minstances |
68 | 99 |
|
69 | 100 |
|
... | ... | |
73 | 104 |
(* Allocation of a node struct: |
74 | 105 |
- if node memory is an array/matrix/etc, we cast it to a pointer (see pp_registers_struct) |
75 | 106 |
*) |
76 |
let print_static_link_macro fmt m =
|
|
107 |
let print_static_link_macro fmt (m, attr, inst) =
|
|
77 | 108 |
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in |
78 |
fprintf fmt "@[<v>@[<v 2>#define %a(inst) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"
|
|
109 |
fprintf fmt "@[<v>@[<v 2>#define %a(%s) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"
|
|
79 | 110 |
pp_machine_static_link_name m.mname.node_id |
111 |
inst |
|
80 | 112 |
(Utils.fprintf_list ~sep:";\\@," |
81 | 113 |
(fun fmt v -> |
82 |
fprintf fmt "inst._reg.%s = (%a*) &%s" |
|
114 |
fprintf fmt "%s._reg.%s = (%a*) &%s" |
|
115 |
inst |
|
83 | 116 |
v.var_id |
84 | 117 |
(fun fmt v -> pp_c_type "" fmt (Types.array_base_type v.var_type)) v |
85 | 118 |
v.var_id |
... | ... | |
87 | 120 |
(Utils.pp_final_char_if_non_empty ";\\@," array_mem) |
88 | 121 |
(Utils.fprintf_list ~sep:";\\@," |
89 | 122 |
(fun fmt (i',m') -> |
90 |
let path = sprintf "inst ## _%s" i' in
|
|
91 |
fprintf fmt "%a;\\@,inst.%s = &%s"
|
|
123 |
let path = sprintf "%s ## _%s" inst i' in
|
|
124 |
fprintf fmt "%a;\\@,%s.%s = &%s"
|
|
92 | 125 |
print_static_link_instance (path,m') |
126 |
inst |
|
93 | 127 |
i' |
94 | 128 |
path |
95 | 129 |
)) m.minstances |
96 |
|
|
97 |
let print_static_alloc_macro fmt m =
|
|
98 |
fprintf fmt "@[<v>@[<v 2>#define %a(attr,%a%tinst)\\@,%a(attr,%a%tinst);\\@,%a(inst);@]@,@]@."
|
|
130 |
|
|
131 |
let print_static_alloc_macro fmt (m, attr, inst) =
|
|
132 |
fprintf fmt "@[<v>@[<v 2>#define %a(%s, %a%t%s)\\@,%a(%s, %a%t%s);\\@,%a(%s);@]@,@]@."
|
|
99 | 133 |
pp_machine_static_alloc_name m.mname.node_id |
134 |
attr |
|
100 | 135 |
(Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic |
101 | 136 |
(Utils.pp_final_char_if_non_empty ", " m.mstatic) |
137 |
inst |
|
102 | 138 |
pp_machine_static_declare_name m.mname.node_id |
139 |
attr |
|
103 | 140 |
(Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic |
104 | 141 |
(Utils.pp_final_char_if_non_empty ", " m.mstatic) |
142 |
inst |
|
105 | 143 |
pp_machine_static_link_name m.mname.node_id |
144 |
inst |
|
106 | 145 |
|
107 |
|
|
108 | 146 |
let print_machine_decl fmt m = |
109 | 147 |
Mod.print_machine_decl_prefix fmt m; |
110 | 148 |
if fst (get_stateless_status m) then |
... | ... | |
117 | 155 |
begin |
118 | 156 |
(* Static allocation *) |
119 | 157 |
if !Options.static_mem |
120 |
then ( |
|
121 |
fprintf fmt "%a@.%a@.%a@." |
|
122 |
print_static_declare_macro m |
|
123 |
print_static_link_macro m |
|
124 |
print_static_alloc_macro m |
|
125 |
) |
|
126 |
else ( |
|
158 |
then |
|
159 |
begin |
|
160 |
let inst = mk_instance m in |
|
161 |
let attr = mk_attribute m in |
|
162 |
fprintf fmt "%a@.%a@.%a@." |
|
163 |
print_static_declare_macro (m, attr, inst) |
|
164 |
print_static_link_macro (m, attr, inst) |
|
165 |
print_static_alloc_macro (m, attr, inst) |
|
166 |
end |
|
167 |
else |
|
168 |
begin |
|
127 | 169 |
(* Dynamic allocation *) |
128 |
fprintf fmt "extern %a;@.@." |
|
129 |
print_alloc_prototype (m.mname.node_id, m.mstatic) |
|
130 |
);
|
|
170 |
fprintf fmt "extern %a;@.@."
|
|
171 |
print_alloc_prototype (m.mname.node_id, m.mstatic)
|
|
172 |
end;
|
|
131 | 173 |
let self = mk_self m in |
132 | 174 |
fprintf fmt "extern %a;@.@." |
133 | 175 |
(print_reset_prototype self) (m.mname.node_id, m.mstatic); |
... | ... | |
148 | 190 |
then |
149 | 191 |
begin |
150 | 192 |
(* Static allocation *) |
193 |
let inst = mk_instance m in |
|
194 |
let attr = mk_attribute m in |
|
151 | 195 |
fprintf fmt "%a@.%a@.%a@." |
152 |
print_static_declare_macro m
|
|
153 |
print_static_link_macro m
|
|
154 |
print_static_alloc_macro m
|
|
196 |
print_static_declare_macro (m, attr, inst)
|
|
197 |
print_static_link_macro (m, attr, inst)
|
|
198 |
print_static_alloc_macro (m, attr, inst)
|
|
155 | 199 |
end |
156 | 200 |
else |
157 | 201 |
begin |
src/backends/C/c_backend_main.ml | ||
---|---|---|
31 | 31 |
(********************************************************************************************) |
32 | 32 |
|
33 | 33 |
let print_get_input fmt v = |
34 |
match v.var_type.Types.tdesc with
|
|
34 |
match (Types.repr v.var_type).Types.tdesc with
|
|
35 | 35 |
| Types.Tint -> fprintf fmt "_get_int(\"%s\")" v.var_id |
36 | 36 |
| Types.Tbool -> fprintf fmt "_get_bool(\"%s\")" v.var_id |
37 | 37 |
| Types.Treal -> fprintf fmt "_get_double(\"%s\")" v.var_id |
... | ... | |
39 | 39 |
|
40 | 40 |
let print_put_outputs fmt ol = |
41 | 41 |
let po fmt o = |
42 |
match o.var_type.Types.tdesc with
|
|
42 |
match (Types.repr o.var_type).Types.tdesc with
|
|
43 | 43 |
| Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o.var_id o.var_id |
44 | 44 |
| Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o.var_id o.var_id |
45 | 45 |
| Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o.var_id o.var_id |
src/backends/C/c_backend_src.ml | ||
---|---|---|
293 | 293 |
pp_machine_alloc_name (node_name m) |
294 | 294 |
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static |
295 | 295 |
|
296 |
let print_alloc_const fmt m = |
|
297 |
let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in |
|
298 |
fprintf fmt "%a%t" |
|
299 |
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) const_locals |
|
300 |
(Utils.pp_final_char_if_non_empty ";@," const_locals) |
|
301 |
|
|
296 | 302 |
let print_alloc_array fmt vdecl = |
297 | 303 |
let base_type = Types.array_base_type vdecl.var_type in |
298 | 304 |
let size_types = Types.array_type_multi_dimension vdecl.var_type in |
... | ... | |
321 | 327 |
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@." |
322 | 328 |
print_stateless_prototype (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
323 | 329 |
(* locals *) |
324 |
(Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
|
|
330 |
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
|
|
325 | 331 |
(Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals) |
326 | 332 |
(* check assertions *) |
327 | 333 |
(pp_c_checks self) m |
... | ... | |
336 | 342 |
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@." |
337 | 343 |
print_stateless_prototype (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs) |
338 | 344 |
(* locals *) |
339 |
(Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals
|
|
345 |
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
|
|
340 | 346 |
(Utils.pp_final_char_if_non_empty ";" base_locals) |
341 | 347 |
(* check assertions *) |
342 | 348 |
(pp_c_checks self) m |
... | ... | |
346 | 352 |
(fun fmt -> fprintf fmt "return;") |
347 | 353 |
|
348 | 354 |
let print_reset_code dependencies fmt m self = |
349 |
fprintf fmt "@[<v 2>%a {@,%a%treturn;@]@,}@.@." |
|
355 |
let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in |
|
356 |
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%treturn;@]@,}@.@." |
|
350 | 357 |
(print_reset_prototype self) (m.mname.node_id, m.mstatic) |
358 |
(* constant locals decl *) |
|
359 |
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) const_locals |
|
360 |
(Utils.pp_final_char_if_non_empty ";" const_locals) |
|
361 |
(* instrs *) |
|
351 | 362 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.minit |
352 | 363 |
(Utils.pp_newline_if_non_empty m.minit) |
353 | 364 |
|
... | ... | |
359 | 370 |
fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t@]@,}@.@." |
360 | 371 |
(print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
361 | 372 |
(* locals *) |
362 |
(Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
|
|
373 |
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
|
|
363 | 374 |
(Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals) |
364 | 375 |
(* array mems *) |
365 | 376 |
(Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems |
... | ... | |
377 | 388 |
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@." |
378 | 389 |
(print_step_prototype self) (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs) |
379 | 390 |
(* locals *) |
380 |
(Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals
|
|
391 |
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
|
|
381 | 392 |
(Utils.pp_final_char_if_non_empty ";" base_locals) |
382 | 393 |
(* check assertions *) |
383 | 394 |
(pp_c_checks self) m |
... | ... | |
402 | 413 |
(* Alloc function, only if non static mode *) |
403 | 414 |
if (not !Options.static_mem) then |
404 | 415 |
begin |
405 |
fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@." |
|
416 |
fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@.@."
|
|
406 | 417 |
print_alloc_prototype (m.mname.node_id, m.mstatic) |
418 |
print_alloc_const m |
|
407 | 419 |
print_alloc_code m; |
408 | 420 |
end; |
409 | 421 |
let self = mk_self m in |
... | ... | |
435 | 447 |
fprintf source_fmt "@[<v>"; |
436 | 448 |
List.iter (fun c -> print_const_def source_fmt (const_of_top c)) (get_consts prog); |
437 | 449 |
fprintf source_fmt "@]@."; |
450 |
|
|
438 | 451 |
if not !Options.static_mem then |
439 | 452 |
begin |
440 | 453 |
fprintf source_fmt "/* External allocation function prototypes */@."; |
... | ... | |
446 | 459 |
List.iter (fun m -> fprintf source_fmt "%a;@." print_alloc_prototype (m.mname.node_id, m.mstatic)) machines; |
447 | 460 |
fprintf source_fmt "@]@."; |
448 | 461 |
end; |
462 |
|
|
449 | 463 |
(* Print the struct definitions of all machines. *) |
450 | 464 |
fprintf source_fmt "/* Struct definitions */@."; |
451 | 465 |
fprintf source_fmt "@[<v>"; |
src/causality.ml | ||
---|---|---|
28 | 28 |
by duplication of some mem vars into local node vars. |
29 | 29 |
Thus, cylic dependency errors may only arise between no-mem vars. |
30 | 30 |
non-mem variables are: |
31 |
- inputs: not needed for causality/scheduling, needed only for detecting useless vars |
|
31 |
- constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars
|
|
32 | 32 |
- read mems (fake vars): same remark as above. |
33 | 33 |
- outputs: decoupled from mems, if necessary |
34 | 34 |
- locals |
... | ... | |
133 | 133 |
let node_local_variables nd = |
134 | 134 |
List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals |
135 | 135 |
|
136 |
let node_constant_variables nd = |
|
137 |
List.fold_left (fun locals v -> if v.var_dec_const then ISet.add v.var_id locals else locals) ISet.empty nd.node_locals |
|
138 |
|
|
136 | 139 |
let node_output_variables nd = |
137 | 140 |
List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs |
138 | 141 |
|
... | ... | |
533 | 536 |
|
534 | 537 |
let global_dependency node = |
535 | 538 |
let mems = ExprDep.node_memory_variables node in |
536 |
let inputs = ExprDep.node_input_variables node in |
|
539 |
let inputs = |
|
540 |
ISet.union |
|
541 |
(ExprDep.node_input_variables node) |
|
542 |
(ExprDep.node_constant_variables node) in |
|
537 | 543 |
let outputs = ExprDep.node_output_variables node in |
538 | 544 |
let node_vars = ExprDep.node_variables node in |
539 | 545 |
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in |
src/clock_calculus.ml | ||
---|---|---|
779 | 779 |
if Types.get_clock_base_type vdecl.var_type <> None |
780 | 780 |
then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped |
781 | 781 |
else ck in |
782 |
vdecl.var_clock <- ck; |
|
782 |
(if vdecl.var_dec_const |
|
783 |
then match vdecl.var_dec_value with |
|
784 |
| None -> () |
|
785 |
| Some v -> |
|
786 |
begin |
|
787 |
let ck_static = clock_expr env v in |
|
788 |
try_unify ck ck_static v.expr_loc |
|
789 |
end); |
|
790 |
try_unify ck vdecl.var_clock vdecl.var_loc; |
|
783 | 791 |
Env.add_value env vdecl.var_id ck |
784 | 792 |
|
785 | 793 |
(* Clocks a variable declaration list *) |
src/clock_predef.ml | ||
---|---|---|
42 | 42 |
let cuniv = new_carrier Carry_var false in |
43 | 43 |
new_ck (Carrow (new_ck (Ccarrying (cuniv, univ)) false, univ)) |
44 | 44 |
|
45 |
let ck_carrier id ck = |
|
46 |
new_ck (Ccarrying (new_carrier (Carry_const id) true, ck)) true |
|
45 | 47 |
(* Local Variables: *) |
46 | 48 |
(* compile-command:"make -C .." *) |
47 | 49 |
(* End: *) |
src/compiler_common.ml | ||
---|---|---|
73 | 73 |
Parse.report_error err; |
74 | 74 |
raise exc |
75 | 75 |
| Corelang.Error (loc, err) as exc -> |
76 |
eprintf "Parsing error %a%a@." |
|
76 |
eprintf "Parsing error: %a%a@."
|
|
77 | 77 |
Corelang.pp_error err |
78 | 78 |
Location.pp_loc loc; |
79 | 79 |
raise exc |
... | ... | |
83 | 83 |
try |
84 | 84 |
Stateless.check_prog decls |
85 | 85 |
with (Stateless.Error (loc, err)) as exc -> |
86 |
eprintf "Stateless status error %a%a@." |
|
86 |
eprintf "Stateless status error: %a%a@."
|
|
87 | 87 |
Stateless.pp_error err |
88 | 88 |
Location.pp_loc loc; |
89 | 89 |
raise exc |
... | ... | |
95 | 95 |
try |
96 | 96 |
Typing.type_prog env decls |
97 | 97 |
with (Types.Error (loc,err)) as exc -> |
98 |
eprintf "Typing error %a%a@." |
|
98 |
eprintf "Typing error: %a%a@."
|
|
99 | 99 |
Types.pp_error err |
100 | 100 |
Location.pp_loc loc; |
101 | 101 |
raise exc |
... | ... | |
112 | 112 |
try |
113 | 113 |
Clock_calculus.clock_prog env decls |
114 | 114 |
with (Clocks.Error (loc,err)) as exc -> |
115 |
eprintf "Clock calculus error %a%a@." Clocks.pp_error err Location.pp_loc loc; |
|
115 |
eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc;
|
|
116 | 116 |
raise exc |
117 | 117 |
end |
118 | 118 |
in |
src/corelang.ml | ||
---|---|---|
41 | 41 |
let mkclock loc d = |
42 | 42 |
{ ck_dec_desc = d; ck_dec_loc = loc } |
43 | 43 |
|
44 |
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const) = |
|
44 |
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) = |
|
45 |
assert (value = None || is_const); |
|
45 | 46 |
{ var_id = id; |
46 | 47 |
var_orig = orig; |
47 | 48 |
var_dec_type = ty_dec; |
48 | 49 |
var_dec_clock = ck_dec; |
49 | 50 |
var_dec_const = is_const; |
51 |
var_dec_value = value; |
|
50 | 52 |
var_type = Types.new_var (); |
51 | 53 |
var_clock = Clocks.new_var true; |
52 | 54 |
var_loc = loc } |
... | ... | |
66 | 68 |
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; |
67 | 69 |
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; |
68 | 70 |
var_dec_const = true; |
71 |
var_dec_value = None; |
|
69 | 72 |
var_type = c.const_type; |
70 | 73 |
var_clock = Clocks.new_var false; |
71 | 74 |
var_loc = c.const_loc } |
... | ... | |
93 | 96 |
let mkpredef_call loc funname args = |
94 | 97 |
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) |
95 | 98 |
|
99 |
let is_clock_dec_type cty = |
|
100 |
match cty with |
|
101 |
| Tydec_clock _ -> true |
|
102 |
| _ -> false |
|
96 | 103 |
|
97 | 104 |
let const_of_top top_decl = |
98 | 105 |
match top_decl.top_decl_desc with |
... | ... | |
578 | 585 |
(************************************************************************) |
579 | 586 |
(* Renaming *) |
580 | 587 |
|
588 |
let rec rename_static rename cty = |
|
589 |
match cty with |
|
590 |
| Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty') |
|
591 |
| Tydec_clock cty -> Tydec_clock (rename_static rename cty) |
|
592 |
| Tydec_struct fl -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl) |
|
593 |
| _ -> cty |
|
594 |
|
|
595 |
let rec rename_carrier rename cck = |
|
596 |
match cck with |
|
597 |
| Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl) |
|
598 |
| _ -> cck |
|
599 |
|
|
600 |
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*) |
|
601 |
|
|
602 |
(* applies the renaming function [fvar] to all variables of expression [expr] *) |
|
603 |
let rec expr_replace_var fvar expr = |
|
604 |
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } |
|
605 |
|
|
606 |
and expr_desc_replace_var fvar expr_desc = |
|
607 |
match expr_desc with |
|
608 |
| Expr_const _ -> expr_desc |
|
609 |
| Expr_ident i -> Expr_ident (fvar i) |
|
610 |
| Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) |
|
611 |
| Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) |
|
612 |
| Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) |
|
613 |
| Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) |
|
614 |
| Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) |
|
615 |
| Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) |
|
616 |
| Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) |
|
617 |
| Expr_pre e' -> Expr_pre (expr_replace_var fvar e') |
|
618 |
| Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) |
|
619 |
| Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) |
|
620 |
| Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') |
|
621 |
|
|
622 |
(* Applies the renaming function [fvar] to every rhs |
|
623 |
only when the corresponding lhs satisfies predicate [pvar] *) |
|
624 |
let eq_replace_rhs_var pvar fvar eq = |
|
625 |
let pvar l = List.exists pvar l in |
|
626 |
let rec replace lhs rhs = |
|
627 |
{ rhs with expr_desc = replace_desc lhs rhs.expr_desc } |
|
628 |
and replace_desc lhs rhs_desc = |
|
629 |
match lhs with |
|
630 |
| [] -> assert false |
|
631 |
| [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc |
|
632 |
| _ -> |
|
633 |
(match rhs_desc with |
|
634 |
| Expr_tuple tl -> |
|
635 |
Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl) |
|
636 |
| Expr_appl (f, arg, None) when Basic_library.is_internal_fun f -> |
|
637 |
let args = expr_list_of_expr arg in |
|
638 |
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) |
|
639 |
| Expr_array _ |
|
640 |
| Expr_access _ |
|
641 |
| Expr_power _ |
|
642 |
| Expr_const _ |
|
643 |
| Expr_ident _ |
|
644 |
| Expr_appl _ -> |
|
645 |
if pvar lhs |
|
646 |
then expr_desc_replace_var fvar rhs_desc |
|
647 |
else rhs_desc |
|
648 |
| Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e) |
|
649 |
| Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2) |
|
650 |
| Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2) |
|
651 |
| Expr_pre e' -> Expr_pre (replace lhs e') |
|
652 |
| Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i |
|
653 |
in Expr_when (replace lhs e', i', l) |
|
654 |
| Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i |
|
655 |
in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl) |
|
656 |
) |
|
657 |
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } |
|
658 |
|
|
659 |
|
|
660 |
let rec rename_expr f_node f_var f_const expr = |
|
661 |
{ expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc } |
|
662 |
and rename_expr_desc f_node f_var f_const expr_desc = |
|
663 |
let re = rename_expr f_node f_var f_const in |
|
664 |
match expr_desc with |
|
665 |
| Expr_const _ -> expr_desc |
|
666 |
| Expr_ident i -> Expr_ident (f_var i) |
|
667 |
| Expr_array el -> Expr_array (List.map re el) |
|
668 |
| Expr_access (e1, d) -> Expr_access (re e1, d) |
|
669 |
| Expr_power (e1, d) -> Expr_power (re e1, d) |
|
670 |
| Expr_tuple el -> Expr_tuple (List.map re el) |
|
671 |
| Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e) |
|
672 |
| Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) |
|
673 |
| Expr_fby (e1, e2) -> Expr_fby (re e1, re e2) |
|
674 |
| Expr_pre e' -> Expr_pre (re e') |
|
675 |
| Expr_when (e', i, l)-> Expr_when (re e', f_var i, l) |
|
676 |
| Expr_merge (i, hl) -> |
|
677 |
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl) |
|
678 |
| Expr_appl (i, e', i') -> |
|
679 |
Expr_appl (f_node i, re e', Utils.option_map re i') |
|
680 |
|
|
681 |
let rename_node_annot f_node f_var f_const expr = |
|
682 |
expr |
|
683 |
(* TODO assert false *) |
|
684 |
|
|
685 |
let rename_expr_annot f_node f_var f_const annot = |
|
686 |
annot |
|
687 |
(* TODO assert false *) |
|
688 |
|
|
689 |
let rename_node f_node f_var f_const nd = |
|
690 |
let rename_var v = { v with var_id = f_var v.var_id } in |
|
691 |
let rename_eq eq = { eq with |
|
692 |
eq_lhs = List.map f_var eq.eq_lhs; |
|
693 |
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs |
|
694 |
} |
|
695 |
in |
|
696 |
let inputs = List.map rename_var nd.node_inputs in |
|
697 |
let outputs = List.map rename_var nd.node_outputs in |
|
698 |
let locals = List.map rename_var nd.node_locals in |
|
699 |
let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in |
|
700 |
let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in |
|
701 |
let node_asserts = List.map |
|
702 |
(fun a -> |
|
703 |
{a with assert_expr = |
|
704 |
let expr = a.assert_expr in |
|
705 |
rename_expr f_node f_var f_const expr}) |
|
706 |
nd.node_asserts |
|
707 |
in |
|
708 |
let node_stmts = List.map (fun eq -> Eq (rename_eq eq)) (get_node_eqs nd) in |
|
709 |
let spec = |
|
710 |
Utils.option_map |
|
711 |
(fun s -> rename_node_annot f_node f_var f_const s) |
|
712 |
nd.node_spec |
|
713 |
in |
|
714 |
let annot = |
|
715 |
List.map |
|
716 |
(fun s -> rename_expr_annot f_node f_var f_const s) |
|
717 |
nd.node_annot |
|
718 |
in |
|
719 |
{ |
|
720 |
node_id = f_node nd.node_id; |
|
721 |
node_type = nd.node_type; |
|
722 |
node_clock = nd.node_clock; |
|
723 |
node_inputs = inputs; |
|
724 |
node_outputs = outputs; |
|
725 |
node_locals = locals; |
|
726 |
node_gencalls = gen_calls; |
|
727 |
node_checks = node_checks; |
|
728 |
node_asserts = node_asserts; |
|
729 |
node_stmts = node_stmts; |
|
730 |
node_dec_stateless = nd.node_dec_stateless; |
|
731 |
node_stateless = nd.node_stateless; |
|
732 |
node_spec = spec; |
|
733 |
node_annot = annot; |
|
734 |
} |
|
735 |
|
|
736 |
|
|
737 |
let rename_const f_const c = |
|
738 |
{ c with const_id = f_const c.const_id } |
|
739 |
|
|
740 |
let rename_typedef f_var t = |
|
741 |
match t.tydef_desc with |
|
742 |
| Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) } |
|
743 |
| _ -> t |
|
744 |
|
|
745 |
let rename_prog f_node f_var f_const prog = |
|
746 |
List.rev ( |
|
747 |
List.fold_left (fun accu top -> |
|
748 |
(match top.top_decl_desc with |
|
749 |
| Node nd -> |
|
750 |
{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) } |
|
751 |
| Const c -> |
|
752 |
{ top with top_decl_desc = Const (rename_const f_const c) } |
|
753 |
| TypeDef tdef -> |
|
754 |
{ top with top_decl_desc = TypeDef (rename_typedef f_var tdef) } |
|
755 |
| ImportedNode _ |
|
756 |
| Open _ -> top) |
|
757 |
::accu |
|
758 |
) [] prog |
|
759 |
) |
|
760 |
|
|
761 |
(**********************************************************************) |
|
762 |
(* Pretty printers *) |
|
763 |
|
|
764 |
let pp_decl_type fmt tdecl = |
|
765 |
match tdecl.top_decl_desc with |
|
766 |
| Node nd -> |
|
767 |
fprintf fmt "%s: " nd.node_id; |
|
768 |
Utils.reset_names (); |
|
769 |
fprintf fmt "%a@ " Types.print_ty nd.node_type |
|
770 |
| ImportedNode ind -> |
|
771 |
fprintf fmt "%s: " ind.nodei_id; |
|
772 |
Utils.reset_names (); |
|
773 |
fprintf fmt "%a@ " Types.print_ty ind.nodei_type |
|
774 |
| Const _ | Open _ | TypeDef _ -> () |
|
775 |
|
|
776 |
let pp_prog_type fmt tdecl_list = |
|
777 |
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list |
|
778 |
|
|
779 |
let pp_decl_clock fmt cdecl = |
|
780 |
match cdecl.top_decl_desc with |
|
781 |
| Node nd -> |
|
782 |
fprintf fmt "%s: " nd.node_id; |
|
783 |
Utils.reset_names (); |
|
784 |
fprintf fmt "%a@ " Clocks.print_ck nd.node_clock |
|
785 |
| ImportedNode ind -> |
|
786 |
fprintf fmt "%s: " ind.nodei_id; |
|
787 |
Utils.reset_names (); |
|
788 |
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock |
|
789 |
| Const _ | Open _ | TypeDef _ -> () |
|
790 |
|
|
791 |
let pp_prog_clock fmt prog = |
|
792 |
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog |
|
793 |
|
|
794 |
let pp_error fmt = function |
|
795 |
Main_not_found -> |
|
796 |
fprintf fmt "Cannot compile node %s: could not find the node definition.@." |
|
797 |
!Options.main_node |
|
798 |
| Main_wrong_kind -> |
|
799 |
fprintf fmt |
|
800 |
"Name %s does not correspond to a (non-imported) node definition.@." |
|
801 |
!Options.main_node |
|
802 |
| No_main_specified -> |
|
803 |
fprintf fmt "No main node specified@." |
|
804 |
| Unbound_symbol sym -> |
|
805 |
fprintf fmt |
|
806 |
"%s is undefined.@." |
|
807 |
sym |
|
808 |
| Already_bound_symbol sym -> |
|
809 |
fprintf fmt |
|
810 |
"%s is already defined.@." |
|
811 |
sym |
|
812 |
| Unknown_library sym -> |
|
813 |
fprintf fmt |
|
814 |
"impossible to load library %s.lusic@.Please compile the corresponding interface or source file.@." |
|
815 |
sym |
|
816 |
| Wrong_number sym -> |
|
817 |
fprintf fmt |
|
818 |
"library %s.lusic has a different version number and may crash compiler@.Please recompile the corresponding interface or source file.@." |
|
819 |
sym |
|
820 |
|
|
821 |
(* filling node table with internal functions *) |
|
822 |
let vdecls_of_typ_ck cpt ty = |
|
823 |
let loc = Location.dummy_loc in |
|
824 |
List.map |
|
825 |
(fun _ -> incr cpt; |
|
826 |
let name = sprintf "_var_%d" !cpt in |
|
827 |
mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None)) |
|
828 |
(Types.type_list_of_type ty) |
|
829 |
|
|
830 |
let mk_internal_node id = |
|
831 |
let spec = None in |
|
832 |
let ty = Env.lookup_value Basic_library.type_env id in |
|
833 |
let ck = Env.lookup_value Basic_library.clock_env id in |
|
834 |
let (tin, tout) = Types.split_arrow ty in |
|
835 |
(*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*) |
|
836 |
let cpt = ref (-1) in |
|
837 |
mktop |
|
838 |
(ImportedNode |
|
839 |
{nodei_id = id; |
|
840 |
nodei_type = ty; |
|
841 |
nodei_clock = ck; |
|
842 |
nodei_inputs = vdecls_of_typ_ck cpt tin; |
|
843 |
nodei_outputs = vdecls_of_typ_ck cpt tout; |
|
844 |
nodei_stateless = Types.get_static_value ty <> None; |
|
845 |
nodei_spec = spec; |
|
846 |
nodei_prototype = None; |
|
847 |
nodei_in_lib = None; |
|
848 |
}) |
|
849 |
|
|
850 |
let add_internal_funs () = |
|
851 |
List.iter |
|
852 |
(fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd) |
|
853 |
Basic_library.internal_funs |
|
854 |
|
|
855 |
|
|
856 |
|
|
857 |
(* Replace any occurence of a var in vars_to_replace by its associated |
|
858 |
expression in defs until e does not contain any such variables *) |
|
859 |
let rec substitute_expr vars_to_replace defs e = |
|
860 |
let se = substitute_expr vars_to_replace defs in |
|
861 |
{ e with expr_desc = |
|
862 |
let ed = e.expr_desc in |
|
863 |
match ed with |
|
864 |
| Expr_const _ -> ed |
|
865 |
| Expr_array el -> Expr_array (List.map se el) |
|
866 |
| Expr_access (e1, d) -> Expr_access (se e1, d) |
|
867 |
| Expr_power (e1, d) -> Expr_power (se e1, d) |
|
868 |
| Expr_tuple el -> Expr_tuple (List.map se el) |
|
869 |
| Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e) |
|
870 |
| Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) |
|
871 |
| Expr_fby (e1, e2) -> Expr_fby (se e1, se e2) |
|
872 |
| Expr_pre e' -> Expr_pre (se e') |
|
873 |
| Expr_when (e', i, l)-> Expr_when (se e', i, l) |
|
874 |
| Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl) |
|
875 |
| Expr_appl (i, e', i') -> Expr_appl (i, se e', i') |
|
876 |
| Expr_ident i -> |
|
877 |
if List.exists (fun v -> v.var_id = i) vars_to_replace then ( |
|
878 |
let eq_i eq = eq.eq_lhs = [i] in |
|
879 |
if List.exists eq_i defs then |
|
880 |
let sub = List.find eq_i defs in |
|
881 |
let sub' = se sub.eq_rhs in |
|
882 |
sub'.expr_desc |
|
883 |
else |
|
884 |
assert false |
|
885 |
) |
|
886 |
else |
|
887 |
ed |
|
888 |
|
|
889 |
} |
|
890 |
(* FAUT IL RETIRER ? |
|
891 |
|
|
892 |
let rec expr_to_eexpr expr = |
|
893 |
{ eexpr_tag = expr.expr_tag; |
|
894 |
eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc; |
|
895 |
eexpr_type = expr.expr_type; |
|
896 |
eexpr_clock = expr.expr_clock; |
|
897 |
eexpr_loc = expr.expr_loc |
|
898 |
} |
|
899 |
and expr_desc_to_eexpr_desc expr_desc = |
|
900 |
let conv = expr_to_eexpr in |
|
901 |
match expr_desc with |
|
902 |
| Expr_const c -> EExpr_const (match c with |
|
903 |
| Const_int x -> EConst_int x |
|
904 |
| Const_real x -> EConst_real x |
|
905 |
| Const_float x -> EConst_float x |
|
906 |
| Const_tag x -> EConst_tag x |
|
907 |
| _ -> assert false |
|
908 |
|
|
909 |
) |
|
910 |
| Expr_ident i -> EExpr_ident i |
|
911 |
| Expr_tuple el -> EExpr_tuple (List.map conv el) |
|
912 |
|
|
913 |
| Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) |
|
914 |
| Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) |
|
915 |
| Expr_pre e' -> EExpr_pre (conv e') |
|
916 |
| Expr_appl (i, e', i') -> |
|
917 |
EExpr_appl |
|
918 |
(i, conv e', match i' with None -> None | Some(id, _) -> Some id) |
|
919 |
|
|
920 |
| Expr_when _ |
|
921 |
| Expr_merge _ -> assert false |
|
922 |
| Expr_array _ |
|
923 |
| Expr_access _ |
|
924 |
| Expr_power _ -> assert false |
|
925 |
| Expr_ite (c, t, e) -> assert false |
|
926 |
| _ -> assert false |
|
927 |
|
|
928 |
*) |
|
929 |
let rec get_expr_calls nodes e = |
|
930 |
get_calls_expr_desc nodes e.expr_desc |
|
931 |
and get_calls_expr_desc nodes expr_desc = |
|
932 |
let get_calls = get_expr_calls nodes in |
|
933 |
match expr_desc with |
|
934 |
| Expr_const _ |
|
935 |
| Expr_ident _ -> Utils.ISet.empty |
|
936 |
| Expr_tuple el |
|
937 |
| Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el |
|
938 |
| Expr_pre e1 |
|
939 |
| Expr_when (e1, _, _) |
|
940 |
| Expr_access (e1, _) |
|
941 |
| Expr_power (e1, _) -> get_calls e1 |
|
942 |
| Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) |
|
943 |
| Expr_arrow (e1, e2) |
|
944 |
| Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2) |
|
945 |
| Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty hl |
|
946 |
| Expr_appl (i, e', i') -> |
|
947 |
if Basic_library.is_internal_fun i then |
|
948 |
(get_calls e') |
|
949 |
else |
|
950 |
let calls = Utils.ISet.add i (get_calls e') in |
|
951 |
let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in |
|
952 |
if List.exists test nodes then |
|
953 |
match (List.find test nodes).top_decl_desc with |
|
954 |
| Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls |
|
955 |
| _ -> assert false |
|
956 |
else |
|
957 |
calls |
|
958 |
|
|
959 |
and get_eq_calls nodes eq = |
|
960 |
get_expr_calls nodes eq.eq_rhs |
|
961 |
and get_node_calls nodes node = |
|
962 |
List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node) |
|
963 |
|
|
964 |
let rec get_expr_vars vars e = |
|
965 |
get_expr_desc_vars vars e.expr_desc |
|
966 |
and get_expr_desc_vars vars expr_desc = |
|
967 |
match expr_desc with |
|
968 |
| Expr_const _ -> vars |
|
969 |
| Expr_ident x -> Utils.ISet.add x vars |
|
970 |
| Expr_tuple el |
|
971 |
| Expr_array el -> List.fold_left get_expr_vars vars el |
|
972 |
| Expr_pre e1 -> get_expr_vars vars e1 |
|
973 |
| Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 |
|
974 |
| Expr_access (e1, d) |
|
975 |
| Expr_power (e1, d) -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d] |
|
976 |
| Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e] |
|
977 |
| Expr_arrow (e1, e2) |
|
978 |
| Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2] |
|
979 |
| Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl |
|
980 |
| Expr_appl (_, arg, None) -> get_expr_vars vars arg |
|
981 |
| Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r] |
|
982 |
|
|
983 |
|
|
984 |
let rec expr_has_arrows e = |
|
985 |
expr_desc_has_arrows e.expr_desc |
|
986 |
and expr_desc_has_arrows expr_desc = |
|
987 |
match expr_desc with |
|
988 |
| Expr_const _ |
|
989 |
| Expr_ident _ -> false |
|
990 |
| Expr_tuple el |
|
991 |
| Expr_array el -> List.exists expr_has_arrows el |
|
992 |
| Expr_pre e1 |
|
993 |
| Expr_when (e1, _, _) |
|
994 |
| Expr_access (e1, _) |
|
995 |
| Expr_power (e1, _) -> expr_has_arrows e1 |
|
996 |
| Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e] |
|
997 |
| Expr_arrow (e1, e2) |
|
998 |
| Expr_fby (e1, e2) -> true |
|
999 |
| Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl |
|
1000 |
| Expr_appl (i, e', i') -> expr_has_arrows e' |
|
1001 |
|
|
1002 |
and eq_has_arrows eq = |
|
1003 |
expr_has_arrows eq.eq_rhs |
|
1004 |
and node_has_arrows node = |
|
1005 |
List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node) |
|
1006 |
|
|
1007 |
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) = |
|
1008 |
assert (value = None || is_const); |
|
1009 |
{ var_id = id; |
|
1010 |
var_orig = orig; |
|
1011 |
var_dec_type = ty_dec; |
|
1012 |
var_dec_clock = ck_dec; |
|
1013 |
var_dec_const = is_const; |
|
1014 |
var_dec_value = value; |
|
1015 |
var_type = Types.new_var (); |
|
1016 |
var_clock = Clocks.new_var true; |
|
1017 |
var_loc = loc } |
|
1018 |
|
|
1019 |
let mkexpr loc d = |
|
1020 |
{ expr_tag = Utils.new_tag (); |
|
1021 |
expr_desc = d; |
|
1022 |
expr_type = Types.new_var (); |
|
1023 |
expr_clock = Clocks.new_var true; |
|
1024 |
expr_delay = Delay.new_var (); |
|
1025 |
expr_annot = None; |
|
1026 |
expr_loc = loc } |
|
1027 |
|
|
1028 |
let var_decl_of_const c = |
|
1029 |
{ var_id = c.const_id; |
|
1030 |
var_orig = true; |
|
1031 |
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; |
|
1032 |
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; |
|
1033 |
var_dec_const = true; |
|
1034 |
var_dec_value = None; |
|
1035 |
var_type = c.const_type; |
|
1036 |
var_clock = Clocks.new_var false; |
|
1037 |
var_loc = c.const_loc } |
|
1038 |
|
|
1039 |
let mk_new_name used id = |
|
1040 |
let rec new_name name cpt = |
|
1041 |
if used name |
|
1042 |
then new_name (sprintf "_%s_%i" id cpt) (cpt+1) |
|
1043 |
else name |
|
1044 |
in new_name id 1 |
|
1045 |
|
|
1046 |
let mkeq loc (lhs, rhs) = |
|
1047 |
{ eq_lhs = lhs; |
|
1048 |
eq_rhs = rhs; |
|
1049 |
eq_loc = loc } |
|
1050 |
|
|
1051 |
let mkassert loc expr = |
|
1052 |
{ assert_loc = loc; |
|
1053 |
assert_expr = expr |
|
1054 |
} |
|
1055 |
|
|
1056 |
let mktop_decl loc own itf d = |
|
1057 |
{ top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf } |
|
1058 |
|
|
1059 |
let mkpredef_call loc funname args = |
|
1060 |
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) |
|
1061 |
|
|
1062 |
let is_clock_dec_type cty = |
|
1063 |
match cty with |
|
1064 |
| Tydec_clock _ -> true |
|
1065 |
| _ -> false |
|
1066 |
|
|
1067 |
let const_of_top top_decl = |
|
1068 |
match top_decl.top_decl_desc with |
|
1069 |
| Const c -> c |
|
1070 |
| _ -> assert false |
|
1071 |
|
|
1072 |
let node_of_top top_decl = |
|
1073 |
match top_decl.top_decl_desc with |
|
1074 |
| Node nd -> nd |
|
1075 |
| _ -> assert false |
|
1076 |
|
|
1077 |
let imported_node_of_top top_decl = |
|
1078 |
match top_decl.top_decl_desc with |
|
1079 |
| ImportedNode ind -> ind |
|
1080 |
| _ -> assert false |
|
1081 |
|
|
1082 |
let typedef_of_top top_decl = |
|
1083 |
match top_decl.top_decl_desc with |
|
1084 |
| TypeDef tdef -> tdef |
|
1085 |
| _ -> assert false |
|
1086 |
|
|
1087 |
let dependency_of_top top_decl = |
|
1088 |
match top_decl.top_decl_desc with |
|
1089 |
| Open (local, dep) -> (local, dep) |
|
1090 |
| _ -> assert false |
|
1091 |
|
|
1092 |
let consts_of_enum_type top_decl = |
|
1093 |
match top_decl.top_decl_desc with |
|
1094 |
| TypeDef tdef -> |
|
1095 |
(match tdef.tydef_desc with |
|
1096 |
| Tydec_enum tags -> List.map (fun tag -> let cdecl = { const_id = tag; const_loc = top_decl.top_decl_loc; const_value = Const_tag tag; const_type = Type_predef.type_const tdef.tydef_id } in { top_decl with top_decl_desc = Const cdecl }) tags |
|
1097 |
| _ -> []) |
|
1098 |
| _ -> assert false |
|
1099 |
|
|
1100 |
(************************************************************) |
|
1101 |
(* Eexpr functions *) |
|
1102 |
(************************************************************) |
|
1103 |
|
|
1104 |
let merge_node_annot ann1 ann2 = |
|
1105 |
{ requires = ann1.requires @ ann2.requires; |
|
1106 |
ensures = ann1.ensures @ ann2.ensures; |
|
1107 |
behaviors = ann1.behaviors @ ann2.behaviors; |
|
1108 |
spec_loc = ann1.spec_loc |
|
1109 |
} |
|
1110 |
|
|
1111 |
let mkeexpr loc expr = |
|
1112 |
{ eexpr_tag = Utils.new_tag (); |
|
1113 |
eexpr_qfexpr = expr; |
|
1114 |
eexpr_quantifiers = []; |
|
1115 |
eexpr_type = Types.new_var (); |
|
1116 |
eexpr_clock = Clocks.new_var true; |
|
1117 |
eexpr_normalized = None; |
|
1118 |
eexpr_loc = loc } |
|
1119 |
|
|
1120 |
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers } |
|
1121 |
|
|
1122 |
(* |
|
1123 |
let mkepredef_call loc funname args = |
|
1124 |
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None)) |
|
1125 |
|
|
1126 |
let mkepredef_unary_call loc funname arg = |
|
1127 |
mkeexpr loc (EExpr_appl (funname, arg, None)) |
|
1128 |
*) |
|
1129 |
|
|
1130 |
let merge_expr_annot ann1 ann2 = |
|
1131 |
match ann1, ann2 with |
|
1132 |
| None, None -> assert false |
|
1133 |
| Some _, None -> ann1 |
|
1134 |
| None, Some _ -> ann2 |
|
1135 |
| Some ann1, Some ann2 -> Some { |
|
1136 |
annots = ann1.annots @ ann2.annots; |
|
1137 |
annot_loc = ann1.annot_loc |
|
1138 |
} |
|
1139 |
|
|
1140 |
let update_expr_annot node_id e annot = |
|
1141 |
List.iter (fun (key, _) -> |
|
1142 |
Annotations.add_expr_ann node_id e.expr_tag key |
|
1143 |
) annot.annots; |
|
1144 |
{ e with expr_annot = merge_expr_annot e.expr_annot (Some annot) } |
|
1145 |
|
|
1146 |
|
|
1147 |
(***********************************************************) |
|
1148 |
(* Fast access to nodes, by name *) |
|
1149 |
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30 |
|
1150 |
let consts_table = Hashtbl.create 30 |
|
1151 |
|
|
1152 |
let print_node_table fmt () = |
|
1153 |
begin |
|
1154 |
Format.fprintf fmt "{ /* node table */@."; |
|
1155 |
Hashtbl.iter (fun id nd -> |
|
1156 |
Format.fprintf fmt "%s |-> %a" |
|
1157 |
id |
|
1158 |
Printers.pp_short_decl nd |
|
1159 |
) node_table; |
|
1160 |
Format.fprintf fmt "}@." |
|
1161 |
end |
|
1162 |
|
|
1163 |
let print_consts_table fmt () = |
|
1164 |
begin |
|
1165 |
Format.fprintf fmt "{ /* consts table */@."; |
|
1166 |
Hashtbl.iter (fun id const -> |
|
1167 |
Format.fprintf fmt "%s |-> %a" |
|
1168 |
id |
|
1169 |
Printers.pp_const_decl (const_of_top const) |
|
1170 |
) consts_table; |
|
1171 |
Format.fprintf fmt "}@." |
|
1172 |
end |
|
1173 |
|
|
1174 |
let node_name td = |
|
1175 |
match td.top_decl_desc with |
|
1176 |
| Node nd -> nd.node_id |
|
1177 |
| ImportedNode nd -> nd.nodei_id |
|
1178 |
| _ -> assert false |
|
1179 |
|
|
1180 |
let is_generic_node td = |
|
1181 |
match td.top_decl_desc with |
|
1182 |
| Node nd -> List.exists (fun v -> v.var_dec_const) nd.node_inputs |
|
1183 |
| ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs |
|
1184 |
| _ -> assert false |
|
1185 |
|
|
1186 |
let node_inputs td = |
|
1187 |
match td.top_decl_desc with |
|
1188 |
| Node nd -> nd.node_inputs |
|
1189 |
| ImportedNode nd -> nd.nodei_inputs |
|
1190 |
| _ -> assert false |
|
1191 |
|
|
1192 |
let node_from_name id = |
|
1193 |
try |
|
1194 |
Hashtbl.find node_table id |
|
1195 |
with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id; |
|
1196 |
assert false) |
|
1197 |
|
|
1198 |
let is_imported_node td = |
|
1199 |
match td.top_decl_desc with |
|
1200 |
| Node nd -> false |
|
1201 |
| ImportedNode nd -> true |
|
1202 |
| _ -> assert false |
|
1203 |
|
|
1204 |
|
|
1205 |
(* alias and type definition table *) |
|
1206 |
|
|
1207 |
let mktop = mktop_decl Location.dummy_loc Version.include_path false |
|
1208 |
|
|
1209 |
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int}) |
|
1210 |
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool}) |
|
1211 |
let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) |
|
1212 |
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real}) |
|
1213 |
|
|
1214 |
let type_table = |
|
1215 |
Utils.create_hashtable 20 [ |
|
1216 |
Tydec_int , top_int_type; |
|
1217 |
Tydec_bool , top_bool_type; |
|
1218 |
Tydec_float, top_float_type; |
|
1219 |
Tydec_real , top_real_type |
|
1220 |
] |
|
1221 |
|
|
1222 |
let print_type_table fmt () = |
|
1223 |
begin |
|
1224 |
Format.fprintf fmt "{ /* type table */@."; |
|
1225 |
Hashtbl.iter (fun tydec tdef -> |
|
1226 |
Format.fprintf fmt "%a |-> %a" |
|
1227 |
Printers.pp_var_type_dec_desc tydec |
|
1228 |
Printers.pp_typedef (typedef_of_top tdef) |
|
1229 |
) type_table; |
|
1230 |
Format.fprintf fmt "}@." |
|
1231 |
end |
|
1232 |
|
|
1233 |
let rec is_user_type typ = |
|
1234 |
match typ with |
|
1235 |
| Tydec_int | Tydec_bool | Tydec_real |
|
1236 |
| Tydec_float | Tydec_any | Tydec_const _ -> false |
|
1237 |
| Tydec_clock typ' -> is_user_type typ' |
|
1238 |
| _ -> true |
|
1239 |
|
|
1240 |
let get_repr_type typ = |
|
1241 |
let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in |
|
1242 |
if is_user_type typ_def then typ else typ_def |
|
1243 |
|
|
1244 |
let rec coretype_equal ty1 ty2 = |
|
1245 |
let res = |
|
1246 |
match ty1, ty2 with |
|
1247 |
| Tydec_any , _ |
|
1248 |
| _ , Tydec_any -> assert false |
|
1249 |
| Tydec_const _ , Tydec_const _ -> get_repr_type ty1 = get_repr_type ty2 |
|
1250 |
| Tydec_const _ , _ -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc |
|
1251 |
in (not (is_user_type ty1')) && coretype_equal ty1' ty2 |
|
1252 |
| _ , Tydec_const _ -> coretype_equal ty2 ty1 |
|
1253 |
| Tydec_int , Tydec_int |
|
1254 |
| Tydec_real , Tydec_real |
|
1255 |
| Tydec_float , Tydec_float |
|
1256 |
| Tydec_bool , Tydec_bool -> true |
|
1257 |
| Tydec_clock ty1 , Tydec_clock ty2 -> coretype_equal ty1 ty2 |
|
1258 |
| Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2 |
|
1259 |
| Tydec_enum tl1 , Tydec_enum tl2 -> List.sort compare tl1 = List.sort compare tl2 |
|
1260 |
| Tydec_struct fl1 , Tydec_struct fl2 -> |
|
1261 |
List.length fl1 = List.length fl2 |
|
1262 |
&& List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2) |
|
1263 |
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1) |
|
1264 |
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2) |
|
1265 |
| _ -> false |
|
1266 |
in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res) |
|
1267 |
|
|
1268 |
let tag_true = "true" |
|
1269 |
let tag_false = "false" |
|
1270 |
let tag_default = "default" |
|
1271 |
|
|
1272 |
let const_is_bool c = |
|
1273 |
match c with |
|
1274 |
| Const_tag t -> t = tag_true || t = tag_false |
|
1275 |
| _ -> false |
|
1276 |
|
|
1277 |
(* Computes the negation of a boolean constant *) |
|
1278 |
let const_negation c = |
|
1279 |
assert (const_is_bool c); |
|
1280 |
match c with |
|
1281 |
| Const_tag t when t = tag_true -> Const_tag tag_false |
|
1282 |
| _ -> Const_tag tag_true |
|
1283 |
|
|
1284 |
let const_or c1 c2 = |
|
1285 |
assert (const_is_bool c1 && const_is_bool c2); |
|
1286 |
match c1, c2 with |
|
1287 |
| Const_tag t1, _ when t1 = tag_true -> c1 |
|
1288 |
| _ , Const_tag t2 when t2 = tag_true -> c2 |
|
1289 |
| _ -> Const_tag tag_false |
|
1290 |
|
|
1291 |
let const_and c1 c2 = |
|
1292 |
assert (const_is_bool c1 && const_is_bool c2); |
|
1293 |
match c1, c2 with |
|
1294 |
| Const_tag t1, _ when t1 = tag_false -> c1 |
|
1295 |
| _ , Const_tag t2 when t2 = tag_false -> c2 |
|
1296 |
| _ -> Const_tag tag_true |
|
1297 |
|
|
1298 |
let const_xor c1 c2 = |
|
1299 |
assert (const_is_bool c1 && const_is_bool c2); |
|
1300 |
match c1, c2 with |
|
1301 |
| Const_tag t1, Const_tag t2 when t1 <> t2 -> Const_tag tag_true |
|
1302 |
| _ -> Const_tag tag_false |
|
1303 |
|
|
1304 |
let const_impl c1 c2 = |
|
1305 |
assert (const_is_bool c1 && const_is_bool c2); |
|
1306 |
match c1, c2 with |
|
1307 |
| Const_tag t1, _ when t1 = tag_false -> Const_tag tag_true |
|
1308 |
| _ , Const_tag t2 when t2 = tag_true -> Const_tag tag_true |
|
1309 |
| _ -> Const_tag tag_false |
|
1310 |
|
|
1311 |
(* To guarantee uniqueness of tags in enum types *) |
|
1312 |
let tag_table = |
|
1313 |
Utils.create_hashtable 20 [ |
|
1314 |
tag_true, top_bool_type; |
|
1315 |
tag_false, top_bool_type |
|
1316 |
] |
|
1317 |
|
|
1318 |
(* To guarantee uniqueness of fields in struct types *) |
|
1319 |
let field_table = |
|
1320 |
Utils.create_hashtable 20 [ |
|
1321 |
] |
|
1322 |
|
|
1323 |
let get_enum_type_tags cty = |
|
1324 |
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*) |
|
1325 |
match cty with |
|
1326 |
| Tydec_bool -> [tag_true; tag_false] |
|
1327 |
| Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
|
1328 |
| Tydec_enum tl -> tl |
|
1329 |
| _ -> assert false) |
|
1330 |
| _ -> assert false |
|
1331 |
|
|
1332 |
let get_struct_type_fields cty = |
Also available in: Unified diff