`term_to_string` being total implies ⊥

[W95Psp]

Hi,

term_to_string is a Tot computation despite being impure because sensitive to the options hide_uvar_nums, print_bound_var_types, print_effect_args, print_implicits, print_real_names, print_universes and ugly. Thus one can derive ⊥ easily by observing the impurity of term_to_string:

module TermToStringFalse
open FStar.Tactics

#push-options "--ugly" (* `ulgy` adds parenthesis around applications *)
let a (): Lemma (term_to_string (`1 1) == "(1 1)") = ()
#pop-options
let b (): Lemma (term_to_string (`1 1) == "1 1") = ()

let proof (): Lemma False = a (); b ()

I see three different ways of fixing that:

1. make term_to_string effectful in Tac;
2. push blank options when calling term_to_string and pop them right after (though this is quite not user friendly, one might want to print a term with certain printing options);
3. parameterize term_to_string by printing options.

To me exposing term prettyprinting as Tot is pleasant since it is supposed to be pure, but (3) requires a lot of verbosity in FStar.Syntax.Print (at least without monads), if we want to make those function really pure. (Alternatively, a parametrized term_to_string reflection could just push/pop options before and after calling the compiler's term_to_string)

[nikswamy]

We discussed this at a recent F* meeting. The simplest and cleanest fix seems to be option 1. Do you have a scenario where you specifically rely on the totality of the printer?

[W95Psp]

Sorry for the late of my reply. Yes, after a bit of thinking, I guess this is the best option: the current pretty-printer is not total, thus it should be marked as Tac.

I think that even if I came up with a scenario requiring a total pretty-printer, with the reflection API being rather complete, the best solution should be to write a pretty-printer within F* itself.