Project

General

Profile

Revision 566dbf49

View differences:

src/annotations.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open LustreSpec
13

  
14

  
15
(* Associate to each annotation key the pair (node, expr tag) *)
16
let expr_annotations : (string list, ident * tag) Hashtbl.t=  Hashtbl.create 13
17
let node_annotations : (string list, ident) Hashtbl.t=  Hashtbl.create 13
18

  
19
let add_expr_ann node_id expr_tag key = Hashtbl.add expr_annotations key (node_id, expr_tag)
20
let add_node_ann node_id key = Hashtbl.add node_annotations key node_id
21

  
22
let get_expr_annotations key = Hashtbl.find_all expr_annotations key
src/corelang.ml
167 167
      annot_loc = ann1.annot_loc
168 168
    }
169 169

  
170
let update_expr_annot e annot =
170
let update_expr_annot node_id e annot =
171
  List.iter (fun (key, _) -> 
172
    Annotations.add_expr_ann node_id e.expr_tag key
173
  ) annot.annots;
171 174
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
172 175

  
173 176

  
src/corelang.mli
116 116
(** rename_prog f_node f_var f_const prog *)
117 117
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program
118 118

  
119
val update_expr_annot: expr -> LustreSpec.expr_annot -> expr
120 119

  
121 120
val substitute_expr: var_decl list -> eq list -> expr -> expr
122 121

  
......
124 123
val mkeexpr: Location.t ->  expr -> eexpr
125 124
val merge_node_annot: node_annot -> node_annot -> node_annot 
126 125
val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
127
val update_expr_annot: expr -> expr_annot -> expr
126
val update_expr_annot: ident -> expr -> LustreSpec.expr_annot -> expr
128 127
(* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*)
129 128

  
130 129
(* Local Variables: *)
src/inliner.ml
11 11

  
12 12
open LustreSpec
13 13
open Corelang
14
open Utils
15

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

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

  
15 25
let check_node_name id = (fun t -> 
16 26
  match t.top_decl_desc with 
......
90 100
   variables and the code of called node instance added to new_eqs
91 101

  
92 102
*)
93
let rec inline_expr expr locals nodes =
103
let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =
104
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
105
  let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
94 106
  let inline_tuple el = 
95 107
    List.fold_right (fun e (el_tail, locals, eqs, asserts) -> 
96 108
      let e', locals', eqs', asserts' = inline_expr e locals nodes in
......
109 121
    | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
110 122
    | _ -> assert false
111 123
  in
112
    
124
  
113 125
  match expr.expr_desc with
114 126
  | Expr_appl (id, args, reset) ->
115 127
    let args', locals', eqs', asserts' = inline_expr args locals nodes in 
116
    if List.exists (check_node_name id) nodes then 
128
    if List.exists (check_node_name id) nodes && (* the current node call is provided
129
						    as arguments nodes *)
130
      (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, 
131
							      it is explicitely inlined here *)
132
    then 
117 133
      (* The node should be inlined *)
118
      (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
134
       let _ =     Format.eprintf "Inlining call to %s@." id in 
119 135
      let node = try List.find (check_node_name id) nodes 
120 136
	with Not_found -> (assert false) in
121 137
      let node = node_of_top node in
......
164 180
    let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
165 181
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
166 182
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
167
and inline_node nd nodes = 
183
and inline_node ?(selection_on_annotation=false) nd nodes = 
184
  let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
168 185
  let new_locals, eqs, asserts = 
169 186
    List.fold_left (fun (locals, eqs, asserts) eq ->
170 187
      let eq_rhs', locals', new_eqs', asserts' = 
......
319 336
  );
320 337
  res
321 338

  
339
let local_inline basename prog type_env clock_env =
340
  let local_anns = Annotations.get_expr_annotations keyword in
341
  if local_anns != [] then (
342
    let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
343
    ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns;
344
    List.fold_right (fun top accu -> 
345
      ( match top.top_decl_desc with
346
      | Node nd when ISet.mem nd.node_id nodes_with_anns ->
347
	{ top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) }
348
      | _ -> top
349
      )::accu) prog []
350
    
351
)
352
 else
353
  prog
354

  
355

  
322 356
(* Local Variables: *)
323 357
(* compile-command:"make -C .." *)
324 358
(* End: *)
src/main_lustre_compiler.ml
127 127
    if !Options.global_inline &&
128 128
      (match !Options.main_node with | "" -> false | _ -> true) then
129 129
      Inliner.global_inline basename prog type_env clock_env
130
    else
131
      prog
130
    else (* if !Option.has_local_inline *)
131
      Inliner.local_inline basename prog type_env clock_env
132 132
  in
133 133

  
134 134
  (* Delay calculus *)
135
  (*
135
  (* TO BE DONE LATER (Xavier)
136 136
    if(!Options.delay_calculus)
137 137
    then
138 138
    begin
......
146 146
    raise exc
147 147
    end;
148 148
  *)
149
  (*
150
    eprintf "Causality analysis@.@?";
151
    (* Causality analysis *)
152
    begin
153
    try
154
    Causality.check_causal_prog prog
155
    with (Causality.Cycle v) as exc ->
156
    Causality.pp_error err_formatter v;
157
    raise exc
158
    end;
159
  *)
160

  
149
  
161 150
  (* Creating destination directory if needed *)
162 151
  create_dest_dir ();
163 152

  
src/parserLustreSpec.mly
73 73
%nonassoc UMINUS
74 74

  
75 75
%start lustre_annot
76
%type <LustreSpec.expr_annot> lustre_annot
76
%type <LustreSpec.ident -> LustreSpec.expr_annot> lustre_annot
77 77

  
78 78
%start lustre_spec
79 79
%type <LustreSpec.node_annot> lustre_spec
......
287 287
| STRING {Const_string $1}
288 288

  
289 289
lustre_annot:
290
lustre_annot_list EOF { $1 }
290
lustre_annot_list EOF { fun node_id -> $1 }
291 291

  
292 292
lustre_annot_list:
293 293
  { [] } 
src/parser_lustre.mly
37 37

  
38 38
let mkannots annots = { annots = annots; annot_loc = get_loc () }
39 39

  
40
let node_stack : ident list ref = ref []
41
let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack
42
let push_node nd =  node_stack:= nd :: !node_stack
43
let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false
44
let get_current_node () = try List.hd !node_stack with _ -> assert false
45

  
40 46
%}
41 47

  
42 48
%token <int> INT
......
118 124
  UIDENT { $1 }
119 125
| IDENT  { $1 }
120 126

  
127
node_ident_decl:
128
 node_ident { push_node $1; $1 }
129

  
121 130
vdecl_ident:
122 131
  UIDENT { $1 }
123 132
| IDENT  { $1 }
......
176 185
				  nodei_prototype = $13;
177 186
				  nodei_in_lib = $14;})
