From ce3b6a862ed0119e5119a72ab4421ae3f0623ebd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 10 Sep 2024 07:26:26 -0700 Subject: [PATCH] Env: filtering units from environment print --- src/checker/Pulse.Typing.Env.fst | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/checker/Pulse.Typing.Env.fst b/src/checker/Pulse.Typing.Env.fst index 004d5f6a9..29e809133 100644 --- a/src/checker/Pulse.Typing.Env.fst +++ b/src/checker/Pulse.Typing.Env.fst @@ -373,13 +373,25 @@ let rec separate_map (sep: document) (f : 'a -> T.Tac document) (l : list 'a) : | x::xs -> f x ^^ sep ^/^ separate_map sep f xs let env_to_doc (e:env) : T.Tac document = + let erase_units = not (Pulse.Config.debug_flag "no_filter_env") in let pp1 : ((var & typ) & ppname) -> T.Tac document = fun ((n, t), x) -> infix 2 1 colon (doc_of_string (T.unseal x.name ^ "#" ^ string_of_int n)) (align (Pulse.Syntax.Printer.term_to_doc t)) in - brackets (separate_map comma pp1 (T.zip e.bs e.names)) + let maybe_filter vtns = + if erase_units then + vtns |> T.filter (fun ((n, t), x) -> + let is_unit = FStar.Reflection.TermEq.term_eq t (`unit) in + let x : ppname = x in + let is_wild = T.unseal x.name = "_" in + not (is_unit && is_wild) + ) + else + vtns + in + T.zip e.bs e.names |> maybe_filter |> separate_map comma pp1 |> brackets let get_range (g:env) (r:option range) : T.Tac range = match r with