Re: [isabelle] code generation for saturated naturals

Hi Brian,

> This brings up another issue: It is generally undesirable to have two
> different copies of the same function around if they are both in
> common use, since this means that we would have to maintain two
> similar-looking but separate sets of simp rules. This was the
> motivation for making "int :: nat => int" into an abbreviation for
> "of_nat :: nat => int" a few years ago; it let us remove a lot of
> duplication and simpset inconsistencies from the standard library.
> So here's what I propose for the saturated arithmetic library: Rename
> the current constant "Sat :: nat => 'a sat" to something like
> Abs_sat', and reintroduce the user-friendly name "Sat" as a
> type-constrained abbreviation for "of_nat".
> The only reason I'm hesitant to make this change myself is that I
> don't know how it might affect code generation -- currently "Sat" has
> some special status because it appears in the [code abstype]
> declaration.

And according to the type discipline of the code generator it must
remain so.  But we need the "old" Sat anyway for bootstrap reasons.  So
I would suggest:

* Abs_sat from typedef
* SAT is what is now called Sat
* Sat is abbreviation for of_nat
* simprule SAT = of_nat
* maybe hide Abs_sat and SAT after bootstrap

I remember a similar issue concerning of_nat can be found in
Code_Numeral, which also contains such duplication due to bootstrap reasons.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.