*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] Code generator: overloaded numeric constants*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Mon, 14 Jun 2010 10:18:22 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <0A0B0528-87AC-4765-9B08-14FB6E0861D8@galois.com>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <C8BDF99A-E03A-4507-B1FB-158724B9587C@galois.com> <4C132DFC.4060301@informatik.tu-muenchen.de> <0A0B0528-87AC-4765-9B08-14FB6E0861D8@galois.com>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.9) Gecko/20100423 Thunderbird/3.0.4

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

**References**:**[isabelle] Code generator: overloaded numeric constants***From:*John Matthews

**Re: [isabelle] Code generator: overloaded numeric constants***From:*Florian Haftmann

**Re: [isabelle] Code generator: overloaded numeric constants***From:*John Matthews

- Previous by Date: Re: [isabelle] Code generator "eq" instances
- Next by Date: Re: [isabelle] safe for boolean equality
- Previous by Thread: Re: [isabelle] Code generator: overloaded numeric constants
- Next by Thread: [isabelle] Haskell code generation feature request
- Cl-isabelle-users June 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list