1

open Lustre_types

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


8

(* Create a node that checks whether two other nodes have the same output *)

9


10

let check_eq nd1 nd2 =

11

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

14

let ok_var =

15

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)

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

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

}

75

in

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

82

(*

83


84

TODO:

85


86

construire

87


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)

91


92

et on ajoute le contrat guarantee ok

93

in

94

check_nd

95


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

