7095d6c · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3−3

compare with master

unifiedsplit

@@ -597,7 +597,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0)

597

598-- | Save information about a name that is not yet defined

599addDeferred' :: NameType

600− -> [(Name, (Int, Maybe Name, Type, Bool))]

600+ -> [(Name, (Int, Maybe Name, Type, [Name], Bool))]

601 -- ^ The Name is the name being made into a metavar,

602 -- the Int is the number of vars that are part of a

603 -- putative proof context, the Maybe Name is the

@@ -606,10 +606,10 @@ addDeferred' :: NameType

606 -- allowed

607 -> Idris ()

608addDeferred' nt ns

609− = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

609+ = do mapM_ (\(n, (i, _, t, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

610 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

611 i <- getIState

612− putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

612+ putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel)) -> (n, (top, i, ns, isTopLevel))) ns ++

613 idris_metavars i }

614 where

615 -- 'tidyNames' is to generate user accessible names in case they are

src/Idris/AbsSyntaxTree.hs+12−7

@@ -195,10 +195,11 @@ data IState = IState {

195 idris_name :: Int,

196 idris_lineapps :: [((FilePath, Int), PTerm)],

197 -- ^ Full application LHS on source line

198− idris_metavars :: [(Name, (Maybe Name, Int, Bool))],

198+ idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool))],

199 -- ^ The currently defined but not proven metavariables. The Int

200 -- is the number of vars to display as a context, the Maybe Name

201+ -- is its top-level function, the [Name] is the list of local variables

201− -- is its top-level function, and the Bool is whether :p is

202+ -- available for proof search and the Bool is whether :p is

202 -- allowed

203 -- allowed

203 idris_coercions :: [Name],

204 idris_coercions :: [Name],

204 idris_errRev :: [(Term, Term)],

205 idris_errRev :: [(Term, Term)],

@@ -404,9 +405,11 @@ data Command = Quit

404 | MakeWith Bool Int Name

405 | MakeWith Bool Int Name

405 | MakeCase Bool Int Name

406 | MakeCase Bool Int Name

406 | MakeLemma Bool Int Name

407 | MakeLemma Bool Int Name

407− | DoProofSearch Bool Bool Int Name [Name]

408+ | DoProofSearch Bool -- update file

408− -- ^ the first bool is whether to update,

409+ Bool -- recursive search

409− -- the second is whether to search recursively (i.e. for the arguments)

410+ Int -- depth

411+ Name -- top level name

412+ [Name] -- hints

410 | SetOpt Opt

413 | SetOpt Opt

411 | UnsetOpt Opt

414 | UnsetOpt Opt

412 | NOP

415 | NOP

@@ -982,7 +985,9 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

982 | MatchRefine Name

985 | MatchRefine Name

983 | LetTac Name t | LetTacTy Name t t

986 | LetTac Name t | LetTacTy Name t t

984 | Exact t | Compute | Trivial | TCInstance

987 | Exact t | Compute | Trivial | TCInstance

985− | ProofSearch Bool Bool Int (Maybe Name) [Name]

988+ | ProofSearch Bool Bool Int (Maybe Name)

989+ [Name] -- allowed local names

990+ [Name] -- hints

986 -- ^ the bool is whether to search recursively

991 -- ^ the bool is whether to search recursively

987 | Solve

992 | Solve

988 | Attack

993 | Attack

@@ -1580,7 +1585,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1580 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =

1585 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =

1581 depth d . bracket p startPrec $

1586 depth d . bracket p startPrec $

1582 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1587 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1583− prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =

1588+ prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =

1584 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>

1589 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>

1585 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1590 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1586 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =

1591 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =

src/Idris/Completion.hs+1−1

@@ -52,7 +52,7 @@ names = do i <- get

52

53metavars :: Idris [String]

54metavars = do i <- get

55− return . map (show . nsroot) $ map fst (filter (\(_, (_,_,t)) -> not t) (idris_metavars i)) \\ primDefs

55+ return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t)) -> not t) (idris_metavars i)) \\ primDefs

56

57

58modules :: Idris [String]

src/Idris/Core/Binary.hs+6−4

@@ -499,9 +499,10 @@ instance (Binary b) => Binary (Binder b) where

499 put x2

500 Hole x1 -> do putWord8 4

501 put x1

502− GHole x1 x2 -> do putWord8 5

502+ GHole x1 x2 x3 -> do putWord8 5

503− put x1

503+ put x1

504− put x2

504+ put x2

505+ put x3

505 Guess x1 x2 -> do putWord8 6

506 Guess x1 x2 -> do putWord8 6

506 put x1

507 put x1

507 put x2

508 put x2

@@ -528,7 +529,8 @@ instance (Binary b) => Binary (Binder b) where

528 return (Hole x1)

529 return (Hole x1)

529 5 -> do x1 <- get

530 5 -> do x1 <- get

530 x2 <- get

531 x2 <- get

532+ x3 <- get

531− return (GHole x1 x2)

533+ return (GHole x1 x2 x3)

532 6 -> do x1 <- get

534 6 -> do x1 <- get

533 x2 <- get

535 x2 <- get

534 return (Guess x1 x2)

536 return (Guess x1 x2)

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

@@ -128,7 +128,7 @@ instance (NFData b) => NFData (Binder b) where

128 rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

129 rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

130 rnf (Hole x1) = rnf x1 `seq` ()

131− rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

