e1ba862 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Find best matching types first in :search with a priority queue.

e1ba862bmsherman12 years ago

src/Idris/TypeSearch.hs+84−68

compare with master

unifiedsplit

@@ -1,3 +1,5 @@

1+{-# LANGUAGE ScopedTypeVariables #-}

1module Idris.TypeSearch (

3module Idris.TypeSearch (

2 searchByType, searchPred, defaultScoreFunction

4 searchByType, searchPred, defaultScoreFunction

3) where

5) where

@@ -6,12 +8,12 @@ import Control.Applicative ((<$>), (<*>), (<|>))

6import Control.Arrow (first, second, (&&&))

8import Control.Arrow (first, second, (&&&))

7import Control.Monad (forM_, guard)

9import Control.Monad (forM_, guard)

9−import Data.Function (on)

10import Data.List (find, delete, deleteBy, minimumBy, partition, sortBy, (\\))

11import Data.List (find, delete, deleteBy, minimumBy, partition, sortBy, (\\))

11import Data.Map (Map)

12import Data.Map (Map)

12import qualified Data.Map as M

13import qualified Data.Map as M

13−import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList)

14+import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList, mapMaybe)

14import Data.Monoid (Monoid (mempty, mappend))

15import Data.Monoid (Monoid (mempty, mappend))

16+import Data.Ord (comparing)

15import qualified Data.PriorityQueue.FingerTree as Q

17import qualified Data.PriorityQueue.FingerTree as Q

16import Data.Set (Set)

18import Data.Set (Set)

17import qualified Data.Set as S

19import qualified Data.Set as S

@@ -24,14 +26,14 @@ import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,

24import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

26import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

25import Idris.Core.TT hiding (score)

27import Idris.Core.TT hiding (score)

26import Idris.Core.Unify (match_unify)

28import Idris.Core.Unify (match_unify)

27−import Idris.Delaborate (delab, delabTy)

29+import Idris.Delaborate (delabTy)

28import Idris.Docstrings (noDocs, overview)

30import Idris.Docstrings (noDocs, overview)

29import Idris.ElabDecls (elabType')

31import Idris.ElabDecls (elabType')

30−import Idris.Output (ihRenderResult, ihPrintResult, ihPrintFunTypes)

32+import Idris.Output (ihRenderResult)

32import System.IO (Handle)

34import System.IO (Handle)

34−import Util.Pretty (text, vsep, char, (<>), Doc)

36+import Util.Pretty (text, char, (<>), Doc)

36searchByType :: Handle -> PTerm -> Idris ()

38searchByType :: Handle -> PTerm -> Idris ()

37searchByType h pterm = do

39searchByType h pterm = do

@@ -42,40 +44,29 @@ searchByType h pterm = do

42 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'

44 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'

43 putIState i -- don't actually make any changes

45 putIState i -- don't actually make any changes

44 let names = searchUsing searchPred i ty

46 let names = searchUsing searchPred i ty

45− let names' = take numLimit $

47+ let names' = take numLimit $ names

46− sortBy (compare `on` getScore) names

47 let docs =

48 let docs =

48 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in

49 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in

49 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

50 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

50− | (n, (_,score)) <- names']

51+ | (n, score) <- names']

51− ihRenderResult h $ vsep docs

52+ mapM_ (ihRenderResult h) docs

52 where

53 where

53− getScore = defaultScoreFunction . snd . snd

54 numLimit = 50

55 syn = defaultSyntax { implicitAllowed = True } -- syntax

56 n = sMN 0 "searchType" -- name

58-- | Conduct a type-directed search using a given match predicate

59−searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]

59+searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])

60+ -> IState -> Type -> [(Name, a)]

60−searchUsing pred istate ty =

61+searchUsing pred istate ty = pred istate nty . concat . M.elems $

61− concat . M.elems $ M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)

62+ M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)

62 where

63 where

64+ nty = normaliseC ctxt [] ty

63 ctxt = tt_ctxt istate

65 ctxt = tt_ctxt istate

64 f k x = do

66 f k x = do

65 guard $ not (special k)

67 guard $ not (special k)

66− y <- get (fst4 x)

68+ type2 <- typeFromDef x

67− let ny = normaliseC ctxt [] y

68− val <- pred istate nty ny

