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

type ident = Utils.ident

13

type rat = Utils.rat

14

type tag = Utils.tag

15

type label = Utils.ident

16


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

(*  Tydec_float *)

26

 Tydec_bool

27

 Tydec_clock of type_dec_desc

28

 Tydec_const of ident

29

 Tydec_enum of ident list

30

 Tydec_struct of (ident * type_dec_desc) list

31

 Tydec_array of Dimension.dim_expr * type_dec_desc

32


33

type typedec_desc =

34

{tydec_id: ident}

35


36

type typedef_desc =

37

{tydef_id: ident;

38

tydef_desc: type_dec_desc}

39


40

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


48


49

type constant =

50

 Const_int of int

51

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

52

 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

type var_decl =

60

{var_id: ident;

61

var_orig:bool;

62

var_dec_type: type_dec;

63

var_dec_clock: clock_dec;

64

var_dec_const: bool;

65

var_dec_value: expr option;

66

mutable var_type: Types.type_expr;

67

mutable var_clock: Clocks.clock_expr;

68

var_loc: Location.t}

69


70

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

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

78

different instances of the same node *)

79

and expr =

80

{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


103

and call_t = ident * expr * expr option

104

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

105


106

and eq =

107

{eq_lhs: ident list;

108

eq_rhs: expr;

109

eq_loc: Location.t}

110


111

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

112

different instances of the same node *)

113

and eexpr =

114

{eexpr_tag: tag;

115

eexpr_qfexpr: expr;

116

eexpr_quantifiers: (quantifier_type * var_decl list) list;

117

mutable eexpr_type: Types.type_expr;

118

mutable eexpr_clock: Clocks.clock_expr;

119

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

120

eexpr_loc: Location.t}

121


122

and expr_annot =

123

{annots: (string list * eexpr) list;

124

annot_loc: Location.t}

125


126

type node_annot = {

127

requires: eexpr list;

128

ensures: eexpr list;

129

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

130

spec_loc: Location.t;

131

}

132


133

type offset =

134

 Index of Dimension.dim_expr

135

 Field of label

136


137

type assert_t =

138

{

139

assert_expr: expr;

140

assert_loc: Location.t;

141

}

142


143

type statement =

144

 Eq of eq

145

 Aut of automata_desc

146


147

and automata_desc =

148

{aut_id : ident;

149

aut_handlers: handler_desc list;

150

aut_loc: Location.t}

151


152

and handler_desc =

153

{hand_state: ident;

154

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

155

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

156

hand_locals: var_decl list;

157

hand_stmts: statement list;

158

hand_asserts: assert_t list;

159

hand_annots: expr_annot list;

160

hand_loc: Location.t}

161


162

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

node_stmts: statement list;

173

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

nodei_in_lib: string list;

189

}

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

 Const of const_desc

201

 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

 TypeDef of typedef_desc

205


206

type top_decl =

207

{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


212

type program = top_decl list

213


214

type dep_t = Dep of

215

bool

216

* ident

217

* (top_decl list)

218

* bool (* is stateful *)

219


220


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

{

240

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

}

244

and instr_t_desc =

245

 MLocalAssign of var_decl * value_t

246

 MStateAssign of var_decl * value_t

247

 MReset of ident

248

 MNoReset of ident

249

 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

(* Local Variables: *)

255

(* compilecommand:"make C .." *)

256

(* End: *)
