@@ -8,6 +8,7 @@ import Idris.Core.Evaluate
88
99import Control.Monad
1010import Control.Monad.State.Strict
11+import Data.Maybe
1112import Data.List
1213import Debug.Trace
1314
@@ -321,7 +322,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
321322 un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
322323 StateT UInfo
323324 TC [(Name, TT Name)]
324− un = un'
325+ un = un' env
325326-- un fn names x y
326327-- = let (xf, _) = unApply x
327328-- (yf, _) = unApply y in
@@ -329,23 +330,23 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
329330-- uplus (un' fn names x y)
330331-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))
331332
332− un' :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
333+ un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
333334 StateT UInfo
334335 TC [(Name, TT Name)]
335− un' fn names x y | x == y = return [] -- shortcut
336− un' fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)
336+ un' env fn names x y | x == y = return [] -- shortcut
337+ un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)
337338 | x /= y = unifyFail topx topy
338− un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
339+ un' env fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
339340 | x /= y = unifyFail topx topy
340− un' fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)
341+ un' env fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)
341342 = unifyFail topx topy
342− un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)
343+ un' env fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)
343344 = unifyFail topx topy
344− un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)
345+ un' env fn names topx@(Constant _) topy@(P (TCon _ _) y _)
345346 = unifyFail topx topy
346− un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)
347+ un' env fn names topx@(P (TCon _ _) x _) topy@(Constant _)
347348 = unifyFail topx topy
348− un' fn bnames tx@(P _ x _) ty@(P _ y _)
349+ un' env fn bnames tx@(P _ x _) ty@(P _ y _)
349350 | (x,y) `elem` map fst bnames || x == y = do sc 1; return []
350351 | injective tx && not (holeIn env y || y `elem` holes)
351352 = unifyTmpFail tx ty
@@ -360,7 +361,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
360361 where envPos i n ((n',_):env) | n == n' = i
361362 envPos i n (_:env) = envPos (i+1) n env
362363 envPos _ _ _ = 100000
363− un' fn bnames xtm@(P _ x _) tm
364+ un' env fn bnames xtm@(P _ x _) tm
364365 | pureTerm tm, holeIn env x || x `elem` holes
365366 = do UI s f <- get
366367 -- injectivity check
@@ -374,7 +375,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
374375 | pureTerm tm, not (injective xtm) && injective tm
375376 = do checkCycle bnames (x, tm)
376377 unifyTmpFail xtm tm
377− un' fn bnames tm ytm@(P _ y _)
378+ un' env fn bnames tm ytm@(P _ y _)
378379 | pureTerm tm, holeIn env y || y `elem` holes
379380 = do UI s f <- get
380381 -- injectivity check
@@ -388,62 +389,118 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
388389 | pureTerm tm, not (injective ytm) && injective tm
389390 = do checkCycle bnames (y, tm)
390391 unifyTmpFail tm ytm
391− un' fn bnames (V i) (P _ x _)
392+ un' env fn bnames (V i) (P _ x _)
392393 | length bnames > i,
393394 fst ((map fst bnames)!!i) == x ||
394395 snd ((map fst bnames)!!i) == x = do sc 1; return []
395− un' fn bnames (P _ x _) (V i)
396+ un' env fn bnames (P _ x _) (V i)
396397 | length bnames > i,
397398 fst ((map fst bnames)!!i) == x ||
398399 snd ((map fst bnames)!!i) == x = do sc 1; return []
399400
400− un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
401− un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
402−
403− un' fn bnames appx@(App _ _ _) appy@(App _ _ _)
404− = unApp fn bnames appx appy
401+ un' env fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y
402+ un' env fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy
403+
404+-- Pattern unification rule
405+ un' env fn bnames tm app@(App _ _ _)
406+ | (P _ mv _, args) <- unApply app,
407+ holeIn env mv || mv `elem` holes,
408+ all rigid args,
409+ containsOnly (mapMaybe getname args) (mapMaybe getV args) tm
410+ -- && TODO: tm does not refer to any variables other than those
411+ -- in 'args'
412+ = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $
413+ checkCycle bnames (mv, eta [] $ bindLams args (substEnv env tm))
414+ where rigid (V i) = True
415+ rigid (P _ t _) = not (holeIn env t || t `elem` holes)
416+ rigid _ = False
417+
418+ getV (V i) = Just i
419+ getV _ = Nothing
420+
421+ getname (P _ n _) = Just n
422+ getname _ = Nothing
423+
424+ containsOnly args vs (V i) = i `elem` vs
425+ containsOnly args vs (P Bound n ty)
426+ = n `elem` args && containsOnly args vs ty
427+ containsOnly args vs (P _ n ty)
428+ = not (holeIn env n || n `elem` holes)
429+ && containsOnly args vs ty
430+ containsOnly args vs (App _ f a)
431+ = containsOnly args vs f && containsOnly args vs a
432+ containsOnly args vs (Bind _ b sc)
433+ = containsOnly args vs (binderTy b) &&
434+ containsOnly args (0 : map (+1) vs) sc
435+ containsOnly args vs _ = True
436+
437+ bindLams [] tm = tm
438+ bindLams (a : as) tm = bindLam a (bindLams as tm)
439+
440+ bindLam (V i) tm = Bind (fst (env !! i))
441+ (Lam (binderTy (snd (env !! i))))
442+ tm
443+ bindLam (P _ n ty) tm = Bind n (Lam ty) tm
444+ bindLam _ tm = error "Can't happen [non rigid bindLam]"
445+
446+ substEnv [] tm = tm
447+ substEnv ((n, t) : env) tm
448+ = substEnv env (substV (P Bound n (binderTy t)) tm)
449+
450+ -- remove any unnecessary lambdas (helps with type class
451+ -- resolution later).
452+ eta ks (Bind n (Lam ty) sc) = eta ((n, ty) : ks) sc
453+ eta ks t = rebind ks t
454+
455+ rebind ((n, ty) : ks) (App _ f (P _ n' _))
456+ | n == n' = eta ks f
457+ rebind ((n, ty) : ks) t = rebind ks (Bind n (Lam ty) t)
458+ rebind _ t = t
459+
460+ un' env fn bnames appx@(App _ _ _) appy@(App _ _ _)
461+ = unApp env fn bnames appx appy
405462-- = uplus (unApp fn bnames appx appy)
406463-- (unifyTmpFail appx appy) -- take the whole lot
407464
408− un' fn bnames x (Bind n (Lam t) (App _ y (P Bound n' _)))
409− | n == n' = un' False bnames x y
410− un' fn bnames (Bind n (Lam t) (App _ x (P Bound n' _))) y
411− | n == n' = un' False bnames x y
412− un' fn bnames x (Bind n (Lam t) (App _ y (V 0)))
413− = un' False bnames x y
414− un' fn bnames (Bind n (Lam t) (App _ x (V 0))) y
415− = un' False bnames x y
416−-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
417−-- = un' False ((x,y):bnames) sx sy
418−-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
419−-- = un' False ((x,y):bnames) sx sy
465+ un' env fn bnames x (Bind n (Lam t) (App _ y (P Bound n' _)))
466+ | n == n' = un' env False bnames x y
467+ un' env fn bnames (Bind n (Lam t) (App _ x (P Bound n' _))) y
468+ | n == n' = un' env False bnames x y
469+ un' env fn bnames x (Bind n (Lam t) (App _ y (V 0)))
470+ = un' env False bnames x y
471+ un' env fn bnames (Bind n (Lam t) (App _ x (V 0))) y
472+ = un' env False bnames x y
473+-- un' env fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)
474+-- = un' env False ((x,y):bnames) sx sy
475+-- un' env fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)
476+-- = un' env False ((x,y):bnames) sx sy
420477
421478 -- f D unifies with t -> D. This is dubious, but it helps with type
422479 -- class resolution for type classes over functions.
423480
424− un' fn bnames (App _ f x) (Bind n (Pi i t k) y)
481+ un' env fn bnames (App _ f x) (Bind n (Pi i t k) y)
425482 | noOccurrence n y && injectiveApp f
426− = do ux <- un' False bnames x y
427− uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
483+ = do ux <- un' env False bnames x y
484+ uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
428485 (Bind n (Pi i t k) (V 1)))
429− combine bnames ux uf
486+ combine env bnames ux uf
430487
431− un' fn bnames (Bind n (Pi i t k) y) (App _ f x)
488+ un' env fn bnames (Bind n (Pi i t k) y) (App _ f x)
432489 | noOccurrence n y && injectiveApp f
433− = do ux <- un' False bnames y x
434− uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
490+ = do ux <- un' env False bnames y x
491+ uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))
435492 (Bind n (Pi i t k) (V 1))) f
436− combine bnames ux uf
493+ combine env bnames ux uf
437494
438− un' fn bnames (Bind x bx sx) (Bind y by sy)
495+ un' env fn bnames (Bind x bx sx) (Bind y by sy)
439496 | sameBinder bx by
440− = do h1 <- uB bnames bx by
441− h2 <- un' False (((x,y),binderTy bx):bnames) sx sy
442− combine bnames h1 h2
497+ = do h1 <- uB env bnames bx by
498+ h2 <- un' ((x, bx) : env) False (((x,y),binderTy bx):bnames) sx sy
499+ combine env bnames h1 h2
443500 where sameBinder (Lam _) (Lam _) = True
444501 sameBinder (Pi i _ _) (Pi i' _ _) = True
445502 sameBinder _ _ = False -- never unify holes/guesses/etc
446− un' fn bnames x y
503+ un' env fn bnames x y
447504 | OK True <- convEq' ctxt holes x y = do sc 1; return []
448505 | isUniverse x && isUniverse y = do sc 1; return []
449506 | otherwise = do UI s f <- get
@@ -455,11 +512,11 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
455512 else do put (UI s ((x, y, True, env, err, from, Unify) : f))
456513 return [] -- lift $ tfail err
457514
458− unApp fn bnames appx@(App _ fx ax) appy@(App _ fy ay)
515+ unApp env fn bnames appx@(App _ fx ax) appy@(App _ fy ay)
459516 -- shortcut for the common case where we just want to check the
460517 -- arguments are correct
461518 | (injectiveApp fx && fx == fy)
462− = un' False bnames ax ay
519+ = un' env False bnames ax ay
463520 | (injectiveApp fx && injectiveApp fy)
464521 || (injectiveApp fx && metavarApp fy && ax == ay)
465522 || (injectiveApp fy && metavarApp fx && ax == ay)
@@ -468,18 +525,18 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
468525 -- fail quickly if the heads are disjoint
469526 checkHeads headx heady
470527 uplus
471− (do hf <- un' True bnames fx fy
528+ (do hf <- un' env True bnames fx fy
472529 let ax' = hnormalise hf ctxt env (substNames hf ax)
473530 let ay' = hnormalise hf ctxt env (substNames hf ay)
474− ha <- un' False bnames ax' ay'
531+ ha <- un' env False bnames ax' ay'
475532 sc 1
476− combine bnames hf ha)
477− (do ha <- un' False bnames ax ay
533+ combine env bnames hf ha)
534+ (do ha <- un' env False bnames ax ay
478535 let fx' = hnormalise ha ctxt env (substNames ha fx)
479536 let fy' = hnormalise ha ctxt env (substNames ha fy)
480− hf <- un' False bnames fx' fy'
537+ hf <- un' env False bnames fx' fy'
481538 sc 1
482− combine bnames hf ha)
539+ combine env bnames hf ha)
483540 | otherwise = unifyTmpFail appx appy
484541 where hnormalise [] _ _ t = t
485542 hnormalise ns ctxt env t = normalise ctxt env t
@@ -497,8 +554,8 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
497554 unArgs as (x : xs) (y : ys)
498555 = do let x' = hnormalise as ctxt env (substNames as x)
499556 let y' = hnormalise as ctxt env (substNames as y)
500− as' <- un' False bnames x' y'
501− vs <- combine bnames as as'
557+ as' <- un' env False bnames x' y'
558+ vs <- combine env bnames as as'
502559 unArgs vs xs ys
503560
504561 numArgs tm = let (f, args) = unApply tm in length args
@@ -564,21 +621,22 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
564621 lift $ tfail err
565622
566623
567− uB bnames (Let tx vx) (Let ty vy)
568− = do h1 <- un' False bnames tx ty
569− h2 <- un' False bnames vx vy
624+ uB env bnames (Let tx vx) (Let ty vy)
625+ = do h1 <- un' env False bnames tx ty
626+ h2 <- un' env False bnames vx vy
570627 sc 1
571− combine bnames h1 h2
572− uB bnames (Guess tx vx) (Guess ty vy)
573− = do h1 <- un' False bnames tx ty
574− h2 <- un' False bnames vx vy
628+ combine env bnames h1 h2
629+ uB env bnames (Guess tx vx) (Guess ty vy)
630+ = do h1 <- un' env False bnames tx ty
631+ h2 <- un' env False bnames vx vy
575632 sc 1
576− combine bnames h1 h2
577− uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty
578− uB bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' False bnames tx ty
579− uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty
580− uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty
581− uB bnames x y = do UI s f <- get
633+ combine env bnames h1 h2
634+ uB env bnames (Lam tx) (Lam ty) = do sc 1; un' env False bnames tx ty
635+ uB env bnames (Pi _ tx _) (Pi _ ty _) = do sc 1; un' env False bnames tx ty
636+ uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty
637+ uB env bnames (PVar tx) (PVar ty) = un' env False bnames tx ty
638+ uB env bnames x y
639+ = do UI s f <- get
582640 let r = recoverable (normalise ctxt env (binderTy x))
583641 (normalise ctxt env (binderTy y))
584642 let err = cantUnify from r (topx, xfrom) (topy, yfrom)
@@ -613,20 +671,15 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
613671 App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))
614672 (P Bound x ty)
615673
616− combineArgs bnames args = ca [] args where
617− ca acc [] = return acc
618− ca acc (x : xs) = do x' <- combine bnames acc x
619− ca x' xs
620−
621− combine bnames as [] = return as
622− combine bnames as ((n, t) : bs)
674+ combine env bnames as [] = return as
675+ combine env bnames as ((n, t) : bs)
623676 = case lookup n as of
624− Nothing -> combine bnames (as ++ [(n,t)]) bs
625− Just t' -> do ns <- un' False bnames t t'
677+ Nothing -> combine env bnames (as ++ [(n,t)]) bs
678+ Just t' -> do ns <- un' env False bnames t t'
626679 -- make sure there's n mapping from n in ns
627680 let ns' = filter (\ (x, _) -> x/=n) ns
628681 sc 1
629− combine bnames as (ns' ++ bs)
682+ combine env bnames as (ns' ++ bs)
630683
631684boundVs :: Int -> Term -> [Int]
632685boundVs i (V j) | j < i = []