c959fb0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Unification changes

c959fb0Edwin Brady13 years ago

libs/base/Data/Vect/Quantifiers.idr+4−4

compare with master

unifiedsplit

@@ -14,10 +14,10 @@ anyElim f _ (There p) = f p

15any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)

16any _ Nil = No anyNilAbsurd

17−any p (x::xs) with (p x)

17+any {P} p (x::xs) with (p x)

18 | Yes prf = Yes (Here prf)

19 | No prf =

20− case any p xs of

20+ case any {P} p xs of

21 Yes prf' => Yes (There prf')

22 No prf' => No (anyElim prf' prf)

@@ -39,9 +39,9 @@ notAllThere np (_ :: ps) = np ps

40all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)

41all _ Nil = Yes Nil

42−all d (x::xs) with (d x)

42+all {P} d (x::xs) with (d x)

43 | No prf = No (notAllHere prf)

44 | Yes prf =

45− case all d xs of

45+ case all {P} d xs of

46 Yes prf' => Yes (prf :: prf')

47 No prf' => No (notAllThere prf')

libs/effects/Effects.idr+20−19

@@ -152,21 +152,6 @@ syntax [tag] ":!" [val] = !(tag :- val)

152

153-- Eff : List (EFFECT m) -> Type -> Type

154

155−implicit

156−lift' : EffM m ys ys' t ->

157− {default tactics { byReflection reflectEff; }

158− prf : SubList ys xs} ->

159− EffM m xs (updateWith ys' xs prf) t

160−lift' e {prf} = lift prf e

161−

162−implicit

163−effect' : {a, b: _} -> {e : Effect} ->

164− (eff : e a b t) ->

165− {default tactics { byReflection reflectEff; }

166− prf : EffElem e a xs} ->

167− EffM m xs (updateResTy xs prf eff) t

168−effect' e {prf} = effect prf e

169−

170-- For making proofs implicitly for 'test' and 'test_lbl'

155-- For making proofs implicitly for 'test' and 'test_lbl'

171

156

172syntax if_valid then [e] else [t] =

157syntax if_valid then [e] else [t] =

@@ -224,8 +209,8 @@ execEff : Env m xs -> (p : EffElem e res xs) ->

224 (Env m (updateResTy xs p eff) -> a -> m t) -> m t

209 (Env m (updateResTy xs p eff) -> a -> m t) -> m t

225execEff (val :: env) Here eff' k

210execEff (val :: env) Here eff' k

226 = handle val eff' (\res, v => k (res :: env) v)

211 = handle val eff' (\res, v => k (res :: env) v)

227−execEff (val :: env) (There p) eff k

212+execEff {e} {a} {b} (val :: env) (There p) eff k

228− = execEff env p eff (\env', v => k (val :: env') v)

213+ = execEff {e} {a} {b} env p eff (\env', v => k (val :: env') v)

229

214

230private

215private

231testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->

216testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->

@@ -278,6 +263,22 @@ eff {xs = [l ::: x]} env (l :- prog) k

278 = let env' = unlabel env in

263 = let env' = unlabel env in

279 eff env' prog (\envk, p' => k (relabel l envk) p')

264 eff env' prog (\envk, p' => k (relabel l envk) p')

280

265

266+implicit

267+lift' : EffM m ys ys' t ->

268+ {default tactics { byReflection reflectEff; }

269+ prf : SubList ys xs} ->

270+ EffM m xs (updateWith ys' xs prf) t

271+lift' e {prf} = lift prf e

272+

273+implicit

274+effect' : {a, b: _} -> {e : Effect} ->

275+ (eff : e a b t) ->

276+ {default tactics { byReflection reflectEff; }

277+ prf : EffElem e a xs} ->

278+ EffM m xs (updateResTy xs prf eff) t

279+effect' e {prf} = effect prf e

280+

281+

281run : Applicative m => Env m xs -> EffM m xs xs' a -> m a

282run : Applicative m => Env m xs -> EffM m xs xs' a -> m a

282run env prog = eff env prog (\env, r => pure r)

283run env prog = eff env prog (\env, r => pure r)

283

284

@@ -287,8 +288,8 @@ runEnv env prog = eff env prog (\env, r => pure (env, r))

287runPure : Env id xs -> EffM id xs xs' a -> a

288runPure : Env id xs -> EffM id xs xs' a -> a

288runPure env prog = eff env prog (\env, r => r)

289runPure env prog = eff env prog (\env, r => r)

289

290

290−runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)

