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

{ck with cdesc =

24

Carrow (subst_ck ck_substs var_substs ck1,

25

subst_ck ck_substs var_substs ck2)}

26

 Ctuple cklist >

27

{ck with cdesc =

28

Ctuple (List.map (subst_ck ck_substs var_substs) cklist)}

29

 Con (ck',c) >

30

{ck with cdesc =

31

Con (subst_ck ck_substs var_substs ck',c)}

32

 Connot (ck',c) >

33

{ck with cdesc =

34

Connot (subst_ck ck_substs var_substs ck',c)}

35

 Pck_up (ck',k) >

36

{ck with cdesc =

37

Pck_up (subst_ck ck_substs var_substs ck', k)}

38

 Pck_down (ck',k) >

39

{ck with cdesc =

40

Pck_down (subst_ck ck_substs var_substs ck', k)}

41

 Pck_phase (ck',q) >

42

{ck with cdesc =

43

Pck_phase (subst_ck ck_substs var_substs ck', q)}

44

 Pck_const _ >

45

ck

46

 Cvar _  Cunivar _ >

47

begin

48

try Hashtbl.find ck_substs ck with Not_found > ck

49

end

50

 Clink ck' >

51

subst_ck ck_substs var_substs ck'

52

 Ccarrying (_,ck') >

53

subst_ck ck_substs var_substs ck'

54


55

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

56

"instance" of expressions [e] of expression [e], where [edesc] is the

57

expanded version of [e]. *)

58

let new_expr_instance ck_substs var_substs e edesc =

59

{expr_tag = Utils.new_tag ();

60

expr_desc = edesc;

61

expr_type = e.expr_type;

62

expr_clock = subst_ck ck_substs var_substs e.expr_clock;

63

expr_delay = Delay.new_var ();

64

expr_loc = e.expr_loc;

65

expr_annot = e.expr_annot}

66


67

let locals_cpt = ref 0

68


69

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

70

let new_local vtyp vck vdd vloc =

71

let vid = "_"^(string_of_int !locals_cpt) in

72

locals_cpt := !locals_cpt+1;

73

let ty_dec = {ty_dec_desc = Tydec_any; ty_dec_loc = vloc} in (* dummy *)

74

let ck_dec = {ck_dec_desc = Ckdec_any; ck_dec_loc = vloc} in (* dummy *)

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

(* Returns an expression correponding to variable v *)

85

let expr_of_var v =

86

{expr_tag = Utils.new_tag ();

87

expr_desc = Expr_ident v.var_id;

88

expr_type = v.var_type;

89

expr_clock = v.var_clock;

90

expr_delay = Delay.new_var ();

91

expr_loc = v.var_loc;

92

expr_annot = None}

93


94

(* [build_ck_substs ck for_ck] computes the variable substitutions

95

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

96

let build_ck_substs ck for_ck =

97

let substs = Hashtbl.create 10 in

98

let rec aux ck for_ck =

99

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

100

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

101

 Clocks.Ctuple cklist1, Clocks.Ctuple cklist2 >

102

List.iter2 aux cklist1 cklist2

103

 _, Clocks.Cunivar _ >

104

Hashtbl.add substs for_ck ck

105

 _,_ >

106

()

107

in

108

aux ck for_ck;

109

substs

110


111

(* Expands a list of expressions *)

112

let rec expand_list ck_substs var_substs elist =

113

List.fold_right

114

(fun e (eqs,locs,elist) >

115

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

116

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

117

elist ([],[],[])

118


119

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

120

and expand_nodeinst parent_ck_substs parent_vsubsts nd args =

121

(* Expand arguments *)

122

let args_eqs, args_locs, args' =

123

expand_expr parent_ck_substs parent_vsubsts args in

124

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

125

let ck_ins = args'.expr_clock in

126

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

127

let ck_substs = build_ck_substs ck_ins for_ck_ins in

128

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

129

to the transformation of node variables into local variables of the

130

main node. *)

131

let var_substs = Hashtbl.create 10 in

132

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

133

into a local variable of the main node *)

134

let eq_ins, loc_ins =

135

List.split

136

(List.map2

137

(fun i e >

138

let i' =

139

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

140

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

141

{eq_lhs = [i'.var_id];

142

eq_rhs = e;

143

eq_loc = i.var_loc}, i')

144

nd.node_inputs (expr_list_of_expr args'))

145

in

146

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

147

node *)

148

let loc_sub =

149

List.map

150

(fun v >

151

let v' = new_local v.var_type v.var_clock v.var_dec_deadline v.var_loc in

152

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

153

v')

154

nd.node_locals

155

in

156

(* Same for outputs *)

157

let loc_outs =

158

List.map

159

(fun o >

160

let o' = new_local o.var_type o.var_clock o.var_dec_deadline o.var_loc in

161

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

162

o')

163

nd.node_outputs

164

in

165

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

166

node *)

167

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

168

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

169

args_eqs@eq_ins@new_eqs,

170

args_locs@loc_ins@loc_outs@loc_sub@new_locals,

171

eout

172


173

(* Expands an expression *)

174

and expand_expr ck_substs var_substs expr =

175

match expr.expr_desc with

176

 Expr_const cst >

177

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

178

 Expr_ident id >

179

let id' = subst_var var_substs id in

180

let edesc = Expr_ident id' in

181

[],[],new_expr_instance ck_substs var_substs expr edesc

182

 Expr_tuple elist >

183

let new_eqs,new_locals,exp_elist =

184

expand_list ck_substs var_substs elist in

185

new_eqs, new_locals,

186

new_expr_instance ck_substs var_substs expr (Expr_tuple exp_elist)

187

 Expr_fby (cst,e) >

188

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

189

let edesc = Expr_fby (cst, e') in

190

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

191

 Expr_concat (cst,e) >

192

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

193

let edesc = Expr_concat (cst, e') in

194

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

195

 Expr_tail e >

196

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

197

let edesc = Expr_tail e' in

198

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

199

 Expr_when (e,c) >

200

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

201

let edesc = Expr_when (e',c) in

202

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

203

 Expr_whennot (e,c) >

204

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

205

let edesc = Expr_whennot (e',c) in

206

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

207

 Expr_merge (c,e1,e2) >

208

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

209

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

210

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

211

new_eqs1@new_eqs2,

212

new_locals1@new_locals2,

213

new_expr_instance ck_substs var_substs expr edesc

214

 Expr_appl (id, e, r) >

215

let decl = Hashtbl.find node_table id in

216

begin

217

match decl.top_decl_desc with

218

 ImportedNode _ >

219

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

220

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

221

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

222

 Node nd >

223

let new_eqs, new_locals, outs =

224

expand_nodeinst ck_substs var_substs nd e in

225

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr outs

226

 Include _  Consts _  SensorDecl _  ActuatorDecl _ > failwith "Internal error expand_expr"

227

end

228

 Expr_uclock (e,k) >

229

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

230

let edesc = Expr_uclock (e',k) in

231

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

232

 Expr_dclock (e,k) >

233

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

234

let edesc = Expr_dclock (e',k) in

235

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

236

 Expr_phclock (e,q) >

237

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

238

let edesc = Expr_phclock (e',q) in

239

new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc

240

 Expr_pre _  Expr_arrow _ > assert false (* Not used in the Prelude part of the code *)

241


242

(* Expands an equation *)

243

and expand_eq ck_substs var_substs eq =

244

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

245

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

246

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

247

new_eqs, new_locals, eq'

248


249

(* Expands a set of equations *)

250

and expand_eqs ck_substs var_substs eqs =

251

List.fold_left

252

(fun (acc_eqs,acc_locals) eq >

253

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

254

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

255

([],[]) eqs

256


257

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

258

it contains by the body of the corresponding node. *)

259

let expand_node nd =

260

let new_eqs, new_locals =

261

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

262

{node_id = nd.node_id;

263

node_type = nd.node_type;

264

node_clock = nd.node_clock;

265

node_inputs = nd.node_inputs;

266

node_outputs = nd.node_outputs;

267

node_locals = new_locals@nd.node_locals;

268

node_asserts = nd.node_asserts;

269

node_eqs = new_eqs;

270

node_spec = nd.node_spec;

271

node_annot = nd.node_annot}

272


273

let expand_program () =

274

if !Options.main_node = "" then

275

raise (Corelang.Error No_main_specified);

276

let main =

277

try

278

Hashtbl.find node_table !Options.main_node

279

with Not_found >

280

raise (Corelang.Error Main_not_found)

281

in

282

match main.top_decl_desc with

283

 Include _  Consts _  ImportedNode _  SensorDecl _  ActuatorDecl _ >

284

raise (Corelang.Error Main_wrong_kind)

285

 Node nd >

286

expand_node nd

287


288

(* Local Variables: *)

289

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

290

(* End: *)
