1

(* 

2

* SchedMCore  A MultiCore Scheduling Framework

3

* Copyright (C) 20092011, ONERA, Toulouse, FRANCE  LIFL, Lille, FRANCE

4

*

5

* This file is part of Prelude

6

*

7

* Prelude is free software; you can redistribute it and/or

8

* modify it under the terms of the GNU Lesser General Public License

9

* as published by the Free Software Foundation ; either version 2 of

10

* the License, or (at your option) any later version.

11

*

12

* Prelude is distributed in the hope that it will be useful, but

13

* WITHOUT ANY WARRANTY ; without even the implied warranty of

14

* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU

15

* Lesser General Public License for more details.

16

*

17

* You should have received a copy of the GNU Lesser General Public

18

* License along with this program ; if not, write to the Free Software

19

* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307

20

* USA

21

* *)

22


23

open LustreSpec

24

(*

25

(** The core language and its ast. *)

26

type ident = Utils.ident

27

type label = Utils.ident

28

type rat = Utils.rat

29

type tag = Utils.tag

30


31

type constant =

32

 Const_int of int

33

 Const_real of string

34

 Const_float of float

35

 Const_array of constant list

36

 Const_tag of label

37

 Const_struct of (label * constant) list

38


39

val dummy_type_dec: type_dec

40


41

type type_dec = LustreSpec.type_dec

42


43

type clock_dec = LustreSpec.clock_dec

44

val dummy_clock_dec: clock_dec

45


46

type var_decl = LustreSpec.var_decl

47


48

type expr =

49

{expr_tag: tag; (* Unique identifier *)

50

expr_desc: expr_desc;

51

mutable expr_type: Types.type_expr;

52

mutable expr_clock: Clocks.clock_expr;

53

mutable expr_delay: Delay.delay_expr; (* Used for the initialisation check *)

54

mutable expr_annot: LustreSpec.expr_annot option; (* Spec *)

55

expr_loc: Location.t}

56


57

and expr_desc =

58

 Expr_const of constant

59

 Expr_ident of ident

60

 Expr_tuple of expr list

61

 Expr_ite of expr * expr * expr

62

 Expr_arrow of expr * expr

63

 Expr_fby of expr * expr

64

(*

65

 Expr_struct of (label * expr) list

66

 Expr_field of expr * label

67

 Expr_update of expr * (label * expr)

68

*)

69

 Expr_array of expr list

70

 Expr_access of expr * Dimension.dim_expr (* acces(e,i) is the ith element

71

of array epxression e *)

72

 Expr_power of expr * Dimension.dim_expr (* power(e,n) is the array of

73

size n filled with expression e *)

74

 Expr_pre of expr

75

 Expr_when of expr * ident * label

76

 Expr_merge of ident * (label * expr) list

77

 Expr_appl of call_t

78

 Expr_uclock of expr * int

79

 Expr_dclock of expr * int

80

 Expr_phclock of expr * rat

81

and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)

82


83

type eq =

84

{eq_lhs: ident list;

85

eq_rhs: expr;

86

eq_loc: Location.t}

87


88

type assert_t =

89

{

90

assert_expr: expr * eq list;

91

assert_loc: Location.t

92

}

93


94

type node_desc =

95

{node_id: ident;

96

mutable node_type: Types.type_expr;

97

mutable node_clock: Clocks.clock_expr;

98

node_inputs: var_decl list;

99

node_outputs: var_decl list;

100

node_locals: var_decl list;

101

mutable node_gencalls: expr list;

102

mutable node_checks: Dimension.dim_expr list;

103

node_asserts: assert_t list;

104

node_eqs: eq list;

105

mutable node_dec_stateless: bool;

106

mutable node_stateless: bool option;

107

node_spec: LustreSpec.node_annot option;

108

node_annot: LustreSpec.expr_annot option;}

109


110

type imported_node_desc =

111

{nodei_id: ident;

112

mutable nodei_type: Types.type_expr;

113

mutable nodei_clock: Clocks.clock_expr;

114

nodei_inputs: var_decl list;

115

nodei_outputs: var_decl list;

116

nodei_stateless: bool;

117

nodei_spec: LustreSpec.node_annot option;

118

nodei_prototype: string option;

119

nodei_in_lib: string option;

120

}

121

(*

122

type imported_fun_desc =

123

{fun_id: ident;

124

mutable fun_type: Types.type_expr;

125

fun_inputs: var_decl list;

126

fun_outputs: var_decl list;

127

fun_spec: LustreSpec.node_annot option;}

128

*)

129

type const_desc =

130

{const_id: ident;

131

const_loc: Location.t;

132

const_value: constant;

133

mutable const_type: Types.type_expr;

134

}

135

(* type sensor_desc = *)

136

(* {sensor_id: ident; *)

137

(* sensor_wcet: int} *)

138


139

(* type actuator_desc = *)

140

(* {actuator_id: ident; *)

141

(* actuator_wcet: int} *)

142


143

type top_decl_desc =

