Re: [isabelle] General code_abort'd constant



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é

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





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