# Re: [isabelle] Code generator: overloaded numeric constants

```Hi John,

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

the inherent problem here is that the Isabelle and Haskell concept of
numeral is quite different.  In the attached theory I have spelled out
what is the best possible solution I can imagine for this discrepancy
using the preprocessor:

a) For instances of number_ring, a substitution number_of k ~> of_int
(number_of k) is used.

b) For other polymorphic numeral expressions, the class number_num can
be used which can be provided with custom instances; then a substitution
number_of k ~> num_of (number_of k) can be applied.

I'm not quite sure whether this solves your problem, but if yes I will
include this into library (or even the Code_Integer theory).

Cheers,
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
```
```theory Number
imports Main Code_Integer
begin

lemma number_of_int:
"number_of k = (of_int (number_of k) :: 'a::number_ring)"
by simp

class number_num = number +
fixes num_of :: "int \<Rightarrow> 'a"
assumes num_of: "num_of = number_of"

lemma number_of_num_of:
"number_of k = num_of (number_of k)"

instantiation nat :: number_num
begin

definition "num_of = nat"

instance proof
qed (simp add: num_of_nat_def nat_number_of_def number_of_is_id expand_fun_eq)

end

setup {*
let
val rewrite_ring =
let
val thm = mk_eq @{thm number_of_int};
val arg = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) thm;
in fn ct => Thm.instantiate ([], [(arg, ct)]) thm end;
val rewrite_num =
let
val thm = mk_eq @{thm number_of_num_of};
val arg = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) thm;
in fn ct => Thm.instantiate ([], [(arg, ct)]) thm end;
fun select_rewrite sort = if Sign.subsort @{theory} (sort, @{sort number_ring})
then SOME rewrite_ring
else if Sign.subsort @{theory} (sort, @{sort number_num})
then SOME rewrite_num
else NONE;
fun sort_of ct = case (range_type o snd o dest_Const o fst o dest_comb o Thm.term_of) ct
of T as Type _ => NONE
| T => SOME (Type.sort_of_atyp T);
fun rewrite ct = case sort_of ct
of SOME sort => (case select_rewrite sort
of SOME f => SOME (f (Thm.dest_arg ct))
| NONE => NONE)
| NONE => NONE;
val simproc = Simplifier.make_simproc { name = "number_of_int",
lhss = [ at {cpat "number_of ?k"}], identifier = [], proc = fn phi => fn ss => rewrite };
in
Code_Preproc.map_pre (fn ss => ss addsimprocs [simproc])
end
*}

definition "example1 (a :: 'a::number_ring) = 4 * a"

definition "example2 (a :: 'a::{number_num, times}) = 4 * a"

code_thms example1 example2

export_code example1 example2 in Haskell file -

end```

Attachment: signature.asc
Description: OpenPGP digital signature

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