Project

General

Profile

Revision 6394042a src/inliner.ml

View differences:

src/inliner.ml
11 11 

  		




  12
  12
  
    
open LustreSpec


  		




  13
  13
  
    
open Corelang


  		




  
  14
  
    
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


  		




  14
  24
  
    

  		




  15
  25
  
    
let check_node_name id = (fun t -> 


  		




  16
  26
  
    
  match t.top_decl_desc with 


  		




  ......




  90
  100
  
    
   variables and the code of called node instance added to new_eqs


  		




  91
  101
  
    

  		




  92
  102
  
    
*)


  		




  93
  
  
    
let rec inline_expr expr locals nodes =


  		




  
  103
  
    
let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =


  		




  
  104
  
    
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in


  		




  
  105
  
    
  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in


  		




  94
  106
  
    
  let inline_tuple el = 


  		




  95
  107
  
    
    List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 


  		




  96
  108
  
    
      let e', locals', eqs', asserts' = inline_expr e locals nodes in


  		




  ......




  109
  121
  
    
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'


  		




  110
  122
  
    
    | _ -> assert false


  		




  111
  123
  
    
  in


  		




  112
  
  
    
    


  		




  
  124
  
    
  


  		




  113
  125
  
    
  match expr.expr_desc with


  		




  114
  126
  
    
  | Expr_appl (id, args, reset) ->


  		




  115
  127
  
    
    let args', locals', eqs', asserts' = inline_expr args locals nodes in 


  		




  116
  
  
    
    if List.exists (check_node_name id) nodes then 


  		




  
  128
  
    
    if List.exists (check_node_name id) nodes && (* the current node call is provided


  		




  
  129
  
    
						    as arguments nodes *)


  		




  
  130
  
    
      (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 


  		




  
  131
  
    
							      it is explicitely inlined here *)


  		




  
  132
  
    
    then 


  		




  117
  133
  
    
      (* The node should be inlined *)


  		




  118
  
  
    
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)


  		




  
  134
  
    
       let _ =     Format.eprintf "Inlining call to %s@." id in 


  		




  119
  135
  
    
      let node = try List.find (check_node_name id) nodes 


  		




  120
  136
  
    
	with Not_found -> (assert false) in


  		




  121
  137
  
    
      let node = node_of_top node in


  		




  ......




  164
  180
  
    
    let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in


  		




  165
  181
  
    
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in


  		




  166
  182
  
    
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'


  		




  167
  
  
    
and inline_node nd nodes = 


  		




  
  183
  
    
and inline_node ?(selection_on_annotation=false) nd nodes = 


  		




  
  184
  
    
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in


  		




  168
  185
  
    
  let new_locals, eqs, asserts = 


  		




  169
  186
  
    
    List.fold_left (fun (locals, eqs, asserts) eq ->


  		




  170
  187
  
    
      let eq_rhs', locals', new_eqs', asserts' = 


  		




  ......




  319
  336
  
    
  );


  		




  320
  337
  
    
  res


  		




  321
  338
  
    

  		




  
  339
  
    
let local_inline basename prog type_env clock_env =


  		




  
  340
  
    
  let local_anns = Annotations.get_expr_annotations keyword in


  		




  
  341
  
    
  if local_anns != [] then (


  		




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


  		




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


  		




  
  344
  
    
    List.fold_right (fun top accu -> 


  		




  
  345
  
    
      ( match top.top_decl_desc with


  		




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


  		




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


  		




  
  348
  
    
      | _ -> top


  		




  
  349
  
    
      )::accu) prog []


  		




  
  350
  
    
    


  		




  
  351
  
    
)


  		




  
  352
  
    
 else


  		




  
  353
  
    
  prog


  		




  
  354
  
    

  		




  
  355
  
    

  		




  322
  356
  
    
(* Local Variables: *)


  		




  323
  357
  
    
(* compile-command:"make -C .." *)


  		




  324
  358
  
    
(* End: *)


  		












Also available in:  Unified diff