Revision ca7ff3f7
Added by LĂ©lio Brun 7 months ago
src/checks/init_calculus.ml  

12  12 
(** Main typing module. Classic inference algorithm with destructive 
13  13 
unification. *) 
14  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. *)


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


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


17 
redefinition allowed. *) 

18  18  
19  19 
open Utils 
20 
(* Yes, opening both modules is dirty as some type names will be 

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

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

22 
yet this makes notations far lighter.*) 

22  23 
open Corelang 
23  24 
open Init 
24  25 
open Format 
25  26  
26 
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in 

27 
type [ty]. False otherwise. *)


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


28 
[ty]. False otherwise. *) 

28  29 
let rec occurs tvar ty = 
29  30 
let ty = repr ty in 
30  31 
match ty.tdesc with 
31 
 Ivar > ty=tvar 

32 
 Ivar > 

33 
ty = tvar 

32  34 
 Iarrow (t1, t2) > 
33 
(occurs tvar t1)  (occurs tvar t2)


35 
occurs tvar t1  occurs tvar t2


34  36 
 Ituple tl > 
35 
List.exists (occurs tvar) tl 

36 
 Ilink t > occurs tvar t 

37 
 Isucc t > occurs tvar t 

38 
 Iunivar > false 

37 
List.exists (occurs tvar) tl 

38 
 Ilink t > 

39 
occurs tvar t 

40 
 Isucc t > 

41 
occurs tvar t 

42 
 Iunivar > 

43 
false 

39  44  
40 
(** Promote monomorphic type variables to polymorphic type variables. *) 

41  45 
(* Generalize by sideeffects *) 
46  
47 
(** Promote monomorphic type variables to polymorphic type variables. *) 

42  48 
let rec generalize ty = 
43  49 
match ty.tdesc with 
44  50 
 Ivar > 
45 
(* No scopes, always generalize *) 

46 
ty.idesc < Iunivar 

47 
 Iarrow (t1,t2) > 

48 
generalize t1; generalize t2 

51 
(* No scopes, always generalize *) 

52 
ty.idesc < Iunivar 

53 
 Iarrow (t1, t2) > 

54 
generalize t1; 

55 
generalize t2 

49  56 
 Ituple tlist > 
50 
List.iter generalize tlist


57 
List.iter generalize tlist 

51  58 
 Ilink t > 
52 
generalize t


59 
generalize t 

53  60 
 Isucc t > 
54 
generalize t 

55 
 Tunivar > () 

61 
generalize t 

62 
 Tunivar > 

63 
() 

56  64  
57  65 
(** Downgrade polymorphic type variables to monomorphic type variables *) 
58  66 
let rec instanciate inst_vars ty = 
59  67 
let ty = repr ty in 
60  68 
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))} 

69 
 Ivar > 

70 
ty 

71 
 Iarrow (t1, t2) > 

72 
{ 

73 
ty with 

74 
idesc = Iarrow (instanciate inst_vars t1, instanciate inst_vars t2); 

75 
} 

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


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


67  78 
 Isucc t > 
68 
(* should not happen *)


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


79 
(* should not happen *)


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


70  81 
 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 

82 
(* should not happen *) 

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

84 
 Iunivar > ( 

85 
try List.assoc ty.iid !inst_vars 

86 
with Not_found > 

87 
let var = new_var () in 

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

89 
var) 

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

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


91 
(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify (t1,t2)] if the


92 
types are not unifiable.*) 

83  93  
84  94 
(* Standard destructive unification *) 
85  95 
(* may loop for omega types *) 
86  96 
let rec unify t1 t2 = 
87  97 
let t1 = repr t1 in 
88  98 
let t2 = repr t2 in 
89 
if t1=t2 then 

90 
() 

99 
if t1 = t2 then () 

91  100 
else 
92  101 
(* No type abbreviations resolution for now *) 
93 
match t1.idesc,t2.idesc with 

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


102 
match t1.idesc, t2.idesc with


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

95  104 
 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' 

