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 
8 
(* Create a node that checks whether two other nodes have the same output *)

4 
9 

5 
10 
let check_eq nd1 nd2 =


11 
(* TODO: check that nd1 and nd2 have the same signature *)

6 
12 
let check_nd = Corelang.copy_node nd1 in (* to keep the type info *)

7 
13 
let loc = Location.dummy_loc in

8 
14 
let ok_var =

...  ...  
13 
19 
false,

14 
20 
None,

15 
21 
None)

16 

in


22 
in


23 
let input_e = expr_of_vars loc check_nd.node_inputs in


24 
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


29 
let copy_vars vl post =


30 
let f v = { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_" ^ post } in


31 
List.map f vl


32 
in


33 
let out_vars1 = copy_vars nd1.node_outputs "1" in


34 
let out_vars2 = copy_vars nd1.node_outputs "2" in


35 
let call_n1 = mk_stmt nd1 out_vars1 in


36 
let call_n2 = mk_stmt nd2 out_vars2 in


37 
let build_eq v1 v2 =


38 
let pair = expr_of_vars loc [v1;v2] in


39 
Corelang.mkexpr loc (Expr_appl ("=", pair, None))


40 
in


41 
let rec build_ok vl1 vl2 =


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


50 
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 


54 
(* 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 
}


67 
in

17 
68 
let check_nd = { check_nd with

18 
69 
node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id;

19 

node_outputs = [ok_var];


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);

20 
74 
}

21 
75 
in

22 

check_nd

23 
76 


77 


78 
Global.type_env := Typing.type_node !Global.type_env check_nd loc;


79 
Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc check_nd;


80 


81 
check_nd

24 
82 
(*

25 
83 

26 
84 
TODO:

...  ...  
38 
96 
*)

39 
97 

40 
98 
(* (\* Build the contract: guarentee output = orig_node(input) *\)

41 

* let expr_of_vars vl =

42 

* Corelang.expr_of_expr_list loc

43 

* (List.map Corelang.expr_of_vdecl vl)

44 

* in


99 
*

45 
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

46 
101 
* let input_e = expr_of_vars copy_nd.node_inputs in

47 
102 
* let call_orig_e =
