La función devuelve "Sin solución" en lugar de "Nada"

Question

Tengo un tipo de datos estándar que representa fórmulas de lógica de predicados. Una función que representa una regla de eliminación de la deducción natural para la separación podría ser:

d_el p q = 
    if p =: (Dis r s) && q =: (Neg r) then Just s else 
    if q =: (Dis r s) && p =: (Neg r) then Just s else 
    Nothing where r,s free 

x =: y = (x =:= y) == success 

En lugar de evaluar a nada cuando la unificación falla, la función devuelve ninguna solución en PACKS:

logic> d_el (Dis Bot Top) (Not Bot) 
Result: Just Top 
More Solutions? [Y(es)/n(o)/a(ll)] n 
logic> d_el (Dis Bot Top) (Not Top) 
No more solutions. 

¿Qué me falta, y ¿por qué el no evalúa a Nothing cuando falla la unificación?

Answer 1

Parece que esta no es la mejor manera de usar restricciones ecuacionales. Cuando a =:= b falla, la cláusula de la función completa también falla.
ej .:

xx x = if (x =:= 5) == success then 1 else x 
xx x = 3 

Evaluación de xx 7 resultados en 3 (no 7) porque 7 =:= 5 termina completamente primera cláusula de la función de xx.

creo que el código debería tener este aspecto:

d_el p q = case (p,q) of 
    (Dis a s, Neg b) -> if a == b then Just s else Nothing 
    (Neg a, Dis b s) -> if a == b then Just s else Nothing 
    _ -> Nothing