lustrec / src / automata.ml @ bc7b6c62
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 |
|