Re: [isabelle] General code_abort'd constant



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




# HG changeset patch
# User Andreas Lochbihler
# Date 1381325600 -7200
# Node ID 464de1eff32343988bac334943894581abfa1cf0
# Parent  782e430e6a83f89b1a9966b28c3d0e0ad883340d
add congruence rule to prevent code_simp from looping

diff -r 782e430e6a83 -r 464de1eff323 src/HOL/String.thy
--- a/src/HOL/String.thy	Mon Oct 07 22:19:08 2013 +0200
+++ b/src/HOL/String.thy	Wed Oct 09 15:33:20 2013 +0200
@@ -425,8 +425,13 @@
 definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
 where [simp, code del]: "abort _ f = f ()"
 
+lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
+by simp
+
 setup {* Sign.map_naming Name_Space.parent_path *}
 
+setup {* Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong}) *}
+
 code_printing constant Code.abort \<rightharpoonup>
     (SML) "!(raise/ Fail/ _)"
     and (OCaml) "failwith"


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