6d3863d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better environment management in unification

6d3863dEdwin Brady13 years ago

src/Idris/Core/ProofState.hs+2

compare with master

unifiedsplit

@@ -184,6 +184,8 @@ unify' ctxt env topx topy =

184 let inj = injective ps

185 (u, fails) <- traceWhen (unifylog ps)

186 ("Trying " ++ show (topx, topy) ++

187+ "\nNormalised " ++ show (normalise ctxt env topx,

188+ normalise ctxt env topy) ++

187 " in " ++ show env ++

189 " in " ++ show env ++

188 "\nHoles: " ++ show (holes ps)

190 "\nHoles: " ++ show (holes ps)

189 ++ "\nInjective: " ++ show (injective ps)

191 ++ "\nInjective: " ++ show (injective ps)

src/Idris/Core/Unify.hs+64−61

@@ -63,12 +63,16 @@ match_unify ctxt env topx topy inj holes =

63 | holeIn env y || y `elem` holes

64 = do sc 1; checkCycle names (y, tm)

65 un bnames (V i) (P _ x _)

66+ | length bnames > i,

67+ fst (fst (bnames!!i)) == x ||

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

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

67 un bnames (P _ x _) (V i)

69 un bnames (P _ x _) (V i)

70+ | length bnames > i,

71+ fst (fst (bnames!!i)) == x ||

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

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

69 un bnames (Bind x bx sx) (Bind y by sy)

73 un bnames (Bind x bx sx) (Bind y by sy)

70 = do h1 <- uB bnames bx by

74 = do h1 <- uB bnames bx by

71− h2 <- un ((x, y) : bnames) sx sy

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

72 combine bnames h1 h2

76 combine bnames h1 h2

73 un names (App fx ax) (App fy ay)

77 un names (App fx ax) (App fy ay)

74 = do hf <- un names fx fy

78 = do hf <- un names fx fy

@@ -126,12 +130,22 @@ match_unify ctxt env topx topy inj holes =

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

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

127

131

128 checkScope ns (x, tm) =

132 checkScope ns (x, tm) =

129− case boundVs (envPos x 0 env) tm of

133+-- case boundVs (envPos x 0 env) tm of

130− [] -> return [(x, tm)]

134+-- [] -> return [(x, tm)]

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

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

132− (inst ns tm) (errEnv env))

136+-- (inst ns tm) (errEnv env))

137+ let v = highV (-1) tm in

138+ if v >= length ns

139+ then lift $ tfail (Msg "SCOPE ERROR")

140+ else return [(x, bind (highV (-1) tm) ns tm)]

133 where inst [] tm = tm

141 where inst [] tm = tm

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

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

143+

144+ bind i ns tm

145+ | i < 0 = tm

146+ | otherwise = let ((x,y),ty) = ns!!i in

147+ App (Bind y (Lam ty) (bind (i-1) ns tm))

148+ (P Bound x ty)

135

149

136renameBinders :: Env -> (Name, TT Name) -> (Name, TT Name)

150renameBinders :: Env -> (Name, TT Name) -> (Name, TT Name)

137renameBinders env (x, tm) = (x, uniqueBinders tm)

151renameBinders env (x, tm) = (x, uniqueBinders tm)

@@ -225,7 +239,7 @@ unify ctxt env topx topy inj holes =

225 then return r

239 then return r

226 else do put (UI s f); u2

240 else do put (UI s f); u2

227

241

228− un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

242+ un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

229 StateT UInfo

243 StateT UInfo

230 TC [(Name, TT Name)]

244 TC [(Name, TT Name)]

231 un = un'

245 un = un'

@@ -236,7 +250,7 @@ unify ctxt env topx topy inj holes =

236-- uplus (un' fn names x y)

250-- uplus (un' fn names x y)

237-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))

251-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))

238

252

239− un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

253+ un' :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

240 StateT UInfo

254 StateT UInfo

241 TC [(Name, TT Name)]

255 TC [(Name, TT Name)]

242 un' fn names x y | x == y = return [] -- shortcut

