Re: [isabelle] General code_abort'd constant
I currently stumbled about a problem that Code.abort does not work in
combination with Eval, where it does not fail, but loop.
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
fun foo x = (if x then true else (raise Fail "not impl.") (fn _ => foo x));
value "foo True" (* True *)
value "foo False" (* loops *)
let fun foo x = (if x then true else (raise Fail "not impl.") (fn _ => foo x))
in foo false
(* delivers intended result: exception Fail raised: not impl. *)
Is this a known limitation, feature, or a bug?
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.
> 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?
>> P.S. To members of the Munich Isabelle group: Sorry for the duplicate email.
This archive was generated by a fusion of
Pipermail (Mailman edition) and