Dear all,
recently I was working a lot with adhoc_overloading. Doing so I often
experienced that my output differed from my input (w.r.t. adhoc
overloading). At that time I did not think too much about it since being
able to input readable formulas was quite enough. But today I suddenly
had an idea what could cause this (to me) strange behavior.
First a minimal example. I introduce a new constant that will be overloaded.
consts F :: "'a ⇒ 'a" ("FOO")
Then I add a locale and register its fixed constant for adhoc overlaoding:
locale a =
fixes f :: "'a ⇒ 'a"
assumes nothing: "f x ≡ x"
begin
adhoc_overloading
F f
end
Inside this locale I can enter "FOO" instead of "f" and "f" will be
printed as "FOO", as I would expect.
Now lets introduce another locale that is built on top of the first one
locale set_a =
elt: a elt_f for elt_f :: "'a ⇒ 'a"
begin
adhoc_overloading
F elt_f
definition "set_f A = elt_f ` A"
adhoc_overloading
F set_f
We now have adhoc overloading for elt_f as well as set_f. For inputting
terms this works as I would expect (i.e., I get an error if it is not
clear from the type which of elt_f and set_f should be inserted for any
given FOO and the corresponding constant, otherwise).
However, as output for
term "A (FOO {x. True})"
I obtain
"A (set_a.set_f FOO {x. True})"
while I would have liked to get
"A (FOO {x. True})"
since this is more readable. Looking at the code of "insert_overloaded"
inside adhoc_overloading.ML reveals a use of "Pattern.rewrite_term",
which seems to do bottom-up rewriting.
So my idea was to instead use top-down rewriting (i.e., first replace
maximal subterms that fit a given pattern). This is what
"Pattern.rewrite_term_top" does, right? So after replacing
"rewrite_term" by "rewrite_term_top", I get the expected results.
Now my question. Can anybody think of a reason why "rewrite_term_top"
would not be generally preferable over "rewrite_term" inside of
"insert_overloaded"?
If not, could one of the devs incorporate this tiny change please?
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
