Email Gateway (Aug 22 2022 at 10:33): Email Gateway (Aug 22 2022 at 10:33):From: Andrew Gacek <andrew.gacek@gmail.com>
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
Email Gateway (Aug 22 2022 at 10:34):From: Dmitriy Traytel <traytel@in.tum.de>
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
Email Gateway (Aug 22 2022 at 10:34):From: Andrew Gacek <andrew.gacek@gmail.com>
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
Email Gateway (Aug 22 2022 at 10:34):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Andrew,
please note that the code below is run on every term that is given to
the type inference. And for the function package this is not only the
term entered by the user, but also some internal stuff, where apparently
undefined appears. I presume the command term and definition will not
give warnings for "f x = (case x of 0 => 0 | Suc n => n)" (not tested).
Otherwise, you probably also want to emit a warning only when the
undefined appears directly under a case combinator (this may reduce the
number of false positives). Thus you will need to refine my rudimentary
proposal.
Dmitriy
Last updated: Nov 21 2024 at 12:39 UTC