Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/lustre_utils.ml | ||
---|---|---|
1 | 1 |
open Lustre_types |
2 | 2 |
|
3 |
let expr_of_vars loc vl = |
|
4 |
Corelang.expr_of_expr_list loc |
|
5 |
(List.map Corelang.expr_of_vdecl vl) |
|
6 |
|
|
7 |
|
|
3 |
let expr_of_vars loc vl = |
|
4 |
Corelang.expr_of_expr_list loc (List.map Corelang.expr_of_vdecl vl) |
|
5 |
|
|
8 | 6 |
(* Create a node that checks whether two other nodes have the same output *) |
9 | 7 |
|
10 | 8 |
let check_eq nd1 nd2 = |
11 | 9 |
(* TODO: check that nd1 and nd2 have the same signature *) |
12 |
let check_nd = Corelang.copy_node nd1 in (* to keep the type info *) |
|
13 |
let loc = Location.dummy_loc in |
|
10 |
let check_nd = Corelang.copy_node nd1 in |
|
11 |
(* to keep the type info *) |
|
12 |
let loc = Location.dummy_loc in |
|
14 | 13 |
let ok_var = |
15 | 14 |
Corelang.mkvar_decl loc ~orig:false |
16 |
("__OK", |
|
17 |
Corelang.mktyp loc Tydec_bool, |
|
18 |
Corelang.mkclock loc Ckdec_any, |
|
19 |
false,
|
|
20 |
None, |
|
21 |
None)
|
|
15 |
( "__OK",
|
|
16 |
Corelang.mktyp loc Tydec_bool,
|
|
17 |
Corelang.mkclock loc Ckdec_any,
|
|
18 |
false, |
|
19 |
None,
|
|
20 |
None )
|
|
22 | 21 |
in |
23 | 22 |
let input_e = expr_of_vars loc check_nd.node_inputs in |
24 | 23 |
let mk_stmt nd out_vars = |
25 |
let call_e = Corelang.mkexpr loc (Expr_appl (nd.node_id, input_e , None)) in |
|
26 |
Eq ( |
|
27 |
Corelang.mkeq loc |
|
28 |
(List.map (fun v -> v.var_id) out_vars, call_e)) in |
|
24 |
let call_e = Corelang.mkexpr loc (Expr_appl (nd.node_id, input_e, None)) in |
|
25 |
Eq (Corelang.mkeq loc (List.map (fun v -> v.var_id) out_vars, call_e)) |
|
26 |
in |
|
29 | 27 |
let copy_vars vl post = |
30 |
let f v = { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_" ^ post } in |
|
28 |
let f v = |
|
29 |
{ (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_" ^ post } |
|
30 |
in |
|
31 | 31 |
List.map f vl |
32 | 32 |
in |
33 | 33 |
let out_vars1 = copy_vars nd1.node_outputs "1" in |
... | ... | |
35 | 35 |
let call_n1 = mk_stmt nd1 out_vars1 in |
36 | 36 |
let call_n2 = mk_stmt nd2 out_vars2 in |
37 | 37 |
let build_eq v1 v2 = |
38 |
let pair = expr_of_vars loc [v1;v2] in
|
|
38 |
let pair = expr_of_vars loc [ v1; v2 ] in
|
|
39 | 39 |
Corelang.mkexpr loc (Expr_appl ("=", pair, None)) |
40 | 40 |
in |
41 | 41 |
let rec build_ok vl1 vl2 = |
42 | 42 |
match vl1, vl2 with |
43 |
| [v1], [v2] -> build_eq v1 v2 |
|
44 |
| hd1::tl1, hd2::tl2 -> |
|
45 |
let e1 = (build_eq hd1 hd2) in |
|
46 |
let e2 = build_ok tl1 tl2 in |
|
47 |
let e = Corelang.mkexpr loc (Expr_tuple [e1; e2]) in |
|
48 |
Corelang.mkexpr loc (Expr_appl ("&&", e, None)) |
|
49 |
| _ -> assert false |
|
43 |
| [ v1 ], [ v2 ] -> |
|
44 |
build_eq v1 v2 |
|
45 |
| hd1 :: tl1, hd2 :: tl2 -> |
|
46 |
let e1 = build_eq hd1 hd2 in |
|
47 |
let e2 = build_ok tl1 tl2 in |
|
48 |
let e = Corelang.mkexpr loc (Expr_tuple [ e1; e2 ]) in |
|
49 |
Corelang.mkexpr loc (Expr_appl ("&&", e, None)) |
|
50 |
| _ -> |
|
51 |
assert false |
|
50 | 52 |
in |
51 |
let ok_expr = build_ok out_vars1 out_vars2 in
|
|
52 |
let ok_stmt = Eq (Corelang.mkeq loc ([ok_var.var_id], ok_expr)) in
|
|
53 |
let ok_expr = build_ok out_vars1 out_vars2 in
|
|
54 |
let ok_stmt = Eq (Corelang.mkeq loc ([ ok_var.var_id ], ok_expr)) in
|
|
53 | 55 |
|
54 | 56 |
(* Building contract *) |
55 |
let ok_e = Corelang.expr_of_vdecl ok_var in
|
|
56 |
let contract = {
|
|
57 |
consts = [];
|
|
58 |
locals = [];
|
|
59 |
stmts = [];
|
|
60 |
assume = [];
|
|
61 |
guarantees = [Corelang.mkeexpr loc ok_e];
|
|
62 |
modes = [];
|
|
63 |
imports = [];
|
|
64 |
spec_loc = loc;
|
|
65 |
|
|
66 |
}
|
|
57 |
let ok_e = Corelang.expr_of_vdecl ok_var in |
|
58 |
let contract = |
|
59 |
{
|
|
60 |
consts = [];
|
|
61 |
locals = [];
|
|
62 |
stmts = [];
|
|
63 |
assume = [];
|
|
64 |
guarantees = [ Corelang.mkeexpr loc ok_e ];
|
|
65 |
modes = [];
|
|
66 |
imports = [];
|
|
67 |
spec_loc = loc; |
|
68 |
} |
|
67 | 69 |
in |
68 |
let check_nd = { check_nd with |
|
69 |
node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id; |
|
70 |
node_outputs = [ok_var]; |
|
71 |
node_locals = out_vars1 @ out_vars2; |
|
72 |
node_stmts = [call_n1; call_n2; ok_stmt]; |
|
73 |
node_spec = Some (Contract contract); |
|
74 |
} |
|
70 |
let check_nd = |
|
71 |
{ |
|
72 |
check_nd with |
|
73 |
node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id; |
|
74 |
node_outputs = [ ok_var ]; |
|
75 |
node_locals = out_vars1 @ out_vars2; |
|
76 |
node_stmts = [ call_n1; call_n2; ok_stmt ]; |
|
77 |
node_spec = Some (Contract contract); |
|
78 |
} |
|
75 | 79 |
in |
76 | 80 |
|
77 |
|
|
78 | 81 |
Global.type_env := Typing.type_node !Global.type_env check_nd loc; |
79 | 82 |
Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc check_nd; |
80 |
|
|
81 |
check_nd |
|
82 |
(* |
|
83 | 83 |
|
84 |
TODO: |
|
84 |
check_nd |
|
85 |
(* TODO: |
|
85 | 86 |
|
86 |
construire
|
|
87 |
construire |
|
87 | 88 |
|
88 |
les variables temporaires pour les outputs de l'un et de l'autre |
|
89 |
les statements d'appels de nodes |
|
90 |
ok = and (o1 = o2) |
|
89 |
les variables temporaires pour les outputs de l'un et de l'autre les |
|
90 |
statements d'appels de nodes ok = and (o1 = o2) |
|
91 | 91 |
|
92 |
et on ajoute le contrat guarantee ok |
|
93 |
in |
|
94 |
check_nd |
|
92 |
et on ajoute le contrat guarantee ok in check_nd *) |
|
95 | 93 |
|
96 |
*) |
|
97 |
|
|
98 |
(* (\* Build the contract: guarentee output = orig_node(input) *\) |
|
99 |
* |
|
100 |
* let local_outputs = List.map (fun v -> { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_local" } ) copy_nd.node_outputs in |
|
101 |
* let input_e = expr_of_vars copy_nd.node_inputs in |
|
102 |
* let call_orig_e = |
|
103 |
* Corelang.mkexpr loc (Expr_appl (orig_nd.node_id, input_e , None)) in |
|
104 |
* let build_orig_outputs = |
|
105 |
* Eq ( |
|
106 |
* Corelang.mkeq loc |
|
107 |
* (List.map (fun v -> v.var_id) local_outputs, call_orig_e)) in |
|
108 |
* let eq_expr = Corelang.expr_of_expr_list loc ( |
|
109 |
* List.map2 (fun v1 v2 -> |
|
110 |
* let args = expr_of_vars [v1;v2] in |
|
111 |
* Corelang.mkexpr loc (Expr_appl ("=", args, None))) |
|
112 |
* copy_nd.node_outputs local_outputs |
|
113 |
* ) |
|
114 |
* in |
|
115 |
* let contract = { |
|
116 |
* consts = []; |
|
117 |
* locals = local_outputs; |
|
118 |
* stmts = [build_orig_outputs]; |
|
119 |
* assume = []; |
|
120 |
* guarantees = [Corelang.mkeexpr loc eq_expr]; |
|
121 |
* modes = []; |
|
122 |
* imports = []; |
|
123 |
* spec_loc = loc; |
|
124 |
* |
|
125 |
* } |
|
126 |
* in *) |
|
127 |
|
|
94 |
(* (\* Build the contract: guarentee output = orig_node(input) *\) * * let |
|
95 |
local_outputs = List.map (fun v -> { (Corelang.copy_var_decl v) with var_id = |
|
96 |
v.var_id ^ "_local" } ) copy_nd.node_outputs in * let input_e = expr_of_vars |
|
97 |
copy_nd.node_inputs in * let call_orig_e = * Corelang.mkexpr loc (Expr_appl |
|
98 |
(orig_nd.node_id, input_e , None)) in * let build_orig_outputs = * Eq ( * |
|
99 |
Corelang.mkeq loc * (List.map (fun v -> v.var_id) local_outputs, |
|
100 |
call_orig_e)) in * let eq_expr = Corelang.expr_of_expr_list loc ( * List.map2 |
|
101 |
(fun v1 v2 -> * let args = expr_of_vars [v1;v2] in * Corelang.mkexpr loc |
|
102 |
(Expr_appl ("=", args, None))) * copy_nd.node_outputs local_outputs * ) * in |
|
103 |
* let contract = { * consts = []; * locals = local_outputs; * stmts = |
|
104 |
[build_orig_outputs]; * assume = []; * guarantees = [Corelang.mkeexpr loc |
|
105 |
eq_expr]; * modes = []; * imports = []; * spec_loc = loc; * * } * in *) |
Also available in: Unified diff
reformatting