Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] General code_abort'd constant

view this post on Zulip Email Gateway (Aug 19 2022 at 11:48):

From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi all,

I have been playing a bit with "code_unspec". I rapidly found myself defining this reusable constant, which I can now use in all sorts of contexts:

definition code_unspec :: "(unit => 'a) => 'a" where
[code del]: "code_unspec f = f ()"

code_abort code_unspec

For example, I can write

f x = (if p x then some_behavior x else code_unspec (%_. f x))

and easily prove it from

p x ==> f x = some_behavior x

and the definition of "code_unspec". I cannot do the same with "undefined", because things like

~ p x ==> f x = undefined
~ p x ==> f x = undefined x

are not theorems in my application.

I can't help but notice that my constant could potentially replace many existing uses of "code_abort", notably "enum_the" in "Enum.thy". Are there any takers, or should I define it in my own ((co)datatype-related) theories?

Jasmin

P.S. To members of the Munich Isabelle group: Sorry for the duplicate email.

view this post on Zulip Email Gateway (Aug 19 2022 at 11:48):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jasmin,

I have been using such a constant for a long time. In 2009, my FinFun theories in the AFP
defined a constant code_abort with exactly the setup, later they made it into HOL/Library
and I have used that in JinjaThreads. The problem with such a code_unspec is that the
generated code will always raise the exception Fail with message "code_unspec". This is a
night-mare when you try to debug the generated code. Therefore, I now use a new constant
Code.abort that also allows to specify an error message (changeset 7bfe0df532a9) that will
be part of the next release. I recommend that you use Code.abort for your purposes.

I would appreciate if all these code_aborts that you mention were consolidated to use
Code.abort.

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 11:48):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,

I have been using such a constant for a long time. In 2009, my FinFun theories in the AFP defined a constant code_abort with exactly the setup, later they made it into HOL/Library and I have used that in JinjaThreads. The problem with such a code_unspec is that the generated code will always raise the exception Fail with message "code_unspec". This is a night-mare when you try to debug the generated code. Therefore, I now use a new constant Code.abort that also allows to specify an error message (changeset 7bfe0df532a9) that will be part of the next release. I recommend that you use Code.abort for your purposes.

That's great. It escaped my simple-minded grep "code_abort" but that's what I need.

I would appreciate if all these code_aborts that you mention were consolidated to use Code.abort.

I second this. Cf. http://goo.gl/4kR3vu :)

Jasmin

view this post on Zulip Email Gateway (Aug 19 2022 at 12:21):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,

I currently stumbled about a problem that Code.abort does not work in
combination with Eval, where it does not fail, but loop.
(in Isabelle-2013-1-RC-1)

theory Scratch
imports Main
begin

definition "foo x = (x :: bool)"
lemma [code]: "foo x = (if x then True else Code.abort (STR ''not impl.'') (% _. foo x))"
by (auto simp: foo_def)

export_code foo in Eval
(* delivers:
fun foo x = (if x then true else (raise Fail "not impl.") (fn _ => foo x));
*)

value "foo True" (* True *)
value "foo False" (* loops *)

ML {*
let fun foo x = (if x then true else (raise Fail "not impl.") (fn _ => foo x))
in foo false
end
*}
(* delivers intended result: exception Fail raised: not impl. *)
end

Is this a known limitation, feature, or a bug?

Cheers,
René

view this post on Zulip Email Gateway (Aug 19 2022 at 12:22):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi René,

I currently stumbled about a problem that Code.abort does not work in
combination with Eval, where it does not fail, but loop.
(in Isabelle-2013-1-RC-1)
Well, it is not Eval that loops but nbe and code_simp. You can see this by specifying the
evaluation mechanism:

value [code] "foo False" (* raises Fail *)
value [simp] "foo False" (* loops *)
value [nbe] "foo False" (* loops *)

It is fairly easy to stop the simplifier from looping, a congruence rule for Code.abort
suffices (see the attached patch).

