Stop using project_lval_ty_from_slot for lval_ty; cover residual un-caught cases in type.ml.
This commit is contained in:
parent
ac228a59ce
commit
62b69503d5
2 changed files with 19 additions and 15 deletions
|
@ -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 =
|
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
|
match htab_search cx.ctxt_all_lval_types (lval_base_id lval) with
|
||||||
Some t -> t
|
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 =
|
let lval_is_static (cx:ctxt) (lval:Ast.lval) : bool =
|
||||||
|
|
|
@ -509,7 +509,8 @@ let check_stmt (cx:Semant.ctxt) : (fn_ctx -> Ast.stmt -> unit) =
|
||||||
end;
|
end;
|
||||||
if n_boxes > 1 then
|
if n_boxes > 1 then
|
||||||
(* TODO: allow more than one level of automatic dereference *)
|
(* 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";
|
implemented; please add explicit dereference operators";
|
||||||
Hashtbl.replace cx.Semant.ctxt_auto_deref_lval lval_id (n_boxes > 0);
|
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_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) ->
|
| Ast.STMT_new_chan (dst, Some port) ->
|
||||||
let ty = Ast.TY_chan (demand_port (check_lval port)) in
|
let ty = Ast.TY_chan (demand_port (check_lval port)) in
|
||||||
infer_lval ty dst
|
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) ->
|
| Ast.STMT_new_box (dst, mut, src) ->
|
||||||
let ty = Ast.TY_box (maybe_mutable mut (check_atom src)) in
|
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
|
let value_ty = demand_chan (check_lval chan) in
|
||||||
infer_lval ~mut:Ast.MUT_immutable value_ty value
|
infer_lval ~mut:Ast.MUT_immutable value_ty value
|
||||||
|
|
||||||
| Ast.STMT_log _ | Ast.STMT_note _ | Ast.STMT_prove _ ->
|
| Ast.STMT_log x | Ast.STMT_note x ->
|
||||||
() (* always well-typed *)
|
(* 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
|
| Ast.STMT_check (_, calls) -> check_check_calls calls
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue