93819ed · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Unification fix

commit93819ed839a8c63091f1cd11ad669dbe5790c428 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 18 Mar 2013, 15:43 (14 years ago) parent1a87674

2 files changed+15−4

compare with master

unifiedsplit

src/Core/ProofState.hs+1−1 src/Core/Unify.hs+14−3

src/Core/ProofState.hs+1−1

@@ -157,7 +157,7 @@ unify' ctxt env topx topy =

157157 do ps <- get

158158 let dont = dontunify ps

159159 (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $

160− lift $ unify ctxt env topx topy dont (holes ps)

160+ lift $ unify ctxt env topx topy dont (holes ps)

161161-- trace ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

162162-- -- " in " ++ show env ++

163163-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

src/Core/Unify.hs+14−3

@@ -133,8 +133,8 @@ unify ctxt env topx topy dont holes =

133133 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

134134

135135 un' fn bnames appx@(App fx ax) appy@(App fy ay)

136− | injective fx && metavarApp appy

137− || injective fy && metavarApp appx

136+ | injective fx && sameArgStruct appx appy && metavarApp appy

137+ || injective fy && sameArgStruct appx appy && metavarApp appx

138138 || injective fx && injective fy

139139 || fx == fy

140140 = do let (headx, _) = unApply fx

@@ -196,10 +196,21 @@ unify ctxt env topx topy dont holes =

196196 metavarApp' tm = let (f, args) = unApply tm in

197197 all (\x -> pat x || metavar x) (f : args)

198198

199− sameStruct (App f x) (App g y) = sameStruct f g && sameStruct x y

199+ sameArgStruct appx appy = let (_, ax) = unApply appx

200+ (_, ay) = unApply appy in

201+ and (zipWith sameStruct ax ay)

202+

203+ sameStruct fapp@(App f x) gapp@(App g y)

204+ = let (f',a') = unApply fapp

205+ (g',b') = unApply gapp in

206+ (f' == g' && length a' == length b' &&

207+ (injective f' || injective g'))

208+ || (sameStruct f g && sameStruct x y)

200209 sameStruct (P _ x _) (P _ y _) = True

201210 sameStruct (V i) (V j) = i == j

202211 sameStruct (Constant x) (Constant y) = True

212+ sameStruct (P _ _ _) (Constant y) = True

213+ sameStruct (Constant x) (P _ _ _) = True

203214 sameStruct (Bind n t sc) (P _ _ _) = True

204215 sameStruct (P _ _ _) (Bind n t sc) = True

205216 sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'