131+ rnf (GHole x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

132 rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

133 rnf (PVar x1) = rnf x1 `seq` ()

134 rnf (PVTy x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+14

@@ -51,6 +51,20 @@ explicit n = do ES (p, a) s m <- get

51 let p' = p { dontunify = n : dontunify p }

52 put (ES (p', a) s m)

53

54+-- Add a name that's okay to use in proof search (typically either because

55+-- it was given explicitly on the lhs, or intrduced as an explicit lambda

56+-- or let binding)

57+addPSname :: Name -> Elab' aux ()

58+addPSname n@(UN _)

59+ = do ES (p, a) s m <- get

60+ let p' = p { psnames = n : psnames p }

61+ put (ES (p', a) s m)

62+addPSname _ = return () -- can only use user given names

63+

64+getPSnames :: Elab' aux [Name]

65+getPSnames = do ES (p, a) s m <- get

66+ return (psnames p)

67+

54saveState :: Elab' aux ()

68saveState :: Elab' aux ()

55saveState = do e@(ES p s _) <- get

69saveState = do e@(ES p s _) <- get

56 put (ES p s (Just e))

70 put (ES p s (Just e))

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

@@ -93,7 +93,7 @@ toTT (EBind n b body) = do n' <- newN n

93 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

94 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

95 fixBinder (Hole t) = Hole <$> toTT t

96− fixBinder (GHole i t) = GHole i <$> toTT t

96+ fixBinder (GHole i ns t) = GHole i ns <$> toTT t

97 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

98 fixBinder (PVar t) = PVar <$> toTT t

99 fixBinder (PVTy t) = PVTy <$> toTT t

src/Idris/Core/ProofState.hs+5−3

@@ -39,6 +39,7 @@ data ProofState = PS { thname :: 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

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

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

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

43 context :: Context,

44 context :: Context,

44 datatypes :: Ctxt TypeInfo,

45 datatypes :: Ctxt TypeInfo,

@@ -301,7 +302,7 @@ newProof n ctxt datatypes ty =

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

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

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

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

303 Nothing [] []

304 Nothing [] []

304− [] [] []

305+ [] [] [] []

305 Nothing ctxt datatypes "" False False [] []

306 Nothing ctxt datatypes "" False False [] []

306

307

307type TState = ProofState -- [TacticAction])

308type TState = ProofState -- [TacticAction])

@@ -429,7 +430,8 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

429 do let env' = filter (\(n, t) -> n `notElem` dropped) env

430 do let env' = filter (\(n, t) -> n `notElem` dropped) env

430 action (\ps -> let hs = holes ps in

431 action (\ps -> let hs = holes ps in

431 ps { holes = hs \\ [x] })

432 ps { holes = hs \\ [x] })

433+ ps <- get

432− return (Bind n (GHole (length env') (mkTy (reverse env') t))

434+ return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))

433 (mkApp (P Ref n ty) (map getP (reverse env'))))

435 (mkApp (P Ref n ty) (map getP (reverse env'))))

434 where

436 where

435 mkTy [] t = t

437 mkTy [] t = t

@@ -445,7 +447,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

445 ds = deferred ps in

447 ds = deferred ps in

446 ps { holes = hs \\ [x],

448 ps { holes = hs \\ [x],

447 deferred = n : ds })

449 deferred = n : ds })

448− return (Bind n (GHole 0 fty)

450+ return (Bind n (GHole 0 [] fty)

449 (mkApp (P Ref n ty) (map getP args)))

451 (mkApp (P Ref n ty) (map getP args)))

450 where

452 where

451 getP n = case lookup n env of

453 getP n = case lookup n env of

src/Idris/Core/TT.hs+8−7

@@ -809,6 +809,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}

809 binderVal :: b }

810 | Hole { binderTy :: !b}

811 | GHole { envlen :: Int,

812+ localnames :: [Name],

812 binderTy :: !b}

813 binderTy :: !b}

813 | Guess { binderTy :: !b,

814 | Guess { binderTy :: !b,

814 binderVal :: b }

815 binderVal :: b }

@@ -827,7 +828,7 @@ instance Sized a => Sized (Binder a) where

827 size (Let ty val) = 1 + size ty + size val

828 size (Let ty val) = 1 + size ty + size val

828 size (NLet ty val) = 1 + size ty + size val

829 size (NLet ty val) = 1 + size ty + size val

829 size (Hole ty) = 1 + size ty

830 size (Hole ty) = 1 + size ty

830− size (GHole _ ty) = 1 + size ty

831+ size (GHole _ _ ty) = 1 + size ty

831 size (Guess ty val) = 1 + size ty + size val

832 size (Guess ty val) = 1 + size ty + size val

832 size (PVar ty) = 1 + size ty

833 size (PVar ty) = 1 + size ty

833 size (PVTy ty) = 1 + size ty

834 size (PVTy ty) = 1 + size ty

@@ -839,7 +840,7 @@ fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)

839fmapMB f (Lam t) = liftM Lam (f t)

840fmapMB f (Lam t) = liftM Lam (f t)

840fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k)

841fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k)

841fmapMB f (Hole t) = liftM Hole (f t)

842fmapMB f (Hole t) = liftM Hole (f t)

842−fmapMB f (GHole i t) = liftM (GHole i) (f t)

843+fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t)

843fmapMB f (PVar t) = liftM PVar (f t)

844fmapMB f (PVar t) = liftM PVar (f t)

844fmapMB f (PVTy t) = liftM PVTy (f t)

845fmapMB f (PVTy t) = liftM PVTy (f t)

845

846

@@ -1494,7 +1495,7 @@ prettyEnv env t = prettyEnv' env t False

1494 -- Render a `Binder` and its name

1495 -- Render a `Binder` and its name

