Project

General

Profile

Revision 45f0f48d 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
DONE: annotations
68
TODO: deal with reset
69 109
*)
70
let inline_call node orig_expr args reset locals caller =
71
  let loc = orig_expr.expr_loc in
72
  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 =
73 114
  let rename v =
74 115
    if v = tag_true || v = tag_false || not (is_node_var node v) then v else
75 116
      Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
......
97 138
	 v.var_dec_const,
98 139
	 Utils.option_map (rename_expr rename) v.var_dec_value) in
99 140
    begin
100
(*
101
      (try
102
	 Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
103
	 Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
104
       with Not_found -> ());
105
      (try
106
Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
107
       with Not_found -> ());
108
(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
109
*)
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
      *)
110 151
      vdecl
111 152
    end
112
    (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
153
  (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
113 154
  in
114 155
  let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
115 156
  let outputs' = List.map rename_var node.node_outputs in
116 157
  let locals' =
117
      (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)
118 159
    @ (List.map rename_var node.node_locals) 
119
in
160
  in
120 161
  (* checking we are at the appropriate (early) step: node_checks and
121 162
     node_gencalls should be empty (not yet assigned) *)
122 163
  assert (node.node_checks = []);
123 164
  assert (node.node_gencalls = []);
124 165

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

  
128
  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
129 174
  let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
130 175
  in
131 176
  let asserts' = (* We rename variables in assert expressions *)
......
134 179
	{a with assert_expr = 
135 180
	    let expr = a.assert_expr in
136 181
	    rename_expr rename expr
137
      })
182
	})
138 183
      node.node_asserts 
139 184
  in
140 185
  let annots' =
......
142 187
  in
143 188
  expr, 
144 189
  inputs'@outputs'@locals'@locals, 
145
  assign_inputs::eqs',
190
  assign_inputs::eqs_r',
146 191
  asserts',
147 192
  annots'
148 193

  
......
194 239
      let called = node_of_top called in
195 240
      let called' = inline_node called nodes in
196 241
      let expr, locals', eqs'', asserts'', annots'' = 
197
	inline_call called' expr args' reset locals' node in
242
	inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
198 243
      expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
199 244
    else 
200 245
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)

Also available in: Unified diff