## lustrec / src / lustreSpec.ml @ 68601cf5

History | View | Annotate | Download (7.16 KB)

1 | a2d97a3e | 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 | 22fe1c93 | ploc | type ident = Utils.ident |

13 | type rat = Utils.rat |
||

14 | type tag = Utils.tag |
||

15 | af5af1e8 | ploc | type label = Utils.ident |

16 | 22fe1c93 | ploc | |

17 | type type_dec = |
||

18 | {ty_dec_desc: type_dec_desc; |
||

19 | ty_dec_loc: Location.t} |
||

20 | |||

21 | and type_dec_desc = |
||

22 | | Tydec_any |
||

23 | | Tydec_int |
||

24 | | Tydec_real |
||

25 | 04a63d25 | xthirioux | (* | Tydec_float *) |

26 | 22fe1c93 | ploc | | Tydec_bool |

27 | | Tydec_clock of type_dec_desc |
||

28 | | Tydec_const of ident |
||

29 | | Tydec_enum of ident list |
||

30 | 6a6abd76 | xthirioux | | Tydec_struct of (ident * type_dec_desc) list |

31 | 22fe1c93 | ploc | | Tydec_array of Dimension.dim_expr * type_dec_desc |

32 | |||

33 | ef34b4ae | xthirioux | type typedec_desc = |

34 | {tydec_id: ident} |
||

35 | |||

36 | type typedef_desc = |
||

37 | {tydef_id: ident; |
||

38 | tydef_desc: type_dec_desc} |
||

39 | b1655a21 | xthirioux | |

40 | 22fe1c93 | ploc | type clock_dec = |

41 | {ck_dec_desc: clock_dec_desc; |
||

42 | ck_dec_loc: Location.t} |
||

43 | |||

44 | and clock_dec_desc = |
||

45 | | Ckdec_any |
||

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

47 | 45f0f48d | xthirioux | |

48 | 22fe1c93 | ploc | |

49 | ec433d69 | xthirioux | type constant = |

50 | | Const_int of int |
||

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

52 | ec433d69 | xthirioux | | Const_array of constant list |

53 | | Const_tag of label |
||

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

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

56 | |||

57 | type quantifier_type = Exists | Forall |
||

58 | |||

59 | 22fe1c93 | ploc | type var_decl = |

60 | {var_id: ident; |
||

61 | 54d032f5 | xthirioux | var_orig:bool; |

62 | 22fe1c93 | ploc | var_dec_type: type_dec; |

63 | var_dec_clock: clock_dec; |
||

64 | var_dec_const: bool; |
||

65 | ec433d69 | xthirioux | var_dec_value: expr option; |

66 | 22fe1c93 | ploc | mutable var_type: Types.type_expr; |

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

68 | var_loc: Location.t} |
||

69 | |||

