Typer Août 2019

typer@iro.umontreal.ca

1 participants
3 discussions

[Git][monnier/typer] Pushed new branch dev/characterization
by Jean-Alexandre Barszcz 30 Aoû '19

30 Aoû '19

Jean-Alexandre Barszcz pushed new branch dev/characterization at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/tree/dev/characterization You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][dev/errors] Print test messages instead of logging them
by Jean-Alexandre Barszcz 22 Aoû '19

22 Aoû '19

Jean-Alexandre Barszcz pushed to branch dev/errors at Stefan / Typer Commits: f23283c3 by Jean-Alexandre Barszcz at 2019-08-22T18:13:46Z Print test messages instead of logging them - - - - - 2 changed files: - src/eval.ml - src/log.ml Changes: ===================================== src/eval.ml ===================================== @@ -908,19 +908,27 @@ let array_empty loc depth args_val = match args_val with let test_fatal loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Log.log_user_fatal section loc msg) + Vcommand (fun () -> + Log.print_entry + (Log.mkEntry Log.Fatal ~kind:"(Unit test fatal)" ~loc ~section msg); + Log.user_error msg + ) | _ -> error loc "Test.fatal takes two String as argument" let test_warning loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Log.log_user_warning section loc msg; - tunit) + Vcommand (fun () -> + Log.print_entry + (Log.mkEntry Log.Warning ~kind:"(Unit test warning)" ~loc ~section msg); + tunit) | _ -> error loc "Test.warning takes two String as argument" let test_info loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Log.log_user_info section loc msg; - tunit) + Vcommand (fun () -> + Log.print_entry + (Log.mkEntry Log.Info ~kind:"(Unit test Info)" ~loc ~section msg); + tunit) | _ -> error loc "Test.info takes two String as argument" let test_location loc depth args_val = match args_val with ===================================== src/log.ml ===================================== @@ -214,11 +214,3 @@ let debug_msg expr = if Debug <= typer_log_config.level then (print_string expr; flush stdout) let not_implemented_error () = internal_error "not implemented" - -let log_user_fatal section loc msg = - log_msg Fatal ~kind:"(Unit test fatal)" ~section ~loc msg; - user_error msg -let log_user_warning section loc msg = - log_msg Warning ~kind:"(Unit test warning)" ~section ~loc msg -let log_user_info section loc msg = - log_msg Info ~kind:"(Unit test info)" ~section ~loc msg View it on GitLab: https://gitlab.com/monnier/typer/commit/f23283c36f16d75a505e4cffcb137ababff… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/f23283c36f16d75a505e4cffcb137ababff… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][dev/errors] 5 commits: Refactor logging
by Jean-Alexandre Barszcz 15 Aoû '19

15 Aoû '19

