## lustrec / src / init_calculus.ml @ 7dedc5f0

History | View | Annotate | Download (11.1 KB)

1 | b38ffff3 | ploc | (********************************************************************) |
---|---|---|---|

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 | 0cbf0839 | ploc | |

12 | (** Main typing module. Classic inference algorithm with destructive |
||

13 | unification. *) |
||

14 | |||

15 | (* Though it shares similarities with the clock calculus module, no code |
||

16 | is shared. Simple environments, very limited identifier scoping, no |
||

17 | identifier redefinition allowed. *) |
||

18 | |||

19 | open Utils |
||

20 | (* Yes, opening both modules is dirty as some type names will be |
||

21 | overwritten, yet this makes notations far lighter.*) |
||

22 | open Corelang |
||

23 | open Init |
||

24 | open Format |
||

25 | |||

26 | (** [occurs tvar ty] returns true if the type variable [tvar] occurs in |
||

27 | type [ty]. False otherwise. *) |
||

28 | let rec occurs tvar ty = |
||

29 | let ty = repr ty in |
||

30 | match ty.tdesc with |
||

31 | | Ivar -> ty=tvar |
||

32 | | Iarrow (t1, t2) -> |
||

33 | (occurs tvar t1) || (occurs tvar t2) |
||

34 | | Ituple tl -> |
||

35 | List.exists (occurs tvar) tl |
||

36 | | Ilink t -> occurs tvar t |
||

37 | | Isucc t -> occurs tvar t |
||

38 | | Iunivar -> false |
||

39 | |||

40 | (** Promote monomorphic type variables to polymorphic type variables. *) |
||

41 | (* Generalize by side-effects *) |
||

42 | let rec generalize ty = |
||

43 | match ty.tdesc with |
||

44 | | Ivar -> |
||

45 | (* No scopes, always generalize *) |
||

46 | ty.idesc <- Iunivar |
||

47 | | Iarrow (t1,t2) -> |
||

48 | generalize t1; generalize t2 |
||

49 | | Ituple tlist -> |
||

50 | List.iter generalize tlist |
||

51 | | Ilink t -> |
||

52 | generalize t |
||

53 | | Isucc t -> |
||

54 | generalize t |
||

55 | | Tunivar -> () |
||

56 | |||

57 | (** Downgrade polymorphic type variables to monomorphic type variables *) |
||

58 | let rec instanciate inst_vars ty = |
||

59 | let ty = repr ty in |
||

60 | match ty.idesc with |
||

61 | | Ivar -> ty |
||

62 | | Iarrow (t1,t2) -> |
||

63 | {ty with idesc = |
||

64 | Iarrow ((instanciate inst_vars t1), (instanciate inst_vars t2))} |
||

65 | | Ituple tlist -> |
||

66 | {ty with idesc = Ituple (List.map (instanciate inst_vars) tlist)} |
||

67 | | Isucc t -> |
||

68 | (* should not happen *) |
||

69 | {ty with idesc = Isucc (instanciate inst_vars t)} |
||

70 | | Ilink t -> |
||

71 | (* should not happen *) |
||

72 | {ty with idesc = Ilink (instanciate inst_vars t)} |
||

73 | | Iunivar -> |
||

74 | try |
||

75 | List.assoc ty.iid !inst_vars |
||

76 | with Not_found -> |
||

77 | let var = new_var () in |
||

78 | inst_vars := (ty.iid, var)::!inst_vars; |
||

79 | var |
||

80 | |||

81 | (** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify |
||

82 | (t1,t2)] if the types are not unifiable.*) |
||

83 | |||

84 | (* Standard destructive unification *) |
||

85 | (* may loop for omega types *) |
||

86 | let rec unify t1 t2 = |
||

87 | let t1 = repr t1 in |
||

88 | let t2 = repr t2 in |
||

89 | if t1=t2 then |
||

90 | () |
||

91 | else |
||

92 | (* No type abbreviations resolution for now *) |
||

93 | match t1.idesc,t2.idesc with |
||

94 | (* This case is not mandory but will keep "older" types *) |
||

95 | | Ivar, Ivar -> |
||

