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

src/Idris/AbsSyntax.hs+3−3

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

597597

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

599599addDeferred' :: NameType

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

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

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

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

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

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

606606 -- allowed

607607 -> Idris ()

608608addDeferred' 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

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

611611 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 ++

613613 idris_metavars i }

614614 where

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

src/Idris/AbsSyntaxTree.hs+12−7

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

195195 idris_name :: Int,

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

197197 -- ^ Full application LHS on source line

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

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

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

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

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

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

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

202203 -- allowed

203204 idris_coercions :: [Name],

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

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

404405 | MakeWith Bool Int Name

405406 | MakeCase Bool Int Name

406407 | MakeLemma Bool Int Name

407− | DoProofSearch Bool Bool Int Name [Name]

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

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

408+ | DoProofSearch Bool -- update file

409+ Bool -- recursive search

410+ Int -- depth

411+ Name -- top level name

412+ [Name] -- hints

410413 | SetOpt Opt

411414 | UnsetOpt Opt

412415 | NOP

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

982985 | MatchRefine Name

983986 | LetTac Name t | LetTacTy Name t t

984987 | 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

986991 -- ^ the bool is whether to search recursively

987992 | Solve

988993 | Attack

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

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

15811586 depth d . bracket p startPrec $

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

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

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

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

src/Idris/Completion.hs+1−1

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

5252

5353metavars :: Idris [String]

5454metavars = 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

5656

5757

5858modules :: Idris [String]

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

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

499499 put x2

500500 Hole x1 -> do putWord8 4

501501 put x1

502− GHole x1 x2 -> do putWord8 5

503− put x1

504− put x2

502+ GHole x1 x2 x3 -> do putWord8 5

503+ put x1

504+ put x2

505+ put x3

505506 Guess x1 x2 -> do putWord8 6

506507 put x1

507508 put x2

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

528529 return (Hole x1)

529530 5 -> do x1 <- get

530531 x2 <- get

531− return (GHole x1 x2)

532+ x3 <- get

533+ return (GHole x1 x2 x3)

532534 6 -> do x1 <- get

533535 x2 <- get

534536 return (Guess x1 x2)

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

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

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

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

