Email Gateway (Aug 22 2022 at 10:55): Email Gateway (Aug 22 2022 at 10:55):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I have this very simple function:
fun rightUnitAppend'0 :: "'T'00 list ⇒ bool" where
"rightUnitAppend'0 (l1'00::'T'00 List.list) = (case l1'00 of [] => True
| (x'6::'T'00) # (x::'T'00 list) => rightUnitAppend'0 x)"
Now, if I look at the generated theorem:
thm rightUnitAppend'0.simps
... and hover over the "x", I get the markup
:: ?'a list
bound variable
However, the markup for "x'6" is:
:: ?'T'00.0
bound variable
Clearly, one of them is incorrect, because it should be either "?'a" or
"?'T'00.0" in both cases. This looks like a problem in the unchecking of
case expressions, because when I look at the term representation:
declare [[ML_print_depth=100]]
MLThm.prop_of @{thm rightUnitAppend'0.simps}
... all I get is "?'T'00.0", as expected. "?'a" is nowhere to be found.
Cheers
Lars
Email Gateway (Aug 22 2022 at 10:55):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Lars,
thanks for the report. Something indeed went wrong during uncheck. It
has to do with eta contracted arguments to the case combinator and shows
already at this minimized example:
term "case_list undefined (λx. f) (xs :: 't list)"
(I resist to comment on your choice of names in your example; I hope
they are automatically generated ;-) )
The uncheck phase has to eta expand before printing and picks the wrong
types from elsewhere. I have a local changeset to improve on that, which
I will test and push soon.
BTW this was a nice opportunity for me to test the newly available
ML_debugger (in the repository)---which is awesome! I could locate the
problem and (hopefully) improve the situation without inserting a single
print statement :-)
Dmitriy
Last updated: Nov 21 2024 at 12:39 UTC