96 | if t1.iid < t2.iid then |
||

97 | t2.idesc <- Ilink t1 |
||

98 | else |
||

99 | t1.idesc <- Ilink t2 |
||

100 | | (Ivar, _) when (not (occurs t1 t2)) -> |
||

101 | t1.idesc <- Ilink t2 |
||

102 | | (_,Ivar) when (not (occurs t2 t1)) -> |
||

103 | t2.idesc <- Ilink t1 |
||

104 | | Isucc t1, Isucc t1' -> unify t1 t1' |
||

105 | | Iarrow (t1,t2), Iarrow (t1',t2') -> |
||

106 | unify t1 t1'; unify t2 t2' |
||

107 | | Ituple tlist1, Ituple tlist2 -> |
||

108 | if (List.length tlist1) <> (List.length tlist2) then |
||

109 | raise (Unify (t1, t2)) |
||

110 | else |
||

111 | List.iter2 unify tlist1 tlist2 |
||

112 | | Iunivar,_ | _, Iunivar -> |
||

113 | () |
||

114 | | _,_ -> raise (Unify (t1, t2)) |
||

115 | |||

116 | let init_of_const c = |
||

117 | Init_predef.init_zero |
||

118 | |||

119 | let rec init_expect env in_main expr ty = |
||

120 | let texpr = init_expr env in_main expr in |
||

121 | try |
||

122 | unify texpr ty |
||

123 | with Unify (t1,t2) -> |
||

124 | raise (Error (expr.expr_loc, Init_clash (t1,t2))) |
||

125 | |||

126 | and init_ident env in_main id loc = |
||

127 | init_expr env in_main (expr_of_ident id loc) |
||

128 | |||

129 | (** [type_expr env in_main expr] types expression [expr] in environment |
||

130 | [env]. *) |
||

131 | and init_expr env in_main expr = |
||

132 | match expr.expr_desc with |
||

133 | | Expr_const c -> |
||

134 | let ty = init_of_const c in |
||

135 | expr.expr_init <- ty; |
||

136 | ty |
||

137 | | Expr_ident v -> |
||

138 | let tyv = |
||

139 | try |
||

140 | Env.lookup_value env v |
||

141 | with Not_found -> |
||

142 | raise (Error (expr.expr_loc, Unbound_value v)) |
||

143 | in |
||

144 | let ty = instanciate (ref []) tyv in |
||

145 | expr.expr_init <- ty; |
||

146 | ty |
||

147 | | Expr_tuple elist -> |
||

148 | let ty = new_ty (Ttuple (List.map (type_expr env in_main) elist)) in |
||

149 | expr.expr_init <- ty; |
||

150 | ty |
||

151 | | Expr_appl (id, args, r) -> |
||

152 | (match r with |
||

153 | | None -> () |
||

154 | | Some x -> let expr_x = expr_of_ident x expr.expr_loc in |
||

155 | init_expect env in_main expr_x Init_predef.init_zero); |
||

156 | let tfun = type_ident env in_main id expr.expr_loc in |
||

157 | let tins,touts= split_arrow tfun in |
||

158 | type_expect env in_main args tins; |
||

159 | expr.expr_type <- touts; |
||

160 | touts |
||

161 | | Expr_arrow (e1,e2) -> |
||

162 | let ty = type_expr env in_main e1 in |
||

163 | type_expect env in_main e2 ty; |
||

164 | expr.expr_type <- ty; |
||

165 | ty |
||

166 | | Expr_fby (init,e) -> |
||

167 | let ty = type_of_const init in |
||

168 | type_expect env in_main e ty; |
||

169 | expr.expr_type <- ty; |
||

170 | ty |
||

171 | | Expr_concat (hd,e) -> |
||

172 | let ty = type_of_const hd in |
||

173 | type_expect env in_main e ty; |
||

174 | expr.expr_type <- ty; |
||

175 | ty |
||

176 | | Expr_tail e -> |
||

177 | let ty = type_expr env in_main e in |
||

178 | expr.expr_type <- ty; |
||

179 | ty |
||

180 | | Expr_pre e -> |
||

181 | let ty = type_expr env in_main e in |
||

182 | expr.expr_type <- ty; |
||

