Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Folding abbreviations with TYPE(_) parameters


view this post on Zulip Email Gateway (Jul 14 2020 at 12:29):

From: Mikhail Mandrykin <mandrykin@ispras.ru>
Hello!

I have a question about the current situation regarding abbreviations
with dummy parameters of type "'a itself" e.g.
⬚‹abbreviation "to_bounds TYPE('a::len) x ≡ uint (word_of_int x :: 'a
word)"›
Here "TYPE('a)" is used to pass the length of the machine word
represented by the corresponding numeral type. It looks like a more or
less proper way to define and use such abbreviations, in particular it's
what Isabelle automatically does for abbreviations with hidden
polymorphism: for
⬚‹
abbreviation "to_bounds' x ≡ uint (word_of_int x)"
term to_bounds'

Isabelle gives ▩‹"to_bounds'" :: "'a itself ⇒ int ⇒ int"›.
However, when I try to use such an abbreviation, it's not folded back
when pretty-printing:
⬚‹term "to_bounds TYPE(8) 534"›
simply prints ▩‹"uint (word_of_int 534)" :: "int"› instead of
▩‹"to_bounds TYPE(8) 534" :: "int"›. The question is whether there's
some pragmatic reason for not fully supporting such abbreviations?

From technical point if view I looked at the implementation of constant
abbreviation folding in Pure and the code looks somewhat dubious about
that. On the one hand, Consts.abbreviate calls
Term.close_schematic_term, which adds dummy "TYPE(_)" parameters to
expose the hidden polymorphism in the RHS of the abbreviation. On the
other hand, a local function strip_abss, which is used by
Consts.abbreviate only strips parameters that occur in the RHS as term
variables and does not take into account type variables. But those
variables of type "'a itself" usually don't occur directly in the RHS
and therefore the reverse abbreviation mechanism tries to fold an
abstraction of the form "λ (_ :: 'a itself). t" instead of the term "t"
and this is not how the unfolded abbreviation is actually represented. I
though it might be better to explicitly support those parameters of type
"'a itself" as instances of the singleton type Pure.type and try to fold
"RHS ('a)" → "LHS v_1 ... v_n (Pure.type :: 'a) v_{n+1} ... v_m" (i.e.
instantiate the LHS and RHS with the singleton Pure.type instead of the
variable, if it does not occur in RHS as a variable), which is supported
by Pattern.match_rew used in Proof_Context.contract_abbrevs. I
implemented a patch based on this idea (attached as
contract_TYPE_abbrevs.patch). It works for the example given above, some
more examples that we have in our formalizations and also passes
"regular" tests of building with "isabelle build -a" on my machine. A
notable quirk of this approach is that it would also fold abbreviations
even if the type does not occur in the RHS by introducing fresh type
variables e.g. folding "f x" to "u TYPE(?'a) TYPE(?'b)" when given "u
TYPE('a) TYPE('b) x ≡ f x". This can be prevented by checking occurrence
of the type variable in the RHS, but I'm not sure how to treat such
cases since they are quite strange anyway. So doesn't this approach have
some undesirable pitfalls or the support was simply missing due to lack
of use cases? The feature seems useful for handling types with phantom
parameters that represent some additional information such as word or
pointer type size.

Regards,
Mikhail
contract_TYPE_abbrevs.patch


Last updated: Sep 28 2021 at 20:18 UTC