1

(* Multiple export channels for switched systems:

2

 lustre

3

 matlab

4

 text

5

*)

6

open Lustre_types

7

open Machine_code_types

8

open Seal_utils

9


10

let verbose = true

11


12

let process_sw vars f_e sw =

13

let process_branch g_opt up =

14

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

15

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

16

ensure that no variable is forgotten. *)

17

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

18

let vid = v.var_id in

19

if List.mem_assoc vid remaining then

20

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

21

(List.remove_assoc vid remaining)

22

else (

23

Format.eprintf

24

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

25

vid

26

(Utils.fprintf_list ~sep:";@ "

27

(fun fmt (id,e) >

28

Format.fprintf fmt

29

"(%s > %a)"

30

id

31

Printers.pp_expr e))

32

remaining;

33

assert false (* Missing variable v in list *)

34

)

35

) vars ([], el)

36

in

37

assert (forgotten = []);

38

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

39

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

40

match g_opt with

41

None > None, new_e, loc

42

 Some g >

43

let g = f_e g in

44

let ee = Corelang.mkeexpr loc g in

45

let new_e = if verbose then

46

{new_e with

47

expr_annot =

48

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

49

annot_loc = loc})} else new_e

50

in

51

Some g, new_e, loc

52

in

53

let rec process_sw f_e sw =

54

match sw with

55

 [] > assert false

56

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

57

let _, up_e, _ = process_branch g_opt up in

58

up_e

59

)

60

 (g_opt,up)::tl >

61

let g_opt, up_e, loc = process_branch g_opt up in

62

match g_opt with

63

 None > (

64

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

65

(pp_sys Printers.pp_expr) sw

66

;

67

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

68

)

69

 Some g >

70

let tl_e = process_sw f_e tl in

71

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

72

in

73

process_sw f_e sw

74


75


76

let sw_to_lustre m sw_init sw_step init_out update_out =

77

let orig_nd = m.mname in

78

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

79

let vl = (* vl are memories *)

80

match sw_init with

81

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

82

shall do the job *)

83


84

 (gl, up)::_ >

85

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

86

in

87

let loc = Location.dummy_loc in

88

let mem_eq =

89

if m.mmemory = [] then

90

[]

91

else

92

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

93

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

94

[Eq

95

{ eq_loc = loc;

96

eq_lhs = vl;

97

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

98

}]

99

in

100

let output_eq =

101

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

102

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

103

[

104

Eq

105

{ eq_loc = loc;

106

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

107

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

108

};

109

]

110

in

111

let new_nd =

112

{ copy_nd with

113

node_id = copy_nd.node_id ^ "_seal";

114

node_locals = m.mmemory;

115

node_stmts = mem_eq @ output_eq;

116

}

117

in

118

new_nd, orig_nd

119


120


121

let funsw_to_lustre m update_out =

122

let orig_nd = m.mname in

123

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

124

let output_eq =

125

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

126

[

127

Eq

128

{ eq_loc = Location.dummy_loc;

129

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

130

eq_rhs = e_update_out

131

};

132

]

133

in

134

let new_nd =

135

{ copy_nd with

136

node_id = copy_nd.node_id ^ "_seal";

137

node_locals = [];

138

node_stmts = output_eq;

139

}

140

in

141

new_nd, orig_nd

142


143


144


145

let to_lustre basename prog new_node orig_node =

146

let loc = Location.dummy_loc in

147

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

148

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

149


150

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

151


152

(* Main output *)

153

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

154

let new_top =

155

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

156

in

157

let out = open_out output_file in

158

let fmt = Format.formatter_of_out_channel out in

159

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

160


161

(* Verif output *)

162

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

163

let out_verif = open_out output_file_verif in

164

let fmt_verif = Format.formatter_of_out_channel out_verif in

165

let check_nd = Lustre_utils.check_eq new_node orig_node in

166

let check_top =

167

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

168

in

169

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

170


171

let node_to_lustre basename prog m sw_init sw_step init_out update_out =

172

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

173

to_lustre basename prog new_node orig_nd

174


175

let fun_to_lustre basename prog m update_out =

176

let new_node, orig_nd = funsw_to_lustre m update_out in

177

to_lustre basename prog new_node orig_nd

178

