## lustrec / src / inliner.ml @ 68601cf5

History | View | Annotate | Download (19.3 KB)

1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|

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 | b09a175c | ploc | open LustreSpec |

13 | open Corelang |
||

14 | 566dbf49 | ploc | open Utils |

15 | |||

16 | (* Local annotations are declared with the following key /inlining/: true *) |
||

17 | let keyword = ["inlining"] |
||

18 | |||

19 | let is_inline_expr expr = |
||

20 | match expr.expr_annot with |
||

21 | | Some ann -> |
||

22 | List.exists (fun (key, value) -> key = keyword) ann.annots |
||

23 | | None -> false |
||

24 | b09a175c | ploc | |

25 | let check_node_name id = (fun t -> |
||

26 | match t.top_decl_desc with |
||

27 | | Node nd -> nd.node_id = id |
||

28 | | _ -> false) |
||

29 | |||

30 | fc886259 | xthirioux | let is_node_var node v = |

31 | try |
||

32 | ignore (Corelang.get_node_var v node); true |
||

33 | with Not_found -> false |
||

34 | b09a175c | ploc | |

35 | af5af1e8 | ploc | let rename_expr rename expr = expr_replace_var rename expr |

36 | fc886259 | xthirioux | |

37 | af5af1e8 | ploc | let rename_eq rename eq = |

38 | { eq with |
||

39 | eq_lhs = List.map rename eq.eq_lhs; |
||

40 | eq_rhs = rename_expr rename eq.eq_rhs |
||

41 | } |
||

42 | 45f0f48d | xthirioux | |

43 | let rec add_expr_reset_cond cond expr = |
||

44 | let aux = add_expr_reset_cond cond in |
||

45 | let new_desc = |
||

46 | match expr.expr_desc with |
||

47 | | Expr_const _ |
||

48 | | Expr_ident _ -> expr.expr_desc |
||

49 | | Expr_tuple el -> Expr_tuple (List.map aux el) |
||

50 | | Expr_ite (c, t, e) -> Expr_ite (aux c, aux t, aux e) |
||

51 | |||

52 | | Expr_arrow (e1, e2) -> |
||

53 | (* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *) |
||

54 | let e1 = aux e1 and e2 = aux e2 in |
||

55 | (* inlining is performed before typing. we can leave the fields free *) |
||

56 | let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in |
||

57 | Expr_arrow (e1, new_e2) |
||

58 | |||

59 | | Expr_fby _ -> assert false (* TODO: deal with fby. This hasn't been much handled yet *) |
||

60 | |||

61 | | Expr_array el -> Expr_array (List.map aux el) |
||

62 | | Expr_access (e, dim) -> Expr_access (aux e, dim) |
||

63 | | Expr_power (e, dim) -> Expr_power (aux e, dim) |
||

64 | | Expr_pre e -> Expr_pre (aux e) |
||

65 | | Expr_when (e, id, l) -> Expr_when (aux e, id, l) |
||

66 | | Expr_merge (id, cases) -> Expr_merge (id, List.map (fun (l,e) -> l, aux e) cases) |
||

67 | |||

68 | | Expr_appl (id, args, reset_opt) -> |
||

69 | (* we "add" cond to the reset field. *) |
||

70 | let new_reset = match reset_opt with |
||

71 | None -> cond |
||

72 | | Some cond' -> mkpredef_call cond'.expr_loc "||" [cond; cond'] |
||

73 | in |
||

74 | Expr_appl (id, args, Some new_reset) |
||

75 | |||

76 | |||

77 | in |
||

78 | { expr with expr_desc = new_desc } |
||

79 | |||

80 | let add_eq_reset_cond cond eq = |
||

81 | { eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs } |
||

82 | ec433d69 | xthirioux | (* |

83 | let get_static_inputs input_arg_list = |
||

84 | List.fold_right (fun (vdecl, arg) res -> |
||

85 | if vdecl.var_dec_const |
||

86 | then (vdecl.var_id, Corelang.dimension_of_expr arg) :: res |
||

87 | else res) |
||

88 | input_arg_list [] |
||

89 | |||

90 | let get_carrier_inputs input_arg_list = |
||

91 | List.fold_right (fun (vdecl, arg) res -> |
||

92 | if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc |
||

93 | then (vdecl.var_id, ident_of_expr arg) :: res |
||

94 | else res) |
||

95 | input_arg_list [] |
||

96 | *) |
||

97 | b09a175c | ploc | (* |

98 | fc886259 | xthirioux | expr, locals', eqs = inline_call id args' reset locals node nodes |

99 | b09a175c | ploc | |

100 | We select the called node equations and variables. |
||

101 | renamed_inputs = args |
||

102 | renamed_eqs |
||

103 | |||

104 | the resulting expression is tuple_of_renamed_outputs |
||

105 | |||

106 | TODO: convert the specification/annotation/assert and inject them |
||

107 | *) |
||

108 | 45f0f48d | xthirioux | (** [inline_call node loc uid args reset locals caller] returns a tuple (expr, |

109 | locals, eqs, asserts) |
||

110 | *) |
||

111 | let inline_call node loc uid args reset locals caller = |
||

112 | 9603460e | xthirioux | let rename v = |

113 | fc886259 | xthirioux | if v = tag_true || v = tag_false || not (is_node_var node v) then v else |

114 | Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v) |
||

115 | b09a175c | ploc | in |

116 | ec433d69 | xthirioux | let eqs' = List.map (rename_eq rename) (get_node_eqs node) in |

117 | let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in |
||

118 | let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) -> vdecl.var_dec_const) input_arg_list in |
||

