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

Commits: 9a8ba87a by Simon Génier at 2023-03-07T18:03:18-05:00 Use format to print values.

- - - - - 19c3ab7d by Simon Génier at 2023-03-07T18:03:25-05:00 Oops: missing closing parenthesis when printing an inductive type.

- - - - -

10 changed files:

- debug_util.ml - src/builtin.ml - src/elab.ml - src/env.ml - src/eval.ml - src/heap.ml - src/lexp.ml - tests/env_test.ml - tests/eval_test.ml - tests/utest_lib.ml

Changes:

===================================== debug_util.ml ===================================== @@ -158,13 +158,13 @@ let main () = let rctx = (try eval_decls_toplevel clean_lxp rctx; with e -> print_string reset; - print_rte_ctx (!global_eval_ctx); + Env.print_rctx ~start:0 (!global_eval_ctx); print_eval_trace None; raise e) in print_string reset;

(if (get_p_option "rctx") then( - print_rte_ctx rctx; print_string "\n")); + Env.print_rctx ~start:0 rctx));

(* Eval Each Expression *) print_string (make_title " Eval Print ");

===================================== src/builtin.ml ===================================== @@ -126,8 +126,8 @@ let v2o_list v = | _ -> log_raise_error ~loc:(E.value_location v) - "Failed to convert the %s with value:\n%s\n to a list." - (E.value_name v) (E.value_string v) + "Failed to convert to a list:\n%s\n" + (Env.string_of_value v) in v2o_list [] v

===================================== src/elab.ml ===================================== @@ -85,12 +85,10 @@ 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_indent_line (Lexp.to_string lexp) let value_print_details value () = - print_details value_name value_string value + print_indent_line (Env.string_of_value value)

let lexp_error loc lexp fmt = error ~loc ~print_action:(lexp_print_details lexp) fmt

===================================== src/env.ml ===================================== @@ -31,8 +31,6 @@ * --------------------------------------------------------------------------- *)

open Elexp -open Fmt (* make_title, table util *) -open Printf open Sexp

module M = Myers @@ -67,6 +65,8 @@ type value = (* Runtime Environ *) and runtime_env = (vname * value ref) M.myers

+let empty = M.nil + let rec value_equal a b = match a, b with | Vint (i1), Vint (i2) -> i1 = i2 @@ -103,105 +103,72 @@ let rec value_equal a b =

| _ -> false

-let rec value_eq_list a b = - match a, b with - | [], [] -> true - | v1::vv1, v2::vv2 -> value_equal v1 v2 && value_eq_list vv1 vv2 - | _ -> false - let value_location : value -> Source.Location.t = function | Vcons ((loc, _), _) -> loc | Closure (_, lxp, _) -> Elexp.location lxp (* location info was lost or never existed *) | _ -> Source.Location.dummy