291+-- runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)

291−runPureEnv env prog = eff env prog (\env, r => (env, r))

292+-- runPureEnv env prog = eff env prog (\env, r => (env, r))

292

293

293runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a

294runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a

294runWith inj env prog = eff env prog (\env, r => inj r)

295runWith inj env prog = eff env prog (\env, r => inj r)

libs/neweffects/Effects.idr+19−17

@@ -183,21 +183,6 @@ data Eff : (m : Type -> Type) ->

183 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

184(>>=) = ebind

185

186−implicit

187−lift' : Eff m t ys ys' ->

188− {default tactics { byReflection reflectEff; }

189− prf : SubList ys xs} ->

190− Eff m t xs (\v => updateWith (ys' v) xs prf)

191−lift' e {prf} = lift prf e

192−

193−implicit

194−effect' : {a, b: _} -> {e : Effect} ->

195− (eff : e t a b) ->

196− {default tactics { byReflection reflectEff; }

197− prf : EffElem e a xs} ->

198− Eff m t xs (\v => updateResTy v xs prf eff)

199−effect' e {prf} = effect prf e

200−

201return : a -> Eff m a xs (\v => xs)

186return : a -> Eff m a xs (\v => xs)

202return x = value x

187return x = value x

203

188

@@ -222,8 +207,9 @@ execEff : Env m xs -> (p : EffElem e res xs) ->

222 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t

207 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t

223execEff (val :: env) Here eff' k

208execEff (val :: env) Here eff' k

224 = handle val eff' (\v, res => k v (res :: env))

209 = handle val eff' (\v, res => k v (res :: env))

210+-- FIXME: Teach the elaborator to propagate parameters here

225−execEff (val :: env) (There p) eff k

211+execEff {a} {res} {resk} (val :: env) (There p) eff k

226− = execEff env p eff (\v, env' => k v (val :: env'))

212+ = execEff {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))

227

213

228-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

214-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

229-- updates can be propagated even through failing computations?

215-- updates can be propagated even through failing computations?

@@ -260,6 +246,22 @@ syntax MkDefaultEnv = with Env

260 [default, default, default, default, default, default, default],

246 [default, default, default, default, default, default, default],

261 [default, default, default, default, default, default, default, default] |)

247 [default, default, default, default, default, default, default, default] |)

262

248

249+implicit

250+lift' : Eff m t ys ys' ->

251+ {default tactics { byReflection reflectEff; }

252+ prf : SubList ys xs} ->

