Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/inliner.ml
14 14
open Utils
15 15

  
16 16
(* Local annotations are declared with the following key /inlining/: true *)
17
let keyword = ["inlining"]
17
let keyword = [ "inlining" ]
18 18

  
19
let is_inline_expr expr = 
20
match expr.expr_annot with
21
| Some ann -> 
22
  List.exists (fun (key, _) -> key = keyword) ann.annots
23
| None -> false
19
let is_inline_expr expr =
20
  match expr.expr_annot with
21
  | Some ann ->
22
    List.exists (fun (key, _) -> key = keyword) ann.annots
23
  | None ->
24
    false
24 25

  
25
let check_node_name id = (fun t -> 
26
  match t.top_decl_desc with 
27
  | Node nd -> nd.node_id = id 
28
  | _ -> false) 
26
let check_node_name id t =
27
  match t.top_decl_desc with Node nd -> nd.node_id = id | _ -> false
29 28

  
30 29
let is_node_var node v =
31
 try
32
   ignore (Corelang.get_node_var v node); true
33
 with Not_found -> false
30
  try
31
    ignore (Corelang.get_node_var v node);
32
    true
33
  with Not_found -> false
34 34

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

  
44 39
let rec add_expr_reset_cond cond expr =
45 40
  let aux = add_expr_reset_cond cond in
46
  let new_desc = 
41
  let new_desc =
47 42
    match expr.expr_desc with
48
    | Expr_const _
49
    | Expr_ident _ -> expr.expr_desc
50
    | Expr_tuple el -> Expr_tuple (List.map aux el)
51
    | Expr_ite (c, t, e) -> Expr_ite (aux c, aux t, aux e)
52
      
53
    | Expr_arrow (e1, e2) -> 
43
    | Expr_const _ | Expr_ident _ ->
44
      expr.expr_desc
45
    | Expr_tuple el ->
46
      Expr_tuple (List.map aux el)
47
    | Expr_ite (c, t, e) ->
48
      Expr_ite (aux c, aux t, aux e)
49
    | Expr_arrow (e1, e2) ->
54 50
      (* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *)
55 51
      let e1 = aux e1 and e2 = aux e2 in
56 52
      (* inlining is performed before typing. we can leave the fields free *)
57 53
      let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in
58
      Expr_arrow (e1, new_e2) 
59

  
60
    | Expr_fby _ -> assert false (* TODO: deal with fby. This hasn't been much handled yet *)
61

  
62
    | Expr_array el -> Expr_array (List.map aux el)
63
    | Expr_access (e, dim) -> Expr_access (aux e, dim)
64
    | Expr_power (e, dim) -> Expr_power (aux e, dim)
65
    | Expr_pre e -> Expr_pre (aux e)
66
    | Expr_when (e, id, l) -> Expr_when (aux e, id, l)
67
    | Expr_merge (id, cases) -> Expr_merge (id, List.map (fun (l,e) -> l, aux e) cases)
68

  
69
    | Expr_appl (id, args, reset_opt) -> 
54
      Expr_arrow (e1, new_e2)
55
    | Expr_fby _ ->
56
      assert false (* TODO: deal with fby. This hasn't been much handled yet *)
57
    | Expr_array el ->
58
      Expr_array (List.map aux el)
59
    | Expr_access (e, dim) ->
60
      Expr_access (aux e, dim)
61
    | Expr_power (e, dim) ->
62
      Expr_power (aux e, dim)
63
    | Expr_pre e ->
64
      Expr_pre (aux e)
65
    | Expr_when (e, id, l) ->
66
      Expr_when (aux e, id, l)
67
    | Expr_merge (id, cases) ->
68
      Expr_merge (id, List.map (fun (l, e) -> l, aux e) cases)
69
    | Expr_appl (id, args, reset_opt) ->
70 70
      (* we "add" cond to the reset field. *)
71
      let new_reset = match reset_opt with
72
	  None -> cond
73
	| Some cond' -> mkpredef_call cond'.expr_loc "||" [cond; cond']
71
      let new_reset =
72
        match reset_opt with
73
        | None ->
74
          cond
75
        | Some cond' ->
76
          mkpredef_call cond'.expr_loc "||" [ cond; cond' ]
74 77
      in
75 78
      Expr_appl (id, args, Some new_reset)
76
      
77

  
78 79
  in
80

  
79 81
  { expr with expr_desc = new_desc }
80 82

  
81 83
let add_eq_reset_cond cond eq =
82 84
  { eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs }
83
(*
84
let get_static_inputs input_arg_list =
85
 List.fold_right (fun (vdecl, arg) res ->
86
   if vdecl.var_dec_const
87
   then (vdecl.var_id, Corelang.dimension_of_expr arg) :: res
88
   else res)
89
   input_arg_list []
90

  
91
let get_carrier_inputs input_arg_list =
92
 List.fold_right (fun (vdecl, arg) res ->
93
   if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc
94
   then (vdecl.var_id, ident_of_expr arg) :: res
95
   else res)
96
   input_arg_list []
97
*)
98
(* 
99
    expr, locals', eqs = inline_call id args' reset locals node nodes
100

  
101
We select the called node equations and variables.
102
   renamed_inputs = args
85
(* let get_static_inputs input_arg_list = List.fold_right (fun (vdecl, arg) res
86
   -> if vdecl.var_dec_const then (vdecl.var_id, Corelang.dimension_of_expr arg)
87
   :: res else res) input_arg_list []
88

  
89
   let get_carrier_inputs input_arg_list = List.fold_right (fun (vdecl, arg) res
90
   -> if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc then
91
   (vdecl.var_id, ident_of_expr arg) :: res else res) input_arg_list [] *)
92
(* expr, locals', eqs = inline_call id args' reset locals node nodes
93

  
94
   We select the called node equations and variables. renamed_inputs = args
103 95
   renamed_eqs
104 96

  
105
the resulting expression is tuple_of_renamed_outputs
106
   
107
TODO: convert the specification/annotation/assert and inject them
108
*)
97
   the resulting expression is tuple_of_renamed_outputs
98

  
99
   TODO: convert the specification/annotation/assert and inject them *)
109 100

  
110 101
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr,
111
    locals, eqs, asserts)    
112
*)
102
    locals, eqs, asserts) *)
