b0a0c0c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improvement for 'auto'

b0a0c0cEdwin Brady12 years ago

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

compare with master

unifiedsplit

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

213get_probs = do ES p _ _ <- get

214 return $! (problems (fst p))

215

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+

216-- get the current goal type

223-- get the current goal type

217goal :: Elab' aux Type

224goal :: Elab' aux Type

218goal = do ES p _ _ <- get

225goal = do ES p _ _ <- get

219 b <- lift $ goalAtFocus (fst p)

226 b <- lift $ goalAtFocus (fst p)

220 return $! (binderTy b)

227 return $! (binderTy b)

221

228

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+

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

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

223get_guess :: Elab' aux Type

237get_guess :: Elab' aux Type

224get_guess = do ES p _ _ <- get

238get_guess = do ES p _ _ <- get

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

262get_instances = do ES p _ _ <- get

276get_instances = do ES p _ _ <- get

263 return $! (instances (fst p))

277 return $! (instances (fst p))

264

278

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+

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

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

266unique_hole = unique_hole' False

285unique_hole = unique_hole' False

267

286

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

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

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

417instanceArg n = processTactic' (Instance n)

436instanceArg n = processTactic' (Instance n)

418

437

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

439+autoArg n = processTactic' (AutoArg n)

440+

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

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

420setinj n = processTactic' (SetInjective n)

442setinj n = processTactic' (SetInjective n)

421

443

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

712 = -- traceWhen r (show err) $

734 = -- traceWhen r (show err) $

713 r || proofSearch

735 r || proofSearch

714 recoverableErr (CantSolveGoal _ _) = False

736 recoverableErr (CantSolveGoal _ _) = False

737+ recoverableErr (CantResolveAlts _) = False

715 recoverableErr (ProofSearchFail (Msg _)) = True

738 recoverableErr (ProofSearchFail (Msg _)) = True

716 recoverableErr (ProofSearchFail _) = False

739 recoverableErr (ProofSearchFail _) = False

717 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

740 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

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

722tryWhen True a b = try a b

745tryWhen True a b = try a b

723tryWhen False a b = a

746tryWhen False a b = a

724

747

725−

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

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

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

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

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

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

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

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

729 where

753 where

730 cantResolve :: Elab' aux a

754 cantResolve :: Elab' aux a

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

743 ps <- get_probs

767 ps <- get_probs

744 case prunStateT pmax True ps x s of

768 case prunStateT pmax True ps x s of

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

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

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

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

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

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

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

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

749− tryAll' cs' newps f xs

773+ tryAll' cs' newps f xs

750 Error err -> do put s

774 Error err -> do put s

751-- if (score err) < 100

775-- if (score err) < 100

752 tryAll' cs pmax (better err f) xs

776 tryAll' cs pmax (better err f) xs

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

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

36 injective :: [Name],

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

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

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

39 previous :: Maybe ProofState, -- for undo

40 previous :: Maybe ProofState, -- for undo

40 context :: Context,

41 context :: Context,

41 plog :: String,

42 plog :: String,

42 unifylog :: Bool,

43 unifylog :: Bool,

43 done :: Bool,

44 done :: Bool,

45+ recents :: [Name],

44 while_elaborating :: [FailContext]

46 while_elaborating :: [FailContext]

45 }

47 }

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

78 | Defer [Name] Name

80 | Defer [Name] Name

79 | DeferType Name Raw [Name]

81 | DeferType Name Raw [Name]

80 | Instance Name

82 | Instance Name

83+ | AutoArg Name

81 | SetInjective Name

84 | SetInjective Name

82 | MoveLast Name

85 | MoveLast Name

83 | MatchProblems Bool

86 | MatchProblems Bool

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

90-- Some utilites on proof and tactic states

93-- Some utilites on proof and tactic states

92instance Show ProofState where

95instance Show ProofState where

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

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

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

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

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

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

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

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

97 wkenv = premises g in

100 wkenv = premises g in

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

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

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

115 showG ps b = showEnv ps (binderTy b)

118 showG ps b = showEnv ps (binderTy b)

116

119

117instance Pretty ProofState OutputAnnotation where

120instance Pretty ProofState OutputAnnotation where

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

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

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

