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 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 = (* memories *)

80

match sw_init with

81

 [] > assert false

82

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

83

in

84

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

85

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

86

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

87

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

88

let loc = Location.dummy_loc in

89

let new_nd =

90

{ copy_nd with

91

node_id = copy_nd.node_id ^ "_seal";

92

node_locals = m.mmemory;

93

node_stmts = [Eq

94

{ eq_loc = loc;

95

eq_lhs = vl;

96

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

97

};

98

Eq

99

{ eq_loc = loc;

100

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

101

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

102

};

103

];

104

}

105

in

106

new_nd, orig_nd

107


108


109

let to_lustre basename prog m sw_init sw_step init_out update_out =

110

let loc = Location.dummy_loc in

111

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

112

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

113

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

114


115

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

116


117

(* Main output *)

118

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

119

let new_top =

120

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

121

in

122

let out = open_out output_file in

123

let fmt = Format.formatter_of_out_channel out in

124

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

125


126

(* Verif output *)

127

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

128

let out_verif = open_out output_file_verif in

129

let fmt_verif = Format.formatter_of_out_channel out_verif in

130

let check_nd = Lustre_utils.check_eq new_node orig_nd in

131

let check_top =

132

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

133

in

134

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