Project

General

Profile

Revision d5fe9ac9 src/automata.ml

View differences:

src/automata.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 Utils
13
open LustreSpec
14
open Corelang
15

  
16
let mkbool loc b =
17
 mkexpr loc (Expr_const (const_of_bool b))
18

  
19
let mkident loc id =
20
 mkexpr loc (Expr_ident id)
21

  
22
let mkfby loc e1 e2 =
23
 mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
24

  
25
let mkidentpair loc restart state =
26
 mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state])
27

  
28
let add_branch (loc, expr, restart, st) cont =
29
 mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont))
30

  
31
let mkhandler loc st unless until locals (stmts, asserts, annots) =
32
 {hand_state = st;
33
  hand_unless = unless;
34
  hand_until = until;
35
  hand_locals = locals;
36
  hand_stmts = stmts;
37
  hand_asserts = asserts;
38
  hand_annots = annots;
39
  hand_loc = loc}
40

  
41
let mkautomata loc id handlers =
42
  {aut_id = id;
43
   aut_handlers = handlers;
44
   aut_loc = loc}
45

  
46
let rec handler_read reads handler =
47
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
48
  let allvars =
49
    List.fold_left (fun read stmt ->
50
      match stmt with
51
      | Eq eq -> get_expr_vars read eq.eq_rhs
52
      | Aut aut -> List.fold_left handler_read read aut.aut_handlers ) reads handler.hand_stmts
53
  in ISet.diff allvars locals
54

  
55
let rec handler_write writes handler =
56
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
57
  let allvars =
58
    List.fold_left (fun write stmt ->
59
      match stmt with
60
      | Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs
61
      | Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts
62
  in ISet.diff allvars locals
63

  
64
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)
65

  
66
let rec rename_stmts_outputs frename stmts =
67
  match stmts with
68
  | []           -> []
69
  | (Eq eq) :: q   -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in
70
		      eq' :: rename_stmts_outputs frename q
71
  | (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in
72
                      let aut' = Aut { aut with aut_handlers = handlers' } in
73
		      aut' :: rename_stmts_outputs frename q
74

  
75
let mk_frename used outputs =
76
  let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in
77
  (fun name -> try IMap.find name table with Not_found -> name)
78
  
79
let node_of_handler nused used node aut_id handler =
80
  let outputs = handler_write ISet.empty handler in
81
  let (new_locals, inputs) = ISet.partition (fun v -> ISet.mem v outputs) (handler_read ISet.empty handler) in
82
  let frename = mk_frename used outputs in
83
  let var_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs) in
84
  let new_var_locals = List.map (fun v -> get_node_var v node) (ISet.elements new_locals) in
85
  let var_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs) in
86
  let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in
87
  let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in
88
  var_outputs,
89
  {
90
    node_id = mk_new_name nused (Format.sprintf "%s_%s_handler" aut_id handler.hand_state);
91
    node_type = Types.new_var ();
92
    node_clock = Clocks.new_var true;
93
    node_inputs = var_inputs;
94
    node_outputs = new_var_outputs;
95
    node_locals = new_var_locals @ handler.hand_locals;
96
    node_gencalls = [];
97
    node_checks = [];
98
    node_asserts = handler.hand_asserts; 
99
    node_stmts = new_output_eqs @ handler.hand_stmts;
100
    node_dec_stateless = false;
101
    node_stateless = None;
102
    node_spec = None;
103
    node_annot = handler.hand_annots
104
  }
105

  
106
let expr_of_exit loc restart state conds tag =
107
  mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
108

  
109
let expr_of_handler loc restart state node tag =
110
  let args = List.map (fun v -> mkexpr loc (Expr_when (mkident loc v.var_id, state, tag))) node.node_inputs in
111
  let arg = mkexpr loc (Expr_tuple args) in
112
  let reset = Some (mkident loc restart) in
113
  mkexpr loc (Expr_appl (node.node_id, arg, reset))
114

  
115
let assign_aut_handlers loc actual_r actual_s hnodes =
116
  let outputs = fst (snd (List.hd hnodes)) in