105 
if t1.iid < t2.iid then t2.idesc < Ilink t1 else t1.idesc < Ilink t2 

106 
 Ivar, _ when not (occurs t1 t2) > 

107 
t1.idesc < Ilink t2 

108 
 _, Ivar when not (occurs t2 t1) > 

109 
t2.idesc < Ilink t1 

110 
 Isucc t1, Isucc t1' > 

111 
unify t1 t1' 

112 
 Iarrow (t1, t2), Iarrow (t1', t2') > 

113 
unify t1 t1'; 

114 
unify t2 t2' 

107  115 
 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)) 

116 
if List.length tlist1 <> List.length tlist2 then raise (Unify (t1, t2)) 

117 
else List.iter2 unify tlist1 tlist2 

118 
 Iunivar, _  _, Iunivar > 

119 
() 

120 
 _, _ > 

121 
raise (Unify (t1, t2)) 

115  122  
116 
let init_of_const c = 

117 
Init_predef.init_zero 

123 
let init_of_const c = Init_predef.init_zero 

118  124  
119  125 
let rec init_expect env in_main expr ty = 
120  126 
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))) 

127 
try unify texpr ty 

128 
with Unify (t1, t2) > raise (Error (expr.expr_loc, Init_clash (t1, t2))) 

125  129  
126 
and init_ident env in_main id loc = 

127 
init_expr env in_main (expr_of_ident id loc) 

130 
and init_ident env in_main id loc = init_expr env in_main (expr_of_ident id loc) 

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

130 
[env]. *) 

132 
(** [type_expr env in_main expr] types expression [expr] in environment [env]. *) 

131  133 
and init_expr env in_main expr = 
132  134 
match expr.expr_desc with 
133  135 
 Expr_const c > 
134 
let ty = init_of_const c in


135 
expr.expr_init < ty;


136 
ty


136 
let ty = init_of_const c in 

137 
expr.expr_init < ty; 

138 
ty 

137  139 
 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 

140 
let tyv = 

141 
try Env.lookup_value env v 

142 
with Not_found > 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  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


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

149 
expr.expr_init < ty; 

150 
ty 

151  151 
 Expr_appl (id, args, r) > 
152  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 

153 
 None > 

154 
() 

155 
 Some x > 

156 
let expr_x = expr_of_ident x expr.expr_loc in 

157 
init_expect env in_main expr_x Init_predef.init_zero); 

158 
let tfun = type_ident env in_main id expr.expr_loc in 

159 
let tins, touts = split_arrow tfun in 

160 
type_expect env in_main args tins; 

161 
expr.expr_type < touts; 

162 
touts 

163 
 Expr_arrow (e1, e2) > 

164 
let ty = type_expr env in_main e1 in 

165 
type_expect env in_main e2 ty; 

166 
expr.expr_type < ty; 

167 
ty 

168 
 Expr_fby (init, e) > 

169 
let ty = type_of_const init in 

170 
type_expect env in_main e ty; 

171 
expr.expr_type < ty; 

172 
ty 

173 
 Expr_concat (hd, e) > 

174 
let ty = type_of_const hd in 

175 
type_expect env in_main e ty; 

176 
expr.expr_type < ty; 

177 
ty 

176  178 
 Expr_tail e > 
177 
let ty = type_expr env in_main e in


178 
expr.expr_type < ty;


179 
ty


179 
let ty = type_expr env in_main e in 

180 
expr.expr_type < ty; 

181 
ty 

180  182 
 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


183 
let ty = type_expr env in_main e in 

184 
expr.expr_type < ty; 

185 
ty 

186 
 Expr_when (e1, c)  Expr_whennot (e1, c) >


187 
let expr_c = expr_of_ident c expr.expr_loc in 

188 
type_expect env in_main expr_c Type_predef.type_bool; 

189 
let tlarg = type_expr env in_main e1 in 

190 
expr.expr_type < tlarg; 

191 
tlarg 

192 
 Expr_merge (c, e2, e3) >


193 
let expr_c = expr_of_ident c expr.expr_loc in 