144

 Node of node_desc

145

 Consts of const_desc list

146

 ImportedNode of imported_node_desc

147

(*  ImportedFun of imported_fun_desc *)

148

(*  SensorDecl of sensor_desc *)

149

(*  ActuatorDecl of actuator_desc *)

150

 Open of bool * string

151


152

type top_decl =

153

{top_decl_desc: top_decl_desc;

154

top_decl_loc: Location.t}

155


156

type program = top_decl list

157


158

type error =

159

Main_not_found

160

 Main_wrong_kind

161

 No_main_specified

162

 Unbound_symbol of ident

163

 Already_bound_symbol of ident

164

*)

165

exception Error of Location.t * error

166


167

val dummy_type_dec: type_dec

168

val dummy_clock_dec: clock_dec

169


170

val mktyp: Location.t > type_dec_desc > type_dec

171

val mkclock: Location.t > clock_dec_desc > clock_dec

172

val mkvar_decl: Location.t > ident * type_dec * clock_dec * bool (* is const *) > var_decl

173

val var_decl_of_const: const_desc > var_decl

174

val mkexpr: Location.t > expr_desc > expr

175

val mkeq: Location.t > ident list * expr > eq

176

val mkassert: Location.t > expr > assert_t

177

val mktop_decl: Location.t > top_decl_desc > top_decl

178

val mkpredef_call: Location.t > ident > expr list > expr

179

val mk_new_name: var_decl list > ident > ident

180


181


182

val node_table : (ident, top_decl) Hashtbl.t

183

val node_name: top_decl > ident

184

val node_inputs: top_decl > var_decl list

185

val node_from_name: ident > top_decl

186

val is_generic_node: top_decl > bool

187

val is_imported_node: top_decl > bool

188


189

val consts_table: (ident, const_desc) Hashtbl.t

190

val type_table: (type_dec_desc, type_dec_desc) Hashtbl.t

191

val get_repr_type: type_dec_desc > type_dec_desc

192

val is_user_type: type_dec_desc > bool

193

val tag_true: label

194

val tag_false: label

195

val tag_table: (label, type_dec_desc) Hashtbl.t

196

val field_table: (label, type_dec_desc) Hashtbl.t

197


198

val get_enum_type_tags: type_dec_desc > label list

199


200

val get_struct_type_fields: type_dec_desc > (label * type_dec_desc) list

201


202

val const_of_bool: bool > constant

203

val const_is_bool: constant > bool

204

val const_negation: constant > constant

205

val const_or: constant > constant > constant

206

val const_and: constant > constant > constant

207

val const_xor: constant > constant > constant

208

val const_impl: constant > constant > constant

209


210

val get_node_vars: node_desc > var_decl list

211

val get_node_var: ident > node_desc > var_decl

212

val get_node_eq: ident > node_desc > eq

213


214

(* val get_const: ident > constant *)

215


216

val sort_handlers : (label * 'a) list > (label * 'a) list

217


218

val is_eq_expr: expr > expr > bool

219


220

val pp_error : Format.formatter > error > unit

221


222

(* Caution, returns an untyped, unclocked, etc, expression *)

223

val is_tuple_expr : expr > bool

224

val ident_of_expr : expr > ident

225

val expr_of_ident : ident > Location.t > expr

226

val expr_list_of_expr : expr > expr list

227

val expr_of_expr_list : Location.t > expr list > expr

228

val call_of_expr: expr > (ident * expr list * (ident * label) option)

229

val expr_of_dimension: Dimension.dim_expr > expr

230

val dimension_of_expr: expr > Dimension.dim_expr

231

val dimension_of_const: Location.t > constant > Dimension.dim_expr

232


233

(* REMOVED, pushed in utils.ml val new_tag : unit > tag *)

234


235

val add_internal_funs: unit > unit

236


237

val pp_prog_type : Format.formatter > program > unit

238


239

val pp_prog_clock : Format.formatter > program > unit

240


241

val get_nodes : program > node_desc list

242

val get_consts : program > const_desc list

243

(* val prog_unfold_consts: program > program *)

244


245

val expr_replace_var: (ident > ident) > expr > expr

246

val eq_replace_rhs_var: (ident > bool) > (ident > ident) > eq > eq

247


248

(** rename_prog f_node f_var f_const prog *)

249

val rename_prog: (ident > ident) > (ident > ident) > (ident > ident) > program > program

250


251

val update_expr_annot: expr > LustreSpec.expr_annot > expr

252


253

val substitute_expr: var_decl list > eq list > expr > expr

254


255

(** Annotation expression related functions *)

256

val mkeexpr: Location.t > expr > eexpr

257

val merge_node_annot: node_annot > node_annot > node_annot

258

val extend_eexpr: (quantifier_type * var_decl list) list > eexpr > eexpr

259

val update_expr_annot: expr > expr_annot > expr

260

(* val mkpredef_call: Location.t > ident > eexpr list > eexpr*)

261


262

(* Local Variables: *)

263

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

264

(* End: *)