256 un' fn names x y | x == y = return [] -- shortcut

@@ -253,7 +267,7 @@ unify ctxt env topx topy inj holes =

253 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)

267 un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)

254 = unifyFail topx topy

268 = unifyFail topx topy

255 un' fn bnames tx@(P _ x _) ty@(P _ y _)

269 un' fn bnames tx@(P _ x _) ty@(P _ y _)

256− | (x,y) `elem` bnames || x == y = do sc 1; return []

270+ | (x,y) `elem` map fst bnames || x == y = do sc 1; return []

257 | injective tx && not (holeIn env y || y `elem` holes)

271 | injective tx && not (holeIn env y || y `elem` holes)

258 = unifyTmpFail tx ty

272 = unifyTmpFail tx ty

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

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

@@ -287,9 +301,16 @@ unify ctxt env topx topy inj holes =

287 = do checkCycle bnames (y, tm)

301 = do checkCycle bnames (y, tm)

288 unifyTmpFail tm ytm

302 unifyTmpFail tm ytm

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

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

304+ | length bnames > i,

305+ fst ((map fst bnames)!!i) == x ||

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

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

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

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

308+ | length bnames > i,

309+ fst ((map fst bnames)!!i) == x ||

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

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

311+

312+ un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y

313+ un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy

293

314

294 un' fn bnames appx@(App _ _) appy@(App _ _)

315 un' fn bnames appx@(App _ _) appy@(App _ _)

295 = unApp fn bnames appx appy

316 = unApp fn bnames appx appy

@@ -327,9 +348,13 @@ unify ctxt env topx topy inj holes =

327 combine bnames ux uf

348 combine bnames ux uf

328

349

329 un' fn bnames (Bind x bx sx) (Bind y by sy)

350 un' fn bnames (Bind x bx sx) (Bind y by sy)

351+ | sameBinder bx by

330− = do h1 <- uB bnames bx by

352+ = do h1 <- uB bnames bx by

331− h2 <- un' False ((x,y):bnames) sx sy

353+ h2 <- un' False (((x,y),binderTy bx):bnames) sx sy

332− combine bnames h1 h2

354+ combine bnames h1 h2

355+ where sameBinder (Lam _) (Lam _) = True

356+ sameBinder (Pi _) (Pi _) = True

357+ sameBinder _ _ = False

333 un' fn bnames x y

358 un' fn bnames x y

334 | OK True <- convEq' ctxt x y = do sc 1; return []

359 | OK True <- convEq' ctxt x y = do sc 1; return []

335 | otherwise = do UI s f <- get

360 | otherwise = do UI s f <- get

@@ -367,24 +392,7 @@ unify ctxt env topx topy inj holes =

367 hf <- un' False bnames fx' fy'

392 hf <- un' False bnames fx' fy'

368 sc 1

393 sc 1

369 combine bnames hf ha)

394 combine bnames hf ha)

370− | otherwise = -- FIXME: This fudge should be:

371− unifyTmpFail appx appy

372−-- do let (headx, argsx) = unApply appx

373−-- let (heady, argsy) = unApply appy

374−-- -- traceWhen (headx == heady) (show (appx, appy)) $

375−-- uplus (

376−-- if (length argsx == length argsy &&

377−-- ((headx == heady && inenv headx) || (argsx == argsy) ||

378−-- (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))

379−-- then

380−-- -- (notFn headx && notFn heady))) then

381−-- do uf <- un' True bnames headx heady

382−-- failed <- errors

383−-- if (not failed) then unArgs uf argsx argsy

384−-- else return []

385−-- else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $

386−-- unifyTmpFail appx appy)

395+ | otherwise = unifyTmpFail appx appy

387−-- (unifyTmpFail appx appy) -- whole application fails

388 where hnormalise [] _ _ t = t

396 where hnormalise [] _ _ t = t

389 hnormalise ns ctxt env t = normalise ctxt env t

397 hnormalise ns ctxt env t = normalise ctxt env t

390 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

398 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

@@ -417,28 +425,6 @@ unify ctxt env topx topy inj holes =