117
  let assign_handlers = List.map (fun (hs, (_, n)) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in
118
  let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in
119
  let assign_eq = mkeq loc (List.map (fun v -> v.var_id) outputs, assign_expr) in
120
  assign_eq
121

  
122
let typedef_of_automata aut =
123
  let tname = Format.sprintf "%s_type" aut.aut_id in
124
  { tydef_id = tname;
125
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
126
  }
127
(*
128
let expand_automata nused used owner typedef node aut =
129
  let initial = (List.hd aut.aut_handlers).hand_state in
130
  let incoming_r = mk_new_name used (aut.aut_id ^ "__restart_in") in
131
  let incoming_s = mk_new_name used (aut.aut_id ^ "__state_in") in
132
  let actual_r = mk_new_name used (aut.aut_id ^ "__restart_act") in
133
  let actual_s = mk_new_name used (aut.aut_id ^ "__state_act") in
134
  let next_incoming_r = mk_new_name used (aut.aut_id ^ "__next_restart_in") in
135
  let next_incoming_s = mk_new_name used (aut.aut_id ^ "__next_state_in") in
136
  (* merge on incoming_s gives actual_s by the unless equations *)
137
  let actual_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc incoming_r incoming_s h.hand_unless h.hand_state)) aut.aut_handlers in
138
  let actual_expr = mkexpr aut.aut_loc (Expr_merge (incoming_s, unless_handlers)) in
139
  let actual_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in
140
  (* next_incoming_s and initial conditions gives incoming_s *)
141
  let incoming_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) (mkidentpair aut.aut_loc next_incoming_r next_incoming_s) in
142
  let incoming_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], incoming_expr) in
143
  (* merge on actual_s gives handler assigned variables and next_incoming_s by the until equations *)
144
  let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in
145
  let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in
146
  let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in
147
  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in
148
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in
149
  let outputs = fst (snd (List.hd hnodes)) in
150
  let next_incoming_and_assigned_vars = next_incoming_r :: next_incoming_s :: List.map (fun v -> v.var_id) outputs in
151
  let next_incoming_and_assigned_handlers =
152
    List.map (fun h -> ) aut.aut_handlers in
153
  let next_incoming_and_assigned_expr = mkexpr loc (Expr_merge (actual_s, next_incoming_and_assigned_handlers) in
154
  let next_incoming_and_assigned_eq = mkeq aut.aut_loc (next_incoming_and_assigned_vars, next_incoming_and_assigned_expr) in
155
  (* declaration of new local variables, equations and handler nodes *)
156
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in
157
  let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in
158
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in
159
  let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false);
160
                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);
161
                 mkvar_decl aut.aut_loc (next_incoming_r  , tydec_bool, ckdec_any, false);
162
                 mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);
163
                 mkvar_decl aut.aut_loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false);
164
                 mkvar_decl aut.aut_loc (next_incoming_s, tydec_state typedef.tydef_id, ckdec_any, false)] in
165
  let eqs' = [Eq actual_eq; Eq next_incoming_and_assigned_eq; Eq incoming_eq] in
166
  (List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
167
  locals',
168
  eqs')
169
*)
170

  
171
let expand_automata nused used owner typedef node aut =
172
  let initial = (List.hd aut.aut_handlers).hand_state in
173
  let incoming_r = mk_new_name used (aut.aut_id ^ "__restart_in") in
174
  let incoming_s = mk_new_name used (aut.aut_id ^ "__state_in") in
175
  let actual_r = mk_new_name used (aut.aut_id ^ "__restart_act") in
176
  let actual_s = mk_new_name used (aut.aut_id ^ "__state_act") in
177
  let unless_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc incoming_r incoming_s h.hand_unless h.hand_state)) aut.aut_handlers in
178
  let unless_expr = mkexpr aut.aut_loc (Expr_merge (incoming_s, unless_handlers)) in
179
  let unless_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in
180
  let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in
181
  let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in
182
  let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in
183
  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in
184
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in
185
  let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in
186
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in
187
  let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in
188
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in
189
  let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false);
190
                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);
191
                 mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);
192
                 mkvar_decl aut.aut_loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false)] in
193
  let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in
194
  (List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
195
  locals',
196
  eqs')
197

  
198
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs) stmt =
199
  match stmt with
200
  | Eq eq -> (top_types, top_nodes, locals, (Eq eq)::eqs)
201
  | Aut aut ->
202
    let typedef = typedef_of_automata aut in
203
    let used' name = used name || List.exists (fun v -> v.var_id = name) locals in
204
    let nused' name =
205
      nused name ||
