Skip to content

Commit

Permalink
re-organize error report mechanism
Browse files Browse the repository at this point in the history
  • Loading branch information
butterunderflow committed Aug 21, 2024
1 parent 455d785 commit 5b8922d
Show file tree
Hide file tree
Showing 7 changed files with 62 additions and 51 deletions.
24 changes: 12 additions & 12 deletions lib/typing/check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -51,10 +51,7 @@ let rec check_expr (e : T.expr) (env : Env.t) : expr =
| T.ECmp (op, e0, e1) -> check_cmp op e0 e1 env
| T.ESeq (e0, e1) -> check_seq e0 e1 env
with
| U.UnificationError (t0, t1) ->
Report.unification_error t0 t1 e.start_loc e.end_loc env
| U.OccurError (tv, te) -> Report.occur_error tv te e.start_loc e.end_loc
| e -> raise e
| err -> Report.wrap_and_reraise err e.start_loc e.end_loc env

and check_const c =
match c with
Expand Down Expand Up @@ -414,14 +411,17 @@ and make_mt_by_scope

and check_mod (me : T.mod_expr) (env : Env.t) : mod_expr =
let me_typed =
match me.desc with
| T.MEName name -> check_mod_name name env
| T.MEStruct body -> check_struct body env
| T.MEFunctor ((name, ext_mt0), me1) ->
check_functor name ext_mt0 me1 env
| T.MEField (me, name) -> check_mod_field me name env
| T.MEApply (me0, me1) -> check_mod_apply me0 me1 env
| T.MERestrict (me, mt) -> check_mod_restrict me mt env
try
match me.desc with
| T.MEName name -> check_mod_name name env
| T.MEStruct body -> check_struct body env
| T.MEFunctor ((name, ext_mt0), me1) ->
check_functor name ext_mt0 me1 env
| T.MEField (me, name) -> check_mod_field me name env
| T.MEApply (me0, me1) -> check_mod_apply me0 me1 env
| T.MERestrict (me, mt) -> check_mod_restrict me mt env
with
| err -> Report.wrap_and_reraise err me.start_loc me.end_loc env
in
Env.try_record_hint me_typed env;
me_typed
Expand Down
4 changes: 3 additions & 1 deletion lib/typing/env.ml
Original file line number Diff line number Diff line change
Expand Up @@ -178,10 +178,12 @@ let mk_tid tn env =
| s :: _ -> (s.curr, tn)
| _ -> failwith "nevnerreach"

let occur = ref (fun (_tpv : I.tv ref) (_te : I.ty) : bool -> assert false)

let captured_scope (s : scope) (tpv : Types_in.tv ref) =
match tpv with
| { contents = I.Unbound _ } ->
List.exists (fun (_, (_, te)) -> Unify.occur tpv te) s.values
List.exists (fun (_, (_, te)) -> !occur tpv te) s.values
| { contents = I.Link _ } -> failwith "neverreach"

let captured (env : t) tpv = List.exists (fun s -> captured_scope s tpv) env
Expand Down
64 changes: 37 additions & 27 deletions lib/typing/report.ml
Original file line number Diff line number Diff line change
@@ -1,29 +1,27 @@
module T = Types_in
module PP = Render.NoTypeHintPP

type err =
| UnificationError of (T.ty * T.ty * Lexing.position * Lexing.position)
exception UnificationError of (T.ty * T.ty)

(* error reportings *)
(* todo: support error tolerable type checking *)
exception
UnificationError of T.ty * T.ty * Lexing.position * Lexing.position * Env.t

let unification_error t0 t1 loc1 loc2 env =
raise (UnificationError (t0, t1, loc1, loc2, env))
exception OccurError of string * T.ty

exception ComponentInCompatible of string * T.bind_ty * T.bind_ty

let in_compatible_error name t0 t1 =
raise (ComponentInCompatible (name, t0, t1))
exception LocatedErr of exn * Lexing.position * Lexing.position * Env.t

let error_incompatible name vt0 vt1 =
raise (ComponentInCompatible (name, vt0, vt1))

exception OccurError of string * T.ty * Lexing.position * Lexing.position
let error_unification t0 t1 = raise (UnificationError (t0, t1))

let occur_error tv te loc1 loc2 =
match !tv with
| T.Unbound (v, _lvl) ->
raise (OccurError (Ident.to_string v, te, loc1, loc2))
| T.Link _ -> failwith "neverreach"
let error_occur name te = raise (OccurError (Ident.to_string name, te))

