45c8eca · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Avoid hole bindings in unification solutions

We assume elsewhere that a hole binding only appears once, and these aren't really solutions. The addresses #1242 (although the code there still doesn't type check for a different type class resolution reason).

commit45c8ecaaa6ecfea8a73fc35581232e684c7f0c10 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 26 May 2014, 16:02 (12 years ago) parent4c85c25

2 files changed+28−11

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+7−3 src/Idris/Core/Unify.hs+21−8

src/Idris/Core/Evaluate.hs+7−3

@@ -537,7 +537,7 @@ wknV i t = return t

537537convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

538538

539539convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

540−convEq ctxt holes = ceq [] where

540+convEq ctxt holes topx topy = ceq [] topx topy where

541541 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

542542 ceq ps (P xt x _) (P yt y _)

543543 | x `elem` holes || y `elem` holes = return True

@@ -550,8 +550,12 @@ convEq ctxt holes = ceq [] where

550550 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

551551 | n == n' = ceq ps x y

552552 ceq ps (V x) (V y) = return (x == y)

553− ceq ps (V x) (P _ y _) = return (fst (ps!!x) == y)

554− ceq ps (P _ x _) (V y) = return (x == snd (ps!!y))

553+ ceq ps (V x) (P _ y _)

554+ | x >= 0 && length ps > x = return (fst (ps!!x) == y)

555+ | otherwise = return False

556+ ceq ps (P _ x _) (V y)

557+ | y >= 0 && length ps > y = return (x == snd (ps!!y))

558+ | otherwise = return False

555559 ceq ps (Bind n xb xs) (Bind n' yb ys)

556560 = liftM2 (&&) (ceqB ps xb yb) (ceq ((n,n'):ps) xs ys)

557561 where

src/Idris/Core/Unify.hs+21−8

@@ -85,7 +85,7 @@ match_unify ctxt env topx topy inj holes from =

8585 | length bnames > i,

8686 fst (fst (bnames!!i)) == x ||

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

88− un bnames (Bind x bx sx) (Bind y by sy)

88+ un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by

8989 = do h1 <- uB bnames bx by

9090 h2 <- un (((x, y), binderTy bx) : bnames) sx sy

9191 combine bnames h1 h2

@@ -119,6 +119,9 @@ match_unify ctxt env topx topy inj holes from =

119119 put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))

120120 return []

121121

122+ notHole (Hole _) = False

123+ notHole _ = True

124+

122125 -- TODO: there's an annoying amount of repetition between this and the

123126 -- main unification function. Consider lifting it out.

124127

@@ -173,7 +176,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

173176 uniqueBinders env (Bind n b sc)

174177 | n `elem` env

175178 = let n' = uniqueName n env in

176− Bind n' (fmap (uniqueBinders env) b)

179+ explicitHole $ Bind n' (fmap (uniqueBinders env) b)

177180 (uniqueBinders (n':env) (rename n n' sc))

178181 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

179182 (uniqueBinders (n:env) sc)

@@ -185,6 +188,10 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

185188 rename n n' (App f a) = App (rename n n' f) (rename n n' a)

186189 rename n n' t = t

187190

191+ explicitHole (Bind n (Hole ty) sc)

192+ = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

193+ explicitHole t = t

194+

188195trimSolutions ns = dropPairs ns

189196 where dropPairs [] = []

190197 dropPairs (n@(x, P _ x' _) : ns)

@@ -204,11 +211,16 @@ expandLets env (x, tm) = (x, doSubst (reverse env) tm)

204211 doSubst (_ : env) tm

205212 = doSubst env tm

206213

214+hasv (V x) = True

215+hasv (App f a) = hasv f || hasv a

216+hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

217+hasv _ = False

207218

208219unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->

209220 TC ([(Name, TT Name)], Fails)

210221unify ctxt env topx topy inj holes from =

211−-- trace ("Unifying " ++ show (topx, topy)) $

222+-- traceWhen (hasv topx || hasv topy)

223+-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

212224 -- don't bother if topx and topy are different at the head

213225 case runStateT (un False [] (renameBindersTm env topx)

214226 (renameBindersTm env topy)) (UI 0 []) of

@@ -295,7 +307,7 @@ unify ctxt env topx topy inj holes from =

295307 | injective ty && not (holeIn env x || x `elem` holes)

296308 = unifyTmpFail tx ty

297309 un' fn bnames xtm@(P _ x _) tm

298− | holeIn env x || x `elem` holes

310+ | pureTerm tm, holeIn env x || x `elem` holes

299311 = do UI s f <- get

300312 -- injectivity check

301313 x <- checkCycle bnames (x, tm)

@@ -305,11 +317,11 @@ unify ctxt env topx topy inj holes from =

305317 then unifyTmpFail xtm tm

306318 else do sc 1

307319 return x

308− | not (injective xtm) && injective tm

320+ | pureTerm tm, not (injective xtm) && injective tm

309321 = do checkCycle bnames (x, tm)

310322 unifyTmpFail xtm tm

311323 un' fn bnames tm ytm@(P _ y _)

312− | holeIn env y || y `elem` holes

324+ | pureTerm tm, holeIn env y || y `elem` holes

313325 = do UI s f <- get

314326 -- injectivity check

315327 x <- checkCycle bnames (y, tm)

@@ -319,7 +331,7 @@ unify ctxt env topx topy inj holes from =

319331 then unifyTmpFail tm ytm

320332 else do sc 1

321333 return x

322− | not (injective ytm) && injective tm

334+ | pureTerm tm, not (injective ytm) && injective tm

323335 = do checkCycle bnames (y, tm)

324336 unifyTmpFail tm ytm

325337 un' fn bnames (V i) (P _ x _)

@@ -524,7 +536,7 @@ unify ctxt env topx topy inj holes from =

524536 | not (x `elem` freeNames tm) = checkScope ns (x, tm)

525537 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

526538

527− checkScope ns (x, tm) =

539+ checkScope ns (x, tm) | pureTerm tm =

528540-- case boundVs (envPos x 0 env) tm of

529541-- [] -> return [(x, tm)]

530542-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))

@@ -535,6 +547,7 @@ unify ctxt env topx topy inj holes from =

535547 else return [(x, bind v ns tm)]

536548 where inst [] tm = tm

537549 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

550+ checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

538551

539552 bind i ns tm

540553 | i < 0 = tm