1495 prettySb env n (Lam t) = prettyB env "λ" "=>" n t

1496 prettySb env n (Lam t) = prettyB env "λ" "=>" n t

1496 prettySb env n (Hole t) = prettyB env "?defer" "." n t

1497 prettySb env n (Hole t) = prettyB env "?defer" "." n t

1497− prettySb env n (GHole _ t) = prettyB env "?gdefer" "." n t

1498+ prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t

1498 prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t

1499 prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t

1499 prettySb env n (PVar t) = prettyB env "pat" "." n t

1500 prettySb env n (PVar t) = prettyB env "pat" "." n t

1500 prettySb env n (PVTy t) = prettyB env "pty" "." n t

1501 prettySb env n (PVTy t) = prettyB env "pty" "." n t

@@ -1539,7 +1540,7 @@ showEnv' env t dbg = se 10 env t where

1539

1540

1540 sb env n (Lam t) = showb env "\\ " " => " n t

1541 sb env n (Lam t) = showb env "\\ " " => " n t

1541 sb env n (Hole t) = showb env "? " ". " n t

1542 sb env n (Hole t) = showb env "? " ". " n t

1542− sb env n (GHole i t) = showb env "?defer " ". " n t

1543+ sb env n (GHole i ns t) = showb env "?defer " ". " n t

1543 sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t

1544 sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t

1544 sb env n (Pi _ t _) = showb env "(" ") -> " n t

1545 sb env n (Pi _ t _) = showb env "(" ") -> " n t

1545 sb env n (PVar t) = showb env "pat " ". " n t

1546 sb env n (PVar t) = showb env "pat " ". " n t

@@ -1739,7 +1740,7 @@ pprintTT bound tm = pp startPrec bound tm

1739 ppb p bound n (Hole ty) sc =

1740 ppb p bound n (Hole ty) sc =

1740 bracket p startPrec . group . align . hang 2 $

1741 bracket p startPrec . group . align . hang 2 $

1741 text "?" <+> bindingOf n False <+> text "." <> line <> sc

1742 text "?" <+> bindingOf n False <+> text "." <> line <> sc

1742− ppb p bound n (GHole _ ty) sc =

1743+ ppb p bound n (GHole _ _ ty) sc =

1743 bracket p startPrec . group . align . hang 2 $

1744 bracket p startPrec . group . align . hang 2 $

1744 text "¿" <+> bindingOf n False <+> text "." <> line <> sc

1745 text "¿" <+> bindingOf n False <+> text "." <> line <> sc

1745 ppb p bound n (Guess ty val) sc =

1746 ppb p bound n (Guess ty val) sc =

@@ -1791,8 +1792,8 @@ pprintRaw bound (RBind n b body) =

1791 vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]

1792 vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]

1792 ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $

1793 ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $

1793 text "Hole" <$> pprintRaw bound ty

1794 text "Hole" <$> pprintRaw bound ty

1794− ppb (GHole _ ty) = enclose lparen rparen . group . align . hang 2 $

1795+ ppb (GHole _ _ ty) = enclose lparen rparen . group . align . hang 2 $

1795− text "GHole" <$> pprintRaw bound ty

1796+ text "GHole" <$> pprintRaw bound ty

1796 ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $

1797 ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $

1797 vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]

1798 vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]

1798 ppb (PVar ty) = enclose lparen rparen . group . align . hang 2 $

1799 ppb (PVar ty) = enclose lparen rparen . group . align . hang 2 $

src/Idris/Core/Typecheck.hs+4−4

@@ -232,12 +232,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

232 let tt' = normalise ctxt env tt

233 lift $ isType ctxt env tt'

