b0a0c0c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Improvement for 'auto'

Now proof search can be deferred if there are too many metavariables in the goal - previously in this case it would happily pick any old solution causing weird errors elsewhere in some cases.

commitb0a0c0cb2f8a56e4d73263b885a7ef026a6e3214 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 4 Dec 2014, 01:04 (12 years ago) parentda237ae

8 files changed+159−48

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+30−6 src/Idris/Core/ProofState.hs+30−8 src/Idris/Core/ProofTerm.hs+2−2 src/Idris/Core/TT.hs+11−10 src/Idris/Elab/Utils.hs+5−5 src/Idris/ElabTerm.hs+35−6 src/Idris/ProofSearch.hs+44−9 src/Idris/Prover.hs+2−2

src/Idris/Core/Elaborate.hs+30−6

@@ -213,12 +213,26 @@ get_probs :: Elab' aux Fails

213213get_probs = do ES p _ _ <- get

214214 return $! (problems (fst p))

215215

216+-- Return recently solved names (that is, the names solved since the

217+-- last call to get_recents)

218+get_recents :: Elab' aux [Name]

219+get_recents = do ES (p, a) l prev <- get

220+ put (ES (p { recents = [] }, a) l prev)

221+ return (recents p)

222+

216223-- get the current goal type

217224goal :: Elab' aux Type

218225goal = do ES p _ _ <- get

219226 b <- lift $ goalAtFocus (fst p)

220227 return $! (binderTy b)

221228

229+is_guess :: Elab' aux Bool

230+is_guess = do ES p _ _ <- get

231+ b <- lift $ goalAtFocus (fst p)

232+ case b of

233+ Guess _ _ -> return True

234+ _ -> return False

235+

222236-- Get the guess at the current hole, if there is one

223237get_guess :: Elab' aux Type

224238get_guess = do ES p _ _ <- get

@@ -262,6 +276,11 @@ get_instances :: Elab' aux [Name]

262276get_instances = do ES p _ _ <- get

263277 return $! (instances (fst p))

264278

279+-- get auto argument names

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

281+get_autos = do ES p _ _ <- get

282+ return $! (autos (fst p))

283+

265284-- given a desired hole name, return a unique hole name

266285unique_hole = unique_hole' False

267286

@@ -416,6 +435,9 @@ deferType n ty ns = processTactic' (DeferType n ty ns)

416435instanceArg :: Name -> Elab' aux ()

417436instanceArg n = processTactic' (Instance n)

418437

438+autoArg :: Name -> Elab' aux ()

439+autoArg n = processTactic' (AutoArg n)

440+

419441setinj :: Name -> Elab' aux ()

420442setinj n = processTactic' (SetInjective n)

421443

@@ -712,6 +734,7 @@ try' t1 t2 proofSearch

712734 = -- traceWhen r (show err) $

713735 r || proofSearch

714736 recoverableErr (CantSolveGoal _ _) = False

737+ recoverableErr (CantResolveAlts _) = False

715738 recoverableErr (ProofSearchFail (Msg _)) = True

716739 recoverableErr (ProofSearchFail _) = False

717740 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

@@ -722,9 +745,10 @@ tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

722745tryWhen True a b = try a b

723746tryWhen False a b = a

724747

725−

726−-- Try a selection of tactics. Exactly one must work, all others must fail

748+-- Bool says whether it's okay to create new unification problems. If set

749+-- to False, then the whole tactic fails if there are any new problems

