c959fb0 · Idris-dev · git.iko.soy

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

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

1414

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

1616any _ Nil = No anyNilAbsurd

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

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

1818 | Yes prf = Yes (Here prf)

1919 | No prf =

20− case any p xs of

20+ case any {P} p xs of

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

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

2323

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

3939

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

4141all _ Nil = Yes Nil

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

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

4343 | No prf = No (notAllHere prf)

4444 | Yes prf =

45− case all d xs of

45+ case all {P} d xs of

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

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

libs/effects/Effects.idr+20−19

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

152152

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

154154

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−

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

171156

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

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

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

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

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

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

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

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

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

229214

230215private

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

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

278263 = let env' = unlabel env in

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

280265

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+

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

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

283284

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

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

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

289290

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

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

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

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

292293

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

294295runWith 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) ->

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

184184(>>=) = ebind

185185

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−

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

202187return x = value x

203188

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

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

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

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

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

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

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

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

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

227213

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

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

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

260246 [default, default, default, default, default, default, default],

261247 [default, default, default, default, default, default, default, default] |)

262248

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+

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

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

265267

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

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

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

1717

1818b8ToString : Bits8 -> String

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

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

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

2121 toFin16 : Bits8 -> Fin 16

2222 toFin16 n = if n == 0

src/Idris/AbsSyntax.hs+1

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

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

951951 en (PHidden t) = PHidden (en t)

952952 en (PUnifyLog t) = PUnifyLog (en t)

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

953954 en (PNoImplicits t) = PNoImplicits (en t)

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

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

src/Idris/Core/Elaborate.hs+4

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

182182get_env = do ES p _ _ <- get

183183 lift $ envAtFocus (fst p)

184184

185+get_inj :: Elab' aux [Name]

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

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

188+

185189get_holes :: Elab' aux [Name]

186190get_holes = do ES p _ _ <- get

187191 return $! (holes (fst p))

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

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

154154match_unify' ctxt env topx topy =

155155 do ps <- get

156156 let dont = dontunify ps

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

157+ let inj = injective ps

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

158159 let (h, ns) = unified ps

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

160161 return u

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

164165unify' ctxt env topx topy =

165166 do ps <- get

166167 let dont = dontunify ps

168+ let inj = injective ps

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

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

169171 " in " ++ show env ++

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

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

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

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

174+ ++ "\n") $

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

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

173177 P _ _ _ -> False

174178 _ -> n `elem` dont) u

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

187191 (holes ps)

188192 put (ps { problems = probs',

189193 unified = (h, ns'),

194+ injective = updateInj u (injective ps),

190195 notunified = notu ++ notunified ps })

191196 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

192204

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

194206getName tag = do ps <- get

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

358370 return (Bind x (Hole t) sc)

359371

360372setinj :: Name -> RunTactic

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

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

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

363375 ps { injective = n : is })

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

376+ return (Bind x b sc)

365377

366378defer :: Name -> RunTactic

367379defer 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"

526538

527539patvar :: Name -> RunTactic

528540patvar 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) })

530543 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

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

532547

533548letbind :: Name -> Raw -> Raw -> RunTactic

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

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

3333

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

3535 TC [(Name, TT Name)]

36−match_unify ctxt env topx topy dont holes =

36+match_unify ctxt env topx topy inj holes =

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

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

3939 res ->

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

169169

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

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

172−unify ctxt env topx topy dont holes =

172+unify ctxt env topx topy inj holes =

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

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

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

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

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

199199 injective _ = False

200200

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+

201208 notP (P _ _ _) = False

202209 notP _ = True

203210

204211 sc i = do UI s f <- get

205212 put (UI (s+i) f)

206213

214+ errors :: StateT UInfo TC Bool

207215 errors = do UI s f <- get

208216 return (not (null f))

209217

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

302310 -- class resolution for type classes over functions.

303311

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

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

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

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

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

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

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

324+ combine bnames ux uf

308325

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

310327 = do h1 <- uB bnames bx by

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

321338 return [] -- lift $ tfail err

322339

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

324− | (injective fx && injective fy)

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

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

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

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

341+ | (injectiveApp fx && injectiveApp fy)

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

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

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

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

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

330347 let (heady, _) = unApply fy

331348 -- fail quickly if the heads are disjoint

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

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

348365 sc 1

349366 combine bnames hf ha)

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

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