234 return (Hole tv, tt')

235− checkBinder (GHole i t)

235+ checkBinder (GHole i ns t)

236 = do (tv, tt) <- chk u env t

237 let tv' = normalise ctxt env tv

238 let tt' = normalise ctxt env tt

239 lift $ isType ctxt env tt'

240− return (GHole i tv, tt')

240+ return (GHole i ns tv, tt')

241 checkBinder (Guess t v)

242 | not holes = lift $ tfail (IncompleteTerm undefined)

243 | otherwise

@@ -273,8 +273,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

273 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)

274 discharge n (Hole t) bt scv sct

275 = return (Bind n (Hole t) scv, sct)

276− discharge n (GHole i t) bt scv sct

276+ discharge n (GHole i ns t) bt scv sct

277− = return (Bind n (GHole i t) scv, sct)

277+ = return (Bind n (GHole i ns t) scv, sct)

278 discharge n (Guess t v) bt scv sct

279 = return (Bind n (Guess t v) scv, sct)

280 discharge n (PVar t) bt scv sct

src/Idris/DeepSeq.hs+2−2

@@ -295,8 +295,8 @@ instance (NFData t) => NFData (PTactic' t) where

295 rnf Compute = ()

296 rnf Trivial = ()

297 rnf TCInstance = ()

298− rnf (ProofSearch r r1 r2 x1 x2)

298+ rnf (ProofSearch r r1 r2 x1 x2 x3)

299− = rnf x1 `seq` rnf x2 `seq` ()

299+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

300 rnf Solve = ()

301 rnf Attack = ()

302 rnf ProofState = ()

src/Idris/Delaborate.hs+2−2

@@ -106,7 +106,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

106 | Just n' <- lookup n env = PRef un [] n'

107 | otherwise

108 = case lookup n (idris_metavars ist) of

109− Just (Just _, mi, _) -> mkMVApp n []

109+ Just (Just _, mi, _, _) -> mkMVApp n []

110 _ -> PRef un [] n

111 de env _ (Bind n (Lam ty) sc)

112 = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)

@@ -169,7 +169,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

169 = PApp un (de env [] f) (map pexp (map (de env []) args))

170 deFn env (P _ n _) args

171 | not mvs = case lookup n (idris_metavars ist) of

172− Just (Just _, mi, _) ->

172+ Just (Just _, mi, _, _) ->

173 mkMVApp n (drop mi (map (de env []) args))

174 _ -> mkPApp n (map (de env []) args)

175 | otherwise = mkPApp n (map (de env []) args)

src/Idris/Elab/Clause.hs+10−6

@@ -632,6 +632,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

632 ((rhs', defer, is, probs, ctxt', newDecls, highlights), _) <-

633 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState

634 (do pbinds ist lhs_tm

635+ -- proof search can use explicitly written names

636+ mapM_ addPSname (allNamesIn lhs_in)

635 mapM_ setinj (nub (params ++ inj))

637 mapM_ setinj (nub (params ++ inj))

636 setNextName

638 setNextName

637 (ElabResult _ _ is ctxt' newDecls highlights) <-

639 (ElabResult _ _ is ctxt' newDecls highlights) <-

@@ -656,9 +658,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

656 logLvl 5 "DONE CHECK"

658 logLvl 5 "DONE CHECK"

657 logLvl 4 $ "---> " ++ show rhs'

659 logLvl 4 $ "---> " ++ show rhs'

658 when (not (null defer)) $ logLvl 1 $ "DEFERRED " ++

660 when (not (null defer)) $ logLvl 1 $ "DEFERRED " ++

659− show (map (\ (n, (_,_,t)) -> (n, t)) defer)

661+ show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)

660 def' <- checkDef fc (Elaborating "deferred type of ") defer

662 def' <- checkDef fc (Elaborating "deferred type of ") defer

661− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

663+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

662 addDeferred def''

664 addDeferred def''

663 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

665 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

664

666

@@ -816,6 +818,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

816 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")

818 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")

817 (bindTyArgs PVTy bargs infP) initEState

819 (bindTyArgs PVTy bargs infP) initEState

818 (do pbinds i lhs_tm

820 (do pbinds i lhs_tm

821+ -- proof search can use explicitly written names

822+ mapM_ addPSname (allNamesIn lhs_in)

819 setNextName

823 setNextName

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

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

821 (ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname

825 (ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname

@@ -828,7 +832,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

828 sendHighlighting highlights

832 sendHighlighting highlights

829

833

830 def' <- checkDef fc iderr defer

834 def' <- checkDef fc iderr defer

831− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

835+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

832 addDeferred def''

836 addDeferred def''

833 mapM_ (elabCaseBlock info opts) is

837 mapM_ (elabCaseBlock info opts) is

834 logLvl 5 ("Checked wval " ++ show wval')

838 logLvl 5 ("Checked wval " ++ show wval')

@@ -890,8 +894,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

890 addIBC (IBCImp wname)

894 addIBC (IBCImp wname)

891 addIBC (IBCStatic wname)

895 addIBC (IBCStatic wname)

892

896

893− def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))]

897+ def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype, []))]

894− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

898+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

895 addDeferred def''

899 addDeferred def''

896

900

897 -- in the subdecls, lhs becomes:

901 -- in the subdecls, lhs becomes:

@@ -932,7 +936,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

932 sendHighlighting highlights

936 sendHighlighting highlights

933

937

934 def' <- checkDef fc iderr defer

938 def' <- checkDef fc iderr defer

935− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

939+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def'

936 addDeferred def''

940 addDeferred def''

937 mapM_ (elabCaseBlock info opts) is

941 mapM_ (elabCaseBlock info opts) is

938 logLvl 5 ("Checked RHS " ++ show rhs')

942 logLvl 5 ("Checked RHS " ++ show rhs')

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

@@ -41,7 +41,7 @@ data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS

41

42data ElabResult =

43 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration

44− , resultMetavars :: [(Name, (Int, Maybe Name, Type))]

44+ , resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]

45 -- ^ Information about new metavariables

46 , resultCaseDecls :: [PDecl]

47 -- ^ Deferred declarations as the meaning of case blocks

@@ -627,6 +627,7 @@ elab ist info emode opts fn tm

627 lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")

628 checkPiGoal n

629 attack; intro (Just n);

630+ addPSname n -- okay for proof search

630 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

631 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

631 elabE (ina { e_inarg = True } ) (Just fc) sc; solve

632 elabE (ina { e_inarg = True } ) (Just fc) sc; solve

632 highlightSource nfc (AnnBoundName n False)

633 highlightSource nfc (AnnBoundName n False)

@@ -643,6 +644,7 @@ elab ist info emode opts fn tm

643 ptm <- get_term

644 ptm <- get_term

644 hs <- get_holes

645 hs <- get_holes

645 introTy (Var tyn) (Just n)

646 introTy (Var tyn) (Just n)

647+ addPSname n -- okay for proof search

646 focus tyn

648 focus tyn

647

649

648 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

650 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

@@ -651,6 +653,7 @@ elab ist info emode opts fn tm

651 highlightSource nfc (AnnBoundName n False)

653 highlightSource nfc (AnnBoundName n False)

652 elab' ina fc (PPi p n nfc Placeholder sc)

654 elab' ina fc (PPi p n nfc Placeholder sc)

653 = do attack; arg n (is_scoped p) (sMN 0 "ty")

655 = do attack; arg n (is_scoped p) (sMN 0 "ty")

656+ addPSname n -- okay for proof search

654 elabE (ina { e_inarg = True, e_intype = True }) fc sc

657 elabE (ina { e_inarg = True, e_intype = True }) fc sc

655 solve

658 solve

656 highlightSource nfc (AnnBoundName n False)

659 highlightSource nfc (AnnBoundName n False)

@@ -661,6 +664,7 @@ elab ist info emode opts fn tm

661 MN _ _ -> unique_hole n

664 MN _ _ -> unique_hole n

662 _ -> return n

665 _ -> return n

663 forall n' (is_scoped p) (Var tyn)

666 forall n' (is_scoped p) (Var tyn)

667+ addPSname n' -- okay for proof search

664 focus tyn

668 focus tyn

665 let ec' = ina { e_inarg = True, e_intype = True }

669 let ec' = ina { e_inarg = True, e_intype = True }

666 elabE ec' fc ty

670 elabE ec' fc ty

@@ -676,6 +680,7 @@ elab ist info emode opts fn tm

676 claim valn (Var tyn)

680 claim valn (Var tyn)

677 explicit valn

681 explicit valn

678 letbind n (Var tyn) (Var valn)

682 letbind n (Var tyn) (Var valn)

683+ addPSname n

679 case ty of

684 case ty of

680 Placeholder -> return ()

685 Placeholder -> return ()

681 _ -> do focus tyn

686 _ -> do focus tyn

@@ -961,6 +966,7 @@ elab ist info emode opts fn tm

961 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

966 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

962 let n' = metavarName (namespace info) n

967 let n' = metavarName (namespace info) n

963 attack

968 attack

969+ psns <- getPSnames

964 defer unique_used n'

970 defer unique_used n'

965 solve

971 solve

966 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

972 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

@@ -1620,7 +1626,7 @@ solveAuto ist fn ambigok n

1620 g <- goal

1626 g <- goal

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

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

1622 when (not isg) $

1628 when (not isg) $

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

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

1624

1630

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

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

1626solveAutos ist fn ambigok

1632solveAutos ist fn ambigok

@@ -1629,12 +1635,12 @@ solveAutos ist fn ambigok

1629

1635

1630trivial' ist

1636trivial' ist

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

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

1632−trivialHoles' h ist

1638+trivialHoles' psn h ist

1633− = trivialHoles h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1639+ = trivialHoles psn h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1634−proofSearch' ist rec ambigok depth prv top n hints

1640+proofSearch' ist rec ambigok depth prv top n psns hints

1635 = do unifyProblems

1641 = do unifyProblems

1636 proofSearch rec prv ambigok (not prv) depth

1642 proofSearch rec prv ambigok (not prv) depth

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

1643+ (elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist

1638

1644

1639-- | Resolve type classes. This will only pick up 'normal' instances, never

1645-- | Resolve type classes. This will only pick up 'normal' instances, never

1640-- named instances (which is enforced by 'findInstances').

1646-- named instances (which is enforced by 'findInstances').

@@ -1674,7 +1680,7 @@ resTC' tcs defaultOn topholes depth topg fn ist

1674 _ -> []

1680 _ -> []

1675

1681

1676 traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

1682 traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

1677− try' (trivialHoles' okholes ist)

1683+ try' (trivialHoles' [] okholes ist)

1678 (do addDefault t tc ttypes

1684 (do addDefault t tc ttypes

1679 let stk = map fst (filter snd $ elab_stack ist)

1685 let stk = map fst (filter snd $ elab_stack ist)

1680 let insts = findInstances ist t

1686 let insts = findInstances ist t

@@ -1799,11 +1805,11 @@ resTC' tcs defaultOn topholes depth topg fn ist

1799 isImp arg = (False, priority arg)

1805 isImp arg = (False, priority arg)

1800

1806

1801collectDeferred :: Maybe Name -> [Name] -> Context ->

1807collectDeferred :: Maybe Name -> [Name] -> Context ->

1802− Term -> State [(Name, (Int, Maybe Name, Type))] Term

1808+ Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term

1803−collectDeferred top casenames ctxt (Bind n (GHole i t) app) =

1809+collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =

1804 do ds <- get

1810 do ds <- get

1805 t' <- collectDeferred top casenames ctxt t

1811 t' <- collectDeferred top casenames ctxt t

1806− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t'))])

1812+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))])

1807 collectDeferred top casenames ctxt app

1813 collectDeferred top casenames ctxt app

1808 where

1814 where

1809 -- Evaluate the top level functions in arguments, if possible, and if it's

1815 -- Evaluate the top level functions in arguments, if possible, and if it's

@@ -2118,7 +2124,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2118 do actualHints <- mapM reifyTTName hs

2124 do actualHints <- mapM reifyTTName hs

2119 unifyProblems

2125 unifyProblems

2120 let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")

2126 let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")

2121− proofSearch True True False False i psElab Nothing (sMN 0 "search ") actualHints ist

2127+ proofSearch True True False False i psElab Nothing (sMN 0 "search ") [] actualHints ist

2122 returnUnit

2128 returnUnit

2123 (Constant (I _), Nothing ) ->

2129 (Constant (I _), Nothing ) ->

2124 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'

2130 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'

@@ -2290,8 +2296,8 @@ runTac autoSolve ist perhapsFC fn tac

2290 runT Compute = compute

2296 runT Compute = compute

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

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

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

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

2293− runT (ProofSearch rec prover depth top hints)

2299+ runT (ProofSearch rec prover depth top psns hints)

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

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

2295 when autoSolve solveAll

2301 when autoSolve solveAll

2296 runT (Focus n) = focus n

2302 runT (Focus n) = focus n

2297 runT Unfocus = do hs <- get_holes

2303 runT Unfocus = do hs <- get_holes

@@ -2499,7 +2505,7 @@ processTacticDecls info steps =

2499 updateIState $ \i -> i { idris_implicits =

2505 updateIState $ \i -> i { idris_implicits =

2500 addDef n impls (idris_implicits i) }

2506 addDef n impls (idris_implicits i) }

2501 addIBC (IBCImp n)

2507 addIBC (IBCImp n)

2502− ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]

2508+ ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty, []))]