183 | ty |
||

184 | | Expr_when (e1,c) | Expr_whennot (e1,c) -> |
||

185 | let expr_c = expr_of_ident c expr.expr_loc in |
||

186 | type_expect env in_main expr_c Type_predef.type_bool; |
||

187 | let tlarg = type_expr env in_main e1 in |
||

188 | expr.expr_type <- tlarg; |
||

189 | tlarg |
||

190 | | Expr_merge (c,e2,e3) -> |
||

191 | let expr_c = expr_of_ident c expr.expr_loc in |
||

192 | type_expect env in_main expr_c Type_predef.type_bool; |
||

193 | let te2 = type_expr env in_main e2 in |
||

194 | type_expect env in_main e3 te2; |
||

195 | expr.expr_type <- te2; |
||

196 | te2 |
||

197 | | Expr_uclock (e,k) | Expr_dclock (e,k) -> |
||

198 | let ty = type_expr env in_main e in |
||

199 | expr.expr_type <- ty; |
||

200 | ty |
||

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

202 | let ty = type_expr env in_main e in |
||

203 | expr.expr_type <- ty; |
||

204 | ty |
||

205 | |||

206 | (** [type_eq env eq] types equation [eq] in environment [env] *) |
||

207 | let type_eq env in_main undefined_vars eq = |
||

208 | (* Check multiple variable definitions *) |
||

209 | let define_var id uvars = |
||

210 | try |
||

211 | ignore(IMap.find id uvars); |
||

212 | IMap.remove id uvars |
||

213 | with Not_found -> |
||

214 | raise (Error (eq.eq_loc, Already_defined id)) |
||

215 | in |
||

216 | let undefined_vars = |
||

217 | List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in |
||

218 | (* Type lhs *) |
||

219 | let get_value_type id = |
||

220 | try |
||

221 | Env.lookup_value env id |
||

222 | with Not_found -> |
||

223 | raise (Error (eq.eq_loc, Unbound_value id)) |
||

224 | in |
||

225 | let tyl_lhs = List.map get_value_type eq.eq_lhs in |
||

226 | let ty_lhs = type_of_type_list tyl_lhs in |
||

227 | (* Type rhs *) |
||

228 | type_expect env in_main eq.eq_rhs ty_lhs; |
||

229 | undefined_vars |
||

230 | |||

231 | (* [type_coretype cty] types the type declaration [cty] *) |
||

232 | let type_coretype cty = |
||

233 | match cty with |
||

234 | | Tydec_any -> new_var () |
||

235 | | Tydec_int -> Type_predef.type_int |
||

236 | | Tydec_real -> Type_predef.type_real |
||

237 | | Tydec_float -> Type_predef.type_real |
||

238 | | Tydec_bool -> Type_predef.type_bool |
||

239 | | Tydec_clock -> Type_predef.type_clock |
||

240 | |||

241 | (* [type_coreclock env ck id loc] types the type clock declaration [ck] |
||

242 | in environment [env] *) |
||

243 | let type_coreclock env ck id loc = |
||

244 | match ck.ck_dec_desc with |
||

245 | | Ckdec_any | Ckdec_pclock (_,_) -> () |
||

246 | | Ckdec_bool cl -> |
||

247 | let dummy_id_expr = expr_of_ident id loc in |
||

248 | let when_expr = |
||

249 | List.fold_left |
||

250 | (fun expr c -> |
||

251 | match c with |
||

252 | | Wtrue id -> |
||

253 | {expr_tag = new_tag (); |
||

254 | expr_desc=Expr_when (expr,id); |
||

255 | expr_type = new_var (); |
||

256 | expr_clock = Clocks.new_var true; |
||

257 | expr_loc=loc} |
||

258 | | Wfalse id -> |
||

259 | {expr_tag = new_tag (); |
||

260 | expr_desc=Expr_whennot (expr,id); |
||

261 | expr_type = new_var (); |
||

262 | expr_clock = Clocks.new_var true; |
||

263 | expr_loc=loc}) |
||

264 | dummy_id_expr cl |
||

265 | in |
||

266 | ignore (type_expr env false when_expr) |
||

