diff --git a/src/boot/me/semant.ml b/src/boot/me/semant.ml index ef73753df5d..8196d568a50 100644 --- a/src/boot/me/semant.ml +++ b/src/boot/me/semant.ml @@ -1206,18 +1206,10 @@ let rec project_lval_ty_from_slot (cx:ctxt) (lval:Ast.lval) : Ast.ty = let lval_ty (cx:ctxt) (lval:Ast.lval) : Ast.ty = - (* - FIXME: The correct definition of this function is just: - - Hashtbl.find cx.ctxt_all_lval_types (lval_base_id lval) - - However, since the typechecker is not presently handling - every stmt, we have a fallback mode to "pick out the slot - type and hope for the best". - *) match htab_search cx.ctxt_all_lval_types (lval_base_id lval) with Some t -> t - | None -> project_lval_ty_from_slot cx lval + | None -> bugi cx (lval_base_id lval) "no type for lval %a" + Ast.sprintf_lval lval ;; let lval_is_static (cx:ctxt) (lval:Ast.lval) : bool = diff --git a/src/boot/me/type.ml b/src/boot/me/type.ml index 0cc6fdd7c92..9d74959a7ac 100644 --- a/src/boot/me/type.ml +++ b/src/boot/me/type.ml @@ -509,7 +509,8 @@ let check_stmt (cx:Semant.ctxt) : (fn_ctx -> Ast.stmt -> unit) = end; if n_boxes > 1 then (* TODO: allow more than one level of automatic dereference *) - Common.err None "sorry, only one level of automatic dereference is \ + Common.unimpl (Some (Semant.lval_base_id lval)) + "sorry, only one level of automatic dereference is \ implemented; please add explicit dereference operators"; Hashtbl.replace cx.Semant.ctxt_auto_deref_lval lval_id (n_boxes > 0); @@ -690,13 +691,19 @@ let check_stmt (cx:Semant.ctxt) : (fn_ctx -> Ast.stmt -> unit) = | Ast.STMT_new_str (dst, _) -> infer_lval Ast.TY_str dst - | Ast.STMT_new_port _ -> () (* we can't actually typecheck this *) + | Ast.STMT_new_port dst -> + (* we can't actually typecheck this *) + ignore (check_lval dst); + () | Ast.STMT_new_chan (dst, Some port) -> let ty = Ast.TY_chan (demand_port (check_lval port)) in infer_lval ty dst - | Ast.STMT_new_chan (_, None) -> () (* can't check this either *) + | Ast.STMT_new_chan (dst, None) -> + (* can't check this either *) + ignore (check_lval dst); + () | Ast.STMT_new_box (dst, mut, src) -> let ty = Ast.TY_box (maybe_mutable mut (check_atom src)) in @@ -818,8 +825,13 @@ let check_stmt (cx:Semant.ctxt) : (fn_ctx -> Ast.stmt -> unit) = let value_ty = demand_chan (check_lval chan) in infer_lval ~mut:Ast.MUT_immutable value_ty value - | Ast.STMT_log _ | Ast.STMT_note _ | Ast.STMT_prove _ -> - () (* always well-typed *) + | Ast.STMT_log x | Ast.STMT_note x -> + (* always well-typed, just record type in passing. *) + ignore (check_atom x) + + | Ast.STMT_prove _ -> + (* always well-typed, static. Ignore. *) + () | Ast.STMT_check (_, calls) -> check_check_calls calls