Re: [isabelle] No Code Equation for LIMSEQ



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







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