2503 addIBC (IBCDef n)

2509 addIBC (IBCDef n)

2504 ctxt <- getContext

2510 ctxt <- getContext

2505 case lookupDef n ctxt of

2511 case lookupDef n ctxt of

@@ -2508,7 +2514,7 @@ processTacticDecls info steps =

2508 -- then it must be added as a metavariable. This needs guarding

2514 -- then it must be added as a metavariable. This needs guarding

2509 -- to prevent overwriting case defs with a metavar, if the case

2515 -- to prevent overwriting case defs with a metavar, if the case

2510 -- defs come after the type decl in the same script!

2516 -- defs come after the type decl in the same script!

2511− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

2517+ let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) ds

2512 in addDeferred ds'

2518 in addDeferred ds'

2513 _ -> return ()

2519 _ -> return ()

2514 RAddInstance className instName ->

2520 RAddInstance className instName ->

src/Idris/Elab/Type.hs+2−2

@@ -159,9 +159,9 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

159 -- Productivity checking now via checking for guarded 'Delay'

160 let opts' = opts -- if corec then (Coinductive : opts) else opts

161 let usety = if norm then nty' else nty

162− ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]

162+ ds <- checkDef fc iderr [(n, (-1, Nothing, usety, []))]

163 addIBC (IBCDef n)

