## lustrec / src / lustre_types.ml @ 32614c2d

History | View | Annotate | Download (6.35 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 | 66359a5e | ploc | |

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 | 04396cc7 | Christophe Garion | | 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 | 04396cc7 | Christophe Garion | type var_decl = |

60 | 22fe1c93 | ploc | {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 | 66359a5e | ploc | mutable var_parent_nodeid: ident option; |

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

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

69 | var_loc: Location.t} |
||

70 | |||

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

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

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

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

75 | |||

76 | |||

77 | |||

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

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

80 | ec433d69 | xthirioux | and expr = |

81 | 01c7d5e1 | 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 | ef34b4ae | xthirioux | |

104 | 04396cc7 | Christophe Garion | and call_t = ident * expr * expr option |

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

106 | ef34b4ae | xthirioux | |

107 | and eq = |
||

108 | {eq_lhs: ident list; |
||

109 | eq_rhs: expr; |
||

110 | eq_loc: Location.t} |
||

111 | |||

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

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

114 | ef34b4ae | xthirioux | and eexpr = |

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

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

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

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

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

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

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

122 | |||

123 | ef34b4ae | xthirioux | and expr_annot = |

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

125 | annot_loc: Location.t} |
||

126 | 22fe1c93 | ploc | |

127 | type node_annot = { |
||

128 | requires: eexpr list; |
||

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

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

131 | spec_loc: Location.t; |
||

132 | 22fe1c93 | ploc | } |

133 | 2d179f5b | xthirioux | |

134 | type offset = |
||

135 | | Index of Dimension.dim_expr |
||

136 | | Field of label |
||

137 | |||

138 | 04396cc7 | Christophe Garion | type assert_t = |

139 | 01c7d5e1 | ploc | { |

140 | assert_expr: expr; |
||

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

142 | b08ffca7 | xthirioux | } |

143 | |||

144 | type statement = |
||

145 | | Eq of eq |
||

146 | | Aut of automata_desc |
||

147 | 01c7d5e1 | ploc | |

148 | b08ffca7 | xthirioux | and automata_desc = |

149 | ef34b4ae | 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 | 2822cf55 | xthirioux | hand_unless: (Location.t * expr * bool * ident) list; |

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

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

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

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

160 | hand_annots: expr_annot list; |
||

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

162 | |||

163 | 01c7d5e1 | 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 | 04396cc7 | Christophe Garion | node_asserts: assert_t list; |

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

174 | 01c7d5e1 | 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 | 66359a5e | ploc | (* nodei_annot: expr_annot list; *) |

189 | 01c7d5e1 | ploc | nodei_prototype: string option; |

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

191 | 01c7d5e1 | ploc | } |

192 | |||

193 | 04396cc7 | Christophe Garion | type const_desc = |

194 | {const_id: ident; |
||

195 | const_loc: Location.t; |
||

196 | const_value: constant; |
||

197 | 01c7d5e1 | ploc | mutable const_type: Types.type_expr; |

198 | } |
||

199 | |||

200 | type top_decl_desc = |
||

201 | | Node of node_desc |
||

202 | ef34b4ae | xthirioux | | Const of const_desc |

203 | 01c7d5e1 | ploc | | ImportedNode of imported_node_desc |

204 | 04396cc7 | Christophe Garion | | Open of bool * string (* the boolean set to true denotes a local |

205 | 01c7d5e1 | ploc | lusi vs a lusi installed at system level *) |

206 | ef34b4ae | xthirioux | | TypeDef of typedef_desc |

207 | 01c7d5e1 | ploc | |

208 | type top_decl = |
||

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

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

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

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

213 | 01c7d5e1 | ploc | |

214 | type program = top_decl list |
||

215 | |||

216 | 04396cc7 | Christophe Garion | type dep_t = Dep of |

217 | bool |
||

218 | 58a463e7 | ploc | * ident |

219 | 04396cc7 | Christophe Garion | * (top_decl list) |

220 | 58a463e7 | ploc | * bool (* is stateful *) |

221 | |||

222 | 04a63d25 | xthirioux | |

223 | |||

224 | |||

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

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

227 | (* End: *) |