## lustrec / src / inliner.ml @ e7cc5186

History | View | Annotate | Download (17.9 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 | then |
||

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

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

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

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

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

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

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

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

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

242 | b09a175c | ploc | else |

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

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

245 | locals', |
||

246 | eqs', |
||

247 | 04a63d25 | xthirioux | asserts', |

248 | annots' |
||

249 | b09a175c | ploc | |

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

251 | | Expr_const _ |
||

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

253 | b09a175c | ploc | | Expr_tuple el -> |

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

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

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

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

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

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

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

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

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

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

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

265 | b09a175c | ploc | | Expr_array el -> |

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

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

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

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

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

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

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

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

274 | b09a175c | ploc | | Expr_pre e -> |

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

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

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

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

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

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

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

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

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

284 | fc886259 | xthirioux | |

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

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

287 | fc886259 | xthirioux | with Not_found -> |

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

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

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

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

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

293 | b09a175c | ploc | in |

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

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

296 | b09a175c | ploc | in |

297 | fc886259 | xthirioux | let inlined = |

298 | { node with |
||

299 | b09a175c | ploc | node_locals = new_locals; |

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

301 | af5af1e8 | ploc | node_asserts = asserts; |

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

303 | b09a175c | ploc | } |

304 | fc886259 | xthirioux | in |

305 | begin |
||

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

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

308 | inlined |
||

309 | end |
||

310 | b09a175c | ploc | |

311 | let inline_all_calls node nodes = |
||

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

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

314 | |||

315 | |||

316 | |||

317 | |||

318 | |||

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

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

321 | let rename_local_node nodes prefix id = |
||

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

323 | prefix ^ id |
||

324 | else |
||

325 | id |
||

326 | in |
||

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

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

329 | |||

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

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

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

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

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

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

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

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

338 | |||

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

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

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

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

343 | mkvar_decl |
||

344 | loc |
||

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

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

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

348 | ec433d69 | xthirioux | false, |

349 | None) |
||

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

351 | in |
||

352 | |||

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

354 | b09a175c | ploc | let ok_output = mkvar_decl |

355 | loc |
||

356 | (ok_ident, |
||

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

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

359 | ec433d69 | xthirioux | false, |

360 | None) |
||

361 | b09a175c | ploc | in |

362 | b50c665d | ploc | let main_ok_expr = |

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

364 | match ok_i with |
||

365 | | [] -> assert false |
||

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

367 | | hd::tl -> |
||

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

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

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

371 | in |
||

372 | |||

373 | (* Building main node *) |
||

374 | |||

375 | b08ffca7 | xthirioux | let ok_i_eq = |

376 | { eq_loc = loc; |
||

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

378 | eq_rhs = |
||

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

380 | let call_orig = |
||

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

382 | let call_inlined = |
||

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

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

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

386 | } in |
||

387 | let ok_eq = |
||

388 | { eq_loc = loc; |
||

389 | eq_lhs = [ok_ident]; |
||

390 | eq_rhs = main_ok_expr; |
||

391 | } in |
||

392 | b09a175c | ploc | let main_node = { |

393 | node_id = "check"; |
||

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

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

396 | node_inputs = main_orig_node.node_inputs; |
||

397 | node_outputs = [ok_output]; |
||

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

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

400 | node_checks = []; |
||

401 | node_asserts = []; |
||

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

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

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

405 | b09a175c | ploc | node_spec = Some |

406 | {requires = []; |
||

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

408 | behaviors = []; |
||

409 | spec_loc = loc |
||

410 | b09a175c | ploc | }; |

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

412 | b09a175c | ploc | } |

413 | in |
||

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

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

416 | 04a63d25 | xthirioux | (* |

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

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

419 | *) |
||

420 | |||

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

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

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

424 | ec433d69 | xthirioux | begin |

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

426 | Format.fprintf witness_fmt |
||

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

428 | Printers.pp_prog witness_fmt new_prog; |
||

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

430 | () |
||

431 | end (* xx *) |
||

432 | b09a175c | ploc | |

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

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

435 | let main_node, other_nodes, other_tops = |
||

436 | ec433d69 | xthirioux | List.fold_right |

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

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

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

440 | Some top, nodes, others |
||

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

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

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

444 | b09a175c | ploc | in |

445 | 85da3a4b | ploc | |

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

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

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

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

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

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

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

453 | witness |
||

454 | basename |
||

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

456 | prog res type_env clock_env |
||

457 | ); |
||

458 | 85da3a4b | ploc | *) |

459 | b09a175c | ploc | res |

460 | b50c665d | ploc | |

461 | 566dbf49 | ploc | let local_inline basename prog type_env clock_env = |

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

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

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

465 | ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns; |
||

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

467 | ( match top.top_decl_desc with |
||

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

469 | { top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) } |
||

470 | | _ -> top |
||

471 | )::accu) prog [] |
||

472 | |||

473 | ) |
||

474 | else |
||

475 | prog |
||

476 | |||

477 | |||

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

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

480 | (* End: *) |