Project

General

Profile

« Previous | Next » 

Revision 333e3a25

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

[general] Refactor get_node_eqs to produce (eqs, auts) with automatons

View differences:

src/inliner.ml
32 32
   ignore (Corelang.get_node_var v node); true
33 33
 with Not_found -> false
34 34

  
35
let rename_expr rename expr = expr_replace_var rename expr
36

  
35
(* let rename_expr rename expr = expr_replace_var rename expr *)
36
(*
37 37
let rename_eq rename eq = 
38 38
  { eq with
39 39
    eq_lhs = List.map rename eq.eq_lhs; 
40 40
    eq_rhs = rename_expr rename eq.eq_rhs
41 41
  }
42

  
42
*)
43
   
43 44
let rec add_expr_reset_cond cond expr =
44 45
  let aux = add_expr_reset_cond cond in
45 46
  let new_desc = 
......
113 114
    if v = tag_true || v = tag_false || not (is_node_var node v) then v else
114 115
      Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
115 116
  in
116
  let eqs' = List.map (rename_eq rename) (get_node_eqs node) in
117
  let eqs, auts = get_node_eqs node in
118
  let eqs' = List.map (rename_eq (fun x -> x) rename) eqs in
119
  let auts' = List.map (rename_aut (fun x -> x) rename) auts in
117 120
  let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in
118 121
  let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) -> vdecl.var_dec_const) input_arg_list in
119 122
  let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in
......
134 137
	 { v.var_dec_type  with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc },
135 138
	 { v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc },
136 139
	 v.var_dec_const,
137
	 Utils.option_map (rename_expr rename) v.var_dec_value) in
140
	 Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value) in
138 141
    begin
