Project

General

Profile

Revision a38c681e src/typing.ml

View differences:

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