Project

General

Profile

Revision 53206908 src/inliner.ml

View differences:

src/inliner.ml
64 64
the resulting expression is tuple_of_renamed_outputs
65 65
   
66 66
TODO: convert the specification/annotation/assert and inject them
67
DONE: annotations
67 68
TODO: deal with reset
68 69
*)
69 70
let inline_call node orig_expr args reset locals caller =
......
136 137
      })
137 138
      node.node_asserts 
138 139
  in
140
  let annots' =
141
    Plugins.inline_annots rename node.node_annot
142
  in
139 143
  expr, 
140 144
  inputs'@outputs'@locals'@locals, 
141 145
  assign_inputs::eqs',
142
  asserts'
146
  asserts',
147
  annots'
143 148

  
144 149

  
145 150

  
......
156 161
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
157 162
  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
158 163
  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, [], [])
164
    List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) -> 
165
      let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in
166
      e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots'
167
    ) el ([], locals, [], [], [])
163 168
  in
164 169
  let inline_pair e1 e2 = 
165
    let el', l', eqs', asserts' = inline_tuple [e1;e2] in
170
    let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in
166 171
    match el' with
167
    | [e1'; e2'] -> e1', e2', l', eqs', asserts'
172
    | [e1'; e2'] -> e1', e2', l', eqs', asserts', annots'
168 173
    | _ -> assert false
169 174
  in
170 175
  let inline_triple e1 e2 e3 = 
171
    let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
176
    let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in
172 177
    match el' with
173
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
178
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts', annots'
174 179
    | _ -> assert false
175 180
  in
176
  
181
    
177 182
  match expr.expr_desc with
178 183
  | Expr_appl (id, args, reset) ->
179
    let args', locals', eqs', asserts' = inline_expr args locals node nodes in 
184
    let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in 
180 185
    if List.exists (check_node_name id) nodes && (* the current node call is provided
181 186
						    as arguments nodes *)
182 187
      (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 
......
188 193
	with Not_found -> (assert false) in
189 194
      let called = node_of_top called in
190 195
      let called' = inline_node called nodes in
191
      let expr, locals', eqs'', asserts'' = 
196
      let expr, locals', eqs'', asserts'', annots'' = 
192 197
	inline_call called' expr args' reset locals' node in
193
      expr, locals', eqs'@eqs'', asserts'@asserts''
198
      expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
194 199
    else 
195 200
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
196 201
      { expr with expr_desc = Expr_appl(id, args', reset)}, 
197 202
      locals', 
198 203
      eqs', 
199
      asserts'
204
      asserts',
205
      annots'
200 206

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

  
236 242
and inline_node ?(selection_on_annotation=false) node nodes =
237 243
  try copy_node (Hashtbl.find inline_table node.node_id)
238 244
  with Not_found ->
239 245
  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' = 
246
  let new_locals, eqs, asserts, annots = 
247
    List.fold_left (fun (locals, eqs, asserts, annots) eq ->
248
      let eq_rhs', locals', new_eqs', asserts', annots' = 
243 249
	inline_expr eq.eq_rhs locals node nodes 
244 250
      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)
251
      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts, annots'@annots
252
    ) (node.node_locals, [], node.node_asserts, node.node_annot) (get_node_eqs node)
247 253
  in
248 254
  let inlined = 
249 255
  { node with
250 256
    node_locals = new_locals;
251 257
    node_stmts = List.map (fun eq -> Eq eq) eqs;
252 258
    node_asserts = asserts;
259
    node_annot = annots;
253 260
  }
254 261
  in
255 262
  begin
......
363 370
  in
364 371
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
365 372
  let new_prog = others@nodes_origs@nodes_inlined@main in
373
(*
374
  let _ = Typing.type_prog type_env new_prog in
375
  let _ = Clock_calculus.clock_prog clock_env new_prog in
376
*)
377
   
366 378
  let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
367 379
  let witness_out = open_out witness_file in
368 380
  let witness_fmt = Format.formatter_of_out_channel witness_out in
......
387 399
	| _ -> main_opt, nodes, top::others) 
388 400
      prog (None, [], []) 
389 401
  in
390

  
391 402
  (* Recursively each call of a node in the top node is replaced *)
392 403
  let main_node = Utils.desome main_node in
393 404
  let main_node' = inline_all_calls main_node other_nodes in
394
  let res = List.map (fun top -> if check_node_name !Options.main_node top then main_node' else top) prog in
405
  let res = main_node'::other_tops in
406
  if !Options.witnesses then (
407
    witness 
408
      basename
409
      (match main_node.top_decl_desc  with Node nd -> nd.node_id | _ -> assert false) 
410
      prog res type_env clock_env
411
  );
395 412
  res
396 413

  
397 414
let local_inline basename prog type_env clock_env =

Also available in: Unified diff