Project

General

Profile

Revision 59294251 src/typing.ml

View differences:

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 semi-unifiable.*)
223
(* Standard destructive semi-unification *)
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