With [nbe], I haven't found a way to achieve termination. As there are no code equations
for Code.abort available, nbe descends into the argument (%_. foo x) and here, the
equation for foo yields the next unfolding. Maybe Florian knows a way to stop nbe.

Therefore, I would call the looping of the simplifier a bug, the looping of nbe a limitation.

@Makarius:
Can you add the attached hg export to isabelle-release?

Andreas

theory Scratch
imports Main
begin

definition "foo x = (x :: bool)"
lemma [code]: "foo x = (if x then True else Code.abort (STR ''not impl.'') (% _. foo x))"
by (auto simp: foo_def)

export_code foo in Eval
(* delivers:
fun foo x = (if x then true else (raise Fail "not impl.") (fn _ => foo x));
*)

value "foo True" (* True *)
value "foo False" (* loops *)

ML {*
let fun foo x = (if x then true else (raise Fail "not impl.") (fn _ => foo x))
in foo false
end
*}
(* delivers intended result: exception Fail raised: not impl. *)
end

Is this a known limitation, feature, or a bug?

Cheers,
René

Am 18.09.2013 um 17:04 schrieb Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>:

Hi Jasmin,

I have been using such a constant for a long time. In 2009, my FinFun theories in the AFP defined a constant code_abort with exactly the setup, later they made it into HOL/Library and I have used that in JinjaThreads. The problem with such a code_unspec is that the generated code will always raise the exception Fail with message "code_unspec". This is a night-mare when you try to debug the generated code. Therefore, I now use a new constant Code.abort that also allows to specify an error message (changeset 7bfe0df532a9) that will be part of the next release. I recommend that you use Code.abort for your purposes.

I would appreciate if all these code_aborts that you mention were consolidated to use Code.abort.

Andreas

On 18/09/13 16:42, Jasmin Christian Blanchette wrote:

Hi all,

I have been playing a bit with "code_unspec". I rapidly found myself defining this reusable constant, which I can now use in all sorts of contexts:

definition code_unspec :: "(unit => 'a) => 'a" where
[code del]: "code_unspec f = f ()"

code_abort code_unspec

For example, I can write

f x = (if p x then some_behavior x else code_unspec (%_. f x))

and easily prove it from

p x ==> f x = some_behavior x

and the definition of "code_unspec". I cannot do the same with "undefined", because things like

~ p x ==> f x = undefined
~ p x ==> f x = undefined x

are not theorems in my application.

I can't help but notice that my constant could potentially replace many existing uses of "code_abort", notably "enum_the" in "Enum.thy". Are there any takers, or should I define it in my own ((co)datatype-related) theories?

Jasmin

P.S. To members of the Munich Isabelle group: Sorry for the duplicate email.

code_abort_code_simp.patch

view this post on Zulip Email Gateway (Aug 19 2022 at 12:23):

From: Makarius <makarius@sketis.net>
Done.

See
https://bitbucket.org/isabelle_project/isabelle-release/commits/da932f511746

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 12:24):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Andreas,

I currently stumbled about a problem that Code.abort does not work in
combination with Eval, where it does not fail, but loop.
(in Isabelle-2013-1-RC-1)
Well, it is not Eval that loops but nbe and code_simp. You can see this by specifying the evaluation mechanism:

value [code] "foo False" (* raises Fail *)
value [simp] "foo False" (* loops *)
value [nbe] "foo False" (* loops *)

thanks for the explanation. I already tried value[nbe], but not value[code] :-(.
Now even my real example works as expected.

Cheers,
René

It is fairly easy to stop the simplifier from looping, a congruence rule for Code.abort suffices (see the attached patch).

With [nbe], I haven't found a way to achieve termination. As there are no code equations for Code.abort available, nbe descends into the argument (%_. foo x) and here, the equation for foo yields the next unfolding. Maybe Florian knows a way to stop nbe.

Therefore, I would call the looping of the simplifier a bug, the looping of nbe a limitation.

Last updated: Apr 30 2024 at 12:28 UTC