Revision 59294251 src/typing.ml
src/typing.ml  

159  159 
let def_t = get_type_definition t in 
160  160 
eq_ground t1 def_t 
161  161 
 Tarrow (t1,t2), Tarrow (t1',t2') > eq_ground t1 t1' && eq_ground t2 t2' 
162 
 Tclock t1', _ > eq_ground t1' t2 

163 
 _, Tclock t2' > eq_ground t1 t2' 

162 
 Tclock t1', Tclock t2' > eq_ground t1' t2' 

164  163 
 Tstatic (e1, t1'), Tstatic (e2, t2') 
165  164 
 Tarray (e1, t1'), Tarray (e2, t2') > Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2' 
166  165 
 _ > false 
167  166  
168 
(** [unify t1 t2] unifies types [t1] and [t2]. Raises [Unify 

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

170 
(* Standard destructive unification *) 

171 
let rec unify t1 t2 = 

172 
let t1 = repr t1 in 

173 
let t2 = repr t2 in 

174 
if t1=t2 then 

175 
() 

176 
else 

177 
(* No type abbreviations resolution for now *) 

178 
match t1.tdesc,t2.tdesc with 

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

180 
 Tvar, Tvar > 

167 
(** [unify t1 t2] unifies types [t1] and [t2] 

168 
using standard destructive unification. 

169 
Raises [Unify (t1,t2)] if the types are not unifiable. 

170 
[t1] is a expected/formal/spec type, [t2] is a computed/real/implem type, 

171 
so in case of unification error: expected type [t1], got type [t2]. 

172 
If [sub]typing is allowed, [t2] may be a subtype of [t1]. 

173 
If [semi] unification is required, 

174 
[t1] should furthermore be an instance of [t2] 

175 
and constants are handled differently.*) 

176 
let unify ?(sub=false) ?(semi=false) t1 t2 = 

177 
let rec unif t1 t2 = 

178 
let t1 = repr t1 in 

179 
let t2 = repr t2 in 

180 
if t1=t2 then 

181 
() 

182 
else 

183 
match t1.tdesc,t2.tdesc with 

184 
(* strictly subtyping cases first *) 

185 
 _ , Tclock t2 when sub && (get_clock_base_type t1 = None) > 

186 
unif t1 t2 

187 
 _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) > 

188 
unif t1 t2 

189 
(* This case is not mandatory but will keep "older" types *) 

190 
 Tvar, Tvar > 

181  191 
if t1.tid < t2.tid then 
182  192 
t2.tdesc < Tlink t1 
183  193 
else 
184  194 
t1.tdesc < Tlink t2 
185 
 (Tvar, _) when (not (occurs t1 t2)) >


195 
 Tvar, _ when (not semi) && (not (occurs t1 t2)) >


186  196 
t1.tdesc < Tlink t2 
187 
 (_,Tvar) when (not (occurs t2 t1)) > 

188 
t2.tdesc < Tlink t1 

189 
 Tarrow (t1,t2), Tarrow (t1',t2') > 

190 
begin 

191 
unify t1 t1'; 

192 
unify t2 t2' 

193 
end 

194 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > 

195 
List.iter2 unify tl tl' 

196 
 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > 

197 
List.iter2 (fun (_, t) (_, t') > unify t t') fl fl' 

198 
 Tclock _, Tstatic _ 

199 
 Tstatic _, Tclock _ > raise (Unify (t1, t2)) 

200 
 Tclock t1', _ > unify t1' t2 

201 
 _, Tclock t2' > unify t1 t2' 

202 
 Tint, Tint  Tbool, Tbool  Trat, Trat 

203 
 Tunivar, _  _, Tunivar > () 

204 
 (Tconst t, _) > 

205 
let def_t = get_type_definition t in 

206 
unify def_t t2 

207 
 (_, Tconst t) > 

208 
let def_t = get_type_definition t in 

209 
unify t1 def_t 

210 
 Tenum tl, Tenum tl' when tl == tl' > () 

211 
 Tstatic (e1, t1'), Tstatic (e2, t2') 

212 
 Tarray (e1, t1'), Tarray (e2, t2') > 

213 
begin 

214 
unify t1' t2'; 

215 
Dimension.eval Basic_library.eval_env (fun c > None) e1; 

216 
Dimension.eval Basic_library.eval_env (fun c > None) e2; 

217 
Dimension.unify e1 e2; 

218 
end 

219 
 _,_ > raise (Unify (t1, t2)) 

220  
221 
(** [semi_unify t1 t2] checks whether type [t1] is an instance of type [t2]. Raises [Unify 

222 
(t1,t2)] if the types are not semiunifiable.*) 

223 
(* Standard destructive semiunification *) 

224 
let rec semi_unify t1 t2 = 

225 
let t1 = repr t1 in 

226 
let t2 = repr t2 in 

227 
if t1=t2 then 

228 
() 

229 
else 

230 
(* No type abbreviations resolution for now *) 

231 
match t1.tdesc,t2.tdesc with 

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

233 
 Tvar, Tvar > 

234 
if t1.tid < t2.tid then 

235 
t2.tdesc < Tlink t1 

236 
else 

237 
t1.tdesc < Tlink t2 

238 
 (Tvar, _) > raise (Unify (t1, t2)) 

239 
 (_,Tvar) when (not (occurs t2 t1)) > 

197 
 _, Tvar when (not (occurs t2 t1)) > 

240  198 
t2.tdesc < Tlink t1 
241 
 Tarrow (t1,t2), Tarrow (t1',t2') > 

242 
begin 

243 
semi_unify t1 t1'; 

244 
semi_unify t2 t2' 

245 
end 

246 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > 

247 
List.iter2 semi_unify tl tl' 

248 
 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > 

249 
List.iter2 (fun (_, t) (_, t') > semi_unify t t') fl fl' 

250 
 Tclock _, Tstatic _ 

251 
 Tstatic _, Tclock _ > raise (Unify (t1, t2)) 

252 
 Tclock t1', _ > semi_unify t1' t2 

253 
 _, Tclock t2' > semi_unify t1 t2' 

254 
 Tint, Tint  Tbool, Tbool  Trat, Trat 

255 
 Tunivar, _  _, Tunivar > () 

256 
 (Tconst t, _) > 

257 
let def_t = get_type_definition t in 

258 
semi_unify def_t t2 

259 
 (_, Tconst t) > 

260 
let def_t = get_type_definition t in 

261 
semi_unify t1 def_t 

262 
 Tenum tl, Tenum tl' when tl == tl' > () 

263  
264 
 Tstatic (e1, t1'), Tstatic (e2, t2') 

265 
 Tarray (e1, t1'), Tarray (e2, t2') > 

266 
begin 

267 
semi_unify t1' t2'; 

268 
Dimension.eval Basic_library.eval_env (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) e1; 

269 
Dimension.eval Basic_library.eval_env (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) e2; 

270 
Dimension.semi_unify e1 e2; 

271 
end 

272 
 _,_ > raise (Unify (t1, t2)) 

199 
 Tarrow (t1,t2), Tarrow (t1',t2') > 

200 
begin 

201 
unif t2 t2'; 

202 
unif t1' t1 

203 
end 

204 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > 

205 
List.iter2 unif tl tl' 

206 
 Ttuple [t1] , _ > unif t1 t2 

207 
 _ , Ttuple [t2] > unif t1 t2 

208 
 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > 

209 
List.iter2 (fun (_, t) (_, t') > unif t t') fl fl' 

210 
 Tclock _, Tstatic _ 

211 
 Tstatic _, Tclock _ > raise (Unify (t1, t2)) 

212 
 Tclock t1', Tclock t2' > unif t1' t2' 

213 
 Tint, Tint  Tbool, Tbool  Trat, Trat 

214 
 Tunivar, _  _, Tunivar > () 

215 
 (Tconst t, _) > 

216 
let def_t = get_type_definition t in 

217 
unif def_t t2 

218 
 (_, Tconst t) > 

219 
let def_t = get_type_definition t in 

220 
unif t1 def_t 

221 
 Tenum tl, Tenum tl' when tl == tl' > () 

222 
 Tstatic (e1, t1'), Tstatic (e2, t2') 

223 
 Tarray (e1, t1'), Tarray (e2, t2') > 

224 
let eval_const = 

225 
if semi 

226 
then (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) 

227 
else (fun c > None) in 

228 
begin 

229 
unif t1' t2'; 

230 
Dimension.eval Basic_library.eval_env eval_const e1; 

231 
Dimension.eval Basic_library.eval_env eval_const e2; 

232 
Dimension.unify ~semi:semi e1 e2; 

233 
end 

234 
 _,_ > raise (Unify (t1, t2)) 

235 
in unif t1 t2 

273  236  
274  237 
(* Expected type ty1, got type ty2 *) 
275 
let try_unify ty1 ty2 loc = 

276 
try 

277 
unify ty1 ty2 

278 
with 

279 
 Unify _ > 

280 
raise (Error (loc, Type_clash (ty1,ty2))) 

281 
 Dimension.Unify _ > 

282 
raise (Error (loc, Type_clash (ty1,ty2))) 

283  
284 
let try_semi_unify ty1 ty2 loc = 

238 
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc = 

285  239 
try 
286 
semi_unify ty1 ty2


240 
unify ~sub:sub ~semi:semi ty1 ty2


287  241 
with 
288  242 
 Unify _ > 
289  243 
raise (Error (loc, Type_clash (ty1,ty2))) 
...  ...  
291  245 
raise (Error (loc, Type_clash (ty1,ty2))) 
292  246  
293  247 
(* ty1 is a subtype of ty2 *) 
248 
(* 

294  249 
let rec sub_unify sub ty1 ty2 = 
295  250 
match (repr ty1).tdesc, (repr ty2).tdesc with 
296  251 
 Ttuple tl1 , Ttuple tl2 > 
...  ...  
314  269 
end 
315  270 
 Tstatic (r_d, t1) , _ when sub > sub_unify sub t1 ty2 
316  271 
 _ > unify ty1 ty2 
317  
318 
let try_sub_unify sub ty1 ty2 loc = 

319 
try 

320 
sub_unify sub ty1 ty2 

321 
with 

322 
 Unify _ > 

323 
raise (Error (loc, Type_clash (ty1,ty2))) 

324 
 Dimension.Unify _ > 

325 
raise (Error (loc, Type_clash (ty1,ty2))) 

272 
*) 

326  273  
327  274 
let rec type_struct_const_field loc (label, c) = 
328  275 
if Hashtbl.mem field_table label 
...  ...  
383  330 
then raise (Error (loc, Not_a_constant)) 
384  331  
385  332 
let rec type_standard_args env in_main const expr_list = 
386 
let ty_list = List.map (fun e > dynamic_type (type_expr env in_main const e)) expr_list in 

333 
let ty_list = 

334 
List.map 

335 
(fun e > let ty = dynamic_type (type_expr env in_main const e) in 

336 
match get_clock_base_type ty with 

337 
 None > ty 

338 
 Some ty > ty) 

339 
expr_list in 

387  340 
let ty_res = new_var () in 
388  341 
List.iter2 (fun e ty > try_unify ty_res ty e.expr_loc) expr_list ty_list; 
389  342 
ty_res 
...  ...  
409  362 
real_static_type 
410  363 
else real_type in 
411  364 
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*) 
412 
try_sub_unify sub real_type formal_type loc


365 
try_unify ~sub:sub formal_type real_type loc


413  366  
414  367 
and type_ident env in_main loc const id = 
415  368 
type_expr env in_main const (expr_of_ident id loc) 
...  ...  
439  392 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
440  393 
let tins = type_list_of_type tins in 
441  394 
if List.length args <> List.length tins then 
442 
raise (Error (loc, WrongArity (List.length args, List.length tins)))


395 
raise (Error (loc, WrongArity (List.length tins, List.length args)))


443  396 
else 
444  397 
List.iter2 (type_subtyping_arg env in_main const) args tins; 
445  398 
touts 
...  ...  
534  487 
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in 
535  488 
let expr_c = expr_of_ident c expr.expr_loc in 
536  489 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
537 
update_clock env in_main c expr.expr_loc typ_l;


490 
(*update_clock env in_main c expr.expr_loc typ_l;*)


538  491 
let ty = type_standard_args env in_main const [e1] in 
539  492 
expr.expr_type < ty; 
540  493 
ty 
...  ...  
545  498 
let expr_c = expr_of_ident c expr.expr_loc in 
546  499 
let typ_l = Type_predef.type_clock typ_in in 
547  500 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
548 
update_clock env in_main c expr.expr_loc typ_l;


501 
(*update_clock env in_main c expr.expr_loc typ_l;*)


549  502 
expr.expr_type < typ_out; 
550  503 
typ_out 
551  504 
 Expr_uclock (e,k)  Expr_dclock (e,k) > 
...  ...  
578  531 
else (typ_in, typ_out) 
579  532 
with Unify (t1, t2) > 
580  533 
raise (Error (loc, Type_clash (t1,t2))) 
581  
534 
(* 

582  535 
and update_clock env in_main id loc typ = 
583  536 
(*Log.report ~level:1 (fun fmt > Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*) 
584  537 
try 
...  ...  
587  540 
with 
588  541 
Not_found > 
589  542 
raise (Error (loc, Unbound_value ("clock " ^ id))) 
590  
543 
*) 

591  544 
(** [type_eq env eq] types equation [eq] in environment [env] *) 
592  545 
let type_eq env in_main undefined_vars eq = 
593  546 
(* Check undefined variables, type lhs *) 
...  ...  
601  554 
with Not_found > 
602  555 
raise (Error (eq.eq_loc, Already_defined id)) 
603  556 
in 
557 
(* check assignment of declared constant, assignment of clock *) 

558 
let ty_lhs = 

559 
type_of_type_list 

560 
(List.map2 (fun ty id > 

561 
if get_static_value ty <> None 

562 
then raise (Error (eq.eq_loc, Assigned_constant id)) else 

563 
match get_clock_base_type ty with 

564 
 None > ty 

565 
 Some ty > ty) 

566 
(type_list_of_type ty_lhs) eq.eq_lhs) in 

604  567 
let undefined_vars = 
605  568 
List.fold_left (fun uvars v > define_var v uvars) undefined_vars eq.eq_lhs in 
606  569 
(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned 
...  ...  
802  765 
raise (Error (loc, Declared_but_undefined k))) in 
803  766 
(*Types.print_ty Format.std_formatter decl_type_k; 
804  767 
Types.print_ty Format.std_formatter computed_t;*) 
805 
try_semi_unify decl_type_k computed_t Location.dummy_loc


768 
try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc


806  769 
) 
807  770  
808  771 
(* Local Variables: *) 
Also available in: Unified diff