727750tryAll :: [(Elab' aux a, Name)] -> Elab' aux a

751+tryAll [(x, _)] = x

728752tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

729753 where

730754 cantResolve :: Elab' aux a

@@ -743,10 +767,10 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

743767 ps <- get_probs

744768 case prunStateT pmax True ps x s of

745769 OK ((v, newps, probs), s') ->

746− do let cs' = if (newps < pmax)

747− then [do put s'; return $! v]

748− else (do put s'; return $! v) : cs

749− tryAll' cs' newps f xs

770+ do let cs' = if (newps < pmax)

771+ then [do put s'; return $! v]

772+ else (do put s'; return $! v) : cs

773+ tryAll' cs' newps f xs

750774 Error err -> do put s

751775-- if (score err) < 100

752776 tryAll' cs pmax (better err f) xs

src/Idris/Core/ProofState.hs+30−8

@@ -36,11 +36,13 @@ data ProofState = PS { thname :: Name,

3636 injective :: [Name],

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

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

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

3940 previous :: Maybe ProofState, -- for undo

4041 context :: Context,

4142 plog :: String,

4243 unifylog :: Bool,

4344 done :: Bool,

45+ recents :: [Name],

4446 while_elaborating :: [FailContext]

4547 }

4648

@@ -78,6 +80,7 @@ data Tactic = Attack

7880 | Defer [Name] Name

7981 | DeferType Name Raw [Name]

8082 | Instance Name

83+ | AutoArg Name

8184 | SetInjective Name

8285 | MoveLast Name

8386 | MatchProblems Bool

@@ -90,9 +93,9 @@ data Tactic = Attack

9093-- Some utilites on proof and tactic states

9194

9295instance Show ProofState where

93− show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)

96+ show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)

9497 = show nm ++ ": no more goals"

95− show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _ _)

98+ show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ _ ctxt _ _ _ _ _)

9699 = let OK g = goal (Just h) tm

97100 wkenv = premises g in

98101 "Other goals: " ++ show hs ++ "\n" ++

@@ -115,9 +118,9 @@ instance Show ProofState where

115118 showG ps b = showEnv ps (binderTy b)

116119

117120instance Pretty ProofState OutputAnnotation where

118− pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

121+ pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

119122 pretty nm <+> colon <+> text " no more goals."

120− pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _ _) =

123+ pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ _ ctxt _ _ _ _ _) =

121124 let OK g = goal (Just h) tm in

122125 let wkEnv = premises g in

123126 text "Other goals" <+> colon <+> pretty hs <+>

@@ -285,8 +288,8 @@ newProof n ctxt ty = let h = holeName 0

285288 PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

286289 (P Bound h ty'))) ty [] (h, []) []

287290 Nothing [] []

288− [] []

289− Nothing ctxt "" False False []

291+ [] [] []

292+ Nothing ctxt "" False False [] []

290293

291294type TState = ProofState -- [TacticAction])

292295type RunTactic = RunTactic' TState

@@ -381,6 +384,16 @@ instanceArg n ctxt env (Bind x (Hole t) sc)

381384 instances = x:is })

382385 return (Bind x (Hole t) sc)

383386

387+autoArg :: Name -> RunTactic

388+autoArg n ctxt env (Bind x (Hole t) sc)

389+ = do action (\ps -> case lookup x (autos ps) of

390+ Nothing ->

391+ let hs = holes ps in

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

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

394+ Just _ -> ps)

395+ return (Bind x (Hole t) sc)

396+

384397setinj :: Name -> RunTactic

385398setinj n ctxt env (Bind x b sc)

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

@@ -494,6 +507,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

494507 solved = Just (x, val),

495508 notunified = updateNotunified [(x,val)]

496509 (notunified ps),

510+ recents = x : recents ps,

497511 instances = instances ps \\ [x] })

498512 let tm' = subst x val sc in

499513 return tm'

@@ -647,7 +661,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

647661 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)

648662 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))

649663 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

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

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

665+ recents = x : recents ps })

651666 mapM_ addConsHole (reverse consargs')

652667 let res' = forget $ res

653668 (scv, sct) <- lift $ check ctxt env res'

@@ -739,7 +754,8 @@ solve_unified ctxt env tm =

739754 let (_, ns) = unified ps

740755 let unify = dropGiven (dontunify ps) ns (holes ps)

741756 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $

742− holes ps \\ map fst unify })

757+ holes ps \\ map fst unify,

758+ recents = recents ps ++ map fst unify })

743759 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })

744760 return (updateSolvedTerm unify tm)

745761

@@ -858,11 +874,13 @@ processTactic EndUnify ps

858874 unified = (h, []),

859875 problems = probs',

860876 notunified = updateNotunified ns'' (notunified ps),

877+ recents = recents ps ++ map fst ns'',

861878 holes = holes ps \\ map fst ns'' }, "")

862879processTactic UnifyAll ps

863880 = let tm' = updateSolved (notunified ps) (pterm ps) in

864881 return (ps { pterm = tm',

865882 notunified = [],

883+ recents = recents ps ++ map fst (notunified ps),

866884 holes = holes ps \\ map fst (notunified ps) }, "")

867885processTactic (Reorder n) ps

868886 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

@@ -882,6 +900,7 @@ processTactic UnifyProblems ps

