La funzione restituisce "Nessuna soluzione" invece di "Niente"

Question

Ho un tipo di dati standard che rappresenta le formule della logica dei predicati. Una funzione che rappresenta una regola di eliminazione deduzione naturale per la disgiunzione potrebbe essere simile:

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 

Invece di valutare a nulla quando l'unificazione fallisce, la funzione restituisce soluzioni in 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. 

Quello che mi manca, e perché lo el non viene valutato a Nothing quando l'unificazione non riesce?

Answer 1

Sembra che questo non sia il modo migliore per utilizzare i vincoli di equazione. Quando a =:= b fallisce, anche la clausola di funzione completa non riesce.
Es .:

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

Valutare xx 7 risultati in 3 (non 7) perché 7 =:= 5 termina completamente prima clausola della funzione xx.

penso che il codice dovrebbe essere simile a questo:

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