idris - 我怎样才能让 Idris 相信我的功能正在覆盖？

Question

我编写了一个函数doSomething，它接受一个左括号或右括号并返回相应的Int:

doSomething : (c : Char) -> {auto isPar : c == '(' || c == ')' = True} -> Int
doSomething '(' {isPar = Refl} = 1
doSomething ')' {isPar = Refl} = -1

使用isPar，我想确保只有括号，没有其他字符可以传递给doSomething。但是 idris 提示道:

Error: doSomething is not covering
Missing cases:
    doSomething _

我如何说服或证明 Idris 涵盖了所有可能的情况？ 我试过:

doSomething 'a' {isPar = Refl} impossible --this type checks
doSomething _   {isPar = Refl} impossible --this not

Answer 1

编译器无法猜测 ( 和 ) 是唯一允许构造 isPar 值的值，因此是无法断定剩下的情况是不可能的。

解决方法是跟踪某些内容不是开括号或闭括号。可以这样做:

import Data.So

doSomething : (c : Char) -> {auto isPar : So (c == '(' || c == ')')} -> Int
doSomething x {isPar} = case (choose (x == '(')) of
  Left _ => 1
  Right notOpen => case (choose (x == ')')) of
    Left _ => -1
    Right notClose => case (soOr isPar) of
        Left isOpen => absurd $ soNotToNotSo notOpen isOpen
        Right isClose => absurd $ soNotToNotSo notClose isClose

So 是谓词为 True 的证明，choose 提供谓词为 True 的证明>(左分支)，或证明它不正确的证据(右分支)。 使用 x 既不是 ( (notOpen) 也不是 ) (notClose )，我们可以通过分析为什么isPar为真(with soOr)来得出结论。

你可以在its package中找到我用来处理So的所有函数的类型.