417 all (\x -> pat x || metavar x) (f : args)

425 all (\x -> pat x || metavar x) (f : args)

418 && nub args == args

426 && nub args == args

419

427

420− sameArgStruct appx appy

421− = let (_, ax) = unApply appx

422− (_, ay) = unApply appy in

423− length ax == length ay &&

424− and (zipWith sameStruct ax ay)

425−

426− sameStruct fapp@(App f x) gapp@(App g y)

427− = let (f',a') = unApply fapp

428− (g',b') = unApply gapp in

429− (f' == g' && length a' == length b' &&

430− (injective f' || injective g'))

431− || (sameStruct f g && sameStruct x y)

432− sameStruct (P _ x _) (P _ y _) = True

433− sameStruct (V i) (V j) = i == j

434− sameStruct (Constant x) (Constant y) = True

435− sameStruct (P _ _ _) (Constant y) = True

436− sameStruct (Constant x) (P _ _ _) = True

437− sameStruct (Bind n t sc) (P _ _ _) = True

438− sameStruct (P _ _ _) (Bind n t sc) = True

439− sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'

440− sameStruct _ _ = False

441−

442 rigid (P (DCon _ _) _ _) = True

428 rigid (P (DCon _ _) _ _) = True

443 rigid (P (TCon _ _) _ _) = True

429 rigid (P (TCon _ _) _ _) = True

444 rigid t@(P Ref _ _) = inenv t || globmetavar t

430 rigid t@(P Ref _ _) = inenv t || globmetavar t

@@ -513,12 +499,22 @@ unify ctxt env topx topy inj holes =

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

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

514

500

515 checkScope ns (x, tm) =

501 checkScope ns (x, tm) =

516− case boundVs (envPos x 0 env) tm of

502+-- case boundVs (envPos x 0 env) tm of

517− [] -> return [(x, tm)]

503+-- [] -> return [(x, tm)]

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

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

519− (inst ns tm) (errEnv env))

505+-- (inst ns tm) (errEnv env))

506+ let v = highV (-1) tm in

507+ if v >= length ns

508+ then lift $ tfail (Msg "SCOPE ERROR")

509+ else return [(x, bind (highV (-1) tm) ns tm)]

520 where inst [] tm = tm

510 where inst [] tm = tm

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

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

512+

513+ bind i ns tm

514+ | i < 0 = tm

515+ | otherwise = let ((x,y),ty) = ns!!i in

516+ App (Bind y (Lam ty) (bind (i-1) ns tm))

517+ (P Bound x ty)

522

518

523 combineArgs bnames args = ca [] args where

519 combineArgs bnames args = ca [] args where

524 ca acc [] = return acc

520 ca acc [] = return acc

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

536 combine bnames as (ns' ++ bs)

532 combine bnames as (ns' ++ bs)

537

533

538boundVs :: Int -> Term -> [Int]

534boundVs :: Int -> Term -> [Int]

539−boundVs i (V j) | j <= i = []

535+boundVs i (V j) | j < i = []

540 | otherwise = [j]

536 | otherwise = [j]

541boundVs i (Bind n b sc) = boundVs (i + 1) sc

537boundVs i (Bind n b sc) = boundVs (i + 1) sc

542boundVs i (App f x) = let fs = boundVs i f

538boundVs i (App f x) = let fs = boundVs i f

@@ -544,6 +540,13 @@ boundVs i (App f x) = let fs = boundVs i f

544 nub (fs ++ xs)

540 nub (fs ++ xs)

545boundVs i _ = []

541boundVs i _ = []

546

542

543+highV :: Int -> Term -> Int

544+highV i (V j) | j > i = j

545+ | otherwise = i

546+highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]

547+highV i (App f x) = max (highV i f) (highV i x)

548+highV i _ = i

549+

547envPos x i [] = 0

550envPos x i [] = 0

548envPos x i ((y, _) : ys) | x == y = i

551envPos x i ((y, _) : ys) | x == y = i

549 | otherwise = envPos x (i + 1) ys

552 | otherwise = envPos x (i + 1) ys