164− let ds' = map (\(n, (i, top, fam)) -> (n, (i, top, fam, True))) ds

164+ let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True))) ds

165 addDeferred ds'

166 setFlags n opts'

167 checkDocs fc argDocs ty

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

@@ -40,21 +40,21 @@ recheckC_borrowing uniq_check bs fc mkerr env t

40iderr :: Name -> Err -> Err

41iderr _ e = e

42

43−checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]

43+checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type, [Name]))]

44− -> Idris [(Name, (Int, Maybe Name, Type))]

44+ -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

45checkDef fc mkerr ns = checkAddDef False True fc mkerr ns

46

47checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)

48− -> [(Name, (Int, Maybe Name, Type))]

48+ -> [(Name, (Int, Maybe Name, Type, [Name]))]

49− -> Idris [(Name, (Int, Maybe Name, Type))]

49+ -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

50checkAddDef add toplvl fc mkerr [] = return []

51−checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns)

51+checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns)

52 = do ctxt <- getContext

53 (t', _) <- recheckC fc (mkerr n) [] t

54− when add $ do addDeferred [(n, (i, top, t, toplvl))]

54+ when add $ do addDeferred [(n, (i, top, t, psns, toplvl))]

55 addIBC (IBCDef n)

56 ns' <- checkAddDef add toplvl fc mkerr ns

57− return ((n, (i, top, t')) : ns')

57+ return ((n, (i, top, t', psns)) : ns')

58

59-- | Get the list of (index, name) of inaccessible arguments from an elaborated

60-- type

src/Idris/Elab/Value.hs+1−1

@@ -76,7 +76,7 @@ elabValBind info aspat norm tm_in

76 let vtm = orderPats (getInferTerm tm')

77

78 def' <- checkDef (fileFC "(input)") iderr defer

79− let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

79+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) def'

80 addDeferred def''

81 mapM_ (elabCaseBlock info []) is

82

src/Idris/IBC.hs+12−10

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 116

43+ibcVersion = 117

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

@@ -78,7 +78,7 @@ data IBCFile = IBCFile { ver :: Word16,

78 ibc_metainformation :: ![(Name, MetaInformation)],

79 ibc_errorhandlers :: ![Name],

80 ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler

81− ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))],

81+ ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool))],

82 ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

83 ibc_postulates :: ![Name],

84 ibc_externs :: ![(Name, Int)],

@@ -610,7 +610,7 @@ pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

610pFunctionErrorHandlers ns = mapM_ (\ (fn,arg,handler) ->

611 addFunctionErrorHandlers fn arg [handler]) ns

612

613−pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

613+pMetavars :: [(Name, (Maybe Name, Int, [Name], Bool))] -> Idris ()

614pMetavars ns = updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })

615

616----- For Cheapskate and docstrings

