@@ -7,6 +7,7 @@ import Core.Evaluate
77
88import Control.Monad
99import Control.Monad.State
10+import Data.List
1011import Debug.Trace
1112
1213-- Unification is applied inside the theorem prover. We're looking for holes
@@ -124,8 +125,7 @@ unify ctxt env topx topy dont holes =
124125 case runStateT (un False [] topxn topyn)
125126 (UI 0 []) of
126127 OK (v, UI _ fails) ->
127− return (filter notTrivial v,
128− reverse fails)
128+ return (filter notTrivial v, reverse fails)
129129-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
130130 Error e -> tfail e
131131 where
@@ -213,7 +213,38 @@ unify ctxt env topx topy dont holes =
213213 un' fn bnames (P _ x _) (V i)
214214 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
215215
216− un' fn bnames appx@(App fx ax) appy@(App fy ay)
216+ un' fn bnames appx@(App _ _) appy@(App _ _)
217+ = unApp fn bnames appx appy
218+-- = uplus (unApp fn bnames appx appy)
219+-- (unifyTmpFail appx appy) -- take the whole lot
220+
221+ un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
222+ | n == n' = un' False bnames x y
223+ un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
224+ | n == n' = un' False bnames x y
225+ un' fn bnames x (Bind n (Lam t) (App y (V 0)))
226+ = un' False bnames x y
227+ un' fn bnames (Bind n (Lam t) (App x (V 0))) y
228+ = un' False bnames x y
229+-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
230+-- = un' False ((x,y):bnames) sx sy
231+-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
232+-- = un' False ((x,y):bnames) sx sy
233+ un' fn bnames (Bind x bx sx) (Bind y by sy)
234+ = do h1 <- uB bnames bx by
235+ h2 <- un' False ((x,y):bnames) sx sy
236+ combine bnames h1 h2
237+ un' fn bnames x y
238+ | OK True <- convEq' ctxt x y = do sc 1; return []
239+ | otherwise = do UI s f <- get
240+ let r = recoverable x y
241+ let err = CantUnify r
242+ topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
243+ if (not r) then lift $ tfail err
244+ else do put (UI s ((x, y, env, err) : f))
245+ return [] -- lift $ tfail err
246+
247+ unApp fn bnames appx@(App fx ax) appy@(App fy ay)
217248 | (injective fx && injective fy)
218249 || (injective fx && rigid appx && metavarApp appy)
219250 || (injective fy && rigid appy && metavarApp appx)
@@ -244,15 +275,17 @@ unify ctxt env topx topy dont holes =
244275 do let (headx, argsx) = unApply appx
245276 let (heady, argsy) = unApply appy
246277 -- traceWhen (headx == heady) (show (appx, appy)) $
247− if (length argsx == length argsy &&
248− ((headx == heady && inenv headx) || (argsx == argsy) ||
249− (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))
250− then
251−-- (notFn headx && notFn heady))) then
252− do uf <- un' True bnames headx heady
253− unArgs uf argsx argsy
254− else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $
255− unifyTmpFail appx appy
278+ uplus (
279+ if (length argsx == length argsy &&
280+ ((headx == heady && inenv headx) || (argsx == argsy) ||
281+ (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))
282+ then
283+-- (notFn headx && notFn heady))) then
284+ do uf <- un' True bnames headx heady
285+ unArgs uf argsx argsy
286+ else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $
287+ unifyTmpFail appx appy)
288+ (unifyTmpFail appx appy) -- whole application fails
256289 where hnormalise [] _ _ t = t
257290 hnormalise ns ctxt env t = normalise ctxt env t
258291 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
@@ -275,10 +308,13 @@ unify ctxt env topx topy dont holes =
275308
276309 metavarApp tm = let (f, args) = unApply tm in
277310 all (\x -> metavar x) (f : args)
311+ && nub args == args
278312 metavarArgs tm = let (f, args) = unApply tm in
279313 all (\x -> metavar x || inenv x) args
314+ && nub args == args
280315 metavarApp' tm = let (f, args) = unApply tm in
281316 all (\x -> pat x || metavar x) (f : args)
317+ && nub args == args
282318
283319 sameArgStruct appx appy
284320 = let (_, ax) = unApply appx
@@ -322,38 +358,13 @@ unify ctxt env topx topy dont holes =
322358
323359 notFn t = injective t || metavar t || inenv t
324360
325− un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
326− | n == n' = un' False bnames x y
327− un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
328− | n == n' = un' False bnames x y
329− un' fn bnames x (Bind n (Lam t) (App y (V 0)))
330− = un' False bnames x y
331− un' fn bnames (Bind n (Lam t) (App x (V 0))) y
332− = un' False bnames x y
333−-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
334−-- = un' False ((x,y):bnames) sx sy
335−-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
336−-- = un' False ((x,y):bnames) sx sy
337− un' fn bnames (Bind x bx sx) (Bind y by sy)
338− = do h1 <- uB bnames bx by
339− h2 <- un' False ((x,y):bnames) sx sy
340− combine bnames h1 h2
341− un' fn bnames x y
342− | OK True <- convEq' ctxt x y = do sc 1; return []
343− | otherwise = do UI s f <- get
344− let r = recoverable x y
345− let err = CantUnify r
346− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
347− if (not r) then lift $ tfail err
348− else do put (UI s ((x, y, env, err) : f))
349− return [] -- lift $ tfail err
350361
351362 unifyTmpFail x y
352363 = do UI s f <- get
353364 let r = recoverable x y
354365 let err = CantUnify r
355366 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
356− put (UI s ((x, y, env, err) : f))
367+ put (UI s ((topx, topy, env, err) : f))
357368 return []
358369
359370 -- shortcut failure, if we *know* nothing can fix it
@@ -361,7 +372,7 @@ unify ctxt env topx topy dont holes =
361372 let r = recoverable x y
362373 let err = CantUnify r
363374 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
364− put (UI s ((x, y, env, err) : f))
375+ put (UI s ((topx, topy, env, err) : f))
365376 lift $ tfail err
366377
367378