Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] normalization method introduces schematic type...


view this post on Zulip Email Gateway (Aug 19 2022 at 11:18):

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

view this post on Zulip Email Gateway (Aug 19 2022 at 11:20):

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"
begin

definition
"example = (1 + 1 :: 4 word)"

ML {* Code_Simp.dynamic_value @{theory} @{term example} *}
ML {* Nbe.dynamic_value @{theory} @{term example} *}

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 11:20):

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