@@ -1869,12 +1869,13 @@ instance (Binary t) => Binary (PTactic' t) where

1869 put x1

1870 ByReflection x1 -> do putWord8 20

1871 put x1

1872− ProofSearch x1 x2 x3 x4 x5 -> do putWord8 21

1872+ ProofSearch x1 x2 x3 x4 x5 x6 -> do putWord8 21

1873− put x1

1873+ put x1

1874− put x2

1874+ put x2

1875− put x3

1875+ put x3

1876− put x4

1876+ put x4

1877− put x5

1877+ put x5

1878+ put x6

1878 DoUnify -> putWord8 22

1879 DoUnify -> putWord8 22

1879 CaseTac x1 -> do putWord8 23

1880 CaseTac x1 -> do putWord8 23

1880 put x1

1881 put x1

@@ -1954,7 +1955,8 @@ instance (Binary t) => Binary (PTactic' t) where

1954 x3 <- get

1955 x3 <- get

1955 x4 <- get

1956 x4 <- get

1956 x5 <- get

1957 x5 <- get

1958+ x6 <- get

1957− return (ProofSearch x1 x2 x3 x4 x5)

1959+ return (ProofSearch x1 x2 x3 x4 x5 x6)

1958 22 -> return DoUnify

1960 22 -> return DoUnify

1959 23 -> do x1 <- get

1961 23 -> do x1 <- get

1960 return (CaseTac x1)

1962 return (CaseTac x1)

src/Idris/IdrisDoc.hs+2−2

@@ -360,8 +360,8 @@ extractPTactic (MatchRefine n) = [n]

360extractPTactic (LetTac n p) = n : extract p

361extractPTactic (LetTacTy n p1 p2) = n : concatMap extract [p1, p2]

362extractPTactic (Exact p) = extract p

363−extractPTactic (ProofSearch _ _ _ m ns) | Just n <- m = n : ns

363+extractPTactic (ProofSearch _ _ _ m _ ns) | Just n <- m = n : ns

364−extractPTactic (ProofSearch _ _ _ _ ns) = ns

364+extractPTactic (ProofSearch _ _ _ _ _ ns) = ns

365extractPTactic (Try t1 t2) = concatMap extractPTactic [t1, t2]

366extractPTactic (TSeq t1 t2) = concatMap extractPTactic [t1, t2]

367extractPTactic (ApplyTactic p) = extract p

src/Idris/Interactive.hs+7−6

@@ -213,12 +213,13 @@ doProofSearch fn updatefile rec l n hints (Just depth)

213 [] -> return n

214 ns -> ierror (CantResolveAlts ns)

215 i <- getIState

216+ let (top, envlen, psnames, _)

216− let (top, envlen, _) = case lookup mn (idris_metavars i) of

217+ = case lookup mn (idris_metavars i) of

217− Just (t, e, False) -> (t, e, False)

218+ Just (t, e, ns, False) -> (t, e, ns, False)

218− _ -> (Nothing, 0, True)

219+ _ -> (Nothing, 0, [], True)

219 let fc = fileFC fn

220 let fc = fileFC fn

220− let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))

221+ let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))

221− (ProofSearch rec False depth t hints)]

222+ (ProofSearch rec False depth t psnames hints)]

222 let def = PClause fc mn (PRef fc [] mn) [] (body top) []

223 let def = PClause fc mn (PRef fc [] mn) [] (body top) []

223 newmv <- idrisCatch

224 newmv <- idrisCatch

224 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])

225 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])

@@ -297,7 +298,7 @@ makeLemma fn updatefile l n

297 ns -> ierror (CantResolveAlts (map fst ns))

298 ns -> ierror (CantResolveAlts (map fst ns))

298 i <- getIState

299 i <- getIState

299 margs <- case lookup n (idris_metavars i) of

300 margs <- case lookup n (idris_metavars i) of

300− Just (_, arity, _) -> return arity

301+ Just (_, arity, _, _) -> return arity

301 _ -> return (-1)

302 _ -> return (-1)

302

303

303 if (not isProv) then do

304 if (not isProv) then do

src/Idris/ParseExpr.hs+2−2

@@ -971,7 +971,7 @@ autoImplicit opts st syn

971 sc <- expr syn

972 highlightP kw AnnKeyword

973 return (bindList (PPi

974− (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)

974+ (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)

975

976defaultImplicit opts st syn = do

977 kw <- reservedFC "default"

@@ -1436,7 +1436,7 @@ tactics =

1436 , noArgs ["unify"] DoUnify

1437 , (["search"], Nothing, const $

1438 do depth <- option 10 $ fst <$> natural

1439− return (ProofSearch True True (fromInteger depth) Nothing []))

1439+ return (ProofSearch True True (fromInteger depth) Nothing [] []))

1440 , noArgs ["instance"] TCInstance

1441 , noArgs ["solve"] Solve

1442 , noArgs ["attack"] Attack

src/Idris/ProofSearch.hs+11−9

@@ -22,10 +22,10 @@ import Debug.Trace

22-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

23

24trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

25−trivial = trivialHoles []

25+trivial = trivialHoles [] []

26

27−trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

27+trivialHoles :: [Name] -> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

28−trivialHoles ok elab ist

28+trivialHoles psnames ok elab ist

29 = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

30 return ())

