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

git.iko.soy/Idris-dev

on master help sign in

Avoid hole bindings in unification solutions

45c8ecaEdwin Brady12 years ago

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

compare with master

unifiedsplit

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

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

538

539convEq :: 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

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

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

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

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

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

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

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

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

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

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

555+ | otherwise = return False

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

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

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

558+ | otherwise = return False

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

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

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

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

557 where

561 where

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

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

85 | length bnames > i,

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

87 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

89 = do h1 <- uB bnames bx by

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

91 combine bnames h1 h2

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

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

120 return []

121

122+ notHole (Hole _) = False

123+ notHole _ = True

124+

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

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

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

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

124

127

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

173 uniqueBinders env (Bind n b sc)

176 uniqueBinders env (Bind n b sc)

174 | n `elem` env

177 | n `elem` env

175 = let n' = uniqueName n env in

178 = let n' = uniqueName n env in

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

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

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

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

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

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

179 (uniqueBinders (n:env) sc)

182 (uniqueBinders (n:env) sc)

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

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

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

186 rename n n' t = t

189 rename n n' t = t

187

190

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

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

193+ explicitHole t = t

194+

188trimSolutions ns = dropPairs ns

195trimSolutions ns = dropPairs ns

189 where dropPairs [] = []

196 where dropPairs [] = []

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

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

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

204 doSubst (_ : env) tm

211 doSubst (_ : env) tm

205 = doSubst env tm

212 = doSubst env tm

206

213

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

207

218

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

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

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

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

210unify ctxt env topx topy inj holes from =

221unify ctxt env topx topy inj holes from =

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

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

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

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

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

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

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

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

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

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

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

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

296 = unifyTmpFail tx ty

308 = unifyTmpFail tx ty

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

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

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

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

299 = do UI s f <- get

311 = do UI s f <- get

300 -- injectivity check

312 -- injectivity check

301 x <- checkCycle bnames (x, tm)

313 x <- checkCycle bnames (x, tm)

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

305 then unifyTmpFail xtm tm

317 then unifyTmpFail xtm tm

306 else do sc 1

318 else do sc 1

307 return x

319 return x

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

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

309 = do checkCycle bnames (x, tm)

321 = do checkCycle bnames (x, tm)

310 unifyTmpFail xtm tm

322 unifyTmpFail xtm tm

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

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

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

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

313 = do UI s f <- get

325 = do UI s f <- get

314 -- injectivity check

326 -- injectivity check

315 x <- checkCycle bnames (y, tm)

327 x <- checkCycle bnames (y, tm)

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

319 then unifyTmpFail tm ytm

331 then unifyTmpFail tm ytm

320 else do sc 1

332 else do sc 1

321 return x

333 return x

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

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

323 = do checkCycle bnames (y, tm)

335 = do checkCycle bnames (y, tm)

324 unifyTmpFail tm ytm

336 unifyTmpFail tm ytm

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

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

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

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

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

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

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

526

538

527− checkScope ns (x, tm) =

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

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

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

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

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

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

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

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

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

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

536 where inst [] tm = tm

548 where inst [] tm = tm

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

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

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

538

551

539 bind i ns tm

552 bind i ns tm

540 | i < 0 = tm

553 | i < 0 = tm