Revision a38c681e src/typing.ml
src/typing.ml  

244  244 
 Dimension.Unify _ > 
245  245 
raise (Error (loc, Type_clash (ty1,ty2))) 
246  246  
247 
(* ty1 is a subtype of ty2 *) 

248 
(* 

249 
let rec sub_unify sub ty1 ty2 = 

250 
match (repr ty1).tdesc, (repr ty2).tdesc with 

251 
 Ttuple tl1 , Ttuple tl2 > 

252 
if List.length tl1 <> List.length tl2 

253 
then raise (Unify (ty1, ty2)) 

254 
else List.iter2 (sub_unify sub) tl1 tl2 

255 
 Ttuple [t1] , _ > sub_unify sub t1 ty2 

256 
 _ , Ttuple [t2] > sub_unify sub ty1 t2 

257 
 Tstruct tl1 , Tstruct tl2 > 

258 
if List.map fst tl1 <> List.map fst tl2 

259 
then raise (Unify (ty1, ty2)) 

260 
else List.iter2 (fun (_, t1) (_, t2) > sub_unify sub t1 t2) tl1 tl2 

261 
 Tclock t1 , Tclock t2 > sub_unify sub t1 t2 

262 
 Tclock t1 , _ when sub > sub_unify sub t1 ty2 

263 
 Tstatic (d1, t1) , Tstatic (d2, t2) > 

264 
begin 

265 
sub_unify sub t1 t2; 

266 
Dimension.eval Basic_library.eval_env (fun c > None) d1; 

267 
Dimension.eval Basic_library.eval_env (fun c > None) d2; 

268 
Dimension.unify d1 d2 

269 
end 

270 
 Tstatic (r_d, t1) , _ when sub > sub_unify sub t1 ty2 

271 
 _ > unify ty1 ty2 

272 
*) 

273  
274  247 
let rec type_struct_const_field loc (label, c) = 
275  248 
if Hashtbl.mem field_table label 
276  249 
then let tydec = Hashtbl.find field_table label in 
...  ...  
330  303 
if const_expected && not const_real 
331  304 
then raise (Error (loc, Not_a_constant)) 
332  305  
333 
let rec type_standard_args env in_main const expr_list = 

334 
let ty_list = 

335 
List.map 

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

337 
match get_clock_base_type ty with 

338 
 None > ty 

339 
 Some ty > ty) 

340 
expr_list in 

341 
let ty_res = new_var () in 

342 
List.iter2 (fun e ty > try_unify ty_res ty e.expr_loc) expr_list ty_list; 

343 
ty_res 

306 
let rec type_add_const env const arg targ = 

307 
if const 

308 
then let d = 

309 
if is_dimension_type targ 

310 
then dimension_of_expr arg 

311 
else Dimension.mkdim_var () in 

312 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in 

313 
Dimension.eval Basic_library.eval_env eval_const d; 

314 
let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in 

315 
(match Types.get_static_value targ with 

316 
 None > () 

317 
 Some d' > try_unify targ real_static_type arg.expr_loc); 

318 
real_static_type 

319 
else targ 

344  320  
345  321 
(* emulates a subtyping relation between types t and (d : t), 
346  322 
used during node applications and assignments *) 
347  323 
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = 
348  324 
let loc = real_arg.expr_loc in 
349  325 
let const = const  (Types.get_static_value formal_type <> None) in 
350 
let real_type = type_expr env in_main const real_arg in 

351 
let real_type = 

352 
if const 

353 
then let d = 

354 
if is_dimension_type real_type 

355 
then dimension_of_expr real_arg 

356 
else Dimension.mkdim_var () in 

357 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in 

358 
Dimension.eval Basic_library.eval_env eval_const d; 

359 
let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in 

360 
(match Types.get_static_value real_type with 

361 
 None > () 

362 
 Some d' > try_unify real_type real_static_type loc); 

363 
real_static_type 

364 
else real_type in 

326 
let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in 

365  327 
(*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;*) 
366  328 
try_unify ~sub:sub formal_type real_type loc 
367  329  
...  ...  
375  337 
it in many calls 
376  338 
*) 
377  339 
and type_appl env in_main loc const f args = 
378 
let args = expr_list_of_expr args in


379 
if Basic_library.is_internal_fun f && List.exists is_tuple_expr args


340 
let targs = List.map (type_expr env in_main const) args in


341 
if Basic_library.is_internal_fun f && List.exists is_tuple_type targs


380  342 
then 
381  343 
try 
382 
let args = Utils.transpose_list (List.map expr_list_of_expr args) in


383 
Types.type_of_type_list (List.map (type_call env in_main loc const f) args)


344 
let targs = Utils.transpose_list (List.map type_list_of_type targs) in


345 
Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)


384  346 
with 
385  347 
Utils.TransposeError (l, l') > raise (Error (loc, WrongMorphism (l, l'))) 
386  348 
else 
387 
type_call env in_main loc const f args


349 
type_dependent_call env in_main loc const f (List.combine args targs)


388  350  
389 
(* type a (single) call. [args] is here a list of arguments. *)


390 
and type_call env in_main loc const f args =


351 
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)


352 
and type_dependent_call env in_main loc const f targs =


