Re: [isabelle] General code_abort'd constant



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.





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