253+ Eff m t xs (\v => updateWith (ys' v) xs prf)

254+lift' e {prf} = lift prf e

255+

256+implicit

257+effect' : {a, b: _} -> {e : Effect} ->

258+ (eff : e t a b) ->

259+ {default tactics { byReflection reflectEff; }

260+ prf : EffElem e a xs} ->

261+ Eff m t xs (\v => updateResTy v xs prf eff)

262+effect' e {prf} = effect prf e

263+

264+

263run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a

265run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a

264run {env} prog = eff env prog (\r, env => pure r)

266run {env} prog = eff env prog (\r, env => pure r)

265

267

libs/prelude/Prelude/Bits.idr+1−1

@@ -16,7 +16,7 @@ toHexDigit n = index n hexVect where

16 'A', 'B', 'C', 'D', 'E', 'F']

18b8ToString : Bits8 -> String

19−b8ToString c = pack [c1, c2] where

19+b8ToString c = pack (with List [c1, c2]) where

20 %assert_total -- We will only supply numbers that can fit in 4 bits

21 toFin16 : Bits8 -> Fin 16

22 toFin16 n = if n == 0

src/Idris/AbsSyntax.hs+1

@@ -950,6 +950,7 @@ expandParams dec ps ns infs tm = en tm

950 en (PAlternative a as) = PAlternative a (map en as)

951 en (PHidden t) = PHidden (en t)

952 en (PUnifyLog t) = PUnifyLog (en t)

953+ en (PDisamb ds t) = PDisamb ds (en t)

953 en (PNoImplicits t) = PNoImplicits (en t)

954 en (PNoImplicits t) = PNoImplicits (en t)

954 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

955 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

955 en (PProof ts) = PProof (map (fmap en) ts)

956 en (PProof ts) = PProof (map (fmap en) ts)

src/Idris/Core/Elaborate.hs+4

@@ -182,6 +182,10 @@ get_env :: Elab' aux Env

182get_env = do ES p _ _ <- get

183 lift $ envAtFocus (fst p)

184

185+get_inj :: Elab' aux [Name]

186+get_inj = do ES p _ _ <- get

187+ return $! (injective (fst p))

188+

185get_holes :: Elab' aux [Name]

189get_holes :: Elab' aux [Name]

186get_holes = do ES p _ _ <- get

190get_holes = do ES p _ _ <- get

187 return $! (holes (fst p))

191 return $! (holes (fst p))

src/Idris/Core/ProofState.hs+21−6

@@ -154,7 +154,8 @@ match_unify' :: Context -> Env -> TT Name -> TT Name ->

154match_unify' ctxt env topx topy =

155 do ps <- get

156 let dont = dontunify ps

157+ let inj = injective ps

157− u <- lift $ match_unify ctxt env topx topy dont (holes ps)

158+ u <- lift $ match_unify ctxt env topx topy inj (holes ps)

158 let (h, ns) = unified ps

159 let (h, ns) = unified ps

159 put (ps { unified = (h, u ++ ns) })

160 put (ps { unified = (h, u ++ ns) })

160 return u

161 return u

@@ -164,11 +165,14 @@ unify' :: Context -> Env -> TT Name -> TT Name ->

164unify' ctxt env topx topy =

165unify' ctxt env topx topy =

165 do ps <- get

166 do ps <- get

166 let dont = dontunify ps

167 let dont = dontunify ps

168+ let inj = injective ps

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

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

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

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

169 " in " ++ show env ++

171 " in " ++ show env ++

170− "\nHoles: " ++ show (holes ps) ++ "\n") $

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

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

174+ ++ "\n") $

171− lift $ unify ctxt env topx topy dont (holes ps)

175+ lift $ unify ctxt env topx topy inj (holes ps)

172 let notu = filter (\ (n, t) -> case t of

176 let notu = filter (\ (n, t) -> case t of

173 P _ _ _ -> False

177 P _ _ _ -> False

174 _ -> n `elem` dont) u

178 _ -> n `elem` dont) u

@@ -187,8 +191,16 @@ unify' ctxt env topx topy =

187 (holes ps)

191 (holes ps)