-let rec value_name v = - match v with - | Vin _ -> "Vin" - | Vout _ -> "Vout" - | Vint _ -> "Vint" - | Vinteger _ -> "Vinteger" - | Vsexp _ -> "Vsexp" - | Vtype _ -> "Vtype" - | Vcons _ -> "Vcons" - | Vfloat _ -> "Vfloat" - | Vundefined -> "Vundefined" - | Vstring _ -> "Vstring" - | Closure _ -> "Closure" - | Vbuiltin _ -> "Vbuiltin" - | Vcommand _ -> "Vcommand" - | Vref v -> ("Vref of "^(value_name (!v))) - | Velabctx _ -> ("Velabctx") - | Varray _ -> ("Varray") - -let rec value_string v = - match v with - | Vin _ -> "in_channel" - | Vout _ -> "out_channel" - | Vundefined -> "<undefined!>" - | Vcommand _ -> "command" - | Vstring s -> """ ^ s ^ """ - | Vbuiltin s -> s - | Vint i -> string_of_int i - | Vinteger i -> Z.to_string i - | Vfloat f -> string_of_float f - | Vsexp s -> Sexp.to_string s - | Vtype e -> Lexp.to_string e - | Closure ((_, s), elexp, _) - -> "(lambda " ^ Lexp.maybename s ^ " -> " ^ Elexp.to_string elexp ^ ")" - | Vcons ((_, s), lst) - -> let args = List.fold_left - (fun str v -> str ^ " " ^ value_string v) - "" lst in - "(" ^ s ^ args ^ ")" - | Vref (v) -> ("Ref of "^(value_string (!v))) - | Velabctx _ -> ("Velabctx") - | Varray a -> if ( (Array.length a) = 0 ) - then "[]" - else ( let - str = (Array.fold_left - (fun str v -> (str^(value_string v)^";")) "" a) - in ("["^(String.sub str 0 ((String.length str) - 1))^"]") ) - -let value_print (vtp: value) = print_string (value_string vtp) - -let make_runtime_ctx = M.nil +let rec pp_print_value (f : Format.formatter) : value -> unit = + let open Format in + function + | Vin _ -> pp_print_string f "#<in_channel>" + | Vout _ -> pp_print_string f "#<out_channel>" + | Vundefined -> pp_print_string f "#<undefined!>" + | Vcommand _ -> pp_print_string f "#<command>" + | Velabctx _ -> pp_print_string f "#<elabctx>" + | Vstring (value) -> fprintf f "%S" value + | Vbuiltin (name) -> fprintf f "##%s" name + | Vint (value) -> pp_print_int f value + | Vinteger (value) -> Z.pp_print f value + | Vfloat (value) -> pp_print_float f value + | Vsexp (value) -> Sexp.pp_print f value + | Vtype (value) -> Lexp.pp_print f value + | Vref (value) -> fprintf f "Ref of %a" pp_print_value !value + + | Closure (param, body, _) + -> fprintf + f "@[<hov 1>(lambda %a ->@ %a)@]" + (Sexp.pp_print_vname ~default:"_") param + Elexp.pp_print body + + | Vcons (name, fields) + -> fprintf f "@[<hov 1>(%a" Sym.pp_print name; + List.iter (fun field -> fprintf f "@ %a" pp_print_value field) fields; + fprintf f ")@]" + + | Varray (elements) + -> fprintf + f "@[<hov 1>[%a]@]" + (pp_print_list ~pp_sep:(fun f () -> fprintf f ";@ ") pp_print_value) + (Array.to_list elements) + +let print_value : value -> unit = + Format.printf "%a" pp_print_value + +let string_of_value : value -> string = + Format.asprintf "%a" pp_print_value + +let pp_print_rctx + (f : Format.formatter) ~(start : int) (rctx : runtime_env) + : unit = + + let open Format in + pp_print_string f (Fmt.make_title "Environment"); + for i = start to Myers.length rctx - 1 do + let name, value = Myers.nth i rctx in + fprintf + f "@[<hov 2>%a =@ %a;@]@." + (Sexp.pp_print_vname ~default:"_") name + pp_print_value !value + done; + pp_print_string f (Fmt.make_sep '=') + +let print_rctx ~(start : int) : runtime_env -> unit = + Format.printf "%a" (pp_print_rctx ~start)

let get_rte_size (ctx: runtime_env): int = M.length ctx

-let print_myers_list l print_fun start = - let n = (M.length l) - 1 in - print_string (make_title " ENVIRONMENT "); - make_rheader [(None, "INDEX"); - (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")]; - print_string (make_sep '-'); - - for i = start to n do - printf " | %5d | " (n -i); - print_fun (M.nth (n - i) l); - done; - print_string (make_sep '=') - -let print_rte_ctx_n (ctx: runtime_env) start = - print_myers_list - ctx - (fun (n, vref) -> - let g = !vref in - let _ = - match n with - | (_, Some m) -> Printf.printf "%-12s | " m - | _ -> print_string (make_line ' ' 12); print_string " | " in - - value_print g; print_string "\n") start - -(* Only print user defined variables *) -let print_rte_ctx ctx = - print_rte_ctx_n ctx (!Lexp.builtin_size) - -(* Dump the whole context *) -let dump_rte_ctx ctx = - print_rte_ctx_n ctx 0 - let get_rte_variable (name: vname) (idx: int) (ctx: runtime_env): value = try @@ -213,7 +180,7 @@ let get_rte_variable (name: vname) (idx: int) then x else fatal - ~print_action:(fun () -> dump_rte_ctx ctx) + ~print_action:(fun () -> Format.printf "%a" (pp_print_rctx ~start:0) ctx) {|Variable lookup failure. Expected "%s[%d]" got "%s"|} n2 idx n1 | _ -> x with

===================================== src/eval.ml ===================================== @@ -48,7 +48,7 @@ type eval_debug_info = elexp list * elexp list

let dloc = dummy_location let global_eval_trace = ref ([], []) -let global_eval_ctx = ref make_runtime_ctx +let global_eval_ctx = ref Env.empty (* let eval_max_recursion_depth = ref 23000 *)

type builtin_function = @@ -110,9 +110,8 @@ let root_string () =

let trace_value (value : value) : string = sprintf - "\t> %s : %s\n\t> Root: %s\n" - (value_name value) - (value_string value) + "\t> %s\n\t> Root: %s\n" + (Env.string_of_value value) (root_string ())

let trace_elexp (elexp : elexp) : string = @@ -404,7 +403,7 @@ let file_read loc _depth args_val = match args_val with * or actually pay attention to the second arg. *) | [Vin channel; Vint _n] -> Vstring (input_line channel) | _ -> error loc ~print_action:(fun _ -> - List.iter (fun v -> value_print v; print_newline ()) args_val; + List.iter (fun v -> Env.print_value v; print_newline ()) args_val; ) "File.read expects an in_channel. Actual arguments:"

@@ -414,7 +413,7 @@ let file_write loc _depth args_val = match args_val with (* FIXME: This should be the unit value! *) Vundefined) | _ -> error loc ~print_action:(fun _ -> - List.iter (fun v -> value_print v; print_newline ()) args_val; + List.iter (fun v -> Env.print_value v; print_newline ()) args_val; ) "File.write expects an out_channel and a string. Actual arguments:"

