Revision b8dfc744 src/lustre_utils.ml
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  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 = 
Also available in: Unified diff