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

open Clocks

13

open Corelang

14


15

(* Applies variable substitutions *)

16

let subst_var var_substs vid =

17

try Hashtbl.find var_substs vid with Not_found > vid

18


19

(* Applies clock substitutions *)

20

let rec subst_ck ck_substs var_substs ck =

21

match ck.cdesc with

22

 Carrow (ck1, ck2) >

23

{

24

ck with

25

cdesc =

26

Carrow

27

(subst_ck ck_substs var_substs ck1, subst_ck ck_substs var_substs ck2);

28

}

29

 Ctuple cklist >

30

{ ck with cdesc = Ctuple (List.map (subst_ck ck_substs var_substs) cklist) }

31

 Con (ck', c) >

32

{ ck with cdesc = Con (subst_ck ck_substs var_substs ck', c) }

33

 Connot (ck', c) >

34

{ ck with cdesc = Connot (subst_ck ck_substs var_substs ck', c) }

35

 Pck_up (ck', k) >

36

{ ck with cdesc = Pck_up (subst_ck ck_substs var_substs ck', k) }

37

 Pck_down (ck', k) >

38

{ ck with cdesc = Pck_down (subst_ck ck_substs var_substs ck', k) }

39

 Pck_phase (ck', q) >

40

{ ck with cdesc = Pck_phase (subst_ck ck_substs var_substs ck', q) }

41

 Pck_const _ >

42

ck

43

 Cvar _  Cunivar _ > (

44

try Hashtbl.find ck_substs ck with Not_found > ck)

45

 Clink ck' >

46

subst_ck ck_substs var_substs ck'

47

 Ccarrying (_, ck') >

48

subst_ck ck_substs var_substs ck'

49


50

(* [new_expr_instance ck_substs var_substs e edesc] returns a new "instance" of

51

expressions [e] of expression [e], where [edesc] is the expanded version of

52

[e]. *)

53

let new_expr_instance ck_substs var_substs e edesc =

54

{

55

expr_tag = Utils.new_tag ();

56

expr_desc = edesc;

57

expr_type = e.expr_type;

58

expr_clock = subst_ck ck_substs var_substs e.expr_clock;

59

expr_delay = Delay.new_var ();

60

expr_loc = e.expr_loc;

61

expr_annot = e.expr_annot;

62

}

63


64

let locals_cpt = ref 0

65


66

(* Returns a new local variable (for the main node) *)

67

let new_local vtyp vck vdd vloc =

68

let vid = "_" ^ string_of_int !locals_cpt in

69

locals_cpt := !locals_cpt + 1;

70

let ty_dec = { ty_dec_desc = Tydec_any; ty_dec_loc = vloc } in

71

(* dummy *)

72

let ck_dec = { ck_dec_desc = Ckdec_any; ck_dec_loc = vloc } in

73

(* dummy *)

74

{

75

var_id = vid;

76

var_orig = false;

77

var_dec_type = ty_dec;

78

var_dec_clock = ck_dec;

79

var_dec_deadline = vdd;

80

var_type = vtyp;

81

var_clock = vck;

82

var_loc = vloc;

83

}

84


85

(* Returns an expression correponding to variable v *)

86

let expr_of_var v =

87

{

88

expr_tag = Utils.new_tag ();

89

expr_desc = Expr_ident v.var_id;

90

expr_type = v.var_type;

91

expr_clock = v.var_clock;

92

expr_delay = Delay.new_var ();

93

expr_loc = v.var_loc;

94

expr_annot = None;

95

}

96


97

(* [build_ck_substs ck for_ck] computes the variable substitutions corresponding

98

to the substitution of [ck] for [for_ck] *)

99

let build_ck_substs ck for_ck =

100

let substs = Hashtbl.create 10 in

101

let rec aux ck for_ck =

102

let ck, for_ck = Clocks.repr ck, Clocks.repr for_ck in

103

match ck.Clocks.cdesc, for_ck.Clocks.cdesc with

104

 Clocks.Ctuple cklist1, Clocks.Ctuple cklist2 >

105

List.iter2 aux cklist1 cklist2

106

 _, Clocks.Cunivar _ >

107

Hashtbl.add substs for_ck ck

108

 _, _ >

109

()

110

in

111

aux ck for_ck;

112

substs

113


114

(* Expands a list of expressions *)

115

let rec expand_list ck_substs var_substs elist =

116

List.fold_right

117

(fun e (eqs, locs, elist) >

118

let eqs', locs', e' = expand_expr ck_substs var_substs e in

119

eqs' @ eqs, locs' @ locs, e' :: elist)

120

elist ([], [], [])

121


122

(* Expands the node instance [nd(args)]. *)

123

and expand_nodeinst parent_ck_substs parent_vsubsts nd args =

124

(* Expand arguments *)

125

let args_eqs, args_locs, args' =

126

expand_expr parent_ck_substs parent_vsubsts args

127

in

128

(* Compute clock substitutions to apply inside node's body *)

129

let ck_ins = args'.expr_clock in

130

let for_ck_ins, _ = Clocks.split_arrow nd.node_clock in

131

let ck_substs = build_ck_substs ck_ins for_ck_ins in

132

(* Compute variable substitutions to apply inside node's body, due to the

133

transformation of node variables into local variables of the main node. *)

134

let var_substs = Hashtbl.create 10 in

135

(* Add an equation in=arg for each node input + transform node input into a

136

local variable of the main node *)

137

let eq_ins, loc_ins =

138

List.split

139

(List.map2

140

(fun i e >

141

let i' =

142

new_local i.var_type i.var_clock i.var_dec_deadline i.var_loc

143

in

144

Hashtbl.add var_substs i.var_id i'.var_id;

145

{ eq_lhs = [ i'.var_id ]; eq_rhs = e; eq_loc = i.var_loc }, i')

146

nd.node_inputs (expr_list_of_expr args'))

147

in

148

(* Transform node local variables into local variables of the main node *)

149

let loc_sub =

150

List.map

151

(fun v >

152

let v' =

153

new_local v.var_type v.var_clock v.var_dec_deadline v.var_loc

154

in

155

Hashtbl.add var_substs v.var_id v'.var_id;

156

v')

157

nd.node_locals

158

in

159

(* Same for outputs *)

160

let loc_outs =

161

List.map

162

(fun o >

163

let o' =

164

new_local o.var_type o.var_clock o.var_dec_deadline o.var_loc

165

in

166

Hashtbl.add var_substs o.var_id o'.var_id;

167

o')

168

nd.node_outputs

169

in

170

(* A tuple made of the node outputs will replace the node call in the parent

171

node *)

172

let eout = Expr_tuple (List.map expr_of_var loc_outs) in

173

let new_eqs, new_locals = expand_eqs ck_substs var_substs nd.node_eqs in

174

( args_eqs @ eq_ins @ new_eqs,

175

args_locs @ loc_ins @ loc_outs @ loc_sub @ new_locals,

176

eout )

177


178

(* Expands an expression *)

179

and expand_expr ck_substs var_substs expr =

180

match expr.expr_desc with

181

 Expr_const cst >

182

[], [], new_expr_instance ck_substs var_substs expr expr.expr_desc

183

 Expr_ident id >

184

let id' = subst_var var_substs id in

185

let edesc = Expr_ident id' in

186

[], [], new_expr_instance ck_substs var_substs expr edesc

187

 Expr_tuple elist >

188

let new_eqs, new_locals, exp_elist =

189

expand_list ck_substs var_substs elist

190

in

191

( new_eqs,

192

new_locals,

193

new_expr_instance ck_substs var_substs expr (Expr_tuple exp_elist) )

194

 Expr_fby (cst, e) >

195

let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in

196

let edesc = Expr_fby (cst, e') in

197

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

198

 Expr_concat (cst, e) >

199

let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in

200

let edesc = Expr_concat (cst, e') in

201

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

202

 Expr_tail e >

203

let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in

204

let edesc = Expr_tail e' in

205

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

206

 Expr_when (e, c) >

207

let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in

208

let edesc = Expr_when (e', c) in

209

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

210

 Expr_whennot (e, c) >

211

let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in

212

let edesc = Expr_whennot (e', c) in

213

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

214

 Expr_merge (c, e1, e2) >

215

let new_eqs1, new_locals1, e1' = expand_expr ck_substs var_substs e1 in

216

let new_eqs2, new_locals2, e2' = expand_expr ck_substs var_substs e2 in

217

let edesc = Expr_merge (c, e1', e2') in

218

( new_eqs1 @ new_eqs2,

219

new_locals1 @ new_locals2,

220

new_expr_instance ck_substs var_substs expr edesc )

221

 Expr_appl (id, e, r) > (

222

let decl = Hashtbl.find node_table id in

223

match decl.top_decl_desc with

224

 ImportedNode _ >

225

let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in

226

let edesc = Expr_appl (id, e', r) in

227

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

228

 Node nd >

229

let new_eqs, new_locals, outs =

230

expand_nodeinst ck_substs var_substs nd e

231

in

232

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr outs

233

 Include _  Consts _  SensorDecl _  ActuatorDecl _ >

234

failwith "Internal error expand_expr")

235

 Expr_uclock (e, k) >

236

let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in

237

let edesc = Expr_uclock (e', k) in

238

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

239

 Expr_dclock (e, k) >

240

let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in

241

let edesc = Expr_dclock (e', k) in

242

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

243

 Expr_phclock (e, q) >

244

let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in

245

let edesc = Expr_phclock (e', q) in

246

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

247

 Expr_pre _  Expr_arrow _ >

248

assert false

249

(* Not used in the Prelude part of the code *)

250


251

(* Expands an equation *)

252

and expand_eq ck_substs var_substs eq =

253

let new_eqs, new_locals, expr = expand_expr ck_substs var_substs eq.eq_rhs in

254

let lhs' = List.map (subst_var var_substs) eq.eq_lhs in

255

let eq' = { eq_lhs = lhs'; eq_rhs = expr; eq_loc = eq.eq_loc } in

256

new_eqs, new_locals, eq'

257


258

(* Expands a set of equations *)

259

and expand_eqs ck_substs var_substs eqs =

260

List.fold_left

261

(fun (acc_eqs, acc_locals) eq >

262

let new_eqs, new_locals, eq' = expand_eq ck_substs var_substs eq in

263

eq' :: (new_eqs @ acc_eqs), new_locals @ acc_locals)

264

([], []) eqs

265


266

(* Expands the body of a node, replacing recursively all the node calls it

267

contains by the body of the corresponding node. *)

268

let expand_node nd =

269

let new_eqs, new_locals =

270

expand_eqs (Hashtbl.create 10) (Hashtbl.create 10) nd.node_eqs

271

in

272

{

273

node_id = nd.node_id;

274

node_type = nd.node_type;

275

node_clock = nd.node_clock;

276

node_inputs = nd.node_inputs;

277

node_outputs = nd.node_outputs;

278

node_locals = new_locals @ nd.node_locals;

279

node_asserts = nd.node_asserts;

280

node_eqs = new_eqs;

281

node_spec = nd.node_spec;

282

node_annot = nd.node_annot;

283

}

284


285

let expand_program () =

286

if !Options.main_node = "" then raise (Corelang.Error No_main_specified);

287

let main =

288

try Hashtbl.find node_table !Options.main_node

289

with Not_found > raise (Corelang.Error Main_not_found)

290

in

291

match main.top_decl_desc with

292

 Include _  Consts _  ImportedNode _  SensorDecl _  ActuatorDecl _ >

293

raise (Corelang.Error Main_wrong_kind)

294

 Node nd >

295

expand_node nd

296


297

(* Local Variables: *)

298

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

299

(* End: *)
