79aae2f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Unification tweak - try a different order on failure

79aae2fEdwin Brady15 years ago

lib/prelude/nat.idr+4

@@ -69,3 +69,7 @@ plus_commutes_Sk = proof {

69 refine plusn_Sm;

70}

72+plus_assoc : (n, m, p : Nat) -> n + (m + p) = (n + m) + p

73+plus_assoc O m p = refl

74+plus_assoc (S k) m p = let ih = plus_assoc k m p in eqRespS ih

75+

src/Core/Unify.hs+10−5

@@ -55,11 +55,16 @@ unify ctxt env topx topy

55 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []

57 un' fn bnames (App fx ax) (App fy ay)

58− = do hf <- un' True bnames fx fy

58+ = mplus (do hf <- un' True bnames fx fy

59− let ax' = normalise ctxt env (substNames hf ax)

59+ let ax' = normalise ctxt env (substNames hf ax)

60− let ay' = normalise ctxt env (substNames hf ay)

60+ let ay' = normalise ctxt env (substNames hf ay)

61− ha <- un' False bnames ax' ay'

61+ ha <- un' False bnames ax' ay'

62+ combine bnames hf ha)

63+ (do ha <- un' False bnames ax ay

64+ let fx' = normalise ctxt env (substNames ha fx)

65+ let fy' = normalise ctxt env (substNames ha fy)

66+ hf <- un' False bnames fx' fy'

62− combine bnames hf ha

67+ combine bnames hf ha)

64 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))

69 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))

65 | n == n' = un' False bnames x y

70 | n == n' = un' False bnames x y