From 0ac6be85a9c1527b0943a3b2751a955f6aa71624 Mon Sep 17 00:00:00 2001 From: Graydon Hoare Date: Wed, 30 Jun 2010 12:39:11 -0700 Subject: [PATCH] Add a COMP_deref to lvals for explicit-derefs, modify typechecker to implicitly deref in only *some* contexts. --- src/boot/fe/ast.ml | 26 ++-- src/boot/me/resolve.ml | 3 +- src/boot/me/semant.ml | 35 ++++- src/boot/me/type.ml | 309 ++++++++++++++++++++++++----------------- 4 files changed, 221 insertions(+), 152 deletions(-) diff --git a/src/boot/fe/ast.ml b/src/boot/fe/ast.ml index 0c12d405afc..7edfd432e4d 100644 --- a/src/boot/fe/ast.ml +++ b/src/boot/fe/ast.ml @@ -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 - fmt_lval ff lv; - fmt ff "."; - fmt_lval_component ff lvc + match lvc with + COMP_named nc -> + fmt_lval ff lv; + fmt ff "."; + 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;; diff --git a/src/boot/me/resolve.ml b/src/boot/me/resolve.ml index 1f563c76c63..2e422d1e82a 100644 --- a/src/boot/me/resolve.ml +++ b/src/boot/me/resolve.ml @@ -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) -> diff --git a/src/boot/me/semant.ml b/src/boot/me/semant.ml index c7536fa65bf..19ef774da6b 100644 --- a/src/boot/me/semant.ml +++ b/src/boot/me/semant.ml @@ -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 -> diff --git a/src/boot/me/type.ml b/src/boot/me/type.ml index 0c39ab8044a..4969d86e88b 100644 --- a/src/boot/me/type.ml +++ b/src/boot/me/type.ml @@ -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 = - 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 (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%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 "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:" 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