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 = true

10


11

let sw_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 process_sw vars f_e sw =

32

let process_branch g_opt up =

33

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

34

(* Sorting list of elements, according to vars, safety check to

35

ensure that no variable is forgotten. *)

36

let el, forgotten = List.fold_right (fun v (res, remaining) >

37

let vid = v.var_id in

38

if List.mem_assoc vid remaining then

39

((List.assoc vid remaining)::res),

40

(List.remove_assoc vid remaining)

41

else

42

assert false (* Missing variable v in list *)

43

) vars ([], el)

44

in

45

assert (forgotten = []);

46

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

47

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

48

match g_opt with

49

None > None, new_e, loc

50

 Some g >

51

let g = f_e g in

52

let ee = Corelang.mkeexpr loc g in

53

let new_e = if verbose then

54

{new_e with

55

expr_annot =

56

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

57

annot_loc = loc})} else new_e

58

in

59

Some g, new_e, loc

60

in

61

let rec process_sw f_e sw =

62

match sw with

63

 [] > assert false

64

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

65

let _, up_e, _ = process_branch g_opt up in

66

up_e

67

)

68

 (g_opt,up)::tl >

69

let g_opt, up_e, loc = process_branch g_opt up in

70

match g_opt with

71

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

72

 Some g >

73

let tl_e = process_sw f_e tl in

74

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

75

in

76

process_sw f_e sw

77

in

78


79

let e_init = process_sw m.mmemory (fun x > x) sw_init in

80

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

81

let e_init_out = process_sw copy_nd.node_outputs (fun x > x) init_out in

82

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

83

let loc = Location.dummy_loc in

84

let new_nd =

85

{ copy_nd with

86

node_id = copy_nd.node_id ^ "_seal";

87

node_locals = m.mmemory;

88

node_stmts = [Eq

89

{ eq_loc = loc;

90

eq_lhs = vl;

91

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

92

};

93

Eq

94

{ eq_loc = loc;

95

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

96

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

97

};

98

];

99

(*node_spec = Some (Contract contract);*)

100


101

(*

102

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

103


104


105

ecrire une expression

106


107

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

108


109

Il faut aussi calculer la fonction de sortie

110


111

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

112

*)

113

}

114

in

115

new_nd, orig_nd

116


117


118

let to_lustre basename prog m sw_init sw_step init_out update_out =

119

let loc = Location.dummy_loc in

120

let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in

121

Global.type_env := Typing.type_node !Global.type_env new_node loc;

122

Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;

123


124

(* Format.eprintf "%a@." Printers.pp_node new_node; *)

125


126

(* Main output *)

127

let output_file = !Options.dest_dir ^ "/" ^ basename ^ "_seal.lus" in

128

let new_top =

129

Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node)

130

in

131

let out = open_out output_file in

132

let fmt = Format.formatter_of_out_channel out in

133

Format.fprintf fmt "%a@." Printers.pp_prog [new_top];

134


135

(* Verif output *)

136

let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in

137

let out_verif = open_out output_file_verif in

138

let fmt_verif = Format.formatter_of_out_channel out_verif in

139

let check_nd = Lustre_utils.check_eq new_node orig_nd in

140

let check_top =

141

Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd)

142

in

143

Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]);
