From bdac338613e243da9c67c45eb2caab4e8440c323 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Thu, 22 Aug 2024 01:21:40 +0800 Subject: [PATCH] re-organize error report mechanism --- lib/typing/check.ml | 24 ++++++------- lib/typing/env.ml | 4 ++- lib/typing/report.ml | 66 +++++++++++++++++++++--------------- lib/typing/subtype.ml | 2 +- lib/typing/unify.ml | 9 ++--- lib/typing/unify.mli | 2 -- tests/regular/typing_test.ml | 8 ++--- 7 files changed, 64 insertions(+), 51 deletions(-) diff --git a/lib/typing/check.ml b/lib/typing/check.ml index d0ae8d1..5a129fe 100644 --- a/lib/typing/check.ml +++ b/lib/typing/check.ml @@ -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 @@ -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 diff --git a/lib/typing/env.ml b/lib/typing/env.ml index 2c96908..f7b0a93 100644 --- a/lib/typing/env.ml +++ b/lib/typing/env.ml @@ -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 diff --git a/lib/typing/report.ml b/lib/typing/report.ml index 619ddb6..73f69f8 100644 --- a/lib/typing/report.ml +++ b/lib/typing/report.ml @@ -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)) + +let error_unification t0 t1 = raise (UnificationError (t0, t1)) -exception OccurError of string * T.ty * Lexing.position * Lexing.position +let error_occur name te = raise (OccurError (Ident.to_string name, te)) -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 wrap_and_reraise (kind : exn) start last env = + match kind with + | LocatedErr _ -> + (* An already wraped 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 @@ -33,21 +31,18 @@ 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); @@ -55,3 +50,20 @@ let wrap_with_error_report f = | 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 -> + unknown_location (); + Printf.printf "%s\n" msg; + None + | _ -> + unknown_location (); + Printf.printf "Some unknown erroer occured"; + None diff --git a/lib/typing/subtype.ml b/lib/typing/subtype.ml index 9ee8b24..67bb9f4 100644 --- a/lib/typing/subtype.ml +++ b/lib/typing/subtype.ml @@ -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)) -> diff --git a/lib/typing/unify.ml b/lib/typing/unify.ml index 82e31f8..b501eca 100644 --- a/lib/typing/unify.ml +++ b/lib/typing/unify.ml @@ -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 @@ -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') -> @@ -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 @@ -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 diff --git a/lib/typing/unify.mli b/lib/typing/unify.mli index 7b59c09..fd30b61 100644 --- a/lib/typing/unify.mli +++ b/lib/typing/unify.mli @@ -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) diff --git a/tests/regular/typing_test.ml b/tests/regular/typing_test.ml index 1b2753a..870f42d 100644 --- a/tests/regular/typing_test.ml +++ b/tests/regular/typing_test.ml @@ -1571,21 +1571,21 @@ 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 @@ -1593,7 +1593,7 @@ module L2 = (K: M) 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