@@ -656,7 +655,7 @@ and sexp_dispatch loc depth args = (* -------------------------------------------------------------------------- *) and print_eval_result i lxp = Printf.printf " Out[%02d] >> " i; - value_print lxp; + Env.print_value lxp; print_string "\n";

and print_typer_trace' trace = @@ -1104,7 +1103,7 @@ let debug_eval lxp ctx = let ectx = !global_eval_ctx in let eval_trace = fst (get_trace ()) in Log.log_info ~section:"EVAL" ~print_action:(fun _ -> - print_rte_ctx ectx; + Env.print_rctx ~start:(!Lexp.builtin_size) ectx; print_eval_trace (Some eval_trace) ) "Exception occured during evaluation in the following context:"; @@ -1203,7 +1202,7 @@ class ast_interpreter lctx = object let elexp = Opslexp.erase_type lctx lexp in debug_eval elexp rctx

- method print_rte_ctx = Env.print_rte_ctx rctx + method print_rte_ctx = Env.print_rctx ~start:(!Lexp.builtin_size) rctx

- method dump_rte_ctx = Env.dump_rte_ctx rctx + method dump_rte_ctx = Env.print_rctx ~start:0 rctx end

===================================== src/heap.ml ===================================== @@ -80,7 +80,7 @@ let store_header | Env.Vcons (symbol, []) -> let constructor, _ = IMap.find address !heap in constructor := Some symbol - | _ -> error ~loc "not a data constructor: %s" (Env.value_string datacons) + | _ -> error ~loc "not a data constructor: %s" (Env.string_of_value datacons)

(** If [address] points to an object of at least [cell_index + 1] cells, mutates the value at that index. *)

===================================== src/lexp.ml ===================================== @@ -914,7 +914,8 @@ let rec pp_print (f : Format.formatter) (e, _ : lexp) : unit = pp_print_params params end; - SMap.iter pp_print_cons constructors + SMap.iter pp_print_cons constructors; + fprintf f ")@]"

| Case (_, e, _, branches, default) -> let pp_print_binding f (_, name) =

===================================== tests/env_test.ml ===================================== @@ -56,7 +56,7 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> add_rte_variable n Vundefined ctx) rctx var in

- print_rte_ctx rctx; + Env.print_rctx ~start:0 rctx;

let rctx, _ = List.fold_left (fun (ctx, idx) (n, _, _) -> @@ -64,7 +64,7 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> (ctx, idx - 1)) (rctx, n) var in

- print_rte_ctx rctx); + Env.print_rctx ~start:0 rctx); success))

===================================== tests/eval_test.ml ===================================== @@ -468,7 +468,7 @@ let _ = (* The result should overflow *) try let result = (eval elxp rctx) in ut_string2 ("EXPECTED overflow for `" ^ str ^ "`\n"); - ut_string2 ("GOT: " ^ (value_string result) ^ "\n"); + ut_string2 ("GOT: " ^ (Env.string_of_value result) ^ "\n"); failure with | Log.Internal_error _ -> Log.clear_log (); success in

===================================== tests/utest_lib.ml ===================================== @@ -127,13 +127,13 @@ let _expect_equal_t equality_test to_string value expect = failure)

let print_value_list values = - List.fold_left (fun s v -> s ^ "\n" ^ Env.value_string v) "" values + List.fold_left (fun s v -> s ^ "\n" ^ Env.string_of_value v) "" values

let expect_equal_bool = _expect_equal_t Bool.equal string_of_bool let expect_equal_int = _expect_equal_t Int.equal string_of_int let expect_equal_float = _expect_equal_t Float.equal string_of_float let expect_equal_str = _expect_equal_t String.equal (fun g -> g) -let expect_equal_values = _expect_equal_t Env.value_eq_list print_value_list +let expect_equal_values = _expect_equal_t (List.equal Env.value_equal) print_value_list

let expect_equal_lexp = _expect_equal_t Lexp.eq Lexp.to_string let expect_conv_lexp ctx = _expect_equal_t (Opslexp.conv_p ctx) Lexp.to_string

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/205ad75ea2420512094ea2942b2442f97...