119 | let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in |
||

120 | let carrier_inputs, other_inputs = List.partition (fun (vdecl, arg) -> Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc) dynamic_inputs in |
||

121 | let carrier_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) carrier_inputs in |
||

122 | fc886259 | xthirioux | let rename_static v = |

123 | try |
||

124 | ec433d69 | xthirioux | snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs) |

125 | with Not_found -> Dimension.mkdim_ident loc v in |
||

126 | fc886259 | xthirioux | let rename_carrier v = |

127 | try |
||

128 | ec433d69 | xthirioux | snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs) |

129 | fc886259 | xthirioux | with Not_found -> v in |

130 | let rename_var v = |
||

131 | ec433d69 | xthirioux | let vdecl = |

132 | Corelang.mkvar_decl v.var_loc |
||

133 | (rename v.var_id, |
||

134 | { v.var_dec_type with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc }, |
||

135 | { v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc }, |
||

136 | v.var_dec_const, |
||

137 | Utils.option_map (rename_expr rename) v.var_dec_value) in |
||

138 | begin |
||

139 | 45f0f48d | xthirioux | (* |

140 | (try |
||

141 | Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs); |
||

142 | Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ())) |
||

143 | with Not_found -> ()); |
||

144 | (try |
||

145 | Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true)) |
||

146 | with Not_found -> ()); |
||

147 | (*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*) |
||

148 | *) |
||

149 | ec433d69 | xthirioux | vdecl |

150 | end |
||

151 | 01d48bb0 | xthirioux | (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*) |

152 | ec433d69 | xthirioux | in |

153 | let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in |
||

154 | b09a175c | ploc | let outputs' = List.map rename_var node.node_outputs in |

155 | ec433d69 | xthirioux | let locals' = |

156 | 01d48bb0 | xthirioux | (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs) |

157 | ec433d69 | xthirioux | @ (List.map rename_var node.node_locals) |

158 | 01d48bb0 | xthirioux | in |

159 | b09a175c | ploc | (* checking we are at the appropriate (early) step: node_checks and |

160 | node_gencalls should be empty (not yet assigned) *) |
||

161 | assert (node.node_checks = []); |
||

162 | assert (node.node_gencalls = []); |
||

163 | |||

164 | 45f0f48d | xthirioux | (* Expressing reset locally in equations *) |

165 | let eqs_r' = |
||

166 | match reset with |
||

167 | None -> eqs' |
||

168 | | Some cond -> List.map (add_eq_reset_cond cond) eqs' |
||

169 | in |
||

170 | let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', |
||

171 | expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in |
||

172 | fc886259 | xthirioux | let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') |

173 | b09a175c | ploc | in |

174 | af5af1e8 | ploc | let asserts' = (* We rename variables in assert expressions *) |

175 | List.map |
||

176 | (fun a -> |
||

177 | {a with assert_expr = |
||

178 | let expr = a.assert_expr in |
||

179 | rename_expr rename expr |
||

180 | 45f0f48d | xthirioux | }) |

181 | af5af1e8 | ploc | node.node_asserts |

182 | in |
||

183 | 04a63d25 | xthirioux | let annots' = |

184 | Plugins.inline_annots rename node.node_annot |
||

185 | in |
||

186 | af5af1e8 | ploc | expr, |