70 | 01c7d5e1 | ploc | (** The core language and its ast. Every element of the ast contains its |

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

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

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

74 | |||

75 | |||

76 | |||

77 | 22fe1c93 | ploc | (* The tag of an expression is a unique identifier used to distinguish |

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

79 | ec433d69 | xthirioux | and expr = |

80 | 01c7d5e1 | ploc | {expr_tag: tag; |

81 | expr_desc: expr_desc; |
||

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

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

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

85 | mutable expr_annot: expr_annot option; |
||

86 | expr_loc: Location.t} |
||

87 | |||

88 | and expr_desc = |
||

89 | | Expr_const of constant |
||

90 | | Expr_ident of ident |
||

91 | | Expr_tuple of expr list |
||

92 | | Expr_ite of expr * expr * expr |
||

93 | | Expr_arrow of expr * expr |
||

94 | | Expr_fby of expr * expr |
||

95 | | Expr_array of expr list |
||

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

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

98 | | Expr_pre of expr |
||

99 | | Expr_when of expr * ident * label |
||

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

101 | | Expr_appl of call_t |
||

102 | ef34b4ae | xthirioux | |

103 | 54d032f5 | xthirioux | and call_t = ident * expr * expr option |

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

105 | ef34b4ae | xthirioux | |

106 | and eq = |
||

107 | {eq_lhs: ident list; |
||

108 | eq_rhs: expr; |
||

109 | eq_loc: Location.t} |
||

110 | |||

111 | 01c7d5e1 | ploc | (* The tag of an expression is a unique identifier used to distinguish |

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

113 | ef34b4ae | xthirioux | and eexpr = |

114 | 22fe1c93 | ploc | {eexpr_tag: tag; |

115 | 01c7d5e1 | ploc | eexpr_qfexpr: expr; |

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

117 | 22fe1c93 | ploc | mutable eexpr_type: Types.type_expr; |

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

119 | 01c7d5e1 | ploc | mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; |

120 | 22fe1c93 | ploc | eexpr_loc: Location.t} |

121 | |||

122 | ef34b4ae | xthirioux | and expr_annot = |

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

124 | annot_loc: Location.t} |
||

125 | 22fe1c93 | ploc | |

126 | type node_annot = { |
||

127 | requires: eexpr list; |
||

128 | 01c7d5e1 | ploc | ensures: eexpr list; |

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

130 | spec_loc: Location.t; |
||

131 | 22fe1c93 | ploc | } |

132 | 2d179f5b | xthirioux | |

133 | type offset = |
||

134 | | Index of Dimension.dim_expr |
||

135 | | Field of label |
||

136 | |||

137 | 01c7d5e1 | ploc | type assert_t = |

138 | { |
||

139 | assert_expr: expr; |
||

140 | af5af1e8 | ploc | assert_loc: Location.t; |

141 | b08ffca7 | xthirioux | } |

142 | |||

143 | type statement = |
||

144 | | Eq of eq |
||

145 | | Aut of automata_desc |
||

146 | 01c7d5e1 | ploc | |

147 | b08ffca7 | xthirioux | and automata_desc = |

148 | ef34b4ae | xthirioux | {aut_id : ident; |

149 | aut_handlers: handler_desc list; |
||

150 | aut_loc: Location.t} |
||

151 | |||

152 | and handler_desc = |
||

153 | {hand_state: ident; |
||

154 | 2822cf55 | xthirioux | hand_unless: (Location.t * expr * bool * ident) list; |

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

156 | ef34b4ae | xthirioux | hand_locals: var_decl list; |

157 | b08ffca7 | xthirioux | hand_stmts: statement list; |

158 | 2822cf55 | xthirioux | hand_asserts: assert_t list; |

159 | hand_annots: expr_annot list; |
||

160 | ef34b4ae | xthirioux | hand_loc: Location.t} |

161 | |||

162 | 01c7d5e1 | ploc | type node_desc = |

163 | {node_id: ident; |
||

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

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

166 | node_inputs: var_decl list; |
||

167 | node_outputs: var_decl list; |
||

168 | node_locals: var_decl list; |
||

169 | mutable node_gencalls: expr list; |
||

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

171 | node_asserts: assert_t list; |
||

172 | b08ffca7 | xthirioux | node_stmts: statement list; |

173 | 01c7d5e1 | ploc | mutable node_dec_stateless: bool; |

174 | mutable node_stateless: bool option; |
||

175 | node_spec: node_annot option; |
||

176 | node_annot: expr_annot list; |
||

177 | } |
||

178 | |||

179 | type imported_node_desc = |
||

180 | {nodei_id: ident; |
||

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

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

183 | nodei_inputs: var_decl list; |
||

184 | nodei_outputs: var_decl list; |
||

185 | nodei_stateless: bool; |
||

186 | nodei_spec: node_annot option; |
||

187 | nodei_prototype: string option; |
||

188 | 04a63d25 | xthirioux | nodei_in_lib: string list; |

189 | 01c7d5e1 | ploc | } |

190 | |||

191 | type const_desc = |
||

192 | {const_id: ident; |
||

193 | const_loc: Location.t; |
||

194 | const_value: constant; |
||

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

196 | } |
||

197 | |||

198 | type top_decl_desc = |
||

199 | | Node of node_desc |
||

200 | ef34b4ae | xthirioux | | Const of const_desc |

201 | 01c7d5e1 | ploc | | ImportedNode of imported_node_desc |

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

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

204 | ef34b4ae | xthirioux | | TypeDef of typedef_desc |

205 | 01c7d5e1 | ploc | |

206 | type top_decl = |
||

207 | ef34b4ae | xthirioux | {top_decl_desc: top_decl_desc; (* description of the symbol *) |

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

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

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

211 | 01c7d5e1 | ploc | |

212 | type program = top_decl list |
||

213 | |||

214 | 58a463e7 | ploc | type dep_t = Dep of |

215 | bool |
||

216 | * ident |
||

217 | * (top_decl list) |
||

218 | * bool (* is stateful *) |
||

219 | |||

220 | 04a63d25 | xthirioux | |

221 | (************ Machine code types *************) |
||

222 | |||

223 | type value_t = |
||

224 | { |
||

225 | value_desc: value_t_desc; |
||

226 | value_type: Types.type_expr; |
||

227 | value_annot: expr_annot option |
||

228 | } |
||

229 | and value_t_desc = |
||

230 | | Cst of constant |
||

231 | | LocalVar of var_decl |
||

232 | | StateVar of var_decl |
||

233 | | Fun of ident * value_t list |
||

234 | | Array of value_t list |
||

235 | | Access of value_t * value_t |
||

236 | | Power of value_t * value_t |
||

237 | |||

238 | type instr_t = |
||

239 | 3ca27bc7 | ploc | { |

240 | 1bff14ac | ploc | instr_desc: instr_t_desc; (* main data: the content *) |

241 | (* lustre_expr: expr option; (* possible representation as a lustre expression *) *) |
||

242 | lustre_eq: eq option; (* possible representation as a lustre flow equation *) |
||

243 | 3ca27bc7 | ploc | } |

244 | and instr_t_desc = |
||

245 | 04a63d25 | xthirioux | | MLocalAssign of var_decl * value_t |

246 | | MStateAssign of var_decl * value_t |
||

247 | | MReset of ident |
||

248 | 45f0f48d | xthirioux | | MNoReset of ident |

249 | 04a63d25 | xthirioux | | MStep of var_decl list * ident * value_t list |

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

251 | | MComment of string |
||

252 | |||

253 | |||

254 | 22fe1c93 | ploc | (* Local Variables: *) |

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

256 | (* End: *) |