@@ -1,3 +1,5 @@
1+{-# LANGUAGE ScopedTypeVariables #-}
2+
13module Idris.TypeSearch (
24 searchByType, searchPred, defaultScoreFunction
35) where
@@ -6,12 +8,12 @@ import Control.Applicative ((<$>), (<*>), (<|>))
68import Control.Arrow (first, second, (&&&))
79import Control.Monad (forM_, guard)
810
9−import Data.Function (on)
1011import Data.List (find, delete, deleteBy, minimumBy, partition, sortBy, (\\))
1112import Data.Map (Map)
1213import qualified Data.Map as M
13−import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList)
14+import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList, mapMaybe)
1415import Data.Monoid (Monoid (mempty, mappend))
16+import Data.Ord (comparing)
1517import qualified Data.PriorityQueue.FingerTree as Q
1618import Data.Set (Set)
1719import qualified Data.Set as S
@@ -24,14 +26,14 @@ import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,
2426import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
2527import Idris.Core.TT hiding (score)
2628import Idris.Core.Unify (match_unify)
27−import Idris.Delaborate (delab, delabTy)
29+import Idris.Delaborate (delabTy)
2830import Idris.Docstrings (noDocs, overview)
2931import Idris.ElabDecls (elabType')
30−import Idris.Output (ihRenderResult, ihPrintResult, ihPrintFunTypes)
32+import Idris.Output (ihRenderResult)
3133
3234import System.IO (Handle)
3335
34−import Util.Pretty (text, vsep, char, (<>), Doc)
36+import Util.Pretty (text, char, (<>), Doc)
3537
3638searchByType :: Handle -> PTerm -> Idris ()
3739searchByType h pterm = do
@@ -42,40 +44,29 @@ searchByType h pterm = do
4244 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'
4345 putIState i -- don't actually make any changes
4446 let names = searchUsing searchPred i ty
45− let names' = take numLimit $
46− sortBy (compare `on` getScore) names
47+ let names' = take numLimit $ names
4748 let docs =
4849 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in
4950 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo
50− | (n, (_,score)) <- names']
51− ihRenderResult h $ vsep docs
51+ | (n, score) <- names']
52+ mapM_ (ihRenderResult h) docs
5253 where
53− getScore = defaultScoreFunction . snd . snd
5454 numLimit = 50
5555 syn = defaultSyntax { implicitAllowed = True } -- syntax
5656 n = sMN 0 "searchType" -- name
5757
5858-- | Conduct a type-directed search using a given match predicate
59−searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]
60−searchUsing pred istate ty =
61− concat . M.elems $ M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
59+searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])
60+ -> IState -> Type -> [(Name, a)]
61+searchUsing pred istate ty = pred istate nty . concat . M.elems $
62+ M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
6263 where
64+ nty = normaliseC ctxt [] ty
6365 ctxt = tt_ctxt istate
6466 f k x = do
6567 guard $ not (special k)
66− y <- get (fst4 x)
67− let ny = normaliseC ctxt [] y
68− val <- pred istate nty ny
69− return (y, val)
70− nty = normaliseC ctxt [] ty
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
68+ type2 <- typeFromDef x
69+ return $ normaliseC ctxt [] type2
7970 special :: Name -> Bool
8071 special (NS n ns) = special n
8172 special (SN _) = True
@@ -83,10 +74,10 @@ searchUsing pred istate ty =
8374 special _ = False
8475
8576-- Our default search predicate.
86−searchPred :: IState -> Type -> Type -> Maybe Score
77+searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]
8778searchPred istate ty1 = matcher where
8879 maxScore = 100
89− matcher = unifyWithHoles istate maxScore ty1
80+ matcher = matchTypesBulk istate maxScore ty1
9081
9182
9283typeFromDef :: (Def, b, c, d) -> Maybe Type
@@ -98,6 +89,8 @@ typeFromDef (def, _, _, _) = get def where
9889 get (CaseOp _ ty _ _ _ _) = Just ty
9990 get _ = Nothing
10091
92+
93+-- | reverse the edges for a directed acyclic graph
10194reverseDag :: Ord k => [((k, a), Set k)] -> [((k, a), Set k)]
10295reverseDag xs = map f xs where
10396 f ((k, v), _) = ((k, v), S.fromList . map (fst . fst) $ filter (S.member k . snd) xs)
@@ -138,6 +131,7 @@ usedVars inj = f where
138131 f (V j) = error "unexpected! run vToP first"
139132 f _ = M.empty
140133
134+-- | Remove a node from a directed acyclic graph
141135deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
142136deleteFromDag name [] = []
143137deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2
@@ -148,13 +142,13 @@ deleteFromArgList :: Ord n => n -> [(n, TT n)] -> [(n, TT n)]
148142deleteFromArgList n = filter ((/= n) . fst)
149143
150144data Score = Score
151− { transposition :: Int
152− , leftApplied :: Int
153− , rightApplied :: Int
154− , leftTypeClassApp :: Int
155− , rightTypeClassApp :: Int
156− , leftTypeClassIntro :: Int
157− , rightTypeClassIntro :: Int } deriving (Eq, Show)
145+ { transposition :: !Int
146+ , leftApplied :: !Int
147+ , rightApplied :: !Int
148+ , leftTypeClassApp :: !Int
149+ , rightTypeClassApp :: !Int
150+ , leftTypeClassIntro :: !Int
151+ , rightTypeClassIntro :: !Int } deriving (Eq, Show)
158152
159153displayScore :: Score -> Doc a
160154displayScore (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)
168162
169163scoreCriterion :: Score -> Bool
170164scoreCriterion (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])
172166
173167defaultScoreFunction :: Score -> Int
174168defaultScoreFunction (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))]
185179
186180-- | The state corresponding to an attempted match of two types.
187181data State = State
188− { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved
189− , 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
191− , 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
193− , score :: !Score -- ^ the score so far
182+ { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved
183+ , args1 :: !ArgsDAG -- ^ arguments for the left type which have yet to be resolved
184+ , args2 :: !ArgsDAG -- ^ arguments for the right type which have yet to be resolved
185+ , classes1 :: ![(Name, Type)] -- ^ typeclass arguments for the left type which haven't been resolved
186+ , classes2 :: ![(Name, Type)] -- ^ typeclass arguments for the right type which haven't been resolved
187+ , score :: !Score -- ^ the score so far
194188 , usedNames :: ![Name] -- ^ all names that have been used
195189 } deriving Show
196190
@@ -243,8 +237,9 @@ isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt c
243237
244238
245239instance Ord Score where
246− compare = compare `on` defaultScoreFunction
240+ compare = comparing defaultScoreFunction
247241
242+-- | Compute the power set
248243subsets :: [a] -> [[a]]
249244subsets [] = [[]]
250245subsets (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
252247
253248--DONT run vToP first!
254249-- | Try to match two types together in a unification-like procedure.
255−-- Returns a list of possible scores representing ways in which the two
256−-- types can be matched.
257−unifyWithHoles :: IState -> Int -> Type -> Type -> Maybe Score
258−unifyWithHoles istate maxScore type1 = \type2 -> let
259− (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)
260− argNames2 = map fst dag2
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
250+-- Returns a list of types and their minimum scores, sorted in order
251+-- of increasing score.
252+matchTypesBulk :: forall info. IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
253+matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues where
254+ getStartQueue :: (info, Type) -> Maybe (Score, (info, Q.PQueue Score State))
255+ getStartQueue nty@(info, type2) = do
256+ state <- unifyQueue (State startingHoles dag1 dag2
267257 typeClassArgs1 typeClassArgs2
268258 mempty usedNames) startingTypes
269− getResults (Q.singleton (score state) state)
270− where
259+ let sc = score state
260+ return $ (sc, (info, Q.singleton sc state))
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+
271287 ctxt = tt_ctxt istate
272288 classInfo = idris_classes istate
273289
@@ -301,14 +317,14 @@ unifyWithHoles istate maxScore type1 = \type2 -> let
301317
302318 resolveUnis ((name, term) : xs)
303319 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
305− (Nothing, Just (_, ix)) -> first (inScore (\score -> score { rightApplied = succ (rightApplied score) })) <$> nextStep
306− (Nothing, Nothing) -> nextStep
307− _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)
320+ (Just (_,ix), Nothing) -> first (inScore (\score -> score { leftApplied = succ (leftApplied score) })) <$> nextStep
321+ (Nothing, Just (_, ix)) -> first (inScore (\score -> score { rightApplied = succ (rightApplied score) })) <$> nextStep
322+ (Nothing, Nothing) -> nextStep
323+ _ -> error ("Idris internal error: TypeSearch.resolveUnis")
308324 where
309325 -- find variables which are determined uniquely by the type
310326 -- due to injectivity
311− varsInTy = M.keys $ usedVars True term --[]
327+ varsInTy = M.keys $ usedVars True term
312328 toDelete = name : varsInTy
313329 deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]
314330
@@ -342,17 +358,17 @@ unifyWithHoles istate maxScore type1 = \type2 -> let
342358 getClassName (P (TCon _ _) className _) = [className]
343359 getClassName _ = []
344360
345−
346− getResults :: Q.PQueue Score State -> Maybe Score
347− getResults queue = do
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
363+ nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)
364+ nextStepsQueue queue = do
348365 ((nextScore, next), rest) <- Q.minViewWithKey queue
349− guard (defaultScoreFunction nextScore <= maxScore)
350366 if isFinal next
351− then return nextScore
367+ then Just $ Right nextScore
352368 else let additions = if scoreCriterion nextScore
353369 then Q.fromList [ (score state, state) | state <- nextSteps next ]
354370 else Q.empty in
355− getResults (Q.union rest additions)
371+ Just $ Left (Q.union rest additions)
356372 where
357373 isFinal (State [] [] [] [] [] score _) = True
358374 isFinal _ = False