inliner.ml

(********************************************************************)
(*                                                                  *)
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
(*                                                                  *)
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
(*  under the terms of the GNU Lesser General Public License        *)
(*  version 2.1.                                                    *)
(*                                                                  *)
(********************************************************************)

open LustreSpec
open Corelang

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


let rename_expr rename expr = expr_replace_var rename expr
let rename_eq rename eq = 
  { eq with
    eq_lhs = List.map rename eq.eq_lhs; 
    eq_rhs = rename_expr rename eq.eq_rhs
  }

(* 
    expr, locals', eqs = inline_call id args' reset locals nodes

We select the called node equations and variables.
   renamed_inputs = args
   renamed_eqs

the resulting expression is tuple_of_renamed_outputs
   
TODO: convert the specification/annotation/assert and inject them
TODO: deal with reset
*)
let inline_call orig_expr args reset locals node =
  let loc = orig_expr.expr_loc in
  let uid = orig_expr.expr_tag in
  let rename v =
    if v = tag_true || v = tag_false then v else
    (Format.fprintf Format.str_formatter "%s_%i_%s" 
      node.node_id uid v;
    Format.flush_str_formatter ())
  in
  let eqs' = List.map (rename_eq rename) node.node_eqs
  in
  let rename_var v = { v with var_id = rename v.var_id } in
  let inputs' = List.map rename_var node.node_inputs in
  let outputs' = List.map rename_var node.node_outputs in
  let locals' = List.map rename_var node.node_locals in

  (* checking we are at the appropriate (early) step: node_checks and
     node_gencalls should be empty (not yet assigned) *)
  assert (node.node_checks = []);
  assert (node.node_gencalls = []);

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

  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
  let expr = expr_of_expr_list 
    loc 
    (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
  in
  let asserts' = (* We rename variables in assert expressions *)
    List.map