Thread a 'simplification' flag through unifier, attempt to strip off layers of ignorable types when simplification is permitted.
Gets std.rc through typechecking, but assigns some wrong types to lvals (the simplified types, not the correct ones).
This commit is contained in:
parent
7b11a52a37
commit
2a00a61ef3
@ -33,23 +33,6 @@ type binopsig =
|
||||
| BINOPSIG_plus_plus_plus (* plusable a * plusable a -> plusable a *)
|
||||
;;
|
||||
|
||||
|
||||
(* 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.
|
||||
*)
|
||||
let simplified t =
|
||||
match t with
|
||||
Ast.TY_mutable (Ast.TY_exterior t) -> t
|
||||
| Ast.TY_mutable t -> t
|
||||
| Ast.TY_exterior t -> t
|
||||
| _ -> t
|
||||
;;
|
||||
|
||||
let rec tyspec_to_str (ts:tyspec) : string =
|
||||
|
||||
let fmt = Format.fprintf in
|
||||
@ -214,15 +197,16 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
let visitor (cx:ctxt) (inner:Walk.visitor) : Walk.visitor =
|
||||
|
||||
let rec unify_slot
|
||||
(simplify:bool)
|
||||
(slot:Ast.slot)
|
||||
(id_opt:node_id option)
|
||||
(tv:tyvar) : unit =
|
||||
match id_opt with
|
||||
Some id -> unify_tyvars (Hashtbl.find bindings id) tv
|
||||
Some id -> unify_tyvars simplify (Hashtbl.find bindings id) tv
|
||||
| None ->
|
||||
match slot.Ast.slot_ty with
|
||||
None -> bug () "untyped unidentified slot"
|
||||
| Some ty -> unify_ty ty tv
|
||||
| Some ty -> unify_ty simplify ty tv
|
||||
|
||||
and check_sane_tyvar tv =
|
||||
match !tv with
|
||||
@ -230,24 +214,53 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
bug () "named-type in type checker"
|
||||
| _ -> ()
|
||||
|
||||
and unify_tyvars (av:tyvar) (bv:tyvar) : unit =
|
||||
iflog cx (fun _ ->
|
||||
log cx "unifying types:";
|
||||
log cx "input tyvar A: %s" (tyspec_to_str !av);
|
||||
log cx "input tyvar B: %s" (tyspec_to_str !bv));
|
||||
check_sane_tyvar av;
|
||||
check_sane_tyvar bv;
|
||||
and unify_tyvars (simplify:bool) (av:tyvar) (bv:tyvar) : unit =
|
||||
let sstr = if simplify then "w/ simplification" else "" in
|
||||
iflog cx (fun _ ->
|
||||
log cx "unifying types%s:" sstr;
|
||||
log cx "input tyvar A: %s" (tyspec_to_str !av);
|
||||
log cx "input tyvar B: %s" (tyspec_to_str !bv));
|
||||
check_sane_tyvar av;
|
||||
check_sane_tyvar bv;
|
||||
|
||||
unify_tyvars' av bv;
|
||||
unify_tyvars' simplify av bv;
|
||||
|
||||
iflog cx (fun _ ->
|
||||
log cx "unified types:";
|
||||
log cx "output tyvar A: %s" (tyspec_to_str !av);
|
||||
log cx "output tyvar B: %s" (tyspec_to_str !bv));
|
||||
check_sane_tyvar av;
|
||||
check_sane_tyvar bv;
|
||||
iflog cx (fun _ ->
|
||||
log cx "unified types%s:" sstr;
|
||||
log cx "output tyvar A: %s" (tyspec_to_str !av);
|
||||
log cx "output tyvar B: %s" (tyspec_to_str !bv));
|
||||
check_sane_tyvar av;
|
||||
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 simplified tv =
|
||||
match !tv with
|
||||
TYSPEC_resolved (params_a, Ast.TY_mutable ty_a) ->
|
||||
Some (ref (TYSPEC_resolved (params_a, ty_a)))
|
||||
| TYSPEC_resolved (params_a, Ast.TY_exterior ty_a) ->
|
||||
Some (ref (TYSPEC_resolved (params_a, ty_a)))
|
||||
| _ -> None
|
||||
in
|
||||
if simplify
|
||||
then
|
||||
match (simplified a, simplified b) with
|
||||
(Some a', _) -> unify_tyvars' simplify a' bv
|
||||
| (_, Some b') -> unify_tyvars' simplify av b'
|
||||
| (None, None) -> unify_tyvars'' av bv
|
||||
else
|
||||
unify_tyvars'' av bv
|
||||
|
||||
and unify_tyvars'' (av:tyvar) (bv:tyvar) : unit =
|
||||
let (a, b) = ((resolve_tyvar av), (resolve_tyvar bv)) in
|
||||
let fail () =
|
||||
err None "mismatched types: %s vs. %s" (tyspec_to_str !av)
|
||||
@ -258,7 +271,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
let c = Hashtbl.create ((Hashtbl.length a) + (Hashtbl.length b)) in
|
||||
let merge ident tv_a =
|
||||
if Hashtbl.mem c ident
|
||||
then unify_tyvars (Hashtbl.find c ident) tv_a
|
||||
then unify_tyvars false (Hashtbl.find c ident) tv_a
|
||||
else Hashtbl.add c ident tv_a
|
||||
in
|
||||
Hashtbl.iter (Hashtbl.add c) b;
|
||||
@ -277,7 +290,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
in
|
||||
|
||||
let check_entry ident tv =
|
||||
unify_ty (find_ty ident) tv
|
||||
unify_ty false (find_ty ident) tv
|
||||
in
|
||||
Hashtbl.iter check_entry dct
|
||||
in
|
||||
@ -288,7 +301,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
let check_entry (query:Ast.ident) tv : unit =
|
||||
match htab_search fns query with
|
||||
None -> fail ()
|
||||
| Some fn -> unify_ty (Ast.TY_fn fn) tv
|
||||
| Some fn -> unify_ty false (Ast.TY_fn fn) tv
|
||||
in
|
||||
Hashtbl.iter check_entry dct
|
||||
in
|
||||
@ -311,13 +324,13 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
in
|
||||
|
||||
let floating (ty:Ast.ty) : bool =
|
||||
match simplified ty with
|
||||
match ty with
|
||||
Ast.TY_mach TY_f32 | Ast.TY_mach TY_f64 -> true
|
||||
| _ -> false
|
||||
in
|
||||
|
||||
let integral (ty:Ast.ty) : bool =
|
||||
match simplified ty with
|
||||
match ty with
|
||||
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_i16 | Ast.TY_mach TY_i32
|
||||
@ -329,7 +342,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
let numeric (ty:Ast.ty) : bool = (integral ty) || (floating ty) in
|
||||
|
||||
let plusable (ty:Ast.ty) : bool =
|
||||
match simplified ty with
|
||||
match ty with
|
||||
Ast.TY_str -> true
|
||||
| Ast.TY_vec _ -> true
|
||||
| _ -> numeric ty
|
||||
@ -365,7 +378,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
| (TYSPEC_callable (out_tv, in_tvs),
|
||||
TYSPEC_resolved (params, ty)) ->
|
||||
let unify_in_slot i in_slot =
|
||||
unify_slot in_slot None in_tvs.(i)
|
||||
unify_slot true in_slot None in_tvs.(i)
|
||||
in
|
||||
begin
|
||||
match ty with
|
||||
@ -375,7 +388,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
}, _) ->
|
||||
if Array.length in_slots != Array.length in_tvs
|
||||
then fail ();
|
||||
unify_slot out_slot None out_tv;
|
||||
unify_slot true out_slot None out_tv;
|
||||
Array.iteri unify_in_slot in_slots
|
||||
| _ -> fail ()
|
||||
end;
|
||||
@ -385,8 +398,8 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
| (TYSPEC_collection tv, TYSPEC_resolved (params, ty)) ->
|
||||
begin
|
||||
match ty with
|
||||
Ast.TY_vec ty -> unify_ty ty tv
|
||||
| Ast.TY_str -> unify_ty (Ast.TY_mach TY_u8) tv
|
||||
Ast.TY_vec ty -> unify_ty false ty tv
|
||||
| Ast.TY_str -> unify_ty false (Ast.TY_mach TY_u8) tv
|
||||
| _ -> fail ()
|
||||
end;
|
||||
TYSPEC_resolved (params, ty)
|
||||
@ -438,7 +451,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
| (TYSPEC_resolved (params, ty), TYSPEC_app (tv, args))
|
||||
| (TYSPEC_app (tv, args), TYSPEC_resolved (params, ty)) ->
|
||||
let ty = rebuild_ty_under_params ty params args false in
|
||||
unify_ty ty tv;
|
||||
unify_ty false ty tv;
|
||||
TYSPEC_resolved ([| |], ty)
|
||||
|
||||
| (TYSPEC_resolved (params, ty), TYSPEC_record dct)
|
||||
@ -460,7 +473,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
then fail ()
|
||||
else
|
||||
let check_elem i tv =
|
||||
unify_ty (elem_tys.(i)) tv
|
||||
unify_ty false (elem_tys.(i)) tv
|
||||
in
|
||||
Array.iteri check_elem tvs
|
||||
| _ -> fail ()
|
||||
@ -472,7 +485,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
begin
|
||||
match ty with
|
||||
Ast.TY_vec ty ->
|
||||
unify_ty ty tv;
|
||||
unify_ty false ty tv;
|
||||
TYSPEC_resolved (params, Ast.TY_vec ty)
|
||||
| _ -> fail ()
|
||||
end
|
||||
@ -481,11 +494,12 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
|
||||
| (TYSPEC_callable (a_out_tv, a_in_tvs),
|
||||
TYSPEC_callable (b_out_tv, b_in_tvs)) ->
|
||||
unify_tyvars a_out_tv b_out_tv;
|
||||
unify_tyvars true a_out_tv b_out_tv;
|
||||
let check_in_tv i a_in_tv =
|
||||
unify_tyvars a_in_tv b_in_tvs.(i)
|
||||
unify_tyvars true a_in_tv b_in_tvs.(i)
|
||||
in
|
||||
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 _, TYSPEC_collection _)
|
||||
@ -516,7 +530,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
(* collection *)
|
||||
|
||||
| (TYSPEC_collection av, TYSPEC_collection bv) ->
|
||||
unify_tyvars av bv;
|
||||
unify_tyvars false av bv;
|
||||
TYSPEC_collection av
|
||||
|
||||
| (TYSPEC_collection av, TYSPEC_comparable)
|
||||
@ -545,7 +559,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
|
||||
| (TYSPEC_collection av, TYSPEC_vector bv)
|
||||
| (TYSPEC_vector bv, TYSPEC_collection av) ->
|
||||
unify_tyvars av bv;
|
||||
unify_tyvars false av bv;
|
||||
TYSPEC_vector av
|
||||
|
||||
(* comparable *)
|
||||
@ -714,7 +728,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
then fail()
|
||||
else
|
||||
begin
|
||||
unify_tyvars tv_a tv_b;
|
||||
unify_tyvars false tv_a tv_b;
|
||||
TYSPEC_app (tv_a, args_a)
|
||||
end
|
||||
|
||||
@ -747,7 +761,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
else if i >= len_b
|
||||
then tvs_a.(i)
|
||||
else begin
|
||||
unify_tyvars tvs_a.(i) tvs_b.(i);
|
||||
unify_tyvars false tvs_a.(i) tvs_b.(i);
|
||||
tvs_a.(i)
|
||||
end
|
||||
in
|
||||
@ -759,7 +773,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
(* vector *)
|
||||
|
||||
| (TYSPEC_vector av, TYSPEC_vector bv) ->
|
||||
unify_tyvars av bv;
|
||||
unify_tyvars false av bv;
|
||||
TYSPEC_vector av
|
||||
in
|
||||
let c = ref result in
|
||||
@ -767,18 +781,19 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
b := TYSPEC_equiv c
|
||||
|
||||
and unify_ty_parametric
|
||||
(simplify:bool)
|
||||
(ty:Ast.ty)
|
||||
(tps:Ast.ty_param array)
|
||||
(tv:tyvar)
|
||||
: unit =
|
||||
unify_tyvars (ref (TYSPEC_resolved (tps, ty))) tv
|
||||
unify_tyvars simplify (ref (TYSPEC_resolved (tps, ty))) tv
|
||||
|
||||
and unify_ty (ty:Ast.ty) (tv:tyvar) : unit =
|
||||
unify_ty_parametric ty [||] tv
|
||||
and unify_ty (simplify:bool) (ty:Ast.ty) (tv:tyvar) : unit =
|
||||
unify_ty_parametric simplify ty [||] tv
|
||||
|
||||
in
|
||||
|
||||
let rec unify_lit (lit:Ast.lit) (tv:tyvar) : unit =
|
||||
let rec unify_lit (simplify:bool) (lit:Ast.lit) (tv:tyvar) : unit =
|
||||
let ty =
|
||||
match lit with
|
||||
Ast.LIT_nil -> Ast.TY_nil
|
||||
@ -788,14 +803,14 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
| Ast.LIT_uint (_, _) -> Ast.TY_uint
|
||||
| Ast.LIT_char _ -> Ast.TY_char
|
||||
in
|
||||
unify_ty ty tv
|
||||
unify_ty simplify ty tv
|
||||
|
||||
and unify_atom (atom:Ast.atom) (tv:tyvar) : unit =
|
||||
and unify_atom (simplify:bool) (atom:Ast.atom) (tv:tyvar) : unit =
|
||||
match atom with
|
||||
Ast.ATOM_literal { node = literal; id = _ } ->
|
||||
unify_lit literal tv
|
||||
unify_lit simplify literal tv
|
||||
| Ast.ATOM_lval lval ->
|
||||
unify_lval lval tv
|
||||
unify_lval simplify lval tv
|
||||
|
||||
and unify_expr (expr:Ast.expr) (tv:tyvar) : unit =
|
||||
match expr with
|
||||
@ -828,64 +843,64 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
begin
|
||||
match binop_sig with
|
||||
BINOPSIG_bool_bool_bool ->
|
||||
unify_atom lhs
|
||||
unify_atom true lhs
|
||||
(ref (TYSPEC_resolved ([||], Ast.TY_bool)));
|
||||
unify_atom rhs
|
||||
unify_atom true rhs
|
||||
(ref (TYSPEC_resolved ([||], Ast.TY_bool)));
|
||||
unify_ty Ast.TY_bool tv
|
||||
unify_ty true Ast.TY_bool tv
|
||||
| BINOPSIG_comp_comp_bool ->
|
||||
let tv_a = ref TYSPEC_comparable in
|
||||
unify_atom lhs tv_a;
|
||||
unify_atom rhs tv_a;
|
||||
unify_ty Ast.TY_bool tv
|
||||
unify_atom true lhs tv_a;
|
||||
unify_atom true rhs tv_a;
|
||||
unify_ty true Ast.TY_bool tv
|
||||
| BINOPSIG_ord_ord_bool ->
|
||||
let tv_a = ref TYSPEC_ordered in
|
||||
unify_atom lhs tv_a;
|
||||
unify_atom rhs tv_a;
|
||||
unify_ty Ast.TY_bool tv
|
||||
unify_atom true lhs tv_a;
|
||||
unify_atom true rhs tv_a;
|
||||
unify_ty true Ast.TY_bool tv
|
||||
| BINOPSIG_integ_integ_integ ->
|
||||
let tv_a = ref TYSPEC_integral in
|
||||
unify_atom lhs tv_a;
|
||||
unify_atom rhs tv_a;
|
||||
unify_tyvars tv tv_a
|
||||
unify_atom true lhs tv_a;
|
||||
unify_atom true rhs tv_a;
|
||||
unify_tyvars true tv tv_a
|
||||
| BINOPSIG_num_num_num ->
|
||||
let tv_a = ref TYSPEC_numeric in
|
||||
unify_atom lhs tv_a;
|
||||
unify_atom rhs tv_a;
|
||||
unify_tyvars tv tv_a
|
||||
unify_atom true lhs tv_a;
|
||||
unify_atom true rhs tv_a;
|
||||
unify_tyvars true tv tv_a
|
||||
| BINOPSIG_plus_plus_plus ->
|
||||
let tv_a = ref TYSPEC_plusable in
|
||||
unify_atom lhs tv_a;
|
||||
unify_atom rhs tv_a;
|
||||
unify_tyvars tv tv_a
|
||||
unify_atom true lhs tv_a;
|
||||
unify_atom true rhs tv_a;
|
||||
unify_tyvars true tv tv_a
|
||||
end
|
||||
| Ast.EXPR_unary (unop, atom) ->
|
||||
begin
|
||||
match unop with
|
||||
Ast.UNOP_not ->
|
||||
unify_atom atom
|
||||
unify_atom true atom
|
||||
(ref (TYSPEC_resolved ([||], Ast.TY_bool)));
|
||||
unify_ty Ast.TY_bool tv
|
||||
unify_ty true Ast.TY_bool tv
|
||||
| Ast.UNOP_bitnot ->
|
||||
let tv_a = ref TYSPEC_integral in
|
||||
unify_atom atom tv_a;
|
||||
unify_tyvars tv tv_a
|
||||
unify_atom true atom tv_a;
|
||||
unify_tyvars true tv tv_a
|
||||
| Ast.UNOP_neg ->
|
||||
let tv_a = ref TYSPEC_numeric in
|
||||
unify_atom atom tv_a;
|
||||
unify_tyvars tv tv_a
|
||||
unify_atom true atom tv_a;
|
||||
unify_tyvars true tv tv_a
|
||||
| Ast.UNOP_cast t ->
|
||||
(* FIXME (issue #84): check cast-validity in
|
||||
* post-typecheck pass. Only some casts make sense.
|
||||
*)
|
||||
let tv_a = ref TYSPEC_all in
|
||||
let t = Hashtbl.find cx.ctxt_all_cast_types t.id in
|
||||
unify_atom atom tv_a;
|
||||
unify_ty t tv
|
||||
unify_atom true atom tv_a;
|
||||
unify_ty true t tv
|
||||
end
|
||||
| Ast.EXPR_atom atom -> unify_atom atom tv
|
||||
| Ast.EXPR_atom atom -> unify_atom true atom tv
|
||||
|
||||
and unify_lval' (lval:Ast.lval) (tv:tyvar) : unit =
|
||||
and unify_lval' (simplify:bool) (lval:Ast.lval) (tv:tyvar) : unit =
|
||||
let note_args args =
|
||||
iflog cx (fun _ -> log cx "noting lval '%a' type arguments: %a"
|
||||
Ast.sprintf_lval lval Ast.sprintf_app_args args);
|
||||
@ -907,7 +922,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
log cx "lval-base slot tyspec for %a = %s"
|
||||
Ast.sprintf_lval lval (tyspec_to_str (!tv));
|
||||
end;
|
||||
unify_slot slot (Some referent) tv
|
||||
unify_slot simplify slot (Some referent) tv
|
||||
|
||||
| _ ->
|
||||
let spec = (!(Hashtbl.find bindings referent)) in
|
||||
@ -929,7 +944,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
ref (TYSPEC_app (tv, args))
|
||||
| _ -> err None "bad lval / tyspec combination"
|
||||
in
|
||||
unify_tyvars (ref spec) tv
|
||||
unify_tyvars simplify (ref spec) tv
|
||||
end
|
||||
| Ast.LVAL_ext (base, comp) ->
|
||||
let base_ts = match comp with
|
||||
@ -950,19 +965,19 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
TYSPEC_tuple (Array.init (i + 1) init)
|
||||
|
||||
| Ast.COMP_atom atom ->
|
||||
unify_atom atom
|
||||
unify_atom simplify atom
|
||||
(ref (TYSPEC_resolved ([||], Ast.TY_int)));
|
||||
TYSPEC_collection tv
|
||||
in
|
||||
let base_tv = ref base_ts in
|
||||
unify_lval' base base_tv;
|
||||
unify_lval' simplify base base_tv;
|
||||
match !(resolve_tyvar base_tv) with
|
||||
TYSPEC_resolved (_, ty) ->
|
||||
unify_ty (project_type ty comp) tv
|
||||
unify_ty simplify (project_type ty comp) tv
|
||||
| _ ->
|
||||
()
|
||||
|
||||
and unify_lval (lval:Ast.lval) (tv:tyvar) : unit =
|
||||
and unify_lval (simplify:bool) (lval:Ast.lval) (tv:tyvar) : unit =
|
||||
let id = lval_base_id lval in
|
||||
(* Fetch lval with type components resolved. *)
|
||||
let lval = Hashtbl.find cx.ctxt_all_lvals id in
|
||||
@ -970,13 +985,13 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
"fetched resolved version of lval #%d = %a"
|
||||
(int_of_node id) Ast.sprintf_lval lval);
|
||||
Hashtbl.add lval_tyvars id tv;
|
||||
unify_lval' lval tv
|
||||
unify_lval' simplify lval tv
|
||||
|
||||
in
|
||||
let gen_atom_tvs atoms =
|
||||
let gen_atom_tv atom =
|
||||
let tv = ref TYSPEC_all in
|
||||
unify_atom atom tv;
|
||||
unify_atom true atom tv;
|
||||
tv
|
||||
in
|
||||
Array.map gen_atom_tv atoms
|
||||
@ -986,12 +1001,12 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
let check_callable out_tv callee args =
|
||||
let in_tvs = gen_atom_tvs args in
|
||||
let callee_tv = ref (TYSPEC_callable (out_tv, in_tvs)) in
|
||||
unify_lval callee callee_tv;
|
||||
unify_lval true callee callee_tv;
|
||||
in
|
||||
match stmt.node with
|
||||
Ast.STMT_spawn (out, _, callee, args) ->
|
||||
let out_tv = ref (TYSPEC_resolved ([||], Ast.TY_nil)) in
|
||||
unify_lval out (ref (TYSPEC_resolved ([||], Ast.TY_task)));
|
||||
unify_lval true out (ref (TYSPEC_resolved ([||], Ast.TY_task)));
|
||||
check_callable out_tv callee args
|
||||
|
||||
| Ast.STMT_init_rec (lval, fields, Some base) ->
|
||||
@ -999,59 +1014,59 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
let tvrec = ref (TYSPEC_record dct) in
|
||||
let add_field (ident, atom) =
|
||||
let tv = ref TYSPEC_all in
|
||||
unify_atom atom tv;
|
||||
unify_atom true atom tv;
|
||||
Hashtbl.add dct ident tv
|
||||
in
|
||||
Array.iter add_field fields;
|
||||
let tvbase = ref TYSPEC_all in
|
||||
unify_lval base tvbase;
|
||||
unify_tyvars tvrec tvbase;
|
||||
unify_lval lval tvrec
|
||||
unify_lval true base tvbase;
|
||||
unify_tyvars true tvrec tvbase;
|
||||
unify_lval true lval tvrec
|
||||
|
||||
| Ast.STMT_init_rec (lval, fields, None) ->
|
||||
let dct = Hashtbl.create 10 in
|
||||
let add_field (ident, atom) =
|
||||
let tv = ref TYSPEC_all in
|
||||
unify_atom atom tv;
|
||||
unify_atom true atom tv;
|
||||
Hashtbl.add dct ident tv
|
||||
in
|
||||
Array.iter add_field fields;
|
||||
unify_lval lval (ref (TYSPEC_record dct))
|
||||
unify_lval true lval (ref (TYSPEC_record dct))
|
||||
|
||||
| Ast.STMT_init_tup (lval, members) ->
|
||||
let member_to_tv atom =
|
||||
let tv = ref TYSPEC_all in
|
||||
unify_atom atom tv;
|
||||
unify_atom true atom tv;
|
||||
tv
|
||||
in
|
||||
let member_tvs = Array.map member_to_tv members in
|
||||
unify_lval lval (ref (TYSPEC_tuple member_tvs))
|
||||
unify_lval true lval (ref (TYSPEC_tuple member_tvs))
|
||||
|
||||
| Ast.STMT_init_vec (lval, atoms) ->
|
||||
let tv = ref TYSPEC_all in
|
||||
let unify_with_tv atom = unify_atom atom tv in
|
||||
let unify_with_tv atom = unify_atom true atom tv in
|
||||
Array.iter unify_with_tv atoms;
|
||||
unify_lval lval (ref (TYSPEC_vector tv))
|
||||
unify_lval true lval (ref (TYSPEC_vector tv))
|
||||
|
||||
| Ast.STMT_init_str (lval, _) ->
|
||||
unify_lval lval (ref (TYSPEC_resolved ([||], Ast.TY_str)))
|
||||
unify_lval true lval (ref (TYSPEC_resolved ([||], Ast.TY_str)))
|
||||
|
||||
| Ast.STMT_copy (lval, expr) ->
|
||||
let tv = ref TYSPEC_all in
|
||||
unify_expr expr tv;
|
||||
unify_lval lval tv
|
||||
unify_lval true lval tv
|
||||
|
||||
| Ast.STMT_copy_binop (lval, binop, at) ->
|
||||
let tv = ref TYSPEC_all in
|
||||
unify_expr (Ast.EXPR_binary (binop, Ast.ATOM_lval lval, at)) tv;
|
||||
unify_lval lval tv;
|
||||
unify_lval true lval tv;
|
||||
|
||||
| Ast.STMT_call (out, callee, args) ->
|
||||
let out_tv = ref TYSPEC_all in
|
||||
unify_lval out out_tv;
|
||||
unify_lval true out out_tv;
|
||||
check_callable out_tv callee args
|
||||
|
||||
| Ast.STMT_log atom -> unify_atom atom (ref TYSPEC_loggable)
|
||||
| Ast.STMT_log atom -> unify_atom true atom (ref TYSPEC_loggable)
|
||||
|
||||
| Ast.STMT_check_expr expr ->
|
||||
unify_expr expr (ref (TYSPEC_resolved ([||], Ast.TY_bool)))
|
||||
@ -1075,8 +1090,8 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
| Ast.STMT_put atom_opt ->
|
||||
begin
|
||||
match atom_opt with
|
||||
None -> unify_ty Ast.TY_nil (retval_tv())
|
||||
| Some atom -> unify_atom atom (retval_tv())
|
||||
None -> unify_ty true Ast.TY_nil (retval_tv())
|
||||
| Some atom -> unify_atom true atom (retval_tv())
|
||||
end
|
||||
|
||||
| Ast.STMT_be (callee, args) ->
|
||||
@ -1094,7 +1109,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
begin
|
||||
match atom_opt with
|
||||
None -> residue := tv :: (!residue);
|
||||
| Some atom -> unify_atom atom tv
|
||||
| Some atom -> unify_atom true atom tv
|
||||
end;
|
||||
tv
|
||||
in
|
||||
@ -1105,14 +1120,14 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
let arg_residue_tvs = Array.of_list (List.rev (!residue)) in
|
||||
let callee_tv = ref (TYSPEC_callable (out_tv, in_tvs)) in
|
||||
let bound_tv = ref (TYSPEC_callable (out_tv, arg_residue_tvs)) in
|
||||
unify_lval callee callee_tv;
|
||||
unify_lval bound bound_tv
|
||||
unify_lval true callee callee_tv;
|
||||
unify_lval true bound bound_tv
|
||||
|
||||
| Ast.STMT_for_each fe ->
|
||||
let out_tv = ref TYSPEC_all in
|
||||
let (si, _) = fe.Ast.for_each_slot in
|
||||
let (callee, args) = fe.Ast.for_each_call in
|
||||
unify_slot si.node (Some si.id) out_tv;
|
||||
unify_slot true si.node (Some si.id) out_tv;
|
||||
check_callable out_tv callee args
|
||||
|
||||
| Ast.STMT_for fo ->
|
||||
@ -1120,13 +1135,13 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
let seq_tv = ref (TYSPEC_collection mem_tv) in
|
||||
let (si, _) = fo.Ast.for_slot in
|
||||
let (_, seq) = fo.Ast.for_seq in
|
||||
unify_lval seq seq_tv;
|
||||
unify_slot si.node (Some si.id) mem_tv
|
||||
unify_lval true seq seq_tv;
|
||||
unify_slot true si.node (Some si.id) mem_tv
|
||||
|
||||
| Ast.STMT_alt_tag
|
||||
{ Ast.alt_tag_lval = lval; Ast.alt_tag_arms = arms } ->
|
||||
let lval_tv = ref TYSPEC_all in
|
||||
unify_lval lval lval_tv;
|
||||
unify_lval true lval lval_tv;
|
||||
Array.iter (fun _ -> push_pat_tv lval_tv) arms
|
||||
|
||||
(* FIXME (issue #52): plenty more to handle here. *)
|
||||
@ -1153,7 +1168,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
let enter_fn fn retspec =
|
||||
let out = fn.Ast.fn_output_slot in
|
||||
push_retval_tv (ref retspec);
|
||||
unify_slot out.node (Some out.id) (retval_tv())
|
||||
unify_slot true out.node (Some out.id) (retval_tv())
|
||||
in
|
||||
|
||||
let visit_obj_fn_pre obj ident fn =
|
||||
@ -1220,12 +1235,12 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
let visit_pat_pre (pat:Ast.pat) : unit =
|
||||
let expected = pat_tv() in
|
||||
match pat with
|
||||
Ast.PAT_lit lit -> unify_lit lit expected
|
||||
Ast.PAT_lit lit -> unify_lit true lit expected
|
||||
|
||||
| Ast.PAT_tag (lval, _) ->
|
||||
let expect ty =
|
||||
let tv = ref TYSPEC_all in
|
||||
unify_ty ty tv;
|
||||
unify_ty true ty tv;
|
||||
push_pat_tv tv;
|
||||
in
|
||||
|
||||
@ -1237,7 +1252,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
||||
* exactly to that function type, rebuilt under any latent type
|
||||
* parameters applied in the lval. *)
|
||||
let lval_tv = ref TYSPEC_all in
|
||||
unify_lval lval lval_tv;
|
||||
unify_lval true lval lval_tv;
|
||||
let tag_ctor_ty =
|
||||
match !(resolve_tyvar lval_tv) with
|
||||
TYSPEC_resolved (_, ty) -> ty
|
||||
@ -1249,13 +1264,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_tv = ref TYSPEC_all in
|
||||
unify_ty tag_ty tag_tv;
|
||||
unify_tyvars expected tag_tv;
|
||||
unify_ty true tag_ty tag_tv;
|
||||
unify_tyvars true expected tag_tv;
|
||||
List.iter expect
|
||||
(List.rev (Array.to_list tag_ty_tup));
|
||||
|
||||
| Ast.PAT_slot (sloti, _) ->
|
||||
unify_slot sloti.node (Some sloti.id) expected
|
||||
unify_slot true sloti.node (Some sloti.id) expected
|
||||
|
||||
| Ast.PAT_wild -> ()
|
||||
in
|
||||
|
Loading…
Reference in New Issue
Block a user