Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] No Code Equation for LIMSEQ


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

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 "embed = (of_int :: int \<Rightarrow> real)"
code_const embed
(OCaml "float'_of'_int")

lemma of_int_eq_embed[code inline]:
"of_int = embed"
unfolding embed_def ..

declare number_of_real_code [code inline del]

definition "test_trig x y a = cos (arctan (y / x) + sin a - pi/4.1)"

export_code test_trig
in OCaml module_name CodegenTest file -

end


Last updated: Mar 29 2024 at 04:18 UTC