Merge pull request #503 from edwinb/search0-heuristic

Add a heuristic for sorting search results

src/Idris/REPL.idr

@@ -427,7 +427,8 @@ processEdit (GenerateDef upd line name rej)
              | Nothing => pure (EditError ("Can't find declaration for " ++ show name ++ " on line " ++ show line))
          case !(lookupDefExact n' (gamma defs)) of
               Just None =>
-                 do let searchdef = makeDef (\p, n => onLine (line - 1) p) n'
+                 do let searchdef = makeDefSort (\p, n => onLine (line - 1) p)
+                                                16 mostUsed n'
                     ropts <- get ROpts
                     put ROpts (record { gdResult = Just (line, searchdef) } ropts)
                     Just (_, (fc, cs)) <- nextGenDef rej

src/TTImp/Interactive/ExprSearch.idr

@@ -88,19 +88,40 @@ filterS p (Result r next)
 export
 searchN : {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
-          Nat -> Core (Search a) -> Core (List a)
+          Nat -> Core (Search a) -> Core (List a, Core (Search a))
 searchN max s
     = tryUnify
          (do res <- s
              xs <- count max res
              pure xs)
-         (pure [])
+         (pure ([], pure NoMore))
   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)
+    count : Nat -> Search a -> Core (List a, Core (Search a))
+    count k NoMore = pure ([], pure NoMore)
+    count Z _ = pure ([], pure NoMore)
+    count (S Z) (Result a next) = pure ([a], next)
+    count (S k) (Result a next)
+        = do (rest, cont) <- count k !next
+             pure $ (a :: rest, cont)
+
+-- Generate definitions in batches, and sort according to some user provided
+-- heuristic (highest proportion of bound variables used is a good one!)
+export
+searchSort : {auto c : Ref Ctxt Defs} ->
+             {auto u : Ref UST UState} ->
+             Nat -> Core (Search a) ->
+             (a -> a -> Ordering) ->
+             Core (Search a)
+searchSort max s ord
+    = do (batch, next) <- searchN max s
+         if isNil batch
+            then pure NoMore
+            else returnBatch (sortBy ord batch) next
+  where
+    returnBatch : List a -> Core (Search a) -> Core (Search a)
+    returnBatch [] res = searchSort max res ord
+    returnBatch (res :: xs) x
+        = pure (Result res (returnBatch xs x))
 
 export
 nextResult : {auto c : Ref Ctxt Defs} ->
@@ -248,6 +269,8 @@ searchName fc rigc opts env target topty defining (n, ndef)
                                  (fullname ndef) (visibility ndef)
              | _ => noResult
          let ty = type ndef
+         let True = usableName (fullname ndef)
+             | _ => noResult
          let namety : NameType
                  = case definition ndef of
                         DCon tag arity _ => DataCon tag arity
@@ -267,6 +290,14 @@ searchName fc rigc opts env target topty defining (n, ndef)
          args' <- traverse (searchIfHole fc opts defining topty env)
                            args
          mkCandidates fc (Ref fc namety n) args'
+  where
+    -- we can only use the name in a search result if it's a user writable
+    -- name (so, no recursive with blocks or case blocks, for example)
+    usableName : Name -> Bool
+    usableName (UN _) = True
+    usableName (NS _ n) = usableName n
+    usableName (Nested _ n) = usableName n
+    usableName _ = False
 
 getSuccessful : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
@@ -628,4 +659,5 @@ exprSearchN : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               FC -> Nat -> Name -> List Name -> Core (List ClosedTerm)
 exprSearchN fc max n hints
-    = searchN max (exprSearch fc n hints)
+    = do (res, _) <- searchN max (exprSearch fc n hints)
+         pure res

src/TTImp/Interactive/GenerateDef.idr

@@ -222,10 +222,54 @@ makeDef p n
                pure (map (\c => (loc, c)) cs'))
            noResult
 
+-- Given a clause, return the bindable names, and the ones that were used in
+-- the rhs
+bindableUsed : ImpClause -> Maybe (List Name, List Name)
+bindableUsed (PatClause fc lhs rhs)
+    = let lhsns = findIBindVars lhs
+          rhsns = findAllNames [] rhs in
+          Just (lhsns, filter (\x => x `elem` lhsns) rhsns)
+bindableUsed _ = Nothing
+
+propBindableUsed : List ImpClause -> Double
+propBindableUsed def
+    = let (b, u) = getProp def in
+          if b == Z
+             then 1.0
+             else the Double (cast u) / the Double (cast b)
+  where
+    getProp : List ImpClause -> (Nat, Nat)
+    getProp [] = (0, 0)
+    getProp (c :: xs)
+        = let (b, u) = getProp xs in
+              case bindableUsed c of
+                   Nothing => (b, u)
+                   Just (b', u') => (b + length (nub b'), u + length (nub u'))
+
+-- Sort by highest proportion of bound variables used. This recalculates every
+-- time it looks, which might seem expensive, but it's only inspecting (not
+-- constructing anything) and it would make the code ugly if we avoid that.
+-- Let's see if it's a bottleneck before doing anything about it...
+export
+mostUsed : List ImpClause -> List ImpClause -> Ordering
+mostUsed def1 def2 = compare (propBindableUsed def2) (propBindableUsed def1)
+
+export
+makeDefSort : {auto c : Ref Ctxt Defs} ->
+              {auto m : Ref MD Metadata} ->
+              {auto u : Ref UST UState} ->
+              (FC -> (Name, Nat, ClosedTerm) -> Bool) ->
+              Nat -> (List ImpClause -> List ImpClause -> Ordering) ->
+              Name -> Core (Search (FC, List ImpClause))
+makeDefSort p max ord n
+    = searchSort max (makeDef p n) (\x, y => ord (snd x) (snd y))
+
 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)
