Project

General

Profile

Revision 01d48bb0 src/inliner.ml

View differences:

src/inliner.ml
27 27
  | Node nd -> nd.node_id = id 
28 28
  | _ -> false) 
29 29

  
30
let get_static_inputs node args =
31
  List.fold_right2 (fun vdecl arg static ->
32
    if vdecl.var_dec_const then (vdecl.var_id, Corelang.dimension_of_expr arg) :: static else static)
33
    node.node_inputs
34
    (Corelang.expr_list_of_expr args)
35
    []
36

  
37
let get_carrier_inputs node args =
38
  List.fold_right2 (fun vdecl arg carrier ->
39
    if Types.get_clock_base_type vdecl.var_type <> None then (vdecl.var_id, ident_of_expr arg) :: carrier else carrier)
40
    node.node_inputs
41
    (Corelang.expr_list_of_expr args)
42
    []
43

  
44 30
let is_node_var node v =
45 31
 try
46 32
   ignore (Corelang.get_node_var v node); true
......
53 39
    eq_lhs = List.map rename eq.eq_lhs; 
54 40
    eq_rhs = rename_expr rename eq.eq_rhs
55 41
  }
56

  
42
(*
43
let get_static_inputs input_arg_list =
44
 List.fold_right (fun (vdecl, arg) res ->
45
   if vdecl.var_dec_const
46
   then (vdecl.var_id, Corelang.dimension_of_expr arg) :: res
47
   else res)
48
   input_arg_list []
49

  
50
let get_carrier_inputs input_arg_list =
51
 List.fold_right (fun (vdecl, arg) res ->
52
   if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc
53
   then (vdecl.var_id, ident_of_expr arg) :: res
54
   else res)
55
   input_arg_list []
56
*)
57 57
(* 
58 58
    expr, locals', eqs = inline_call id args' reset locals node nodes
59 59

  
......
73 73
    if v = tag_true || v = tag_false || not (is_node_var node v) then v else
74 74
      Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
75 75
  in
76
  let eqs' = List.map (rename_eq rename) (get_node_eqs node)
77
  in
78
  let static_inputs = get_static_inputs node args in
79
  let carrier_inputs = get_carrier_inputs node args in
76
  let eqs' = List.map (rename_eq rename) (get_node_eqs node) in
77
  let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in
78
  let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) -> vdecl.var_dec_const) input_arg_list in
79
  let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in
80
  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
81
  let carrier_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) carrier_inputs in
80 82
  let rename_static v =
81 83
    try
82
      List.assoc v static_inputs
83
    with Not_found -> Dimension.mkdim_ident loc v
84
    (*Format.eprintf "Inliner.rename_static %s = %a@." v Dimension.pp_dimension res; res*)
85
  in
84
      snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs)
85
    with Not_found -> Dimension.mkdim_ident loc v in
86 86
  let rename_carrier v =
87 87
    try
88
      List.assoc v carrier_inputs
88
      snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs)
89 89
    with Not_found -> v in
90 90
  let rename_var v =