113 103
let inline_call node loc uid args reset locals caller =
114 104
  let rename v =
115
    if v = tag_true || v = tag_false || not (is_node_var node v) then v else
116
      Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
105
    if v = tag_true || v = tag_false || not (is_node_var node v) then v
106
    else
107
      Corelang.mk_new_node_name caller
108
        (Format.sprintf "%s_%i_%s" node.node_id uid v)
117 109
  in
118 110
  let eqs, auts = get_node_eqs node in
119 111
  let eqs' = List.map (rename_eq (fun x -> x) rename) eqs in
120 112
  let auts' = List.map (rename_aut (fun x -> x) rename) auts in
121
  let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in
122
  let static_inputs, dynamic_inputs = List.partition (fun (vdecl, _) -> vdecl.var_dec_const) input_arg_list in
123
  let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in
124
  let carrier_inputs, _ = List.partition (fun (vdecl, _) -> Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc) dynamic_inputs in
125
  let carrier_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) carrier_inputs in
113
  let input_arg_list =
114
    List.combine node.node_inputs (Corelang.expr_list_of_expr args)
115
  in
116
  let static_inputs, dynamic_inputs =
117
    List.partition (fun (vdecl, _) -> vdecl.var_dec_const) input_arg_list
118
  in
119
  let static_inputs =
120
    List.map
121
      (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg)
122
      static_inputs
123
  in
124
  let carrier_inputs, _ =
125
    List.partition
126
      (fun (vdecl, _) ->
127
        Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc)
128
      dynamic_inputs
129
  in
130
  let carrier_inputs =
131
    List.map
132
      (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg)
133
      carrier_inputs
134
  in
126 135
  let rename_static v =
127
    try
128
      snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs)
129
    with Not_found -> Dimension.mkdim_ident loc v in
136
    try snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs)
137
    with Not_found -> Dimension.mkdim_ident loc v
138
  in
130 139
  let rename_carrier v =
131
    try
132
      snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs)
133
    with Not_found -> v in
140
    try snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs)
141
    with Not_found -> v
142
  in
134 143
  let rename_var v =
135 144
    let vdecl =
136 145
      Corelang.mkvar_decl v.var_loc
137
	(rename v.var_id,
138
	 { v.var_dec_type  with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc },
139
	 { v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc },
140
	 v.var_dec_const,
141
	 Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value,
142
	 v.var_parent_nodeid (* we keep the original parent name *)
143
	) in
144
    begin
145
      (*
146
	(try
147
	Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
148
	Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
149
	with Not_found -> ());
150
	(try
151
	Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
152
	with Not_found -> ());
153
      (*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
154
      *)
155
      vdecl
156
    end
146
        ( rename v.var_id,
147
          {
148
            v.var_dec_type with
149
            ty_dec_desc =
150
              Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc;
151
          },
152
          {
153
            v.var_dec_clock with
154
            ck_dec_desc =
155
              Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc;
156
          },
157
          v.var_dec_const,
158
          Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value,
159
          v.var_parent_nodeid (* we keep the original parent name *) )
160
    in
161
    (* (try Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty
162
       vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id
163
       static_inputs); Typing.unify vdecl.var_type (Type_predef.type_static
164
       (List.assoc v.var_id static_inputs) (Types.new_var ())) with Not_found ->
165
       ()); (try Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier
166
       (List.assoc v.var_id carrier_inputs) (Clocks.new_var true)) with
167
       Not_found -> ()); (*Format.eprintf "Inliner.inline_call res=%a@."
168
       Printers.pp_var vdecl;*) *)