882900 return (ps { pterm = pterm', solved = Nothing, problems = probs',

883901 previous = Just ps, plog = "",

884902 notunified = updateNotunified ns' (notunified ps),

903+ recents = recents ps ++ map fst ns',

885904 holes = holes ps \\ (map fst ns') }, plog ps)

886905processTactic (MatchProblems all) ps

887906 = let (ns', probs') = matchProblems all [] (context ps)

@@ -897,6 +916,7 @@ processTactic (MatchProblems all) ps

897916 return (ps { pterm = pterm', solved = Nothing, problems = probs'',

898917 previous = Just ps, plog = "",

899918 notunified = updateNotunified ns'' (notunified ps),

919+ recents = recents ps ++ map fst ns'',

900920 holes = holes ps \\ (map fst ns'') }, plog ps)

901921processTactic t ps

902922 = case holes ps of

@@ -921,6 +941,7 @@ processTactic t ps

921941 problems = probs',

922942 notunified = updateNotunified ns' (notunified ps'),

923943 previous = Just ps, plog = "",

944+ recents = recents ps' ++ map fst ns',

924945 holes = holes ps' \\ (map fst ns')}, plog ps')

925946

926947process :: Tactic -> Name -> StateT TState TC ()

@@ -959,5 +980,6 @@ process t h = tactic (Just h) (mktac t)

959980 mktac (Defer ns n) = defer ns n

960981 mktac (DeferType n t a) = deferType n t a

961982 mktac (Instance n) = instanceArg n

983+ mktac (AutoArg n) = autoArg n

962984 mktac (SetInjective n) = setinj n

963985 mktac (MoveLast n) = movelast n

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

@@ -180,8 +180,8 @@ updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns e

180180

181181updateSolvedPath [] t = t

182182updateSolvedPath ns Top = Top

183−updateSolvedPath ns (AppL p r) = AppL p (updateSolvedTerm ns r)

184−updateSolvedPath ns (AppR l p) = AppR (updateSolvedTerm ns l) p

183+updateSolvedPath ns (AppL p r) = AppL (updateSolvedPath ns p) (updateSolvedTerm ns r)

184+updateSolvedPath ns (AppR l p) = AppR (updateSolvedTerm ns l) (updateSolvedPath ns p)

185185updateSolvedPath ns (InBind n b sc)

186186 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)

187187 where

src/Idris/Core/TT.hs+11−10

@@ -1360,24 +1360,25 @@ orderPats tm = op [] tm

13601360

13611361 sortP ps = pick [] (reverse ps)

13621362

1363− namesIn (P _ n _) = [n]

1364− namesIn (Bind n b t) = nub $ nb b ++ (namesIn t \\ [n])

1365− where nb (Let t v) = nub (namesIn t) ++ nub (namesIn v)

1366− nb (Guess t v) = nub (namesIn t) ++ nub (namesIn v)

1367− nb t = namesIn (binderTy t)

1368− namesIn (App f a) = nub (namesIn f ++ namesIn a)

1369− namesIn _ = []

1370−

13711363 pick acc [] = reverse acc

13721364 pick acc ((n, t) : ps) = pick (insert n t acc) ps

13731365

13741366 insert n t [] = [(n, t)]

13751367 insert n t ((n',t') : ps)

