02367f9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Unification fix

02367f9Edwin Brady13 years ago

src/Core/Unify.hs+50−39

compare with master

unifiedsplit

@@ -7,6 +7,7 @@ import Core.Evaluate

8import Control.Monad

9import Control.Monad.State

10+import Data.List

10import Debug.Trace

11import Debug.Trace

12-- Unification is applied inside the theorem prover. We're looking for holes

13-- Unification is applied inside the theorem prover. We're looking for holes

@@ -124,8 +125,7 @@ unify ctxt env topx topy dont holes =

124 case runStateT (un False [] topxn topyn)

125 case runStateT (un False [] topxn topyn)

125 (UI 0 []) of

126 (UI 0 []) of

126 OK (v, UI _ fails) ->

127 OK (v, UI _ fails) ->

127− return (filter notTrivial v,

128+ return (filter notTrivial v, reverse fails)

128− reverse fails)

129-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

130 Error e -> tfail e

131 where

@@ -213,7 +213,38 @@ unify ctxt env topx topy dont holes =

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

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

215

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)

217 | (injective fx && injective fy)

248 | (injective fx && injective fy)

218 || (injective fx && rigid appx && metavarApp appy)

249 || (injective fx && rigid appx && metavarApp appy)

219 || (injective fy && rigid appy && metavarApp appx)

250 || (injective fy && rigid appy && metavarApp appx)

@@ -244,15 +275,17 @@ unify ctxt env topx topy dont holes =

244 do let (headx, argsx) = unApply appx

275 do let (headx, argsx) = unApply appx

245 let (heady, argsy) = unApply appy

276 let (heady, argsy) = unApply appy

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

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

278+ uplus (

247− if (length argsx == length argsy &&

279+ if (length argsx == length argsy &&

248− ((headx == heady && inenv headx) || (argsx == argsy) ||

280+ ((headx == heady && inenv headx) || (argsx == argsy) ||

249− (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))

281+ (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))

250− then

282+ then

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

283+-- (notFn headx && notFn heady))) then

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

284+ do uf <- un' True bnames headx heady

253− unArgs uf argsx argsy

285+ unArgs uf argsx argsy

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

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

255− unifyTmpFail appx appy

287+ unifyTmpFail appx appy)

288+ (unifyTmpFail appx appy) -- whole application fails

256 where hnormalise [] _ _ t = t

289 where hnormalise [] _ _ t = t

257 hnormalise ns ctxt env t = normalise ctxt env t

290 hnormalise ns ctxt env t = normalise ctxt env t

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

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

@@ -275,10 +308,13 @@ unify ctxt env topx topy dont holes =

275

308

276 metavarApp tm = let (f, args) = unApply tm in

309 metavarApp tm = let (f, args) = unApply tm in

277 all (\x -> metavar x) (f : args)

310 all (\x -> metavar x) (f : args)

311+ && nub args == args

278 metavarArgs tm = let (f, args) = unApply tm in

312 metavarArgs tm = let (f, args) = unApply tm in

279 all (\x -> metavar x || inenv x) args

313 all (\x -> metavar x || inenv x) args

314+ && nub args == args

280 metavarApp' tm = let (f, args) = unApply tm in

315 metavarApp' tm = let (f, args) = unApply tm in

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

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

317+ && nub args == args

282

318

283 sameArgStruct appx appy

319 sameArgStruct appx appy

284 = let (_, ax) = unApply appx

320 = let (_, ax) = unApply appx

@@ -322,38 +358,13 @@ unify ctxt env topx topy dont holes =

322

358

323 notFn t = injective t || metavar t || inenv t

359 notFn t = injective t || metavar t || inenv t

324

360

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

350

361

351 unifyTmpFail x y

362 unifyTmpFail x y

352 = do UI s f <- get

363 = do UI s f <- get

353 let r = recoverable x y

364 let r = recoverable x y

354 let err = CantUnify r

365 let err = CantUnify r

355 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

366 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))

357 return []

368 return []

358

369

359 -- shortcut failure, if we *know* nothing can fix it

370 -- shortcut failure, if we *know* nothing can fix it

@@ -361,7 +372,7 @@ unify ctxt env topx topy dont holes =

361 let r = recoverable x y

372 let r = recoverable x y

362 let err = CantUnify r

373 let err = CantUnify r

363 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

374 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))

365 lift $ tfail err

376 lift $ tfail err

366

377

367

378

test/reg010/expected+1−1

@@ -1,4 +1,4 @@

1reg010.idr:5:Can't unify P x with P y

3Specifically:

4− Can't unify x with y

4+ Can't unify P x with P y

test/reg021/expectednew file

No changes to the content.

test/reg021/reg021.idrnew file+22

@@ -0,0 +1,22 @@

1+module Main

3+%default total

5+data Ty = TyBool

7+data Id a = I a

9+interpTy : Ty -> Type

10+interpTy TyBool = Id Bool

11+

12+data Term : Ty -> Type where

13+ TLit : Bool -> Term TyBool

14+ TNot : Term TyBool -> Term TyBool

15+

16+map : (a -> b) -> Id a -> Id b

17+map f (I x) = I (f x)

18+

19+interp : Term t -> interpTy t

20+interp (TLit x) = I x

21+interp (TNot x) = map not (interp x)

22+

test/reg021/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ reg021.idr --check

3+rm -f *.ibc