Simon Génier pushed to branch master at Stefan / Typer
Commits: d17622a1 by Simon Génier at 2021-03-08T12:46:52-05:00 Truncate the lexp context that is printed on error.
You can still opt in the whole thing by passing -Vfull-lctx.
- - - - - a2a6e95e by Simon Génier at 2021-03-08T13:24:54-05:00 Merge branch 'truncate-lctx'
- - - - -
2 changed files:
- src/REPL.ml - src/debruijn.ml
Changes:
===================================== src/REPL.ml ===================================== @@ -286,6 +286,9 @@ let arg_defs = [ ("--verbosity", Arg.String Log.set_typer_log_level_str, "Set the logging level"); ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); + ("-Vfull-lctx", + Arg.Set Debruijn.log_full_lctx, + "Print the full lexp context on error."); (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) (*"-I", Arg.String (fun f -> searchpath := f::!searchpath),
===================================== src/debruijn.ml ===================================== @@ -261,105 +261,123 @@ let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx
-(* Print context *) -let print_lexp_ctx_n (ctx : lexp_context) start = - let n = (M.length ctx) - 1 in - - print_string (make_title " LEXP CONTEXT "); - - make_rheader [ - (Some ('l', 7), "INDEX"); - (Some ('l', 4), "OFF"); - (Some ('l', 10), "NAME"); - (Some ('l', 42), "VALUE:TYPE")]; - - print_string (make_sep '-'); - - (* it is annoying to print according to SMap order *) - (* let's use myers list order *) - let rec extract_names (lst: lexp_context) acc = - let names = ref [] in - for i = start to n do - let name = match (M.nth (n - i) lst) with - | ((_, Some name), _, _) -> name - | _ -> "" in - names := name::!names - done; !names in - - let ord = extract_names ctx [] in - - let rec print idx ord = - match ord with - | [] -> () - | hd::tl ->( - - print_string " | "; lalign_print_int (n - idx - 1) 7; - print_string " | "; - - let ptr_str = " | | | | " in - - try let r, name, exp, tp = - match env_lookup_by_index (n - idx - 1) ctx with - | ((_, name), LetDef (r, exp), tp) -> r, name, Some exp, tp - | ((_, name), _, tp) -> 0, name, None, tp in - - (* Print env Info *) - lalign_print_int r 4; - print_string " | "; - lalign_print_string (maybename name) 10; (* name must match *) - print_string " | "; - - let _ = match exp with - | None -> print_string "<var>" - | Some exp -> ( - let str = lexp_str (!debug_ppctx) exp in - let str = (match str_split str '\n' with - | hd::tl -> print_string hd; tl - | _ -> []) in - - List.iter (fun elem -> - print_string ("\n" ^ ptr_str ^ elem)) str) in - - print_string (": "); lexp_print tp; print_string "\n"; - - print (idx + 1) tl - - with Not_found -> - (print_string "Not_found |\n"; print (idx + 1) tl)) in - - print (start - 1) ord; print_string (make_sep '=') - +let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = + print_string (make_title " LEXP CONTEXT "); + + make_rheader + [(Some ('l', 7), "INDEX"); + (Some ('l', 4), "OFF"); + (Some ('l', 10), "NAME"); + (Some ('l', 42), "VALUE : TYPE")]; + + print_string (make_sep '-'); + + let prefix = " | | | | " in + + let print i = + try + let r, name, lexp, ty = + match env_lookup_by_index i ctx with + | ((_, name), LetDef (r, exp), ty) -> r, name, Some exp, ty + | ((_, name), _, ty) -> 0, name, None, ty + in + let name' = maybename name in + let short_name = + if String.length name' > 10 + then + String.sub name' 0 9 ^ "…" + else name' + in + Printf.printf " | %-7d | %-4d | %-10s | " i r short_name; + (match lexp with + | None -> print_string "<var>" + | Some lexp + -> (let str = lexp_str (!debug_ppctx) lexp in + let strs = + match String.split_on_char '\n' str with + | hd :: tl -> print_string hd; tl + | [] -> [] + in + List.iter + (fun elem -> + print_newline (); + print_string prefix; + print_string elem) + strs)); + print_string " : "; + lexp_print ty; + print_newline () + with + | Not_found + -> print_endline " | %-7d | Not_found |" + in + + let rec print_range lower i = + let i' = i - 1 in + if i' >= lower + then + (print i'; + print_range lower i') + in + + let rec print_ranges = function + | [] -> () + | (lower, upper) :: ranges' + -> (print_range lower upper; + print_ranges ranges') + in + + print_ranges ranges; + print_string (make_sep '=')
(* Only print user defined variables *) -let print_lexp_ctx (ctx : lexp_context) = - print_lexp_ctx_n ctx !builtin_size +let print_lexp_ctx (lctx : lexp_context) : unit = + print_lexp_ctx_n lctx [(0, M.length lctx - !builtin_size)]
(* Dump the whole context *) -let dump_lexp_ctx (ctx : lexp_context) = - print_lexp_ctx_n ctx 0 +let dump_lexp_ctx (lctx : lexp_context) : unit = + print_lexp_ctx_n lctx [(0, M.length lctx)] + +let summarize_lctx (lctx : lexp_context) (at : int) : unit = + let ranges = + if at < 7 + then [(0, min (max (at + 2) 5) (M.length lctx))] + else [(at - 2, min (at + 2) (M.length lctx)); (0, 5)] + in + print_lexp_ctx_n lctx ranges; + print_endline "This context was trucated. Pass the option -Vfull-lctx to view it in full." + +let log_full_lctx = ref false
(* generic lookup *) let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = - let ((loc, oename), dbi) = v in - - try(let ret = (Myers.nth dbi ctx) in - let _ = match (ret, oename) with - | (((_, Some name), _, _), Some ename) -> - (* Check if names match *) - if not (ename = name) then - 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 -> fatal ~loc ("DeBruijn index " - ^ string_of_int dbi ^ " of `" ^ maybename oename - ^ "` out of bounds!") + let ((loc, oename), dbi) = v in + try + let ret = Myers.nth dbi ctx in + let _ = match (ret, oename) with + | (((_, Some name), _, _), Some ename) + -> (* Check if names match *) + if not (ename = name) then + let print_action = + if !log_full_lctx + then fun () -> (print_lexp_ctx ctx; print_newline ()) + else fun () -> summarize_lctx ctx dbi + in + let message = + "DeBruijn index " ^ string_of_int dbi + ^ " refers to wrong name. " + ^ "Expected: `" ^ ename + ^ "` got `" ^ name ^ "`" + in + fatal ~loc ~print_action message + | _ -> () in + + ret + with + | Not_found + -> fatal ~loc ("DeBruijn index " + ^ string_of_int dbi ^ " of `" ^ maybename oename + ^ "` out of bounds!")
let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/77981fd4dc8bc6af20e1db5148a9fb14f...
Afficher les réponses par date