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

git.iko.soy/Idris-dev

Unification tweak - try a different order on failure

commit79aae2f99ac387f94d6abe2608b2b58761b74374 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 8 Jan 2012, 01:04 (15 years ago) parent7f74f91

2 files changed+14−5

unifiedsplit

lib/prelude/nat.idr+4

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

6969 refine plusn_Sm;

7070}

7171

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

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

5656

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

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

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

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

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

62− combine bnames hf ha

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

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

60+ let ay' = normalise ctxt env (substNames hf 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'

67+ combine bnames hf ha)

6368

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

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