## 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