Email Gateway (Aug 18 2022 at 18:57): Email Gateway (Aug 18 2022 at 18:57):From: Makarius <makarius@sketis.net>
(I am answering this on isabelle-users, not on isabelle-dev, because
Isabelle/ML is perfectly normal user space; "the ML level" is actually
part of the Isar toplevel. I also refrain from cross-posting (!) to
isabelle-dev, because that list is de-facto a subset of isabelle-users
and duplicates don't help.)
The beta contraction observed above is actually part of the treatment of
term abbreviations, which uses principles from higher-order rewriting and
that includes beta-contraction. Abbreviations are treated both in the
"term check" phase for input and the "term uncheck" phase for output. So
it is hard to input terms that are not beta normal, and the following uses
some plain Isabelle/Isar/ML:
ML {*
val t = @{term "%x::'a. x"} $ @{term "a::'a"};
val u = singleton (Syntax.uncheck_terms @{context}) t;
*}
val t = Abs ("x", "'a", Bound 0) $ Free ("a", "'a"): term
val u = Free ("a", "'a"): term
The actual pretty printing is done in the so-called "unparse" phase and is
innocent here: it does not do any beta contraction on its own. You could
even try to make your own low-level printing for diagnostic purposes based
on Syntax.uncheck_terms alone, which is mainly the pretty printer only.
In order to disable merely the contraction of abbreviations (with its beta
conversion) during term-unchecking, you can use the following suitable
configuration option on the context:
declare [[show_abbrevs = false]]
Of course you need to use the correct context for printing to see the
effect.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC