Re: [isabelle] No warning for non-exhaustive case



Thanks, this does indeed catch the undefined. But for me it also gives
spurious warnings, e.g. on

fun f :: "nat => nat" where
  "f x = (case x of 0 => 0 | Suc n => n)"

This is on Isabelle2014.

-Andrew

On Tue, Jun 9, 2015 at 4:48 PM, Dmitriy Traytel <traytel at in.tum.de> wrote:
> Hi Andrew,
>
> no, there is no direct way to do this (i.e. the case translation facility
> does not provide this functionality).
>
> Of course, with Isabelle's user-space type inference, you can implement a
> check phase that does what you want. Here is a quick and dirty example that
> just shouts whenever it finds an undefined in a term (which is the case in
> your example):
>
> ML â
> Context.>>
>   (Syntax_Phases.term_check 2 "Warn undefined"
>     (fn _ => fn ts =>
>       let
>         val _ = map (fn t => fold_term_types (fn t => fn T => fn () =>
>           if t = Const (@{const_name undefined}, T) then warning "undefined"
> else ()) t ()) ts
>       in ts end))
> â
>
> Dmitriy
>
>
> On 09.06.2015 22:44, Andrew Gacek wrote:
>>
>> Is there a way to enable warnings when a case expression is
>> non-exhaustive? For example, Isabelle/HOL accepts this without a
>> warning:
>>
>> fun f :: "nat => nat" where
>>    "f x = (case x of 0 => 0)"
>>
>> Thanks,
>> Andrew
>>
>




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