91
  (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
92
    { v with
93
      var_id = rename v.var_id;
94
      var_type = Types.rename_static rename_static v.var_type;
95
      var_clock = Clocks.rename_static rename_carrier v.var_clock;
96
    } in
97
  let inputs' = List.map rename_var node.node_inputs in
91
    let vdecl =
92
      Corelang.mkvar_decl v.var_loc
93
	(rename v.var_id,
94
	 { v.var_dec_type  with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc },
95
	 { v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc },
96
	 v.var_dec_const,
97
	 Utils.option_map (rename_expr rename) v.var_dec_value) in
98
    begin
99
(*
100
      (try
101
	 Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
102
	 Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
103
       with Not_found -> ());
104
      (try
105
Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
106
       with Not_found -> ());
107
(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
108
*)
109
      vdecl
110
    end
111
    (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
112
  in
113
  let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
98 114
  let outputs' = List.map rename_var node.node_outputs in
99
  let locals' = List.map rename_var node.node_locals in
115
  let locals' =
116
      (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
117
    @ (List.map rename_var node.node_locals) 
118
in
100 119
  (* checking we are at the appropriate (early) step: node_checks and
101 120
     node_gencalls should be empty (not yet assigned) *)
102 121
  assert (node.node_checks = []);
......
105 124
  (* Bug included: todo deal with reset *)
106 125
  assert (reset = None);
107 126

  
108
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
127
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
109 128
  let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
110 129
  in
111 130
  let asserts' = (* We rename variables in assert expressions *)
......
215 234
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
216 235

  
217 236
and inline_node ?(selection_on_annotation=false) node nodes =
218
  try Hashtbl.find inline_table node.node_id
237
  try copy_node (Hashtbl.find inline_table node.node_id)
219 238
  with Not_found ->
220 239
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
221 240
  let new_locals, eqs, asserts = 
......
269 288

  
270 289
  (* One ok_i boolean variable  per output var *)
271 290
  let nb_outputs = List.length main_orig_node.node_outputs in
291
  let ok_ident = "OK" in
272 292
  let ok_i = List.map (fun id ->
273 293
    mkvar_decl 
274 294
      loc 
275
      ("OK" ^ string_of_int id,
295
      (Format.sprintf "%s_%i" ok_ident id,
276 296
       {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
277 297
       {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
278
       false)
298
       false,
299
       None)
279 300
  ) (Utils.enumerate nb_outputs) 
280 301
  in
281 302

  
282 303
  (* OK = ok_1 and ok_2 and ... ok_n-1 *)
283
  let ok_ident = "OK" in
284 304
  let ok_output = mkvar_decl 
285 305
    loc 
286 306
    (ok_ident,
287 307
     {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
288 308
     {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
289
     false)
309
     false,
310
     None)
290 311
  in
291 312
  let main_ok_expr =
292 313
    let mkv x = mkexpr loc (Expr_ident x) in
......
342 363
  in
343 364
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
344 365
  let new_prog = others@nodes_origs@nodes_inlined@main in
345

  
346
  let _ = Typing.type_prog type_env new_prog in
347
  let _ = Clock_calculus.clock_prog clock_env new_prog in
348

  
349
   
350 366
  let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
351 367
  let witness_out = open_out witness_file in
352 368
  let witness_fmt = Format.formatter_of_out_channel witness_out in
353
  Format.fprintf witness_fmt
354
    "(* Generated lustre file to check validity of inlining process *)@.";
355
  Printers.pp_prog witness_fmt new_prog;
356
  Format.fprintf witness_fmt "@.";
357
  () (* xx *)
369
  begin
370
    List.iter (fun vdecl -> Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) (ok_output::ok_i);
371
    Format.fprintf witness_fmt
372
      "(* Generated lustre file to check validity of inlining process *)@.";
373
    Printers.pp_prog witness_fmt new_prog;
374
    Format.fprintf witness_fmt "@.";
375
    ()
376
  end (* xx *)
358 377

  
359 378
let global_inline basename prog type_env clock_env =
360 379
  (* We select the main node desc *)
361 380
  let main_node, other_nodes, other_tops = 
362
    List.fold_left 
363
      (fun (main_opt, nodes, others) top -> 
381
    List.fold_right
382
      (fun top (main_opt, nodes, others) -> 
364 383
	match top.top_decl_desc with 
365 384
	| Node nd when nd.node_id = !Options.main_node -> 
366 385
	  Some top, nodes, others
367 386
	| Node _ -> main_opt, top::nodes, others
368 387
	| _ -> main_opt, nodes, top::others) 
369
      (None, [], []) prog 
388
      prog (None, [], []) 
370 389
  in
390

  
371 391
  (* Recursively each call of a node in the top node is replaced *)
372 392
  let main_node = Utils.desome main_node in
373 393
  let main_node' = inline_all_calls main_node other_nodes in
374
  let res = main_node'::other_tops in
375
  if !Options.witnesses then (
376
    witness 
377
      basename
378
      (match main_node.top_decl_desc  with Node nd -> nd.node_id | _ -> assert false) 
379
      prog res type_env clock_env
380
  );
394
  let res = List.map (fun top -> if check_node_name !Options.main_node top then main_node' else top) prog in
381 395
  res
382 396

  
383 397
let local_inline basename prog type_env clock_env =

Also available in: Unified diff