## lustrec / src / expand.ml @ d4807c3d

History | View | Annotate | Download (11.1 KB)

1 | 22fe1c93 | ploc | (* ---------------------------------------------------------------------------- |
---|---|---|---|

2 | * SchedMCore - A MultiCore Scheduling Framework |
||

3 | * Copyright (C) 2009-2011, 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 02111-1307 |
||

20 | * USA |
||

21 | *---------------------------------------------------------------------------- *) |
||

22 | |||

23 | open Clocks |
||

24 | open Corelang |
||

25 | |||

26 | (* Applies variable substitutions *) |
||

27 | let subst_var var_substs vid = |
||

28 | try Hashtbl.find var_substs vid with Not_found -> vid |
||

29 | |||

30 | (* Applies clock substitutions *) |
||

31 | let rec subst_ck ck_substs var_substs ck = |
||

32 | match ck.cdesc with |
||

33 | | Carrow (ck1,ck2) -> |
||

34 | {ck with cdesc = |
||

35 | Carrow (subst_ck ck_substs var_substs ck1, |
||

36 | subst_ck ck_substs var_substs ck2)} |
||

37 | | Ctuple cklist -> |
||

38 | {ck with cdesc = |
||

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

40 | | Con (ck',c) -> |
||

41 | {ck with cdesc = |
||

42 | Con (subst_ck ck_substs var_substs ck',c)} |
||

43 | | Connot (ck',c) -> |
||

44 | {ck with cdesc = |
||

45 | Connot (subst_ck ck_substs var_substs ck',c)} |
||

46 | | Pck_up (ck',k) -> |
||

47 | {ck with cdesc = |
||

48 | Pck_up (subst_ck ck_substs var_substs ck', k)} |
||

49 | | Pck_down (ck',k) -> |
||

50 | {ck with cdesc = |
||

51 | Pck_down (subst_ck ck_substs var_substs ck', k)} |
||

52 | | Pck_phase (ck',q) -> |
||

53 | {ck with cdesc = |
||

54 | Pck_phase (subst_ck ck_substs var_substs ck', q)} |
||

55 | | Pck_const _ -> |
||

56 | ck |
||

57 | | Cvar _ | Cunivar _ -> |
||

58 | begin |
||

59 | try Hashtbl.find ck_substs ck with Not_found -> ck |
||

60 | end |
||

61 | | Clink ck' -> |
||

62 | subst_ck ck_substs var_substs ck' |
||

63 | | Ccarrying (_,ck') -> |
||

64 | subst_ck ck_substs var_substs ck' |
||

65 | |||

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

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

68 | expanded version of [e]. *) |
||

69 | let new_expr_instance ck_substs var_substs e edesc = |
||

70 | {expr_tag = Utils.new_tag (); |
||

71 | expr_desc = edesc; |
||

72 | expr_type = e.expr_type; |
||

73 | expr_clock = subst_ck ck_substs var_substs e.expr_clock; |
||

74 | expr_delay = Delay.new_var (); |
||

75 | expr_loc = e.expr_loc; |
||

76 | expr_annot = e.expr_annot} |
||

77 | |||

78 | let locals_cpt = ref 0 |
||

79 | |||

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

81 | let new_local vtyp vck vdd vloc = |
||

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

83 | locals_cpt := !locals_cpt+1; |
||

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

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

86 | {var_id = vid; |
||

87 | var_dec_type = ty_dec; |
||

88 | var_dec_clock = ck_dec; |
||

89 | var_dec_deadline = vdd; |
||

90 | var_type = vtyp; |
||

91 | var_clock = vck; |
||

92 | var_loc = vloc} |
||

93 | |||

94 | (* Returns an expression correponding to variable v *) |
||

95 | let expr_of_var v = |
||

96 | {expr_tag = Utils.new_tag (); |
||

97 | expr_desc = Expr_ident v.var_id; |
||

98 | expr_type = v.var_type; |
||

99 | expr_clock = v.var_clock; |
||

100 | expr_delay = Delay.new_var (); |
||

101 | expr_loc = v.var_loc; |
||

102 | expr_annot = None} |
||

103 | |||

104 | (* [build_ck_substs ck for_ck] computes the variable substitutions |
||

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

106 | let build_ck_substs ck for_ck = |
||

107 | let substs = Hashtbl.create 10 in |
||

108 | let rec aux ck for_ck = |
||

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

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

111 | | Clocks.Ctuple cklist1, Clocks.Ctuple cklist2 -> |
||

112 | List.iter2 aux cklist1 cklist2 |
||

113 | | _, Clocks.Cunivar _ -> |
||

114 | Hashtbl.add substs for_ck ck |
||

115 | | _,_ -> |
||

116 | () |
||

117 | in |
||

118 | aux ck for_ck; |
||

119 | substs |
||

120 | |||

121 | (* Expands a list of expressions *) |
||

122 | let rec expand_list ck_substs var_substs elist = |
||

123 | List.fold_right |
||

124 | (fun e (eqs,locs,elist) -> |
||

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

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

127 | elist ([],[],[]) |
||

128 | |||

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

130 | and expand_nodeinst parent_ck_substs parent_vsubsts nd args = |
||

131 | (* Expand arguments *) |
||

132 | let args_eqs, args_locs, args' = |
||

133 | expand_expr parent_ck_substs parent_vsubsts args in |
||

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

135 | let ck_ins = args'.expr_clock in |
||

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

137 | let ck_substs = build_ck_substs ck_ins for_ck_ins in |
||

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

139 | to the transformation of node variables into local variables of the |
||

140 | main node. *) |
||

141 | let var_substs = Hashtbl.create 10 in |
||

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

143 | into a local variable of the main node *) |
||

144 | let eq_ins, loc_ins = |
||

145 | List.split |
||

146 | (List.map2 |
||

147 | (fun i e -> |
||

148 | let i' = |
||

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

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

151 | {eq_lhs = [i'.var_id]; |
||

152 | eq_rhs = e; |
||

153 | eq_loc = i.var_loc}, i') |
||

154 | nd.node_inputs (expr_list_of_expr args')) |
||

155 | in |
||

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

157 | node *) |
||

158 | let loc_sub = |
||

159 | List.map |
||

160 | (fun v -> |
||

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

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

163 | v') |
||

164 | nd.node_locals |
||

165 | in |
||

166 | (* Same for outputs *) |
||

167 | let loc_outs = |
||

168 | List.map |
||

169 | (fun o -> |
||

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

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

172 | o') |
||

173 | nd.node_outputs |
||

174 | in |
||

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

176 | node *) |
||

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

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

179 | args_eqs@eq_ins@new_eqs, |
||

180 | args_locs@loc_ins@loc_outs@loc_sub@new_locals, |
||

181 | eout |
||

182 | |||

183 | (* Expands an expression *) |
||

184 | and expand_expr ck_substs var_substs expr = |
||

185 | match expr.expr_desc with |
||

186 | | Expr_const cst -> |
||

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

188 | | Expr_ident id -> |
||

189 | let id' = subst_var var_substs id in |
||

190 | let edesc = Expr_ident id' in |
||

191 | [],[],new_expr_instance ck_substs var_substs expr edesc |
||

192 | | Expr_tuple elist -> |
||

193 | let new_eqs,new_locals,exp_elist = |
||

194 | expand_list ck_substs var_substs elist in |
||

195 | new_eqs, new_locals, |
||

196 | new_expr_instance ck_substs var_substs expr (Expr_tuple exp_elist) |
||

197 | | Expr_fby (cst,e) -> |
||

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

199 | let edesc = Expr_fby (cst, e') in |
||

200 | new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc |
||

201 | | Expr_concat (cst,e) -> |
||

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

203 | let edesc = Expr_concat (cst, e') in |
||

204 | new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc |
||

205 | | Expr_tail e -> |
||

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

207 | let edesc = Expr_tail e' in |
||

208 | new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc |
||

209 | | Expr_when (e,c) -> |
||

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

211 | let edesc = Expr_when (e',c) in |
||

212 | new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc |
||

213 | | Expr_whennot (e,c) -> |
||

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

215 | let edesc = Expr_whennot (e',c) in |
||

216 | new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc |
||

217 | | Expr_merge (c,e1,e2) -> |
||

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

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

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

221 | new_eqs1@new_eqs2, |
||

222 | new_locals1@new_locals2, |
||

223 | new_expr_instance ck_substs var_substs expr edesc |
||

224 | | Expr_appl (id, e, r) -> |
||

225 | let decl = Hashtbl.find node_table id in |
||

226 | begin |
||

227 | match decl.top_decl_desc with |
||

228 | | ImportedNode _ -> |
||

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

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

231 | new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc |
||

232 | | Node nd -> |
||

233 | let new_eqs, new_locals, outs = |
||

234 | expand_nodeinst ck_substs var_substs nd e in |
||

235 | new_eqs, new_locals, new_expr_instance ck_substs var_substs expr outs |
||

236 | | Include _ | Consts _ | SensorDecl _ | ActuatorDecl _ -> failwith "Internal error expand_expr" |
||

237 | end |
||

238 | | Expr_uclock (e,k) -> |
||

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

240 | let edesc = Expr_uclock (e',k) in |
||

241 | new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc |
||

242 | | Expr_dclock (e,k) -> |
||

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

244 | let edesc = Expr_dclock (e',k) in |
||

245 | new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc |
||

246 | | Expr_phclock (e,q) -> |
||

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

248 | let edesc = Expr_phclock (e',q) in |
||

249 | new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc |
||

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

251 | |||

252 | (* Expands an equation *) |
||

253 | and expand_eq ck_substs var_substs eq = |
||

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

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

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

257 | new_eqs, new_locals, eq' |
||

258 | |||

259 | (* Expands a set of equations *) |
||

260 | and expand_eqs ck_substs var_substs eqs = |
||

261 | List.fold_left |
||

262 | (fun (acc_eqs,acc_locals) eq -> |
||

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

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

265 | ([],[]) eqs |
||

266 | |||

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

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

269 | let expand_node nd = |
||

270 | let new_eqs, new_locals = |
||

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

272 | {node_id = nd.node_id; |
||

273 | node_type = nd.node_type; |
||

274 | node_clock = nd.node_clock; |
||

275 | node_inputs = nd.node_inputs; |
||

276 | node_outputs = nd.node_outputs; |
||

277 | node_locals = new_locals@nd.node_locals; |
||

278 | node_asserts = nd.node_asserts; |
||

279 | node_eqs = new_eqs; |
||

280 | node_spec = nd.node_spec; |
||

281 | node_annot = nd.node_annot} |
||

282 | |||

283 | let expand_program () = |
||

284 | if !Options.main_node = "" then |
||

285 | raise (Corelang.Error No_main_specified); |
||

286 | let main = |
||

287 | try |
||

288 | Hashtbl.find node_table !Options.main_node |
||

289 | with Not_found -> |
||

290 | raise (Corelang.Error Main_not_found) |
||

291 | in |
||

292 | match main.top_decl_desc with |
||

293 | | Include _ | Consts _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ -> |
||

294 | raise (Corelang.Error Main_wrong_kind) |
||

295 | | Node nd -> |
||

296 | expand_node nd |
||

297 | |||

298 | (* Local Variables: *) |
||

299 | (* compile-command:"make -C .." *) |
||

300 | (* End: *) |