206
      List.exists (fun t -> match t.top_decl_desc with
207
      | ImportedNode nd -> nd.nodei_id = name | Node nd -> nd.node_id = name
208
      | _ -> false) top_nodes in
209
    let (top_decls', locals', eqs') = expand_automata nused' used' owner typedef node aut in
210
    let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in
211
    (top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs)
212

  
213
let expand_node_stmts nused used loc owner node =
214
  let (top_types', top_nodes', locals', eqs') =
215
    List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in
216
  let node' = 
217
    { node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in
218
  let top_node = mktop_decl loc owner false (Node node') in
219
  top_types', top_node, top_nodes'
220

  
221
let rec expand_decls_rec nused top_decls =
222
  match top_decls with
223
  | [] -> []
224
  | top_decl::q ->
225
    match top_decl.top_decl_desc with
226
    | Node nd ->
227
      let used name =
228
	   List.exists (fun v -> v.var_id = name) nd.node_inputs
229
	|| List.exists (fun v -> v.var_id = name) nd.node_outputs
230
	|| List.exists (fun v -> v.var_id = name) nd.node_locals in
231
      let (top_types', top_decl', top_nodes') = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in
232
      top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q))
233
    | _       -> top_decl :: expand_decls_rec nused q
234

  
235
let expand_decls top_decls =
236
  let top_names = List.fold_left (fun names t -> match t.top_decl_desc with
237
    | Node nd         -> ISet.add nd.node_id names
238
    | ImportedNode nd -> ISet.add nd.nodei_id names
239
    | _               -> names) ISet.empty top_decls in
240
  let nused name = ISet.mem name top_names in
241
  expand_decls_rec nused top_decls
242

  
243
(* Local Variables: *)
244
(* compile-command:"make -C .." *)
245
(* End: *)
246

  
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 Utils
13
open LustreSpec
14
open Corelang
15

  
16

  
17
type aut_state =
18
    {
19
      incoming_r' : var_decl;
20
      incoming_s' : var_decl;
21
      incoming_r : var_decl;
22
      incoming_s : var_decl;
23
      actual_r : var_decl;
24
      actual_s : var_decl
25
    }
26

  
27
let as_clock var_decl =
28
  let tydec = var_decl.var_dec_type in
29
  { var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } }
30

  
31
let mkbool loc b =
32
 mkexpr loc (Expr_const (const_of_bool b))
33

  
34
let mkident loc id =
35
 mkexpr loc (Expr_ident id)
36

  
37
let mkfby loc e1 e2 =
38
 mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
39

  
40
let mkidentpair loc restart state =
41
 mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state])
42

  
43
let add_branch (loc, expr, restart, st) cont =
44
 mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont))
45

  
46
let mkhandler loc st unless until locals (stmts, asserts, annots) =
47
 {hand_state = st;
48
  hand_unless = unless;
49
  hand_until = until;
50
  hand_locals = locals;
51
  hand_stmts = stmts;
52
  hand_asserts = asserts;
53
  hand_annots = annots;
54
  hand_loc = loc}
55

  
56
let mkautomata loc id handlers =
57
  {aut_id = id;
58
   aut_handlers = handlers;
59
   aut_loc = loc}
60

  
61
let expr_of_exit loc restart state conds tag =
62
  mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
63

  
64
let rec unless_read reads handler =
65
  List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_unless
66

  
67
let rec until_read reads handler =
68
  List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_until
69

  
70
let rec handler_read reads handler =
71
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
72
  let allvars =
73
    List.fold_left (fun read stmt ->
74
      match stmt with
75
      | Eq eq -> get_expr_vars read eq.eq_rhs
76
      | Aut aut -> List.fold_left handler_read read aut.aut_handlers ) reads handler.hand_stmts
77
  in ISet.diff allvars locals
78

  
79
let rec handler_write writes handler =
80
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
81
  let allvars =
82
    List.fold_left (fun write stmt ->
83
      match stmt with
84
      | Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs
85
      | Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts
86
  in ISet.diff allvars locals
87

  
88
let node_vars_of_idents node iset =
89
  List.fold_right (fun v res -> if ISet.mem v.var_id iset then v :: res else res) (get_node_vars node) []
90

  
91
let mkautomata_state used typedef loc id =
92
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in
93
  let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in
94
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in
95
  let incoming_r' = mk_new_name used (id ^ "__next_restart_in") in
96
  let incoming_s' = mk_new_name used (id ^ "__next_state_in") in
97
  let incoming_r = mk_new_name used (id ^ "__restart_in") in
98
  let incoming_s = mk_new_name used (id ^ "__state_in") in
99
  let actual_r = mk_new_name used (id ^ "__restart_act") in
100
  let actual_s = mk_new_name used (id ^ "__state_act") in
101
  {
102
    incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false);
103
    incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false);
