c931eff · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Proof search improvements

Postpone failing searches rather than giving up immediately, since more information (e.g. type class constraints) may be available when trying later. Also improves error reporting of postponed searches by recording what was being elaborated at the time. Fixes #2456

commitc931eff0ba951e037a58607d3fcc009f47527043 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 6 Sep 2015, 12:41 (11 years ago) parentdbe3887

12 files changed+117−28

compare with master

unifiedsplit

idris.cabal+3 src/Idris/Core/Elaborate.hs+1−1 src/Idris/Core/ProofState.hs+2−2 src/Idris/Core/TT.hs+15 src/Idris/Core/Unify.hs+2−1 src/Idris/Delaborate.hs+5−2 src/Idris/Elab/Term.hs+34−15 src/Idris/ProofSearch.hs+14−3 test/error004/expected+4−4 test/proofsearch003/expected test/proofsearch003/proofsearch003.idr+34 test/proofsearch003/run+3

idris.cabal+3

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

616616 test/proofsearch002/run

617617 test/proofsearch002/*.idr

618618 test/proofsearch002/expected

619+ test/proofsearch003/run

620+ test/proofsearch003/*.idr

621+ test/proofsearch003/expected

619622

620623 test/quasiquote001/run

621624 test/quasiquote001/*.idr

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

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

309309 return $! (instances (fst p))

310310

311311-- | get auto argument names

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

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

313313get_autos = do ES p _ _ <- get

314314 return $! (autos (fst p))

315315

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

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

3838 injective :: [Name],

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

4040 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

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

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

4444 context :: Context,

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

415415 Nothing ->

416416 let hs = holes ps in

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

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

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

419419 Just _ -> ps)

420420 return (Bind x (Hole t) sc)

421421

src/Idris/Core/TT.hs+15

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

376376 show x ++ ": " ++ show e

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

378378 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"

379394 show _ = "Error"

380395

381396instance 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 =

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

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

414414 where rigid (V i) = True

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

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

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

416417 rigid _ = False

417418

418419 getV (V i) = Just i

src/Idris/Delaborate.hs+5−2

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

355355pprintErr' i (CantMatch t) =

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

357357pprintErr' i (IncompleteTerm t)

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

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

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

359+ case missing of

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

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

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

360363 where

361364 pprintIncomplete (tm, arg)

362365 | expname arg

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

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

9191 ptm <- get_term

9292 resolveTC' True True 10 g fn ist) ivs

9393

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

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

9595

9696 tm <- get_term

9797 ctxt <- get_context

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

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

105105 do unify_all; matchProblems True; unifyProblems

106106

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

108+

107109 probs <- get_probs

108110 case probs of

109111 [] -> return ()

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

269271 hs <- get_holes

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

271273 -- have another go at solving them now.

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

273− then solveAuto ist fn False a

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

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

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

274277 else return ()) as

275278

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

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

452455 (do movelast h

453456 delayElab 5 $ do

454457 hs <- get_holes

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

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

456459 focus h

457460 as'' <- doPrune as'

458461 case as'' of

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

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

16211624

16221625-- Try again to solve auto implicits

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

1624−solveAuto ist fn ambigok n

1625− = do hs <- get_holes

1626− tm <- get_term

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

1628− focus n

1629− g <- goal

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

1631− when (not isg) $

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

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

1627+solveAuto ist fn ambigok (n, failc)

1628+ = do hs <- get_holes

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

1630+ env <- get_env

1631+ g <- goal

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

1633+ focus n

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

1635+ when (not isg) $

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

16331651

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

16351653solveAutos ist fn ambigok

16361654 = 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)

16381656

16391657trivial' ist

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

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

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

23382356 handle e = do ist <- getIState

23392357 logLvl 2 "Starting error reflection"

2358+ logLvl 5 (show e)

23402359 let handlers = idris_errorhandlers ist

23412360 applyHandlers e handlers

23422361 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

165165 if ambigok || argsok then

166166 case lookupCtxt nroot (idris_tyinfodata ist) of

167167 [TISolution ts] -> findInferredTy ts

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

169− else do ptm <- get_term

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

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

169+ -- postpone if it fails early in elaboration

170+ else handleError cantsolve

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

172+ (autoArg (sUN "auto"))

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

171174 where

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

173176

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+

174185 conArgsOK ty

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

176187 case f of

test/error004/expected+4−4

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

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

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

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

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

33 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:

55When 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

3+data Wrapper = Wrap (Fin 9)

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)

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