git.iko.soy/Idris-dev
on master help sign in
Unification fix
93819edEdwin Brady
src/Core/ProofState.hs+1−1
compare with master
unifiedsplit
@@ -157,7 +157,7 @@ unify' ctxt env topx topy =
157 do ps <- get
157 do ps <- get
158 let dont = dontunify ps
158 let dont = dontunify ps
159 (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $
159 (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)
161-- trace ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
161-- trace ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
162-- -- " in " ++ show env ++
162-- -- " in " ++ show env ++
163-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"
163-- "\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 =
133 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
133 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
134
134
135 un' fn bnames appx@(App fx ax) appy@(App fy ay)
135 un' fn bnames appx@(App fx ax) appy@(App fy ay)
136− | injective fx && metavarApp appy
136+ | injective fx && sameArgStruct appx appy && metavarApp appy
137− || injective fy && metavarApp appx
137+ || injective fy && sameArgStruct appx appy && metavarApp appx
138 || injective fx && injective fy
138 || injective fx && injective fy
139 || fx == fy
139 || fx == fy
140 = do let (headx, _) = unApply fx
140 = do let (headx, _) = unApply fx
@@ -196,10 +196,21 @@ unify ctxt env topx topy dont holes =
196 metavarApp' tm = let (f, args) = unApply tm in
196 metavarApp' tm = let (f, args) = unApply tm in
197 all (\x -> pat x || metavar x) (f : args)
197 all (\x -> pat x || metavar x) (f : args)
198
198
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'))
199− sameStruct (App f x) (App g y) = sameStruct f g && sameStruct x y
208+ || (sameStruct f g && sameStruct x y)
200 sameStruct (P _ x _) (P _ y _) = True
209 sameStruct (P _ x _) (P _ y _) = True
201 sameStruct (V i) (V j) = i == j
210 sameStruct (V i) (V j) = i == j
202 sameStruct (Constant x) (Constant y) = True
211 sameStruct (Constant x) (Constant y) = True
212+ sameStruct (P _ _ _) (Constant y) = True
213+ sameStruct (Constant x) (P _ _ _) = True
203 sameStruct (Bind n t sc) (P _ _ _) = True
214 sameStruct (Bind n t sc) (P _ _ _) = True
204 sameStruct (P _ _ _) (Bind n t sc) = True
215 sameStruct (P _ _ _) (Bind n t sc) = True
205 sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'
216 sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'