187 | inputs'@outputs'@locals'@locals, |
||

188 | 45f0f48d | xthirioux | assign_inputs::eqs_r', |

189 | 04a63d25 | xthirioux | asserts', |

190 | annots' |
||

191 | b09a175c | ploc | |

192 | |||

193 | |||

194 | fc886259 | xthirioux | let inline_table = Hashtbl.create 23 |

195 | b09a175c | ploc | |

196 | (* |
||

197 | fc886259 | xthirioux | new_expr, new_locals, new_eqs = inline_expr expr locals node nodes |

198 | b09a175c | ploc | |

199 | Each occurence of a node in nodes in the expr should be replaced by fresh |
||

200 | variables and the code of called node instance added to new_eqs |
||

201 | |||

202 | *) |
||

203 | fc886259 | xthirioux | let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes = |

204 | 566dbf49 | ploc | let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |

205 | let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in |
||

206 | b09a175c | ploc | let inline_tuple el = |

207 | 04a63d25 | xthirioux | List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) -> |

208 | let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in |
||

209 | e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots' |
||

210 | ) el ([], locals, [], [], []) |
||

211 | b09a175c | ploc | in |

212 | let inline_pair e1 e2 = |
||

213 | 04a63d25 | xthirioux | let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in |

214 | b09a175c | ploc | match el' with |

215 | d2d9d4cb | ploc | | [e1'; e2'] -> e1', e2', l', eqs', asserts', annots' |

216 | b09a175c | ploc | | _ -> assert false |

217 | in |
||

218 | let inline_triple e1 e2 e3 = |
||

219 | 04a63d25 | xthirioux | let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in |

220 | b09a175c | ploc | match el' with |

221 | 04a63d25 | xthirioux | | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts', annots' |

222 | b09a175c | ploc | | _ -> assert false |

223 | in |
||

224 | 566dbf49 | ploc | |

225 | b09a175c | ploc | match expr.expr_desc with |

226 | | Expr_appl (id, args, reset) -> |
||

227 | 04a63d25 | xthirioux | let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in |

228 | 566dbf49 | ploc | if List.exists (check_node_name id) nodes && (* the current node call is provided |

229 | as arguments nodes *) |
||

230 | (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, |
||

231 | it is explicitely inlined here *) |
||

232 | 264a4844 | ploc | then ( |

233 | (* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *) |
||

234 | b09a175c | ploc | (* The node should be inlined *) |

235 | fc886259 | xthirioux | (* let _ = Format.eprintf "Inlining call to %s@." id in *) |

236 | let called = try List.find (check_node_name id) nodes |
||

237 | b09a175c | ploc | with Not_found -> (assert false) in |

238 | fc886259 | xthirioux | let called = node_of_top called in |

239 | let called' = inline_node called nodes in |
||

240 | 04a63d25 | xthirioux | let expr, locals', eqs'', asserts'', annots'' = |

241 | 45f0f48d | xthirioux | inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in |

242 | 04a63d25 | xthirioux | expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots'' |

243 | 264a4844 | ploc | ) |

244 | b09a175c | ploc | else |

245 | (* let _ = Format.eprintf "Not inlining call to %s@." id in *) |
||