352− let (heady, argsy) = unApply appy

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

354− uplus (

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

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

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

358− then

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

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

361− failed <- errors

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

363− else return []

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

365− unifyTmpFail appx appy)

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

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

368+ unifyTmpFail appx appy

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

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

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

372+-- uplus (

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

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

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

376+-- then

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

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

379+-- failed <- errors

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

381+-- else return []

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

383+-- unifyTmpFail appx appy)

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

367385 where hnormalise [] _ _ t = t

368386 hnormalise ns ctxt env t = normalise ctxt env t

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

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

433451 _ -> False

434452

435453 metavar t = case t of

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

437− not (x `elem` dont))

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

438455 || globmetavar t

439456 _ -> False

440457 pat t = case t of

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

447464 notFn t = injective t || metavar t || inenv t

448465

449466

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

450468 unifyTmpFail x y

451469 = do UI s f <- get

452470 let r = recoverable x y

src/Idris/ElabDecls.hs+23−9

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

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

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

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

699− (do pbinds lhs_tm

699+ (do pbinds i lhs_tm

700700 setNextName

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

702702 erun fc $ psolve lhs_tm

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

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

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

12981298

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

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

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

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

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

13031303 probs <- get_probs

1304− return (res, probs))

1304+ inj <- get_inj

1305+ return (res, probs, inj))

13051306

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

13071308

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

13091310 let lhs_ty = getInferType lhs'

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

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

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

13121314

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

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

13511353 logLvl 5 "STARTING CHECK"

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

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

1354− (do pbinds lhs_tm

1356+ (do pbinds ist lhs_tm

1357+ mapM_ setinj inj

13551358 setNextName

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

13571360 (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)

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

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

15251528 (bindTyArgs PVTy bargs infP) []

1526− (do pbinds lhs_tm

1529+ (do pbinds i lhs_tm

15271530 setNextName

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

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

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

15871590 i <- getIState

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

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

1590− (do pbinds lhs_tm

1593+ (do pbinds i lhs_tm

15911594 setNextName

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

15931596 psolve lhs_tm

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

20582061 dappname t = t

20592062

20602063

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

2062− pbinds sc

2063−pbinds tm = return ()

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

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

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

2074+ pbinds i sc

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

2076+ setinjArg _ = return ()

2077+pbinds i tm = return ()

20642078

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

20662080pbty _ tm = tm

src/Idris/ElabTerm.hs+23−5

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

125125 end_unify

126126 when pattern -- convert remaining holes to pattern vars

127127 (do update_term orderPats

128+ matchProblems; unifyProblems

128129 mkPat)

129130 where

130131 tcgen = Dictionary `elem` opts

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

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

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

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

457+ -- mark any type class arguments as injective

458+ mapM_ checkIfInjective (map snd ns)

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

457460 let (ns', eargs) = unzip $

458461 sortBy cmpArg (zip ns args)

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

475478 (movelast n)

476479 else movelast n)

477480 (ivs' \\ ivs)

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

479− tcArg _ = False

480−

481− -- normal < tactic < default tactic

481+ where -- normal < tactic < default tactic

482482 cmpArg (_, x) (_, y)

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

484484 where alt t = case getTm t of

485485 PAlternative False _ -> 5

486486 _ -> 0

487487

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+

488504 tacTm (PTactics _) = True

489505 tacTm (PProof _) = True

490506 tacTm _ = False

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

918934runTac autoSolve ist tac

919935 = do env <- get_env

920936 g <- goal

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

937+ if autoSolve

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

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

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

923941 where

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

src/Idris/ErrReverse.hs+1−1

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

1313-- errors will be more readable

1414

1515errReverse :: IState -> Term -> Term

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

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

1717 where

1818

1919 rewrite 0 t = t

test/reg025/reg025.idr+2−2

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

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

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

2929find _ Nil = Left Nil

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

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

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

3232 | No prf =

33− case find d xs of

33+ case find {P} d xs of

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

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

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

test/reg026/reg026.idr+3−3

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

99data Action = Left | Ahead | Right

1010

1111admissible : X t -> Action -> Bool

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

13−admissible x Left = column x <= 2

14−admissible x Right = column x >= 2

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

13+admissible {t} x Left = column {t} 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

1616 pure v = \x => v

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

1818

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

19+instance Monad IntFn where

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

2121

2222dbl : IntFn Int