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)"
  by (simp add: num_of number_of_is_id)

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.