246 | af5af1e8 | ploc | { expr with expr_desc = Expr_appl(id, args', reset)}, |

247 | locals', |
||

248 | eqs', |
||

249 | 04a63d25 | xthirioux | asserts', |

250 | annots' |
||

251 | b09a175c | ploc | |

252 | (* For other cases, we just keep the structure, but convert sub-expressions *) |
||

253 | | Expr_const _ |
||

254 | 04a63d25 | xthirioux | | Expr_ident _ -> expr, locals, [], [], [] |

255 | b09a175c | ploc | | Expr_tuple el -> |

256 | 04a63d25 | xthirioux | let el', l', eqs', asserts', annots' = inline_tuple el in |

257 | { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots' |
||

258 | b09a175c | ploc | | Expr_ite (g, t, e) -> |

259 | 04a63d25 | xthirioux | let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in |

260 | { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots' |
||

261 | b09a175c | ploc | | Expr_arrow (e1, e2) -> |

262 | 04a63d25 | xthirioux | let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in |

263 | { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots' |
||

264 | b09a175c | ploc | | Expr_fby (e1, e2) -> |

265 | 04a63d25 | xthirioux | let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in |

266 | { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots' |
||

267 | b09a175c | ploc | | Expr_array el -> |

268 | 04a63d25 | xthirioux | let el', l', eqs', asserts', annots' = inline_tuple el in |

269 | { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots' |
||

270 | b09a175c | ploc | | Expr_access (e, dim) -> |

271 | 04a63d25 | xthirioux | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |

272 | { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots' |
||

273 | b09a175c | ploc | | Expr_power (e, dim) -> |

274 | 04a63d25 | xthirioux | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |

275 | { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots' |
||

276 | b09a175c | ploc | | Expr_pre e -> |

277 | 04a63d25 | xthirioux | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |

278 | { expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots' |
||

279 | b09a175c | ploc | | Expr_when (e, id, label) -> |

280 | 04a63d25 | xthirioux | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |

281 | { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots' |
||

282 | b09a175c | ploc | | Expr_merge (id, branches) -> |

283 | 04a63d25 | xthirioux | let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in |

284 | b09a175c | ploc | let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |

285 | 04a63d25 | xthirioux | { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots' |

286 | fc886259 | xthirioux | |

287 | and inline_node ?(selection_on_annotation=false) node nodes = |
||

288 | ec433d69 | xthirioux | try copy_node (Hashtbl.find inline_table node.node_id) |

289 | fc886259 | xthirioux | with Not_found -> |

290 | 566dbf49 | ploc | let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |

291 | 04a63d25 | xthirioux | let new_locals, eqs, asserts, annots = |

292 | List.fold_left (fun (locals, eqs, asserts, annots) eq -> |
||

293 | let eq_rhs', locals', new_eqs', asserts', annots' = |
||

294 | fc886259 | xthirioux | inline_expr eq.eq_rhs locals node nodes |

295 | b09a175c | ploc | in |

296 | 04a63d25 | xthirioux | locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts, annots'@annots |

297 | ) (node.node_locals, [], node.node_asserts, node.node_annot) (get_node_eqs node) |
||

298 | b09a175c | ploc | in |

299 | fc886259 | xthirioux | let inlined = |

300 | { node with |
||

301 | b09a175c | ploc | node_locals = new_locals; |

302 | b08ffca7 | xthirioux | node_stmts = List.map (fun eq -> Eq eq) eqs; |

303 | af5af1e8 | ploc | node_asserts = asserts; |

304 | 04a63d25 | xthirioux | node_annot = annots; |

305 | b09a175c | ploc | } |

306 | fc886259 | xthirioux | in |

307 | begin |
||

308 | (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*) |
||

309 | Hashtbl.add inline_table node.node_id inlined; |
||

310 | inlined |
||

311 | end |
||

312 | b09a175c | ploc | |

313 | let inline_all_calls node nodes = |
||

314 | let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
||

315 | { node with top_decl_desc = Node (inline_node nd nodes) } |
||

316 | |||

317 | |||

318 | |||

319 | |||

320 | |||

321 | 592f508c | ploc | let witness filename main_name orig inlined type_env clock_env = |

322 | b09a175c | ploc | let loc = Location.dummy_loc in |

323 | let rename_local_node nodes prefix id = |
||

324 | if List.exists (check_node_name id) nodes then |
||

325 | prefix ^ id |
||

326 | else |
||

327 | id |
||

328 | in |
||

329 | let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with |
||

330 | Node nd -> nd | _ -> assert false in |
||

331 | |||

332 | let orig_rename = rename_local_node orig "orig_" in |
||

333 | let inlined_rename = rename_local_node inlined "inlined_" in |
||

334 | let identity = (fun x -> x) in |
||

335 | let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in |
||

336 | let orig = rename_prog orig_rename identity identity orig in |
||

337 | let inlined = rename_prog inlined_rename identity identity inlined in |
||

338 | let nodes_origs, others = List.partition is_node orig in |
||

339 | let nodes_inlined, _ = List.partition is_node inlined in |
||

340 | |||

341 | b50c665d | ploc | (* One ok_i boolean variable per output var *) |

342 | let nb_outputs = List.length main_orig_node.node_outputs in |
||

343 | ec433d69 | xthirioux | let ok_ident = "OK" in |

344 | b50c665d | ploc | let ok_i = List.map (fun id -> |

345 | mkvar_decl |
||

346 | loc |
||

347 | ec433d69 | xthirioux | (Format.sprintf "%s_%i" ok_ident id, |

348 | b50c665d | ploc | {ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, |

349 | {ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, |
||

350 | ec433d69 | xthirioux | false, |

351 | None) |
||

352 | b50c665d | ploc | ) (Utils.enumerate nb_outputs) |

353 | in |
||

354 | |||

355 | (* OK = ok_1 and ok_2 and ... ok_n-1 *) |
||

356 | b09a175c | ploc | let ok_output = mkvar_decl |

357 | loc |
||

358 | (ok_ident, |
||

359 | {ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, |
||

360 | {ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, |
||

361 | ec433d69 | xthirioux | false, |

362 | None) |
||

363 | b09a175c | ploc | in |

364 | b50c665d | ploc | let main_ok_expr = |

365 | let mkv x = mkexpr loc (Expr_ident x) in |
||

366 | match ok_i with |
||

367 | | [] -> assert false |
||

368 | | [x] -> mkv x.var_id |
||

369 | | hd::tl -> |
||

370 | List.fold_left (fun accu elem -> |
||

371 | mkpredef_call loc "&&" [mkv elem.var_id; accu] |
||

372 | ) (mkv hd.var_id) tl |
||

373 | in |
||

374 | |||

375 | (* Building main node *) |
||

376 | |||

377 | b08ffca7 | xthirioux | let ok_i_eq = |

378 | { eq_loc = loc; |
||

379 | eq_lhs = List.map (fun v -> v.var_id) ok_i; |
||

380 | eq_rhs = |
||

381 | let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in |
||

382 | let call_orig = |
||

383 | mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in |
||

384 | let call_inlined = |
||

385 | mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in |
||

386 | let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in |
||

387 | mkexpr loc (Expr_appl ("=", args, None)) |
||

388 | } in |
||

389 | let ok_eq = |
||

390 | { eq_loc = loc; |
||

391 | eq_lhs = [ok_ident]; |
||

392 | eq_rhs = main_ok_expr; |
||

393 | } in |
||

394 | b09a175c | ploc | let main_node = { |

395 | node_id = "check"; |
||

396 | node_type = Types.new_var (); |
||

397 | node_clock = Clocks.new_var true; |
||

398 | node_inputs = main_orig_node.node_inputs; |
||

399 | node_outputs = [ok_output]; |
||

400 | 9603460e | xthirioux | node_locals = ok_i; |

401 | b09a175c | ploc | node_gencalls = []; |

402 | node_checks = []; |
||

403 | node_asserts = []; |
||

404 | b08ffca7 | xthirioux | node_stmts = [Eq ok_i_eq; Eq ok_eq]; |

405 | 3ab5748b | ploc | node_dec_stateless = false; |

406 | 52cfee34 | xthirioux | node_stateless = None; |

407 | b09a175c | ploc | node_spec = Some |

408 | {requires = []; |
||

409 | 01c7d5e1 | ploc | ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))]; |

410 | behaviors = []; |
||

411 | spec_loc = loc |
||

412 | b09a175c | ploc | }; |

413 | 01c7d5e1 | ploc | node_annot = []; |

414 | b09a175c | ploc | } |

415 | in |
||

416 | ef34b4ae | xthirioux | let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in |

417 | b09a175c | ploc | let new_prog = others@nodes_origs@nodes_inlined@main in |

418 | 04a63d25 | xthirioux | (* |

419 | let _ = Typing.type_prog type_env new_prog in |
||

420 | let _ = Clock_calculus.clock_prog clock_env new_prog in |
||

421 | *) |
||

422 | |||

423 | 1bff14ac | ploc | let witness_file = (Options_management.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in |

424 | b09a175c | ploc | let witness_out = open_out witness_file in |

425 | let witness_fmt = Format.formatter_of_out_channel witness_out in |
||

426 | ec433d69 | xthirioux | begin |

427 | List.iter (fun vdecl -> Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) (ok_output::ok_i); |
||

428 | Format.fprintf witness_fmt |
||

429 | "(* Generated lustre file to check validity of inlining process *)@."; |
||

430 | Printers.pp_prog witness_fmt new_prog; |
||

431 | Format.fprintf witness_fmt "@."; |
||

432 | () |
||

433 | end (* xx *) |
||

434 | b09a175c | ploc | |

435 | 592f508c | ploc | let global_inline basename prog type_env clock_env = |

436 | b09a175c | ploc | (* We select the main node desc *) |

437 | let main_node, other_nodes, other_tops = |
||

438 | ec433d69 | xthirioux | List.fold_right |

439 | (fun top (main_opt, nodes, others) -> |
||

440 | b09a175c | ploc | match top.top_decl_desc with |

441 | | Node nd when nd.node_id = !Options.main_node -> |
||

442 | Some top, nodes, others |
||

443 | | Node _ -> main_opt, top::nodes, others |
||

444 | | _ -> main_opt, nodes, top::others) |
||

445 | ec433d69 | xthirioux | prog (None, [], []) |

446 | b09a175c | ploc | in |

447 | 85da3a4b | ploc | |

448 | b09a175c | ploc | (* Recursively each call of a node in the top node is replaced *) |

449 | let main_node = Utils.desome main_node in |
||

450 | let main_node' = inline_all_calls main_node other_nodes in |
||

451 | ec433d69 | xthirioux | let res = List.map (fun top -> if check_node_name !Options.main_node top then main_node' else top) prog in |

452 | 85da3a4b | ploc | (* Code snippet from unstable branch. May be used when reactivating witnesses. |

453 | let res = main_node'::other_tops in |
||

454 | 53206908 | xthirioux | if !Options.witnesses then ( |

455 | witness |
||

456 | basename |
||

457 | (match main_node.top_decl_desc with Node nd -> nd.node_id | _ -> assert false) |
||

458 | prog res type_env clock_env |
||

459 | ); |
||

460 | 85da3a4b | ploc | *) |

461 | b09a175c | ploc | res |

462 | b50c665d | ploc | |

463 | 264a4844 | ploc | let pp_inline_calls fmt prog = |

464 | 566dbf49 | ploc | let local_anns = Annotations.get_expr_annotations keyword in |

465 | 264a4844 | ploc | let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in |

466 | Format.fprintf fmt "@[<v 0>Inlined expresssions in node (by tags):@ %a@]" |
||

467 | (fprintf_list ~sep:"" |
||

468 | (fun fmt top -> |
||

469 | match top.top_decl_desc with |
||

470 | | Node nd when ISet.mem nd.node_id nodes_with_anns -> |
||

471 | Format.fprintf fmt "%s: {@[<v 0>%a}@]@ " |
||

472 | nd.node_id |
||

473 | (fprintf_list ~sep:"@ " (fun fmt tag -> Format.fprintf fmt "%i" tag)) |
||

474 | (List.fold_left |
||

475 | (fun accu (id, tag) -> if id = nd.node_id then tag::accu else accu) |
||

476 | [] |
||

477 | local_anns |
||

478 | ) |
||

479 | (* | Node nd -> Format.fprintf fmt "%s: no inline annotations" nd.node_id *) |
||

480 | | _ -> () |
||

481 | )) |
||

482 | prog |
||

483 | |||

484 | |||

485 | let local_inline prog (* type_env clock_env *) = |
||

486 | Log.report ~level:2 (fun fmt -> Format.fprintf fmt ".. @[<v 2>Inlining@,"); |
||

487 | let local_anns = Annotations.get_expr_annotations keyword in |
||

488 | let prog = |
||

489 | if local_anns != [] then ( |
||

490 | let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in |
||

491 | ISet.iter (fun node_id -> Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Node %s has local expression annotations@ " node_id)) |
||

492 | nodes_with_anns; |
||

493 | List.fold_right (fun top accu -> |
||

494 | ( match top.top_decl_desc with |
||

495 | | Node nd when ISet.mem nd.node_id nodes_with_anns -> |
||

496 | Log.report ~level:2 (fun fmt -> Format.fprintf fmt "[local inline] Processing node %s@ " nd.node_id); |
||

497 | let inlined_node = inline_node ~selection_on_annotation:true nd prog in |
||

498 | (* Format.eprintf "Before inline@.%a@.After:@.%a@." *) |
||

499 | (* Printers.pp_node nd *) |
||

500 | (* Printers.pp_node inlined_node; *) |
||

501 | { top with top_decl_desc = Node inlined_node } |
||

502 | |||

503 | | _ -> top |
||

504 | )::accu) prog [] |
||

505 | |||

506 | ) |
||

507 | else ( |
||

508 | Log.report ~level:2 (fun fmt -> Format.fprintf fmt "No local inline information!@ "); |
||

509 | prog |
||

510 | ) |
||

511 | in |
||

512 | Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@]@,"); |
||

513 | 566dbf49 | ploc | prog |

514 | |||

515 | b50c665d | ploc | (* Local Variables: *) |

516 | (* compile-command:"make -C .." *) |
||

517 | (* End: *) |