391  353 
let tins, touts = new_var (), new_var () in 
392  354 
let tfun = Type_predef.type_arrow tins touts in 
393  355 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
394  356 
let tins = type_list_of_type tins in 
395 
if List.length args <> List.length tins then 

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

357 
if List.length targs <> List.length tins then


358 
raise (Error (loc, WrongArity (List.length tins, List.length targs)))


397  359 
else 
398 
List.iter2 (type_subtyping_arg env in_main const) args tins; 

360 
begin 

361 
List.iter2 (fun (a,t) ti > 

362 
let t' = type_add_const env (const  Types.get_static_value ti <> None) a t 

363 
in try_unify ~sub:true ti t' a.expr_loc) targs tins; 

364 
touts 

365 
end 

366  
367 
(* type a simple call without dependent types 

368 
but possible homomorphic extension. 

369 
[targs] is here a list of arguments' types. *) 

370 
and type_simple_call env in_main loc const f targs = 

371 
let tins, touts = new_var (), new_var () in 

372 
let tfun = Type_predef.type_arrow tins touts in 

373 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 

374 
(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*) 

375 
try_unify ~sub:true tins (type_of_type_list targs) loc; 

399  376 
touts 
400  377  
401  378 
(** [type_expr env in_main expr] types expression [expr] in environment 
...  ...  
425  402 
expr.expr_type < ty; 
426  403 
ty 
427  404 
 Expr_array elist > 
428 
let ty_elt = type_standard_args env in_main const elist in 

405 
let ty_elt = new_var () in 

406 
List.iter (fun e > try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist; 

429  407 
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in 
430  408 
let ty = Type_predef.type_array d ty_elt in 
431  409 
expr.expr_type < ty; 
...  ...  
441  419 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in 
442  420 
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; 
443  421 
Dimension.eval Basic_library.eval_env eval_const d; 
444 
let ty_elt = type_standard_args env in_main const [e1] in


422 
let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in


445  423 
let ty = Type_predef.type_array d ty_elt in 
446  424 
expr.expr_type < ty; 
447  425 
ty 
...  ...  
451  429 
ty 
452  430 
 Expr_ite (c, t, e) > 
453  431 
type_subtyping_arg env in_main const c Type_predef.type_bool; 
454 
let ty = type_standard_args env in_main const [t; e] in


432 
let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in


455  433 
expr.expr_type < ty; 
456  434 
ty 
457  435 
 Expr_appl (id, args, r) > 
...  ...  
466  444 
Type_predef.type_clock 
467  445 
(type_const expr.expr_loc (Const_tag l)) in 
468  446 
type_subtyping_arg env in_main ~sub:false const expr_x typ_l); 
469 
let touts = type_appl env in_main expr.expr_loc const id args in


447 
let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in


470  448 
expr.expr_type < touts; 
471  449 
touts 
472  450 
 Expr_fby (e1,e2) 
473  451 
 Expr_arrow (e1,e2) > 
474  452 
(* fby/arrow is not legal in a constant expression *) 
475  453 
check_constant expr.expr_loc const false; 
476 
let ty = type_standard_args env in_main const [e1; e2] in


454 
let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in


477  455 
expr.expr_type < ty; 
478  456 
ty 
479  457 
 Expr_pre e > 
480  458 
(* pre is not legal in a constant expression *) 
481  459 
check_constant expr.expr_loc const false; 
482 
let ty = type_standard_args env in_main const [e] in


460 
let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in


483  461 
expr.expr_type < ty; 
484  462 
ty 
485  463 
 Expr_when (e1,c,l) > 
...  ...  
488  466 
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in 
489  467 
let expr_c = expr_of_ident c expr.expr_loc in 
490  468 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
491 
(*update_clock env in_main c expr.expr_loc typ_l;*) 

492 
let ty = type_standard_args env in_main const [e1] in 

469 
let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in 

493  470 
expr.expr_type < ty; 
494  471 
ty 
495  472 
 Expr_merge (c,hl) > 
...  ...  
499  476 
let expr_c = expr_of_ident c expr.expr_loc in 
500  477 
let typ_l = Type_predef.type_clock typ_in in 
501  478 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
502 
(*update_clock env in_main c expr.expr_loc typ_l;*) 

503  479 
expr.expr_type < typ_out; 
504  480 
typ_out 
505  481 
in 
...  ...  
524  500 
else (typ_in, typ_out) 
525  501 
with Unify (t1, t2) > 
526  502 
raise (Error (loc, Type_clash (t1,t2))) 
527 
(* 

528 
and update_clock env in_main id loc typ = 

529 
(*Log.report ~level:1 (fun fmt > Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*) 

530 
try 

531 
let vdecl = List.find (fun v > v.var_id = id) (snd env) 

532 
in vdecl.var_type < typ 

533 
with 

534 
Not_found > 

535 
raise (Error (loc, Unbound_value ("clock " ^ id))) 

536 
*) 

503  
537  504 
(** [type_eq env eq] types equation [eq] in environment [env] *) 
538  505 
let type_eq env in_main undefined_vars eq = 
539  506 
(* Check undefined variables, type lhs *) 
Also available in: Unified diff