Project

General

Profile

Revision 3b2bd83d src/inliner.ml

View differences:

src/inliner.ml
39 39
    eq_lhs = List.map rename eq.eq_lhs; 
40 40
    eq_rhs = rename_expr rename eq.eq_rhs
41 41
  }
42

  
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 }
42 82
(*
43 83
let get_static_inputs input_arg_list =
44 84
 List.fold_right (fun (vdecl, arg) res ->
......
54 94
   else res)
55 95
   input_arg_list []
56 96
*)
97

  
98

  
57 99
(* 
58 100
    expr, locals', eqs = inline_call id args' reset locals node nodes
59 101

  
......
64 106
the resulting expression is tuple_of_renamed_outputs
65 107
   
66 108
TODO: convert the specification/annotation/assert and inject them
67
TODO: deal with reset
68 109
*)
69
let inline_call node orig_expr args reset locals caller =
70
  let loc = orig_expr.expr_loc in
71
  let uid = orig_expr.expr_tag in
110
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr,
111
    locals, eqs, asserts)    
112
*)
113
let inline_call node loc uid args reset locals caller =
72 114
  let rename v =
73 115
    if v = tag_true || v = tag_false || not (is_node_var node v) then v else
74 116
      Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
......
96 138
	 v.var_dec_const,
97 139
	 Utils.option_map (rename_expr rename) v.var_dec_value) in
98 140
    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
*)
141
      (*
142
	(try
143
	Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
144
	Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
145
	with Not_found -> ());
146
	(try
147
	Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
148
	with Not_found -> ());
149
      (*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
150
      *)
109 151
      vdecl
110 152
    end
111
    (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
153
  (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
112 154
  in
113 155
  let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
114 156
  let outputs' = List.map rename_var node.node_outputs in
115 157
  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)
158
    (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 159
    @ (List.map rename_var node.node_locals) 
118
in
160
  in
119 161
  (* checking we are at the appropriate (early) step: node_checks and
120 162
     node_gencalls should be empty (not yet assigned) *)
121 163
  assert (node.node_checks = []);
122 164
  assert (node.node_gencalls = []);
123 165

  
124
  (* Bug included: todo deal with reset *)
125
  assert (reset = None);
126

  
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
166
  (* Expressing reset locally in equations *)
167
  let eqs_r' =
168
    match reset with
169
      None -> eqs'
170
    | Some cond -> List.map (add_eq_reset_cond cond) eqs'
171
  in
172
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs',
173
                                expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
128 174
  let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
129 175
  in
130 176
  let asserts' = (* We rename variables in assert expressions *)
......
133 179
	{a with assert_expr = 
134 180
	    let expr = a.assert_expr in
135 181
	    rename_expr rename expr
136
      })
182
	})
137 183
      node.node_asserts 
138 184
  in
185
  let annots' =
186
    Plugins.inline_annots rename node.node_annot
187
  in
139 188
  expr, 
140 189
  inputs'@outputs'@locals'@locals, 
141
  assign_inputs::eqs',
142
  asserts'
190
  assign_inputs::eqs_r',
191
  asserts',
192
  annots'
143 193

  
144 194

  
145 195

  
......
156 206
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
157 207
  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
158 208
  let inline_tuple el = 
159
    List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 
160
      let e', locals', eqs', asserts' = inline_expr e locals node nodes in
161
      e'::el_tail, locals', eqs'@eqs, asserts@asserts'
162
    ) el ([], locals, [], [])
209
    List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) -> 
210
      let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in
211
      e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots'
212
    ) el ([], locals, [], [], [])
163 213
  in
164 214
  let inline_pair e1 e2 = 
165
    let el', l', eqs', asserts' = inline_tuple [e1;e2] in
215
    let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in
166 216
    match el' with
167
    | [e1'; e2'] -> e1', e2', l', eqs', asserts'
217
    | [e1'; e2'] -> e1', e2', l', eqs', asserts', annots'
168 218
    | _ -> assert false
169 219
  in
170 220
  let inline_triple e1 e2 e3 = 
171
    let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
221
    let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in
172 222
    match el' with
173
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
223
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts', annots'
174 224
    | _ -> assert false
175 225
  in
176 226
  
