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_bool of bool

51

 Const_int of int

52

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

53

 Const_array of constant list

54

 Const_tag of label

55

 Const_string of string (* used only for annotations *)

56

 Const_struct of (label * constant) list

57


58

type quantifier_type = Exists  Forall

59


60

type var_decl =

61

{var_id: ident;

62

var_orig:bool;

63

var_dec_type: type_dec;

64

var_dec_clock: clock_dec;

65

var_dec_const: bool;

66

var_dec_value: expr option;

67

mutable var_type: Types.type_expr;

68

mutable var_clock: Clocks.clock_expr;

69

var_loc: Location.t}

70


71

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

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

{

241

instr_desc: instr_t_desc; (* main data: the content *)

242

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

243

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

244

}

245

and instr_t_desc =

246

 MLocalAssign of var_decl * value_t

247

 MStateAssign of var_decl * value_t

248

 MReset of ident

249

 MNoReset of ident

250

 MStep of var_decl list * ident * value_t list

251

 MBranch of value_t * (label * instr_t list) list

252

 MComment of string

253


254


255

(* Local Variables: *)

256

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

257

(* End: *)
