@@ -12,6 +12,7 @@ import Data.Map (Map)
1212import qualified Data.Map as M
1313import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList)
1414import Data.Monoid (Monoid (mempty, mappend))
15+import qualified Data.PriorityQueue.FingerTree as Q
1516import Data.Set (Set)
1617import qualified Data.Set as S
1718import qualified Data.Text as T (pack, isPrefixOf)
@@ -41,7 +42,7 @@ searchByType h pterm = do
4142 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'
4243 putIState i -- don't actually make any changes
4344 let names = searchUsing searchPred i ty
44− let names' = take numLimit . takeWhile ((< scoreLimit) . getScore) $
45+ let names' = take numLimit $
4546 sortBy (compare `on` getScore) names
4647 let docs =
4748 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in
@@ -51,7 +52,6 @@ searchByType h pterm = do
5152 where
5253 getScore = defaultScoreFunction . snd . snd
5354 numLimit = 50
54− scoreLimit = 100
5555 syn = defaultSyntax { implicitAllowed = True } -- syntax
5656 n = sMN 0 "searchType" -- name
5757
@@ -84,10 +84,9 @@ searchUsing pred istate ty =
8484
8585-- Our default search predicate.
8686searchPred :: IState -> Type -> Type -> Maybe Score
87−searchPred istate ty1 = \ty2 -> case matcher ty2 of
88− xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)
89− where
90− matcher = unifyWithHoles istate ty1
87+searchPred istate ty1 = matcher where
88+ maxScore = 100
89+ matcher = unifyWithHoles istate maxScore ty1
9190
9291
9392typeFromDef :: (Def, b, c, d) -> Maybe Type
@@ -237,22 +236,25 @@ isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt c
237236 getClassName _ = []
238237
239238
239+instance Ord Score where
240+ compare = compare `on` defaultScoreFunction
241+
240242--DONT run vToP first!
241243-- | Try to match two types together in a unification-like procedure.
242244-- Returns a list of possible scores representing ways in which the two
243245-- types can be matched.
244−unifyWithHoles :: IState -> Type -> Type -> [Score]
245−unifyWithHoles istate type1 = \type2 -> let
246+unifyWithHoles :: IState -> Int -> Type -> Type -> Maybe Score
247+unifyWithHoles istate maxScore type1 = \type2 -> let
246248 (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders argNames1 type2)
247249 argNames2 = map (fst . fst) dag2
248250 startingHoles = argNames1 ++ argNames2
249251
250252 startingTypes = (retTy1, retTy2) : []
251− in case unifyQueue (State startingHoles dag1 dag2
253+ in do
254+ state <- unifyQueue (State startingHoles dag1 dag2
252255 typeClassArgs1 typeClassArgs2
253256 mempty startingHoles) startingTypes
254− of Nothing -> []
255− Just state -> possibleMatches state
257+ getResults (Q.singleton (score state) state)
256258 where
257259 ctxt = tt_ctxt istate
258260 classInfo = idris_classes istate
@@ -327,20 +329,29 @@ unifyWithHoles istate type1 = \type2 -> let
327329 getClassName _ = []
328330
329331
330− collect :: [State] -> [Score]
331− collect states = concat [ possibleMatches state | state <- states, scoreCriterion (score state) ]
332+ getResults :: Q.PQueue Score State -> Maybe Score
333+ getResults queue = do
334+ ((nextScore, next), rest) <- Q.minViewWithKey queue
335+ if isFinal next
336+ then return nextScore
337+ else do
338+ guard (defaultScoreFunction nextScore <= maxScore)
339+ let additions = if scoreCriterion nextScore
340+ then Q.fromList [ (score state, state) | state <- nextSteps next ]
341+ else Q.empty
342+ getResults (Q.union rest additions)
343+ where
344+ isFinal (State [] [] [] [] [] score _) = True
345+ isFinal _ = False
332346
333347 -- | Find all possible matches starting from a given state.
334348 -- We go in stages rather than concatenating all three results in hopes of narrowing
335349 -- the search tree. Once we advance in a phase, there should be no going back.
336− possibleMatches :: State -> [Score]
337−
338− -- Stage 3 - we're done!
339− possibleMatches (State [] [] [] [] [] scoreAcc _) = [scoreAcc]
350+ nextSteps :: State -> [State]
340351
341352 -- Stage 2 - match typeclasses
342− possibleMatches (State [] [] [] c1 c2 scoreAcc usedNames) =
343− collect (if null results2 then results3 else results2)
353+ nextSteps (State [] [] [] c1 c2 scoreAcc usedNames) =
354+ if null results2 then results3 else results2
344355 where
345356 -- try to match a typeclass argument from the left with a typeclass argument from the right
346357 results2 =
@@ -367,7 +378,7 @@ unifyWithHoles istate type1 = \type2 -> let
367378 , let newHoles = map fst newClassArgs ]
368379
369380 -- Stage 1 - match arguments
370− possibleMatches (State holes dag1 dag2 c1 c2 scoreAcc usedNames) = collect results1 where
381+ nextSteps (State holes dag1 dag2 c1 c2 scoreAcc usedNames) = results1 where
371382
372383 -- we only try to match arguments whose names don't appear in the types
373384 -- of any other arguments