From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
I found that normalisation introduces fresh type variables when the word type from
HOL-Word occurs in the goal statement. Here is a tiny example:
theory Scratch imports "~~/src/HOL/Word/Word" begin
lemma "(2 + 3 :: 4 word) = 3 + 2"
using [[show_consts, show_sorts]]
apply normalization
Before the call to normalization, there are no type variables in the goal state. The
normalization method turns the goal into the following:
uint (Word.Word (snd (divmod_int (uint (Word.Word 3) + uint (Word.Word 2)) 4294967296))) =
uint (Word.Word (snd (divmod_int (uint (Word.Word 2) + uint (Word.Word 3)) 4294967296)))
The unexpected thing is that each occurrence of Word.Word now has a different type with a
schematic type variable, i.e., Word.Word :: int => ?'a word, Word.Word :: int => ?'b word,
etc. Correspondingly, every occurrence of uint also has a type variable in there.
All the new type variables have sort {}. Consequently, I cannot use many of the other
methods like simp that do not like such schematic type variables.
Why does normalization introduce these type variables at all? Is this intended? How can I
disable this feature or is this inherent to NBE?
Cheers,
Andreas
From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
Why does normalization introduce these type variables at all? Is this
intended? How can I disable this feature or is this inherent to NBE?
nbe itself does not even permit schematic type variables in results.
The problem stems from the postprocessor. I guess it is a problem with
hidden polymorphism which escaped attention so far, but it will need
further time to investigate this.
An even more minimal example:
theory Foo
imports "~~/src/HOL/Word/Word"
begindefinition
"example = (1 + 1 :: 4 word)"ML {* Code_Simp.dynamic_value @{theory} @{term example} *}
ML {* Nbe.dynamic_value @{theory} @{term example} *}
Cheers,
Florian
signature.asc
From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
Thanks for looking into this.
The last line just raises Option (line 81 of General/basics.ML). I got these exceptions
quite often, but I thought that I had just done something wrong.
Andreas
Last updated: Mar 29 2024 at 08:18 UTC