1376− | n `elem` (namesIn (binderTy t') ++

1377− concatMap namesIn (map (binderTy . snd) ps))

1368+ | n `elem` (refsIn (binderTy t') ++

1369+ concatMap refsIn (map (binderTy . snd) ps))

13781370 = (n', t') : insert n t ps

13791371 | otherwise = (n,t):(n',t'):ps

13801372

1373+refsIn :: TT Name -> [Name]

1374+refsIn (P _ n _) = [n]

1375+refsIn (Bind n b t) = nub $ nb b ++ (refsIn t \\ [n])

1376+ where nb (Let t v) = nub (refsIn t) ++ nub (refsIn v)

1377+ nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)

1378+ nb t = refsIn (binderTy t)

1379+refsIn (App f a) = nub (refsIn f ++ refsIn a)

1380+refsIn _ = []

1381+

13811382-- Make sure all the pattern bindings are as far out as possible

13821383liftPats :: Term -> Term

13831384liftPats tm = let (tm', ps) = runState (getPats tm) [] in

src/Idris/Elab/Utils.hs+5−5

@@ -229,11 +229,11 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

229229

230230 use n = do ns <- get; put (n : ns)

231231

232− getUniqB env us (Let t v) = do getUniq env us t; getUniq env us v

233− getUniqB env us (Guess t v) = do getUniq env us t; getUniq env us v

234− getUniqB env us (Pi t v) = do getUniq env us t; getUniq env us v

235− getUniqB env us (NLet t v) = do getUniq env us t; getUniq env us v

236− getUniqB env us b = getUniq env us (binderTy b)

232+ getUniqB env us (Let t v) = getUniq env us v

233+ getUniqB env us (Guess t v) = getUniq env us v

234+-- getUniqB env us (Pi t v) = do getUniq env us t; getUniq env us v

235+ getUniqB env us (NLet t v) = getUniq env us v

236+ getUniqB env us b = return () -- getUniq env us (binderTy b)

237237

238238-- In a functional application, return the names which are used

239239-- directly in a static position

src/Idris/ElabTerm.hs+35−6

@@ -52,8 +52,11 @@ build ist info emode opts fn tm

5252 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

5353 [TIPartial] -> True

5454 _ -> False

55− ivs <- get_instances

55+

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

57+

5658 hs <- get_holes

59+ ivs <- get_instances

5760 ptm <- get_term

5861 -- Resolve remaining type classes. Two passes - first to get the

5962 -- default Num instances, second to clean up the rest

@@ -187,12 +190,21 @@ elab ist info emode opts fn tm

187190 elabE ina fc' t =

188191 --do g <- goal

189192 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $

190− do ct <- insertCoerce ina t

193+ do solved <- get_recents

194+ as <- get_autos

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

196+ -- have another go at solving them now.

197+ mapM_ (\(a, ns) -> if any (\n -> n `elem` solved) ns

198+ then solveAuto ist fn False a

199+ else return ()) as

200+

201+ ct <- insertCoerce ina t

191202 t' <- insertLazy ct

192203 g <- goal

193204 tm <- get_term

194205 ps <- get_probs

195206 hs <- get_holes

207+

196208 --trace ("Elaborating " ++ show t' ++ " in " ++ show g

197209 -- ++ "\n" ++ show tm

198210 -- ++ "\nholes " ++ show hs

@@ -967,7 +979,8 @@ elab ist info emode opts fn tm

967979 elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)

968980 = elabArg argName holeName t

969981 where elabArg argName holeName t =

970− do now_elaborating fc f argName

982+ do -- solveAutos ist fn False

983+ now_elaborating fc f argName

971984 wrapErr f argName $ do

972985 hs <- get_holes

973986 tm <- get_term

@@ -1077,11 +1090,27 @@ findInstances ist t

10771090 _ -> []

10781091 | otherwise = []

10791092

1093+-- Try again to solve auto implicits

1094+solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

1095+solveAuto ist fn ambigok n

1096+ = do hs <- get_holes

1097+ when (n `elem` hs) $ do

1098+ focus n

1099+ g <- goal

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

1101+ when (not isg) $

1102+ proofSearch' ist True ambigok 100 True Nothing fn []

1103+

1104+solveAutos :: IState -> Name -> Bool -> ElabD ()

1105+solveAutos ist fn ambigok

1106+ = do autos <- get_autos

1107+ mapM_ (solveAuto ist fn ambigok) (map fst autos)

1108+

10801109trivial' ist

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

1082−proofSearch' ist rec depth prv top n hints

1111+proofSearch' ist rec ambigok depth prv top n hints

10831112 = do unifyProblems

1084− proofSearch rec prv depth

1113+ proofSearch rec prv ambigok (not prv) depth

10851114 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist

10861115

10871116resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

@@ -1334,7 +1363,7 @@ runTac autoSolve ist perhapsFC fn tac

13341363 runT Trivial = do trivial' ist; when autoSolve solveAll

13351364 runT TCInstance = runT (Exact (PResolveTC emptyFC))

13361365 runT (ProofSearch rec prover depth top hints)

1337− = do proofSearch' ist rec depth prover top fn hints

1366+ = do proofSearch' ist rec False depth prover top fn hints

13381367 when autoSolve solveAll

13391368 runT (Focus n) = focus n

13401369 runT Solve = solve

src/Idris/ProofSearch.hs+44−9

@@ -38,20 +38,22 @@ trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)

3838 (tryAll xs) True

3939 else tryAll xs

4040

41−cantSolveGoal :: ElabD ()

41+cantSolveGoal :: ElabD a

4242cantSolveGoal = do g <- goal

4343 env <- get_env

4444 lift $ tfail $

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

4646

47−proofSearch :: Bool ->

47+proofSearch :: Bool -> -- recursive search (False for 'refine')

4848 Bool -> -- invoked from a tactic proof. If so, making

4949 -- new metavariables is meaningless, and there shoudl

5050 -- be an error reported instead.

51+ Bool -> -- ambiguity ok

52+ Bool -> -- defer on failure

5153 Int -> -- maximum depth

5254 (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->

5355 IState -> ElabD ()

54−proofSearch False fromProver depth elab _ nroot [fn] ist

56+proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist

5557 = do -- get all possible versions of the name, take the first one that

5658 -- works

5759 let all_imps = lookupCtxtName fn (idris_implicits ist)

@@ -82,13 +84,44 @@ proofSearch False fromProver depth elab _ nroot [fn] ist

8284

8385 isImp (PImp p _ _ _ _) = (True, p)

8486 isImp arg = (True, priority arg) -- try to get all of them by unification

85−proofSearch rec fromProver maxDepth elab fn nroot hints ist

86− = case lookupCtxt nroot (idris_tyinfodata ist) of

87− [TISolution ts] -> findInferredTy ts

88− _ -> psRec rec maxDepth

87+proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

88+ = do ty <- goal

89+ argsok <- conArgsOK ty

90+ if ambigok || argsok then

91+ case lookupCtxt nroot (idris_tyinfodata ist) of

92+ [TISolution ts] -> findInferredTy ts

93+ _ -> psRec rec maxDepth

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

8995 where

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

9197

98+ conArgsOK ty

99+ = let (f, as) = unApply ty in

100+ case f of

101+ P _ n _ -> case lookupCtxt n (idris_datatypes ist) of

102+ [t] -> do rs <- mapM (conReady as) (con_names t)

103+ return (and rs)

104+ _ -> fail "Ambiguous name"

105+ TType _ -> return True

106+ _ -> fail "Not a data type"

107+

108+ conReady :: [Term] -> Name -> ElabD Bool

109+ conReady as n

110+ = case lookupTyExact n (tt_ctxt ist) of

111+ Just ty -> do let (_, cs) = unApply (getRetTy ty)

112+ -- if any metavariables in 'as' correspond to

113+ -- a constructor form in 'cs', then we're not

114+ -- ready to run auto yet. Otherwise, go for it

115+ hs <- get_holes

116+ return $ and (map (notHole hs) (zip as cs))

117+ Nothing -> fail "Can't happen"

118+

119+ notHole hs (P _ n _, c)

120+ | (P _ cn _, _) <- unApply c,

121+ n `elem` hs && isConName cn (tt_ctxt ist) = False

122+ | Constant _ <- c = not (n `elem` hs)

123+ notHole _ _ = True

124+

92125 toUN t@(P nt (MN i n) ty)

93126 | ('_':xs) <- str n = t

94127 | otherwise = P nt (UN n) ty

@@ -140,8 +173,9 @@ proofSearch rec fromProver maxDepth elab fn nroot hints ist

140173 (psRec True d) "proof search local apply"

141174

142175 -- Like type class resolution, but searching with constructors

143− tryCon d n =

144− do let imps = case lookupCtxtName n (idris_implicits ist) of

176+ tryCon d n =

177+ do ty <- goal

178+ let imps = case lookupCtxtName n (idris_implicits ist) of

145179 [] -> []

146180 [args] -> map isImp (snd args)

147181 _ -> fail "Ambiguous name"

@@ -153,6 +187,7 @@ proofSearch rec fromProver maxDepth elab fn nroot hints ist

153187 hs' <- get_holes

154188 when (length ps < length ps') $ fail "Can't apply constructor"

155189 mapM_ (\ (_, h) -> do focus h

190+ aty <- goal

156191 psRec True d)

157192 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

158193 solve

src/Idris/Prover.hs+2−2

@@ -114,10 +114,10 @@ elabStep st e = case runStateT eCheck st of

114114 ((_,_,_,e,_,_):_) -> lift $ Error e

115115

116116dumpState :: IState -> ProofState -> Idris ()

117−dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

117+dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

118118 do rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."

119119 iputGoal rendered

120−dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) = do

120+dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ _ ctxt _ _ _ _ _) = do

121121 let OK ty = goalAtFocus ps

122122 let OK env = envAtFocus ps

123123 let state = prettyOtherGoals hs <> line <>