CristalCaveGem » LustreC

(********************************************************************)

(*                                                                  *)

(*  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

(* Associate to each annotation key the pair (node, expr tag) *)

let expr_annotations : (string list, ident * tag) Hashtbl.t=  Hashtbl.create 13

let node_annotations : (string list, ident) Hashtbl.t=  Hashtbl.create 13

let add_expr_ann node_id expr_tag key = Hashtbl.add expr_annotations key (node_id, expr_tag)

let add_node_ann node_id key = Hashtbl.add node_annotations key node_id

let get_expr_annotations key = Hashtbl.find_all expr_annotations key

let update_expr_annot node_id e annot =

  List.iter (fun (key, _) -> 

    Annotations.add_expr_ann node_id e.expr_tag key

  ) annot.annots;

val update_expr_annot: ident -> expr -> LustreSpec.expr_annot -> expr

open Utils

(* Local annotations are declared with the following key /inlining/: true *)

let keyword = ["inlining"]

let is_inline_expr expr = 

match expr.expr_annot with

| Some ann -> 

  List.exists (fun (key, value) -> key = keyword) ann.annots

| None -> false

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

  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in

  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in

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

						    as arguments nodes *)

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

							      it is explicitely inlined here *)

    then 

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

and inline_node ?(selection_on_annotation=false) nd nodes = 

  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in

let local_inline basename prog type_env clock_env =

  let local_anns = Annotations.get_expr_annotations keyword in

  if local_anns != [] then (

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

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

    List.fold_right (fun top accu -> 

      ( match top.top_decl_desc with

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

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

      | _ -> top

      )::accu) prog []

)

 else

  prog

    else (* if !Option.has_local_inline *)

      Inliner.local_inline basename prog type_env clock_env

  (* TO BE DONE LATER (Xavier)

%type <LustreSpec.ident -> LustreSpec.expr_annot> lustre_annot

lustre_annot_list EOF { fun node_id -> $1 }

let node_stack : ident list ref = ref []

let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack

let push_node nd =  node_stack:= nd :: !node_stack

let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false

let get_current_node () = try List.hd !node_stack with _ -> assert false

node_ident_decl:

 node_ident { push_node $1; $1 }

     pop_node ();

| nodespec_list state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL 

    {

      let stmts, asserts, annots = $16 in

      (* Declaring eqs annots *)

      List.iter (fun ann -> 

	List.iter (fun (key, _) -> 

	  Annotations.add_node_ann $3 key

	) ann.annots

      ) annots;

     (* Building the node *)

      let nd = mktop_decl false (Node

				   {node_id = $3;

				    node_type = Types.new_var ();

				    node_clock = Clocks.new_var true;

				    node_inputs = List.rev $5;

				    node_outputs = List.rev $10;

				    node_locals = List.rev $14;

				    node_gencalls = [];

				    node_checks = [];

				    node_asserts = asserts; 

				    node_stmts = stmts;

				    node_dec_stateless = $2;

				    node_stateless = None;

				    node_spec = $1;

				    node_annot = annots})

      in

 nodespec_list:

    {update_expr_annot (get_current_node ()) $3 $2}