122 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 _ _ _ _ _) =

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

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

122 let wkEnv = premises g in

125 let wkEnv = premises g in

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

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

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

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

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

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

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

287 Nothing [] []

290 Nothing [] []

288− [] []

291+ [] [] []

289− Nothing ctxt "" False False []

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

290

293

291type TState = ProofState -- [TacticAction])

294type TState = ProofState -- [TacticAction])

292type RunTactic = RunTactic' TState

295type RunTactic = RunTactic' TState

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

381 instances = x:is })

384 instances = x:is })

382 return (Bind x (Hole t) sc)

385 return (Bind x (Hole t) sc)

383

386

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+

384setinj :: Name -> RunTactic

397setinj :: Name -> RunTactic

385setinj n ctxt env (Bind x b sc)

398setinj n ctxt env (Bind x b sc)

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

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

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

494 solved = Just (x, val),

507 solved = Just (x, val),

495 notunified = updateNotunified [(x,val)]

508 notunified = updateNotunified [(x,val)]

496 (notunified ps),

509 (notunified ps),

510+ recents = x : recents ps,

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

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

498 let tm' = subst x val sc in

512 let tm' = subst x val sc in

499 return tm'

513 return tm'

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

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

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

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

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

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

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

651 mapM_ addConsHole (reverse consargs')

666 mapM_ addConsHole (reverse consargs')

652 let res' = forget $ res

667 let res' = forget $ res

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

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

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

739 let (_, ns) = unified ps

754 let (_, ns) = unified ps

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

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

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

756 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 })

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

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

744 return (updateSolvedTerm unify tm)

760 return (updateSolvedTerm unify tm)

745

761

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

858 unified = (h, []),

874 unified = (h, []),

859 problems = probs',

875 problems = probs',

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

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

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

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

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

862processTactic UnifyAll ps

879processTactic UnifyAll ps

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

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