178 187
     in
188
     pop_node ();
179 189
     (*add_imported_node $3 nd;*) [nd] }
180 190

  
181 191
prototype_opt:
......
188 198

  
189 199
top_decl:
190 200
| CONST cdecl_list { List.rev ($2 false) }
191
| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL 
192
    {let stmts, asserts, annots = $16 in
193
     let nd = mktop_decl false (Node
194
				  {node_id = $3;
195
				   node_type = Types.new_var ();
196
				   node_clock = Clocks.new_var true;
197
				   node_inputs = List.rev $5;
198
				   node_outputs = List.rev $10;
199
				   node_locals = List.rev $14;
200
				   node_gencalls = [];
201
				   node_checks = [];
202
				   node_asserts = asserts; 
203
				   node_stmts = stmts;
204
				   node_dec_stateless = $2;
205
				   node_stateless = None;
206
				   node_spec = $1;
207
				   node_annot = annots})
208
     in
201
| 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 
202
    {
203
      let stmts, asserts, annots = $16 in
204
      (* Declaring eqs annots *)
205
      List.iter (fun ann -> 
206
	List.iter (fun (key, _) -> 
207
	  Annotations.add_node_ann $3 key
208
	) ann.annots
209
      ) annots;
210
     (* Building the node *)
211
      let nd = mktop_decl false (Node
212
				   {node_id = $3;
213
				    node_type = Types.new_var ();
214
				    node_clock = Clocks.new_var true;
215
				    node_inputs = List.rev $5;
216
				    node_outputs = List.rev $10;
217
				    node_locals = List.rev $14;
218
				    node_gencalls = [];
219
				    node_checks = [];
220
				    node_asserts = asserts; 
221
				    node_stmts = stmts;
222
				    node_dec_stateless = $2;
223
				    node_stateless = None;
224
				    node_spec = $1;
225
				    node_annot = annots})
226
      in
209 227
     (*add_node $3 nd;*) [nd] }
210

  
211
nodespec_list:
228
    
229
 nodespec_list:
212 230
 { None }
213 231
| NODESPEC nodespec_list { 
214 232
  (function 
......
350 368
| IDENT { mkexpr (Expr_ident $1) }
351 369
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
352 370
| LPAR ANNOT expr RPAR
353
    {update_expr_annot $3 $2}
371
    {update_expr_annot (get_current_node ()) $3 $2}
354 372
| LPAR expr RPAR
355 373
    {$2}
356 374
| LPAR tuple_expr RPAR

Also available in: Unified diff