31 (do env <- get_env

@@ -41,7 +41,7 @@ trivialHoles ok elab ist

41 g <- goal

42 -- anywhere but the top is okay for a hole, if holesOK set

43 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

44− holesOK hs (binderTy b)

44+ holesOK hs (binderTy b) && (null psnames || x `elem` psnames)

45 then try' (elab (PRef (fileFC "prf") [] x))

46 (tryAll xs) True

47 else tryAll xs

@@ -73,9 +73,11 @@ proofSearch :: Bool -> -- recursive search (False for 'refine')

73 Bool -> -- ambiguity ok

74 Bool -> -- defer on failure

75 Int -> -- maximum depth

76− (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->

76+ (PTerm -> ElabD ()) -> Maybe Name -> Name ->

77+ [Name] ->

78+ [Name] ->

77 IState -> ElabD ()

79 IState -> ElabD ()

78−proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist

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

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

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

80 -- works

82 -- works

81 let all_imps = lookupCtxtName fn (idris_implicits ist)

83 let all_imps = lookupCtxtName fn (idris_implicits ist)

@@ -106,7 +108,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist

106

108

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

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

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

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

109−proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

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

110 = do compute

112 = do compute

111 ty <- goal

113 ty <- goal

112 hs <- get_holes

114 hs <- get_holes

@@ -177,7 +179,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

177 ty <- goal

179 ty <- goal

178 when (S.member ty tys) $ fail "Been here before"

180 when (S.member ty tys) $ fail "Been here before"

179 let tys' = S.insert ty tys

181 let tys' = S.insert ty tys

180− try' (trivial elab ist)

182+ try' (trivialHoles psnames [] elab ist)

181 (try' (try' (resolveByCon (d - 1) locs tys')

183 (try' (try' (resolveByCon (d - 1) locs tys')

182 (resolveByLocals (d - 1) locs tys')

184 (resolveByLocals (d - 1) locs tys')

183 True)

185 True)

@@ -215,7 +217,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

215

217

216 tryLocals d locs tys [] = fail "Locals failed"

218 tryLocals d locs tys [] = fail "Locals failed"

217 tryLocals d locs tys ((x, t) : xs)

219 tryLocals d locs tys ((x, t) : xs)

218− | x `elem` locs = tryLocals d locs tys xs

220+ | x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs

219 | otherwise = try' (tryLocal d (x : locs) tys x t)

221 | otherwise = try' (tryLocal d (x : locs) tys x t)

220 (tryLocals d locs tys xs) True

222 (tryLocals d locs tys xs) True

221

223

src/Idris/REPL.hs+5−5

@@ -904,8 +904,8 @@ process fn (Check (PRef _ _ n))

904 case lookupNames n ctxt of

905 ts@(t:_) ->

906 case lookup t (idris_metavars ist) of

907− Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

907+ Just (_, i, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

908− showMetavarInfo ppo ist n i

908+ showMetavarInfo ppo ist n i

909 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

910 [] -> iPrintError $ "No such variable " ++ show n

911 where

@@ -1079,7 +1079,7 @@ process fn (RmProof n')

1079 insertMetavar n =

1080 do i <- getIState

1081 let ms = idris_metavars i

1082− putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }

1082+ putIState $ i { idris_metavars = (n, (Nothing, 0, [], False)) : ms }

1083

1084process fn' (AddProof prf)

1085 = do fn <- do

@@ -1132,8 +1132,8 @@ process fn (Prove mode n')

1132 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns

1133 n <- case metavars of

1134 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

1135− [(n, (_,_,False))] -> return n

1135+ [(n, (_,_,_,False))] -> return n

1136− [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

1136+ [(_, (_,_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

1137 ns -> ierror (CantResolveAlts (map fst ns))

1138 prover mode (lit fn) n

1139 -- recheck totality

src/Idris/Reflection.hs+4−4

@@ -76,7 +76,7 @@ reify _ t = fail ("Unknown tactic " ++ show t)

76reifyApp :: IState -> Name -> [Term] -> ElabD PTactic

77reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)

78reifyApp _ t [Constant (I i)]

79− | t == reflm "Search" = return (ProofSearch True True i Nothing [])

79+ | t == reflm "Search" = return (ProofSearch True True i Nothing [] [])

80reifyApp _ t [x]

81 | t == reflm "Refine" = do n <- reifyTTName x

82 return $ Refine n []

@@ -307,7 +307,7 @@ reifyTTBinderApp reif f [x, y]

307reifyTTBinderApp reif f [t]

308 | f == reflm "Hole" = liftM Hole (reif t)

309reifyTTBinderApp reif f [t]

310− | f == reflm "GHole" = liftM (GHole 0) (reif t)

310+ | f == reflm "GHole" = liftM (GHole 0 []) (reif t)

311reifyTTBinderApp reif f [x, y]

312 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)

313reifyTTBinderApp reif f [t]

@@ -580,7 +580,7 @@ reflectBinderQuotePattern q ty unq (Hole t)

580 fill $ reflCall "Hole" [ty, Var t']

581 solve

582 focus t'; q unq t

583−reflectBinderQuotePattern q ty unq (GHole _ t)

583+reflectBinderQuotePattern q ty unq (GHole _ _ t)

584 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

585 fill $ reflCall "GHole" [ty, Var t']

586 solve

@@ -731,7 +731,7 @@ reflectBinderQuote q ty unq (NLet x y)

731 = reflCall "NLet" [Var ty, q unq x, q unq y]

732reflectBinderQuote q ty unq (Hole t)

733 = reflCall "Hole" [Var ty, q unq t]

734−reflectBinderQuote q ty unq (GHole _ t)

734+reflectBinderQuote q ty unq (GHole _ _ t)

735 = reflCall "GHole" [Var ty, q unq t]

736reflectBinderQuote q ty unq (Guess x y)

737 = reflCall "Guess" [Var ty, q unq x, q unq y]

test/interactive003/expected+1

@@ -2,3 +2,4 @@ ys

2x :: app xs ys

3[]

4f x y :: vzipWith f xs ys

5+?word_length_rhs_3 :: word_length xs

test/interactive003/input+1

@@ -2,3 +2,4 @@

2:ps 5 app_rhs_2

3:ps 8 vzipWith_rhs_3

4:ps 9 vzipWith_rhs_1

5+:ps 13 word_length_rhs_2

test/interactive003/interactive003.idr+5

@@ -8,3 +8,8 @@ vzipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

8vzipWith f [] [] = ?vzipWith_rhs_3

9vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_1

10

11+word_length : Vect n String -> Vect n Nat

12+word_length [] = []

13+word_length (x :: xs) = ?word_length_rhs_2

14+

15+