*To*: Dave Thayer <dathayer at microsoft.com>*Subject*: Re: [isabelle] No Code Equation for LIMSEQ*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Fri, 11 Nov 2011 11:20:25 +0100*Cc*: Tobias Nipkow <nipkow at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <717F714B587F944C88837A99AA4D008149DD65AA@TK5EX14MBXC111.redmond.corp.microsoft.com>*Organization*: Technische Universität München*References*: <717F714B587F944C88837A99AA4D008149DD634A@TK5EX14MBXC111.redmond.corp.microsoft.com> <4EBB7869.4030900@in.tum.de> <717F714B587F944C88837A99AA4D008149DD65AA@TK5EX14MBXC111.redmond.corp.microsoft.com>

Hi David, as floats are acceptable for you, you can directly compile real to float with: theory Code_Float imports Complex_Main "~~/src/HOL/Library/Code_Integer" begin code_type real (OCaml "float") code_const "0 :: real" (OCaml "0.0") declare zero_real_code[code inline del] code_const "1 :: real" (OCaml "1.0") declare one_real_code[code inline del] code_const "op + :: real \<Rightarrow> real \<Rightarrow> real" (OCaml "Pervasives.( +. )") code_const "op * :: real \<Rightarrow> real \<Rightarrow> real" (OCaml "Pervasives.( *. )") code_const "op - :: real \<Rightarrow> real \<Rightarrow> real" (OCaml "Pervasives.( -. )") code_const "op / :: real \<Rightarrow> real \<Rightarrow> real" (OCaml "Pervasives.( '/. )") code_const cos (OCaml "Pervasives.cos") declare cos_def[code del] code_const sin (OCaml "Pervasives.sin") declare sin_def[code del] code_const pi (OCaml "Pervasives.pi") declare pi_def[code del] code_const arctan (OCaml "Pervasives.atan") declare arctan_def[code del] code_const arccos (OCaml "Pervasives.acos") declare arccos_def[code del] code_const arcsin (OCaml "Pervasives.asin") declare arcsin_def[code del] definition "test_trig x y a = cos (arctan (y / x) + sin a - pi/(1 + 1 + 1 + 1))" export_code test_trig in OCaml module_name CodegenTest file - end I tried it in Isabelle 2009 (not 2009-2), and it generates the expected code, but I don't know if OCaml accepts this code. I have a problem with numerals (i.e. numbers greater 2, just write them as 1 + 1 + ... + 1). A good example how to map number types to special types for the code generator is "~~/src/HOL/Library/Code_Integer.thy". We do not provide these code generator setup, as obviously many equalities don't hold any more. For example, in Haskell: cos (pi / 2 :: Double) == 0 returns False. I hope this helps, Johannes Am Donnerstag, den 10.11.2011, 20:23 +0000 schrieb Dave Thayer: > We are trying to create hypothetical explanations couched in HOL terms for a set of orbital observations and create an executable piece of code that determines how well the observations act as a model for our theory. Therefore creating a function that accepts real values as floats is quite acceptable. > > David > > > -----Original Message----- > From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Tobias Nipkow > Sent: Wednesday, November 09, 2011 11:08 PM > To: cl-isabelle-users at lists.cam.ac.uk > Subject: Re: [isabelle] No Code Equation for LIMSEQ > > You are trying to generate code for real numbers and functions defined by limits. Such definitions are not executable. You have two choices: > you can generate code that utilizes machine floats, or you can generate code that realizes arbitrary precision interval arithmetic. The former is a quick hack, the latter is sound but more work. Depending on what you want, we can tell you how to do it. > > Tobias > > Am 10/11/2011 00:23, schrieb Dave Thayer: > > For technical reasons I am restricted at the moment to using > > Isabelle2009 I am trying to use code generation to generate code for trigonometric functions and other functions that utilize the real datatype. > > > > I have the following code that is attempting to exercise this ability. > > > > definition test_pi :: "real" where "test_pi = pi" > > definition test_sin :: "real => real" where "test_sin x = sin x" > > definition test_cos :: "real => real" where "test_cos x = cos x" > > definition test_tan :: "real => real" where "test_tan x = tan x" > > definition test_arcsin :: "real => real" where "test_arcsin x = arcsin x" > > definition test_arccos :: "real => real" where "test_arccos x = arccos x" > > definition test_arctan :: "real => real" where "test_arctan x = arctan x" > > definition test_trig :: "real => real => real => real" where "test_trig x y a = cos (arctan (y / x) + sin a - pi/4)" > > > > export_code > > test_pi test_sin test_cos test_tan > > test_arcsin test_arccos test_arctan > > test_trig > > in OCaml > > module_name "TestCodeGen" > > file "TestCodeGen3.ml" > > > > I am getting the following error message ### No code equation for > > LIMSEQ, The > > > > Does anybody know where the code equations for LIMSEQ are defined? > > I have looked through the HOL/Library but found nothing so far. > > > > Thank you for your time, > > David Thayer > > >

**References**:**[isabelle] No Code Equation for LIMSEQ***From:*Dave Thayer

**Re: [isabelle] No Code Equation for LIMSEQ***From:*Tobias Nipkow

**Re: [isabelle] No Code Equation for LIMSEQ***From:*Dave Thayer

- Previous by Date: Re: [isabelle] Subset Types
- Next by Date: Re: [isabelle] No Code Equation for LIMSEQ
- Previous by Thread: Re: [isabelle] No Code Equation for LIMSEQ
- Next by Thread: Re: [isabelle] No Code Equation for LIMSEQ
- Cl-isabelle-users November 2011 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