194 
type_expect env in_main expr_c Type_predef.type_bool; 

195 
let te2 = type_expr env in_main e2 in 

196 
type_expect env in_main e3 te2; 

197 
expr.expr_type < te2; 

198 
te2 

199 
 Expr_uclock (e, k)  Expr_dclock (e, k) >


200 
let ty = type_expr env in_main e in 

201 
expr.expr_type < ty; 

202 
ty 

203 
 Expr_phclock (e, q) >


204 
let ty = type_expr env in_main e in 

205 
expr.expr_type < ty; 

206 
ty 

205  207  
206  208 
(** [type_eq env eq] types equation [eq] in environment [env] *) 
207  209 
let type_eq env in_main undefined_vars eq = 
208  210 
(* Check multiple variable definitions *) 
209  211 
let define_var id uvars = 
210  212 
try 
211 
ignore(IMap.find id uvars); 

213 
ignore (IMap.find id uvars);


212  214 
IMap.remove id uvars 
213 
with Not_found > 

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

215 
with Not_found > raise (Error (eq.eq_loc, Already_defined id)) 

215  216 
in 
216  217 
let undefined_vars = 
217 
List.fold_left (fun uvars v > define_var v uvars) undefined_vars eq.eq_lhs in 

218 
List.fold_left (fun uvars v > define_var v uvars) undefined_vars eq.eq_lhs 

219 
in 

218  220 
(* Type lhs *) 
219  221 
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)) 

222 
try Env.lookup_value env id 

223 
with Not_found > raise (Error (eq.eq_loc, Unbound_value id)) 

224  224 
in 
225  225 
let tyl_lhs = List.map get_value_type eq.eq_lhs in 
226  226 
let ty_lhs = type_of_type_list tyl_lhs in 
227 
(* Type rhs *)


227 
(* Type rhs *) 

228  228 
type_expect env in_main eq.eq_rhs ty_lhs; 
229  229 
undefined_vars 
230  230  
231  231 
(* [type_coretype cty] types the type declaration [cty] *) 
232  232 
let type_coretype cty = 
233  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 

234 
 Tydec_any > 

235 
new_var () 

236 
 Tydec_int > 

237 
Type_predef.type_int 

238 
 Tydec_real > 

239 
Type_predef.type_real 

240 
 Tydec_float > 

241 
Type_predef.type_real 

242 
 Tydec_bool > 

243 
Type_predef.type_bool 

244 
 Tydec_clock > 

245 
Type_predef.type_clock 

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

242 
in environment [env] *)


247 
(* [type_coreclock env ck id loc] types the type clock declaration [ck] in


248 
environment [env] *) 

243  249 
let type_coreclock env ck id loc = 
244  250 
match ck.ck_dec_desc with 
245 
 Ckdec_any  Ckdec_pclock (_,_) > () 

251 
 Ckdec_any  Ckdec_pclock (_, _) > 

252 
() 

246  253 
 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) 

254 
let dummy_id_expr = expr_of_ident id loc in 

255 
let when_expr = 

256 
List.fold_left 

257 
(fun expr c > 

258 
match c with 

259 
 Wtrue id > 

260 
{ 

261 
expr_tag = new_tag (); 

262 
expr_desc = Expr_when (expr, id); 

263 
expr_type = new_var (); 

264 
expr_clock = Clocks.new_var true; 

265 
expr_loc = loc; 

266 
} 

267 
 Wfalse id > 

268 
{ 

269 
expr_tag = new_tag (); 

270 
expr_desc = Expr_whennot (expr, id); 

271 
expr_type = new_var (); 

272 
expr_clock = Clocks.new_var true; 

273 
expr_loc = loc; 

274 
}) 

275 
dummy_id_expr cl 

276 
in 

277 
ignore (type_expr env false when_expr) 

267  278  
268  279 
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)) 

280 
if Env.exists_value env vdecl.var_id then


281 
raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))


