From f8ef44f1b049d7cf24a0e006434ca312c38fa122 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Mon, 27 Jul 2020 12:04:39 +0100 Subject: [PATCH] Allow multiple results from generate-defs Return a 'Search' rather than a single definition. Also, change the order of search in expressions so that we look at recursive calls earlier when under a constructor - the assumption being that this is more likely than nested constructors. --- src/Idris/IDEMode/REPL.idr | 2 +- src/Idris/Parser.idr | 7 +- src/Idris/REPL.idr | 28 ++++-- src/Idris/Syntax.idr | 2 +- src/TTImp/Interactive/ExprSearch.idr | 131 ++++++++++++++++++-------- src/TTImp/Interactive/GenerateDef.idr | 78 +++++++++------ src/Yaffle/REPL.idr | 6 +- 7 files changed, 167 insertions(+), 87 deletions(-) diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 6fa6fd9d3..c332e659e 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -170,7 +170,7 @@ process (ExprSearch l n hs all) = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n) (map UN hs) all)) process (GenerateDef l n) - = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n))) + = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n) False)) process (MakeLemma l n) = replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n))) process (MakeCase l n) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index a1575a100..577d6f263 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1720,7 +1720,12 @@ editCmd upd <- option False (do symbol "!"; pure True) line <- intLit n <- name - pure (GenerateDef upd (fromInteger line) n) + pure (GenerateDef upd (fromInteger line) n False) + <|> do replCmd ["gdall"] + upd <- option False (do symbol "!"; pure True) + line <- intLit + n <- name + pure (GenerateDef upd (fromInteger line) n True) <|> do replCmd ["ml", "makelemma"] upd <- option False (do symbol "!"; pure True) line <- intLit diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 4aeec84ed..87a5e3661 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -336,7 +336,7 @@ processEdit (ExprSearch upd line name hints all) let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn) case !(lookupDefName name (gamma defs)) of [(n, nidx, Hole locs _)] => - do tms <- exprSearchN replFC 1 name [] + do tms <- exprSearchN replFC (if all then 20 else 1) name [] defs <- get Ctxt restms <- traverse (normaliseHoles defs []) tms itms <- the (Core (List PTerm)) @@ -375,23 +375,33 @@ processEdit (ExprSearch upd line name hints all) dropLams Z env tm = (_ ** (env, tm)) dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc dropLams _ env tm = (_ ** (env, tm)) -processEdit (GenerateDef upd line name) +processEdit (GenerateDef upd line name all) = do defs <- get Ctxt Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine (line - 1) p) | Nothing => pure (EditError ("Can't find declaration for " ++ show name ++ " on line " ++ show line)) case !(lookupDefExact n' (gamma defs)) of Just None => handleUnify - (do Just (fc, cs) <- makeDef (\p, n => onLine (line - 1) p) n' - | Nothing => pure $ EditError $ "Can't find a definition for " ++ show n' + (do progs <- makeDefN (\p, n => onLine (line - 1) p) + (if all then 20 else 1) + n' Just srcLine <- getSourceLine line | Nothing => pure (EditError "Source line not found") let (markM, srcLineUnlit) = isLitLine srcLine - let l : Nat = integerToNat (cast (snd (startPos fc))) - ls <- traverse (printClause markM l) cs - if upd - then updateFile (addClause (unlines ls) (integerToNat (cast line))) - else pure $ DisplayEdit ls) + if all + then do ls <- traverse (\ (fc, cs) => + do let l : Nat = integerToNat (cast (snd (startPos fc))) + res <- traverse (printClause markM l) cs + pure (res ++ ["----"])) progs + pure $ DisplayEdit (concat ls) + else case progs of + [] => pure (EditError "No search results") + ((fc, cs) :: _) => + do let l : Nat = integerToNat (cast (snd (startPos fc))) + ls <- traverse (printClause markM l) cs + if upd + then updateFile (addClause (unlines ls) (integerToNat (cast line))) + else pure $ DisplayEdit ls) (\err => pure $ EditError $ "Can't find a definition for " ++ show n' ++ ": " ++ show err) Just _ => pure $ EditError "Already defined" Nothing => pure $ EditError $ "Can't find declaration for " ++ show name diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 34903d131..84da61c5a 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -385,7 +385,7 @@ data EditCmd : Type where CaseSplit : Bool -> Int -> Int -> Name -> EditCmd AddClause : Bool -> Int -> Name -> EditCmd ExprSearch : Bool -> Int -> Name -> List Name -> Bool -> EditCmd - GenerateDef : Bool -> Int -> Name -> EditCmd + GenerateDef : Bool -> Int -> Name -> Bool -> EditCmd MakeLemma : Bool -> Int -> Name -> EditCmd MakeCase : Bool -> Int -> Name -> EditCmd MakeWith : Bool -> Int -> Name -> EditCmd diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index 354c58724..0d6b08a6c 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/src/TTImp/Interactive/ExprSearch.idr @@ -42,6 +42,7 @@ record SearchOpts where holesOK : Bool recOK : Bool depth : Nat + inArg : Bool export data Search : Type -> Type where @@ -62,6 +63,10 @@ export one : a -> Core (Search a) one res = pure $ Result res (pure NoMore) +export +noResult : Core (Search a) +noResult = pure NoMore + export traverse : (a -> Core b) -> Search a -> Core (Search b) traverse f NoMore = pure NoMore @@ -80,6 +85,26 @@ filterS p (Result r next) then pure $ Result r fnext else fnext +export +searchN : {auto c : Ref Ctxt Defs} -> + {auto m : Ref MD Metadata} -> + {auto u : Ref UST UState} -> + Nat -> Core (Search a) -> Core (List a) +searchN max s + = tryUnify + (do foo <- getNextEntry + res <- s + xs <- count max res + pure xs) + (pure []) + where + count : Nat -> Search a -> Core (List a) + count k NoMore = pure [] + count Z _ = pure [] + count (S Z) (Result a next) = pure [a] + count (S k) (Result a next) = pure $ a :: !(count k !next) + + search : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> @@ -111,17 +136,18 @@ searchIfHole : {vars : _} -> Core (Search (Term vars)) searchIfHole fc opts defining topty env arg = case depth opts of - Z => pure NoMore + Z => noResult S k => do let hole = holeID arg let rig = argRig arg defs <- get Ctxt Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs) - | Nothing => pure NoMore + | Nothing => noResult let Hole _ _ = definition gdef | _ => one !(normaliseHoles defs env (metaApp arg)) -- already solved - res <- search fc rig (record { depth = k} opts) + res <- search fc rig (record { depth = k, + inArg = True } opts) defining topty (Resolved hole) -- When we solve an argument, we're also building a lambda -- expression for its environment, so we need to apply it to @@ -137,9 +163,9 @@ explicit ai firstSuccess : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> - List (Core (Search (Term vars))) -> - Core (Search (Term vars)) -firstSuccess [] = pure NoMore + List (Core (Search a)) -> + Core (Search a) +firstSuccess [] = noResult firstSuccess (elab :: elabs) = do ust <- get UST defs <- get Ctxt @@ -148,13 +174,39 @@ firstSuccess (elab :: elabs) pure (Result res (continue ust defs (more :: elabs)))) (\err => continue ust defs elabs) where - continue : UState -> Defs -> List (Core (Search (Term vars))) -> - Core (Search (Term vars)) + continue : UState -> Defs -> List (Core (Search a)) -> + Core (Search a) continue ust defs elabs = do put UST ust put Ctxt defs firstSuccess elabs +export +trySearch : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + Core (Search a) -> + Core (Search a) -> + Core (Search a) +trySearch s1 s2 = firstSuccess [s1, s2] + +export +combine : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + (a -> b -> t) -> Search a -> Search b -> Core (Search t) +combine f NoMore y = pure NoMore +combine f (Result x next) NoMore = pure NoMore +combine f (Result x nextx) (Result y nexty) + = pure $ Result (f x y) $ + (do nexty' <- nexty + combine f !(one x) nexty') + `trySearch` + ((do nextx' <- nextx + combine f nextx' !(one y)) + `trySearch` + (do nextx' <- nextx + nexty' <- nexty + combine f nextx' nexty')) + mkCandidates : {vars : _} -> {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> @@ -163,7 +215,7 @@ mkCandidates : {vars : _} -> -- out of arguments, we have a candidate mkCandidates fc f [] = one f -- argument has run out of ideas, we're stuck -mkCandidates fc f (NoMore :: argss) = pure NoMore +mkCandidates fc f (NoMore :: argss) = noResult -- make a candidate from 'f arg' applied to the rest of the arguments mkCandidates fc f (Result arg next :: argss) = firstSuccess @@ -185,7 +237,7 @@ searchName fc rigc opts env target topty defining (n, ndef) = do defs <- get Ctxt let True = visibleInAny (!getNS :: !getNestedNS) (fullname ndef) (visibility ndef) - | _ => pure NoMore + | _ => noResult let ty = type ndef let namety : NameType = case definition ndef of @@ -199,7 +251,7 @@ searchName fc rigc opts env target topty defining (n, ndef) logNF 10 "App type" env appTy ures <- unify inSearch fc env target appTy let [] = constraints ures - | _ => pure NoMore + | _ => noResult -- Search the explicit arguments first, they may resolve other holes traverse (searchIfHole fc opts defining topty env) (filter explicit args) @@ -230,7 +282,7 @@ getSuccessful {vars} fc rig opts mkHole env ty topty defining all (Hole (length env) (holeInit False)) False one tm - else pure NoMore + else noResult r => pure r searchNames : {vars : _} -> @@ -241,7 +293,7 @@ searchNames : {vars : _} -> Term vars -> ClosedTerm -> Maybe RecData -> List Name -> Core (Search (Term vars)) searchNames fc rig opts env ty topty defining [] - = pure NoMore + = noResult searchNames fc rig opts env ty topty defining (n :: ns) = do defs <- get Ctxt vis <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns) @@ -268,11 +320,11 @@ tryRecursive : {vars : _} -> Env Term vars -> Term vars -> ClosedTerm -> Maybe RecData -> Core (Search (Term vars)) tryRecursive fc rig opts env ty topty Nothing - = pure NoMore + = noResult tryRecursive fc rig opts env ty topty (Just rdata) = do defs <- get Ctxt case !(lookupCtxtExact (recname rdata) (gamma defs)) of - Nothing => pure NoMore + Nothing => noResult Just def => do res <- searchName fc rig opts env !(nf defs env ty) topty Nothing @@ -337,7 +389,7 @@ searchLocalWith : {vars : _} -> Term vars -> ClosedTerm -> Maybe RecData -> Core (Search (Term vars)) searchLocalWith fc rig opts env [] ty topty defining - = pure NoMore + = noResult searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining = do defs <- get Ctxt nty <- nf defs env ty @@ -364,11 +416,11 @@ searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining mkCandidates fc (f prf) []) (do ures <- unify inTerm fc env ty appTy let [] = constraints ures - | _ => pure NoMore + | _ => noResult args' <- traverse (searchIfHole fc opts defining topty env) args mkCandidates fc (f prf) args') - else pure NoMore + else noResult findPos : Defs -> Term vars -> (Term vars -> Term vars) -> @@ -401,7 +453,7 @@ searchLocalWith {vars} fc rig opts env ((p, pty) :: rest) ty topty defining ytytm, f arg]) ytynf target)] - else pure NoMore)] + else noResult)] findPos defs prf f nty target = findDirect defs prf f nty target searchLocal : {vars : _} -> @@ -455,14 +507,22 @@ searchType fc rig opts env defining topty _ ty -- Then try a recursive call log 10 $ "Hints found for " ++ show n ++ " " ++ show allHints - getSuccessful fc rig opts True env ty topty defining - ([searchLocal fc rig opts env ty topty defining, - searchNames fc rig opts env ty topty defining - allHints] - ++ if recOK opts - then [tryRecursive fc rig opts env ty topty defining] - else []) - else pure NoMore + let tries = + [searchLocal fc rig opts env ty topty defining, + searchNames fc rig opts env ty topty defining allHints] + let tryRec = + if recOK opts + then [tryRecursive fc rig opts env ty topty defining] + else [] + -- if we're in an argument, try the recursive call + -- first. We're more likely to want that than nested + -- constructors. + let allns : List _ + = if inArg opts + then tryRec ++ tries + else tries ++ tryRec + getSuccessful fc rig opts True env ty topty defining allns + else noResult _ => do logTerm 10 "Searching locals only at" ty getSuccessful fc rig opts True env ty topty defining ([searchLocal fc rig opts env ty topty defining] @@ -522,7 +582,7 @@ getLHSData defs (Just tm) = pure $ getLHS !(normaliseHoles defs [] tm) firstLinearOK : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> FC -> Search ClosedTerm -> Core (Search ClosedTerm) -firstLinearOK fc NoMore = pure NoMore +firstLinearOK fc NoMore = noResult firstLinearOK fc (Result t next) = tryUnify (do linearCheck fc linear False [] t @@ -541,7 +601,7 @@ exprSearch fc n_in hints | Nothing => throw (UndefinedName fc n_in) lhs <- findHoleLHS !(getFullName (Resolved idx)) log 10 $ "LHS hole data " ++ show (n, lhs) - res <- search fc (multiplicity gdef) (MkSearchOpts False True 5) + res <- search fc (multiplicity gdef) (MkSearchOpts False True 5 False) !(getLHSData defs lhs) (type gdef) n firstLinearOK fc res where @@ -559,15 +619,4 @@ exprSearchN : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> FC -> Nat -> Name -> List Name -> Core (List ClosedTerm) exprSearchN fc max n hints - = tryUnify - (do foo <- getNextEntry - res <- exprSearch fc n hints - xs <- count max res - pure xs) - (pure []) - where - count : Nat -> Search a -> Core (List a) - count k NoMore = pure [] - count Z _ = pure [] - count (S Z) (Result a next) = pure [a] - count (S k) (Result a next) = pure $ a :: !(count k !next) + = searchN max (exprSearch fc n hints) diff --git a/src/TTImp/Interactive/GenerateDef.idr b/src/TTImp/Interactive/GenerateDef.idr index 3797033e3..78edf9e44 100644 --- a/src/TTImp/Interactive/GenerateDef.idr +++ b/src/TTImp/Interactive/GenerateDef.idr @@ -53,12 +53,12 @@ expandClause : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> FC -> Int -> ImpClause -> - Core (List ImpClause) + Core (Search (List ImpClause)) expandClause loc n c = do c <- uniqueRHS c Right clause <- checkClause linear Private False n [] (MkNested []) [] c - | Left err => pure [] -- TODO: impossible clause, do something - -- appropriate + | Left err => noResult -- TODO: impossible clause, do something + -- appropriate let MkClause {vars} env lhs rhs = clause let Meta _ i fn _ = getFn rhs @@ -67,16 +67,16 @@ expandClause loc n c Just (Hole locs _) <- lookupDefExact (Resolved fn) (gamma defs) | _ => throw (GenericMsg loc "No searchable hole on RHS") log 10 $ "Expression search for " ++ show (i, fn) - (rhs' :: _) <- exprSearchN loc 1 (Resolved fn) [] - | _ => throw (GenericMsg loc "No result found for search on RHS") - defs <- get Ctxt - rhsnf <- normaliseHoles defs [] rhs' - let (_ ** (env', rhsenv)) = dropLams locs [] rhsnf + rhs' <- exprSearch loc (Resolved fn) [] + traverse (\rhs' => + do defs <- get Ctxt + rhsnf <- normaliseHoles defs [] rhs' + let (_ ** (env', rhsenv)) = dropLams locs [] rhsnf - rhsraw <- unelab env' rhsenv - logTermNF 5 "Got clause" env lhs - logTermNF 5 " = " env' rhsenv - pure [updateRHS c rhsraw] + rhsraw <- unelab env' rhsenv + logTermNF 5 "Got clause" env lhs + logTermNF 5 " = " env' rhsenv + pure [updateRHS c rhsraw]) rhs' where updateRHS : ImpClause -> RawImp -> ImpClause updateRHS (PatClause fc lhs _) rhs = PatClause fc lhs rhs @@ -149,46 +149,54 @@ generateSplits {c} {m} {u} loc fn (PatClause fc lhs rhs) (IBindHere loc PATTERN lhs) Nothing traverse (trySplit fc lhs lhstm rhs) (splittableNames lhs) +collectClauses : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + List (Search (List ImpClause)) -> + Core (Search (List ImpClause)) +collectClauses [] = one [] +collectClauses (x :: xs) + = do xs' <- collectClauses xs + combine (++) x xs' + mutual tryAllSplits : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> - FC -> Int -> Error -> + FC -> Int -> List (Name, List ImpClause) -> - Core (List ImpClause) - tryAllSplits loc n err [] = throw err - tryAllSplits loc n err ((x, []) :: rest) - = tryAllSplits loc n err rest - tryAllSplits loc n err ((x, cs) :: rest) + Core (Search (List ImpClause)) + tryAllSplits loc n [] = noResult + tryAllSplits loc n ((x, []) :: rest) + = tryAllSplits loc n rest + tryAllSplits loc n ((x, cs) :: rest) = do log 5 $ "Splitting on " ++ show x - tryUnify (do cs' <- traverse (mkSplits loc n) cs - pure (concat cs')) - (tryAllSplits loc n err rest) + trySearch (do cs' <- traverse (mkSplits loc n) cs + collectClauses cs') + (tryAllSplits loc n rest) mkSplits : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> FC -> Int -> ImpClause -> - Core (List ImpClause) + Core (Search (List ImpClause)) -- If the clause works, use it. Otherwise, split on one of the splittable -- variables and try all of the resulting clauses mkSplits loc n c - = handleUnify + = trySearch (expandClause loc n c) - (\err => - do cs <- generateSplits loc n c - log 5 $ "Splits: " ++ show cs - tryAllSplits loc n err cs) + (do cs <- generateSplits loc n c + log 5 $ "Splits: " ++ show cs + tryAllSplits loc n cs) export makeDef : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> (FC -> (Name, Nat, ClosedTerm) -> Bool) -> - Name -> Core (Maybe (FC, List ImpClause)) + Name -> Core (Search (FC, List ImpClause)) makeDef p n = do Just (loc, nidx, envlen, ty) <- findTyDeclAt p - | Nothing => pure Nothing + | Nothing => noResult n <- getFullName nidx logTerm 5 ("Searching for " ++ show n) ty tryUnify @@ -211,5 +219,13 @@ makeDef p n put Ctxt defs put MD meta put UST ust - pure (Just (loc, cs'))) - (pure Nothing) + pure (map (\c => (loc, c)) cs')) + noResult + +export +makeDefN : {auto c : Ref Ctxt Defs} -> + {auto m : Ref MD Metadata} -> + {auto u : Ref UST UState} -> + (FC -> (Name, Nat, ClosedTerm) -> Bool) -> + Nat -> Name -> Core (List (FC, List ImpClause)) +makeDefN p max n = searchN max (makeDef p n) diff --git a/src/Yaffle/REPL.idr b/src/Yaffle/REPL.idr index 58101452f..6a08e7b84 100644 --- a/src/Yaffle/REPL.idr +++ b/src/Yaffle/REPL.idr @@ -89,9 +89,9 @@ process (GenerateDef line name) case !(lookupDefExact n' (gamma defs)) of Just None => catch - (do Just (fc, cs) <- logTime "Generation" $ - makeDef (\p, n => onLine line p) n' - | Nothing => coreLift (putStrLn "Failed") + (do ((fc, cs) :: _) <- logTime "Generation" $ + makeDefN (\p, n => onLine line p) 1 n' + | _ => coreLift (putStrLn "Failed") coreLift $ putStrLn (show cs)) (\err => coreLift $ putStrLn $ "Can't find a definition for " ++ show n') Just _ => coreLift $ putStrLn "Already defined"