1

(* Multiple export channels for switched systems:

2

 lustre

3

 matlab

4

 text

5

*)

6

open Lustre_types

7

open Machine_code_types

8


9

let verbose = false

10


11

let to_lustre m sw_init sw_step init_out update_out =

12

let orig_nd = m.mname in

13

let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in

14

let vl = (* memories *)

15

match sw_init with

16

 [] > assert false

17

 (gl, up)::_ > List.map (fun (v,_) > v) up

18

in

19

(* let add_pre sw =

20

List.map (fun (gl, up) >

21

List.map (fun (g,b) >

22

if not b then

23

assert false (* should be guaranted by constrauction *)

24

else

25

add_pre_expr vl g) gl,

26

List.map (fun (v,e) > add_pre_expr vl e) up

27

) sw

28

in

29

*)

30


31

let rec process_sw f_e sw =

32

let process_branch g_opt up =

33

let el = List.map (fun (v,e) > f_e e) up in

34

let loc = (List.hd el).expr_loc in

35

let new_e = Corelang.mkexpr loc (Expr_tuple el) in

36

match g_opt with

37

None > None, new_e, loc

38

 Some g >

39

let g = f_e g in

40

let ee = Corelang.mkeexpr loc g in

41

let new_e = if verbose then

42

{new_e with

43

expr_annot =

44

Some ({annots = [["seal";"guards"],ee];

45

annot_loc = loc})} else new_e

46

in

47

Some g, new_e, loc

48

in

49

match sw with

50

 [] > assert false

51

 [g_opt,up] > ((* last case, no need to guard it *)

52

let _, up_e, _ = process_branch g_opt up in

53

up_e

54

)

55

 (g_opt,up)::tl >

56

let g_opt, up_e, loc = process_branch g_opt up in

57

match g_opt with

58

 None > assert false (* How could this happen anyway ? *)

59

 Some g >

60

let tl_e = process_sw f_e tl in

61

Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e))

62

in

63


64

let e_init = process_sw (fun x > x) sw_init in

65

let e_step = process_sw (Corelang.add_pre_expr vl) sw_step in

66

let e_init_out = process_sw (fun x > x) init_out in

67

let e_update_out = process_sw (Corelang.add_pre_expr vl) update_out in

68

let loc = Location.dummy_loc in

69

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

70

let expr_of_vars vl =

71

Corelang.expr_of_expr_list loc

72

(List.map Corelang.expr_of_vdecl vl)

73

in

74

let input_e = expr_of_vars copy_nd.node_inputs in

75

let output_e = expr_of_vars copy_nd.node_outputs in

76

let call_orig_e =

77

Corelang.mkexpr loc (Expr_appl (orig_nd.node_id, input_e , None)) in

78

let args = Corelang.mkexpr loc (Expr_tuple([output_e; call_orig_e])) in

79

let eq_expr = (Corelang.mkexpr loc (Expr_appl ("=", args, None))) in

80

let contract = {

81

consts = [];

82

locals = [];

83

stmts = [];

84

assume = [];

85

guarantees = [Corelang.mkeexpr loc eq_expr];

86

modes = [];

87

imports = [];

88

spec_loc = loc;

89


90

}

91

in

92

{ copy_nd with

93

node_id = copy_nd.node_id ^ "_seal";

94

node_locals = m.mmemory;

95

node_stmts = [Eq

96

{ eq_loc = loc;

97

eq_lhs = vl;

98

eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step))

99

};

100

Eq

101

{ eq_loc = loc;

102

eq_lhs = List.map (fun v > v.var_id) copy_nd.node_outputs;

103

eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))

104

};

105

];

106

node_spec = Some (Contract contract);

107


108

(*

109

il faut mettre un pre devant chaque memoire dans les updates comme dans les gardes par contre pas besoin de mettre de pre devant les entrees, ni dans les updates, ni dans les gardes

110


111


112

ecrire une expression

113


114

(mem1, mem2, mem3) = if garde1 then (e1,e2,e2) else if garde2 then (e1,e2,e3) else ...... else (* garde3 *) (e1,e2,e2)

115


116

Il faut aussi calculer la fonction de sortie

117


118

out1,out2 = if garde1 then e1,e2 else if garde2 ....

119

*)

120

}
