Project

General

Profile

Revision b50c665d src/inliner.ml

View differences:

src/inliner.ml
179 179
  let nodes_origs, others = List.partition is_node orig in
180 180
  let nodes_inlined, _ = List.partition is_node inlined in
181 181

  
182
  (* One ok_i boolean variable  per output var *)
183
  let nb_outputs = List.length main_orig_node.node_outputs in
184
  let ok_i = List.map (fun id ->
185
    mkvar_decl 
186
      loc 
187
      ("OK" ^ string_of_int id,
188
       {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
189
       {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
190
       false)
191
  ) (Utils.enumerate nb_outputs) 
192
  in
193

  
194
  (* OK = ok_1 and ok_2 and ... ok_n-1 *)
182 195
  let ok_ident = "OK" in
183 196
  let ok_output = mkvar_decl 
184 197
    loc 
......
187 200
     {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
188 201
     false)
189 202
  in
203
  let main_ok_expr =
204
    let mkv x = mkexpr loc (Expr_ident x) in
205
    match ok_i with
206
    | [] -> assert false
207
    | [x] -> mkv x.var_id 
208
    | hd::tl -> 
209
      List.fold_left (fun accu elem -> 
210
	mkpredef_call loc "&&" [mkv elem.var_id; accu]
211
      ) (mkv hd.var_id) tl
212
  in
213

  
214
  (* Building main node *)
215

  
190 216
  let main_node = {
191 217
    node_id = "check";
192 218
    node_type = Types.new_var ();
......
199 225
    node_asserts = [];
200 226
    node_eqs = [
201 227
      { eq_loc = loc;
202
	eq_lhs = [ok_ident];
228
	eq_lhs = List.map (fun v -> v.var_id) ok_i;
203 229
	eq_rhs = 
204 230
	  let inputs = expr_of_expr_list  loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
205 231
	  let call_orig = 
......
208 234
	    mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
209 235
	  let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
210 236
	  mkexpr loc (Expr_appl ("=", args, None))
211
      }];
237
      };
238
      { eq_loc = loc;
239
	eq_lhs = [ok_ident];
240
	eq_rhs = main_ok_expr;
241
      }
242
    ];
212 243
    node_dec_stateless = false;
213 244
    node_stateless = None;
214 245
    node_spec = Some 
......
257 288
      prog res type_env clock_env
258 289
  );
259 290
  res
291

  
292
(* Local Variables: *)
293
(* compile-command:"make -C .." *)
294
(* End: *)

Also available in: Unified diff