## lustrec / src / lustreSpec.ml @ ca88e660

History | View | Annotate | Download (7.21 KB)

1 |
(********************************************************************) |
---|---|

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 |
open Format |

13 | |

14 |
type ident = Utils.ident |

15 |
type rat = Utils.rat |

16 |
type tag = Utils.tag |

17 |
type label = Utils.ident |

18 | |

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 |
(* | Tydec_float *) |

28 |
| Tydec_bool |

29 |
| Tydec_clock of type_dec_desc |

30 |
| Tydec_const of ident |

31 |
| Tydec_enum of ident list |

32 |
| Tydec_struct of (ident * type_dec_desc) list |

33 |
| Tydec_array of Dimension.dim_expr * type_dec_desc |

34 | |

35 |
type typedec_desc = |

36 |
{tydec_id: ident} |

37 | |

38 |
type typedef_desc = |

39 |
{tydef_id: ident; |

40 |
tydef_desc: type_dec_desc} |

41 | |

42 |
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 |
type constant = |

52 |
| Const_int of int |

53 |
| 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 |
| 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 |
type var_decl = |

63 |
{var_id: ident; |

64 |
var_orig:bool; |

65 |
var_dec_type: type_dec; |

66 |
var_dec_clock: clock_dec; |

67 |
var_dec_const: bool; |

68 |
var_dec_value: expr option; |

69 |
mutable var_type: Types.type_expr; |

70 |
mutable var_clock: Clocks.clock_expr; |

71 |
var_loc: Location.t} |

72 | |

73 |
(** 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 |
(* The tag of an expression is a unique identifier used to distinguish |

79 |
different instances of the same node *) |

80 |
and expr = |

81 |
{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 | |

104 |
and call_t = ident * expr * expr option |

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

106 | |

107 |
and eq = |

108 |
{eq_lhs: ident list; |

109 |
eq_rhs: expr; |

110 |
eq_loc: Location.t} |

111 | |

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

113 |
different instances of the same node *) |

114 |
and eexpr = |

115 |
{eexpr_tag: tag; |

116 |
eexpr_qfexpr: expr; |

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

118 |
mutable eexpr_type: Types.type_expr; |

119 |
mutable eexpr_clock: Clocks.clock_expr; |

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

121 |
eexpr_loc: Location.t} |

122 | |

123 |
and expr_annot = |

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

125 |
annot_loc: Location.t} |

126 | |

127 |
type node_annot = { |

128 |
requires: eexpr list; |

129 |
ensures: eexpr list; |

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

131 |
spec_loc: Location.t; |

132 |
} |

133 | |

134 |
type offset = |

135 |
| Index of Dimension.dim_expr |

136 |
| Field of label |

137 | |

138 |
type assert_t = |

139 |
{ |

140 |
assert_expr: expr; |

141 |
assert_loc: Location.t; |

142 |
} |

143 | |

144 |
type statement = |

145 |
| Eq of eq |

146 |
| Aut of automata_desc |

147 | |

148 |
and automata_desc = |

149 |
{aut_id : ident; |

150 |
aut_handlers: handler_desc list; |

151 |
aut_loc: Location.t} |

152 | |

153 |
and handler_desc = |

154 |
{hand_state: ident; |

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

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

157 |
hand_locals: var_decl list; |

158 |
hand_stmts: statement list; |

159 |
hand_asserts: assert_t list; |

160 |
hand_annots: expr_annot list; |

161 |
hand_loc: Location.t} |

162 | |

163 |
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 |
node_stmts: statement list; |

174 |
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 |
nodei_in_lib: string list; |

190 |
} |

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 |
| Const of const_desc |

202 |
| 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 |
| TypeDef of typedef_desc |

206 | |

207 |
type top_decl = |

208 |
{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 | |

213 |
type program = top_decl list |

214 | |

215 |
type dep_t = Dep of |

216 |
bool |

217 |
* ident |

218 |
* (top_decl list) |

219 |
* bool (* is stateful *) |

220 | |

221 | |

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 |
| MNoReset of ident (* used to symmetrize the reset function *) |

244 |
| 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 |
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 |
| Unknown_library of ident |

256 |
| Wrong_number of ident |

257 | |

258 |
(* Local Variables: *) |

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

260 |
(* End: *) |