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 assert_t =

84

{

85

assert_expr: expr;

86

assert_loc: Location.t

87

}

88


89

type eq =

90

{eq_lhs: ident list;

91

eq_rhs: expr;

92

eq_loc: Location.t}

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 mktyp: Location.t > type_dec_desc > type_dec

168

val mkclock: Location.t > clock_dec_desc > clock_dec

169

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

170

val var_decl_of_const: const_desc > var_decl

171

val mkexpr: Location.t > expr_desc > expr

172

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

173

val mkassert: Location.t > expr > assert_t

174

val mktop_decl: Location.t > top_decl_desc > top_decl

175

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

176

val mk_new_name: var_decl list > ident > ident

177


178


179

val node_table : (ident, top_decl) Hashtbl.t

180

val node_name: top_decl > ident

181

val node_inputs: top_decl > var_decl list

182

val node_from_name: ident > top_decl

183

val is_generic_node: top_decl > bool

184

val is_imported_node: top_decl > bool

185


186

val consts_table: (ident, const_desc) Hashtbl.t

187

val type_table: (type_dec_desc, type_dec_desc) Hashtbl.t

188

val get_repr_type: type_dec_desc > type_dec_desc

189

val is_user_type: type_dec_desc > bool

190

val tag_true: label

191

val tag_false: label

192

val tag_table: (label, type_dec_desc) Hashtbl.t

193

val field_table: (label, type_dec_desc) Hashtbl.t

194


195

val get_enum_type_tags: type_dec_desc > label list

196


197

val get_struct_type_fields: type_dec_desc > (label * type_dec_desc) list

198


199

val const_of_bool: bool > constant

200

val const_is_bool: constant > bool

201

val const_negation: constant > constant

202

val const_or: constant > constant > constant

203

val const_and: constant > constant > constant

204

val const_xor: constant > constant > constant

205

val const_impl: constant > constant > constant

206


207

val node_vars: node_desc > var_decl list

208

val node_var: ident > node_desc > var_decl

209

val node_eq: ident > node_desc > eq

210


211

(* val get_const: ident > constant *)

212


213

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

214


215

val is_eq_expr: expr > expr > bool

216


217

val pp_error : Format.formatter > error > unit

218


219

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

220

val is_tuple_expr : expr > bool

221

val expr_of_ident : ident > Location.t > expr

222

val expr_list_of_expr : expr > expr list

223

val expr_of_expr_list : Location.t > expr list > expr

224

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

225

val expr_of_dimension: Dimension.dim_expr > expr

226

val dimension_of_expr: expr > Dimension.dim_expr

227

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

228


229

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

230


231

val add_internal_funs: unit > unit

232


233

val pp_prog_type : Format.formatter > program > unit

234


235

val pp_prog_clock : Format.formatter > program > unit

236


237

val get_nodes : program > node_desc list

238

val get_consts : program > const_desc list

239

val prog_unfold_consts: program > program

240

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

241

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

242


243

(** rename_prog f_node f_var f_const prog *)

244

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

245


246

val update_expr_annot: expr > LustreSpec.expr_annot > expr

247


248


249

(* Local Variables: *)

250

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

251

(* End: *)
