Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / automata.ml @ d5767b5a

History | View | Annotate | Download (8.16 KB)

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 init 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 node_of_handler nused node aut_id handler =
65
  let inputs = handler_read ISet.empty handler in
66
  let outputs = handler_write ISet.empty handler in
67
  {
68
    node_id = mk_new_name nused (Format.sprintf "%s_%s_handler" aut_id handler.hand_state);
69
    node_type = Types.new_var ();
70
    node_clock = Clocks.new_var true;
71
    node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs);
72
    node_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs);
73
    node_locals = handler.hand_locals;
74
    node_gencalls = [];
75
    node_checks = [];
76
    node_asserts = handler.hand_asserts; 
77
    node_stmts = handler.hand_stmts;
78
    node_dec_stateless = false;
79
    node_stateless = None;
80
    node_spec = None;
81
    node_annot = handler.hand_annots
82
  }
83

    
84
let expr_of_exit loc restart state conds tag =
85
  mkexpr loc (Expr_when (List.fold_right add_branch conds (init loc restart state), state, tag))
86

    
87
let expr_of_handler loc restart state node tag =
88
  let arg = mkexpr loc (Expr_tuple (List.map (fun v -> mkident loc v.var_id) node.node_inputs)) in
89
  mkexpr loc (Expr_when (mkexpr loc (Expr_appl (node.node_id, arg, Some (restart, tag_true))), state, tag))
90

    
91
let assign_aut_handlers loc actual_r actual_s hnodes =
92
  let outputs = (snd (List.hd hnodes)).node_outputs in
93
  let assign_handlers = List.map (fun (hs, n) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in
94
  let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in
95
  let assign_eq = mkeq loc (List.map (fun v -> v.var_id) outputs, assign_expr) in
96
  assign_eq
97

    
98
let typedef_of_automata aut =
99
  let tname = Format.sprintf "%s_type" aut.aut_id in
100
  { tydef_id = tname;
101
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
102
  }
103

    
104
let expand_automata nused used owner typedef node aut =
105
  let initial = (List.hd aut.aut_handlers).hand_state in
106
  let incoming_r = mk_new_name used (aut.aut_id ^ "__restart_in") in
107
  let incoming_s = mk_new_name used (aut.aut_id ^ "__state_in") in
108
  let actual_r = mk_new_name used (aut.aut_id ^ "__restart_act") in
109
  let actual_s = mk_new_name used (aut.aut_id ^ "__state_act") in
110
  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
111
  let unless_expr = mkexpr aut.aut_loc (Expr_merge (incoming_s, unless_handlers)) in
112
  let unless_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in
113
  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
114
  let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in
115
  let fby_until_expr = mkfby aut.aut_loc (init aut.aut_loc tag_false initial) until_expr in
116
  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in
117
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused node aut.aut_id h)) aut.aut_handlers in
118
  let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in
119
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in
120
  let tydec_const id = { ty_dec_desc = Tydec_const id; ty_dec_loc = aut.aut_loc } in
121
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in
122
  let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false);
123
                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);
124
                 mkvar_decl aut.aut_loc (incoming_s, tydec_const typedef.tydef_id, ckdec_any, false);
125
                 mkvar_decl aut.aut_loc (actual_s  , tydec_const typedef.tydef_id, ckdec_any, false)] in
126
  let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in
127
  (List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
128
  locals',
129
  eqs')
130

    
131
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs) stmt =
132
  match stmt with
133
  | Eq eq -> (top_types, top_nodes, locals, (Eq eq)::eqs)
134
  | Aut aut ->
135
    let typedef = typedef_of_automata aut in
136
    let used' name = used name || List.exists (fun v -> v.var_id = name) locals in
137
    let nused' name =
138
      nused name ||
139
      List.exists (fun t -> match t.top_decl_desc with
140
      | ImportedNode nd -> nd.nodei_id = name | Node nd -> nd.node_id = name
141
      | _ -> false) top_nodes in
142
    let (top_decls', locals', eqs') = expand_automata nused' used' owner typedef node aut in
143
    let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in
144
    (top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs)
145

    
146
let expand_node_stmts nused used loc owner node =
147
  let (top_types', top_nodes', locals', eqs') =
148
    List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in
149
  let node' = 
150
    { node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in
151
  let top_node = mktop_decl loc owner false (Node node') in
152
  top_types', top_node, top_nodes'
153

    
154
let rec expand_decls_rec nused top_decls =
155
  match top_decls with
156
  | [] -> []
157
  | top_decl::q ->
158
    match top_decl.top_decl_desc with
159
    | Node nd ->
160
      let used name =
161
	   List.exists (fun v -> v.var_id = name) nd.node_inputs
162
	|| List.exists (fun v -> v.var_id = name) nd.node_outputs
163
	|| List.exists (fun v -> v.var_id = name) nd.node_locals in
164
      let (top_types', top_decl', top_nodes') = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in
165
      top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q))
166
    | _       -> top_decl :: expand_decls_rec nused q
167

    
168
let expand_decls top_decls =
169
  let top_names = List.fold_left (fun names t -> match t.top_decl_desc with
170
    | Node nd         -> ISet.add nd.node_id names
171
    | ImportedNode nd -> ISet.add nd.nodei_id names
172
    | _               -> names) ISet.empty top_decls in
173
  let nused name = ISet.mem name top_names in
174
  expand_decls_rec nused top_decls
175

    
176
(* Local Variables: *)
177
(* compile-command:"make -C .." *)
178
(* End: *)
179