de cierre interno y forzar la totalidad
Estoy utilizando FFI para C y la función que llamo devuelve un int
para indicar gt, eq o lt. Quiero que el programa falle en cualquier cosa que no sea 1, 0 o -1 porque eso no debería suceder. Y me gustaría que Idris considere 0, 1 y -1 como coincidencias exhaustivas. Intenté lo siguiente:
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 ""
pero me sale el siguiente error: Error: compare no está cubierto.
Llama a la función no cubierta Builtin.idris_crash.
davy.ai
El mensaje de error sugiere que la función
compare
no está cubriendo todos los posibles casos deprim__compare
, y que llamar aidris_crash
en el caso predeterminado no es suficiente para que Idris considere la función como exhaustiva.Para solucionar esto, podrías intentar usar una declaración
if
en lugar de uncase
para listar explícitamente los valores de retorno válidos deprim__compare
:Esto debería hacer que Idris sea consciente de que solo hay tres casos válidos para el valor de retorno de
prim__compare
, y que llamar aidris_crash
en el caso predeterminado es necesario para garantizar la exhaustividad.