271  282 
else 
272  283 
let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in 
273  284 
let new_env = Env.add_value env vdecl.var_id ty in 
...  ...  
275  286 
vdecl.var_type < ty; 
276  287 
new_env 
277  288  
278 
let type_var_decl_list env l = 

279 
List.fold_left type_var_decl env l 

289 
let type_var_decl_list env l = List.fold_left type_var_decl env l 

280  290  
281  291 
let type_of_vlist vars = 
282  292 
let tyl = List.map (fun v > v.var_type) vars in 
283  293 
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. *)


294  
295 
(** [type_node env nd loc] types node [nd] in environment env. The location is


296 
used for error reports. *) 

287  297 
let type_node env nd loc = 
288  298 
let is_main = nd.node_id = !Options.main_node in 
289  299 
let delta_env = type_var_decl_list IMap.empty nd.node_inputs in 
...  ...  
293  303 
let undefined_vars_init = 
294  304 
List.fold_left 
295  305 
(fun uvs v > IMap.add v.var_id () uvs) 
296 
IMap.empty (nd.node_outputs@nd.node_locals) in 

306 
IMap.empty 

307 
(nd.node_outputs @ nd.node_locals) 

308 
in 

297  309 
let undefined_vars = 
298  310 
List.fold_left (type_eq new_env is_main) undefined_vars_init nd.node_eqs 
299  311 
in 
300  312 
(* check that table is empty *) 
301 
if (not (IMap.is_empty undefined_vars)) then


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

313 
if not (IMap.is_empty undefined_vars) then


314 
raise (Error (loc, Undefined_var undefined_vars));


303  315 
let ty_ins = type_of_vlist nd.node_inputs in 
304  316 
let ty_outs = type_of_vlist nd.node_outputs in 
305 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 

317 
let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in


306  318 
generalize ty_node; 
307  319 
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) 
308  320 
nd.node_type < ty_node; 
...  ...  
310  322  
311  323 
let type_imported_node env nd loc = 
312  324 
let new_env = type_var_decl_list env nd.nodei_inputs in 
313 
ignore(type_var_decl_list new_env nd.nodei_outputs); 

325 
ignore (type_var_decl_list new_env nd.nodei_outputs);


314  326 
let ty_ins = type_of_vlist nd.nodei_inputs in 
315  327 
let ty_outs = type_of_vlist nd.nodei_outputs in 
316 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 

328 
let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in


317  329 
generalize ty_node; 
318 
if (is_polymorphic ty_node) then


330 
if is_polymorphic ty_node then


319  331 
raise (Error (loc, Poly_imported_node nd.nodei_id)); 
320  332 
let new_env = Env.add_value env nd.nodei_id ty_node in 
321  333 
nd.nodei_type < ty_node; 
...  ...  
323  335  
324  336 
let type_top_decl env decl = 
325  337 
match decl.top_decl_desc with 
326 
 Node nd >


327 
type_node env nd decl.top_decl_loc


338 
 Node nd > 

339 
type_node env nd decl.top_decl_loc 

328  340 
 ImportedNode nd > 
329 
type_imported_node env nd decl.top_decl_loc 

330 
 SensorDecl _  ActuatorDecl _  Consts _ > env 

341 
type_imported_node env nd decl.top_decl_loc 

342 
 SensorDecl _  ActuatorDecl _  Consts _ > 

343 
env 

331  344  
332  345 
let type_top_consts env decl = 
333  346 
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 

347 
 Consts clist > 

348 
List.fold_left 

349 
(fun env (id, c) > 

350 
let ty = type_of_const c in 

351 
Env.add_value env id ty) 

352 
env clist 

353 
 Node _  ImportedNode _  SensorDecl _  ActuatorDecl _ > 

354 
env 

340  355  
341  356 
let type_prog env decls = 
342  357 
let new_env = List.fold_left type_top_consts env decls in 
343 
ignore(List.fold_left type_top_decl new_env decls) 

358 
ignore (List.fold_left type_top_decl new_env decls)


344  359  
345  360 
(* Local Variables: *) 
346  361 
(* compilecommand:"make C .." *) 
Also available in: Unified diff
reformatting