From 7095d6c1edb3d520e8a00e8a7f1408999fa39155 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 1 Aug 2015 21:12:14 +0100 Subject: [PATCH] Proof search should only use user visible names If they are implicits or class arguments, it's fine for 'auto' to see them since they're only used internally, but interactive proof search will give odd results if it uses them. So, we make a list of names which proof search in interactive mode is allowed to use. --- src/Idris/AbsSyntax.hs | 6 ++--- src/Idris/AbsSyntaxTree.hs | 19 +++++++++----- src/Idris/Completion.hs | 2 +- src/Idris/Core/Binary.hs | 10 ++++--- src/Idris/Core/DeepSeq.hs | 2 +- src/Idris/Core/Elaborate.hs | 14 ++++++++++ src/Idris/Core/Execute.hs | 2 +- src/Idris/Core/ProofState.hs | 8 +++--- src/Idris/Core/TT.hs | 15 ++++++----- src/Idris/Core/Typecheck.hs | 8 +++--- src/Idris/DeepSeq.hs | 4 +-- src/Idris/Delaborate.hs | 4 +-- src/Idris/Elab/Clause.hs | 16 +++++++----- src/Idris/Elab/Term.hs | 36 +++++++++++++++----------- src/Idris/Elab/Type.hs | 4 +-- src/Idris/Elab/Utils.hs | 14 +++++----- src/Idris/Elab/Value.hs | 2 +- src/Idris/IBC.hs | 22 +++++++++------- src/Idris/IdrisDoc.hs | 4 +-- src/Idris/Interactive.hs | 13 +++++----- src/Idris/ParseExpr.hs | 4 +-- src/Idris/ProofSearch.hs | 20 +++++++------- src/Idris/REPL.hs | 10 +++---- src/Idris/Reflection.hs | 8 +++--- test/interactive003/expected | 1 + test/interactive003/input | 1 + test/interactive003/interactive003.idr | 5 ++++ 27 files changed, 150 insertions(+), 104 deletions(-) diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs index 033a7c732..df9daf5f8 100644 --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -597,7 +597,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0) -- | Save information about a name that is not yet defined addDeferred' :: NameType - -> [(Name, (Int, Maybe Name, Type, Bool))] + -> [(Name, (Int, Maybe Name, Type, [Name], Bool))] -- ^ The Name is the name being made into a metavar, -- the Int is the number of vars that are part of a -- putative proof context, the Maybe Name is the @@ -606,10 +606,10 @@ addDeferred' :: NameType -- allowed -> Idris () addDeferred' nt ns - = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns + = do mapM_ (\(n, (i, _, t, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns i <- getIState - putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++ + putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel)) -> (n, (top, i, ns, isTopLevel))) ns ++ idris_metavars i } where -- 'tidyNames' is to generate user accessible names in case they are diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs index 317aa9b6d..a6c91f76e 100644 --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -195,10 +195,11 @@ data IState = IState { idris_name :: Int, idris_lineapps :: [((FilePath, Int), PTerm)], -- ^ Full application LHS on source line - idris_metavars :: [(Name, (Maybe Name, Int, Bool))], + idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool))], -- ^ The currently defined but not proven metavariables. The Int -- is the number of vars to display as a context, the Maybe Name - -- is its top-level function, and the Bool is whether :p is + -- is its top-level function, the [Name] is the list of local variables + -- available for proof search and the Bool is whether :p is -- allowed idris_coercions :: [Name], idris_errRev :: [(Term, Term)], @@ -404,9 +405,11 @@ data Command = Quit | MakeWith Bool Int Name | MakeCase Bool Int Name | MakeLemma Bool Int Name - | DoProofSearch Bool Bool Int Name [Name] - -- ^ the first bool is whether to update, - -- the second is whether to search recursively (i.e. for the arguments) + | DoProofSearch Bool -- update file + Bool -- recursive search + Int -- depth + Name -- top level name + [Name] -- hints | SetOpt Opt | UnsetOpt Opt | NOP @@ -982,7 +985,9 @@ data PTactic' t = Intro [Name] | Intros | Focus Name | MatchRefine Name | LetTac Name t | LetTacTy Name t t | Exact t | Compute | Trivial | TCInstance - | ProofSearch Bool Bool Int (Maybe Name) [Name] + | ProofSearch Bool Bool Int (Maybe Name) + [Name] -- allowed local names + [Name] -- hints -- ^ the bool is whether to search recursively | Solve | Attack @@ -1580,7 +1585,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) = depth d . bracket p startPrec $ prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" prettySe (decD d) startPrec ((n, True):bnd) sc - prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) = + prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) = lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+> text "->" prettySe (decD d) startPrec ((n, True):bnd) sc prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) = diff --git a/src/Idris/Completion.hs b/src/Idris/Completion.hs index e5c668037..fee9821cc 100644 --- a/src/Idris/Completion.hs +++ b/src/Idris/Completion.hs @@ -52,7 +52,7 @@ names = do i <- get metavars :: Idris [String] metavars = do i <- get - return . map (show . nsroot) $ map fst (filter (\(_, (_,_,t)) -> not t) (idris_metavars i)) \\ primDefs + return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t)) -> not t) (idris_metavars i)) \\ primDefs modules :: Idris [String] diff --git a/src/Idris/Core/Binary.hs b/src/Idris/Core/Binary.hs index fe8da7794..f0a834f8a 100644 --- a/src/Idris/Core/Binary.hs +++ b/src/Idris/Core/Binary.hs @@ -499,9 +499,10 @@ instance (Binary b) => Binary (Binder b) where put x2 Hole x1 -> do putWord8 4 put x1 - GHole x1 x2 -> do putWord8 5 - put x1 - put x2 + GHole x1 x2 x3 -> do putWord8 5 + put x1 + put x2 + put x3 Guess x1 x2 -> do putWord8 6 put x1 put x2 @@ -528,7 +529,8 @@ instance (Binary b) => Binary (Binder b) where return (Hole x1) 5 -> do x1 <- get x2 <- get - return (GHole x1 x2) + x3 <- get + return (GHole x1 x2 x3) 6 -> do x1 <- get x2 <- get return (Guess x1 x2) diff --git a/src/Idris/Core/DeepSeq.hs b/src/Idris/Core/DeepSeq.hs index 72789b858..fc0f8c1b9 100644 --- a/src/Idris/Core/DeepSeq.hs +++ b/src/Idris/Core/DeepSeq.hs @@ -128,7 +128,7 @@ instance (NFData b) => NFData (Binder b) where rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` () rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` () rnf (Hole x1) = rnf x1 `seq` () - rnf (GHole x1 x2) = rnf x1 `seq` rnf x2 `seq` () + rnf (GHole x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` () rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` () rnf (PVar x1) = rnf x1 `seq` () rnf (PVTy x1) = rnf x1 `seq` () diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs index 6595c3da1..a8d6abde2 100644 --- a/src/Idris/Core/Elaborate.hs +++ b/src/Idris/Core/Elaborate.hs @@ -51,6 +51,20 @@ explicit n = do ES (p, a) s m <- get let p' = p { dontunify = n : dontunify p } put (ES (p', a) s m) +-- Add a name that's okay to use in proof search (typically either because +-- it was given explicitly on the lhs, or intrduced as an explicit lambda +-- or let binding) +addPSname :: Name -> Elab' aux () +addPSname n@(UN _) + = do ES (p, a) s m <- get + let p' = p { psnames = n : psnames p } + put (ES (p', a) s m) +addPSname _ = return () -- can only use user given names + +getPSnames :: Elab' aux [Name] +getPSnames = do ES (p, a) s m <- get + return (psnames p) + saveState :: Elab' aux () saveState = do e@(ES p s _) <- get put (ES p s (Just e)) diff --git a/src/Idris/Core/Execute.hs b/src/Idris/Core/Execute.hs index 46f9233b7..57b08e23a 100644 --- a/src/Idris/Core/Execute.hs +++ b/src/Idris/Core/Execute.hs @@ -93,7 +93,7 @@ toTT (EBind n b body) = do n' <- newN n fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2 fixBinder (Hole t) = Hole <$> toTT t - fixBinder (GHole i t) = GHole i <$> toTT t + fixBinder (GHole i ns t) = GHole i ns <$> toTT t fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2 fixBinder (PVar t) = PVar <$> toTT t fixBinder (PVTy t) = PVTy <$> toTT t diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs index bcdfe46ce..215cb79f5 100644 --- a/src/Idris/Core/ProofState.hs +++ b/src/Idris/Core/ProofState.hs @@ -39,6 +39,7 @@ data ProofState = PS { thname :: Name, deferred :: [Name], -- ^ names we'll need to define instances :: [Name], -- ^ instance arguments (for type classes) autos :: [(Name, [Name])], -- ^ unsolved 'auto' implicits with their holes + psnames :: [Name], -- ^ Local names okay to use in proof search previous :: Maybe ProofState, -- ^ for undo context :: Context, datatypes :: Ctxt TypeInfo, @@ -301,7 +302,7 @@ newProof n ctxt datatypes ty = in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty') (P Bound h ty'))) ty [] (h, []) [] [] Nothing [] [] - [] [] [] + [] [] [] [] Nothing ctxt datatypes "" False False [] [] type TState = ProofState -- [TacticAction]) @@ -429,7 +430,8 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' = do let env' = filter (\(n, t) -> n `notElem` dropped) env action (\ps -> let hs = holes ps in ps { holes = hs \\ [x] }) - return (Bind n (GHole (length env') (mkTy (reverse env') t)) + ps <- get + return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t)) (mkApp (P Ref n ty) (map getP (reverse env')))) where mkTy [] t = t @@ -445,7 +447,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' = ds = deferred ps in ps { holes = hs \\ [x], deferred = n : ds }) - return (Bind n (GHole 0 fty) + return (Bind n (GHole 0 [] fty) (mkApp (P Ref n ty) (map getP args))) where getP n = case lookup n env of diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs index be044f319..1255c6c81 100644 --- a/src/Idris/Core/TT.hs +++ b/src/Idris/Core/TT.hs @@ -809,6 +809,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-} binderVal :: b } | Hole { binderTy :: !b} | GHole { envlen :: Int, + localnames :: [Name], binderTy :: !b} | Guess { binderTy :: !b, binderVal :: b } @@ -827,7 +828,7 @@ instance Sized a => Sized (Binder a) where size (Let ty val) = 1 + size ty + size val size (NLet ty val) = 1 + size ty + size val size (Hole ty) = 1 + size ty - size (GHole _ ty) = 1 + size ty + size (GHole _ _ ty) = 1 + size ty size (Guess ty val) = 1 + size ty + size val size (PVar ty) = 1 + size ty size (PVTy ty) = 1 + size ty @@ -839,7 +840,7 @@ fmapMB f (Guess t v) = liftM2 Guess (f t) (f v) fmapMB f (Lam t) = liftM Lam (f t) fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k) fmapMB f (Hole t) = liftM Hole (f t) -fmapMB f (GHole i t) = liftM (GHole i) (f t) +fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t) fmapMB f (PVar t) = liftM PVar (f t) fmapMB f (PVTy t) = liftM PVTy (f t) @@ -1494,7 +1495,7 @@ prettyEnv env t = prettyEnv' env t False -- Render a `Binder` and its name prettySb env n (Lam t) = prettyB env "λ" "=>" n t prettySb env n (Hole t) = prettyB env "?defer" "." n t - prettySb env n (GHole _ t) = prettyB env "?gdefer" "." n t + prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t prettySb env n (PVar t) = prettyB env "pat" "." n t prettySb env n (PVTy t) = prettyB env "pty" "." n t @@ -1539,7 +1540,7 @@ showEnv' env t dbg = se 10 env t where sb env n (Lam t) = showb env "\\ " " => " n t sb env n (Hole t) = showb env "? " ". " n t - sb env n (GHole i t) = showb env "?defer " ". " n t + sb env n (GHole i ns t) = showb env "?defer " ". " n t sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t sb env n (Pi _ t _) = showb env "(" ") -> " n t sb env n (PVar t) = showb env "pat " ". " n t @@ -1739,7 +1740,7 @@ pprintTT bound tm = pp startPrec bound tm ppb p bound n (Hole ty) sc = bracket p startPrec . group . align . hang 2 $ text "?" <+> bindingOf n False <+> text "." <> line <> sc - ppb p bound n (GHole _ ty) sc = + ppb p bound n (GHole _ _ ty) sc = bracket p startPrec . group . align . hang 2 $ text "¿" <+> bindingOf n False <+> text "." <> line <> sc ppb p bound n (Guess ty val) sc = @@ -1791,8 +1792,8 @@ pprintRaw bound (RBind n b body) = vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v] ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $ text "Hole" <$> pprintRaw bound ty - ppb (GHole _ ty) = enclose lparen rparen . group . align . hang 2 $ - text "GHole" <$> pprintRaw bound ty + ppb (GHole _ _ ty) = enclose lparen rparen . group . align . hang 2 $ + text "GHole" <$> pprintRaw bound ty ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $ vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v] ppb (PVar ty) = enclose lparen rparen . group . align . hang 2 $ diff --git a/src/Idris/Core/Typecheck.hs b/src/Idris/Core/Typecheck.hs index 5106cb59a..b2d8ce8e6 100644 --- a/src/Idris/Core/Typecheck.hs +++ b/src/Idris/Core/Typecheck.hs @@ -232,12 +232,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where let tt' = normalise ctxt env tt lift $ isType ctxt env tt' return (Hole tv, tt') - checkBinder (GHole i t) + checkBinder (GHole i ns t) = do (tv, tt) <- chk u env t let tv' = normalise ctxt env tv let tt' = normalise ctxt env tt lift $ isType ctxt env tt' - return (GHole i tv, tt') + return (GHole i ns tv, tt') checkBinder (Guess t v) | not holes = lift $ tfail (IncompleteTerm undefined) | otherwise @@ -273,8 +273,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where = return (Bind n (NLet t v) scv, Bind n (Let t v) sct) discharge n (Hole t) bt scv sct = return (Bind n (Hole t) scv, sct) - discharge n (GHole i t) bt scv sct - = return (Bind n (GHole i t) scv, sct) + discharge n (GHole i ns t) bt scv sct + = return (Bind n (GHole i ns t) scv, sct) discharge n (Guess t v) bt scv sct = return (Bind n (Guess t v) scv, sct) discharge n (PVar t) bt scv sct diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs index b5f398420..b2a5dbed1 100644 --- a/src/Idris/DeepSeq.hs +++ b/src/Idris/DeepSeq.hs @@ -295,8 +295,8 @@ instance (NFData t) => NFData (PTactic' t) where rnf Compute = () rnf Trivial = () rnf TCInstance = () - rnf (ProofSearch r r1 r2 x1 x2) - = rnf x1 `seq` rnf x2 `seq` () + rnf (ProofSearch r r1 r2 x1 x2 x3) + = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` () rnf Solve = () rnf Attack = () rnf ProofState = () diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs index 80bad709e..ef413820e 100644 --- a/src/Idris/Delaborate.hs +++ b/src/Idris/Delaborate.hs @@ -106,7 +106,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm | Just n' <- lookup n env = PRef un [] n' | otherwise = case lookup n (idris_metavars ist) of - Just (Just _, mi, _) -> mkMVApp n [] + Just (Just _, mi, _, _) -> mkMVApp n [] _ -> PRef un [] n de env _ (Bind n (Lam ty) sc) = 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 = PApp un (de env [] f) (map pexp (map (de env []) args)) deFn env (P _ n _) args | not mvs = case lookup n (idris_metavars ist) of - Just (Just _, mi, _) -> + Just (Just _, mi, _, _) -> mkMVApp n (drop mi (map (de env []) args)) _ -> mkPApp n (map (de env []) args) | otherwise = mkPApp n (map (de env []) args) diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs index 58dbf0293..b95d5f170 100644 --- a/src/Idris/Elab/Clause.hs +++ b/src/Idris/Elab/Clause.hs @@ -632,6 +632,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc ((rhs', defer, is, probs, ctxt', newDecls, highlights), _) <- tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState (do pbinds ist lhs_tm + -- proof search can use explicitly written names + mapM_ addPSname (allNamesIn lhs_in) mapM_ setinj (nub (params ++ inj)) setNextName (ElabResult _ _ is ctxt' newDecls highlights) <- @@ -656,9 +658,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc logLvl 5 "DONE CHECK" logLvl 4 $ "---> " ++ show rhs' when (not (null defer)) $ logLvl 1 $ "DEFERRED " ++ - show (map (\ (n, (_,_,t)) -> (n, t)) defer) + show (map (\ (n, (_,_,t,_)) -> (n, t)) defer) def' <- checkDef fc (Elaborating "deferred type of ") defer - let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def' + let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def' addDeferred def'' mapM_ (\(n, _) -> addIBC (IBCDef n)) def'' @@ -816,6 +818,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock) tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS") (bindTyArgs PVTy bargs infP) initEState (do pbinds i lhs_tm + -- proof search can use explicitly written names + mapM_ addPSname (allNamesIn lhs_in) setNextName -- TODO: may want where here - see winfo abpve (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) sendHighlighting highlights def' <- checkDef fc iderr defer - let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def' + let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def' addDeferred def'' mapM_ (elabCaseBlock info opts) is logLvl 5 ("Checked wval " ++ show wval') @@ -890,8 +894,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock) addIBC (IBCImp wname) addIBC (IBCStatic wname) - def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))] - let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def' + def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype, []))] + let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def' addDeferred def'' -- in the subdecls, lhs becomes: @@ -932,7 +936,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock) sendHighlighting highlights def' <- checkDef fc iderr defer - let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def' + let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False))) def' addDeferred def'' mapM_ (elabCaseBlock info opts) is logLvl 5 ("Checked RHS " ++ show rhs') diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs index 7d4ee8a0f..cd3088571 100644 --- a/src/Idris/Elab/Term.hs +++ b/src/Idris/Elab/Term.hs @@ -41,7 +41,7 @@ data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS data ElabResult = ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration - , resultMetavars :: [(Name, (Int, Maybe Name, Type))] + , resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))] -- ^ Information about new metavariables , resultCaseDecls :: [PDecl] -- ^ Deferred declarations as the meaning of case blocks @@ -627,6 +627,7 @@ elab ist info emode opts fn tm lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here") checkPiGoal n attack; intro (Just n); + addPSname n -- okay for proof search -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm) elabE (ina { e_inarg = True } ) (Just fc) sc; solve highlightSource nfc (AnnBoundName n False) @@ -643,6 +644,7 @@ elab ist info emode opts fn tm ptm <- get_term hs <- get_holes introTy (Var tyn) (Just n) + addPSname n -- okay for proof search focus tyn elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty @@ -651,6 +653,7 @@ elab ist info emode opts fn tm highlightSource nfc (AnnBoundName n False) elab' ina fc (PPi p n nfc Placeholder sc) = do attack; arg n (is_scoped p) (sMN 0 "ty") + addPSname n -- okay for proof search elabE (ina { e_inarg = True, e_intype = True }) fc sc solve highlightSource nfc (AnnBoundName n False) @@ -661,6 +664,7 @@ elab ist info emode opts fn tm MN _ _ -> unique_hole n _ -> return n forall n' (is_scoped p) (Var tyn) + addPSname n' -- okay for proof search focus tyn let ec' = ina { e_inarg = True, e_intype = True } elabE ec' fc ty @@ -676,6 +680,7 @@ elab ist info emode opts fn tm claim valn (Var tyn) explicit valn letbind n (Var tyn) (Var valn) + addPSname n case ty of Placeholder -> return () _ -> do focus tyn @@ -961,6 +966,7 @@ elab ist info emode opts fn tm let unique_used = getUniqueUsed (tt_ctxt ist) ptm let n' = metavarName (namespace info) n attack + psns <- getPSnames defer unique_used n' solve highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing) @@ -1620,7 +1626,7 @@ solveAuto ist fn ambigok n g <- goal isg <- is_guess -- if it's a guess, we're working on it recursively, so stop when (not isg) $ - proofSearch' ist True ambigok 100 True Nothing fn [] + proofSearch' ist True ambigok 100 True Nothing fn [] [] solveAutos :: IState -> Name -> Bool -> ElabD () solveAutos ist fn ambigok @@ -1629,12 +1635,12 @@ solveAutos ist fn ambigok trivial' ist = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist -trivialHoles' h ist - = trivialHoles h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist -proofSearch' ist rec ambigok depth prv top n hints +trivialHoles' psn h ist + = trivialHoles psn h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist +proofSearch' ist rec ambigok depth prv top n psns hints = do unifyProblems proofSearch rec prv ambigok (not prv) depth - (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist + (elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist -- | Resolve type classes. This will only pick up 'normal' instances, never -- named instances (which is enforced by 'findInstances'). @@ -1674,7 +1680,7 @@ resTC' tcs defaultOn topholes depth topg fn ist _ -> [] traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $ - try' (trivialHoles' okholes ist) + try' (trivialHoles' [] okholes ist) (do addDefault t tc ttypes let stk = map fst (filter snd $ elab_stack ist) let insts = findInstances ist t @@ -1799,11 +1805,11 @@ resTC' tcs defaultOn topholes depth topg fn ist isImp arg = (False, priority arg) collectDeferred :: Maybe Name -> [Name] -> Context -> - Term -> State [(Name, (Int, Maybe Name, Type))] Term -collectDeferred top casenames ctxt (Bind n (GHole i t) app) = + Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term +collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) = do ds <- get t' <- collectDeferred top casenames ctxt t - when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t'))]) + when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))]) collectDeferred top casenames ctxt app where -- 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 do actualHints <- mapM reifyTTName hs unifyProblems let psElab = elab ist toplevel ERHS [] (sMN 0 "tac") - proofSearch True True False False i psElab Nothing (sMN 0 "search ") actualHints ist + proofSearch True True False False i psElab Nothing (sMN 0 "search ") [] actualHints ist returnUnit (Constant (I _), Nothing ) -> lift . tfail . InternalMsg $ "Not a list: " ++ show hints' @@ -2290,8 +2296,8 @@ runTac autoSolve ist perhapsFC fn tac runT Compute = compute runT Trivial = do trivial' ist; when autoSolve solveAll runT TCInstance = runT (Exact (PResolveTC emptyFC)) - runT (ProofSearch rec prover depth top hints) - = do proofSearch' ist rec False depth prover top fn hints + runT (ProofSearch rec prover depth top psns hints) + = do proofSearch' ist rec False depth prover top fn psns hints when autoSolve solveAll runT (Focus n) = focus n runT Unfocus = do hs <- get_holes @@ -2499,7 +2505,7 @@ processTacticDecls info steps = updateIState $ \i -> i { idris_implicits = addDef n impls (idris_implicits i) } addIBC (IBCImp n) - ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))] + ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty, []))] addIBC (IBCDef n) ctxt <- getContext case lookupDef n ctxt of @@ -2508,7 +2514,7 @@ processTacticDecls info steps = -- then it must be added as a metavariable. This needs guarding -- to prevent overwriting case defs with a metavar, if the case -- defs come after the type decl in the same script! - let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds + let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) ds in addDeferred ds' _ -> return () RAddInstance className instName -> diff --git a/src/Idris/Elab/Type.hs b/src/Idris/Elab/Type.hs index ec510cf7c..7f873f2a3 100644 --- a/src/Idris/Elab/Type.hs +++ b/src/Idris/Elab/Type.hs @@ -159,9 +159,9 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par -- Productivity checking now via checking for guarded 'Delay' let opts' = opts -- if corec then (Coinductive : opts) else opts let usety = if norm then nty' else nty - ds <- checkDef fc iderr [(n, (-1, Nothing, usety))] + ds <- checkDef fc iderr [(n, (-1, Nothing, usety, []))] addIBC (IBCDef n) - let ds' = map (\(n, (i, top, fam)) -> (n, (i, top, fam, True))) ds + let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True))) ds addDeferred ds' setFlags n opts' checkDocs fc argDocs ty diff --git a/src/Idris/Elab/Utils.hs b/src/Idris/Elab/Utils.hs index 8d7596e26..8e62a21b0 100644 --- a/src/Idris/Elab/Utils.hs +++ b/src/Idris/Elab/Utils.hs @@ -40,21 +40,21 @@ recheckC_borrowing uniq_check bs fc mkerr env t iderr :: Name -> Err -> Err iderr _ e = e -checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))] - -> Idris [(Name, (Int, Maybe Name, Type))] +checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type, [Name]))] + -> Idris [(Name, (Int, Maybe Name, Type, [Name]))] checkDef fc mkerr ns = checkAddDef False True fc mkerr ns checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err) - -> [(Name, (Int, Maybe Name, Type))] - -> Idris [(Name, (Int, Maybe Name, Type))] + -> [(Name, (Int, Maybe Name, Type, [Name]))] + -> Idris [(Name, (Int, Maybe Name, Type, [Name]))] checkAddDef add toplvl fc mkerr [] = return [] -checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns) +checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns) = do ctxt <- getContext (t', _) <- recheckC fc (mkerr n) [] t - when add $ do addDeferred [(n, (i, top, t, toplvl))] + when add $ do addDeferred [(n, (i, top, t, psns, toplvl))] addIBC (IBCDef n) ns' <- checkAddDef add toplvl fc mkerr ns - return ((n, (i, top, t')) : ns') + return ((n, (i, top, t', psns)) : ns') -- | Get the list of (index, name) of inaccessible arguments from an elaborated -- type diff --git a/src/Idris/Elab/Value.hs b/src/Idris/Elab/Value.hs index e39247f5f..eb5e8423c 100644 --- a/src/Idris/Elab/Value.hs +++ b/src/Idris/Elab/Value.hs @@ -76,7 +76,7 @@ elabValBind info aspat norm tm_in let vtm = orderPats (getInferTerm tm') def' <- checkDef (fileFC "(input)") iderr defer - let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def' + let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True))) def' addDeferred def'' mapM_ (elabCaseBlock info []) is diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs index ffbf5ecb9..beb7734f4 100644 --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -40,7 +40,7 @@ import System.Directory import Codec.Archive.Zip ibcVersion :: Word16 -ibcVersion = 116 +ibcVersion = 117 data IBCFile = IBCFile { ver :: Word16, sourcefile :: FilePath, @@ -78,7 +78,7 @@ data IBCFile = IBCFile { ver :: Word16, ibc_metainformation :: ![(Name, MetaInformation)], ibc_errorhandlers :: ![Name], ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler - ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))], + ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool))], ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))], ibc_postulates :: ![Name], ibc_externs :: ![(Name, Int)], @@ -610,7 +610,7 @@ pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris () pFunctionErrorHandlers ns = mapM_ (\ (fn,arg,handler) -> addFunctionErrorHandlers fn arg [handler]) ns -pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris () +pMetavars :: [(Name, (Maybe Name, Int, [Name], Bool))] -> Idris () pMetavars ns = updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i }) ----- For Cheapskate and docstrings @@ -1869,12 +1869,13 @@ instance (Binary t) => Binary (PTactic' t) where put x1 ByReflection x1 -> do putWord8 20 put x1 - ProofSearch x1 x2 x3 x4 x5 -> do putWord8 21 - put x1 - put x2 - put x3 - put x4 - put x5 + ProofSearch x1 x2 x3 x4 x5 x6 -> do putWord8 21 + put x1 + put x2 + put x3 + put x4 + put x5 + put x6 DoUnify -> putWord8 22 CaseTac x1 -> do putWord8 23 put x1 @@ -1954,7 +1955,8 @@ instance (Binary t) => Binary (PTactic' t) where x3 <- get x4 <- get x5 <- get - return (ProofSearch x1 x2 x3 x4 x5) + x6 <- get + return (ProofSearch x1 x2 x3 x4 x5 x6) 22 -> return DoUnify 23 -> do x1 <- get return (CaseTac x1) diff --git a/src/Idris/IdrisDoc.hs b/src/Idris/IdrisDoc.hs index 752ec118b..7ee69af97 100644 --- a/src/Idris/IdrisDoc.hs +++ b/src/Idris/IdrisDoc.hs @@ -360,8 +360,8 @@ extractPTactic (MatchRefine n) = [n] extractPTactic (LetTac n p) = n : extract p extractPTactic (LetTacTy n p1 p2) = n : concatMap extract [p1, p2] extractPTactic (Exact p) = extract p -extractPTactic (ProofSearch _ _ _ m ns) | Just n <- m = n : ns -extractPTactic (ProofSearch _ _ _ _ ns) = ns +extractPTactic (ProofSearch _ _ _ m _ ns) | Just n <- m = n : ns +extractPTactic (ProofSearch _ _ _ _ _ ns) = ns extractPTactic (Try t1 t2) = concatMap extractPTactic [t1, t2] extractPTactic (TSeq t1 t2) = concatMap extractPTactic [t1, t2] extractPTactic (ApplyTactic p) = extract p diff --git a/src/Idris/Interactive.hs b/src/Idris/Interactive.hs index 43846caed..061470a22 100644 --- a/src/Idris/Interactive.hs +++ b/src/Idris/Interactive.hs @@ -213,12 +213,13 @@ doProofSearch fn updatefile rec l n hints (Just depth) [] -> return n ns -> ierror (CantResolveAlts ns) i <- getIState - let (top, envlen, _) = case lookup mn (idris_metavars i) of - Just (t, e, False) -> (t, e, False) - _ -> (Nothing, 0, True) + let (top, envlen, psnames, _) + = case lookup mn (idris_metavars i) of + Just (t, e, ns, False) -> (t, e, ns, False) + _ -> (Nothing, 0, [], True) let fc = fileFC fn - let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints)) - (ProofSearch rec False depth t hints)] + let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints)) + (ProofSearch rec False depth t psnames hints)] let def = PClause fc mn (PRef fc [] mn) [] (body top) [] newmv <- idrisCatch (do elabDecl' EAll recinfo (PClauses fc [] mn [def]) @@ -297,7 +298,7 @@ makeLemma fn updatefile l n ns -> ierror (CantResolveAlts (map fst ns)) i <- getIState margs <- case lookup n (idris_metavars i) of - Just (_, arity, _) -> return arity + Just (_, arity, _, _) -> return arity _ -> return (-1) if (not isProv) then do diff --git a/src/Idris/ParseExpr.hs b/src/Idris/ParseExpr.hs index 42fca12bf..c69edf4a6 100644 --- a/src/Idris/ParseExpr.hs +++ b/src/Idris/ParseExpr.hs @@ -971,7 +971,7 @@ autoImplicit opts st syn sc <- expr syn highlightP kw AnnKeyword return (bindList (PPi - (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc) + (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc) defaultImplicit opts st syn = do kw <- reservedFC "default" @@ -1436,7 +1436,7 @@ tactics = , noArgs ["unify"] DoUnify , (["search"], Nothing, const $ do depth <- option 10 $ fst <$> natural - return (ProofSearch True True (fromInteger depth) Nothing [])) + return (ProofSearch True True (fromInteger depth) Nothing [] [])) , noArgs ["instance"] TCInstance , noArgs ["solve"] Solve , noArgs ["attack"] Attack diff --git a/src/Idris/ProofSearch.hs b/src/Idris/ProofSearch.hs index c3d26ca3d..3e620d176 100644 --- a/src/Idris/ProofSearch.hs +++ b/src/Idris/ProofSearch.hs @@ -22,10 +22,10 @@ import Debug.Trace -- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm trivial :: (PTerm -> ElabD ()) -> IState -> ElabD () -trivial = trivialHoles [] +trivial = trivialHoles [] [] -trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD () -trivialHoles ok elab ist +trivialHoles :: [Name] -> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD () +trivialHoles psnames ok elab ist = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False]) return ()) (do env <- get_env @@ -41,7 +41,7 @@ trivialHoles ok elab ist g <- goal -- anywhere but the top is okay for a hole, if holesOK set if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b)) - holesOK hs (binderTy b) + holesOK hs (binderTy b) && (null psnames || x `elem` psnames) then try' (elab (PRef (fileFC "prf") [] x)) (tryAll xs) True else tryAll xs @@ -73,9 +73,11 @@ proofSearch :: Bool -> -- recursive search (False for 'refine') Bool -> -- ambiguity ok Bool -> -- defer on failure Int -> -- maximum depth - (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] -> + (PTerm -> ElabD ()) -> Maybe Name -> Name -> + [Name] -> + [Name] -> IState -> ElabD () -proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist +proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn] ist = do -- get all possible versions of the name, take the first one that -- works let all_imps = lookupCtxtName fn (idris_implicits ist) @@ -106,7 +108,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist isImp (PImp p _ _ _ _) = (True, p) isImp arg = (True, priority arg) -- try to get all of them by unification -proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist +proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist = do compute ty <- goal hs <- get_holes @@ -177,7 +179,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist ty <- goal when (S.member ty tys) $ fail "Been here before" let tys' = S.insert ty tys - try' (trivial elab ist) + try' (trivialHoles psnames [] elab ist) (try' (try' (resolveByCon (d - 1) locs tys') (resolveByLocals (d - 1) locs tys') True) @@ -215,7 +217,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist tryLocals d locs tys [] = fail "Locals failed" tryLocals d locs tys ((x, t) : xs) - | x `elem` locs = tryLocals d locs tys xs + | x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs | otherwise = try' (tryLocal d (x : locs) tys x t) (tryLocals d locs tys xs) True diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs index 60cdc3291..c89cabf37 100644 --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -904,8 +904,8 @@ process fn (Check (PRef _ _ n)) case lookupNames n ctxt of ts@(t:_) -> case lookup t (idris_metavars ist) of - Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist True) $ - showMetavarInfo ppo ist n i + Just (_, i, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $ + showMetavarInfo ppo ist n i Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts) [] -> iPrintError $ "No such variable " ++ show n where @@ -1079,7 +1079,7 @@ process fn (RmProof n') insertMetavar n = do i <- getIState let ms = idris_metavars i - putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms } + putIState $ i { idris_metavars = (n, (Nothing, 0, [], False)) : ms } process fn' (AddProof prf) = do fn <- do @@ -1132,8 +1132,8 @@ process fn (Prove mode n') let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns n <- case metavars of [] -> ierror (Msg $ "Cannot find metavariable " ++ show n') - [(n, (_,_,False))] -> return n - [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover") + [(n, (_,_,_,False))] -> return n + [(_, (_,_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover") ns -> ierror (CantResolveAlts (map fst ns)) prover mode (lit fn) n -- recheck totality diff --git a/src/Idris/Reflection.hs b/src/Idris/Reflection.hs index cb3da6698..917ff0f66 100644 --- a/src/Idris/Reflection.hs +++ b/src/Idris/Reflection.hs @@ -76,7 +76,7 @@ reify _ t = fail ("Unknown tactic " ++ show t) reifyApp :: IState -> Name -> [Term] -> ElabD PTactic reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r) reifyApp _ t [Constant (I i)] - | t == reflm "Search" = return (ProofSearch True True i Nothing []) + | t == reflm "Search" = return (ProofSearch True True i Nothing [] []) reifyApp _ t [x] | t == reflm "Refine" = do n <- reifyTTName x return $ Refine n [] @@ -307,7 +307,7 @@ reifyTTBinderApp reif f [x, y] reifyTTBinderApp reif f [t] | f == reflm "Hole" = liftM Hole (reif t) reifyTTBinderApp reif f [t] - | f == reflm "GHole" = liftM (GHole 0) (reif t) + | f == reflm "GHole" = liftM (GHole 0 []) (reif t) reifyTTBinderApp reif f [x, y] | f == reflm "Guess" = liftM2 Guess (reif x) (reif y) reifyTTBinderApp reif f [t] @@ -580,7 +580,7 @@ reflectBinderQuotePattern q ty unq (Hole t) fill $ reflCall "Hole" [ty, Var t'] solve focus t'; q unq t -reflectBinderQuotePattern q ty unq (GHole _ t) +reflectBinderQuotePattern q ty unq (GHole _ _ t) = do t' <- claimTy (sMN 0 "ty") ty; movelast t' fill $ reflCall "GHole" [ty, Var t'] solve @@ -731,7 +731,7 @@ reflectBinderQuote q ty unq (NLet x y) = reflCall "NLet" [Var ty, q unq x, q unq y] reflectBinderQuote q ty unq (Hole t) = reflCall "Hole" [Var ty, q unq t] -reflectBinderQuote q ty unq (GHole _ t) +reflectBinderQuote q ty unq (GHole _ _ t) = reflCall "GHole" [Var ty, q unq t] reflectBinderQuote q ty unq (Guess x y) = reflCall "Guess" [Var ty, q unq x, q unq y] diff --git a/test/interactive003/expected b/test/interactive003/expected index 9c6d2612a..9434501a6 100644 --- a/test/interactive003/expected +++ b/test/interactive003/expected @@ -2,3 +2,4 @@ ys x :: app xs ys [] f x y :: vzipWith f xs ys +?word_length_rhs_3 :: word_length xs diff --git a/test/interactive003/input b/test/interactive003/input index f8c7587af..0b4229f32 100644 --- a/test/interactive003/input +++ b/test/interactive003/input @@ -2,3 +2,4 @@ :ps 5 app_rhs_2 :ps 8 vzipWith_rhs_3 :ps 9 vzipWith_rhs_1 +:ps 13 word_length_rhs_2 diff --git a/test/interactive003/interactive003.idr b/test/interactive003/interactive003.idr index 1f14484b1..fa257a935 100644 --- a/test/interactive003/interactive003.idr +++ b/test/interactive003/interactive003.idr @@ -8,3 +8,8 @@ vzipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c vzipWith f [] [] = ?vzipWith_rhs_3 vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_1 +word_length : Vect n String -> Vect n Nat +word_length [] = [] +word_length (x :: xs) = ?word_length_rhs_2 + +