130130 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` ()

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

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

134134 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

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

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

5353

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+

5468saveState :: Elab' aux ()

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

5670 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

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

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

9595 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

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

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

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

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

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

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

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

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

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

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

4344 context :: Context,

4445 datatypes :: Ctxt TypeInfo,

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

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

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

303304 Nothing [] []

304− [] [] []

305+ [] [] [] []

305306 Nothing ctxt datatypes "" False False [] []

306307

307308type TState = ProofState -- [TacticAction])

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

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

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

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

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

433+ ps <- get

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

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

434436 where

435437 mkTy [] t = t

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

445447 ds = deferred ps in

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

447449 deferred = n : ds })

448− return (Bind n (GHole 0 fty)

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

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

450452 where

451453 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-}

809809 binderVal :: b }

810810 | Hole { binderTy :: !b}

811811 | GHole { envlen :: Int,

812+ localnames :: [Name],

812813 binderTy :: !b}

813814 | Guess { binderTy :: !b,

814815 binderVal :: b }

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

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

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

829830 size (Hole ty) = 1 + size ty

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

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

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

832833 size (PVar ty) = 1 + size ty

833834 size (PVTy ty) = 1 + size ty

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

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

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

841842fmapMB 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)

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

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

845846

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

14941495 -- Render a `Binder` and its name

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

14961497 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

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

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

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

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

15391540

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

15411542 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

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

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

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

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

17391740 ppb p bound n (Hole ty) sc =

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

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

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

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

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

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

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

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

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

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

17931794 text "Hole" <$> pprintRaw bound ty

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

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

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

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

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

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

17981799 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

232232 let tt' = normalise ctxt env tt

233233 lift $ isType ctxt env tt'

234234 return (Hole tv, tt')

235− checkBinder (GHole i t)

235+ checkBinder (GHole i ns t)

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

237237 let tv' = normalise ctxt env tv

238238 let tt' = normalise ctxt env tt

239239 lift $ isType ctxt env tt'

240− return (GHole i tv, tt')

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

241241 checkBinder (Guess t v)

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

243243 | otherwise

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

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

274274 discharge n (Hole t) bt scv sct

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

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

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

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

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

278278 discharge n (Guess t v) bt scv sct

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

280280 discharge n (PVar t) bt scv sct

src/Idris/DeepSeq.hs+2−2

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

295295 rnf Compute = ()

296296 rnf Trivial = ()

297297 rnf TCInstance = ()

298− rnf (ProofSearch r r1 r2 x1 x2)

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

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

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

300300 rnf Solve = ()

301301 rnf Attack = ()

302302 rnf ProofState = ()

src/Idris/Delaborate.hs+2−2

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

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

107107 | otherwise

108108 = case lookup n (idris_metavars ist) of

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

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

110110 _ -> PRef un [] n

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

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

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

170170 deFn env (P _ n _) args

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

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

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

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

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

175175 | 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

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

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

634634 (do pbinds ist lhs_tm

635+ -- proof search can use explicitly written names

636+ mapM_ addPSname (allNamesIn lhs_in)

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

636638 setNextName

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

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

656658 logLvl 5 "DONE CHECK"

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

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

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

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

660662 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'

662664 addDeferred def''

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

664666

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

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

817819 (bindTyArgs PVTy bargs infP) initEState

818820 (do pbinds i lhs_tm

821+ -- proof search can use explicitly written names

822+ mapM_ addPSname (allNamesIn lhs_in)

819823 setNextName

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

821825 (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)

828832 sendHighlighting highlights

829833

830834 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'

832836 addDeferred def''

833837 mapM_ (elabCaseBlock info opts) is

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

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

890894 addIBC (IBCImp wname)

891895 addIBC (IBCStatic wname)

892896

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

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

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

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

895899 addDeferred def''

896900

897901 -- in the subdecls, lhs becomes:

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

932936 sendHighlighting highlights

933937

934938 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'

936940 addDeferred def''

937941 mapM_ (elabCaseBlock info opts) is

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

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

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

4141

4242data ElabResult =

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

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

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

4545 -- ^ Information about new metavariables

4646 , resultCaseDecls :: [PDecl]

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

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

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

628628 checkPiGoal n

629629 attack; intro (Just n);

630+ addPSname n -- okay for proof search

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

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

632633 highlightSource nfc (AnnBoundName n False)

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

643644 ptm <- get_term

644645 hs <- get_holes

645646 introTy (Var tyn) (Just n)

647+ addPSname n -- okay for proof search

646648 focus tyn

647649

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

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

651653 highlightSource nfc (AnnBoundName n False)

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

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

656+ addPSname n -- okay for proof search

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

655658 solve

656659 highlightSource nfc (AnnBoundName n False)

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

661664 MN _ _ -> unique_hole n

662665 _ -> return n

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

667+ addPSname n' -- okay for proof search

664668 focus tyn

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

666670 elabE ec' fc ty

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

676680 claim valn (Var tyn)

677681 explicit valn

678682 letbind n (Var tyn) (Var valn)

683+ addPSname n

679684 case ty of

680685 Placeholder -> return ()

681686 _ -> do focus tyn

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

961966 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

962967 let n' = metavarName (namespace info) n

963968 attack

969+ psns <- getPSnames

964970 defer unique_used n'

965971 solve

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

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

16201626 g <- goal

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

16221628 when (not isg) $

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

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

16241630

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

16261632solveAutos ist fn ambigok

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

16291635

16301636trivial' ist

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

1632−trivialHoles' h ist

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

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

1638+trivialHoles' psn h ist

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

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

16351641 = do unifyProblems

16361642 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

16381644

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

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

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

16741680 _ -> []

16751681

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

1677− try' (trivialHoles' okholes ist)

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

16781684 (do addDefault t tc ttypes

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

16801686 let insts = findInstances ist t

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

17991805 isImp arg = (False, priority arg)

18001806

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

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

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

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

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

18041810 do ds <- get

18051811 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))])

18071813 collectDeferred top casenames ctxt app

18081814 where

18091815 -- 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

21182124 do actualHints <- mapM reifyTTName hs

21192125 unifyProblems

21202126 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

21222128 returnUnit

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

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

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

22902296 runT Compute = compute

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

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

2293− runT (ProofSearch rec prover depth top hints)

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

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

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

22952301 when autoSolve solveAll

22962302 runT (Focus n) = focus n

22972303 runT Unfocus = do hs <- get_holes

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

24992505 updateIState $ \i -> i { idris_implicits =

25002506 addDef n impls (idris_implicits i) }

25012507 addIBC (IBCImp n)

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

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

25032509 addIBC (IBCDef n)

25042510 ctxt <- getContext

25052511 case lookupDef n ctxt of

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

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

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

25102516 -- 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

25122518 in addDeferred ds'

25132519 _ -> return ()

25142520 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

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

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

161161 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, []))]

163163 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

165165 addDeferred ds'

166166 setFlags n opts'

167167 checkDocs fc argDocs ty

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

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

4040iderr :: Name -> Err -> Err

4141iderr _ e = e

4242

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

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

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

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

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

4646

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

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

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

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

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

5050checkAddDef 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)

5252 = do ctxt <- getContext

5353 (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))]

5555 addIBC (IBCDef n)

5656 ns' <- checkAddDef add toplvl fc mkerr ns

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

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

5858

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

6060-- type

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

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

7676 let vtm = orderPats (getInferTerm tm')

7777

7878 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'

8080 addDeferred def''

8181 mapM_ (elabCaseBlock info []) is

8282

src/Idris/IBC.hs+12−10

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 116

43+ibcVersion = 117

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

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

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

7979 ibc_errorhandlers :: ![Name],

8080 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))],

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

8383 ibc_postulates :: ![Name],

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

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

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

611611 addFunctionErrorHandlers fn arg [handler]) ns

612612

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

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

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

615615

616616----- For Cheapskate and docstrings

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

18691869 put x1

18701870 ByReflection x1 -> do putWord8 20

18711871 put x1

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

1873− put x1

1874− put x2

1875− put x3

1876− put x4

1877− put x5

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

1873+ put x1

1874+ put x2

1875+ put x3

1876+ put x4

1877+ put x5

1878+ put x6

18781879 DoUnify -> putWord8 22

18791880 CaseTac x1 -> do putWord8 23

18801881 put x1

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

19541955 x3 <- get

19551956 x4 <- get

19561957 x5 <- get

1957− return (ProofSearch x1 x2 x3 x4 x5)

1958+ x6 <- get

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

19581960 22 -> return DoUnify

19591961 23 -> do x1 <- get

19601962 return (CaseTac x1)

src/Idris/IdrisDoc.hs+2−2

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

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

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

362362extractPTactic (Exact p) = extract p

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

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

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

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

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

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

367367extractPTactic (ApplyTactic p) = extract p

src/Idris/Interactive.hs+7−6

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

213213 [] -> return n

214214 ns -> ierror (CantResolveAlts ns)

215215 i <- getIState

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

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

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

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

217+ = case lookup mn (idris_metavars i) of

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

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

219220 let fc = fileFC fn

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

221− (ProofSearch rec False depth t hints)]

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

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

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

223224 newmv <- idrisCatch

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

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

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

298299 i <- getIState

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

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

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

301302 _ -> return (-1)

302303

303304 if (not isProv) then do

src/Idris/ParseExpr.hs+2−2

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

971971 sc <- expr syn

972972 highlightP kw AnnKeyword

973973 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)

975975

976976defaultImplicit opts st syn = do

977977 kw <- reservedFC "default"

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

14361436 , noArgs ["unify"] DoUnify

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

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

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

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

14401440 , noArgs ["instance"] TCInstance

14411441 , noArgs ["solve"] Solve

14421442 , noArgs ["attack"] Attack

src/Idris/ProofSearch.hs+11−9

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

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

2323

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

25−trivial = trivialHoles []

25+trivial = trivialHoles [] []

2626

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

28−trivialHoles ok elab ist

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

28+trivialHoles psnames ok elab ist

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

3030 return ())

3131 (do env <- get_env

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

4141 g <- goal

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

4343 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)

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

4646 (tryAll xs) True

4747 else tryAll xs

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

7373 Bool -> -- ambiguity ok

7474 Bool -> -- defer on failure

7575 Int -> -- maximum depth

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

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

77+ [Name] ->

78+ [Name] ->

7779 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

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

8082 -- works

8183 let all_imps = lookupCtxtName fn (idris_implicits ist)

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

106108

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

108110 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

110112 = do compute

111113 ty <- goal

112114 hs <- get_holes

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

177179 ty <- goal

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

179181 let tys' = S.insert ty tys

180− try' (trivial elab ist)

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

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

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

183185 True)

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

215217

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

217219 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

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

220222 (tryLocals d locs tys xs) True

221223

src/Idris/REPL.hs+5−5

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

904904 case lookupNames n ctxt of

905905 ts@(t:_) ->

906906 case lookup t (idris_metavars ist) of

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

908− showMetavarInfo ppo ist n i

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

908+ showMetavarInfo ppo ist n i

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

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

911911 where

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

10791079 insertMetavar n =

10801080 do i <- getIState

10811081 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 }

10831083

10841084process fn' (AddProof prf)

10851085 = do fn <- do

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

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

11331133 n <- case metavars of

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

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

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

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

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

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

11381138 prover mode (lit fn) n

11391139 -- recheck totality

src/Idris/Reflection.hs+4−4

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

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

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

7878reifyApp _ t [Constant (I i)]

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

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

8080reifyApp _ t [x]

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

8282 return $ Refine n []

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

307307reifyTTBinderApp reif f [t]

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

309309reifyTTBinderApp reif f [t]

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

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

311311reifyTTBinderApp reif f [x, y]

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

313313reifyTTBinderApp reif f [t]

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

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

581581 solve

582582 focus t'; q unq t

583−reflectBinderQuotePattern q ty unq (GHole _ t)

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

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

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

586586 solve

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

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

732732reflectBinderQuote q ty unq (Hole t)

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

734−reflectBinderQuote q ty unq (GHole _ t)

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

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

736736reflectBinderQuote q ty unq (Guess x y)

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

test/interactive003/expected+1

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

22x :: app xs ys

33[]

44f x y :: vzipWith f xs ys

5+?word_length_rhs_3 :: word_length xs

test/interactive003/input+1

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

22:ps 5 app_rhs_2

33:ps 8 vzipWith_rhs_3

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

88vzipWith f [] [] = ?vzipWith_rhs_3

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

1010

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

12+word_length [] = []

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

14+

15+