69− return (y, val)

70− nty = normaliseC ctxt [] ty

69+ return $ normaliseC ctxt [] type2

71− fst4 :: (a,b,c,d) -> a

72− fst4 (w,x,y,z) = w

73− get :: Def -> Maybe Type

74− get (Function ty tm) = Just ty

75− get (TyDecl _ ty) = Just ty

76− -- get (Operator ty _ _) = Just ty

77− get (CaseOp _ ty _ _ _ _) = Just ty

78− get _ = Nothing

79 special :: Name -> Bool

70 special :: Name -> Bool

80 special (NS n ns) = special n

71 special (NS n ns) = special n

81 special (SN _) = True

72 special (SN _) = True

@@ -83,10 +74,10 @@ searchUsing pred istate ty =

83 special _ = False

74 special _ = False

85-- Our default search predicate.

76-- Our default search predicate.

86−searchPred :: IState -> Type -> Type -> Maybe Score

77+searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]

87searchPred istate ty1 = matcher where

78searchPred istate ty1 = matcher where

88 maxScore = 100

79 maxScore = 100

89− matcher = unifyWithHoles istate maxScore ty1

80+ matcher = matchTypesBulk istate maxScore ty1

92typeFromDef :: (Def, b, c, d) -> Maybe Type

83typeFromDef :: (Def, b, c, d) -> Maybe Type

@@ -98,6 +89,8 @@ typeFromDef (def, _, _, _) = get def where

98 get (CaseOp _ ty _ _ _ _) = Just ty

89 get (CaseOp _ ty _ _ _ _) = Just ty

99 get _ = Nothing

90 get _ = Nothing

100

92+

93+-- | reverse the edges for a directed acyclic graph

101reverseDag :: Ord k => [((k, a), Set k)] -> [((k, a), Set k)]

94reverseDag :: Ord k => [((k, a), Set k)] -> [((k, a), Set k)]

102reverseDag xs = map f xs where

95reverseDag xs = map f xs where

103 f ((k, v), _) = ((k, v), S.fromList . map (fst . fst) $ filter (S.member k . snd) xs)

96 f ((k, v), _) = ((k, v), S.fromList . map (fst . fst) $ filter (S.member k . snd) xs)

@@ -138,6 +131,7 @@ usedVars inj = f where

138 f (V j) = error "unexpected! run vToP first"

131 f (V j) = error "unexpected! run vToP first"

139 f _ = M.empty

132 f _ = M.empty

140

133

134+-- | Remove a node from a directed acyclic graph

141deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]

135deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]

142deleteFromDag name [] = []

136deleteFromDag name [] = []

143deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2

137deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2

@@ -148,13 +142,13 @@ deleteFromArgList :: Ord n => n -> [(n, TT n)] -> [(n, TT n)]

148deleteFromArgList n = filter ((/= n) . fst)

142deleteFromArgList n = filter ((/= n) . fst)

149

143

150data Score = Score

144data Score = Score

151− { transposition :: Int

145+ { transposition :: !Int

152− , leftApplied :: Int

146+ , leftApplied :: !Int

153− , rightApplied :: Int

147+ , rightApplied :: !Int

154− , leftTypeClassApp :: Int

148+ , leftTypeClassApp :: !Int

155− , rightTypeClassApp :: Int

149+ , rightTypeClassApp :: !Int

156− , leftTypeClassIntro :: Int

150+ , leftTypeClassIntro :: !Int

157− , rightTypeClassIntro :: Int } deriving (Eq, Show)

151+ , rightTypeClassIntro :: !Int } deriving (Eq, Show)

158

152

159displayScore :: Score -> Doc a

153displayScore :: Score -> Doc a

160displayScore (Score trans lapp rapp lclassapp rclassapp lclassintro rclassintro) = text $ case (lt, gt) of

154displayScore (Score trans lapp rapp lclassapp rclassapp lclassintro rclassintro) = text $ case (lt, gt) of

@@ -168,7 +162,7 @@ displayScore (Score trans lapp rapp lclassapp rclassapp lclassintro rclassintro)

168

162

169scoreCriterion :: Score -> Bool

163scoreCriterion :: Score -> Bool

170scoreCriterion (Score a b c d e f g) = not