let wrap_and_reraise (kind : exn) start last env =
match kind with
| LocatedErr _ ->
(* make sure there're only one layer of located exception *)
raise kind
| _ -> raise (LocatedErr (kind, start, last, env))

let print_code_range (start : Lexing.position) (last : Lexing.position) =
let start_col = start.pos_cnum - start.pos_bol in
Expand All @@ -33,25 +31,37 @@ let print_code_range (start : Lexing.position) (last : Lexing.position) =

let unknown_location () = Printf.printf "At some unknown location: "

let wrap_with_error_report f =
try Some (f ()) with
| UnificationError (t0, t1, start, last, env) ->
print_code_range start last;
Printf.printf "Can't unify `%s` with `%s`" (PP.pp_str_of_ty ~env t0)
(PP.pp_str_of_ty ~env t1);
let report_error ?env (err : exn) =
match err with
| UnificationError (t0, t1) ->
Printf.printf "Can't unify `%s` with `%s`" (PP.pp_str_of_ty ?env t0)
(PP.pp_str_of_ty ?env t1);
None
| OccurError (tv, te, start, last) ->
print_code_range start last;
| OccurError (tvn, te) ->
Printf.printf "internal error: occur check error\n";
Printf.printf "type variable %s occured in " tv;
Printf.printf "type variable %s occured in " tvn;
PP.pp_ty Format.std_formatter te;
None
| ComponentInCompatible (name, (_, t0), (_, t1)) ->
unknown_location ();
Printf.printf
"Value component %s has type `%s`, which is not compatible with `%s`"
name (PP.pp_str_of_ty t0) (PP.pp_str_of_ty t1);
None
| Failure msg ->
Printf.printf "%s\n" msg;
None
| _ ->
Printf.printf "unknown error";
None

let wrap_with_error_report f =
try Some (f ()) with
| LocatedErr (e, start, last, env) ->
print_code_range start last;
report_error ~env e
| Failure msg ->
Printf.printf "%s\n" msg;
None
| _ ->
Printf.printf "Some unknown erroer occured";
None
2 changes: 1 addition & 1 deletion lib/typing/subtype.ml
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ let compatible mt0 mt1 =
let vt0 = List.assoc name vds0 in
if
P.align_inst vt0 <> P.align_inst (Alias.dealias vt1 !alias_map)
then Report.in_compatible_error name vt0 vt1)
then Report.error_incompatible name vt0 vt1)
vds1;
List.iter
(fun (name, (cd1, cid1)) ->
Expand Down
9 changes: 5 additions & 4 deletions lib/typing/unify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,6 @@ open Types_in
module SMap = Map.Make (Ident)
module Tree = Syntax.Parsetree

exception UnificationError of (ty * ty)

exception OccurError of (tv ref * ty)

exception IllFormType
Expand All @@ -16,7 +14,7 @@ let occurs (tpv : tv ref) (te : ty) : unit =
List.iter go tes
| TVar tpv' when tpv == tpv' -> (
match tpv with
| { contents = Unbound _ } -> raise (OccurError (tpv, te))
| { contents = Unbound (name, _) } -> Report.error_occur name te
| { contents = Link _ } -> failwith "illegal occur check value")
| TVar { contents = Link te } -> go te
| TVar ({ contents = Unbound (tvn', level') } as tpv') ->
Expand Down Expand Up @@ -53,7 +51,7 @@ let rec unify (t0 : ty) (t1 : ty) : unit =
unify_lst [ op0; arg0 ] [ op1; arg1 ]
| TTuple tes0, TTuple tes1 -> unify_lst tes0 tes1
(* by default raise an exception *)
| _ -> raise (UnificationError (t0, t1))
| _ -> Report.error_unification t0 t1

and unify_lst t0 t1 =
match (t0, t1) with
Expand All @@ -69,3 +67,6 @@ let occur (tpv : tv ref) (te : ty) : bool =
false
with
| OccurError (_tpv, _te) -> true

(* initialize forward definition *)
let () = Env.occur := occur
2 changes: 0 additions & 2 deletions lib/typing/unify.mli
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,4 @@ val unify : Types_in.ty -> Types_in.ty -> unit

val occur : Types_in.tv ref -> Types_in.ty -> bool

exception UnificationError of (Types_in.ty * Types_in.ty)

exception OccurError of (Types_in.tv ref * Types_in.ty)
8 changes: 4 additions & 4 deletions tests/regular/typing_test.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1571,29 +1571,29 @@ module L2 = (K: M)

let result = _
|};
[%expect {| name `_` not found |}];
[%expect {| 4:26-4:26 name `_` not found |}];
print_typed
{|
module M = struct end
module X = M
module Bad = M(M)
|};
[%expect {| try apply a structure |}];
[%expect {| 4:18-4:18 try apply a structure |}];
print_typed
{|
module type M = sig end
module F = functor (X:M) -> struct end
let x = F.x
|};
[%expect {| try get field from functor |}];
[%expect {| 4:13-4:13 try get field from functor |}];
print_typed
{|
module M = functor(X:sig end) -> struct
end

module F = M.N
|};
[%expect {| try get field from functor |}];
[%expect {| 5:16-5:16 try get field from functor |}];
print_typed
{|
module type MT = sig
Expand Down

0 comments on commit 5b8922d

Please sign in to comment.