Funkcja zwraca "Brak rozwiązania" Zamiast "Nic"

Question

Mam standardowy typ danych reprezentujący formuły logiki predykatów. Funkcja przedstawiający zasadę eliminacji dedukcja naturalna dla alternatywy może wyglądać tak:

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 

zamiast oceniać na nic, gdy zjednoczenie się nie powiedzie, funkcja zwraca żadnych rozwiązań w 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. 

Co mi brakuje, i dlaczego el nie ocenia się na Nothing, gdy unifikacja się nie powiedzie?

Answer 1

Wygląda na to, że nie jest to najlepszy sposób na użycie więzów równania. Po niepowodzeniu a =:= b kończy się również klauzula function.
Np .:

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

Analizowanie xx 7 powoduje 3 (nie 7), ponieważ 7 =:= 5 całkowicie zamyka pierwszy zapis funkcji xx.

myślę, że kod powinien wyglądać tak:

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