## lustrec / src / lustreSpec.ml @ ca88e660

History | View | Annotate | Download (7.21 KB)

1 | b38ffff3 | ploc | (********************************************************************) |
---|---|---|---|

2 | (* *) |
||

3 | (* The LustreC compiler toolset / The LustreC Development Team *) |
||

4 | (* Copyright 2012 - -- ONERA - CNRS - INPT *) |
||

5 | (* *) |
||

6 | (* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
||

7 | (* under the terms of the GNU Lesser General Public License *) |
||

8 | (* version 2.1. *) |
||

9 | (* *) |
||

10 | (********************************************************************) |
||

11 | |||

12 | 0cbf0839 | ploc | open Format |

13 | |||

14 | type ident = Utils.ident |
||

15 | type rat = Utils.rat |
||

16 | type tag = Utils.tag |
||

17 | 36454535 | ploc | type label = Utils.ident |

18 | 0cbf0839 | ploc | |

19 | type type_dec = |
||

20 | {ty_dec_desc: type_dec_desc; |
||

21 | ty_dec_loc: Location.t} |
||

22 | |||

23 | and type_dec_desc = |
||

24 | | Tydec_any |
||

25 | | Tydec_int |
||

26 | | Tydec_real |
||

27 | 53206908 | xthirioux | (* | Tydec_float *) |

28 | 0cbf0839 | ploc | | Tydec_bool |

29 | | Tydec_clock of type_dec_desc |
||

30 | | Tydec_const of ident |
||

31 | | Tydec_enum of ident list |
||

32 | 6560bb94 | xthirioux | | Tydec_struct of (ident * type_dec_desc) list |

33 | 0cbf0839 | ploc | | Tydec_array of Dimension.dim_expr * type_dec_desc |

34 | |||

35 | 70e1006b | xthirioux | type typedec_desc = |

36 | {tydec_id: ident} |
||

37 | |||

38 | type typedef_desc = |
||

39 | {tydef_id: ident; |
||

40 | tydef_desc: type_dec_desc} |
||

41 | 6aeb3388 | xthirioux | |

42 | 0cbf0839 | ploc | type clock_dec = |

43 | {ck_dec_desc: clock_dec_desc; |
||

44 | ck_dec_loc: Location.t} |
||

45 | |||

46 | and clock_dec_desc = |
||

47 | | Ckdec_any |
||

48 | | Ckdec_bool of (ident * ident) list |
||

49 | | Ckdec_pclock of int * rat |
||

50 | |||

51 | 01d48bb0 | xthirioux | type constant = |

52 | | Const_int of int |
||

53 | 53206908 | xthirioux | | Const_real of Num.num * int * string (* (a,b, c) means a * 10^-b. c is the original string *) |

54 | (* | Const_float of float *) |
||

55 | 01d48bb0 | xthirioux | | Const_array of constant list |

56 | | Const_tag of label |
||

57 | | Const_string of string (* used only for annotations *) |
||

58 | | Const_struct of (label * constant) list |
||

59 | |||

60 | type quantifier_type = Exists | Forall |
||

61 | |||

62 | 0cbf0839 | ploc | type var_decl = |

63 | {var_id: ident; |
||

64 | 6a1a01d2 | xthirioux | var_orig:bool; |

65 | 0cbf0839 | ploc | var_dec_type: type_dec; |

66 | var_dec_clock: clock_dec; |
||

67 | var_dec_const: bool; |
||

68 | 01d48bb0 | xthirioux | var_dec_value: expr option; |

69 | 0cbf0839 | ploc | mutable var_type: Types.type_expr; |

70 | mutable var_clock: Clocks.clock_expr; |
||

71 | var_loc: Location.t} |
||

72 | |||

73 | 0038002e | ploc | (** The core language and its ast. Every element of the ast contains its |

74 | location in the program text. The type and clock of an ast element |
||

75 | is mutable (and initialized to dummy values). This avoids to have to |
||

76 | duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *) |
||

77 | |||

78 | 0cbf0839 | ploc | (* The tag of an expression is a unique identifier used to distinguish |

79 | different instances of the same node *) |
||

80 | 01d48bb0 | xthirioux | and expr = |

81 | 0038002e | ploc | {expr_tag: tag; |

82 | expr_desc: expr_desc; |
||

83 | mutable expr_type: Types.type_expr; |
||

84 | mutable expr_clock: Clocks.clock_expr; |
||

85 | mutable expr_delay: Delay.delay_expr; |
||

86 | mutable expr_annot: expr_annot option; |
||

87 | expr_loc: Location.t} |
||

88 | |||

89 | and expr_desc = |
||

90 | | Expr_const of constant |
||

91 | | Expr_ident of ident |
||

92 | | Expr_tuple of expr list |
||

93 | | Expr_ite of expr * expr * expr |
||

94 | | Expr_arrow of expr * expr |
||

95 | | Expr_fby of expr * expr |
||

96 | | Expr_array of expr list |
||

97 | | Expr_access of expr * Dimension.dim_expr |
||

98 | | Expr_power of expr * Dimension.dim_expr |
||

99 | | Expr_pre of expr |
||

100 | | Expr_when of expr * ident * label |
||

101 | | Expr_merge of ident * (label * expr) list |
||

102 | | Expr_appl of call_t |
||

103 | 70e1006b | xthirioux | |

104 | 6a1a01d2 | xthirioux | and call_t = ident * expr * expr option |

105 | (* The third part denotes the boolean condition for resetting *) |
||

106 | 70e1006b | xthirioux | |

107 | and eq = |
||

108 | {eq_lhs: ident list; |
||

109 | eq_rhs: expr; |
||

110 | eq_loc: Location.t} |
||

111 | |||

112 | 0038002e | ploc | (* The tag of an expression is a unique identifier used to distinguish |

113 | different instances of the same node *) |
||

114 | 70e1006b | xthirioux | and eexpr = |

115 | 0cbf0839 | ploc | {eexpr_tag: tag; |

116 | 0038002e | ploc | eexpr_qfexpr: expr; |

117 | eexpr_quantifiers: (quantifier_type * var_decl list) list; |
||

118 | 0cbf0839 | ploc | mutable eexpr_type: Types.type_expr; |

119 | mutable eexpr_clock: Clocks.clock_expr; |
||

120 | 0038002e | ploc | mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; |

121 | 0cbf0839 | ploc | eexpr_loc: Location.t} |

122 | |||

123 | 70e1006b | xthirioux | and expr_annot = |

124 | {annots: (string list * eexpr) list; |
||

125 | annot_loc: Location.t} |
||

126 | 0cbf0839 | ploc | |

127 | type node_annot = { |
||

128 | requires: eexpr list; |
||

129 | 0038002e | ploc | ensures: eexpr list; |

130 | behaviors: (string * eexpr list * eexpr list * Location.t) list; |
||

131 | spec_loc: Location.t; |
||

132 | 0cbf0839 | ploc | } |

133 | 79614a15 | xthirioux | |

134 | type offset = |
||

135 | | Index of Dimension.dim_expr |
||

136 | | Field of label |
||

137 | |||

138 | 0038002e | ploc | type assert_t = |

139 | { |
||

140 | assert_expr: expr; |
||

141 | 36454535 | ploc | assert_loc: Location.t; |

142 | 1eda3e78 | xthirioux | } |

143 | |||

144 | type statement = |
||

145 | | Eq of eq |
||

146 | | Aut of automata_desc |
||

147 | 0038002e | ploc | |

148 | 1eda3e78 | xthirioux | and automata_desc = |

149 | 70e1006b | xthirioux | {aut_id : ident; |

150 | aut_handlers: handler_desc list; |
||

151 | aut_loc: Location.t} |
||

152 | |||

153 | and handler_desc = |
||

154 | {hand_state: ident; |
||

155 | 29ced7be | xthirioux | hand_unless: (Location.t * expr * bool * ident) list; |

156 | hand_until: (Location.t * expr * bool * ident) list; |
||

157 | 70e1006b | xthirioux | hand_locals: var_decl list; |

158 | 1eda3e78 | xthirioux | hand_stmts: statement list; |

159 | 29ced7be | xthirioux | hand_asserts: assert_t list; |

160 | hand_annots: expr_annot list; |
||

161 | 70e1006b | xthirioux | hand_loc: Location.t} |

162 | |||

163 | 0038002e | ploc | type node_desc = |

164 | {node_id: ident; |
||

165 | mutable node_type: Types.type_expr; |
||

166 | mutable node_clock: Clocks.clock_expr; |
||

167 | node_inputs: var_decl list; |
||

168 | node_outputs: var_decl list; |
||

169 | node_locals: var_decl list; |
||

170 | mutable node_gencalls: expr list; |
||

171 | mutable node_checks: Dimension.dim_expr list; |
||

172 | node_asserts: assert_t list; |
||

173 | 1eda3e78 | xthirioux | node_stmts: statement list; |

174 | 0038002e | ploc | mutable node_dec_stateless: bool; |

175 | mutable node_stateless: bool option; |
||

176 | node_spec: node_annot option; |
||

177 | node_annot: expr_annot list; |
||

178 | } |
||

179 | |||

180 | type imported_node_desc = |
||

181 | {nodei_id: ident; |
||

182 | mutable nodei_type: Types.type_expr; |
||

183 | mutable nodei_clock: Clocks.clock_expr; |
||

184 | nodei_inputs: var_decl list; |
||

185 | nodei_outputs: var_decl list; |
||

186 | nodei_stateless: bool; |
||

187 | nodei_spec: node_annot option; |
||

188 | nodei_prototype: string option; |
||

189 | 53206908 | xthirioux | nodei_in_lib: string list; |

190 | 0038002e | ploc | } |

191 | |||

192 | type const_desc = |
||

193 | {const_id: ident; |
||

194 | const_loc: Location.t; |
||

195 | const_value: constant; |
||

196 | mutable const_type: Types.type_expr; |
||

197 | } |
||

198 | |||

199 | type top_decl_desc = |
||

200 | | Node of node_desc |
||

201 | 70e1006b | xthirioux | | Const of const_desc |

202 | 0038002e | ploc | | ImportedNode of imported_node_desc |

203 | | Open of bool * string (* the boolean set to true denotes a local |
||

204 | lusi vs a lusi installed at system level *) |
||

205 | 70e1006b | xthirioux | | TypeDef of typedef_desc |

206 | 0038002e | ploc | |

207 | type top_decl = |
||

208 | 70e1006b | xthirioux | {top_decl_desc: top_decl_desc; (* description of the symbol *) |

209 | top_decl_owner: Location.filename; (* the module where it is defined *) |
||

210 | top_decl_itf: bool; (* header or source file ? *) |
||

211 | top_decl_loc: Location.t} (* the location where it is defined *) |
||

212 | 0038002e | ploc | |

213 | type program = top_decl list |
||

214 | |||

215 | 830de634 | ploc | type dep_t = Dep of |

216 | bool |
||

217 | * ident |
||

218 | * (top_decl list) |
||

219 | * bool (* is stateful *) |
||

220 | |||

221 | 53206908 | xthirioux | |

222 | (************ Machine code types *************) |
||

223 | |||

224 | type value_t = |
||

225 | { |
||

226 | value_desc: value_t_desc; |
||

227 | value_type: Types.type_expr; |
||

228 | value_annot: expr_annot option |
||

229 | } |
||

230 | and value_t_desc = |
||

231 | | Cst of constant |
||

232 | | LocalVar of var_decl |
||

233 | | StateVar of var_decl |
||

234 | | Fun of ident * value_t list |
||

235 | | Array of value_t list |
||

236 | | Access of value_t * value_t |
||

237 | | Power of value_t * value_t |
||

238 | |||

239 | type instr_t = |
||

240 | | MLocalAssign of var_decl * value_t |
||

241 | | MStateAssign of var_decl * value_t |
||

242 | | MReset of ident |
||

243 | ca88e660 | Ploc | | MNoReset of ident (* used to symmetrize the reset function *) |

244 | 53206908 | xthirioux | | MStep of var_decl list * ident * value_t list |

245 | | MBranch of value_t * (label * instr_t list) list |
||

246 | | MComment of string |
||

247 | |||

248 | |||

249 | 0038002e | ploc | type error = |

250 | Main_not_found |
||

251 | | Main_wrong_kind |
||

252 | | No_main_specified |
||

253 | | Unbound_symbol of ident |
||

254 | | Already_bound_symbol of ident |
||

255 | 70e1006b | xthirioux | | Unknown_library of ident |

256 | 01d48bb0 | xthirioux | | Wrong_number of ident |

257 | 0cbf0839 | ploc | |

258 | (* Local Variables: *) |
||

259 | (* compile-command:"make -C .." *) |
||

260 | (* End: *) |