Jean-Alexandre Barszcz pushed to branch dev/errors at Stefan / Typer Commits: 3e992d26 by Jean-Alexandre Barszcz at 2019-08-15T18:18:20Z Refactor logging - - - - - ef27ab61 by Jean-Alexandre Barszcz at 2019-08-15T18:18:20Z Add optional color to logging - - - - - 6eda68cf by Jean-Alexandre Barszcz at 2019-08-15T19:05:34Z Print errors/warnings all at once, after compilation stops - - - - - 027b878d by Jean-Alexandre Barszcz at 2019-08-15T19:05:34Z Add an option to control the verbosity/logging level - - - - - db872087 by Jean-Alexandre Barszcz at 2019-08-15T19:05:34Z Always print the log after evaluation If there are warnings (or other messages of lesser priority in the log), we want to print them. Similarly, errors for which we were able to recover might still exist in the log. Regardless of whether compilation has been stopped, we thus print the log. - - - - - 17 changed files: - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/inverse_subst.ml - src/lexp.ml - src/log.ml - src/opslexp.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/utest_lib.ml Changes: ===================================== src/REPL.ml ===================================== @@ -63,8 +63,16 @@ let print_input_line i = ralign_print_int i 2; print_string "] >> " -let ieval_error loc msg = - Log.msg_error "IEVAL" loc msg +let ieval_error = Log.log_error ~section:"IEVAL" + +let print_and_clear_log () = + if (not Log.typer_log_config.print_at_log) then + Log.print_and_clear_log () + +let handle_stopped_compilation msg = + print_and_clear_log (); + print_string msg; print_newline (); + flush stdout (* Read stdin for input. Returns only when the last char is ';' * We can use '%' to prevent parsing @@ -207,7 +215,7 @@ let readfiles files (i, lctx, rctx) prt = (List.iter (print_eval_result i) ret; (i + 1, lctx, rctx)) with Sys_error _ -> ( - ieval_error dloc ("file \"" ^ file ^ "\" does not exist."); + ieval_error ("file \"" ^ file ^ "\" does not exist."); (i, lctx, rctx)) ) (i, lctx, rctx) files @@ -231,8 +239,8 @@ let rec repl i clxp rctx = let (i, clxp, rctx) = try readfiles args (i, clxp, rctx) false - with Log.Stop_Compilation s -> - (print_string s; (i,clxp,rctx)) + with Log.Stop_Compilation msg -> + (handle_stopped_compilation msg; (i,clxp,rctx)) in repl clxp rctx; | "%who"::args | "%w"::args -> ( @@ -247,18 +255,25 @@ let rec repl i clxp rctx = repl clxp rctx) | cmd::_ -> - ieval_error dloc (" \"" ^ cmd ^ "\" is not a correct repl command"); + ieval_error (" \"" ^ cmd ^ "\" is not a correct repl command"); repl clxp rctx | _ -> repl clxp rctx) (* eval input *) - | _ -> ( + | _ -> try let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in + print_and_clear_log (); List.iter (print_eval_result i) ret; repl clxp rctx - with e -> match e with - | Log.Stop_Compilation msg -> (print_string msg; repl clxp rctx) - | _ -> Log.catch_error (); repl clxp rctx) + with + | Log.Stop_Compilation msg -> + (handle_stopped_compilation msg; repl clxp rctx) + | Log.Internal_error msg -> + (handle_stopped_compilation ("Internal error: " ^ msg); + repl clxp rctx) + | Log.User_error msg -> + (handle_stopped_compilation ("Fatal user error: " ^ msg); + repl clxp rctx) let arg_files = ref [] @@ -266,6 +281,9 @@ let arg_files = ref [] (* ./typer [options] files *) let arg_defs = [ ("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); + ("--verbosity", + Arg.String Log.set_typer_log_level_str, "Set the logging level"); + ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) (*"-I", Arg.String (fun f -> searchpath := f::!searchpath), @@ -287,8 +305,19 @@ let main () = print_string (make_sep '-'); flush stdout); - let (i, ectx, rctx) = readfiles (List.rev !arg_files) (1, ectx, rctx) - (not !arg_batch) in + let (i, ectx, rctx) = ( + try + let res = + readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in + print_and_clear_log (); res + with + | Log.Stop_Compilation msg -> + handle_stopped_compilation msg; exit 1 + | Log.Internal_error msg -> + handle_stopped_compilation ("Internal error: " ^ msg); exit 1 + | Log.User_error msg -> + handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 + ) in flush stdout; ===================================== src/builtin.ml ===================================== @@ -64,8 +64,9 @@ open Lexp module DB = Debruijn module E = Env -let error loc msg = Log.msg_error "BUILT-IN" loc msg; raise (Log.internal_error msg) -let warning loc msg = Log.msg_warning "BUILT-IN" loc msg +let log_raise_error ?loc msg = + Log.log_error ~section:"BUILT-IN" ?loc msg; + Log.internal_error msg let predef_names = [ "cons"; (* FIXME: Should be used but isn't! *) @@ -87,7 +88,7 @@ let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in mkSusp p (S.shift r) - with Not_found -> error dummy_location ("\""^ name ^ "\" was not predefined") + with Not_found -> log_raise_error ("\""^ name ^ "\" was not predefined") let set_predef name lexp = predef_map := SMap.add name lexp (!predef_map) @@ -131,9 +132,9 @@ let v2o_list v = match v with | E.Vcons ((_, "cons"), [hd; tl]) -> v2o_list (hd::acc) tl | E.Vcons ((_, "nil"), []) -> List.rev acc - | _ -> print_string (E.value_name v); print_string "\n"; - E.value_print v; - error dloc "List conversion failure'" in + | _ -> log_raise_error ~loc:(E.value_location v) ( + "Failed to convert the " ^ E.value_name v ^ " with value :\n" + ^ E.value_string v ^ "\n to a list.") in v2o_list [] v (* Map of lexp builtin elements accessible via (## <name>). *) ===================================== src/debruijn.ml ===================================== @@ -42,8 +42,7 @@ open Fmt module S = Subst -let error l m = Log.msg_error "DEBRUIJN" l m; Log.internal_error m -let warning = Log.msg_warning "DEBRUIJN" +let fatal = Log.log_fatal ~section:"DEBRUIJN" (* Handling scoping/bindings is always tricky. So it's always important * to keep in mind for *every* expression which is its context. @@ -316,17 +315,17 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = | (((_, Some name), _, _), Some ename) -> (* Check if names match *) if not (ename = name) then - (print_lexp_ctx ctx; - error loc ("DeBruijn index " - ^ string_of_int dbi - ^ " refers to wrong name. " - ^ "Expected: `" ^ ename - ^ "` got `" ^ name ^ "`")) + fatal ~loc ~print_action:(fun _ -> + print_lexp_ctx ctx; print_newline ()) + ("DeBruijn index " ^ string_of_int dbi + ^ " refers to wrong name. " + ^ "Expected: `" ^ ename + ^ "` got `" ^ name ^ "`") | _ -> () in ret) with - Not_found -> error loc ("DeBruijn index " + Not_found -> fatal ~loc ("DeBruijn index " ^ string_of_int dbi ^ " of `" ^ maybename oename ^ "` out of bounds!") @@ -366,7 +365,7 @@ let rec lctx_view lctx = | _ -> CVfix (defs, lctx) in loop 2 lctx [(loname, def, t)] | Myers.Mcons ((_, LetDef (o, def), _), _, _, _) when o > 1 - -> Log.internal_error "Unexpected lexp_context shape!" + -> fatal "Unexpected lexp_context shape!" | Myers.Mcons ((loname, odef, t), lctx, _, _) -> CVlet (loname, odef, t, lctx) ===================================== src/elab.ml ===================================== @@ -69,21 +69,28 @@ let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl" -let warning = Log.msg_warning "ELAB" -let error = Log.msg_error "ELAB" -let fatal = Log.msg_fatal "ELAB" - -(* Print Lexp name followed by the lexp in itself, finally throw an exception *) -let debug_message error_type type_name type_string loc expr message = - EV.debug_messages error_type loc - message [ - (type_name expr) ^ ": " ^ (type_string expr); - ] - -let lexp_fatal = debug_message fatal lexp_name lexp_string -let lexp_warning = debug_message warning lexp_name lexp_string -let lexp_error = debug_message error lexp_name lexp_string -let value_fatal = debug_message fatal value_name value_string +let fatal = Log.log_fatal ~section:"ELAB" +let error = Log.log_error ~section:"ELAB" +let warning = Log.log_warning ~section:"ELAB" +let info = Log.log_info ~section:"ELAB" + +let indent_line str = + " > " ^ str +let print_indent_line str = + print_endline (indent_line str) +let print_details to_name to_str elem = + print_indent_line ((to_name elem) ^ ": " ^ (to_str elem)) +let lexp_print_details lexp () = + print_details lexp_name lexp_string lexp +let value_print_details value () = + print_details value_name value_string value + +let lexp_error loc lexp = + error ~loc ~print_action:(lexp_print_details lexp) +let lexp_fatal loc lexp = + fatal ~loc ~print_action:(lexp_print_details lexp) +let value_fatal loc value = + fatal ~loc ~print_action:(value_print_details value) (** Type info returned by elaboration. *) type sform_type = @@ -116,9 +123,9 @@ let sform_default_ectx = ref empty_elab_context let elab_check_sort (ctx : elab_context) lsort var ltp = match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) with e -> - print_string "Exception during whnf of "; - lexp_print lsort; - print_string "\n"; + info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) + ~loc:(lexp_location lsort) + "Exception during whnf of sort:"; raise e) with | Sort (_, _) -> () (* All clear! *) | _ -> let lexp_string e = lexp_string (L.clean e) in @@ -135,14 +142,18 @@ let elab_check_proper_type (ctx : elab_context) ltp var = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp with e -> match e with | Log.Stop_Compilation _ -> raise e - | _ -> print_string "Exception while checking type `"; - lexp_print ltp; - (match var with - | (_, None) -> () - | (_, Some name) - -> print_string ("` of var `" ^ name ^"`\n")); - print_lexp_ctx (ectx_to_lctx ctx); - raise e + | _ -> + info + ~print_action:(fun _ -> + print_lexp_ctx (ectx_to_lctx ctx); print_newline () + ) + ~loc:(lexp_location ltp) + ("Exception while checking type `" ^ (lexp_string ltp) ^ "`" + ^ (match var with + | (_, None) -> "" + | (_, Some name) + -> " of var `" ^ name ^ "`")); + raise e let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in @@ -151,29 +162,36 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lexp_string e = lexp_string (L.clean e) in let ltype' = try OL.check lctx lxp with e -> match e with - (* lexp_error is fatal but Stop_Compilation isn't *) | Log.Stop_Compilation _ -> raise e - | _ -> lexp_error loc lxp "Error while type-checking"; + | _ -> + info + ~print_action:(fun _ -> + lexp_print_details lxp (); print_lexp_ctx (ectx_to_lctx ctx); - raise e in + print_newline () + ) + ~loc + "Error while type-checking"; + raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' - with e - -> print_string ("Exception while conversion-checking types:\n"); - lexp_print ltype; - print_string (" and "); - lexp_print ltype'; - print_string ("\n"); - lexp_error loc lxp - ("Exception while conversion-checking types " - ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); - raise e) + with e -> + info ~print_action:(lexp_print_details lxp) + ~loc + ("Exception while conversion-checking types " + ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); + raise e) then elab_check_proper_type ctx ltype var else - (EV.debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ - lexp_string lxp ^ " !: " ^ lexp_string ltype; - " because"; - lexp_string ltype' ^ " != " ^ lexp_string ltype]) + fatal + ~print_action:(fun _ -> + List.iter print_indent_line [ + lexp_string lxp ^ " !: " ^ lexp_string ltype; + " because"; + lexp_string ltype' ^ " != " ^ lexp_string ltype + ]) + ~loc + "Type check error: ¡¡ctx_define error!!" let ctx_extend (ctx: elab_context) (var : vname) def ltype = elab_check_proper_type ctx ltype var; @@ -449,7 +467,7 @@ let rec elaborate ctx se ot = and infer (p : sexp) (ctx : elab_context): lexp * ltype = match elaborate ctx p None with - | (_, Checked) -> fatal (sexp_location p) "`infer` got Checked!" + | (_, Checked) -> fatal ~loc:(sexp_location p) "`infer` got Checked!" | (e, Lazy) -> (e, OL.get_type (ectx_to_lctx ctx) e) | (e, Inferred t) -> (e, t) @@ -608,7 +626,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let pat_string p = sexp_string (pexp_u_pat p) in let uniqueness_warn pat = - warning (pexp_pat_location pat) + warning ~loc:(pexp_pat_location pat) ("Pattern " ^ pat_string pat ^ " is a duplicate. It will override previous pattern.") in @@ -911,7 +929,10 @@ and lexp_eval ectx e = ^ track_fv rctx (ectx_to_lctx ectx) e); try EV.eval ee rctx - with exc -> EV.print_eval_trace None; raise exc + with exc -> + info ~print_action:(fun _ -> EV.print_eval_trace None) + "Exception happened during evaluation:"; + raise exc and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) : value_type = @@ -945,11 +966,11 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = | Vcommand cmd -> (match (cmd ()) with | Vsexp (sexp) -> sexp - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a IO sexp")) - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return an IO") + | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return a IO sexp")) + | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return an IO") with e -> - fatal loc ("Macro `" ^ mname ^ "` not found") + fatal ~loc ("Macro `" ^ mname ^ "` not found") and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) @@ -1015,8 +1036,8 @@ and lexp_decls_1 let rec lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = match sdecls with | [] -> (if not (SMap.is_empty pending_decls) then - let (s, l) = SMap.choose pending_decls in - error l ("Variable `" ^ s ^ "` declared but not defined!") + let (s, loc) = SMap.choose pending_decls in + error ~loc ("Variable `" ^ s ^ "` declared but not defined!") else assert (pending_defs == [])); [], [], nctx @@ -1028,11 +1049,11 @@ and lexp_decls_1 -> lexp_decls_1 (List.append sdecls' sdecls) ectx nctx pending_decls pending_defs - | Node (Symbol (l, "_:_"), args) :: sdecls + | Node (Symbol (loc, "_:_"), args) :: sdecls (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol (l, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (l, Some vname) in + | [Symbol (loc, vname); stp] + -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in @@ -1043,7 +1064,7 @@ and lexp_decls_1 (* Unify it with the new one. *) let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with | (None | Some (_::_)) - -> lexp_error l ltp + -> lexp_error loc ltp ("New type annotation `" ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") @@ -1051,13 +1072,13 @@ and lexp_decls_1 lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then - (error l ("Variable `" ^ vname ^ "` already defined!"); + (error ~loc ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) else lexp_decls_1 sdecls ectx - (ectx_extend nctx (l, Some vname) ForwardRef ltp) - (SMap.add vname l pending_decls) + (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + (SMap.add vname loc pending_decls) pending_defs - | _ -> error l "Invalid type declaration syntax"; + | _ -> error ~loc "Invalid type declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | Node (Symbol (l, "_=_") as head, args) :: sdecls @@ -1093,7 +1114,7 @@ and lexp_decls_1 lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else - (error l ("`" ^ vname ^ "` defined but not declared!"); + (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | [Node (Symbol s, args) as d; body] @@ -1105,7 +1126,7 @@ and lexp_decls_1 :: sdecls) ectx nctx pending_decls pending_defs - | _ -> error l "Invalid definition syntax"; + | _ -> error ~loc:l "Invalid definition syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | Node (Symbol (l, "define-operator"), args) :: sdecls @@ -1120,7 +1141,7 @@ and lexp_decls_1 pending_decls pending_defs | sexp :: sdecls - -> error (sexp_location sexp) "Invalid declaration syntax"; + -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in (EV.set_getenv nctx; @@ -1157,17 +1178,17 @@ and sform_new_attribute ctx loc sargs ot = OL.lexp_close (ectx_to_lctx ctx) ltp, Some AttributeMap.empty), Lazy) - | _ -> fatal loc "new-attribute expects a single Type argument" + | _ -> fatal ~loc "new-attribute expects a single Type argument" and sform_add_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, Some name), idx); attr] -> table, (n - idx, name), attr - | _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in + | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type - | _ -> fatal loc "add-attribute expects a table as first argument" in + | _ -> fatal ~loc "add-attribute expects a table as first argument" in (* FIXME: Type check (attr: type == attr_type) *) let attr' = OL.lexp_close (ectx_to_lctx ctx) attr in @@ -1179,11 +1200,11 @@ and get_attribute ctx loc largs = let ctx_n = get_size ctx in let table, var = match largs with | [table; Var((_, Some name), idx)] -> table, (ctx_n - idx, name) - | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in + | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map - | _ -> fatal loc "get-attribute expects a table as first argument" in + | _ -> fatal ~loc "get-attribute expects a table as first argument" in try Some (AttributeMap.find var map) with Not_found -> None @@ -1197,7 +1218,7 @@ and sform_has_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, Some name), idx)] -> table, (n - idx, name) - | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in + | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type @@ -1211,9 +1232,9 @@ and sform_declexpr ctx loc sargs ot = | [Var((_, vn), vi)] -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> (lxp, Lazy) - | None -> error loc "no expr available"; + | None -> error ~loc "no expr available"; sform_dummy_ret ctx loc) - | _ -> error loc "declexpr expects one argument"; + | _ -> error ~loc "declexpr expects one argument"; sform_dummy_ret ctx loc @@ -1221,7 +1242,7 @@ let sform_decltype ctx loc sargs ot = match List.map (lexp_parse_sexp ctx) sargs with | [Var((_, vn), vi)] -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) - | _ -> error loc "decltype expects one argument"; + | _ -> error ~loc "decltype expects one argument"; sform_dummy_ret ctx loc let builtin_value_types : ltype option SMap.t ref = ref SMap.empty @@ -1237,13 +1258,13 @@ let sform_built_in ctx loc sargs ot = sexp_error loc ("Unknown built-in `" ^ name ^ "`"); BI.add_builtin_cst name bi; (bi, Checked) - | None -> error loc "Built-in's type not provided by context!"; + | None -> error ~loc "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) - | true, _ -> error loc "Wrong Usage of `Built-in`"; + | true, _ -> error ~loc "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc - | false, _ -> error loc "Use of `Built-in` in user code"; + | false, _ -> error ~loc "Use of `Built-in` in user code"; sform_dummy_ret ctx loc let sform_datacons ctx loc sargs ot = @@ -1273,8 +1294,9 @@ let elab_typecons_arg arg : (arg_kind * vname * sexp option) = -> (elab_colon_to_ak k, (l, Some name), Some e) | Symbol (l, name) -> (Anormal, (l, Some name), None) - | _ -> sexp_print arg; - (sexp_error (sexp_location arg) "Unrecognized formal arg"); + | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) + (sexp_location arg) + "Unrecognized formal arg"; (Anormal, (sexp_location arg, None), None) let sform_typecons ctx loc sargs ot = @@ -1402,7 +1424,7 @@ let sform_identifier ctx loc sargs ot = (if not (name = "") then let idx = match mv with | Metavar (idx, _, _) -> idx - | _ -> fatal loc "newMetavar returned a non-Metavar" in + | _ -> fatal ~loc "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); (mkSusp mv subst, match ot with Some _ -> Checked | None -> Lazy) @@ -1583,7 +1605,8 @@ let sform_load usr_elctx loc sargs ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error loc "argument to load should be one file name (String)"; !sform_default_ectx) in + | _ -> (error ~loc "argument to load should be one file name (String)"; + !sform_default_ectx) in (* get lexp_context *) let usr_lctx = ectx_to_lctx usr_elctx in @@ -1670,8 +1693,8 @@ let default_ectx let idx = senv_lookup name elctx in let v = mkVar ((dloc, Some name), idx) in BI.set_predef name v) BI.predef_names; - with e -> - warning dloc "Predef not found"; in + with Senv_Lookup_Fail _ -> + warning "Predef not found"; in (* Empty context *) let lctx = empty_elab_context in @@ -1698,7 +1721,7 @@ let default_ectx (fun () -> read_file (btl_folder ^ "/pervasive.typer") lctx) in let _ = sform_default_ectx := ectx in ectx - with (Log.Stop_Compilation _) -> fatal dloc "compilation stopped in default context" + with (Log.Stop_Compilation _) -> fatal "compilation stopped in default context" let default_rctx = EV.from_ectx default_ectx @@ -1714,7 +1737,7 @@ let lexp_expr_str str ctx = List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps; lexps - with Log.Stop_Compilation s -> (print_string s; []) + with Log.Stop_Compilation s -> [] let lexp_decl_str str ctx = try let tenv = default_stt in @@ -1722,7 +1745,7 @@ let lexp_decl_str str ctx = let limit = Some ";" in let sdecls = sexp_parse_str str tenv grm limit in lexp_p_decls sdecls ctx - with Log.Stop_Compilation s -> (print_string s; ([],ctx)) + with Log.Stop_Compilation s -> ([],ctx) (* Eval String @@ -1733,7 +1756,7 @@ let eval_expr_str str lctx rctx = try let lxps = lexp_expr_str str lctx in let elxps = List.map OL.erase_type lxps in EV.eval_all elxps rctx false - with Log.Stop_Compilation s -> (print_string s; []) + with Log.Stop_Compilation s -> [] let eval_decl_str str lctx rctx = let prev_lctx, prev_rctx = lctx, rctx in @@ -1741,5 +1764,5 @@ let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in let elxps = (List.map OL.clean_decls lxps) in (EV.eval_decls_toplevel elxps rctx), lctx - with Log.Stop_Compilation s -> (print_string s; prev_rctx, prev_lctx) + with Log.Stop_Compilation s -> (prev_rctx, prev_lctx) ===================================== src/env.ml ===================================== @@ -30,7 +30,6 @@ * * --------------------------------------------------------------------------- *) -open Util (* msg_error *) open Fmt (* make_title, table util *) open Sexp @@ -41,10 +40,10 @@ module L = Lexp module BI = Big_int module DB = Debruijn -let dloc = dummy_location +let dloc = Util.dummy_location -let error loc msg = Log.msg_error "ENV" loc msg; raise (Log.internal_error msg) -let warning loc msg = Log.msg_warning "ENV" loc msg +let fatal = Log.log_fatal ~section:"ENV" +let warning = Log.log_warning ~section:"ENV" let str_idx idx = "[" ^ (string_of_int idx) ^ "]" @@ -81,11 +80,11 @@ let rec value_equal a b = | Vin (c1), Vin (c2) -> c1 = c2 | Vout (c1), Vout (c2) -> c2 = c2 | Vcommand (f1), Vcommand (f2) -> f1 = f2 - | Vundefined, _ | _, Vundefined -> warning dloc "Vundefined"; false - | Vtype e1, Vtype e2 -> warning dloc "Vtype"; false + | Vundefined, _ | _, Vundefined -> warning "Vundefined"; false + | Vtype e1, Vtype e2 -> warning "Vtype"; false | Closure (s1, b1, ctx1), Closure (s2, b2, ctx2) - -> warning dloc "Closure"; + -> warning "Closure"; if (s1 != s2) then false else true | Vcons ((_, ct1), a1), Vcons ((_, ct2), a2) @@ -178,14 +177,14 @@ let get_rte_variable (name: vname) (idx: int) if n1 = n2 then x else ( - error dloc + fatal ("Variable lookup failure. Expected: \"" ^ n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "\" got \"" ^ n1 ^ "\""))) | _ -> x) with Not_found -> let n = match name with (_, Some n) -> n | _ -> "" in - error dloc ("Variable lookup failure. Var: \"" ^ + fatal ("Variable lookup failure. Var: \"" ^ n ^ "\" idx: " ^ (str_idx idx)) let add_rte_variable (name:vname) (x: value_type) (ctx: runtime_env) @@ -199,7 +198,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = (match (n, name) with | ((_, Some n1), (_, Some n2)) -> if (n1 != n2) then - error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) + fatal ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) | _ -> ()); ref_cell := v ===================================== src/eval.ml ===================================== @@ -82,13 +82,12 @@ let rec_depth trace = List.length b (* eval error are always fatal *) -let error loc msg = - Log.msg_error "EVAL" loc msg; - flush stdout; - raise (Log.internal_error msg) +let error loc ?print_action msg = + Log.log_error ~section:"EVAL" ~loc ?print_action msg; + Log.internal_error msg -let fatal = Log.msg_fatal "EVAL" -let warning = Log.msg_warning "EVAL" +let fatal loc msg = Log.log_fatal ~section:"EVAL" ~loc msg +let warning loc msg = Log.log_warning ~section:"EVAL" ~loc msg (* Print a message that look like this: * @@ -119,7 +118,7 @@ let debug_message error_type type_name type_string loc expr message = (* Print value name followed by the value in itself, finally throw an exception *) let value_fatal = debug_message fatal value_name value_string -let value_error = debug_message error value_name value_string +let value_error = debug_message (error ?print_action:None) value_name value_string let elexp_fatal = debug_message fatal elexp_name elexp_string @@ -341,16 +340,20 @@ let file_read loc depth args_val = match args_val with (* FIXME: Either rename it to "readline" and drop the second arg, * or actually pay attention to the second arg. *) | [Vin channel; Vint n] -> Vstring (input_line channel) - | _ -> List.iter (fun v -> value_print v; print_string "\n") args_val; - error loc "File.read expects an in_channel" + | _ -> error loc ~print_action:(fun _ -> + List.iter (fun v -> value_print v; print_newline ()) args_val; + ) + "File.read expects an in_channel. Actual arguments:" let file_write loc depth args_val = match args_val with | [Vout channel; Vstring msg] -> Vcommand (fun () -> fprintf channel "%s" msg; (* FIXME: This should be the unit value! *) Vundefined) - | _ -> List.iter (fun v -> value_print v) args_val; - error loc "File.write expects an out_channel and a string" + | _ -> error loc ~print_action:(fun _ -> + List.iter (fun v -> value_print v; print_newline ()) args_val; + ) + "File.write expects an out_channel and a string. Actual arguments:" let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) = @@ -470,9 +473,12 @@ and eval_call loc unef i f args = buildbody (arity - nargs - 1), buildctx args Myers.nil) - with Not_found - -> error loc ("Requested Built-in `" ^ name ^ "` does not exist") - | e -> error loc ("Exception thrown from primitive `" ^ name ^"`")) + with + | Not_found -> + error loc ("Requested Built-in `" ^ name ^ "` does not exist") + | e -> + warning loc ("Exception thrown from primitive `" ^ name ^"`"); + raise e) | Vtype e, _ (* We may call a Vlexp e.g. for "x = Map Int String". @@ -902,18 +908,18 @@ let array_empty loc depth args_val = match args_val with let test_fatal loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Log.msg_user_fatal section loc msg) + Vcommand (fun () -> Log.log_user_fatal section loc msg) | _ -> error loc "Test.fatal takes two String as argument" let test_warning loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Log.msg_user_warning section loc msg; + Vcommand (fun () -> Log.log_user_warning section loc msg; tunit) | _ -> error loc "Test.warning takes two String as argument" let test_info loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Log.msg_user_info section loc msg; + Vcommand (fun () -> Log.log_user_info section loc msg; tunit) | _ -> error loc "Test.info takes two String as argument" @@ -1049,10 +1055,12 @@ let eval lxp ctx = eval lxp ctx ([], []) let debug_eval lxp ctx = try eval lxp ctx with e -> ( - print_rte_ctx (!global_eval_ctx); - print_eval_trace None; - raise e) - + Log.log_info ~section:"EVAL" ~print_action:(fun _ -> + print_rte_ctx (!global_eval_ctx); + print_eval_trace None + ) + "Exception occured during evaluation in the following context:"; + raise e) let eval_decls decls ctx = eval_decls decls ctx ([], []) ===================================== src/fmt.ml ===================================== @@ -156,3 +156,6 @@ let yellow = "\x1b[33m" let magenta = "\x1b[35m" let cyan = "\x1b[36m" let reset = "\x1b[0m" + +let color_string color str = + color ^ str ^ reset ===================================== src/inverse_subst.ml ===================================== @@ -168,11 +168,11 @@ let inverse (s: Lexp.subst) : Lexp.subst option = | Some s1 -> if is_identity (Lexp.scompose s s1) || is_identity (Lexp.scompose s1 s) then () - else (print_string ("Subst-inversion-bug: " - ^ subst_string s ^ " ∘ " - ^ subst_string s1 ^ " == " - ^ subst_string (Lexp.scompose s1 s) - ^ " !!\n")) + else (Log.log_debug ("Subst-inversion-bug: " + ^ subst_string s ^ " ∘ " + ^ subst_string s1 ^ " == " + ^ subst_string (Lexp.scompose s1 s) + ^ " !!\n")) | _ -> ()); res ===================================== src/lexp.ml ===================================== @@ -166,7 +166,7 @@ let metavar_table = ref (U.IMap.empty : meta_subst) let metavar_lookup (id : meta_id) : metavar_info = try U.IMap.find id (!metavar_table) with Not_found - -> Log.msg_fatal "LEXP" U.dummy_location "metavar lookup failure!" + -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" (********************** Hash-consing **********************) ===================================== src/log.ml ===================================== @@ -22,15 +22,162 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util -(* - * -1 - Nothing (* During testing we may want to produce errors *) - * 0 - Fatal - * 1 - Error - * 2 - Warning - * 3 - Info - *) - -let typer_verbose = ref 20 +(* LOGGING LEVELS *) + +type log_level = Nothing | Fatal | Error | Warning | Info | Debug + +let int_of_level lvl = + match lvl with + | Nothing -> -1 (* We might not want to print anything during testing *) + | Fatal -> 0 | Error -> 1 | Warning -> 2 | Info -> 3 | Debug -> 4 + +let level_of_int i = + match i with + | _ when i < 0 -> Nothing + | 0 -> Fatal | 1 -> Error | 2 -> Warning | 3 -> Info + | _ -> Debug + +let string_of_level lvl = + match lvl with + | Nothing -> "Nothing" + | Fatal -> "Fatal" + | Error -> "Error" + | Warning -> "Warning" + | Info -> "Info" + | Debug -> "Debug" + +let level_of_string str = + match Util.string_uppercase str with + | "NOTHING" -> Nothing + | "FATAL" -> Fatal + | "ERROR" -> Error + | "WARNING" -> Warning + | "INFO" -> Info + | "DEBUG" -> Debug + | _ -> invalid_arg ("`"^str^"` is not a logging level") + +let level_color lvl = + match lvl with + | Nothing -> None + | Fatal -> Some Fmt.red + | Error -> Some Fmt.red + | Warning -> Some Fmt.yellow + | Info -> Some Fmt.cyan + | Debug -> Some Fmt.magenta + +(* LOGGING CONFIGURATION *) + +type log_config = { + mutable level : log_level; + mutable print_at_log : bool; + mutable print_in_reverse : bool; + mutable color : bool; + } + +let typer_log_config = { + level = Warning; + print_at_log = false; + print_in_reverse = false; + color = true; + } + +(* LOG DEFINITION *) + +type log_entry = { + level : log_level; + kind : string option; + section : string option; + print_action : (unit -> unit) option; + loc : location option; + msg : string; + } + +type log = log_entry list + +let empty_log = [] + +let typer_log = ref empty_log + +(* PRIVATE OPERATIONS *) + +let mkEntry level ?kind ?section ?print_action ?loc msg = + {level; kind; section; print_action; loc; msg} + +let log_push (entry : log_entry) = + typer_log := entry::(!typer_log) + +let string_of_location (loc : location) = + (loc.file ^ ":" + ^ string_of_int loc.line ^ ":" + ^ string_of_int loc.column ^ ":") + +let maybe_color_string color_opt str = + match color_opt with + | Some color -> Fmt.color_string color str + | None -> str + +let string_of_log_entry {level; kind; section; loc; msg} = + let color = if typer_log_config.color then (level_color level) else None in + let parens s = "(" ^ s ^ ")" in + (option_default "" (option_map string_of_location loc) + ^ maybe_color_string color (option_default (string_of_level level) kind) ^ ":" + ^ option_default "" (option_map parens section) ^ " " + ^ msg) + +let print_entry entry = + print_endline (string_of_log_entry entry); + match entry.print_action with + | Some f -> f () + | None -> () + +let log_entry (entry : log_entry) = + if (entry.level <= typer_log_config.level) + then ( + log_push entry; + if (typer_log_config.print_at_log) + then + (print_entry entry; + flush stdout) + ) + +let count_msgs (lvlp : log_level -> bool) = + let count_step count {level} = + if lvlp level then count + 1 else count + in + List.fold_left count_step 0 !typer_log + +let error_count () = count_msgs (fun level -> level <= Error) +let warning_count () = count_msgs (fun level -> level = Warning) + +(* PUBLIC INTERFACE *) + +let set_typer_log_level lvl = + typer_log_config.level <- lvl + +let set_typer_log_level_str str = + try set_typer_log_level (level_of_int (int_of_string str)) + with + _ -> set_typer_log_level (level_of_string str) + +let increment_log_level () = + typer_log_config.level + |> int_of_level + |> (+) 1 + |> level_of_int + |> set_typer_log_level + +let clear_log () = typer_log := empty_log + +let print_log () = + let reverse = typer_log_config.print_in_reverse in + let l = if reverse then !typer_log else List.rev !typer_log in + List.iter print_entry l + +let print_and_clear_log () = + print_log (); clear_log () + +let log_msg level ?kind ?section ?print_action ?loc msg = + log_entry (mkEntry level ?kind ?section ?print_action ?loc msg) exception Internal_error of string let internal_error s = raise (Internal_error s) @@ -41,88 +188,37 @@ let user_error s = raise (User_error s) exception Stop_Compilation of string let stop_compilation s = raise (Stop_Compilation s) -(* `error list * warning list` both of type `level * kind * section * loc * msg` *) -type error_log_type = ((int * string * string * location * string) list * - (int * string * string * location * string) list) - -let empty_error_log : error_log_type = ([],[]) - -let error_log = ref empty_error_log - -let error_count () : int = let errors, _ = !error_log in - List.length errors - -let warning_count () : int = let _, warnings = !error_log in - List.length warnings - -let new_error lvl kind section loc msg = let errors, warnings = !error_log in - error_log := ((lvl,kind,section,loc,msg)::errors,warnings) - -let new_warning lvl kind section loc msg = let errors, warnings = !error_log in - error_log := (errors,(lvl,kind,section,loc,msg)::warnings) - -let reset_error_log () = error_log := empty_error_log - -(* Section is the name of the compilation step [for debugging] *) -(* 'prerr' output is ugly *) -let msg_message (error : bool) lvl kind section (loc: location) msg = - let message = (loc.file - ^ ":" ^ string_of_int loc.line - ^ ":" ^ string_of_int loc.column - ^ ":" ^ kind - ^ (if section = "" then " " else "(" ^ section ^ ") ") - ^ msg ^ "\n") in - - if error then - new_error lvl kind section loc msg - else - new_warning lvl kind section loc msg; - - if lvl <= !typer_verbose then - print_string message - else () - -let stop_on_error () = if (0 < (error_count ())) then - (let count = error_count () in - reset_error_log (); - stop_compilation - ("Compiler stopped after: "^(string_of_int count)^" error\n")) - else () - -let stop_on_warning () = (stop_on_error (); - if (0 < (warning_count ())) then - let count = warning_count () in - reset_error_log (); - stop_compilation - ("Compiler stopped after: "^(string_of_int count)^" warning\n") - else ()) - -let catch_error () = try stop_on_error () - with e -> match e with - | Stop_Compilation msg -> print_string msg - | _ -> () - -let msg_fatal s l m = - msg_message false 0 "[X] Fatal " s l m; - flush stdout; - reset_error_log (); - internal_error "Compiler Fatal Error" - -let msg_error = msg_message true 1 "Error:" -let msg_warning = msg_message false 2 "Warning:" -let msg_info = msg_message false 3 "Info:" - -let msg_user_fatal s l m = - msg_message true 1 "(Unit test fatal):" s l m; - flush stdout; - reset_error_log (); - user_error "User Fatal Error" - -let msg_user_warning = msg_message false 2 "(Unit test warning):" -let msg_user_info = msg_message false 3 "(Unit test info):" +let log_fatal ?section ?print_action ?loc m = + log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m; + internal_error "Compiler Fatal Error" +let log_error = log_msg Error ?kind:None +let log_warning = log_msg Warning ?kind:None +let log_info = log_msg Info ?kind:None +let log_debug = log_msg Debug ?kind:None + +let stop_on_error () = + let count = error_count () in + if (0 < count) then + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" errors\n") + +let stop_on_warning () = + stop_on_error (); + let count = warning_count () in + if (0 < count) then + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" warnings\n") (* Compiler Internal Debug print *) let debug_msg expr = - if 4 <= !typer_verbose then (print_string expr; flush stdout) else () + if Debug <= typer_log_config.level then (print_string expr; flush stdout) let not_implemented_error () = internal_error "not implemented" + +let log_user_fatal section loc msg = + log_msg Fatal ~kind:"(Unit test fatal)" ~section ~loc msg; + user_error msg +let log_user_warning section loc msg = + log_msg Warning ~kind:"(Unit test warning)" ~section ~loc msg +let log_user_info section loc msg = + log_msg Info ~kind:"(Unit test info)" ~section ~loc msg ===================================== src/opslexp.ml ===================================== @@ -38,6 +38,9 @@ module S = Subst (* module L = List *) module DB = Debruijn +let error_tc = Log.log_error ~section:"TC" +let warning_tc = Log.log_warning ~section:"TC" + (* `conv_erase` is supposed to be safe according to the ICC papers. *) let conv_erase = true (* Makes conv ignore erased terms. *) @@ -161,7 +164,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = -> match default with | Some (v,default) -> lexp_whnf (push_susp default (S.substitute e')) ctx - | _ -> Log.msg_error "WHNF" l + | _ -> Log.log_error ~section:"WHNF" ~loc:l ("Unhandled constructor " ^ name ^ "in case expression"); mkCase (l, e, rt, branches, default) in @@ -399,7 +402,7 @@ let rec check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () - else (Log.msg_error "TC" (lexp_location e) + else (error_tc ~loc:(lexp_location e) ("Type mismatch for " ^ lexp_string (L.clean e) ^ " : " ^ lexp_string (L.clean t) ^ " != " @@ -409,7 +412,7 @@ let rec check'' erased ctx e = let s = check erased ctx t in (match lexp_whnf s ctx with | Sort _ -> () - | _ -> Log.msg_error "TC" (lexp_location t) + | _ -> error_tc ~loc:(lexp_location t) ("Not a proper type: " ^ lexp_string t)); (* FIXME: return the `sort` rather than the surrounding `lexp`! *) s in @@ -419,7 +422,7 @@ let rec check'' erased ctx e = | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) - -> (Log.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; + -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) @@ -440,7 +443,7 @@ let rec check'' erased ctx e = mkSort (l, Stype (mkSortLevel (SLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) - -> ((* Log.msg_error "TC" (lexp_location e) "Reached unreachable sort!"; + -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t, _) @@ -450,7 +453,7 @@ let rec check'' erased ctx e = (* FIXME: Check recursive references. *) | Var (((l, name), idx) as v) -> if DB.set_mem idx erased then - Log.msg_error "TC" l + error_tc ~loc:l ("Var `" ^ maybename name ^ "`" ^ " can't be used here, because it's `erasable`"); lookup_type ctx v @@ -483,14 +486,14 @@ let rec check'' erased ctx e = match sort_compose ctx l ak k1 k2 with | SortResult k -> k | SortInvalid - -> Log.msg_error "TC" l "Invalid arrow: inner TypelLevel argument"; + -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; mkSort (l, StypeOmega) | SortK1NotType - -> (Log.msg_error "TC" (lexp_location t1) + -> (error_tc ~loc:(lexp_location t1) "Not a proper type"; mkSort (l, StypeOmega)) | SortK2NotType - -> (Log.msg_error "TC" (lexp_location t2) + -> (error_tc ~loc:(lexp_location t2) "Not a proper type"; mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) @@ -508,12 +511,12 @@ let rec check'' erased ctx e = match lexp_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then - (Log.msg_error "TC" (lexp_location arg) + (error_tc ~loc:(lexp_location arg) "arg kind mismatch"; ()) else (); assert_type ctx arg t1 at; mkSusp t2 (S.substitute arg) - | _ -> (Log.msg_error "TC" (lexp_location arg) + | _ -> (error_tc ~loc:(lexp_location arg) ("Calling a non function (type = " ^ lexp_string ft ^ ")!"); ft)) @@ -539,14 +542,15 @@ let rec check'' erased ctx e = * in the plain `check` code! *) (Inverse_subst.apply_inv_subst level' (S.shift n)) - | tt -> Log.msg_error "TC" (lexp_location t) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string tt ^")"); - DB.print_lexp_ctx ictx; - (* Log.internal_error "Oops"; *) - level), + | tt -> error_tc ~loc:(lexp_location t) + ~print_action:(fun _ -> + DB.print_lexp_ctx ictx; print_newline () + ) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string tt ^")"); + level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, n + 1)) @@ -579,7 +583,7 @@ let rec check'' erased ctx e = (* We don't check aarg's type, because we assume that `check` * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (Log.msg_error "TC" l + | _,_ -> (error_tc ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in SMap.iter @@ -596,7 +600,7 @@ let rec check'' erased ctx e = (S.cons (Var (vdef, 0)) (S.mkShift s 1)) vdefs fieldtypes - | _,_ -> (Log.msg_error "TC" l + | _,_ -> (error_tc ~loc:l "Wrong number of args to constructor!"; (erased, ctx)) in let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in @@ -608,15 +612,15 @@ let rec check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 then - Log.msg_warning "TC" l "Redundant default clause"; + warning_tc ~loc:l "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in assert_type nctx d (mkSusp ret (S.shift 1)) (check (DB.set_sink 1 erased) nctx d) | None -> if diff > 0 then - Log.msg_error "TC" l ("Non-exhaustive match: " + error_tc ~loc:l ("Non-exhaustive match: " ^ string_of_int diff ^ " cases missing")) - | _,_ -> Log.msg_error "TC" l "Case on a non-inductive type!"); + | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); ret | Cons (t, (l, name)) -> (match lexp_whnf t ctx with @@ -644,10 +648,10 @@ let rec check'' erased ctx e = buildtype fargs) in buildtype fargs with Not_found - -> (Log.msg_error "TC" l + -> (error_tc ~loc:l ("Constructor \"" ^ name ^ "\" does not exist"); DB.type_int)) - | _ -> (Log.msg_error "TC" (lexp_location e) + | _ -> (error_tc ~loc:(lexp_location e) ("Cons of a non-inductive type: " ^ lexp_string t); DB.type_int)) ===================================== src/pexp.ml ===================================== @@ -25,7 +25,7 @@ open Sexp (* Symbol *) open Lexer open Grammar -let pexp_error = Log.msg_error "PEXP" +let pexp_error loc = Log.log_error ~section:"PEXP" ~loc (*************** The Pexp Parser *********************) ===================================== src/prelexer.ml ===================================== @@ -22,7 +22,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util -let prelexer_error = Log.msg_error "PRELEXER" +let prelexer_error loc = Log.log_error ~section:"PRELEXER" ~loc type pretoken = | Pretoken of location * string ===================================== src/sexp.ml ===================================== @@ -24,7 +24,8 @@ open Util open Prelexer open Grammar -let sexp_error = Log.msg_error "SEXP" +let sexp_error ?print_action loc msg = + Log.log_error ~section:"SEXP" ?print_action ~loc msg type integer = (* Num.num *) int type symbol = location * string ===================================== src/unification.ml ===================================== @@ -27,6 +27,8 @@ module DB = Debruijn (** Provide unify function for unifying two Lambda-Expression *) +let log_info = Log.log_info ~section:"UNIF" + (* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*) @@ -220,12 +222,11 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) | MVar (_, t, _) -> push_susp t s in match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible - -> print_string "Unification of metavar failed:\n "; - print_string ("?[" ^ subst_string s ^ "]"); - print_string "\nAgainst:\n "; - lexp_print lxp; - print_string "\n"; - None + -> log_info ?loc:None ("Unification of metavar failed:\n " + ^ "?[" ^ subst_string s ^ "]" + ^ "\nAgainst:\n " + ^ lexp_string lxp ^ "\n"); + None | lxp' when occurs_in idx lxp' -> None | lxp' -> metavar_table := associate idx lxp' (!metavar_table); @@ -233,11 +234,12 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) | Some [] as r -> r (* FIXME: Let's ignore the error for now. *) | _ - -> print_string ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - Some [] in + -> log_info ?loc:None + ("Unification of metavar type failed:\n " + ^ lexp_string (Lexp.clean t) ^ " != " + ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + Some [] in match lxp2 with | Metavar (idx2, s2, _) -> if idx = idx2 then ===================================== src/util.ml ===================================== @@ -106,3 +106,13 @@ let padding_left (str: string ) (dim: int ) (char_: char) : string = let diff = (dim - string_width str) in let lpad = max diff 0 in (String.make lpad char_) ^ str + +let option_default (default : 'a) (opt : 'a option) : 'a = + match opt with + | None -> default + | Some x -> x + +let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = + match opt with + | None -> None + | Some x -> Some (fn x) ===================================== tests/utest_lib.ml ===================================== @@ -76,7 +76,7 @@ let global_ftitle = ref "" let set_verbose lvl = global_verbose_lvl := lvl; - (if lvl >= 3 then Log.typer_verbose := 20 else Log.typer_verbose := (-1)) + Log.set_typer_log_level (if lvl >= 3 then Log.Debug else Log.Nothing) let arg_defs = [ ("--verbose=", View it on GitLab: https://gitlab.com/monnier/typer/compare/a96034f0f65cbcda9f6eef8e49b4e2464a… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/a96034f0f65cbcda9f6eef8e49b4e2464a… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Août 2019