104
    incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false);
105
    incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);
106
    actual_r = mkvar_decl loc (actual_r  , tydec_bool, ckdec_any, false);
107
    actual_s = mkvar_decl loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false)
108
  }
109

  
110
let vars_of_aut_state aut_state =
111
  [aut_state.incoming_r'; aut_state.incoming_r; aut_state.actual_r; aut_state.incoming_s'; as_clock aut_state.incoming_s; as_clock aut_state.actual_s]
112

  
113
let node_of_unless nused used node aut_id aut_state handler =
114
  let inputs = unless_read ISet.empty handler in
115
  let var_inputs = aut_state.incoming_r :: aut_state.incoming_s :: (node_vars_of_idents node inputs) in
116
  let var_outputs = aut_state.actual_r :: aut_state.actual_s :: [] in
117
  let expr_outputs = List.fold_right add_branch handler.hand_unless (mkidentpair handler.hand_loc aut_state.incoming_r.var_id aut_state.incoming_s.var_id) in
118
  let eq_outputs = Eq (mkeq handler.hand_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], expr_outputs)) in
119
  let node_id = mk_new_name nused (Format.sprintf "%s__%s_unless" aut_id handler.hand_state) in
120
  let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.incoming_s.var_id, handler.hand_state))) var_inputs in
121
  let reset = Some (mkident handler.hand_loc aut_state.incoming_r.var_id) in
122
  {
123
    node_id = node_id;
124
    node_type = Types.new_var ();
125
    node_clock = Clocks.new_var true;
126
    node_inputs = var_inputs;
127
    node_outputs = var_outputs;
128
    node_locals = [];
129
    node_gencalls = [];
130
    node_checks = [];
131
    node_asserts = []; 
132
    node_stmts = [ eq_outputs ];
133
    node_dec_stateless = false;
134
    node_stateless = None;
135
    node_spec = None;
136
    node_annot = []
137
  },
138
  mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
139

  
140

  
141
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)
142

  
143
let rec rename_stmts_outputs frename stmts =
144
  match stmts with
145
  | []           -> []
146
  | (Eq eq) :: q   -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in
147
		      eq' :: rename_stmts_outputs frename q
148
  | (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in
149
                      let aut' = Aut { aut with aut_handlers = handlers' } in
150
		      aut' :: rename_stmts_outputs frename q
151

  
152
let mk_frename used outputs =
153
  let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in
154
  (fun name -> try IMap.find name table with Not_found -> name)
155

  
156
let node_of_assign_until nused used node aut_id aut_state handler =
157
  let writes = handler_write ISet.empty handler in
158
  let inputs = ISet.diff (handler_read (until_read ISet.empty handler) handler) writes in
159
  let frename = mk_frename used writes in
160
  let var_inputs = node_vars_of_idents node inputs in
161
  let new_var_locals = node_vars_of_idents node writes in
162
  let var_outputs = node_vars_of_idents node writes in
163
  let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in
164
  let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in
165
  let until_expr = List.fold_right add_branch handler.hand_until (mkidentpair handler.hand_loc aut_state.actual_r.var_id aut_state.actual_s.var_id) in
166
  let until_eq = Eq (mkeq handler.hand_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], until_expr)) in
167
  let node_id = mk_new_name nused (Format.sprintf "%s__%s_handler_until" aut_id handler.hand_state) in
168
  let var_inputs = aut_state.actual_r :: aut_state.actual_s :: var_inputs in
169
  let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.actual_s.var_id, handler.hand_state))) var_inputs in
170
  let reset = Some (mkident handler.hand_loc aut_state.actual_r.var_id) in
171
  List.fold_left (fun res v -> ISet.add v.var_id res) ISet.empty var_outputs,
172
  {
173
    node_id = node_id;
174
    node_type = Types.new_var ();
175
    node_clock = Clocks.new_var true;
176
    node_inputs = var_inputs;
177
    node_outputs = aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs;
178
    node_locals = new_var_locals @ handler.hand_locals;
179
    node_gencalls = [];
180
    node_checks = [];
181
    node_asserts = handler.hand_asserts; 
182
    node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts;
183
    node_dec_stateless = false;
184
    node_stateless = None;
185
    node_spec = None;
186
    node_annot = handler.hand_annots
187
  },
