Some pretty printing failures

[mtzguido]

module Bad

let f (y:int) : x:int -> int = fun x -> x+y

let vquote = `%Prims._assert

let f = fun x ->
  match x with
  | 0 -> 0
  | _ -> x+1

let get_squash (#p:prop) (_:unit{p}) : squash p = ()

Result of --print:

module Bad

let f (y: int)   (x: int) : int = fun x -> x + y

let vquote = `%assert

let f =
  function
  | 0 -> 0
  | _ -> x + 1

let get_squash
      (#p: prop)
      (_:
          (_:
            unit
              { match _ with
                | _ -> p
                | _ -> False }))
    : squash p = ()

So: 1- pushed a binder from the type into a pattern, but the body did not change accordingly 2- Prims._assert gets replaced with assert in the vquote, which then does not parse 3- The contraction of fun x -> match x with ... does not take into account that x appears in the branches 4- Some weird thing with nameless refinements.

These seem to be all the parsing failures we get if we pretty-print the entire library, so not too bad!

[amosr]

Hi Guido, I just noticed an issue with pretty-printing after normalising with nbe inside a tactic. It looks like a different case to the above, but I thought it looked related. Is it OK to post as a comment here, or would it be better as a separate issue?

(* Strange pretty-printing behaviour with nbe and pattern-matching. *)
(* Examples use dump tactic to show pretty-printed expressions after simplifying - the actual assertion is not interesting *)

module PrettyPrint

let ok (): unit =
  (* This example pretty-prints ok: snd is printed as something like `match (_, _2) -> _2` *)
  assert (exists e. e == snd #unit #unit) by
    (FStar.Tactics.norm [primops; iota; zeta; delta]; FStar.Tactics.dump "ok")

let nok (): unit =
  (* If we add `nbe` to the norm tactic, the body of `snd` is pretty-printed as `match (_, _) -> _` where we lose the body *)
  assert (exists e. e == snd #unit #unit) by
    (FStar.Tactics.norm [nbe; primops; iota; zeta; delta]; FStar.Tactics.dump "nok")

[mtzguido]

Hi Amos, thanks for reporting. It's indeed related, resugaring is not very smart about which names nor shadowing. You can avoid that by using --print_full_names, at the cost of some verbosity.

https://github.com/FStarLang/FStar/issues/2808 is also related to that. I will give this a shot to see if we can improve it.

However that particular problem with NBE is fixable, we just need to keep track of the names when translating. Pushing a fix soon.

[amosr]

Thanks Guido! Your recent commit works for me (as does --print_full_names)