164scoreCriterion (Score a b c d e f g) = not

171− ( (b > 0 && c > 0) || (b + c) > 4 || d > 3 || e > 3 )

165+ ( (b > 0 && c > 0) || (b + c) > 4 || any (> 3) [d,e,f,g])

172

166

173defaultScoreFunction :: Score -> Int

167defaultScoreFunction :: Score -> Int

174defaultScoreFunction (Score a b c d e f g) = a + 9*b + 3*c + 12*d + 4*e + 6*f + 2*g + 100*(2*b + d + f)*(2*c + e + g)

168defaultScoreFunction (Score a b c d e f g) = a + 9*b + 3*c + 12*d + 4*e + 6*f + 2*g + 100*(2*b + d + f)*(2*c + e + g)

@@ -185,12 +179,12 @@ type ArgsDAG = [((Name, Type), (Int, Set Name))]

185

179

186-- | The state corresponding to an attempted match of two types.

180-- | The state corresponding to an attempted match of two types.

187data State = State

181data State = State

188− { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved

182+ { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved

189− , args1 :: !ArgsDAG -- ^ arguments for the left type which have yet to be resolved

183+ , args1 :: !ArgsDAG -- ^ arguments for the left type which have yet to be resolved

190− , args2 :: !ArgsDAG -- ^ arguments for the right type which have yet to be resolved

184+ , args2 :: !ArgsDAG -- ^ arguments for the right type which have yet to be resolved

191− , classes1 :: ![(Name, Type)] -- ^ typeclass arguments for the left type which haven't been resolved

185+ , classes1 :: ![(Name, Type)] -- ^ typeclass arguments for the left type which haven't been resolved

192− , classes2 :: ![(Name, Type)] -- ^ typeclass arguments for the right type which haven't been resolved

186+ , classes2 :: ![(Name, Type)] -- ^ typeclass arguments for the right type which haven't been resolved

193− , score :: !Score -- ^ the score so far

187+ , score :: !Score -- ^ the score so far

194 , usedNames :: ![Name] -- ^ all names that have been used

188 , usedNames :: ![Name] -- ^ all names that have been used

195 } deriving Show

189 } deriving Show

196

190

@@ -243,8 +237,9 @@ isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt c

243

237

244

238

245instance Ord Score where

239instance Ord Score where

246− compare = compare `on` defaultScoreFunction

240+ compare = comparing defaultScoreFunction

247

241

242+-- | Compute the power set

248subsets :: [a] -> [[a]]

243subsets :: [a] -> [[a]]

249subsets [] = [[]]

244subsets [] = [[]]

250subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss

245subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss

@@ -252,22 +247,43 @@ subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss

252

247

253--DONT run vToP first!

248--DONT run vToP first!

254-- | Try to match two types together in a unification-like procedure.

249-- | Try to match two types together in a unification-like procedure.

255−-- Returns a list of possible scores representing ways in which the two

250+-- Returns a list of types and their minimum scores, sorted in order

256−-- types can be matched.

251+-- of increasing score.

257−unifyWithHoles :: IState -> Int -> Type -> Type -> Maybe Score

252+matchTypesBulk :: forall info. IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]

258−unifyWithHoles istate maxScore type1 = \type2 -> let

253+matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues where

259− (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)

254+ getStartQueue :: (info, Type) -> Maybe (Score, (info, Q.PQueue Score State))

260− argNames2 = map fst dag2

255+ getStartQueue nty@(info, type2) = do

261− usedNames = map fst (argNames1 ++ argNames2)

262− startingHoles = argNames1 ++ argNames2

263−

264− startingTypes = (retTy1, retTy2) : []

265− in do

266− state <- unifyQueue (State startingHoles dag1 dag2

256+ state <- unifyQueue (State startingHoles dag1 dag2

267 typeClassArgs1 typeClassArgs2

257 typeClassArgs1 typeClassArgs2

268 mempty usedNames) startingTypes

258 mempty usedNames) startingTypes

259+ let sc = score state

269− getResults (Q.singleton (score state) state)

260+ return $ (sc, (info, Q.singleton sc state))

270− where

261+ where

262+ (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)

263+ argNames2 = map fst dag2

264+ usedNames = map fst (argNames1 ++ argNames2)