188 put (ps { problems = probs',

192 put (ps { problems = probs',

189 unified = (h, ns'),

193 unified = (h, ns'),

194+ injective = updateInj u (injective ps),

190 notunified = notu ++ notunified ps })

195 notunified = notu ++ notunified ps })

191 return u

196 return u

197+ where updateInj ((n, a) : us) inj

198+ | (P _ n' _, _) <- unApply a,

199+ n `elem` inj = updateInj us (n':inj)

200+ | (P _ n' _, _) <- unApply a,

201+ n' `elem` inj = updateInj us (n:inj)

202+ updateInj (_ : us) inj = updateInj us inj

203+ updateInj [] inj = inj

192

204

193getName :: Monad m => String -> StateT TState m Name

205getName :: Monad m => String -> StateT TState m Name

194getName tag = do ps <- get

206getName tag = do ps <- get

@@ -358,10 +370,10 @@ instanceArg n ctxt env (Bind x (Hole t) sc)

358 return (Bind x (Hole t) sc)

370 return (Bind x (Hole t) sc)

359

371

360setinj :: Name -> RunTactic

372setinj :: Name -> RunTactic

361−setinj n ctxt env (Bind x (Hole t) sc)

373+setinj n ctxt env (Bind x b sc)

362 = do action (\ps -> let is = injective ps in

374 = do action (\ps -> let is = injective ps in

363 ps { injective = n : is })

375 ps { injective = n : is })

364− return (Bind x (Hole t) sc)

376+ return (Bind x b sc)

365

377

366defer :: Name -> RunTactic

378defer :: Name -> RunTactic

367defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

379defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

@@ -526,8 +538,11 @@ forall n ty ctxt env _ = fail "Can't pi bind here"

526

538

527patvar :: Name -> RunTactic

539patvar :: Name -> RunTactic

528patvar n ctxt env (Bind x (Hole t) sc) =

540patvar n ctxt env (Bind x (Hole t) sc) =

529− do action (\ps -> ps { holes = holes ps \\ [x] })

541+ do action (\ps -> ps { holes = holes ps \\ [x],

542+ injective = addInj n x (injective ps) })

530 return $ Bind n (PVar t) (subst x (P Bound n t) sc)

543 return $ Bind n (PVar t) (subst x (P Bound n t) sc)

544+ where addInj n x ps | x `elem` ps = n : ps

545+ | otherwise = ps

531patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm

546patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm

532

547

533letbind :: Name -> Raw -> Raw -> RunTactic

548letbind :: Name -> Raw -> Raw -> RunTactic

src/Idris/Core/Unify.hs+47−29

@@ -33,7 +33,7 @@ data UResult a = UOK a

34match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

35 TC [(Name, TT Name)]

36−match_unify ctxt env topx topy dont holes =

36+match_unify ctxt env topx topy inj holes =

37 case runStateT (un [] topx topy) (UI 0 []) of

38 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))

39 res ->

@@ -169,7 +169,7 @@ expandLets env (x, tm) = (x, doSubst (reverse env) tm)

169

170unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

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

172−unify ctxt env topx topy dont holes =

172+unify ctxt env topx topy inj holes =

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

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

175 case runStateT (un False [] topx topy) (UI 0 []) of

@@ -198,12 +198,20 @@ unify ctxt env topx topy dont holes =

198 injective (App f a) = injective f -- && injective a

199 injective _ = False

200

201+-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK

202+ injectiveVar (P _ n _) = n `elem` inj

203+ injectiveVar (App f a) = injectiveVar f -- && injective a

204+ injectiveVar _ = False

205+

206+ injectiveApp x = injective x || injectiveVar x

207+

201 notP (P _ _ _) = False

208 notP (P _ _ _) = False

202 notP _ = True

209 notP _ = True

203

210

204 sc i = do UI s f <- get

211 sc i = do UI s f <- get

205 put (UI (s+i) f)

212 put (UI (s+i) f)

206

213

214+ errors :: StateT UInfo TC Bool

207 errors = do UI s f <- get

215 errors = do UI s f <- get

208 return (not (null f))

216 return (not (null f))

209

217

@@ -302,9 +310,18 @@ unify ctxt env topx topy dont holes =

302 -- class resolution for type classes over functions.

310 -- class resolution for type classes over functions.

303

311

304 un' fn bnames (App f x) (Bind n (Pi t) y)

312 un' fn bnames (App f x) (Bind n (Pi t) y)

305− | noOccurrence n y && x == y

313+ | noOccurrence n y && injectiveApp f

314+ = do ux <- un' False bnames x y

315+ uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

316+ (Bind n (Pi t) (V 1)))

317+ combine bnames ux uf

318+

319+ un' fn bnames (Bind n (Pi t) y) (App f x)

320+ | noOccurrence n y && injectiveApp f

321+ = do ux <- un' False bnames y x

306− = un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

322+ uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

307− (Bind n (Pi t) (V 1)))

323+ (Bind n (Pi t) (V 1))) f

324+ combine bnames ux uf

308

325

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

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

310 = do h1 <- uB bnames bx by

327 = do h1 <- uB bnames bx by

@@ -321,11 +338,11 @@ unify ctxt env topx topy dont holes =

321 return [] -- lift $ tfail err

338 return [] -- lift $ tfail err

322

339

323 unApp fn bnames appx@(App fx ax) appy@(App fy ay)

340 unApp fn bnames appx@(App fx ax) appy@(App fy ay)

324− | (injective fx && injective fy)

341+ | (injectiveApp fx && injectiveApp fy)

325− || (injective fx && rigid appx && metavarApp appy)

342+ || (injectiveApp fx && rigid appx && metavarApp appy)

326− || (injective fy && rigid appy && metavarApp appx)

343+ || (injectiveApp fy && rigid appy && metavarApp appx)

327− || (injective fx && metavarApp fy && ax == ay)

344+ || (injectiveApp fx && metavarApp fy && ax == ay)

