1

(* Multiple export channels for switched systems:

2

 lustre

3

 matlab

4

 text

5

*)

6

open Lustrec

7

open Lustre_types

8

open Machine_code_types

9

open Seal_utils

10


11

let verbose = true

12


13

let process_sw vars f_e sw =

14

let process_branch g_opt up =

15

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

16

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

17

ensure that no variable is forgotten. *)

18

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

19

let vid = v.var_id in

20

if List.mem_assoc vid remaining then

21

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

22

(List.remove_assoc vid remaining)

23

else (

24

Format.eprintf

25

"Looking for variable %s in remaining expressions: [%a]@."

26

vid

27

(Utils.fprintf_list ~sep:";@ "

28

(fun fmt (id,e) >

29

Format.fprintf fmt

30

"(%s > %a)"

31

id

32

Printers.pp_expr e))

33

remaining;

34

assert false (* Missing variable v in list *)

35

)

36

) vars ([], el)

37

in

38

assert (forgotten = []);

39

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

40

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

41

match g_opt with

42

None > None, new_e, loc

43

 Some g >

44

let g = f_e g in

45

let ee = Corelang.mkeexpr loc g in

46

let new_e = if verbose then

47

{new_e with

48

expr_annot =

49

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

50

annot_loc = loc})} else new_e

51

in

52

Some g, new_e, loc

53

in

54

let rec process_sw f_e sw =

55

match sw with

56

 [] > assert false

57

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

58

let _, up_e, _ = process_branch g_opt up in

59

up_e

60

)

61

 (g_opt,up)::tl >

62

let g_opt, up_e, loc = process_branch g_opt up in

63

match g_opt with

64

 None > (

65

Format.eprintf "SEAL issue: process_sw with %a"

66

(pp_sys Printers.pp_expr) sw

67

;

68

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

69

)

70

 Some g >

71

let tl_e = process_sw f_e tl in

72

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

73

in

74

process_sw f_e sw

75


76


77

let sw_to_lustre m sw_init sw_step init_out update_out =

78

let orig_nd = m.mname in

79

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

80

let vl = (* vl are memories *)

81

match sw_init with

82

 [] > [] (* the system is stateless. Returning an empty list

83

shall do the job *)

84


85

 (gl, up)::_ >

86

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

87

in

88

let loc = Location.dummy_loc in

89

let mem_eq =

90

if m.mmemory = [] then

91

[]

92

else

93

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

94

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

95

[Eq

96

{ eq_loc = loc;

97

eq_lhs = vl;

98

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

99

}]

100

in

101

let output_eq =

102

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

103

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

104

[

105

Eq

106

{ eq_loc = loc;

107

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

108

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

109

};

110

]

111

in

112

let new_nd =

113

{ copy_nd with

114

node_id = copy_nd.node_id ^ "_seal";

115

node_locals = m.mmemory;

116

node_stmts = mem_eq @ output_eq;

117

}

118

in

119

new_nd, orig_nd

120


121


122

let funsw_to_lustre m update_out =

123

let orig_nd = m.mname in

124

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

125

let output_eq =

126

let e_update_out = process_sw copy_nd.node_outputs (fun x > x) update_out in

127

[

128

Eq

129

{ eq_loc = Location.dummy_loc;

130

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

131

eq_rhs = e_update_out

132

};

133

]

134

in

135

let new_nd =

136

{ copy_nd with

137

node_id = copy_nd.node_id ^ "_seal";

138

node_locals = [];

139

node_stmts = output_eq;

140

}

141

in

142

new_nd, orig_nd

143


144


145


146

let to_lustre basename prog new_node orig_node =

147

let loc = Location.dummy_loc in

148

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

149

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

150


151

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

152


153

(* Main output *)

154

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

155

let new_top =

156

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

157

in

158

let out = open_out output_file in

159

let fmt = Format.formatter_of_out_channel out in

160

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

161


162

(* Verif output *)

163

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

164

let out_verif = open_out output_file_verif in

165

let fmt_verif = Format.formatter_of_out_channel out_verif in

166

let check_nd = Lustre_utils.check_eq new_node orig_node in

167

let check_top =

168

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

169

in

170

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

171


172

let node_to_lustre basename prog m sw_init sw_step init_out update_out =

173

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

174

to_lustre basename prog new_node orig_nd

175


176

let fun_to_lustre basename prog m update_out =

177

let new_node, orig_nd = funsw_to_lustre m update_out in

178

to_lustre basename prog new_node orig_nd

179

