Add a COMP_deref to lvals for explicit-derefs, modify typechecker to implicitly deref in only *some* contexts.
This commit is contained in:
parent
8e4a10790f
commit
0ac6be85a9
|
@ -337,6 +337,7 @@ and lit =
|
|||
and lval_component =
|
||||
COMP_named of name_component
|
||||
| COMP_atom of atom
|
||||
| COMP_deref
|
||||
|
||||
|
||||
(* identifying the name_base here is sufficient to identify the full lval *)
|
||||
|
@ -862,24 +863,21 @@ and fmt_atom_opts (ff:Format.formatter) (az:(atom option) array) : unit =
|
|||
az;
|
||||
fmt ff ")"
|
||||
|
||||
and fmt_lval_component (ff:Format.formatter) (lvc:lval_component) : unit =
|
||||
match lvc with
|
||||
COMP_named nc -> fmt_name_component ff nc
|
||||
| COMP_atom a ->
|
||||
begin
|
||||
fmt ff "(";
|
||||
fmt_atom ff a;
|
||||
fmt ff ")"
|
||||
end
|
||||
|
||||
and fmt_lval (ff:Format.formatter) (l:lval) : unit =
|
||||
match l with
|
||||
LVAL_base nbi -> fmt_name_base ff nbi.node
|
||||
| LVAL_ext (lv, lvc) ->
|
||||
begin
|
||||
match lvc with
|
||||
COMP_named nc ->
|
||||
fmt_lval ff lv;
|
||||
fmt ff ".";
|
||||
fmt_lval_component ff lvc
|
||||
fmt_name_component ff nc
|
||||
| COMP_atom a ->
|
||||
fmt_bracketed "(" ")" fmt_atom ff a;
|
||||
| COMP_deref ->
|
||||
fmt ff "*";
|
||||
fmt_lval ff lv
|
||||
end
|
||||
|
||||
and fmt_stmt (ff:Format.formatter) (s:stmt) : unit =
|
||||
|
@ -1336,8 +1334,8 @@ and fmt_crate (ff:Format.formatter) (c:crate) : unit =
|
|||
|
||||
let sprintf_expr = sprintf_fmt fmt_expr;;
|
||||
let sprintf_name = sprintf_fmt fmt_name;;
|
||||
let sprintf_name_component = sprintf_fmt fmt_name_component;;
|
||||
let sprintf_lval = sprintf_fmt fmt_lval;;
|
||||
let sprintf_lval_component = sprintf_fmt fmt_lval_component;;
|
||||
let sprintf_atom = sprintf_fmt fmt_atom;;
|
||||
let sprintf_slot = sprintf_fmt fmt_slot;;
|
||||
let sprintf_slot_key = sprintf_fmt fmt_slot_key;;
|
||||
|
|
|
@ -636,7 +636,8 @@ let type_resolving_visitor
|
|||
Ast.LVAL_ext (base, ext) ->
|
||||
let ext =
|
||||
match ext with
|
||||
Ast.COMP_named (Ast.COMP_ident _)
|
||||
Ast.COMP_deref
|
||||
| Ast.COMP_named (Ast.COMP_ident _)
|
||||
| Ast.COMP_named (Ast.COMP_idx _)
|
||||
| Ast.COMP_atom (Ast.ATOM_literal _) -> ext
|
||||
| Ast.COMP_atom (Ast.ATOM_lval lv) ->
|
||||
|
|
|
@ -557,7 +557,8 @@ let rec lval_slots (cx:ctxt) (lv:Ast.lval) : node_id array =
|
|||
if referent_is_slot cx referent
|
||||
then [| referent |]
|
||||
else [| |]
|
||||
| Ast.LVAL_ext (lv, Ast.COMP_named _) -> lval_slots cx lv
|
||||
| Ast.LVAL_ext (lv, Ast.COMP_named _)
|
||||
| Ast.LVAL_ext (lv, Ast.COMP_deref) -> lval_slots cx lv
|
||||
| Ast.LVAL_ext (lv, Ast.COMP_atom a) ->
|
||||
Array.append (lval_slots cx lv) (atom_slots cx a)
|
||||
|
||||
|
@ -1074,11 +1075,11 @@ let rec simplified_ty (t:Ast.ty) : Ast.ty =
|
|||
| _ -> t
|
||||
;;
|
||||
|
||||
let project_type
|
||||
let rec project_type
|
||||
(base_ty:Ast.ty)
|
||||
(comp:Ast.lval_component)
|
||||
: Ast.ty =
|
||||
match (simplified_ty base_ty, comp) with
|
||||
match (base_ty, comp) with
|
||||
(Ast.TY_rec elts, Ast.COMP_named (Ast.COMP_ident id)) ->
|
||||
begin
|
||||
match atab_search elts id with
|
||||
|
@ -1096,10 +1097,30 @@ let project_type
|
|||
| (Ast.TY_obj (_, fns), Ast.COMP_named (Ast.COMP_ident id)) ->
|
||||
(Ast.TY_fn (Hashtbl.find fns id))
|
||||
|
||||
| (Ast.TY_exterior t, Ast.COMP_deref) -> t
|
||||
|
||||
(* Exterior, mutable and constrained are transparent to the
|
||||
* other lval-ext forms: x.y and x.(y).
|
||||
*)
|
||||
| (Ast.TY_exterior t, _)
|
||||
| (Ast.TY_mutable t, _)
|
||||
| (Ast.TY_constrained (t, _), _) -> project_type t comp
|
||||
|
||||
| (_,_) ->
|
||||
bug ()
|
||||
"project_ty: bad lval-ext: %a indexed by %a"
|
||||
Ast.sprintf_ty base_ty Ast.sprintf_lval_component comp
|
||||
"project_ty: bad lval-ext: %s"
|
||||
(match comp with
|
||||
Ast.COMP_atom at ->
|
||||
Printf.sprintf "%a.(%a)"
|
||||
Ast.sprintf_ty base_ty
|
||||
Ast.sprintf_atom at
|
||||
| Ast.COMP_named nc ->
|
||||
Printf.sprintf "%a.%a"
|
||||
Ast.sprintf_ty base_ty
|
||||
Ast.sprintf_name_component nc
|
||||
| Ast.COMP_deref ->
|
||||
Printf.sprintf "*(%a)"
|
||||
Ast.sprintf_ty base_ty)
|
||||
;;
|
||||
|
||||
let exports_permit (view:Ast.mod_view) (ident:Ast.ident) : bool =
|
||||
|
@ -1129,8 +1150,8 @@ let rec lval_item (cx:ctxt) (lval:Ast.lval) : Ast.mod_item =
|
|||
| Ast.COMP_named (Ast.COMP_app (i, args)) -> (i, args)
|
||||
| _ ->
|
||||
bug ()
|
||||
"unhandled lval-component '%a' in Semant.lval_item"
|
||||
Ast.sprintf_lval_component comp
|
||||
"unhandled lval-component in '%a' in lval_item"
|
||||
Ast.sprintf_lval lval
|
||||
in
|
||||
match htab_search items i with
|
||||
| Some sub when exports_permit view i ->
|
||||
|
|
|
@ -5,6 +5,7 @@ type tyspec =
|
|||
TYSPEC_equiv of tyvar
|
||||
| TYSPEC_all
|
||||
| TYSPEC_resolved of (Ast.ty_param array) * Ast.ty
|
||||
| TYSPEC_exterior of tyvar (* @ of some t *)
|
||||
| TYSPEC_callable of (tyvar * tyvar array) (* out, ins *)
|
||||
| TYSPEC_collection of tyvar (* vec or str *)
|
||||
| TYSPEC_comparable (* comparable with = and != *)
|
||||
|
@ -105,6 +106,10 @@ let rec tyspec_to_str (ts:tyspec) : string =
|
|||
| TYSPEC_equiv tv ->
|
||||
fmt_tyspec ff (!tv)
|
||||
|
||||
| TYSPEC_exterior tv ->
|
||||
fmt ff "@";
|
||||
fmt_tyspec ff (!tv)
|
||||
|
||||
| TYSPEC_callable (out, ins) ->
|
||||
fmt_obb ff;
|
||||
fmt ff "callable fn(";
|
||||
|
@ -198,15 +203,16 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
let visitor (cx:ctxt) (inner:Walk.visitor) : Walk.visitor =
|
||||
|
||||
let rec unify_slot
|
||||
(auto_deref: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 auto_deref (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 auto_deref ty tv
|
||||
|
||||
and check_sane_tyvar tv =
|
||||
match !tv with
|
||||
|
@ -214,24 +220,25 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
bug () "named-type in type checker"
|
||||
| _ -> ()
|
||||
|
||||
and unify_tyvars (av:tyvar) (bv:tyvar) : unit =
|
||||
and unify_tyvars (auto_deref:bool) (av:tyvar) (bv:tyvar) : unit =
|
||||
let dstr = if auto_deref then " w/ auto-deref" else "" in
|
||||
iflog cx (fun _ ->
|
||||
log cx "unifying types:";
|
||||
log cx "unifying types%s:" dstr;
|
||||
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' auto_deref av bv;
|
||||
|
||||
iflog cx (fun _ ->
|
||||
log cx "unified types:";
|
||||
log cx "unified types%s:" dstr;
|
||||
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 =
|
||||
and unify_tyvars' (auto_deref:bool) (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)
|
||||
|
@ -242,7 +249,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 auto_deref (Hashtbl.find c ident) tv_a
|
||||
else Hashtbl.add c ident tv_a
|
||||
in
|
||||
Hashtbl.iter (Hashtbl.add c) b;
|
||||
|
@ -261,7 +268,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
in
|
||||
|
||||
let check_entry ident tv =
|
||||
unify_ty (find_ty ident) tv
|
||||
unify_ty auto_deref (find_ty ident) tv
|
||||
in
|
||||
Hashtbl.iter check_entry dct
|
||||
in
|
||||
|
@ -272,7 +279,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 auto_deref (Ast.TY_fn fn) tv
|
||||
in
|
||||
Hashtbl.iter check_entry dct
|
||||
in
|
||||
|
@ -283,7 +290,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
: 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 a, b | b, Ast.TY_exterior a when auto_deref ->
|
||||
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)
|
||||
|
@ -304,16 +311,22 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
| Ast.TY_fn _ | Ast.TY_obj _
|
||||
| Ast.TY_param _ | Ast.TY_native _ | Ast.TY_type -> false
|
||||
| Ast.TY_named _ -> bug () "unexpected named type"
|
||||
| Ast.TY_exterior ty
|
||||
| Ast.TY_mutable ty
|
||||
| Ast.TY_constrained (ty, _) ->
|
||||
is_comparable_or_ordered comparable ty
|
||||
| Ast.TY_exterior ty ->
|
||||
if auto_deref
|
||||
then
|
||||
is_comparable_or_ordered comparable ty
|
||||
else
|
||||
false
|
||||
in
|
||||
|
||||
let rec floating (ty:Ast.ty) : bool =
|
||||
match ty with
|
||||
Ast.TY_mach TY_f32 | Ast.TY_mach TY_f64 -> true
|
||||
| Ast.TY_exterior ty | Ast.TY_mutable ty -> floating ty
|
||||
| Ast.TY_mutable ty -> floating ty
|
||||
| Ast.TY_exterior ty when auto_deref -> floating ty
|
||||
| _ -> false
|
||||
in
|
||||
|
||||
|
@ -324,7 +337,8 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
| Ast.TY_mach TY_i16 | Ast.TY_mach TY_i32
|
||||
| Ast.TY_mach TY_i64 ->
|
||||
true
|
||||
| Ast.TY_exterior ty | Ast.TY_mutable ty -> integral ty
|
||||
| Ast.TY_mutable ty -> integral ty
|
||||
| Ast.TY_exterior ty when auto_deref -> integral ty
|
||||
| _ -> false
|
||||
in
|
||||
|
||||
|
@ -334,7 +348,8 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
match ty with
|
||||
Ast.TY_str -> true
|
||||
| Ast.TY_vec _ -> true
|
||||
| Ast.TY_exterior ty | Ast.TY_mutable ty -> plusable ty
|
||||
| Ast.TY_mutable ty -> plusable ty
|
||||
| Ast.TY_exterior ty when auto_deref -> plusable ty
|
||||
| _ -> numeric ty
|
||||
in
|
||||
|
||||
|
@ -344,7 +359,8 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
| 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
|
||||
-> true
|
||||
| Ast.TY_exterior ty | Ast.TY_mutable ty -> loggable ty
|
||||
| Ast.TY_mutable ty -> loggable ty
|
||||
| Ast.TY_exterior ty when auto_deref -> loggable ty
|
||||
| _ -> false
|
||||
in
|
||||
|
||||
|
@ -355,6 +371,24 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
|
||||
| (TYSPEC_all, other) | (other, TYSPEC_all) -> other
|
||||
|
||||
(* exterior *)
|
||||
|
||||
| (TYSPEC_exterior a',
|
||||
TYSPEC_resolved (_, Ast.TY_exterior _)) ->
|
||||
unify_tyvars auto_deref a' b; !b
|
||||
|
||||
| (TYSPEC_resolved (_, Ast.TY_exterior _),
|
||||
TYSPEC_exterior b') ->
|
||||
unify_tyvars auto_deref a b'; !b
|
||||
|
||||
| (TYSPEC_exterior a', _) when auto_deref
|
||||
-> unify_tyvars auto_deref a' b; !a
|
||||
| (_, TYSPEC_exterior b') when auto_deref
|
||||
-> unify_tyvars auto_deref a b'; !b
|
||||
|
||||
| (_, TYSPEC_exterior _)
|
||||
| (TYSPEC_exterior _, _) -> fail()
|
||||
|
||||
(* resolved *)
|
||||
|
||||
| (TYSPEC_resolved (params_a, ty_a),
|
||||
|
@ -368,7 +402,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 false in_slot None in_tvs.(i)
|
||||
in
|
||||
let rec unify ty =
|
||||
match ty with
|
||||
|
@ -380,10 +414,11 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
then
|
||||
fail ()
|
||||
else
|
||||
unify_slot out_slot None out_tv;
|
||||
unify_slot false out_slot None out_tv;
|
||||
Array.iteri unify_in_slot in_slots;
|
||||
ty
|
||||
| Ast.TY_exterior ty -> Ast.TY_exterior (unify ty)
|
||||
| Ast.TY_exterior ty when auto_deref
|
||||
-> Ast.TY_exterior (unify ty)
|
||||
| Ast.TY_mutable ty -> Ast.TY_mutable (unify ty)
|
||||
| _ -> fail ()
|
||||
in
|
||||
|
@ -393,9 +428,11 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
| (TYSPEC_collection tv, TYSPEC_resolved (params, ty)) ->
|
||||
let rec unify ty =
|
||||
match ty with
|
||||
Ast.TY_vec ty -> unify_ty ty tv; ty
|
||||
| Ast.TY_str -> unify_ty (Ast.TY_mach TY_u8) tv; ty
|
||||
| Ast.TY_exterior ty -> Ast.TY_exterior (unify ty)
|
||||
Ast.TY_vec ty -> unify_ty auto_deref ty tv; ty
|
||||
| Ast.TY_str ->
|
||||
unify_ty auto_deref (Ast.TY_mach TY_u8) tv; ty
|
||||
| Ast.TY_exterior ty
|
||||
when auto_deref -> Ast.TY_exterior (unify ty)
|
||||
| Ast.TY_mutable ty -> Ast.TY_mutable (unify ty)
|
||||
| _ -> fail ()
|
||||
in
|
||||
|
@ -421,7 +458,8 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
| Ast.TY_obj (_, fns) ->
|
||||
unify_dict_with_obj_fns dct fns;
|
||||
ty
|
||||
| Ast.TY_exterior ty -> Ast.TY_exterior (unify ty)
|
||||
| Ast.TY_exterior ty
|
||||
when auto_deref -> Ast.TY_exterior (unify ty)
|
||||
| Ast.TY_mutable ty -> Ast.TY_mutable (unify ty)
|
||||
| _ -> fail ()
|
||||
in
|
||||
|
@ -452,7 +490,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 auto_deref ty tv;
|
||||
TYSPEC_resolved ([| |], ty)
|
||||
|
||||
| (TYSPEC_resolved (params, ty), TYSPEC_record dct)
|
||||
|
@ -462,7 +500,8 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
Ast.TY_rec fields ->
|
||||
unify_dict_with_record_fields dct fields;
|
||||
ty
|
||||
| Ast.TY_exterior ty -> Ast.TY_exterior (unify ty)
|
||||
| Ast.TY_exterior ty
|
||||
when auto_deref -> Ast.TY_exterior (unify ty)
|
||||
| Ast.TY_mutable ty -> Ast.TY_mutable (unify ty)
|
||||
| _ -> fail ()
|
||||
in
|
||||
|
@ -477,11 +516,12 @@ 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 auto_deref (elem_tys.(i)) tv
|
||||
in
|
||||
Array.iteri check_elem tvs;
|
||||
ty
|
||||
| Ast.TY_exterior ty -> Ast.TY_exterior (unify ty)
|
||||
| Ast.TY_exterior ty
|
||||
when auto_deref -> Ast.TY_exterior (unify ty)
|
||||
| Ast.TY_mutable ty -> Ast.TY_mutable (unify ty)
|
||||
| _ -> fail ()
|
||||
in
|
||||
|
@ -491,8 +531,9 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
| (TYSPEC_vector tv, TYSPEC_resolved (params, ty)) ->
|
||||
let rec unify ty =
|
||||
match ty with
|
||||
Ast.TY_vec ty' -> unify_ty ty' tv; ty
|
||||
| Ast.TY_exterior ty -> Ast.TY_exterior (unify ty)
|
||||
Ast.TY_vec ty' -> unify_ty auto_deref ty' tv; ty
|
||||
| Ast.TY_exterior ty when auto_deref ->
|
||||
Ast.TY_exterior (unify ty)
|
||||
| Ast.TY_mutable ty -> Ast.TY_mutable (unify ty)
|
||||
| _ -> fail ()
|
||||
in
|
||||
|
@ -502,9 +543,9 @@ 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 false 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 false a_in_tv b_in_tvs.(i)
|
||||
in
|
||||
Array.iteri check_in_tv a_in_tvs;
|
||||
TYSPEC_callable (a_out_tv, a_in_tvs)
|
||||
|
@ -537,7 +578,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
(* collection *)
|
||||
|
||||
| (TYSPEC_collection av, TYSPEC_collection bv) ->
|
||||
unify_tyvars av bv;
|
||||
unify_tyvars auto_deref av bv;
|
||||
TYSPEC_collection av
|
||||
|
||||
| (TYSPEC_collection av, TYSPEC_comparable)
|
||||
|
@ -566,7 +607,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 auto_deref av bv;
|
||||
TYSPEC_vector av
|
||||
|
||||
(* comparable *)
|
||||
|
@ -735,7 +776,7 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
then fail()
|
||||
else
|
||||
begin
|
||||
unify_tyvars tv_a tv_b;
|
||||
unify_tyvars auto_deref tv_a tv_b;
|
||||
TYSPEC_app (tv_a, args_a)
|
||||
end
|
||||
|
||||
|
@ -768,7 +809,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
|
||||
|
@ -780,7 +821,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
|
||||
|
@ -788,18 +829,19 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
b := TYSPEC_equiv c
|
||||
|
||||
and unify_ty_parametric
|
||||
(auto_deref:bool)
|
||||
(ty:Ast.ty)
|
||||
(tps:Ast.ty_param array)
|
||||
(tv:tyvar)
|
||||
: unit =
|
||||
unify_tyvars (ref (TYSPEC_resolved (tps, ty))) tv
|
||||
unify_tyvars auto_deref (ref (TYSPEC_resolved (tps, ty))) tv
|
||||
|
||||
and unify_ty (ty:Ast.ty) (tv:tyvar) : unit =
|
||||
unify_ty_parametric ty [||] tv
|
||||
and unify_ty (auto_deref:bool) (ty:Ast.ty) (tv:tyvar) : unit =
|
||||
unify_ty_parametric auto_deref ty [||] tv
|
||||
|
||||
in
|
||||
|
||||
let rec unify_lit (lit:Ast.lit) (tv:tyvar) : unit =
|
||||
let rec unify_lit (auto_deref:bool) (lit:Ast.lit) (tv:tyvar) : unit =
|
||||
let ty =
|
||||
match lit with
|
||||
Ast.LIT_nil -> Ast.TY_nil
|
||||
|
@ -809,16 +851,16 @@ 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 auto_deref ty tv
|
||||
|
||||
and unify_atom (atom:Ast.atom) (tv:tyvar) : unit =
|
||||
and unify_atom (auto_deref:bool) (atom:Ast.atom) (tv:tyvar) : unit =
|
||||
match atom with
|
||||
Ast.ATOM_literal { node = literal; id = _ } ->
|
||||
unify_lit literal tv
|
||||
unify_lit auto_deref literal tv
|
||||
| Ast.ATOM_lval lval ->
|
||||
unify_lval lval tv
|
||||
unify_lval auto_deref lval tv
|
||||
|
||||
and unify_expr (expr:Ast.expr) (tv:tyvar) : unit =
|
||||
and unify_expr (auto_deref:bool) (expr:Ast.expr) (tv:tyvar) : unit =
|
||||
match expr with
|
||||
Ast.EXPR_binary (binop, lhs, rhs) ->
|
||||
let binop_sig = match binop with
|
||||
|
@ -849,64 +891,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 auto_deref atom tv
|
||||
|
||||
and unify_lval' (lval:Ast.lval) (tv:tyvar) : unit =
|
||||
and unify_lval' (auto_deref: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);
|
||||
|
@ -928,7 +970,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 auto_deref slot (Some referent) tv
|
||||
|
||||
| _ ->
|
||||
let spec = (!(Hashtbl.find bindings referent)) in
|
||||
|
@ -950,7 +992,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 auto_deref (ref spec) tv
|
||||
end
|
||||
| Ast.LVAL_ext (base, comp) ->
|
||||
let base_ts = match comp with
|
||||
|
@ -971,19 +1013,22 @@ 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 true atom
|
||||
(ref (TYSPEC_resolved ([||], Ast.TY_int)));
|
||||
TYSPEC_collection tv
|
||||
|
||||
| Ast.COMP_deref ->
|
||||
TYSPEC_exterior tv
|
||||
in
|
||||
let base_tv = ref base_ts in
|
||||
unify_lval' base base_tv;
|
||||
unify_lval' auto_deref base base_tv;
|
||||
match !(resolve_tyvar base_tv) with
|
||||
TYSPEC_resolved (_, ty) ->
|
||||
unify_ty (project_type ty comp) tv
|
||||
unify_ty auto_deref (project_type ty comp) tv
|
||||
| _ ->
|
||||
()
|
||||
|
||||
and unify_lval (lval:Ast.lval) (tv:tyvar) : unit =
|
||||
and unify_lval (auto_deref: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
|
||||
|
@ -991,13 +1036,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' auto_deref 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 false atom tv;
|
||||
tv
|
||||
in
|
||||
Array.map gen_atom_tv atoms
|
||||
|
@ -1007,12 +1052,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 false 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) ->
|
||||
|
@ -1020,62 +1065,63 @@ 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_expr false expr tv;
|
||||
unify_lval false 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_expr false
|
||||
(Ast.EXPR_binary (binop, Ast.ATOM_lval lval, at)) tv;
|
||||
unify_lval false lval tv;
|
||||
|
||||
| Ast.STMT_call (out, callee, args) ->
|
||||
let out_tv = ref TYSPEC_all in
|
||||
unify_lval out out_tv;
|
||||
unify_lval false 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)))
|
||||
unify_expr true expr (ref (TYSPEC_resolved ([||], Ast.TY_bool)))
|
||||
|
||||
| Ast.STMT_check (_, check_calls) ->
|
||||
let out_tv = ref (TYSPEC_resolved ([||], Ast.TY_bool)) in
|
||||
|
@ -1084,11 +1130,14 @@ let process_crate (cx:ctxt) (crate:Ast.crate) : unit =
|
|||
check_callable out_tv callee args)
|
||||
check_calls
|
||||
|
||||
| Ast.STMT_while { Ast.while_lval = (_, expr); Ast.while_body = _ } ->
|
||||
unify_expr expr (ref (TYSPEC_resolved ([||], Ast.TY_bool)))
|
||||
| Ast.STMT_while { Ast.while_lval = (_, expr);
|
||||
Ast.while_body = _ } ->
|
||||
unify_expr true
|
||||
expr (ref (TYSPEC_resolved ([||], Ast.TY_bool)))
|
||||
|
||||
| Ast.STMT_if { Ast.if_test = if_test } ->
|
||||
unify_expr if_test (ref (TYSPEC_resolved ([||], Ast.TY_bool)));
|
||||
unify_expr true
|
||||
if_test (ref (TYSPEC_resolved ([||], Ast.TY_bool)));
|
||||
|
||||
| Ast.STMT_decl _ -> ()
|
||||
|
||||
|
@ -1096,8 +1145,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 false Ast.TY_nil (retval_tv())
|
||||
| Some atom -> unify_atom false atom (retval_tv())
|
||||
end
|
||||
|
||||
| Ast.STMT_be (callee, args) ->
|
||||
|
@ -1115,7 +1164,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 false atom tv
|
||||
end;
|
||||
tv
|
||||
in
|
||||
|
@ -1126,14 +1175,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 false 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 false si.node (Some si.id) out_tv;
|
||||
check_callable out_tv callee args
|
||||
|
||||
| Ast.STMT_for fo ->
|
||||
|
@ -1141,13 +1190,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 false 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. *)
|
||||
|
@ -1174,7 +1223,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 false out.node (Some out.id) (retval_tv())
|
||||
in
|
||||
|
||||
let visit_obj_fn_pre obj ident fn =
|
||||
|
@ -1241,12 +1290,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 false ty tv;
|
||||
push_pat_tv tv;
|
||||
in
|
||||
|
||||
|
@ -1258,7 +1307,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 false lval lval_tv;
|
||||
let tag_ctor_ty =
|
||||
match !(resolve_tyvar lval_tv) with
|
||||
TYSPEC_resolved (_, ty) -> ty
|
||||
|
@ -1270,13 +1319,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 false tag_ty tag_tv;
|
||||
unify_tyvars false 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 false sloti.node (Some sloti.id) expected
|
||||
|
||||
| Ast.PAT_wild -> ()
|
||||
in
|
||||
|
|
Loading…
Reference in New Issue