328− || (injective fy && metavarApp fx && ax == ay)

345+ || (injectiveApp fy && metavarApp fx && ax == ay)

329 = do let (headx, _) = unApply fx

346 = do let (headx, _) = unApply fx

330 let (heady, _) = unApply fy

347 let (heady, _) = unApply fy

331 -- fail quickly if the heads are disjoint

348 -- fail quickly if the heads are disjoint

@@ -347,23 +364,24 @@ unify ctxt env topx topy dont holes =

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

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

348 sc 1

365 sc 1

349 combine bnames hf ha)

366 combine bnames hf ha)

350− | otherwise = -- trace (show (appx, appy, injective fx, metavarApp appy, sameArgStruct appx appy)) $

367+ | otherwise = -- FIXME: This fudge should be:

368+ unifyTmpFail appx appy

351− do let (headx, argsx) = unApply appx

369+-- do let (headx, argsx) = unApply appx

352− let (heady, argsy) = unApply appy

370+-- let (heady, argsy) = unApply appy

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

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

354− uplus (

372+-- uplus (

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

373+-- if (length argsx == length argsy &&

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

374+-- ((headx == heady && inenv headx) || (argsx == argsy) ||

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

375+-- (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))

358− then

376+-- then

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

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

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

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

361− failed <- errors

379+-- failed <- errors

362− if (not failed) then unArgs uf argsx argsy

380+-- if (not failed) then unArgs uf argsx argsy

363− else return []

381+-- else return []

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

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

365− unifyTmpFail appx appy)

383+-- unifyTmpFail appx appy)

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

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

367 where hnormalise [] _ _ t = t

385 where hnormalise [] _ _ t = t

368 hnormalise ns ctxt env t = normalise ctxt env t

386 hnormalise ns ctxt env t = normalise ctxt env t

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

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

@@ -433,8 +451,7 @@ unify ctxt env topx topy dont holes =

433 _ -> False

451 _ -> False

434

452

435 metavar t = case t of

453 metavar t = case t of

436− P _ x _ -> ((x `elem` holes || holeIn env x) &&

454+ P _ x _ -> (x `elem` holes || holeIn env x)

437− not (x `elem` dont))

438 || globmetavar t

455 || globmetavar t

439 _ -> False

456 _ -> False

440 pat t = case t of

457 pat t = case t of

@@ -447,6 +464,7 @@ unify ctxt env topx topy dont holes =

447 notFn t = injective t || metavar t || inenv t

464 notFn t = injective t || metavar t || inenv t

448

465

449

466

467+ unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]

450 unifyTmpFail x y

468 unifyTmpFail x y

451 = do UI s f <- get

469 = do UI s f <- get

452 let r = recoverable x y

470 let r = recoverable x y

src/Idris/ElabDecls.hs+23−9

@@ -696,7 +696,7 @@ elabTransform info fc safe lhs_in rhs_in

696 let rhs = addImplBound i (map fst newargs) rhs_in

