Re: [isabelle] Code generator: overloaded numeric constants



Hi Florian,

I'd like to stay with just the "syntactic" number, plus, etc. classes, since our Haskell number instances don't necessarily satisfy the ring axioms. So I can generate reasonable Haskell code from this Isabelle definition:

  definition
    "foo (x::'a::{number,plus,times}) y = x + number_of 2 * y"

However I don't want to have to insert "number_of" functions wherever I'm using a numeric literal. But right now I don't see any way of generating reasonable Haskell code from this more readable version of the above definition:

  definition
    "foo (x::'a::{number,plus,times}) y = x + 2 * y"

Is there any way to get the code generator to work well on this second form?

Thanks,
-john

On Jun 11, 2010, at 11:49 PM, Florian Haftmann wrote:

Hi John,

the number class in Isabelle/HOL is a little bit arcane;  concerning
code generation, you may use numerals on numeric types (nat, int, rat,
real), but not polymorphic ('a::number).  Otherwise you only get
formally and partially correct code:

 foo :: forall a. (Plus a, Times a, Number a) => a -> a -> a;
 foo x y =
   plus x (times (number_of (error "Bit0" (error "Bit1" (error
"Pls")))) y);

In typical Isabelle/HOL specifications, the number class will not show
up that often since it is only syntactic -- a classical joke is that you cannot prove "2 + 2 = (4::'a::number)". Of more relevance is the class
number_ring which describes structures in which the integers can be
embedded semantically (number_of = of_int).  This you can use to
circumvent the number_of problem: instead of

 definition double :: "'a::number_ring ⇒ 'a" where
   "double k = 2 * k"

write

 definition double :: "'a::number_ring ⇒ 'a" where
   "double k = of_int 2 * k"

Since (number_of = of_int), you can even prove the second version from
the first.  This could also be done by the preprocessor but would
require writing a simproc since the naive rewrite (number_of k = of_int
(number_of k)) does not terminate.

Hope this helps,
	Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de


Attachment: smime.p7s
Description: S/MIME cryptographic signature



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