## lustrec / src / tools / seal / seal_export.ml @ 03c767b1

History | View | Annotate | Download (4.88 KB)

1 | d75eb6f1 | ploc | (* Multiple export channels for switched systems: |
---|---|---|---|

2 | - lustre |
||

3 | - matlab |
||

4 | - text |
||

5 | *) |
||

6 | open Lustre_types |
||

7 | open Machine_code_types |
||

8 | 03c767b1 | ploc | open Seal_utils |

9 | d75eb6f1 | ploc | |

10 | 5b4c0069 | ploc | let verbose = true |

11 | 03c767b1 | ploc | |

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 | 3e07a17b | ploc | ensure that no variable is forgotten. *) |

17 | 03c767b1 | ploc | 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 | d75eb6f1 | ploc | in |

37 | 03c767b1 | ploc | 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 | d75eb6f1 | ploc | | [] -> 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 | 03c767b1 | ploc | | 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 | d75eb6f1 | ploc | | 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 | 03c767b1 | ploc | process_sw f_e sw |

74 | |||

75 | d75eb6f1 | ploc | |

76 | 03c767b1 | ploc | 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 | 3e07a17b | ploc | 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 | 0292f958 | ploc | let loc = Location.dummy_loc in |

89 | 518951ed | ploc | let new_nd = |

90 | { copy_nd with |
||

91 | d75eb6f1 | ploc | 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 | 0292f958 | ploc | ]; |

104 | 518951ed | ploc | } |

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 | b8dfc744 | ploc | let loc = Location.dummy_loc in |

111 | 518951ed | ploc | let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in |

112 | b8dfc744 | ploc | 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 | 518951ed | ploc | (* 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 | b8dfc744 | ploc | let out = open_out output_file in |

123 | 518951ed | ploc | 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]); |