697 ((rhs', defer), _) <-

698 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []

699− (do pbinds lhs_tm

699+ (do pbinds i lhs_tm

700 setNextName

701 erun fc (build i info False [] (sUN "transform") rhs)

702 erun fc $ psolve lhs_tm

@@ -1296,12 +1296,13 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1296 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

1297 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

1298

1299− (((lhs', dlhs, []), probs), _) <-

1299+ (((lhs', dlhs, []), probs, inj), _) <-

1300 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1301 (do res <- errAt "left hand side of " fname

1302 (erun fc (buildTC i info True opts fname (infTerm lhs)))

1303 probs <- get_probs

1304+ inj <- get_inj

1304− return (res, probs))

1305+ return (res, probs, inj))

1305

1306

1306 when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)

1307 when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)

1307

1308

@@ -1309,6 +1310,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1309 let lhs_ty = getInferType lhs'

1310 let lhs_ty = getInferType lhs'

1310 logLvl 3 ("Elaborated: " ++ show lhs_tm)

1311 logLvl 3 ("Elaborated: " ++ show lhs_tm)

1311 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

1312 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

1313+ logLvl 5 ("Injective: " ++ show fname ++ " " ++ show inj)

1312

1314

1313 -- If we're inferring metavariables in the type, don't recheck,

1315 -- If we're inferring metavariables in the type, don't recheck,

1314 -- because we're only doing this to try to work out those metavariables

1316 -- because we're only doing this to try to work out those metavariables

@@ -1351,7 +1353,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1351 logLvl 5 "STARTING CHECK"

1353 logLvl 5 "STARTING CHECK"

1352 ((rhs', defer, is, probs), _) <-

1354 ((rhs', defer, is, probs), _) <-

1353 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

1355 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

1354− (do pbinds lhs_tm

1356+ (do pbinds ist lhs_tm

1357+ mapM_ setinj inj

1355 setNextName

1358 setNextName

1356 (_, _, is) <- errAt "right hand side of " fname

1359 (_, _, is) <- errAt "right hand side of " fname

1357 (erun fc (build i info False opts fname rhs))

1360 (erun fc (build i info False opts fname rhs))

@@ -1523,7 +1526,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1523 ((wval', defer, is), _) <-

1526 ((wval', defer, is), _) <-

1524 tclift $ elaborate ctxt (sMN 0 "withRHS")

1527 tclift $ elaborate ctxt (sMN 0 "withRHS")

1525 (bindTyArgs PVTy bargs infP) []

1528 (bindTyArgs PVTy bargs infP) []

1526− (do pbinds lhs_tm

1529+ (do pbinds i lhs_tm

1527 setNextName

1530 setNextName

1528 -- TODO: may want where here - see winfo abpve

1531 -- TODO: may want where here - see winfo abpve

1529 (_', d, is) <- errAt "with value in " fname

1532 (_', d, is) <- errAt "with value in " fname

@@ -1587,7 +1590,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1587 i <- getIState

1590 i <- getIState

1588 ((rhs', defer, is), _) <-

1591 ((rhs', defer, is), _) <-

1589 tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []

1592 tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []

1590− (do pbinds lhs_tm

1593+ (do pbinds i lhs_tm

1591 setNextName

1594 setNextName

1592 (_, d, is) <- erun fc (build i info False opts fname rhs)

1595 (_, d, is) <- erun fc (build i info False opts fname rhs)

1593 psolve lhs_tm

1596 psolve lhs_tm

@@ -2058,9 +2061,20 @@ decorateid decorate (PClauses f o n cs)

2058 dappname t = t

2061 dappname t = t

2059

2062

2060

2063

2064+-- if 't' is a type class application, assume its arguments are injective

2065+pbinds :: IState -> Term -> ElabD ()

2061−pbinds (Bind n (PVar t) sc) = do attack; patbind n

2066+pbinds i (Bind n (PVar t) sc)

2067+ = do attack; patbind n

2068+ case unApply t of

2069+ (P _ c _, args) -> case lookupCtxt c (idris_classes i) of

2070+ [] -> return ()

2071+ _ -> -- type class, set as injective

2072+ mapM_ setinjArg args

2073+ _ -> return ()

2062− pbinds sc

2074+ pbinds i sc

2075+ where setinjArg (P _ n _) = setinj n

2076+ setinjArg _ = return ()

2063−pbinds tm = return ()

2077+pbinds i tm = return ()

2064

2078

2065pbty (Bind n (PVar t) sc) tm = Bind n (PVTy t) (pbty sc tm)

2079pbty (Bind n (PVar t) sc) tm = Bind n (PVTy t) (pbty sc tm)

2066pbty _ tm = tm

2080pbty _ tm = tm

src/Idris/ElabTerm.hs+23−5

@@ -125,6 +125,7 @@ elab ist info pattern opts fn tm

125 end_unify

126 when pattern -- convert remaining holes to pattern vars

127 (do update_term orderPats

128+ matchProblems; unifyProblems

128 mkPat)

129 mkPat)

129 where

130 where

130 tcgen = Dictionary `elem` opts

131 tcgen = Dictionary `elem` opts

@@ -453,6 +454,8 @@ elab ist info pattern opts fn tm

453-- trace ("args is " ++ show args) $ return ()

454-- trace ("args is " ++ show args) $ return ()

454 ns <- apply (Var f) (map isph args)

455 ns <- apply (Var f) (map isph args)

455-- trace ("ns is " ++ show ns) $ return ()

456-- trace ("ns is " ++ show ns) $ return ()

457+ -- mark any type class arguments as injective

458+ mapM_ checkIfInjective (map snd ns)

456 -- Sort so that the implicit tactics and alternatives go last

459 -- Sort so that the implicit tactics and alternatives go last

457 let (ns', eargs) = unzip $

460 let (ns', eargs) = unzip $

458 sortBy cmpArg (zip ns args)

461 sortBy cmpArg (zip ns args)

@@ -475,16 +478,29 @@ elab ist info pattern opts fn tm

475 (movelast n)

478 (movelast n)

476 else movelast n)

479 else movelast n)

477 (ivs' \\ ivs)

480 (ivs' \\ ivs)

478− where tcArg (n, PConstraint _ _ Placeholder _) = True

479− tcArg _ = False

480−

481− -- normal < tactic < default tactic

481+ where -- normal < tactic < default tactic

482 cmpArg (_, x) (_, y)

483 = compare (priority x + alt x) (priority y + alt y)

484 where alt t = case getTm t of

485 PAlternative False _ -> 5

486 _ -> 0

487

488+ checkIfInjective n = do

489+ env <- get_env

490+ case lookup n env of

491+ Nothing -> return ()

492+ Just b ->

493+ case unApply (binderTy b) of

494+ (P _ c _, args) ->

495+ case lookupCtxt c (idris_classes ist) of

496+ [] -> return ()

497+ _ -> -- type class, set as injective

498+ mapM_ setinjArg args

499+ _ -> return ()

500+

501+ setinjArg (P _ n _) = setinj n

502+ setinjArg _ = return ()

503+

488 tacTm (PTactics _) = True

504 tacTm (PTactics _) = True

489 tacTm (PProof _) = True

505 tacTm (PProof _) = True

490 tacTm _ = False

506 tacTm _ = False

@@ -918,7 +934,9 @@ runTac :: Bool -> IState -> PTactic -> ElabD ()

918runTac autoSolve ist tac

934runTac autoSolve ist tac

919 = do env <- get_env

935 = do env <- get_env

920 g <- goal

936 g <- goal

937+ if autoSolve

938+ then runT (fmap (addImplBound ist (map fst env)) tac)

921− no_errors (runT (fmap (addImplBound ist (map fst env)) tac))

939+ else no_errors (runT (fmap (addImplBound ist (map fst env)) tac))

922 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))

940 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))

923 where

941 where

924 runT (Intro []) = do g <- goal

942 runT (Intro []) = do g <- goal

src/Idris/ErrReverse.hs+1−1

@@ -13,7 +13,7 @@ import Debug.Trace

13-- errors will be more readable

15errReverse :: IState -> Term -> Term

16−errReverse ist t = rewrite 5 (elideLambdas t)

16+errReverse ist t = rewrite 5 t -- (elideLambdas t)

17 where

19 rewrite 0 t = t

test/reg025/reg025.idr+2−2

@@ -27,10 +27,10 @@ indexStep = refl

27find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)

28 -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))

29find _ Nil = Left Nil

30−find d (x::xs) with (d x)

30+find {P} d (x::xs) with (d x)

31 | Yes prf = Right (x ** (prf, (fZ ** refl)))

32 | No prf =

33− case find d xs of

33+ case find {P} d xs of

34 Right (y ** (prf', (i ** prf''))) =>

35 Right (y ** (prf', (fS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

36 Left prf' => Left (prf::prf')

test/reg026/reg026.idr+3−3

@@ -9,6 +9,6 @@ column = getWitness

9data Action = Left | Ahead | Right

11admissible : X t -> Action -> Bool

12−admissible x Ahead = column x == 0 || column x == 4

12+admissible {t} x Ahead = column {t} x == 0 || column {t} x == 4

13−admissible x Left = column x <= 2

13+admissible {t} x Left = column {t} x <= 2

14−admissible x Right = column x >= 2

14+admissible {t} x Right = column {t} x >= 2

test/reg027/reg027.idr+1−1

@@ -16,7 +16,7 @@ instance Applicative (\x => Int -> x) where

16 pure v = \x => v

17 (<$>) f a = \x => f x (a x)

19−instance Monad (\x => Int -> x) where

19+instance Monad IntFn where

20 f >>= k = \x => k (f x) x

22dbl : IntFn Int