bjoernager/rust
bjoernager/rust
1
Fork 0
Code Activity

Teach the typechecker about the auto-dereference and auto-promote-to-mutable semantics we're going with

Browse source
This commit is contained in:
Patrick Walton 2010-06-29 19:53:24 -07:00
parent f05fc6b9d7
commit c2d4c1116f
2 changed files with 210 additions and 221 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/boot/me/trans.ml
View file

@ -3131,7 +3131,6 @@ let trans_visitor
(src:Il.cell) (src_ty:Ast.ty) (src:Il.cell) (src_ty:Ast.ty)
: unit = : unit =
let dst_ty = slot_ty dst_slot in let dst_ty = slot_ty dst_slot in
assert (src_ty = dst_ty);
match (dst_slot.Ast.slot_mode, clone) with match (dst_slot.Ast.slot_mode, clone) with
(Ast.MODE_alias, CLONE_none) -> (Ast.MODE_alias, CLONE_none) ->
mov dst (Il.Cell (alias (Il.Mem (need_mem_cell src)))) mov dst (Il.Cell (alias (Il.Mem (need_mem_cell src))))

430
src/boot/me/type.ml
View file

@ -2,27 +2,23 @@ open Common;;
open Semant;; open Semant;;
type tyspec = type tyspec =
TYSPEC_equiv of (simpl * tyvar) TYSPEC_equiv of tyvar
| TYSPEC_all | TYSPEC_all
| TYSPEC_resolved of (Ast.ty_param array) * Ast.ty | TYSPEC_resolved of (Ast.ty_param array) * Ast.ty
| TYSPEC_callable of (tyvar * tyvar array) (* out, ins *) | TYSPEC_callable of (tyvar * tyvar array) (* out, ins *)
| TYSPEC_collection of tyvar (* vec or str *) | TYSPEC_collection of tyvar (* vec or str *)
| TYSPEC_comparable (* comparable with = and != *) | TYSPEC_comparable (* comparable with = and != *)
| TYSPEC_plusable (* nums, vecs, and strings *) | TYSPEC_plusable (* nums, vecs, and strings *)
| TYSPEC_dictionary of dict | TYSPEC_dictionary of dict
| TYSPEC_integral (* int-like *) | TYSPEC_integral (* int-like *)
| TYSPEC_loggable | TYSPEC_loggable
| TYSPEC_numeric (* int-like or float-like *) | TYSPEC_numeric (* int-like or float-like *)
| TYSPEC_ordered (* comparable with < etc. *) | TYSPEC_ordered (* comparable with < etc. *)
| TYSPEC_record of dict | TYSPEC_record of dict
| TYSPEC_tuple of tyvar array (* heterogeneous tuple *) | TYSPEC_tuple of tyvar array (* heterogeneous tuple *)
| TYSPEC_vector of tyvar | TYSPEC_vector of tyvar
| TYSPEC_app of (tyvar * Ast.ty array) | TYSPEC_app of (tyvar * Ast.ty array)
and simpl = SIMPL_none
| SIMPL_exterior
| SIMPL_mutable
and dict = (Ast.ident, tyvar) Hashtbl.t and dict = (Ast.ident, tyvar) Hashtbl.t
and tyvar = tyspec ref;; and tyvar = tyspec ref;;
@ -37,6 +33,7 @@ type binopsig =
| BINOPSIG_plus_plus_plus (* plusable a * plusable a -> plusable a *) | BINOPSIG_plus_plus_plus (* plusable a * plusable a -> plusable a *)
;; ;;
let rec tyspec_to_str (ts:tyspec) : string = let rec tyspec_to_str (ts:tyspec) : string =
let fmt = Format.fprintf in let fmt = Format.fprintf in
@ -105,15 +102,7 @@ let rec tyspec_to_str (ts:tyspec) : string =
else else
Ast.fmt_ty ff ty Ast.fmt_ty ff ty
| TYSPEC_equiv (SIMPL_none, tv) -> | TYSPEC_equiv tv ->
fmt_tyspec ff (!tv)
| TYSPEC_equiv (SIMPL_exterior, tv) ->
fmt ff "@";
fmt_tyspec ff (!tv)
| TYSPEC_equiv (SIMPL_mutable, tv) ->
fmt ff "mutable ";
fmt_tyspec ff (!tv) fmt_tyspec ff (!tv)
| TYSPEC_callable (out, ins) -> | TYSPEC_callable (out, ins) ->
@ -168,7 +157,7 @@ let iflog cx thunk =
let rec resolve_tyvar (tv:tyvar) : tyvar = let rec resolve_tyvar (tv:tyvar) : tyvar =
match !tv with match !tv with
TYSPEC_equiv (_, subtv) -> resolve_tyvar subtv TYSPEC_equiv subtv -> resolve_tyvar subtv
| _ -> tv | _ -> tv
;; ;;
@ -209,16 +198,15 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
let visitor (cx:ctxt) (inner:Walk.visitor) : Walk.visitor = let visitor (cx:ctxt) (inner:Walk.visitor) : Walk.visitor =
let rec unify_slot let rec unify_slot
(simplify:bool)
(slot:Ast.slot) (slot:Ast.slot)
(id_opt:node_id option) (id_opt:node_id option)
(tv:tyvar) : unit = (tv:tyvar) : unit =
match id_opt with match id_opt with
Some id -> unify_tyvars simplify (Hashtbl.find bindings id) tv Some id -> unify_tyvars (Hashtbl.find bindings id) tv
| None -> | None ->
match slot.Ast.slot_ty with match slot.Ast.slot_ty with
None -> bug () "untyped unidentified slot" None -> bug () "untyped unidentified slot"
| Some ty -> unify_ty simplify ty tv | Some ty -> unify_ty ty tv
and check_sane_tyvar tv = and check_sane_tyvar tv =
match !tv with match !tv with
@ -226,56 +214,24 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
bug () "named-type in type checker" bug () "named-type in type checker"
| _ -> () | _ -> ()
and unify_tyvars (simplify:bool) (av:tyvar) (bv:tyvar) : unit = and unify_tyvars (av:tyvar) (bv:tyvar) : unit =
let sstr = if simplify then "w/ simplification" else "" in iflog cx (fun _ ->
iflog cx (fun _ -> log cx "unifying types:";
log cx "unifying types%s:" sstr; log cx "input tyvar A: %s" (tyspec_to_str !av);
log cx "input tyvar A: %s" (tyspec_to_str !av); log cx "input tyvar B: %s" (tyspec_to_str !bv));
log cx "input tyvar B: %s" (tyspec_to_str !bv)); check_sane_tyvar av;
check_sane_tyvar av; check_sane_tyvar bv;
check_sane_tyvar bv;
unify_tyvars' simplify av bv; unify_tyvars' av bv;
iflog cx (fun _ -> iflog cx (fun _ ->
log cx "unified types%s:" sstr; log cx "unified types:";
log cx "output tyvar A: %s" (tyspec_to_str !av); log cx "output tyvar A: %s" (tyspec_to_str !av);
log cx "output tyvar B: %s" (tyspec_to_str !bv)); log cx "output tyvar B: %s" (tyspec_to_str !bv));
check_sane_tyvar av; check_sane_tyvar av;
check_sane_tyvar bv; check_sane_tyvar bv;
and unify_tyvars' (av:tyvar) (bv:tyvar) : unit =
(* In some instances we will strip off a layer of mutability or
* exterior-ness, as trans is willing to transplant and/or overlook
* mutability / exterior differences wrt. many operators.
*
* Note: there is a secondary mutability-checking pass in effect.ml to
* ensure you're not actually mutating the insides of an immutable. That's
* not the typechecker's job.
*)
and unify_tyvars' (simplify:bool) (av:tyvar) (bv:tyvar) : unit =
let (a, b) = ((resolve_tyvar av), (resolve_tyvar bv)) in
let wrap tv =
match !tv with
TYSPEC_resolved (params, Ast.TY_mutable ty) ->
tv := TYSPEC_equiv (SIMPL_mutable,
(ref (TYSPEC_resolved (params, ty))));
true
| TYSPEC_resolved (params, Ast.TY_exterior ty) ->
tv := TYSPEC_equiv (SIMPL_exterior,
(ref (TYSPEC_resolved (params, ty))));
true
| _ -> false
in
if simplify
then
if (wrap a) || (wrap b)
then unify_tyvars' simplify a b
else unify_tyvars'' a b
else
unify_tyvars'' av bv
and unify_tyvars'' (av:tyvar) (bv:tyvar) : unit =
let (a, b) = ((resolve_tyvar av), (resolve_tyvar bv)) in let (a, b) = ((resolve_tyvar av), (resolve_tyvar bv)) in
let fail () = let fail () =
err None "mismatched types: %s vs. %s" (tyspec_to_str !av) err None "mismatched types: %s vs. %s" (tyspec_to_str !av)
@ -286,7 +242,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
let c = Hashtbl.create ((Hashtbl.length a) + (Hashtbl.length b)) in let c = Hashtbl.create ((Hashtbl.length a) + (Hashtbl.length b)) in
let merge ident tv_a = let merge ident tv_a =
if Hashtbl.mem c ident if Hashtbl.mem c ident
then unify_tyvars false (Hashtbl.find c ident) tv_a then unify_tyvars (Hashtbl.find c ident) tv_a
else Hashtbl.add c ident tv_a else Hashtbl.add c ident tv_a
in in
Hashtbl.iter (Hashtbl.add c) b; Hashtbl.iter (Hashtbl.add c) b;
@ -305,7 +261,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
in in
let check_entry ident tv = let check_entry ident tv =
unify_ty false (find_ty ident) tv unify_ty (find_ty ident) tv
in in
Hashtbl.iter check_entry dct Hashtbl.iter check_entry dct
in in
@ -316,11 +272,24 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
let check_entry (query:Ast.ident) tv : unit = let check_entry (query:Ast.ident) tv : unit =
match htab_search fns query with match htab_search fns query with
None -> fail () None -> fail ()
| Some fn -> unify_ty false (Ast.TY_fn fn) tv | Some fn -> unify_ty (Ast.TY_fn fn) tv
in in
Hashtbl.iter check_entry dct Hashtbl.iter check_entry dct
in in
let rec unify_resolved_types
(ty_a:Ast.ty)
(ty_b:Ast.ty)
: Ast.ty =
match ty_a, ty_b with
a, b when a = b -> a
| Ast.TY_exterior a, b | b, Ast.TY_exterior a ->
Ast.TY_exterior (unify_resolved_types a b)
| Ast.TY_mutable a, b | b, Ast.TY_mutable a ->
Ast.TY_mutable (unify_resolved_types a b)
| _ -> fail()
in
let rec is_comparable_or_ordered (comparable:bool) (ty:Ast.ty) : bool = let rec is_comparable_or_ordered (comparable:bool) (ty:Ast.ty) : bool =
match ty with match ty with
Ast.TY_mach _ | Ast.TY_int | Ast.TY_uint Ast.TY_mach _ | Ast.TY_int | Ast.TY_uint
@ -338,38 +307,41 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
is_comparable_or_ordered comparable ty is_comparable_or_ordered comparable ty
in in
let floating (ty:Ast.ty) : bool = let rec floating (ty:Ast.ty) : bool =
match ty with match ty with
Ast.TY_mach TY_f32 | Ast.TY_mach TY_f64 -> true Ast.TY_mach TY_f32 | Ast.TY_mach TY_f64 -> true
| Ast.TY_exterior ty | Ast.TY_mutable ty -> floating ty
| _ -> false | _ -> false
in in
let integral (ty:Ast.ty) : bool = let rec integral (ty:Ast.ty) : bool =
match ty with match ty with
Ast.TY_int | Ast.TY_uint | Ast.TY_mach TY_u8 | Ast.TY_mach TY_u16 Ast.TY_int | Ast.TY_uint | Ast.TY_mach TY_u8 | Ast.TY_mach TY_u16
| Ast.TY_mach TY_u32 | Ast.TY_mach TY_u64 | Ast.TY_mach TY_i8 | Ast.TY_mach TY_u32 | Ast.TY_mach TY_u64 | Ast.TY_mach TY_i8
| Ast.TY_mach TY_i16 | Ast.TY_mach TY_i32 | Ast.TY_mach TY_i16 | Ast.TY_mach TY_i32
| Ast.TY_mach TY_i64 -> | Ast.TY_mach TY_i64 ->
true true
| Ast.TY_exterior ty | Ast.TY_mutable ty -> integral ty
| _ -> false | _ -> false
in in
let numeric (ty:Ast.ty) : bool = (integral ty) || (floating ty) in let numeric (ty:Ast.ty) : bool = (integral ty) || (floating ty) in
let plusable (ty:Ast.ty) : bool = let rec plusable (ty:Ast.ty) : bool =
match ty with match ty with
Ast.TY_str -> true Ast.TY_str -> true
| Ast.TY_vec _ -> true | Ast.TY_vec _ -> true
| Ast.TY_exterior ty | Ast.TY_mutable ty -> plusable ty
| _ -> numeric ty | _ -> numeric ty
in in
let loggable (ty:Ast.ty) : bool = let rec loggable (ty:Ast.ty) : bool =
match ty with match ty with
Ast.TY_str | Ast.TY_bool | Ast.TY_int | Ast.TY_uint Ast.TY_str | Ast.TY_bool | Ast.TY_int | Ast.TY_uint | Ast.TY_char
| Ast.TY_char
| Ast.TY_mach TY_u8 | Ast.TY_mach TY_u16 | Ast.TY_mach TY_u32 | Ast.TY_mach TY_u8 | Ast.TY_mach TY_u16 | Ast.TY_mach TY_u32
| Ast.TY_mach TY_i8 | Ast.TY_mach TY_i16 | Ast.TY_mach TY_i32 | Ast.TY_mach TY_i8 | Ast.TY_mach TY_i16 | Ast.TY_mach TY_i32
-> true -> true
| Ast.TY_exterior ty | Ast.TY_mutable ty -> loggable ty
| _ -> false | _ -> false
in in
@ -384,40 +356,46 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
| (TYSPEC_resolved (params_a, ty_a), | (TYSPEC_resolved (params_a, ty_a),
TYSPEC_resolved (params_b, ty_b)) -> TYSPEC_resolved (params_b, ty_b)) ->
if params_a <> params_b || ty_a <> ty_b if params_a <> params_b then fail()
then fail() else TYSPEC_resolved (params_a, (unify_resolved_types ty_a ty_b))
else TYSPEC_resolved (params_a, ty_a)
| (TYSPEC_resolved (params, ty), | (TYSPEC_resolved (params, ty),
TYSPEC_callable (out_tv, in_tvs)) TYSPEC_callable (out_tv, in_tvs))
| (TYSPEC_callable (out_tv, in_tvs), | (TYSPEC_callable (out_tv, in_tvs),
TYSPEC_resolved (params, ty)) -> TYSPEC_resolved (params, ty)) ->
let unify_in_slot i in_slot = let unify_in_slot i in_slot =
unify_slot true in_slot None in_tvs.(i) unify_slot in_slot None in_tvs.(i)
in in
begin let rec unify ty =
match ty with match ty with
Ast.TY_fn ({ Ast.TY_fn ({
Ast.sig_input_slots = in_slots; Ast.sig_input_slots = in_slots;
Ast.sig_output_slot = out_slot Ast.sig_output_slot = out_slot
}, _) -> }, _) ->
if Array.length in_slots != Array.length in_tvs if Array.length in_slots != Array.length in_tvs
then fail (); then
unify_slot true out_slot None out_tv; fail ()
Array.iteri unify_in_slot in_slots else
unify_slot out_slot None out_tv;
Array.iteri unify_in_slot in_slots;
ty
| Ast.TY_exterior ty -> Ast.TY_exterior (unify ty)
| Ast.TY_mutable ty -> Ast.TY_mutable (unify ty)
| _ -> fail () | _ -> fail ()
end; in
TYSPEC_resolved (params, ty) TYSPEC_resolved (params, unify ty)
| (TYSPEC_resolved (params, ty), TYSPEC_collection tv) | (TYSPEC_resolved (params, ty), TYSPEC_collection tv)
| (TYSPEC_collection tv, TYSPEC_resolved (params, ty)) -> | (TYSPEC_collection tv, TYSPEC_resolved (params, ty)) ->
begin let rec unify ty =
match ty with match ty with
Ast.TY_vec ty -> unify_ty false ty tv Ast.TY_vec ty -> unify_ty ty tv; ty
| Ast.TY_str -> unify_ty false (Ast.TY_mach TY_u8) tv | Ast.TY_str -> unify_ty (Ast.TY_mach TY_u8) tv; ty
| Ast.TY_exterior ty -> Ast.TY_exterior (unify ty)
| Ast.TY_mutable ty -> Ast.TY_mutable (unify ty)
| _ -> fail () | _ -> fail ()
end; in
TYSPEC_resolved (params, ty) TYSPEC_resolved (params, unify ty)
| (TYSPEC_resolved (params, ty), TYSPEC_comparable) | (TYSPEC_resolved (params, ty), TYSPEC_comparable)
| (TYSPEC_comparable, TYSPEC_resolved (params, ty)) -> | (TYSPEC_comparable, TYSPEC_resolved (params, ty)) ->
@ -431,15 +409,19 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
| (TYSPEC_resolved (params, ty), TYSPEC_dictionary dct) | (TYSPEC_resolved (params, ty), TYSPEC_dictionary dct)
| (TYSPEC_dictionary dct, TYSPEC_resolved (params, ty)) -> | (TYSPEC_dictionary dct, TYSPEC_resolved (params, ty)) ->
begin let rec unify ty =
match ty with match ty with
Ast.TY_rec fields -> Ast.TY_rec fields ->
unify_dict_with_record_fields dct fields unify_dict_with_record_fields dct fields;
ty
| Ast.TY_obj (_, fns) -> | Ast.TY_obj (_, fns) ->
unify_dict_with_obj_fns dct fns unify_dict_with_obj_fns dct fns;
ty
| Ast.TY_exterior ty -> Ast.TY_exterior (unify ty)
| Ast.TY_mutable ty -> Ast.TY_mutable (unify ty)
| _ -> fail () | _ -> fail ()
end; in
TYSPEC_resolved (params, ty) TYSPEC_resolved (params, unify ty)
| (TYSPEC_resolved (params, ty), TYSPEC_integral) | (TYSPEC_resolved (params, ty), TYSPEC_integral)
| (TYSPEC_integral, TYSPEC_resolved (params, ty)) -> | (TYSPEC_integral, TYSPEC_resolved (params, ty)) ->
@ -466,55 +448,61 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
| (TYSPEC_resolved (params, ty), TYSPEC_app (tv, args)) | (TYSPEC_resolved (params, ty), TYSPEC_app (tv, args))
| (TYSPEC_app (tv, args), TYSPEC_resolved (params, ty)) -> | (TYSPEC_app (tv, args), TYSPEC_resolved (params, ty)) ->
let ty = rebuild_ty_under_params ty params args false in let ty = rebuild_ty_under_params ty params args false in
unify_ty false ty tv; unify_ty ty tv;
TYSPEC_resolved ([| |], ty) TYSPEC_resolved ([| |], ty)
| (TYSPEC_resolved (params, ty), TYSPEC_record dct) | (TYSPEC_resolved (params, ty), TYSPEC_record dct)
| (TYSPEC_record dct, TYSPEC_resolved (params, ty)) -> | (TYSPEC_record dct, TYSPEC_resolved (params, ty)) ->
begin let rec unify ty =
match ty with match ty with
Ast.TY_rec fields -> Ast.TY_rec fields ->
unify_dict_with_record_fields dct fields unify_dict_with_record_fields dct fields;
ty
| Ast.TY_exterior ty -> Ast.TY_exterior (unify ty)
| Ast.TY_mutable ty -> Ast.TY_mutable (unify ty)
| _ -> fail () | _ -> fail ()
end; in
TYSPEC_resolved (params, ty) TYSPEC_resolved (params, unify ty)
| (TYSPEC_resolved (params, ty), TYSPEC_tuple tvs) | (TYSPEC_resolved (params, ty), TYSPEC_tuple tvs)
| (TYSPEC_tuple tvs, TYSPEC_resolved (params, ty)) -> | (TYSPEC_tuple tvs, TYSPEC_resolved (params, ty)) ->
begin let rec unify ty =
match ty with match ty with
Ast.TY_tup (elem_tys:Ast.ty array) -> Ast.TY_tup (elem_tys:Ast.ty array) ->
if (Array.length elem_tys) <> (Array.length tvs) if (Array.length elem_tys) <> (Array.length tvs)
then fail () then fail ()
else else
let check_elem i tv = let check_elem i tv =
unify_ty false (elem_tys.(i)) tv unify_ty (elem_tys.(i)) tv
in in
Array.iteri check_elem tvs Array.iteri check_elem tvs;
ty
| Ast.TY_exterior ty -> Ast.TY_exterior ty
| Ast.TY_mutable ty -> Ast.TY_mutable ty
| _ -> fail () | _ -> fail ()
end; in
TYSPEC_resolved (params, ty) TYSPEC_resolved (params, unify ty)
| (TYSPEC_resolved (params, ty), TYSPEC_vector tv) | (TYSPEC_resolved (params, ty), TYSPEC_vector tv)
| (TYSPEC_vector tv, TYSPEC_resolved (params, ty)) -> | (TYSPEC_vector tv, TYSPEC_resolved (params, ty)) ->
begin let rec unify ty =
match ty with match ty with
Ast.TY_vec ty -> Ast.TY_vec ty -> unify_ty ty tv; ty
unify_ty false ty tv; | Ast.TY_exterior ty -> Ast.TY_exterior ty
TYSPEC_resolved (params, Ast.TY_vec ty) | Ast.TY_mutable ty -> Ast.TY_mutable ty
| _ -> fail () | _ -> fail ()
end in
TYSPEC_resolved (params, unify ty)
(* callable *) (* callable *)
| (TYSPEC_callable (a_out_tv, a_in_tvs), | (TYSPEC_callable (a_out_tv, a_in_tvs),
TYSPEC_callable (b_out_tv, b_in_tvs)) -> TYSPEC_callable (b_out_tv, b_in_tvs)) ->
unify_tyvars true a_out_tv b_out_tv; unify_tyvars a_out_tv b_out_tv;
let check_in_tv i a_in_tv = let check_in_tv i a_in_tv =
unify_tyvars true a_in_tv b_in_tvs.(i) unify_tyvars a_in_tv b_in_tvs.(i)
in in
Array.iteri check_in_tv a_in_tvs; Array.iteri check_in_tv a_in_tvs;
unify_tyvars true a_out_tv b_out_tv;
TYSPEC_callable (a_out_tv, a_in_tvs) TYSPEC_callable (a_out_tv, a_in_tvs)
| (TYSPEC_callable _, TYSPEC_collection _) | (TYSPEC_callable _, TYSPEC_collection _)
@ -545,7 +533,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
(* collection *) (* collection *)
| (TYSPEC_collection av, TYSPEC_collection bv) -> | (TYSPEC_collection av, TYSPEC_collection bv) ->
unify_tyvars false av bv; unify_tyvars av bv;
TYSPEC_collection av TYSPEC_collection av
| (TYSPEC_collection av, TYSPEC_comparable) | (TYSPEC_collection av, TYSPEC_comparable)
@ -574,7 +562,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
| (TYSPEC_collection av, TYSPEC_vector bv) | (TYSPEC_collection av, TYSPEC_vector bv)
| (TYSPEC_vector bv, TYSPEC_collection av) -> | (TYSPEC_vector bv, TYSPEC_collection av) ->
unify_tyvars false av bv; unify_tyvars av bv;
TYSPEC_vector av TYSPEC_vector av
(* comparable *) (* comparable *)
@ -743,7 +731,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
then fail() then fail()
else else
begin begin
unify_tyvars false tv_a tv_b; unify_tyvars tv_a tv_b;
TYSPEC_app (tv_a, args_a) TYSPEC_app (tv_a, args_a)
end end
@ -776,7 +764,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
else if i >= len_b else if i >= len_b
then tvs_a.(i) then tvs_a.(i)
else begin else begin
unify_tyvars false tvs_a.(i) tvs_b.(i); unify_tyvars tvs_a.(i) tvs_b.(i);
tvs_a.(i) tvs_a.(i)
end end
in in
@ -788,27 +776,26 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
(* vector *) (* vector *)
| (TYSPEC_vector av, TYSPEC_vector bv) -> | (TYSPEC_vector av, TYSPEC_vector bv) ->
unify_tyvars false av bv; unify_tyvars av bv;
TYSPEC_vector av TYSPEC_vector av
in in
let c = ref result in let c = ref result in
a := TYSPEC_equiv (SIMPL_none, c); a := TYSPEC_equiv c;
b := TYSPEC_equiv (SIMPL_none, c) b := TYSPEC_equiv c
and unify_ty_parametric and unify_ty_parametric
(simplify:bool)
(ty:Ast.ty) (ty:Ast.ty)
(tps:Ast.ty_param array) (tps:Ast.ty_param array)
(tv:tyvar) (tv:tyvar)
: unit = : unit =
unify_tyvars simplify (ref (TYSPEC_resolved (tps, ty))) tv unify_tyvars (ref (TYSPEC_resolved (tps, ty))) tv
and unify_ty (simplify:bool) (ty:Ast.ty) (tv:tyvar) : unit = and unify_ty (ty:Ast.ty) (tv:tyvar) : unit =
unify_ty_parametric simplify ty [||] tv unify_ty_parametric ty [||] tv
in in
let rec unify_lit (simplify:bool) (lit:Ast.lit) (tv:tyvar) : unit = let rec unify_lit (lit:Ast.lit) (tv:tyvar) : unit =
let ty = let ty =
match lit with match lit with
Ast.LIT_nil -> Ast.TY_nil Ast.LIT_nil -> Ast.TY_nil
@ -818,14 +805,14 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
| Ast.LIT_uint (_, _) -> Ast.TY_uint | Ast.LIT_uint (_, _) -> Ast.TY_uint
| Ast.LIT_char _ -> Ast.TY_char | Ast.LIT_char _ -> Ast.TY_char
in in
unify_ty simplify ty tv unify_ty ty tv
and unify_atom (simplify:bool) (atom:Ast.atom) (tv:tyvar) : unit = and unify_atom (atom:Ast.atom) (tv:tyvar) : unit =
match atom with match atom with
Ast.ATOM_literal { node = literal; id = _ } -> Ast.ATOM_literal { node = literal; id = _ } ->
unify_lit simplify literal tv unify_lit literal tv
| Ast.ATOM_lval lval -> | Ast.ATOM_lval lval ->
unify_lval simplify lval tv unify_lval lval tv
and unify_expr (expr:Ast.expr) (tv:tyvar) : unit = and unify_expr (expr:Ast.expr) (tv:tyvar) : unit =
match expr with match expr with
@ -858,64 +845,64 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
begin begin
match binop_sig with match binop_sig with
BINOPSIG_bool_bool_bool -> BINOPSIG_bool_bool_bool ->
unify_atom true lhs unify_atom lhs
(ref (TYSPEC_resolved ([||], Ast.TY_bool))); (ref (TYSPEC_resolved ([||], Ast.TY_bool)));
unify_atom true rhs unify_atom rhs
(ref (TYSPEC_resolved ([||], Ast.TY_bool))); (ref (TYSPEC_resolved ([||], Ast.TY_bool)));
unify_ty true Ast.TY_bool tv unify_ty Ast.TY_bool tv
| BINOPSIG_comp_comp_bool -> | BINOPSIG_comp_comp_bool ->
let tv_a = ref TYSPEC_comparable in let tv_a = ref TYSPEC_comparable in
unify_atom true lhs tv_a; unify_atom lhs tv_a;
unify_atom true rhs tv_a; unify_atom rhs tv_a;
unify_ty true Ast.TY_bool tv unify_ty Ast.TY_bool tv
| BINOPSIG_ord_ord_bool -> | BINOPSIG_ord_ord_bool ->
let tv_a = ref TYSPEC_ordered in let tv_a = ref TYSPEC_ordered in
unify_atom true lhs tv_a; unify_atom lhs tv_a;
unify_atom true rhs tv_a; unify_atom rhs tv_a;
unify_ty true Ast.TY_bool tv unify_ty Ast.TY_bool tv
| BINOPSIG_integ_integ_integ -> | BINOPSIG_integ_integ_integ ->
let tv_a = ref TYSPEC_integral in let tv_a = ref TYSPEC_integral in
unify_atom true lhs tv_a; unify_atom lhs tv_a;
unify_atom true rhs tv_a; unify_atom rhs tv_a;
unify_tyvars true tv tv_a unify_tyvars tv tv_a
| BINOPSIG_num_num_num -> | BINOPSIG_num_num_num ->
let tv_a = ref TYSPEC_numeric in let tv_a = ref TYSPEC_numeric in
unify_atom true lhs tv_a; unify_atom lhs tv_a;
unify_atom true rhs tv_a; unify_atom rhs tv_a;
unify_tyvars true tv tv_a unify_tyvars tv tv_a
| BINOPSIG_plus_plus_plus -> | BINOPSIG_plus_plus_plus ->
let tv_a = ref TYSPEC_plusable in let tv_a = ref TYSPEC_plusable in
unify_atom true lhs tv_a; unify_atom lhs tv_a;
unify_atom true rhs tv_a; unify_atom rhs tv_a;
unify_tyvars true tv tv_a unify_tyvars tv tv_a
end end
| Ast.EXPR_unary (unop, atom) -> | Ast.EXPR_unary (unop, atom) ->
begin begin
match unop with match unop with
Ast.UNOP_not -> Ast.UNOP_not ->
unify_atom true atom unify_atom atom
(ref (TYSPEC_resolved ([||], Ast.TY_bool))); (ref (TYSPEC_resolved ([||], Ast.TY_bool)));
unify_ty true Ast.TY_bool tv unify_ty Ast.TY_bool tv
| Ast.UNOP_bitnot -> | Ast.UNOP_bitnot ->
let tv_a = ref TYSPEC_integral in let tv_a = ref TYSPEC_integral in
unify_atom true atom tv_a; unify_atom atom tv_a;
unify_tyvars true tv tv_a unify_tyvars tv tv_a
| Ast.UNOP_neg -> | Ast.UNOP_neg ->
let tv_a = ref TYSPEC_numeric in let tv_a = ref TYSPEC_numeric in
unify_atom true atom tv_a; unify_atom atom tv_a;
unify_tyvars true tv tv_a unify_tyvars tv tv_a
| Ast.UNOP_cast t -> | Ast.UNOP_cast t ->
(* FIXME (issue #84): check cast-validity in (* FIXME (issue #84): check cast-validity in
* post-typecheck pass. Only some casts make sense. * post-typecheck pass. Only some casts make sense.
*) *)
let tv_a = ref TYSPEC_all in let tv_a = ref TYSPEC_all in
let t = Hashtbl.find cx.ctxt_all_cast_types t.id in let t = Hashtbl.find cx.ctxt_all_cast_types t.id in
unify_atom true atom tv_a; unify_atom atom tv_a;
unify_ty true t tv unify_ty t tv
end end
| Ast.EXPR_atom atom -> unify_atom true atom tv | Ast.EXPR_atom atom -> unify_atom atom tv
and unify_lval' (simplify:bool) (lval:Ast.lval) (tv:tyvar) : unit = and unify_lval' (lval:Ast.lval) (tv:tyvar) : unit =
let note_args args = let note_args args =
iflog cx (fun _ -> log cx "noting lval '%a' type arguments: %a" iflog cx (fun _ -> log cx "noting lval '%a' type arguments: %a"
Ast.sprintf_lval lval Ast.sprintf_app_args args); Ast.sprintf_lval lval Ast.sprintf_app_args args);
@ -937,7 +924,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
log cx "lval-base slot tyspec for %a = %s" log cx "lval-base slot tyspec for %a = %s"
Ast.sprintf_lval lval (tyspec_to_str (!tv)); Ast.sprintf_lval lval (tyspec_to_str (!tv));
end; end;
unify_slot simplify slot (Some referent) tv unify_slot slot (Some referent) tv
| _ -> | _ ->
let spec = (!(Hashtbl.find bindings referent)) in let spec = (!(Hashtbl.find bindings referent)) in
@ -959,7 +946,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
ref (TYSPEC_app (tv, args)) ref (TYSPEC_app (tv, args))
| _ -> err None "bad lval / tyspec combination" | _ -> err None "bad lval / tyspec combination"
in in
unify_tyvars simplify (ref spec) tv unify_tyvars (ref spec) tv
end end
| Ast.LVAL_ext (base, comp) -> | Ast.LVAL_ext (base, comp) ->
let base_ts = match comp with let base_ts = match comp with
@ -980,19 +967,19 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
TYSPEC_tuple (Array.init (i + 1) init) TYSPEC_tuple (Array.init (i + 1) init)
| Ast.COMP_atom atom -> | Ast.COMP_atom atom ->
unify_atom simplify atom unify_atom atom
(ref (TYSPEC_resolved ([||], Ast.TY_int))); (ref (TYSPEC_resolved ([||], Ast.TY_int)));
TYSPEC_collection tv TYSPEC_collection tv
in in
let base_tv = ref base_ts in let base_tv = ref base_ts in
unify_lval' simplify base base_tv; unify_lval' base base_tv;
match !(resolve_tyvar base_tv) with match !(resolve_tyvar base_tv) with
TYSPEC_resolved (_, ty) -> TYSPEC_resolved (_, ty) ->
unify_ty simplify (project_type ty comp) tv unify_ty (project_type ty comp) tv
| _ -> | _ ->
() ()
and unify_lval (simplify:bool) (lval:Ast.lval) (tv:tyvar) : unit = and unify_lval (lval:Ast.lval) (tv:tyvar) : unit =
let id = lval_base_id lval in let id = lval_base_id lval in
(* Fetch lval with type components resolved. *) (* Fetch lval with type components resolved. *)
let lval = Hashtbl.find cx.ctxt_all_lvals id in let lval = Hashtbl.find cx.ctxt_all_lvals id in
@ -1000,13 +987,13 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
"fetched resolved version of lval #%d = %a" "fetched resolved version of lval #%d = %a"
(int_of_node id) Ast.sprintf_lval lval); (int_of_node id) Ast.sprintf_lval lval);
Hashtbl.add lval_tyvars id tv; Hashtbl.add lval_tyvars id tv;
unify_lval' simplify lval tv unify_lval' lval tv
in in
let gen_atom_tvs atoms = let gen_atom_tvs atoms =
let gen_atom_tv atom = let gen_atom_tv atom =
let tv = ref TYSPEC_all in let tv = ref TYSPEC_all in
unify_atom true atom tv; unify_atom atom tv;
tv tv
in in
Array.map gen_atom_tv atoms Array.map gen_atom_tv atoms
@ -1016,12 +1003,12 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
let check_callable out_tv callee args = let check_callable out_tv callee args =
let in_tvs = gen_atom_tvs args in let in_tvs = gen_atom_tvs args in
let callee_tv = ref (TYSPEC_callable (out_tv, in_tvs)) in let callee_tv = ref (TYSPEC_callable (out_tv, in_tvs)) in
unify_lval true callee callee_tv; unify_lval callee callee_tv;
in in
match stmt.node with match stmt.node with
Ast.STMT_spawn (out, _, callee, args) -> Ast.STMT_spawn (out, _, callee, args) ->
let out_tv = ref (TYSPEC_resolved ([||], Ast.TY_nil)) in let out_tv = ref (TYSPEC_resolved ([||], Ast.TY_nil)) in
unify_lval true out (ref (TYSPEC_resolved ([||], Ast.TY_task))); unify_lval out (ref (TYSPEC_resolved ([||], Ast.TY_task)));
check_callable out_tv callee args check_callable out_tv callee args
| Ast.STMT_init_rec (lval, fields, Some base) -> | Ast.STMT_init_rec (lval, fields, Some base) ->
@ -1029,59 +1016,59 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
let tvrec = ref (TYSPEC_record dct) in let tvrec = ref (TYSPEC_record dct) in
let add_field (ident, atom) = let add_field (ident, atom) =
let tv = ref TYSPEC_all in let tv = ref TYSPEC_all in
unify_atom true atom tv; unify_atom atom tv;
Hashtbl.add dct ident tv Hashtbl.add dct ident tv
in in
Array.iter add_field fields; Array.iter add_field fields;
let tvbase = ref TYSPEC_all in let tvbase = ref TYSPEC_all in
unify_lval true base tvbase; unify_lval base tvbase;
unify_tyvars true tvrec tvbase; unify_tyvars tvrec tvbase;
unify_lval true lval tvrec unify_lval lval tvrec
| Ast.STMT_init_rec (lval, fields, None) -> | Ast.STMT_init_rec (lval, fields, None) ->
let dct = Hashtbl.create 10 in let dct = Hashtbl.create 10 in
let add_field (ident, atom) = let add_field (ident, atom) =
let tv = ref TYSPEC_all in let tv = ref TYSPEC_all in
unify_atom true atom tv; unify_atom atom tv;
Hashtbl.add dct ident tv Hashtbl.add dct ident tv
in in
Array.iter add_field fields; Array.iter add_field fields;
unify_lval true lval (ref (TYSPEC_record dct)) unify_lval lval (ref (TYSPEC_record dct))
| Ast.STMT_init_tup (lval, members) -> | Ast.STMT_init_tup (lval, members) ->
let member_to_tv atom = let member_to_tv atom =
let tv = ref TYSPEC_all in let tv = ref TYSPEC_all in
unify_atom true atom tv; unify_atom atom tv;
tv tv
in in
let member_tvs = Array.map member_to_tv members in let member_tvs = Array.map member_to_tv members in
unify_lval true lval (ref (TYSPEC_tuple member_tvs)) unify_lval lval (ref (TYSPEC_tuple member_tvs))
| Ast.STMT_init_vec (lval, atoms) -> | Ast.STMT_init_vec (lval, atoms) ->
let tv = ref TYSPEC_all in let tv = ref TYSPEC_all in
let unify_with_tv atom = unify_atom true atom tv in let unify_with_tv atom = unify_atom atom tv in
Array.iter unify_with_tv atoms; Array.iter unify_with_tv atoms;
unify_lval true lval (ref (TYSPEC_vector tv)) unify_lval lval (ref (TYSPEC_vector tv))
| Ast.STMT_init_str (lval, _) -> | Ast.STMT_init_str (lval, _) ->
unify_lval true lval (ref (TYSPEC_resolved ([||], Ast.TY_str))) unify_lval lval (ref (TYSPEC_resolved ([||], Ast.TY_str)))
| Ast.STMT_copy (lval, expr) -> | Ast.STMT_copy (lval, expr) ->
let tv = ref TYSPEC_all in let tv = ref TYSPEC_all in
unify_expr expr tv; unify_expr expr tv;
unify_lval true lval tv unify_lval lval tv
| Ast.STMT_copy_binop (lval, binop, at) -> | Ast.STMT_copy_binop (lval, binop, at) ->
let tv = ref TYSPEC_all in let tv = ref TYSPEC_all in
unify_expr (Ast.EXPR_binary (binop, Ast.ATOM_lval lval, at)) tv; unify_expr (Ast.EXPR_binary (binop, Ast.ATOM_lval lval, at)) tv;
unify_lval true lval tv; unify_lval lval tv;
| Ast.STMT_call (out, callee, args) -> | Ast.STMT_call (out, callee, args) ->
let out_tv = ref TYSPEC_all in let out_tv = ref TYSPEC_all in
unify_lval true out out_tv; unify_lval out out_tv;
check_callable out_tv callee args check_callable out_tv callee args
| Ast.STMT_log atom -> unify_atom true atom (ref TYSPEC_loggable) | Ast.STMT_log atom -> unify_atom atom (ref TYSPEC_loggable)
| Ast.STMT_check_expr expr -> | Ast.STMT_check_expr expr ->
unify_expr expr (ref (TYSPEC_resolved ([||], Ast.TY_bool))) unify_expr expr (ref (TYSPEC_resolved ([||], Ast.TY_bool)))
@ -1105,8 +1092,8 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
| Ast.STMT_put atom_opt -> | Ast.STMT_put atom_opt ->
begin begin
match atom_opt with match atom_opt with
None -> unify_ty true Ast.TY_nil (retval_tv()) None -> unify_ty Ast.TY_nil (retval_tv())
| Some atom -> unify_atom true atom (retval_tv()) | Some atom -> unify_atom atom (retval_tv())
end end
| Ast.STMT_be (callee, args) -> | Ast.STMT_be (callee, args) ->
@ -1124,7 +1111,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
begin begin
match atom_opt with match atom_opt with
None -> residue := tv :: (!residue); None -> residue := tv :: (!residue);
| Some atom -> unify_atom true atom tv | Some atom -> unify_atom atom tv
end; end;
tv tv
in in
@ -1135,14 +1122,14 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
let arg_residue_tvs = Array.of_list (List.rev (!residue)) in let arg_residue_tvs = Array.of_list (List.rev (!residue)) in
let callee_tv = ref (TYSPEC_callable (out_tv, in_tvs)) in let callee_tv = ref (TYSPEC_callable (out_tv, in_tvs)) in
let bound_tv = ref (TYSPEC_callable (out_tv, arg_residue_tvs)) in let bound_tv = ref (TYSPEC_callable (out_tv, arg_residue_tvs)) in
unify_lval true callee callee_tv; unify_lval callee callee_tv;
unify_lval true bound bound_tv unify_lval bound bound_tv
| Ast.STMT_for_each fe -> | Ast.STMT_for_each fe ->
let out_tv = ref TYSPEC_all in let out_tv = ref TYSPEC_all in
let (si, _) = fe.Ast.for_each_slot in let (si, _) = fe.Ast.for_each_slot in
let (callee, args) = fe.Ast.for_each_call in let (callee, args) = fe.Ast.for_each_call in
unify_slot true si.node (Some si.id) out_tv; unify_slot si.node (Some si.id) out_tv;
check_callable out_tv callee args check_callable out_tv callee args
| Ast.STMT_for fo -> | Ast.STMT_for fo ->
@ -1150,13 +1137,13 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
let seq_tv = ref (TYSPEC_collection mem_tv) in let seq_tv = ref (TYSPEC_collection mem_tv) in
let (si, _) = fo.Ast.for_slot in let (si, _) = fo.Ast.for_slot in
let (_, seq) = fo.Ast.for_seq in let (_, seq) = fo.Ast.for_seq in
unify_lval true seq seq_tv; unify_lval seq seq_tv;
unify_slot true si.node (Some si.id) mem_tv unify_slot si.node (Some si.id) mem_tv
| Ast.STMT_alt_tag | Ast.STMT_alt_tag
{ Ast.alt_tag_lval = lval; Ast.alt_tag_arms = arms } -> { Ast.alt_tag_lval = lval; Ast.alt_tag_arms = arms } ->
let lval_tv = ref TYSPEC_all in let lval_tv = ref TYSPEC_all in
unify_lval true lval lval_tv; unify_lval lval lval_tv;
Array.iter (fun _ -> push_pat_tv lval_tv) arms Array.iter (fun _ -> push_pat_tv lval_tv) arms
(* FIXME (issue #52): plenty more to handle here. *) (* FIXME (issue #52): plenty more to handle here. *)
@ -1183,7 +1170,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
let enter_fn fn retspec = let enter_fn fn retspec =
let out = fn.Ast.fn_output_slot in let out = fn.Ast.fn_output_slot in
push_retval_tv (ref retspec); push_retval_tv (ref retspec);
unify_slot true out.node (Some out.id) (retval_tv()) unify_slot out.node (Some out.id) (retval_tv())
in in
let visit_obj_fn_pre obj ident fn = let visit_obj_fn_pre obj ident fn =
@ -1250,12 +1237,12 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
let visit_pat_pre (pat:Ast.pat) : unit = let visit_pat_pre (pat:Ast.pat) : unit =
let expected = pat_tv() in let expected = pat_tv() in
match pat with match pat with
Ast.PAT_lit lit -> unify_lit true lit expected Ast.PAT_lit lit -> unify_lit lit expected
| Ast.PAT_tag (lval, _) -> | Ast.PAT_tag (lval, _) ->
let expect ty = let expect ty =
let tv = ref TYSPEC_all in let tv = ref TYSPEC_all in
unify_ty true ty tv; unify_ty ty tv;
push_pat_tv tv; push_pat_tv tv;
in in
@ -1267,7 +1254,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
* exactly to that function type, rebuilt under any latent type * exactly to that function type, rebuilt under any latent type
* parameters applied in the lval. *) * parameters applied in the lval. *)
let lval_tv = ref TYSPEC_all in let lval_tv = ref TYSPEC_all in
unify_lval true lval lval_tv; unify_lval lval lval_tv;
let tag_ctor_ty = let tag_ctor_ty =
match !(resolve_tyvar lval_tv) with match !(resolve_tyvar lval_tv) with
TYSPEC_resolved (_, ty) -> ty TYSPEC_resolved (_, ty) -> ty
@ -1279,13 +1266,13 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
let tag_ty_tup = tag_or_iso_ty_tup_by_name tag_ty lval_nm in let tag_ty_tup = tag_or_iso_ty_tup_by_name tag_ty lval_nm in
let tag_tv = ref TYSPEC_all in let tag_tv = ref TYSPEC_all in
unify_ty true tag_ty tag_tv; unify_ty tag_ty tag_tv;
unify_tyvars true expected tag_tv; unify_tyvars expected tag_tv;
List.iter expect List.iter expect
(List.rev (Array.to_list tag_ty_tup)); (List.rev (Array.to_list tag_ty_tup));
| Ast.PAT_slot (sloti, _) -> | Ast.PAT_slot (sloti, _) ->
unify_slot true sloti.node (Some sloti.id) expected unify_slot sloti.node (Some sloti.id) expected
| Ast.PAT_wild -> () | Ast.PAT_wild -> ()
in in
@ -1386,21 +1373,24 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
| _ -> bug () "check_auto_tyvar: no slot defn" | _ -> bug () "check_auto_tyvar: no slot defn"
in in
let rec get_resolved_ty tv id = let get_resolved_ty tv id =
match !tv with let ts = !(resolve_tyvar tv) in
TYSPEC_resolved ([||], ty) -> ty match ts with
| TYSPEC_vector tv -> TYSPEC_resolved ([||], ty) -> ty
Ast.TY_vec (get_resolved_ty tv id) | TYSPEC_vector (tv) ->
| TYSPEC_equiv (SIMPL_none, tv) -> begin
get_resolved_ty tv id match !(resolve_tyvar tv) with
| TYSPEC_equiv (SIMPL_mutable, tv) -> TYSPEC_resolved ([||], ty) ->
Ast.TY_mutable (get_resolved_ty tv id) (Ast.TY_vec ty)
| TYSPEC_equiv (SIMPL_exterior, tv) -> | _ ->
Ast.TY_exterior (get_resolved_ty tv id) err (Some id)
| _ -> err (Some id) "unresolved vector-element type in %s (%d)"
"unresolved type %s (%d)" (tyspec_to_str ts) (int_of_node id)
(tyspec_to_str !tv) end
(int_of_node id) | _ -> err (Some id)
"unresolved type %s (%d)"
(tyspec_to_str ts)
(int_of_node id)
in in
let check_auto_tyvar id = let check_auto_tyvar id =