c931eff · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -616,6 +616,9 @@ Extra-source-files:

616 test/proofsearch002/run

617 test/proofsearch002/*.idr

618 test/proofsearch002/expected

619+ test/proofsearch003/run

620+ test/proofsearch003/*.idr

621+ test/proofsearch003/expected

619

622

620 test/quasiquote001/run

623 test/quasiquote001/run

621 test/quasiquote001/*.idr

624 test/quasiquote001/*.idr

src/Idris/Core/Elaborate.hs+1−1

@@ -309,7 +309,7 @@ get_instances = do ES p _ _ <- get

309 return $! (instances (fst p))

310

311-- | get auto argument names

312−get_autos :: Elab' aux [(Name, [Name])]

312+get_autos :: Elab' aux [(Name, ([FailContext], [Name]))]

313get_autos = do ES p _ _ <- get

314 return $! (autos (fst p))

315

src/Idris/Core/ProofState.hs+2−2

@@ -38,7 +38,7 @@ data ProofState = PS { thname :: Name,

38 injective :: [Name],

39 deferred :: [Name], -- ^ names we'll need to define

40 instances :: [Name], -- ^ instance arguments (for type classes)

41− autos :: [(Name, [Name])], -- ^ unsolved 'auto' implicits with their holes

41+ autos :: [(Name, ([FailContext], [Name]))], -- ^ unsolved 'auto' implicits with their holes

42 psnames :: [Name], -- ^ Local names okay to use in proof search

43 previous :: Maybe ProofState, -- ^ for undo

44 context :: Context,

@@ -415,7 +415,7 @@ autoArg n ctxt env (Bind x (Hole t) sc)

415 Nothing ->

416 let hs = holes ps in

417 ps { holes = (hs \\ [x]) ++ [x],

418− autos = (x, refsIn t) : autos ps }

418+ autos = (x, (while_elaborating ps, refsIn t)) : autos ps }

419 Just _ -> ps)

420 return (Bind x (Hole t) sc)

421

src/Idris/Core/TT.hs+15

@@ -376,6 +376,21 @@ instance Show Err where

376 show x ++ ": " ++ show e

377 show (Elaborating what n e) = "Elaborating " ++ what ++ show n ++ ":" ++ show e

378 show (ProofSearchFail e) = "Proof search fail: " ++ show e

379+ show (InfiniteUnify _ _ _) = "InfiniteUnify"

380+ show (UnifyScope _ _ _ _) = "UnifyScope"

381+ show (NonFunctionType _ _) = "NonFunctionType"

382+ show (NotEquality _ _) = "NotEquality"

383+ show (TooManyArguments _) = "TooManyArguments"

384+ show (CantIntroduce _) = "CantIntroduce"

385+ show (NoSuchVariable _) = "NoSuchVariable"

386+ show (WithFnType _) = "WithFnType"

387+ show (NoTypeDecl _) = "NoTypeDecl"

388+ show (NotInjective _ _ _) = "NotInjective"

389+ show (CantResolve _ _) = "CantResolve"

390+ show (InvalidTCArg _ _) = "InvalidTCArg"

391+ show (CantResolveAlts _) = "CantResolveAlts"

392+ show (NoValidAlts _) = "NoValidAlts"

393+ show (IncompleteTerm _) = "IncompleteTerm"

379 show _ = "Error"

394 show _ = "Error"

380

395

381instance Pretty Err OutputAnnotation where

396instance Pretty Err OutputAnnotation where

src/Idris/Core/Unify.hs+2−1

@@ -412,7 +412,8 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

412 = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $

413 checkCycle bnames (mv, eta [] $ bindLams args (substEnv env tm))

414 where rigid (V i) = True

415+ rigid (P _ t _) = t `elem` map fst env &&

415− rigid (P _ t _) = not (holeIn env t || t `elem` holes)

416+ not (holeIn env t || t `elem` holes)

416 rigid _ = False

417 rigid _ = False

417

418

418 getV (V i) = Just i

419 getV (V i) = Just i

src/Idris/Delaborate.hs+5−2

@@ -355,8 +355,11 @@ pprintErr' i (WithFnType ty) =

355pprintErr' i (CantMatch t) =

356 text "Can't match on" <+> annTm t (pprintTerm i (delabSugared i t))

357pprintErr' i (IncompleteTerm t)

358+ = let missing = getMissing [] [] t in

359+ case missing of

360+ [] -> text "Incomplete term" <+> annTm t (pprintTerm i (delabSugared i t))

358− = align (cat (punctuate (comma <> space)

361+ _ -> align (cat (punctuate (comma <> space)

359− (map pprintIncomplete (nub $ getMissing [] [] t))))

362+ (map pprintIncomplete (nub $ getMissing [] [] t))))

360 where

363 where

361 pprintIncomplete (tm, arg)

364 pprintIncomplete (tm, arg)

362 | expname arg

365 | expname arg

src/Idris/Elab/Term.hs+34−15

@@ -91,7 +91,7 @@ build ist info emode opts fn tm

91 ptm <- get_term

92 resolveTC' True True 10 g fn ist) ivs

93

94− when (not pattern) $ solveAutos ist fn True

94+ when (not pattern) $ solveAutos ist fn False

95

96 tm <- get_term

97 ctxt <- get_context

@@ -104,6 +104,8 @@ build ist info emode opts fn tm

104 "Remaining problems:\n" ++ qshow probs) $

105 do unify_all; matchProblems True; unifyProblems

106

107+ when (not pattern) $ solveAutos ist fn True

108+

107 probs <- get_probs

109 probs <- get_probs

108 case probs of

110 case probs of

109 [] -> return ()

111 [] -> return ()

@@ -269,8 +271,9 @@ elab ist info emode opts fn tm

269 hs <- get_holes

271 hs <- get_holes

270 -- If any of the autos use variables which have recently been solved,

272 -- If any of the autos use variables which have recently been solved,

271 -- have another go at solving them now.

273 -- have another go at solving them now.

274+ mapM_ (\(a, (failc, ns)) ->

272− mapM_ (\(a, ns) -> if any (\n -> n `elem` solved) ns && head hs /= a

275+ if any (\n -> n `elem` solved) ns && head hs /= a

273− then solveAuto ist fn False a

276+ then solveAuto ist fn False (a, failc)

274 else return ()) as

277 else return ()) as

275

278

276 itm <- if not pattern then insertImpLam ina t else return t

279 itm <- if not pattern then insertImpLam ina t else return t

@@ -452,7 +455,7 @@ elab ist info emode opts fn tm

452 (do movelast h

455 (do movelast h

453 delayElab 5 $ do

456 delayElab 5 $ do

454 hs <- get_holes

457 hs <- get_holes

455− when (not (null hs)) $ do

458+ when (h `elem` hs) $ do

456 focus h

459 focus h

457 as'' <- doPrune as'

460 as'' <- doPrune as'

458 case as'' of

461 case as'' of

@@ -1620,21 +1623,36 @@ findHighlight n = do ctxt <- get_context

1620 "Can't find name" ++ show n

1623 "Can't find name" ++ show n

1621

1624

1622-- Try again to solve auto implicits

1625-- Try again to solve auto implicits

1623−solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

1626+solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()

1624−solveAuto ist fn ambigok n

1627+solveAuto ist fn ambigok (n, failc)

1625− = do hs <- get_holes

1628+ = do hs <- get_holes

1626− tm <- get_term

1629+ when (not (null hs)) $ do

1630+ env <- get_env

1631+ g <- goal

1627− when (n `elem` hs) $ do

1632+ handleError cantsolve (when (n `elem` hs) $ do

1628− focus n

1633+ focus n

1629− g <- goal

1630− isg <- is_guess -- if it's a guess, we're working on it recursively, so stop

1634+ isg <- is_guess -- if it's a guess, we're working on it recursively, so stop

1631− when (not isg) $

1635+ when (not isg) $

1632− proofSearch' ist True ambigok 100 True Nothing fn [] []

1636+ proofSearch' ist True ambigok 100 True Nothing fn [] [])

1637+ (lift $ Error (addLoc failc

1638+ (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))))

1639+ return ()

1640+ where addLoc (FailContext fc f x : prev) err

1641+ = At fc (ElaboratingArg f x

1642+ (map (\(FailContext _ f' x') -> (f', x')) prev) err)

1643+ addLoc _ err = err

1644+

1645+ cantsolve (CantSolveGoal _ _) = True

1646+ cantsolve (InternalMsg _) = True

1647+ cantsolve (At _ e) = cantsolve e

1648+ cantsolve (Elaborating _ _ e) = cantsolve e

1649+ cantsolve (ElaboratingArg _ _ _ e) = cantsolve e

1650+ cantsolve _ = False

1633

1651

1634solveAutos :: IState -> Name -> Bool -> ElabD ()

1652solveAutos :: IState -> Name -> Bool -> ElabD ()

1635solveAutos ist fn ambigok

1653solveAutos ist fn ambigok

1636 = do autos <- get_autos

1654 = do autos <- get_autos

1637− mapM_ (solveAuto ist fn ambigok) (map fst autos)

1655+ mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)

1638

1656

1639trivial' ist

1657trivial' ist

1640 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1658 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

@@ -2337,6 +2355,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2337 -- TODO: argument-specific error handlers go here for ElaboratingArg

2355 -- TODO: argument-specific error handlers go here for ElaboratingArg

2338 handle e = do ist <- getIState

2356 handle e = do ist <- getIState

2339 logLvl 2 "Starting error reflection"

2357 logLvl 2 "Starting error reflection"

2358+ logLvl 5 (show e)

2340 let handlers = idris_errorhandlers ist

2359 let handlers = idris_errorhandlers ist

2341 applyHandlers e handlers

2360 applyHandlers e handlers

2342 getFnHandlers :: Name -> Name -> Idris [Name]

2361 getFnHandlers :: Name -> Name -> Idris [Name]

src/Idris/ProofSearch.hs+14−3

@@ -165,12 +165,23 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

165 if ambigok || argsok then

166 case lookupCtxt nroot (idris_tyinfodata ist) of

167 [TISolution ts] -> findInferredTy ts

168− _ -> psRec rec maxDepth [] S.empty

168+ _ -> if ambigok then psRec rec maxDepth [] S.empty

169− else do ptm <- get_term

169+ -- postpone if it fails early in elaboration

170+ else handleError cantsolve

171+ (psRec rec maxDepth [] S.empty)

172+ (autoArg (sUN "auto"))

170− autoArg (sUN "auto") -- not enough info in the type yet

173+ else autoArg (sUN "auto") -- not enough info in the type yet

171 where

174 where

172 findInferredTy (t : _) = elab (delab ist (toUN t))

175 findInferredTy (t : _) = elab (delab ist (toUN t))

173

176

177+ cantsolve (InternalMsg _) = True

178+ cantsolve (CantSolveGoal _ _) = True

179+ cantsolve (IncompleteTerm _) = True

180+ cantsolve (At _ e) = cantsolve e

181+ cantsolve (Elaborating _ _ e) = cantsolve e

182+ cantsolve (ElaboratingArg _ _ _ e) = cantsolve e

183+ cantsolve err = False

184+

174 conArgsOK ty

185 conArgsOK ty

175 = let (f, as) = unApply ty in

186 = let (f, as) = unApply ty in

176 case f of

187 case f of

test/error004/expected+4−4

@@ -1,6 +1,6 @@

1−FunErrTest.idr:35:10:When checking right hand side of badCadr1:

1+FunErrTest.idr:35:17:When checking right hand side of badCadr1:

2−When checking argument cons1 to function FunErrTest.cadr:

2+When checking argument cons2 to function FunErrTest.cadr:

3 Could not prove that [] has at least two elements.

4−FunErrTest.idr:38:10:When checking right hand side of badCadr2:

4+FunErrTest.idr:38:17:When checking right hand side of badCadr2:

5When checking argument cons2 to function FunErrTest.cadr:

6− Could not prove that tail [1] has at least two elements.

6+ Could not prove that [] has at least two elements.

test/proofsearch003/expectednew file

No changes to the content.

test/proofsearch003/proofsearch003.idrnew file+34

@@ -0,0 +1,34 @@

1+import Data.Fin

2+

3+data Wrapper = Wrap (Fin 9)

4+

5+data Seq : Fin 9 -> Fin 9 -> Type where

6+ Seq12 : {n : Fin 8} -> Seq (weaken n) (FS n)

7+ Seq21 : {n : Fin 8} -> Seq (FS n) (weaken n)

8+

9+class Evil t where

10+ value : t -> Fin 9

11+

12+instance Evil Wrapper where

13+ value (Wrap n) = n

14+

15+consTest : (Evil t) => (a : t) -> (b : t) ->

16+ {auto p : Seq (value a) (value b)} -> Bool

17+consTest _ _ = True

18+

19+-- Fails!

20+test1 : Bool

21+test1 = consTest (Wrap 3) (Wrap 4) -- {p = ?foo}

22+

23+-- Succeeds!

24+test2 : Bool

25+test2 = consTest (Wrap 3) (Wrap 4) {p = Seq12}

26+

27+-- Succeeds!

28+test3 : Bool

29+test3 = consTest (Wrap 3) (Wrap 4) {p = (| Seq12, Seq21 |)}

30+

31+-- Fails!

32+-- test4 : Bool

33+-- test4 = consTest (Wrap 3) (Wrap 4) {p = (| Seq21, Seq12 |)}

34+

test/proofsearch003/runnew file+3

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

1+#!/usr/bin/env bash

2+idris --check proofsearch003.idr

3+rm -f *.ibc