139 142
      (*
140 143
	(try
......
162 165
  assert (node.node_gencalls = []);
163 166

  
164 167
  (* Expressing reset locally in equations *)
165
  let eqs_r' =
168
  let eqs_r' = 
169
    let all_eqs = (List.map (fun eq -> Eq eq) eqs') @ (List.map (fun aut -> Aut aut) auts') in
166 170
    match reset with
167
      None -> eqs'
168
    | Some cond -> List.map (add_eq_reset_cond cond) eqs'
171
      None -> all_eqs
172
    | Some cond -> (
173
      assert (auts' = []); (* TODO: we do not handle properly automaton in case of reset call *)
174
      List.map (fun eq -> Eq (add_eq_reset_cond cond eq)) eqs'
175
    )
169 176
  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
177
  let assign_inputs = Eq (mkeq loc (List.map (fun v -> v.var_id) inputs',
178
                                expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs))) in
172 179
  let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
173 180
  in
174 181
  let asserts' = (* We rename variables in assert expressions *)
......
176 183
      (fun a -> 
177 184
	{a with assert_expr = 
178 185
	    let expr = a.assert_expr in
179
	    rename_expr rename expr
186
	    rename_expr (fun x -> x) rename expr
180 187
	})
181 188
      node.node_asserts 
182 189
  in
......
224 231
  
225 232
  match expr.expr_desc with
226 233
  | Expr_appl (id, args, reset) ->
227
    let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in 
228
    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
      (* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *)
234
      (* The node should be inlined *)
235
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
236
      let called = try List.find (check_node_name id) nodes 
237
	with Not_found -> (assert false) in
238
      let called = node_of_top called in
239
      let called' = inline_node called nodes in
240
      let expr, locals', eqs'', asserts'', annots'' = 
241
	inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
242
      expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
243
    )
244
    else 
245
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
246
      { expr with expr_desc = Expr_appl(id, args', reset)}, 
247
      locals', 
248
      eqs', 
249
      asserts',
250
      annots'
234
     let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in 
235
     if List.exists (check_node_name id) nodes && (* the current node call is provided
236
						     as arguments nodes *)
237
       (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 
238
							       it is explicitely inlined here *)
239
     then (
240
       (* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *)
241
       (* The node should be inlined *)
242
       (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
243
       let called = try List.find (check_node_name id) nodes 
244
	 with Not_found -> (assert false) in
245
       let called = node_of_top called in
246
       let called' = inline_node called nodes in
247
       let expr, locals', eqs'', asserts'', annots'' = 
248
	 inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
249
       expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
250
     )
251
     else 
252
       (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
253
       { expr with expr_desc = Expr_appl(id, args', reset)}, 
254
       locals', 
255
       eqs', 
256
       asserts',
257
       annots'
251 258

  
252 259
  (* For other cases, we just keep the structure, but convert sub-expressions *)
253 260
  | Expr_const _ 
254 261
  | Expr_ident _ -> expr, locals, [], [], []
255 262
  | Expr_tuple el -> 
256
    let el', l', eqs', asserts', annots' = inline_tuple el in
257
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
263
     let el', l', eqs', asserts', annots' = inline_tuple el in
264
     { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
258 265
  | Expr_ite (g, t, e) ->
259
    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'
266
     let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in
267
     { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'
261 268
  | Expr_arrow (e1, e2) ->
262
    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'
269
     let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
270
     { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots'
264 271
  | Expr_fby (e1, e2) ->
265
    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'
272
     let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
273
     { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'
267 274
  | Expr_array el ->
268
    let el', l', eqs', asserts', annots' = inline_tuple el in
269
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
275
     let el', l', eqs', asserts', annots' = inline_tuple el in
276
     { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
270 277
  | Expr_access (e, dim) ->
271
    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'
278
     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
279
     { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'
273 280
  | Expr_power (e, dim) ->
274
    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'
281
     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
282
     { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'
276 283
  | Expr_pre e ->
277
    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'
284
     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
285
     { expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'
279 286
  | Expr_when (e, id, label) ->
280
    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'
287
     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
288
     { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots'
282 289
  | Expr_merge (id, branches) ->
283
    let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in
284
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
285
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'
290
     let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in
291
     let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
292
     { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'
286 293

  
287 294
and inline_node ?(selection_on_annotation=false) node nodes =
288 295
  try copy_node (Hashtbl.find inline_table node.node_id)
289 296
  with Not_found ->
290
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
291
  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
	inline_expr eq.eq_rhs locals node nodes 
295
      in
296
      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
  in
299
  let inlined = 
300
  { node with
301
    node_locals = new_locals;
302
    node_stmts = List.map (fun eq -> Eq eq) eqs;
303
    node_asserts = asserts;
304
    node_annot = annots;
305
  }
306
  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
297
    let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
298
    let eqs, auts = get_node_eqs node in
299
    assert (auts = []); (* No inlining of automaton yet. One should visit each
300
			   handler eqs and perform similar computation *)
301
    let new_locals, stmts, asserts, annots = 
302
      List.fold_left (fun (locals, stmts, asserts, annots) eq ->
303
	let eq_rhs', locals', new_stmts', asserts', annots' = 
304
	  inline_expr eq.eq_rhs locals node nodes 
305
	in
306
	locals', Eq { eq with eq_rhs = eq_rhs' }::new_stmts'@stmts, asserts'@asserts, annots'@annots
307
      ) (node.node_locals, [], node.node_asserts, node.node_annot) eqs
308
    in
309
    let inlined = 
310
      { node with
311
	node_locals = new_locals;
312
	node_stmts = stmts;
313
	node_asserts = asserts;
314
	node_annot = annots;
315
      }
316
    in
317
    begin
318
      (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
319
      Hashtbl.add inline_table node.node_id inlined;
320
      inlined
321
    end
312 322

  
313 323
let inline_all_calls node nodes =
314 324
  let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
......
333 343
  let inlined_rename = rename_local_node inlined "inlined_" in
334 344
  let identity = (fun x -> x) in
335 345
  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
346
  let orig = rename_prog orig_rename (* f_node *) identity (* f_var *) identity (* f_const *) orig in
337 347
  let inlined = rename_prog inlined_rename identity identity inlined in
338 348
  let nodes_origs, others = List.partition is_node orig in
339 349
  let nodes_inlined, _ = List.partition is_node inlined in

Also available in: Unified diff