188
  mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
189

  
190
let typedef_of_automata aut =
191
  let tname = Format.sprintf "%s__type" aut.aut_id in
192
  { tydef_id = tname;
193
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
194
  }
195

  
196
let expand_automata nused used owner typedef node aut =
197
  let initial = (List.hd aut.aut_handlers).hand_state in
198
  let aut_state = mkautomata_state used typedef aut.aut_loc aut.aut_id in
199
  let unodes = List.map (fun h -> node_of_unless nused used node aut.aut_id aut_state h) aut.aut_handlers in
200
  let aunodes = List.map (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h) aut.aut_handlers in
201
  let all_outputs = List.fold_left (fun all (outputs, _, _) -> ISet.union outputs all) ISet.empty aunodes in
202
  let unless_handlers = List.map2 (fun h (n, c) -> (h.hand_state, c)) aut.aut_handlers unodes in
203
  let unless_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.incoming_s.var_id, unless_handlers)) in
204
  let unless_eq = mkeq aut.aut_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], unless_expr) in
205
  let assign_until_handlers = List.map2 (fun h (_, n, c) -> (h.hand_state, c)) aut.aut_handlers aunodes in
206
  let assign_until_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers)) in
207
  let assign_until_vars = [aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id] @ (ISet.elements all_outputs) in
208
  let assign_until_eq = mkeq aut.aut_loc (assign_until_vars, assign_until_expr) in
209
  let fby_incoming_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id aut_state.incoming_s'.var_id) in
210
  let incoming_eq = mkeq aut.aut_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], fby_incoming_expr) in
211
  let locals' = vars_of_aut_state aut_state in
212
  let eqs' = [Eq unless_eq; Eq assign_until_eq; Eq incoming_eq] in
213
  (  List.map2 (fun h (n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers unodes
214
   @ List.map2 (fun h (_, n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers aunodes,
215
  locals',
216
  eqs')
217

  
218
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs) stmt =
219
  match stmt with
220
  | Eq eq -> (top_types, top_nodes, locals, (Eq eq)::eqs)
221
  | Aut aut ->
222
    let typedef = typedef_of_automata aut in
223
    let used' name = used name || List.exists (fun v -> v.var_id = name) locals in
224
    let nused' name =
225
      nused name ||
226
      List.exists (fun t -> match t.top_decl_desc with
227
      | ImportedNode nd -> nd.nodei_id = name | Node nd -> nd.node_id = name
228
      | _ -> false) top_nodes in
229
    let (top_decls', locals', eqs') = expand_automata nused' used' owner typedef node aut in
230
    let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in
231
    (top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs)
232

  
233
let expand_node_stmts nused used loc owner node =
234
  let (top_types', top_nodes', locals', eqs') =
235
    List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in
236
  let node' = 
237
    { node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in
238
  let top_node = mktop_decl loc owner false (Node node') in
239
  top_types', top_node, top_nodes'
240

  
241
let rec expand_decls_rec nused top_decls =
242
  match top_decls with
243
  | [] -> []
244
  | top_decl::q ->
245
    match top_decl.top_decl_desc with
246
    | Node nd ->
247
      let used name =
248
	   List.exists (fun v -> v.var_id = name) nd.node_inputs
249
	|| List.exists (fun v -> v.var_id = name) nd.node_outputs
250
	|| List.exists (fun v -> v.var_id = name) nd.node_locals in
251
      let (top_types', top_decl', top_nodes') = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in
252
      top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q))
253
    | _       -> top_decl :: expand_decls_rec nused q
254

  
255
let expand_decls top_decls =
256
  let top_names = List.fold_left (fun names t -> match t.top_decl_desc with
257
    | Node nd         -> ISet.add nd.node_id names
258
    | ImportedNode nd -> ISet.add nd.nodei_id names
259
    | _               -> names) ISet.empty top_decls in
260
  let nused name = ISet.mem name top_names in
261
  expand_decls_rec nused top_decls
262

  
263
(* Local Variables: *)
264
(* compile-command:"make -C .." *)
265
(* End: *)
266

  

Also available in: Unified diff