177 227
  match expr.expr_desc with
178 228
  | Expr_appl (id, args, reset) ->
179
    let args', locals', eqs', asserts' = inline_expr args locals node nodes in 
229
    let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in 
180 230
    if List.exists (check_node_name id) nodes && (* the current node call is provided
181 231
						    as arguments nodes *)
182 232
      (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 
......
188 238
	with Not_found -> (assert false) in
189 239
      let called = node_of_top called in
190 240
      let called' = inline_node called nodes in
191
      let expr, locals', eqs'', asserts'' = 
192
	inline_call called' expr args' reset locals' node in
193
      expr, locals', eqs'@eqs'', asserts'@asserts''
241
      let expr, locals', eqs'', asserts'', annots'' = 
242
	inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
243
      expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
194 244
    else 
195 245
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
196 246
      { expr with expr_desc = Expr_appl(id, args', reset)}, 
197 247
      locals', 
198 248
      eqs', 
199
      asserts'
249
      asserts',
250
      annots'
200 251

  
201 252
  (* For other cases, we just keep the structure, but convert sub-expressions *)
202 253
  | Expr_const _ 
203
  | Expr_ident _ -> expr, locals, [], []
254
  | Expr_ident _ -> expr, locals, [], [], []
204 255
  | Expr_tuple el -> 
205
    let el', l', eqs', asserts' = inline_tuple el in
206
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
256
    let el', l', eqs', asserts', annots' = inline_tuple el in
257
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
207 258
  | Expr_ite (g, t, e) ->
208
    let g', t', e', l', eqs', asserts' = inline_triple g t e in
209
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts'
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'
210 261
  | Expr_arrow (e1, e2) ->
211
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
212
    { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
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'
213 264
  | Expr_fby (e1, e2) ->
214
    let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
215
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
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'
216 267
  | Expr_array el ->
217
    let el', l', eqs', asserts' = inline_tuple el in
218
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts'
268
    let el', l', eqs', asserts', annots' = inline_tuple el in
269
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
219 270
  | Expr_access (e, dim) ->
220
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
221
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
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'
222 273
  | Expr_power (e, dim) ->
223
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
224
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
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'
225 276
  | Expr_pre e ->
226
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
227
    { expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
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'
228 279
  | Expr_when (e, id, label) ->
229
    let e', l', eqs', asserts' = inline_expr e locals node nodes in 
230
    { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
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'
231 282
  | Expr_merge (id, branches) ->
232
    let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
283
    let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in
233 284
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
234
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
285
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'
235 286

  
236 287
and inline_node ?(selection_on_annotation=false) node nodes =
237 288
  try copy_node (Hashtbl.find inline_table node.node_id)
238 289
  with Not_found ->
239 290
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
240
  let new_locals, eqs, asserts = 
241
    List.fold_left (fun (locals, eqs, asserts) eq ->
242
      let eq_rhs', locals', new_eqs', asserts' = 
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' = 
243 294
	inline_expr eq.eq_rhs locals node nodes 
244 295
      in
245
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
246
    ) (node.node_locals, [], node.node_asserts) (get_node_eqs node)
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)
247 298
  in
248 299
  let inlined = 
249 300
  { node with
250 301
    node_locals = new_locals;
251 302
    node_stmts = List.map (fun eq -> Eq eq) eqs;
252 303
    node_asserts = asserts;
304
    node_annot = annots;
253 305
  }
254 306
  in
255 307
  begin
......
363 415
  in
364 416
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
365 417
  let new_prog = others@nodes_origs@nodes_inlined@main in
418
(*
419
  let _ = Typing.type_prog type_env new_prog in
420
  let _ = Clock_calculus.clock_prog clock_env new_prog in
421
*)
422
   
366 423
  let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
367 424
  let witness_out = open_out witness_file in
368 425
  let witness_fmt = Format.formatter_of_out_channel witness_out in
......
387 444
	| _ -> main_opt, nodes, top::others) 
388 445
      prog (None, [], []) 
389 446
  in
390

  
391 447
  (* Recursively each call of a node in the top node is replaced *)
392 448
  let main_node = Utils.desome main_node in
393 449
  let main_node' = inline_all_calls main_node other_nodes in

Also available in: Unified diff