+makeDefN p max n
+    = do (res, _) <- searchN max (makeDef p n)
+         pure res

tests/idris2/interactive005/expected

@@ -6,7 +6,7 @@ Main> append [] ys = ys
 append (x :: xs) ys = x :: append xs ys
 Main> lappend [] ys = ys
 lappend (x :: xs) ys = x :: lappend xs ys
-Main> zipWith f [] ys = []
+Main> zipWith f [] [] = []
 zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
 Main> lookup Here (ECons x es) = x
 lookup (There p) (ECons x es) = lookup p es

tests/idris2/interactive010/expected

@@ -1,4 +1,4 @@
 1/1: Building IEdit (IEdit.idr)
-Main>     zipHere [] ys = []
+Main>     zipHere [] [] = []
     zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
 Main> Bye for now!

tests/idris2/interactive015/expected

@@ -5,28 +5,31 @@ Main> append [] ys = ys
 append (x :: xs) ys = x :: append xs ys
 Main> append [] ys = ys
 append (x :: xs) [] = x :: append xs []
-append (x :: xs) (y :: ys) = x :: append xs (x :: ys)
+append (x :: xs) (y :: ys) = x :: append xs (y :: ys)
 Main> lappend [] ys = ys
 lappend (x :: xs) ys = x :: lappend xs ys
 Main> lappend [] ys = ys
 lappend (x :: xs) ys = x :: lappend ys xs
 Main> lappend [] ys = ys
 lappend (x :: xs) ys = lappend xs (x :: ys)
-Main> lappend1 xs ys = ys
-Main> lappend1 xs ys = xs
-Main> lappend1 xs ys = []
 Main> lappend1 [] ys = ys
-lappend1 (x :: xs) ys = xs
+lappend1 (x :: xs) ys = x :: lappend1 xs ys
 Main> lappend1 [] ys = ys
-lappend1 (x :: xs) ys = ys
+lappend1 (x :: xs) ys = x :: lappend1 xs (x :: ys)
 Main> lappend1 [] ys = ys
-lappend1 (x :: xs) ys = []
+lappend1 (x :: xs) ys = x :: lappend1 xs (x :: (x :: ys))
 Main> lappend1 [] ys = ys
 lappend1 (x :: xs) ys = x :: lappend1 xs xs
 Main> lappend1 [] ys = ys
-lappend1 (x :: xs) ys = x :: lappend1 xs ys
+lappend1 (x :: xs) ys = x :: lappend1 xs []
 Main> lappend1 [] ys = ys
-lappend1 (x :: xs) ys = x :: lappend1 xs ys
+lappend1 (x :: xs) ys = x :: lappend1 xs (x :: xs)
+Main> lappend1 [] ys = ys
+lappend1 (x :: xs) ys = x :: lappend1 xs [x]
+Main> lappend1 [] ys = ys
+lappend1 (x :: xs) ys = x :: lappend1 xs (x :: (x :: xs))
+Main> lappend1 [] ys = ys
+lappend1 (x :: xs) ys = x :: lappend1 xs (x :: (x :: xs))
 Main> ys
 Main> []
 Main> lappend2 ys ys

tests/idris2/literate003/expected

@@ -6,7 +6,7 @@ Main> > append [] ys = ys
 > append (x :: xs) ys = x :: append xs ys
 Main> > lappend [] ys = ys
 > lappend (x :: xs) ys = x :: lappend xs ys
-Main> > zipWith f [] ys = []
+Main> > zipWith f [] [] = []
 > zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
 Main> > lookup Here (ECons x es) = x
 > lookup (There p) (ECons x es) = lookup p es

tests/idris2/literate007/expected

@@ -1,8 +1,8 @@
 1/1: Building IEdit (IEdit.lidr)
-Main> >     zipHere [] ys = []
+Main> >     zipHere [] [] = []
 >     zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
 Main> Bye for now!
 1/1: Building IEditOrg (IEditOrg.org)
-Main> #+IDRIS:     zipHere [] ys = []
+Main> #+IDRIS:     zipHere [] [] = []
 #+IDRIS:     zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
 Main> Bye for now!

tests/idris2/literate011/expected

@@ -1,4 +1,4 @@
 1/1: Building IEdit (IEdit.md)
-Main>     zipHere [] ys = []
+Main>     zipHere [] [] = []
     zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
 Main> Bye for now!