ffi - 如何在内部错误上崩溃并强制整体

Question

我正在使用 C 并且我调用的函数返回一个int表示 gt、eq 或 lt 的函数。我想在任何不应该发生的 1、0 或 -1 cos 上崩溃。我希望 Idris 将 0、1 和 -1 视为详尽匹配。我试过

prim__compare : Scalar -> Scalar -> Int

Ord Scalar where
  compare x y = case prim__compare x y of
                  -1 => LT
                  0 => EQ
                  1 => GT
                  _ => idris_crash ""

但我明白了

Error: compare is not covering.

Calls non covering function Builtin.idris_crash

Answer 1

由于崩溃只能是由于内部错误，因此使用它是合理的assert_total

Ord Scalar where
  compare x y = case prim__compare x y of
                  -1 => LT
                  0 => EQ
                  1 => GT
                  _ => (assert_total idris_crash) ""