Simon Génier pushed to branch simon--pp-print-lctx at Stefan / Typer

Commits: 023768b1 by Simon Génier at 2023-03-24T17:03:13-04:00 Dump lctx from typer.exe rather than debug_util.exe.

- - - - -

3 changed files:

- debug_util.ml - src/lctx.ml - typer.ml

Changes:

===================================== debug_util.ml ===================================== @@ -68,10 +68,6 @@ let get_p_option name = let arg_defs = [ ("-typecheck", Arg.Unit (add_p_option "typecheck"), " Enable type checking"); - - (* Debug *) - ("-lctx", - Arg.Unit (add_p_option "lctx"), " Print lexp context"); ("-rctx", Arg.Unit (add_p_option "rctx"), " Print runtime context"); ("-all", @@ -144,9 +140,6 @@ let main () = print_string (" " ^ (make_line '-' 76)); print_string "\n";));

- (if (get_p_option "lctx") then( - Lctx.print (ectx_to_lctx nctx); print_string "\n")); - (* Type erasure *) let _, clean_lxp = List.fold_left_map OL.clean_decls (ectx_to_lctx nctx) lexps

===================================== src/lctx.ml ===================================== @@ -113,11 +113,15 @@ let summarize ~(around : int) (lctx : t) : unit = print_endline "This context was trucated. Pass the option -Vfull-lctx to view it in full."

(** Only print user defined variables *) -let print (lctx : t) : unit = +let pp_print (f : Format.formatter) (lctx : t) : unit = let ranges = [(0, Myers.length lctx - !builtin_size)] in - let f = Fmt.formatter_of_out_channel stdout in Format.fprintf f "%a" (pp_print_ranges ~ranges) lctx

+(** Only print user defined variables *) +let print (lctx : t) : unit = + let f = Fmt.formatter_of_out_channel stdout in + pp_print f lctx + (** Print the whole context, including builtins. *) let dump (lctx : t) : unit = let ranges = [(0, Myers.length lctx)] in

===================================== typer.ml ===================================== @@ -188,6 +188,29 @@ let dump_elexps_main argv = in ()

+let dump_lctx_main argv = + let usage = Sys.executable_name ^ " dump-lexps <file> …" in + parse_args ~arg_defs:dump_lexps_arg_defs argv usage; + + let dump_lexps_of_file ectx path = + let source = Source.of_path path in + let pretokens = Prelexer.prelex source in + let tokens = Lexer.lex Grammar.default_stt pretokens in + let _, ectx' = Elab.lexp_p_decls [] tokens ectx in + let f = Fmt.formatter_of_out_channel stdout in + if !print_indices then + Lexp.pp_enable_print_indices f; + Format.fprintf f "%a@." Lctx.pp_print (ectx_to_lctx ectx'); + ectx' + in + let _ = + List.fold_left + dump_lexps_of_file + Elab.default_ectx + (list_input_files ()) + in + () + let main () = let command, argv = if Array.length Sys.argv <= 1 @@ -214,6 +237,7 @@ let main () = | "dump-tokens" -> dump_tokens_main argv | "dump-lexps" -> dump_lexps_main argv | "dump-elexps" -> dump_elexps_main argv + | "dump-lctx" -> dump_lctx_main argv | _ -> eprintf {|unknown command "%s"|} command; exit 1)

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/023768b1d7c1c94d1ff44ee7037e3e3b0c...