864 return (ps { pterm = tm',

881 return (ps { pterm = tm',

865 notunified = [],

882 notunified = [],

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

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

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

867processTactic (Reorder n) ps

885processTactic (Reorder n) ps

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

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

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

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

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

883 previous = Just ps, plog = "",

901 previous = Just ps, plog = "",

884 notunified = updateNotunified ns' (notunified ps),

902 notunified = updateNotunified ns' (notunified ps),

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

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

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

886processTactic (MatchProblems all) ps

905processTactic (MatchProblems all) ps

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

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

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

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

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

898 previous = Just ps, plog = "",

917 previous = Just ps, plog = "",

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

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

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

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

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

901processTactic t ps

921processTactic t ps

902 = case holes ps of

922 = case holes ps of

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

921 problems = probs',

941 problems = probs',

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

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

923 previous = Just ps, plog = "",

943 previous = Just ps, plog = "",

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

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

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

925

946

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

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

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

959 mktac (Defer ns n) = defer ns n

980 mktac (Defer ns n) = defer ns n

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

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

961 mktac (Instance n) = instanceArg n

982 mktac (Instance n) = instanceArg n

983+ mktac (AutoArg n) = autoArg n

962 mktac (SetInjective n) = setinj n

984 mktac (SetInjective n) = setinj n

963 mktac (MoveLast n) = movelast n

985 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

180

181updateSolvedPath [] t = t

182updateSolvedPath ns Top = Top

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

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

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

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

185updateSolvedPath ns (InBind n b sc)

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

187 where

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

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

1360

1361 sortP ps = pick [] (reverse ps)

1362

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−

1371 pick acc [] = reverse acc

1363 pick acc [] = reverse acc

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

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

1373

1365

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

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

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

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

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

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

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

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

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

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

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

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

1380

1372

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+

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

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

1382liftPats :: Term -> Term

1383liftPats :: Term -> Term

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

1384liftPats 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) []

229

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

231

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

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

233− getUniqB env us (Guess t v) = do getUniq env us t; 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

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

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

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

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

237

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

239-- directly in a static position

src/Idris/ElabTerm.hs+35−6

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

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

53 [TIPartial] -> True

54 _ -> False

55− ivs <- get_instances

55+

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

57+

56 hs <- get_holes

58 hs <- get_holes

59+ ivs <- get_instances

57 ptm <- get_term

60 ptm <- get_term

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

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

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

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

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

187 elabE ina fc' t =

190 elabE ina fc' t =

188 --do g <- goal

191 --do g <- goal

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

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

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+

190− do ct <- insertCoerce ina t

201+ ct <- insertCoerce ina t

191 t' <- insertLazy ct

202 t' <- insertLazy ct

192 g <- goal

203 g <- goal

193 tm <- get_term

204 tm <- get_term

194 ps <- get_probs

205 ps <- get_probs

195 hs <- get_holes

206 hs <- get_holes

207+

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

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

197 -- ++ "\n" ++ show tm

209 -- ++ "\n" ++ show tm

198 -- ++ "\nholes " ++ show hs

210 -- ++ "\nholes " ++ show hs

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

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

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

968 = elabArg argName holeName t

980 = elabArg argName holeName t

969 where elabArg argName holeName t =

981 where elabArg argName holeName t =

982+ do -- solveAutos ist fn False

970− do now_elaborating fc f argName

983+ now_elaborating fc f argName

971 wrapErr f argName $ do

984 wrapErr f argName $ do

972 hs <- get_holes

985 hs <- get_holes

973 tm <- get_term

986 tm <- get_term

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

1077 _ -> []

1090 _ -> []

1078 | otherwise = []

1091 | otherwise = []

1079

1092

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+

1080trivial' ist

1109trivial' ist

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

1110 = 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

1083 = do unifyProblems

1112 = do unifyProblems

1084− proofSearch rec prv depth

1113+ proofSearch rec prv ambigok (not prv) depth

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

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

1086

1115

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

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

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

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

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

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

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

1336 runT (ProofSearch rec prover depth top hints)

1365 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

1338 when autoSolve solveAll

1367 when autoSolve solveAll

1339 runT (Focus n) = focus n

1368 runT (Focus n) = focus n

1340 runT Solve = solve

1369 runT Solve = solve

src/Idris/ProofSearch.hs+44−9

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

38 (tryAll xs) True

39 else tryAll xs

41−cantSolveGoal :: ElabD ()

41+cantSolveGoal :: ElabD a

42cantSolveGoal = do g <- goal

43 env <- get_env

44 lift $ tfail $

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

47−proofSearch :: Bool ->

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

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

49 -- new metavariables is meaningless, and there shoudl

50 -- be an error reported instead.

51+ Bool -> -- ambiguity ok

52+ Bool -> -- defer on failure

51 Int -> -- maximum depth

53 Int -> -- maximum depth

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

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

53 IState -> ElabD ()

55 IState -> ElabD ()

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

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

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

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

56 -- works

58 -- works

57 let all_imps = lookupCtxtName fn (idris_implicits ist)

59 let all_imps = lookupCtxtName fn (idris_implicits ist)

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

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

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

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

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

85−proofSearch rec fromProver maxDepth elab fn nroot hints ist

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

86− = case lookupCtxt nroot (idris_tyinfodata ist) of

91+ case lookupCtxt nroot (idris_tyinfodata ist) of

87− [TISolution ts] -> findInferredTy ts

92+ [TISolution ts] -> findInferredTy ts

88− _ -> psRec rec maxDepth

93+ _ -> psRec rec maxDepth

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

89 where

95 where

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

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

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+

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

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

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

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

94 | otherwise = P nt (UN n) ty

127 | otherwise = P nt (UN n) ty

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

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

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

141

174

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

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

143− tryCon d n =

176+ tryCon d n =

177+ do ty <- goal

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

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

145 [] -> []

179 [] -> []

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

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

147 _ -> fail "Ambiguous name"

181 _ -> fail "Ambiguous name"

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

153 hs' <- get_holes

187 hs' <- get_holes

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

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

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

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

190+ aty <- goal

156 psRec True d)

191 psRec True d)

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

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

158 solve

193 solve

src/Idris/Prover.hs+2−2

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

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

115

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

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

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

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

119 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

121 let OK ty = goalAtFocus ps

122 let OK env = envAtFocus ps

123 let state = prettyOtherGoals hs <> line <>