[isabelle] No Code Equation for LIMSEQ · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] No Code Equation for LIMSEQ

Email Gateway (Aug 18 2022 at 18:42):

From: Dave Thayer <dathayer@microsoft.com>
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

Email Gateway (Aug 18 2022 at 18:42):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Email Gateway (Aug 18 2022 at 18:42):

From: Dave Thayer <dathayer@microsoft.com>
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

Email Gateway (Aug 18 2022 at 18:43):

From: Johannes Hölzl <hoelzl@in.tum.de>
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

Email Gateway (Aug 18 2022 at 18:43):

From: Johannes Hölzl <hoelzl@in.tum.de>
Okay now with numerals support:

theory Scratch
imports Complex_Main "~~/src/HOL/Library/Code_Integer"
begin