169
    vdecl
157 170
    (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
158 171
  in
159 172
  let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
160 173
  let outputs' = List.map rename_var node.node_outputs in
161 174
  let locals' =
162
      (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
163
    @ (List.map rename_var node.node_locals) 
164
in
175
    List.map
176
      (fun (vdecl, arg) ->
177
        let vdecl' = rename_var vdecl in
178
        { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) })
179
      static_inputs
180
    @ List.map rename_var node.node_locals
181
  in
165 182
  (* checking we are at the appropriate (early) step: node_checks and
166 183
     node_gencalls should be empty (not yet assigned) *)
167 184
  assert (node.node_checks = []);
168 185
  assert (node.node_gencalls = []);
169 186

  
170 187
  (* Expressing reset locally in equations *)
171
  let eqs_r' = 
172
    let all_eqs = (List.map (fun eq -> Eq eq) eqs') @ (List.map (fun aut -> Aut aut) auts') in
188
  let eqs_r' =
189
    let all_eqs =
190
      List.map (fun eq -> Eq eq) eqs' @ List.map (fun aut -> Aut aut) auts'
191
    in
173 192
    match reset with
174
      None -> all_eqs
175
    | Some cond -> (
176
      assert (auts' = []); (* TODO: we do not handle properly automaton in case of reset call *)
193
    | None ->
194
      all_eqs
195
    | Some cond ->
196
      assert (auts' = []);
197
      (* TODO: we do not handle properly automaton in case of reset call *)
177 198
      List.map (fun eq -> Eq (add_eq_reset_cond cond eq)) eqs'
178
    )
179
  in
180
  let assign_inputs = Eq (mkeq loc (List.map (fun v -> v.var_id) inputs',
181
                                expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs))) in
182
  let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
183 199
  in
184
  let asserts' = (* We rename variables in assert expressions *)
185
    List.map 
186
      (fun a -> 
187
	{a with assert_expr = 
188
	    let expr = a.assert_expr in
189
	    rename_expr (fun x -> x) rename expr
190
	})
191
      node.node_asserts 
200
  let assign_inputs =
201
    Eq
202
      (mkeq loc
203
         ( List.map (fun v -> v.var_id) inputs',
204
           expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs) ))
192 205
  in
193
  let annots' =
194
    Plugins.inline_annots rename node.node_annot
206
  let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') in
207
  let asserts' =
208
    (* We rename variables in assert expressions *)
209
    List.map
210
      (fun a ->
211
        {
212
          a with
213
          assert_expr =
214
            (let expr = a.assert_expr in
215
             rename_expr (fun x -> x) rename expr);
216
        })
217
      node.node_asserts
195 218
  in
196
  expr, 
197
  inputs'@outputs'@locals'@locals, 
198
  assign_inputs::eqs_r',
199
  asserts',
200
  annots'
201

  
202

  
219
  let annots' = Plugins.inline_annots rename node.node_annot in
220
  ( expr,
221
    inputs' @ outputs' @ locals' @ locals,
222
    assign_inputs :: eqs_r',
223
    asserts',
224
    annots' )
203 225

  
204 226
let inline_table = Hashtbl.create 23
205 227

  
206
(* 
207
   new_expr, new_locals, new_eqs = inline_expr expr locals node nodes
208
   
228
(* new_expr, new_locals, new_eqs = inline_expr expr locals node nodes
229

  
209 230
   Each occurence of a node in nodes in the expr should be replaced by fresh
210
   variables and the code of called node instance added to new_eqs
211

  
212
*)
213
let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
214
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
215
  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
216
  let inline_tuple el = 
217
    List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) -> 
218
      let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in
219
      e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots'
220
    ) el ([], locals, [], [], [])
221
  in
222
  let inline_pair e1 e2 = 
223
    let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in
231
   variables and the code of called node instance added to new_eqs *)
232
let rec inline_expr ?(selection_on_annotation = false) expr locals node nodes =
233
  let inline_expr = inline_expr ~selection_on_annotation in
234
  let inline_node = inline_node ~selection_on_annotation in
235
  let inline_tuple el =
236
    List.fold_right
