git.iko.soy/Idris-dev
on master help sign in
Use a priority queue to improve performance when matching types in :search
e1ef65dbmsherman
idris.cabal+1
compare with master
unifiedsplit
@@ -622,6 +622,7 @@ Library
622 , directory
622 , directory
623 , directory >= 1.2
623 , directory >= 1.2
624 , filepath
624 , filepath
625+ , fingertree >= 0.1
625 , haskeline >= 0.7
626 , haskeline >= 0.7
626 , language-java >= 0.2.6
627 , language-java >= 0.2.6
627 , lens >= 4.1.1
628 , lens >= 4.1.1
src/Idris/TypeSearch.hs+31−20
@@ -12,6 +12,7 @@ import Data.Map (Map)
12import qualified Data.Map as M
12import qualified Data.Map as M
13import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList)
13import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList)
14import Data.Monoid (Monoid (mempty, mappend))
14import Data.Monoid (Monoid (mempty, mappend))
15+import qualified Data.PriorityQueue.FingerTree as Q
15import Data.Set (Set)
16import Data.Set (Set)
16import qualified Data.Set as S
17import qualified Data.Set as S
17import qualified Data.Text as T (pack, isPrefixOf)
18import qualified Data.Text as T (pack, isPrefixOf)
@@ -41,7 +42,7 @@ searchByType h pterm = do
41 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'
42 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'
42 putIState i -- don't actually make any changes
43 putIState i -- don't actually make any changes
43 let names = searchUsing searchPred i ty
44 let names = searchUsing searchPred i ty
44− let names' = take numLimit . takeWhile ((< scoreLimit) . getScore) $
45+ let names' = take numLimit $
45 sortBy (compare `on` getScore) names
46 sortBy (compare `on` getScore) names
46 let docs =
47 let docs =
47 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in
48 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in
@@ -51,7 +52,6 @@ searchByType h pterm = do
51 where
52 where
52 getScore = defaultScoreFunction . snd . snd
53 getScore = defaultScoreFunction . snd . snd
53 numLimit = 50
54 numLimit = 50
54− scoreLimit = 100
55 syn = defaultSyntax { implicitAllowed = True } -- syntax
55 syn = defaultSyntax { implicitAllowed = True } -- syntax
56 n = sMN 0 "searchType" -- name
56 n = sMN 0 "searchType" -- name
57
57
@@ -84,10 +84,9 @@ searchUsing pred istate ty =
84
84
85-- Our default search predicate.
85-- Our default search predicate.
86searchPred :: IState -> Type -> Type -> Maybe Score
86searchPred :: IState -> Type -> Type -> Maybe Score
87−searchPred istate ty1 = \ty2 -> case matcher ty2 of
87+searchPred istate ty1 = matcher where
88− xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)
88+ maxScore = 100
89− where
90− matcher = unifyWithHoles istate ty1
89+ matcher = unifyWithHoles istate maxScore ty1
91
90
92
91
93typeFromDef :: (Def, b, c, d) -> Maybe Type
92typeFromDef :: (Def, b, c, d) -> Maybe Type
@@ -237,22 +236,25 @@ isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt c
237 getClassName _ = []
236 getClassName _ = []
238
237
239
238
239+instance Ord Score where
240+ compare = compare `on` defaultScoreFunction
241+
240--DONT run vToP first!
242--DONT run vToP first!
241-- | Try to match two types together in a unification-like procedure.
243-- | Try to match two types together in a unification-like procedure.
242-- Returns a list of possible scores representing ways in which the two
244-- Returns a list of possible scores representing ways in which the two
243-- types can be matched.
245-- types can be matched.
244−unifyWithHoles :: IState -> Type -> Type -> [Score]
246+unifyWithHoles :: IState -> Int -> Type -> Type -> Maybe Score
245−unifyWithHoles istate type1 = \type2 -> let
247+unifyWithHoles istate maxScore type1 = \type2 -> let
246 (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders argNames1 type2)
248 (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders argNames1 type2)
247 argNames2 = map (fst . fst) dag2
249 argNames2 = map (fst . fst) dag2
248 startingHoles = argNames1 ++ argNames2
250 startingHoles = argNames1 ++ argNames2
249
251
250 startingTypes = (retTy1, retTy2) : []
252 startingTypes = (retTy1, retTy2) : []
253+ in do
251− in case unifyQueue (State startingHoles dag1 dag2
254+ state <- unifyQueue (State startingHoles dag1 dag2
252 typeClassArgs1 typeClassArgs2
255 typeClassArgs1 typeClassArgs2
253 mempty startingHoles) startingTypes
256 mempty startingHoles) startingTypes
254− of Nothing -> []
257+ getResults (Q.singleton (score state) state)
255− Just state -> possibleMatches state
256 where
258 where
257 ctxt = tt_ctxt istate
259 ctxt = tt_ctxt istate
258 classInfo = idris_classes istate
260 classInfo = idris_classes istate
@@ -327,20 +329,29 @@ unifyWithHoles istate type1 = \type2 -> let
327 getClassName _ = []
329 getClassName _ = []
328
330
329
331
330− collect :: [State] -> [Score]
332+ getResults :: Q.PQueue Score State -> Maybe Score
331− collect states = concat [ possibleMatches state | state <- states, scoreCriterion (score state) ]
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
332
346
333 -- | Find all possible matches starting from a given state.
347 -- | Find all possible matches starting from a given state.
334 -- We go in stages rather than concatenating all three results in hopes of narrowing
348 -- We go in stages rather than concatenating all three results in hopes of narrowing
335 -- the search tree. Once we advance in a phase, there should be no going back.
349 -- the search tree. Once we advance in a phase, there should be no going back.
336− possibleMatches :: State -> [Score]
350+ nextSteps :: State -> [State]
337−
338− -- Stage 3 - we're done!
339− possibleMatches (State [] [] [] [] [] scoreAcc _) = [scoreAcc]
340
351
341 -- Stage 2 - match typeclasses
352 -- Stage 2 - match typeclasses
342− possibleMatches (State [] [] [] c1 c2 scoreAcc usedNames) =
353+ nextSteps (State [] [] [] c1 c2 scoreAcc usedNames) =
343− collect (if null results2 then results3 else results2)
354+ if null results2 then results3 else results2
344 where
355 where
345 -- try to match a typeclass argument from the left with a typeclass argument from the right
356 -- try to match a typeclass argument from the left with a typeclass argument from the right
346 results2 =
357 results2 =
@@ -367,7 +378,7 @@ unifyWithHoles istate type1 = \type2 -> let
367 , let newHoles = map fst newClassArgs ]
378 , let newHoles = map fst newClassArgs ]
368
379
369 -- Stage 1 - match arguments
380 -- 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
371
382
372 -- we only try to match arguments whose names don't appear in the types
383 -- we only try to match arguments whose names don't appear in the types
373 -- of any other arguments
384 -- of any other arguments