265+ startingHoles = argNames1 ++ argNames2

266+

267+ startingTypes = (retTy1, retTy2) : []

268+

269+

270+ startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)

271+ startQueueOfQueues = Q.fromList $ mapMaybe getStartQueue types

272+

273+ getAllResults :: Q.PQueue Score (info, Q.PQueue Score State) -> [(info, Score)]

274+ getAllResults q = case Q.minViewWithKey q of

275+ Nothing -> []

276+ Just ((nextScore, (info, stateQ)), q') ->

277+ if defaultScoreFunction nextScore <= maxScore

278+ then case nextStepsQueue stateQ of

279+ Nothing -> getAllResults q'

280+ Just (Left stateQ') -> case Q.minViewWithKey stateQ' of

281+ Nothing -> getAllResults q'

282+ Just ((newQscore,_), _) -> getAllResults (Q.add newQscore (info, stateQ') q')

283+ Just (Right score) -> (info, score) : getAllResults q'

284+ else []

285+

286+

271 ctxt = tt_ctxt istate

287 ctxt = tt_ctxt istate

272 classInfo = idris_classes istate

288 classInfo = idris_classes istate

273

289

@@ -301,14 +317,14 @@ unifyWithHoles istate maxScore type1 = \type2 -> let

301

317

302 resolveUnis ((name, term) : xs)

318 resolveUnis ((name, term) : xs)

303 state@(State holes args1 args2 _ _ _ _) = case (findLeft name state, findRight name state) of

319 state@(State holes args1 args2 _ _ _ _) = case (findLeft name state, findRight name state) of

304− (Just (_,ix), Nothing) -> first (inScore (\score -> score { leftApplied = succ (leftApplied score) })) <$> nextStep

320+ (Just (_,ix), Nothing) -> first (inScore (\score -> score { leftApplied = succ (leftApplied score) })) <$> nextStep

305− (Nothing, Just (_, ix)) -> first (inScore (\score -> score { rightApplied = succ (rightApplied score) })) <$> nextStep

321+ (Nothing, Just (_, ix)) -> first (inScore (\score -> score { rightApplied = succ (rightApplied score) })) <$> nextStep

306− (Nothing, Nothing) -> nextStep

322+ (Nothing, Nothing) -> nextStep

307− _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)

323+ _ -> error ("Idris internal error: TypeSearch.resolveUnis")

308 where

324 where

309 -- find variables which are determined uniquely by the type

325 -- find variables which are determined uniquely by the type

310 -- due to injectivity

326 -- due to injectivity

311− varsInTy = M.keys $ usedVars True term --[]

327+ varsInTy = M.keys $ usedVars True term

312 toDelete = name : varsInTy

328 toDelete = name : varsInTy

313 deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]

329 deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]

314

330

@@ -342,17 +358,17 @@ unifyWithHoles istate maxScore type1 = \type2 -> let

342 getClassName (P (TCon _ _) className _) = [className]

358 getClassName (P (TCon _ _) className _) = [className]

343 getClassName _ = []

359 getClassName _ = []

344

360

345−

361+ -- Just if the computation hasn't totally failed yet, Nothing if it has

362+ -- Left if we haven't found a terminal state, Right if we have

346− getResults :: Q.PQueue Score State -> Maybe Score

363+ nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)

347− getResults queue = do

364+ nextStepsQueue queue = do

348 ((nextScore, next), rest) <- Q.minViewWithKey queue

365 ((nextScore, next), rest) <- Q.minViewWithKey queue

349− guard (defaultScoreFunction nextScore <= maxScore)

350 if isFinal next

366 if isFinal next

351− then return nextScore

367+ then Just $ Right nextScore

352 else let additions = if scoreCriterion nextScore

368 else let additions = if scoreCriterion nextScore

353 then Q.fromList [ (score state, state) | state <- nextSteps next ]

369 then Q.fromList [ (score state, state) | state <- nextSteps next ]

354 else Q.empty in

370 else Q.empty in

355− getResults (Q.union rest additions)

371+ Just $ Left (Q.union rest additions)

356 where

372 where

357 isFinal (State [] [] [] [] [] score _) = True

373 isFinal (State [] [] [] [] [] score _) = True

358 isFinal _ = False

374 isFinal _ = False