267 | |||

268 | let type_var_decl env vdecl = |
||

269 | if (Env.exists_value env vdecl.var_id) then |
||

270 | raise (Error (vdecl.var_loc,Already_bound vdecl.var_id)) |
||

271 | else |
||

272 | let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in |
||

273 | let new_env = Env.add_value env vdecl.var_id ty in |
||

274 | type_coreclock new_env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; |
||

275 | vdecl.var_type <- ty; |
||

276 | new_env |
||

277 | |||

278 | let type_var_decl_list env l = |
||

279 | List.fold_left type_var_decl env l |
||

280 | |||

281 | let type_of_vlist vars = |
||

282 | let tyl = List.map (fun v -> v.var_type) vars in |
||

283 | type_of_type_list tyl |
||

284 | |||

285 | (** [type_node env nd loc] types node [nd] in environment env. The |
||

286 | location is used for error reports. *) |
||

287 | let type_node env nd loc = |
||

288 | let is_main = nd.node_id = !Options.main_node in |
||

289 | let delta_env = type_var_decl_list IMap.empty nd.node_inputs in |
||

290 | let delta_env = type_var_decl_list delta_env nd.node_outputs in |
||

291 | let delta_env = type_var_decl_list delta_env nd.node_locals in |
||

292 | let new_env = Env.overwrite env delta_env in |
||

293 | let undefined_vars_init = |
||

294 | List.fold_left |
||

295 | (fun uvs v -> IMap.add v.var_id () uvs) |
||

296 | IMap.empty (nd.node_outputs@nd.node_locals) in |
||

297 | let undefined_vars = |
||

298 | List.fold_left (type_eq new_env is_main) undefined_vars_init nd.node_eqs |
||

299 | in |
||

300 | (* check that table is empty *) |
||

301 | if (not (IMap.is_empty undefined_vars)) then |
||

302 | raise (Error (loc,Undefined_var undefined_vars)); |
||

303 | let ty_ins = type_of_vlist nd.node_inputs in |
||

304 | let ty_outs = type_of_vlist nd.node_outputs in |
||

305 | let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
||

306 | generalize ty_node; |
||

307 | (* TODO ? Check that no node in the hierarchy remains polymorphic ? *) |
||

308 | nd.node_type <- ty_node; |
||

309 | Env.add_value env nd.node_id ty_node |
||

310 | |||

311 | let type_imported_node env nd loc = |
||

312 | let new_env = type_var_decl_list env nd.nodei_inputs in |
||

313 | ignore(type_var_decl_list new_env nd.nodei_outputs); |
||

314 | let ty_ins = type_of_vlist nd.nodei_inputs in |
||

315 | let ty_outs = type_of_vlist nd.nodei_outputs in |
||

316 | let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
||

317 | generalize ty_node; |
||

318 | if (is_polymorphic ty_node) then |
||

319 | raise (Error (loc, Poly_imported_node nd.nodei_id)); |
||

320 | let new_env = Env.add_value env nd.nodei_id ty_node in |
||

321 | nd.nodei_type <- ty_node; |
||

322 | new_env |
||

323 | |||

324 | let type_top_decl env decl = |
||

325 | match decl.top_decl_desc with |
||

326 | | Node nd -> |
||

327 | type_node env nd decl.top_decl_loc |
||

328 | | ImportedNode nd -> |
||

329 | type_imported_node env nd decl.top_decl_loc |
||

330 | | SensorDecl _ | ActuatorDecl _ | Consts _ -> env |
||

331 | |||

332 | let type_top_consts env decl = |
||

333 | match decl.top_decl_desc with |
||

334 | | Consts clist -> |
||

335 | List.fold_left (fun env (id, c) -> |
||

336 | let ty = type_of_const c in |
||

337 | Env.add_value env id ty |
||

338 | ) env clist |
||

339 | | Node _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ -> env |
||

340 | |||

341 | let type_prog env decls = |
||

342 | let new_env = List.fold_left type_top_consts env decls in |
||

343 | ignore(List.fold_left type_top_decl new_env decls) |
||

344 | |||

345 | (* Local Variables: *) |
||

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

347 | (* End: *) |