237
      (fun e (el_tail, locals, eqs, asserts, annots) ->
238
        let e', locals', eqs', asserts', annots' =
239
          inline_expr e locals node nodes
240
        in
241
        e' :: el_tail, locals', eqs' @ eqs, asserts @ asserts', annots @ annots')
242
      el ([], locals, [], [], [])
243
  in
244
  let inline_pair e1 e2 =
245
    let el', l', eqs', asserts', annots' = inline_tuple [ e1; e2 ] in
224 246
    match el' with
225
    | [e1'; e2'] -> e1', e2', l', eqs', asserts', annots'
226
    | _ -> assert false
247
    | [ e1'; e2' ] ->
248
      e1', e2', l', eqs', asserts', annots'
249
    | _ ->
250
      assert false
227 251
  in
228
  let inline_triple e1 e2 e3 = 
229
    let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in
252
  let inline_triple e1 e2 e3 =
253
    let el', l', eqs', asserts', annots' = inline_tuple [ e1; e2; e3 ] in
230 254
    match el' with
231
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts', annots'
232
    | _ -> assert false
255
    | [ e1'; e2'; e3' ] ->
256
      e1', e2', e3', l', eqs', asserts', annots'
257
    | _ ->
258
      assert false
233 259
  in
234
  
260

  
235 261
  match expr.expr_desc with
236 262
  | Expr_appl (id, args, reset) ->
237
     let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in 
238
     if List.exists (check_node_name id) nodes && (* the current node call is provided
239
						     as arguments nodes *)
240
       (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 
241
							       it is explicitely inlined here *)
242
     then (
243
       (* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *)
244
       (* The node should be inlined *)
245
       (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
246
       let called = try List.find (check_node_name id) nodes 
247
	 with Not_found -> (assert false) in
248
       let called = node_of_top called in
249
       let called' = inline_node called nodes in
250
       let expr, locals', eqs'', asserts'', annots'' = 
251
	 inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
252
       expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
253
     )
254
     else 
255
       (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
256
       { expr with expr_desc = Expr_appl(id, args', reset)}, 
257
       locals', 
258
       eqs', 
259
       asserts',
260
       annots'
261

  
263
    let args', locals', eqs', asserts', annots' =
264
      inline_expr args locals node nodes
265
    in
266
    if
267
      List.exists (check_node_name id) nodes
268
      && (* the current node call is provided as arguments nodes *)
269
      ((not selection_on_annotation) || is_inline_expr expr)
270
      (* and if selection on annotation is activated, it is explicitely inlined
271
         here *)
272
    then
273
      (* Format.eprintf "Inlining call to %s in expression %a@." id
274
         Printers.pp_expr expr; *)
275
      (* The node should be inlined *)
276
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
277
      let called =
278
        try List.find (check_node_name id) nodes
279
        with Not_found -> assert false
280
      in
281
      let called = node_of_top called in
282
      let called' = inline_node called nodes in
283
      let expr, locals', eqs'', asserts'', annots'' =
284
        inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node
285
      in
286
      expr, locals', eqs' @ eqs'', asserts' @ asserts'', annots' @ annots''
287
    else
288
      (* let _ = Format.eprintf "Not inlining call to %s@." id in *)
289
      ( { expr with expr_desc = Expr_appl (id, args', reset) },
290
        locals',
291
        eqs',
292
        asserts',
293
        annots' )
262 294
  (* For other cases, we just keep the structure, but convert sub-expressions *)
263
  | Expr_const _ 
264
  | Expr_ident _ -> expr, locals, [], [], []
265
  | Expr_tuple el -> 
266
     let el', l', eqs', asserts', annots' = inline_tuple el in
267
     { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
295
  | Expr_const _ | Expr_ident _ ->
296
    expr, locals, [], [], []
297
  | Expr_tuple el ->
298
    let el', l', eqs', asserts', annots' = inline_tuple el in
299
    { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
268 300
  | Expr_ite (g, t, e) ->
269
     let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in
270
     { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'
301
    let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in
302
    { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'
271 303
  | Expr_arrow (e1, e2) ->
272
     let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
273
     { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots'
304
    let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
305
    { expr with expr_desc = Expr_arrow (e1', e2') }, l', eqs', asserts', annots'
274 306
  | Expr_fby (e1, e2) ->
275
     let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
276
     { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'
307
    let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
308
    { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'
277 309
  | Expr_array el ->
278
     let el', l', eqs', asserts', annots' = inline_tuple el in
279
     { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
310
    let el', l', eqs', asserts', annots' = inline_tuple el in
311
    { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
280 312
  | Expr_access (e, dim) ->
281
     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
282
     { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'
313
    let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
314
    { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'
283 315
  | Expr_power (e, dim) ->
284
     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
285
     { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'
316
    let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
317
    { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'
286 318
  | Expr_pre e ->
287
     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
288
     { expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'
319
    let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
320
    { expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'
289 321
  | Expr_when (e, id, label) ->
290
     let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in 
291
     { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots'
322
    let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
323
    ( { expr with expr_desc = Expr_when (e', id, label) },
324
      l',
325
      eqs',
326
      asserts',
327
      annots' )
292 328
  | Expr_merge (id, branches) ->
293
     let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in
294
     let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
295
     { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'
296

  
297
and inline_node ?(selection_on_annotation=false) node nodes =
329
    let el, l', eqs', asserts', annots' =
330
      inline_tuple (List.map snd branches)
331
    in
332
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
333
    ( { expr with expr_desc = Expr_merge (id, branches') },
334
      l',
335
      eqs',
336
      asserts',
337
      annots' )
338

  
339
and inline_node ?(selection_on_annotation = false) node nodes =
298 340
  try copy_node (Hashtbl.find inline_table node.node_id)
299 341
  with Not_found ->
300
    let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
342
    let inline_expr = inline_expr ~selection_on_annotation in
301 343
    let eqs, auts = get_node_eqs node in
302
    assert (auts = []); (* No inlining of automaton yet. One should visit each
303
			   handler eqs and perform similar computation *)
304
    let new_locals, stmts, asserts, annots = 
305
      List.fold_left (fun (locals, stmts, asserts, annots) eq ->
306
	let eq_rhs', locals', new_stmts', asserts', annots' = 
307
	  inline_expr eq.eq_rhs locals node nodes 
308
	in
309
	locals', Eq { eq with eq_rhs = eq_rhs' }::new_stmts'@stmts, asserts'@asserts, annots'@annots
310
      ) (node.node_locals, [], node.node_asserts, node.node_annot) eqs
344
    assert (auts = []);
345
    (* No inlining of automaton yet. One should visit each handler eqs and
346
       perform similar computation *)
347
    let new_locals, stmts, asserts, annots =
348
      List.fold_left
349
        (fun (locals, stmts, asserts, annots) eq ->
350
          let eq_rhs', locals', new_stmts', asserts', annots' =
351
            inline_expr eq.eq_rhs locals node nodes
352
          in
353
          ( locals',
354
            Eq { eq with eq_rhs = eq_rhs' } :: new_stmts' @ stmts,
355
            asserts' @ asserts,
356
            annots' @ annots ))
357
        (node.node_locals, [], node.node_asserts, node.node_annot)
358
        eqs
311 359
    in
312
    let inlined = 
313
      { node with
314
	node_locals = new_locals;
315
	node_stmts = stmts;
316
	node_asserts = asserts;
317
	node_annot = annots;
360
    let inlined =
361
      {
362
        node with
363
        node_locals = new_locals;
364
        node_stmts = stmts;
365
        node_asserts = asserts;
366
        node_annot = annots;
318 367
      }
319 368
    in
320
    begin
321
      (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
322
      Hashtbl.add inline_table node.node_id inlined;
323
      inlined
324
    end
369
    (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
370
    Hashtbl.add inline_table node.node_id inlined;
371
    inlined
325 372

  
326 373
let inline_all_calls node nodes =
327 374
  let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
328 375
  { node with top_decl_desc = Node (inline_node nd nodes) }
329
    
330

  
331

  
332

  
333 376

  
334 377
let witness filename main_name orig inlined (* type_env clock_env *) =
335 378
  let loc = Location.dummy_loc in
336 379
  let rename_local_node nodes prefix id =
337
    if List.exists (check_node_name id) nodes then
338
      prefix ^ id 
339
    else
340
      id
380
    if List.exists (check_node_name id) nodes then prefix ^ id else id
341 381
  in
342
  let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with
343
  Node nd -> nd | _ -> assert false in
344
  
382
  let main_orig_node =
383
    match (List.find (check_node_name main_name) orig).top_decl_desc with
384
    | Node nd ->
385
      nd
386
    | _ ->
387
      assert false
388
  in
389

  
345 390
  let orig_rename = rename_local_node orig "orig_" in
346 391
  let inlined_rename = rename_local_node inlined "inlined_" in
347
  let identity = (fun x -> x) in
348
  let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in
349
  let orig = rename_prog orig_rename (* f_node *) identity (* f_var *) identity (* f_const *) orig in
392
  let identity x = x in
393
  let is_node top =
394
    match top.top_decl_desc with Node _ -> true | _ -> false
395
  in
396
  let orig =
397
    rename_prog orig_rename (* f_node *) identity (* f_var *) identity
398
      (* f_const *) orig
399
  in
350 400
  let inlined = rename_prog inlined_rename identity identity inlined in
351 401
  let nodes_origs, others = List.partition is_node orig in
352 402
  let nodes_inlined, _ = List.partition is_node inlined in
353 403

  
354
  (* One ok_i boolean variable  per output var *)
404
  (* One ok_i boolean variable per output var *)
355 405
  let nb_outputs = List.length main_orig_node.node_outputs in
356 406
  let ok_ident = "OK" in
357
  let ok_i = List.map (fun id ->
358
    mkvar_decl 
359
      loc 
360
      (Format.sprintf "%s_%i" ok_ident id,
361
       {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
362
       {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
363
       false,
364
       None,
365
       None
366
      )
367
  ) (Utils.enumerate nb_outputs) 
407
  let ok_i =
408
    List.map
409
      (fun id ->
410
        mkvar_decl loc
411
          ( Format.sprintf "%s_%i" ok_ident id,
412
            { ty_dec_desc = Tydec_bool; ty_dec_loc = loc },
413
            { ck_dec_desc = Ckdec_any; ck_dec_loc = loc },
414
            false,
415
            None,
416
            None ))
417
      (Utils.enumerate nb_outputs)
368 418
  in
369 419

  
370 420
  (* OK = ok_1 and ok_2 and ... ok_n-1 *)
371
  let ok_output = mkvar_decl 
372
    loc 
373
    (ok_ident,
374
     {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
375
     {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
376
     false,
377
     None,
378
     None
379
    )
421
  let ok_output =
422
    mkvar_decl loc
423
      ( ok_ident,
424
        { ty_dec_desc = Tydec_bool; ty_dec_loc = loc },
425
        { ck_dec_desc = Ckdec_any; ck_dec_loc = loc },
426
        false,
427
        None,
428
        None )
380 429
  in
381 430
  let main_ok_expr =
382 431
    let mkv x = mkexpr loc (Expr_ident x) in
383 432
    match ok_i with
384
    | [] -> assert false
385
    | [x] -> mkv x.var_id 
386
    | hd::tl -> 
387
      List.fold_left (fun accu elem -> 
388
	mkpredef_call loc "&&" [mkv elem.var_id; accu]
389
      ) (mkv hd.var_id) tl
433
    | [] ->
434
      assert false
435
    | [ x ] ->
436
      mkv x.var_id
437
    | hd :: tl ->
438
      List.fold_left
439
        (fun accu elem -> mkpredef_call loc "&&" [ mkv elem.var_id; accu ])
440
        (mkv hd.var_id) tl
390 441
  in
391 442

  
392 443
  (* Building main node *)
393

  
394 444
  let ok_i_eq =
395
    { eq_loc = loc;
445
    {
446
      eq_loc = loc;
396 447
      eq_lhs = List.map (fun v -> v.var_id) ok_i;
397
      eq_rhs = 
398
	let inputs = expr_of_expr_list  loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
399
	let call_orig = 
400
	  mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
401
	let call_inlined = 
402
	  mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
403
	let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
404
	mkexpr loc (Expr_appl ("=", args, None))
405
    } in
406
  let ok_eq =
407
    { eq_loc = loc;
408
      eq_lhs = [ok_ident];
409
      eq_rhs = main_ok_expr;
410
    } in
411
  let main_node = {
412
    node_id = "check";
413
    node_type = Types.new_var ();
414
    node_clock = Clocks.new_var true;
415
    node_inputs = main_orig_node.node_inputs;
416
    node_outputs = [ok_output];
417
    node_locals = ok_i;
418
    node_gencalls = [];
419
    node_checks = [];
420
    node_asserts = [];
421
    node_stmts = [Eq ok_i_eq; Eq ok_eq];
422
    node_dec_stateless = false;
423
    node_stateless = None;
424
    node_spec = Some 
425
                  (Contract
426
                     (mk_contract_guarantees None
427
                        (mkeexpr loc (mkexpr loc (Expr_ident ok_ident)))
428
                     )
429
                  );
430
    node_annot = [];
431
    node_iscontract = true;
448
      eq_rhs =
449
        (let inputs =
450
           expr_of_expr_list loc
451
             (List.map
452
                (fun v -> mkexpr loc (Expr_ident v.var_id))
453
                main_orig_node.node_inputs)
454
         in
455
         let call_orig =
456
           mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None))
457
         in
458
         let call_inlined =
459
           mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None))
460
         in
461
         let args = mkexpr loc (Expr_tuple [ call_orig; call_inlined ]) in
462
         mkexpr loc (Expr_appl ("=", args, None)));
463
    }
464
  in
465
  let ok_eq = { eq_loc = loc; eq_lhs = [ ok_ident ]; eq_rhs = main_ok_expr } in
466
  let main_node =
467
    {
468
      node_id = "check";
469
      node_type = Types.new_var ();
470
      node_clock = Clocks.new_var true;
471
      node_inputs = main_orig_node.node_inputs;
472
      node_outputs = [ ok_output ];
473
      node_locals = ok_i;
474
      node_gencalls = [];
475
      node_checks = [];
476
      node_asserts = [];
477
      node_stmts = [ Eq ok_i_eq; Eq ok_eq ];
478
      node_dec_stateless = false;
479
      node_stateless = None;
480
      node_spec =
481
        Some
482
          (Contract
483
             (mk_contract_guarantees None
484
                (mkeexpr loc (mkexpr loc (Expr_ident ok_ident)))));
485
      node_annot = [];
486
      node_iscontract = true;
432 487
    }
433 488
  in
434
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
435
  let new_prog = others@nodes_origs@nodes_inlined@main in
436
(*
437
  let _ = Typing.type_prog type_env new_prog in
438
  let _ = Clock_calculus.clock_prog clock_env new_prog in
439
*)
440
   
441
  let witness_file = (Options_management.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
489
  let main =
490
    [
491
      {
492
        top_decl_desc = Node main_node;
493
        top_decl_loc = loc;
494
        top_decl_owner = filename;
495
        top_decl_itf = false;
496
      };
497
    ]
498
  in
499
  let new_prog = others @ nodes_origs @ nodes_inlined @ main in
500

  
501
  (* let _ = Typing.type_prog type_env new_prog in let _ =
502
     Clock_calculus.clock_prog clock_env new_prog in *)
503
  let witness_file =
504
    Options_management.get_witness_dir filename ^ "/" ^ "inliner_witness.lus"
505
  in
442 506
  let witness_out = open_out witness_file in
443 507
  let witness_fmt = Format.formatter_of_out_channel witness_out in
444
  begin
445
    List.iter (fun vdecl -> Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) (ok_output::ok_i);
446
    Format.fprintf witness_fmt
447
      "(* Generated lustre file to check validity of inlining process *)@.";
448
    Printers.pp_prog witness_fmt new_prog;
449
    Format.fprintf witness_fmt "@.";
450
    ()
451
  end (* xx *)
508
  List.iter
509
    (fun vdecl ->
510
      Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc)
511
    (ok_output :: ok_i);
512
  Format.fprintf witness_fmt
513
    "(* Generated lustre file to check validity of inlining process *)@.";
514
  Printers.pp_prog witness_fmt new_prog;
515
  Format.fprintf witness_fmt "@.";
516
  ()
517
(* xx *)
452 518

  
453 519
let global_inline prog (*type_env clock_env*) =
454 520
  (* We select the main node desc *)
455 521
  let main_node, other_nodes, _ =
456 522
    List.fold_right
457
      (fun top (main_opt, nodes, others) -> 
458
	match top.top_decl_desc with 
459
	| Node nd when nd.node_id = !Options.main_node -> 
460
	  Some top, nodes, others
461
	| Node _ -> main_opt, top::nodes, others
462
	| _ -> main_opt, nodes, top::others) 
463
      prog (None, [], []) 
523
      (fun top (main_opt, nodes, others) ->
524
        match top.top_decl_desc with
525
        | Node nd when nd.node_id = !Options.main_node ->
526
          Some top, nodes, others
527
        | Node _ ->
528
          main_opt, top :: nodes, others
529
        | _ ->
530
          main_opt, nodes, top :: others)
531
      prog (None, [], [])
464 532
  in
465 533

  
466 534
  (* Recursively each call of a node in the top node is replaced *)
467 535
  let main_node = Utils.desome main_node in
468 536
  let main_node' = inline_all_calls main_node other_nodes in
469
  let res = List.map (fun top -> if check_node_name !Options.main_node top then main_node' else top) prog in
470
 (* Code snippet from unstable branch. May be used when reactivating witnesses. 
471
 let res = main_node'::other_tops in
472
  if !Options.witnesses then (
473
    witness 
474
      basename
475
      (match main_node.top_decl_desc  with Node nd -> nd.node_id | _ -> assert false) 
476
      prog res type_env clock_env
477
  );
478
*)
537
  let res =
538
    List.map
539
      (fun top ->
540
        if check_node_name !Options.main_node top then main_node' else top)
541
      prog
542
  in
543
  (* Code snippet from unstable branch. May be used when reactivating witnesses.
544
     let res = main_node'::other_tops in if !Options.witnesses then ( witness
545
     basename (match main_node.top_decl_desc with Node nd -> nd.node_id | _ ->
546
     assert false) prog res type_env clock_env ); *)
479 547
  res
480 548

  
481 549
let pp_inline_calls fmt prog =
482 550
  let local_anns = Annotations.get_expr_annotations keyword in
483
  let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
551
  let nodes_with_anns =
552
    List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns
553
  in
484 554
  Format.fprintf fmt "@[<v 0>Inlined expresssions in node (by tags):@ %a@]"
485
    (fprintf_list ~sep:""
486
       (fun fmt top ->
487
	 match top.top_decl_desc with
488
	 | Node nd when ISet.mem nd.node_id nodes_with_anns ->
489
	    Format.fprintf fmt "%s: {@[<v 0>%a}@]@ "
490
	      nd.node_id
491
	      (fprintf_list ~sep:"@ " (fun fmt tag -> Format.fprintf fmt "%i" tag))
492
	      (List.fold_left
493
		 (fun accu (id, tag) -> if id = nd.node_id then tag::accu else accu)
494
		 []
495
		 local_anns
496
	      )	      
497
	 (* | Node nd -> Format.fprintf fmt "%s: no inline annotations" nd.node_id *)
498
	 | _ -> ()
499
     ))
555
    (fprintf_list ~sep:"" (fun fmt top ->
556
         match top.top_decl_desc with
557
         | Node nd when ISet.mem nd.node_id nodes_with_anns ->
558
           Format.fprintf fmt "%s: {@[<v 0>%a}@]@ " nd.node_id
559
             (fprintf_list ~sep:"@ " (fun fmt tag ->
560
                  Format.fprintf fmt "%i" tag))
561
             (List.fold_left
562
                (fun accu (id, tag) ->
563
                  if id = nd.node_id then tag :: accu else accu)
564
                [] local_anns)
565
         (* | Node nd -> Format.fprintf fmt "%s: no inline annotations"
566
            nd.node_id *)
567
         | _ ->
568
           ()))
500 569
    prog
501
  
502
  
570

  
503 571
let local_inline prog (* type_env clock_env *) =
504 572
  Log.report ~level:2 (fun fmt -> Format.fprintf fmt ".. @[<v 2>Inlining@,");
505 573
  let local_anns = Annotations.get_expr_annotations keyword in
506
  let prog = 
574
  let prog =
507 575
    if local_anns != [] then (
508
      let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
509
      ISet.iter (fun node_id -> Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Node %s has local expression annotations@ " node_id))
510
	nodes_with_anns;
511
      List.fold_right (fun top accu -> 
512
	( match top.top_decl_desc with
513
	| Node nd when ISet.mem nd.node_id nodes_with_anns ->
514
	   Log.report ~level:2 (fun fmt -> Format.fprintf fmt "[local inline] Processing node %s@ " nd.node_id);
515
	  let inlined_node = inline_node ~selection_on_annotation:true nd prog in
516
	  (* Format.eprintf "Before inline@.%a@.After:@.%a@." *)
517
	  (*   Printers.pp_node nd *)
518
	  (*   Printers.pp_node inlined_node; *)
519
	  { top with top_decl_desc = Node inlined_node }
520
	    
521
	| _ -> top
522
	)::accu) prog []
523
	
524
    )
576
      let nodes_with_anns =
577
        List.fold_left
578
          (fun accu (k, _) -> ISet.add k accu)
579
          ISet.empty local_anns
580
      in
581
      ISet.iter
582
        (fun node_id ->
583
          Log.report ~level:2 (fun fmt ->
584
              Format.fprintf fmt "Node %s has local expression annotations@ "
585
                node_id))
586
        nodes_with_anns;
587
      List.fold_right
588
        (fun top accu ->
589
          (match top.top_decl_desc with
590
          | Node nd when ISet.mem nd.node_id nodes_with_anns ->
591
            Log.report ~level:2 (fun fmt ->
592
                Format.fprintf fmt "[local inline] Processing node %s@ "
593
                  nd.node_id);
594
            let inlined_node =
595
              inline_node ~selection_on_annotation:true nd prog
596
            in
597
            (* Format.eprintf "Before inline@.%a@.After:@.%a@." *)
598
            (*   Printers.pp_node nd *)
599
            (*   Printers.pp_node inlined_node; *)
600
            { top with top_decl_desc = Node inlined_node }
601
          | _ ->
602
            top)
603
          :: accu)
604
        prog [])
525 605
    else (
526
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "No local inline information!@ ");
527
      prog
528
    )
606
      Log.report ~level:2 (fun fmt ->
607
          Format.fprintf fmt "No local inline information!@ ");
608
      prog)
529 609
  in
530 610
  Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@]@,");
531 611
  prog

Also available in: Unified diff